Merge pull request #1092 from goblint/fix-gobview-search

Towards fixing GobView search: Avoid truncation of very large integers

scripts/test-gobview.py

@@ -61,6 +61,72 @@ def serve():
     panel = browser.find_element(By.CLASS_NAME, "panel")
     print("found DOM elements main, sidebar-left, sidebar-right, content and panel")
 
+    # test syntactic search
+    leftS.find_element(By.LINK_TEXT,  "Search").click()
+    leftS.find_element(By.CLASS_NAME, "switch-to-json").click()
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","fail"],"find":["uses"],"mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("syntactic search for variable use of 'fail' found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 2)
+    assert("tests/regression/00-sanity/01-assert.c:7" in locations)
+    assert("tests/regression/00-sanity/01-assert.c:12" in locations)
+
+    # clear results
+    leftS.find_element(By.CLASS_NAME, "clear-btn").click()
+
+    # test semantic search 1
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 1","mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("semantic search for variable use of 'success' where it must be 1 found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 2)
+    assert("tests/regression/00-sanity/01-assert.c:10" in locations)
+    assert("tests/regression/00-sanity/01-assert.c:5" in locations)
+
+    # clear results
+    leftS.find_element(By.CLASS_NAME, "clear-btn").click()
+
+    # test semantic search 2
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 0","mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("semantic search for variable use of 'success' where it must be 0 found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 0)
+
+    # close "No results found" alert
+    leftS.find_element(By.CLASS_NAME, "btn-close").click()
+
     cleanup(browser, thread)
 
 except Exception as e:

src/common/framework/cfgTools.ml

@@ -122,7 +122,6 @@ let rec pretty_edges () = function
   | [_,x] -> Edge.pretty_plain () x
   | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs
 
-
 let node_scc_global = NH.create 113
 
 exception Not_connect of fundec

src/common/util/cilfacade.ml

@@ -8,11 +8,9 @@ include Cilfacade0
 
 (** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *)
 let create_var (var: varinfo) =
-  (* TODO Hack: this offset should preempt conflicts with ids generated by CIL *)
-  let start_id = 10_000_000_000 in
+  (* Hack: using negative integers should preempt conflicts with ids generated by CIL *)
   let hash = Hashtbl.hash { var with vid = 0 } in
-  let hash = if hash < start_id then hash + start_id else hash in
-  { var with vid = hash }
+  { var with vid = - hash } (* Hashtbl.hash returns non-negative integer *)
 
 
 (** Is character type (N1570 6.2.5.15)? *)
@@ -531,9 +529,7 @@ let stmt_fundecs: fundec StmtH.t ResettableLazy.t =
 
 
 let get_pseudo_return_id fd =
-  let start_id = 10_000_000_000 in (* TODO get max_sid? *)
-  let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
-  if sid < start_id then sid + start_id else sid
+  - fd.svar.vid (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
 
 let pseudo_return_to_fun = StmtH.create 113
 

src/transform/expressionEvaluation.ml

@@ -17,7 +17,7 @@ type query =
     structure : (CodeQuery.structure [@default None_s]);
     limitation : (CodeQuery.constr [@default None_c]);
 
-    expression : string;
+    expression : (string option [@default None]);
     mode : [ `Must | `May ];
 
   } [@@deriving yojson]
@@ -60,7 +60,11 @@ struct
 
       val global_variables =
         file.globals
-        |> List.filter_map (function Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v) | _ -> None)
+        |> List.filter_map (function
+            | Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v)
+            | Cil.GFun (f, l) -> Some (f.svar.vname, Cil.Fv f.svar)
+            | Cil.GVarDecl (v, l) -> Some (v.vname, Cil.Fv v)
+            | _ -> None)
       val statements =
         file.globals
         |> List.filter_map (function Cil.GFun (f, _) -> Some f | _ -> None)
@@ -77,7 +81,7 @@ struct
         (* Compute the available local variables *)
         let local_variables =
           match Hashtbl.find_option statements location with
-          | Some (function_definition, _) -> function_definition.slocals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v)
+          | Some (fd, _) -> fd.slocals @ fd.sformals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v)
           | None -> []
         in
         (* Parse expression *)
@@ -191,8 +195,8 @@ struct
         |> List.group file_compare
         (* Sort, remove duplicates, ungroup *)
         |> List.concat_map (fun ls -> List.sort_uniq byte_compare ls)
-        (* Semantic queries *)
-        |> List.map (fun (n, l, s, i) -> ((n, l, s, i), evaluator#evaluate l query.expression))
+        (* Semantic queries if query.expression is some *)
+        |> List.map (fun (n, l, s, i) -> ((n, l, s, i), Option.map_default (evaluator#evaluate l) (Some true) query.expression))
       in
       let print ((_, loc, _, _), res) =
         match res with