diff --git a/gobview b/gobview index c8fcb09e9a..7cfdafd2db 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit c8fcb09e9a3e27de22d4803606d5784f667a542a +Subproject commit 7cfdafd2dbc6715007c5090a621581f454220658 diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py index 1ac8f6a76c..dcff1eac81 100644 --- a/scripts/test-gobview.py +++ b/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: diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index d47f1efde0..106f8eb5c3 100644 --- a/src/common/framework/cfgTools.ml +++ b/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 diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 4057359d3d..6100ab9a3c 100644 --- a/src/common/util/cilfacade.ml +++ b/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 diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index 8ebdbb9b58..2c7e61efd0 100644 --- a/src/transform/expressionEvaluation.ml +++ b/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