From 98bf2b5c4655722e5a1f451bdf7ebf1a0a9f3b49 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 19 Jun 2023 18:35:36 +0200 Subject: [PATCH 1/8] avoid truncation of very large integers --- src/framework/cfgTools.ml | 2 +- src/util/cilfacade.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index 8f98a48e84..85a1c73732 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -123,7 +123,7 @@ let rec pretty_edges () = function | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs let get_pseudo_return_id fd = - let start_id = 10_000_000_000 in (* TODO get max_sid? *) + let start_id = 1_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 diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index 09231b4f45..6d48770a50 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -9,7 +9,7 @@ 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 + let start_id = 1_000_000_000 in 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 } From 1fa71e1021902611a63f15e6f5296aabf440e6d2 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Wed, 21 Jun 2023 16:08:12 +0200 Subject: [PATCH 2/8] allow syntactic queries (no expression field) through Goblint --- src/transform/expressionEvaluation.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index 815e5742f6..56e73d815f 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] @@ -191,8 +191,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 From b6ac9e05e1920e6c997fc9125a4ba35cdcdcd94e Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 22 Jun 2023 11:08:48 +0200 Subject: [PATCH 3/8] use negative ids for varinfos generated by Goblint and pseudo return nodes --- src/framework/cfgTools.ml | 4 +--- src/util/cilfacade.ml | 6 ++---- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index 85a1c73732..f12dfbb590 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -123,9 +123,7 @@ let rec pretty_edges () = function | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs let get_pseudo_return_id fd = - let start_id = 1_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 + - (Hashtbl.hash 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 node_scc_global = NH.create 113 diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index 6d48770a50..b8d0aba906 100644 --- a/src/util/cilfacade.ml +++ b/src/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 = 1_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 } (** Is character type (N1570 6.2.5.15)? *) From 11ab2274d2e471d22249c7a2300f2236ba0d988d Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 26 Jun 2023 16:07:58 +0200 Subject: [PATCH 4/8] add test cases for syntactic and semantic search in GobView --- scripts/test-gobview.py | 66 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py index 0dc2cacaa4..5f6e3472d3 100644 --- a/scripts/test-gobview.py +++ b/scripts/test-gobview.py @@ -62,6 +62,72 @@ class Server(socketserver.TCPServer): 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, httpd, thread) except Exception as e: From 2b47ef1ec9cac53efb89738a88b3ceb811d6ec07 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 27 Jun 2023 19:30:36 +0200 Subject: [PATCH 5/8] allow for semantic search expressions with function pointers and function parameters --- src/transform/expressionEvaluation.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index 56e73d815f..bde704f0c9 100644 --- a/src/transform/expressionEvaluation.ml +++ b/src/transform/expressionEvaluation.ml @@ -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 *) From c2d6c6752b43bb2dd9de5f9d2c5aabe9db7a8ea5 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 26 Jan 2024 13:27:05 +0100 Subject: [PATCH 6/8] use function id instead of (possibly negative) hash --- src/framework/cfgTools.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index f12dfbb590..2555295902 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -123,7 +123,7 @@ let rec pretty_edges () = function | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs let get_pseudo_return_id fd = - - (Hashtbl.hash 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. *) + - 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 node_scc_global = NH.create 113 From 7bd3b4f5e60a6e13dac7e3f50eebaad800dc5977 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 1 Feb 2024 19:15:17 +0100 Subject: [PATCH 7/8] add comment --- src/common/util/cilfacade.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 276f67c78e..6100ab9a3c 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -10,7 +10,7 @@ include Cilfacade0 let create_var (var: varinfo) = (* Hack: using negative integers should preempt conflicts with ids generated by CIL *) let hash = Hashtbl.hash { var with vid = 0 } in - { var with vid = - hash } + { var with vid = - hash } (* Hashtbl.hash returns non-negative integer *) (** Is character type (N1570 6.2.5.15)? *) From d53037a7f56325ee0d117a5ff2ece234021d72aa Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 5 Feb 2024 15:50:23 +0100 Subject: [PATCH 8/8] update GobView submodule --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index c8fcb09e9a..7cfdafd2db 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit c8fcb09e9a3e27de22d4803606d5784f667a542a +Subproject commit 7cfdafd2dbc6715007c5090a621581f454220658