Semantic search returns no results

[keremc]

Semantic search returns no results.

Steps to reproduce the issue:

1. Run Goblint & start an HTTP server in the run directory:

$ ./goblint --enable gobview tests/regression/03-practical/06-callback.c && cd run && python3 -m http.server

2. Open the web UI. Scroll down until you see "Switch to JSON editor" and click it.
3. Enter the following query and click "Execute":

{"kind":["var"],"target":["name","x"],"find":["uses"],"expression":"x == 5","mode":["Must"]}

If you save the same query in a file (e.g., query.json) and execute the semantic search in the terminal like this, it returns the expected results:

$ ./goblint tests/regression/03-practical/06-callback.c --set 'trans.activated[+]' expeval --set trans.expeval.query_file_name query.json
tests/regression/03-practical/06-callback.c:9:3-9:8 [16587]
tests/regression/03-practical/06-callback.c:19:3-19:17 [16685]

[sofamaniac]

I have found the culprit.

gobview/src/state/search.ml

Lines 30 to 38 in f8c509d

	let execute (q : t) cil =
	if is_semantic q then (
	ExpressionEvaluation.gv_query := Some q;
	Maingoblint.do_analyze (Analyses.empty_increment_data cil) cil;
	let results = !ExpressionEvaluation.gv_results in
	let pred =
	if q.mode = `Must then snd %> Option.default false else snd %> Option.default true
	in
	results |> List.filter pred |> List.map fst)

The pred filter filters everything out

[sim642]

The real question then is why, because that pred hasn't recently been changed according to git blame, so the second components of results might've somehow changed to become all Some false or whatnot.

[michael-schwarz]

goblint/analyzer#651 contains some discussions, but no fix yet. This should be looked into again!

[michael-schwarz]

I'll check if this still happens.