Skip to content

Commit e5ec72d

Browse files
michael-schwarzmichael-schwarz
committed
Merge branch 'feature/syntactic_search' into develop
2 parents 1481c4d + a67a702 commit e5ec72d

File tree

14 files changed

+1865
-4
lines changed

14 files changed

+1865
-4
lines changed

‎META.goblint-cil.template‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
# DUNE_GEN
22

33
package "default-features" (
4-
requires="goblint-cil.simplemem goblint-cil.canonicalize goblint-cil.dataslicing goblint-cil.liveness goblint-cil.heapify goblint-cil.oneret goblint-cil.logcalls goblint-cil.pta goblint-cil.partial goblint-cil.sfi goblint-cil.simplify goblint-cil.callgraph goblint-cil.logwrites goblint-cil.epicenter"
4+
requires="goblint-cil.simplemem goblint-cil.canonicalize goblint-cil.dataslicing goblint-cil.liveness goblint-cil.heapify goblint-cil.oneret goblint-cil.logcalls goblint-cil.pta goblint-cil.partial goblint-cil.sfi goblint-cil.simplify goblint-cil.callgraph goblint-cil.logwrites goblint-cil.epicenter goblint-cil.syntacticsearch"
55
version = "1.7.7"
66
)
77

88
package "all-features" (
9-
requires="goblint-cil.simplemem goblint-cil.canonicalize goblint-cil.dataslicing goblint-cil.liveness goblint-cil.llvm goblint-cil.heapify goblint-cil.oneret goblint-cil.logcalls goblint-cil.pta goblint-cil.inliner goblint-cil.partial goblint-cil.blockinggraph goblint-cil.sfi goblint-cil.simplify goblint-cil.cqualann goblint-cil.callgraph goblint-cil.zrapp goblint-cil.logwrites goblint-cil.epicenter goblint-cil.ccl"
9+
requires="goblint-cil.simplemem goblint-cil.canonicalize goblint-cil.dataslicing goblint-cil.liveness goblint-cil.llvm goblint-cil.heapify goblint-cil.oneret goblint-cil.logcalls goblint-cil.pta goblint-cil.inliner goblint-cil.partial goblint-cil.blockinggraph goblint-cil.sfi goblint-cil.simplify goblint-cil.cqualann goblint-cil.callgraph goblint-cil.zrapp goblint-cil.logwrites goblint-cil.epicenter goblint-cil.ccl goblint-cil.syntacticsearch"
1010
version = "1.7.7"
1111
)

‎_tags‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
# Traverse only subdirectories containing source code
2-
true: -traverse, package(zarith), package(stdlib-shims)
2+
true: -traverse, package(zarith), package(stdlib-shims), package(batteries)
33
<src>: include
44
# build every cmo in debug mode (for cil.cma)
55
<**/*.cmo>: debug

‎dune-project‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,9 @@ Changes:
2727
(dune (>= 2.3.0))
2828
(odoc :with-doc)
2929
stdlib-shims
30+
ppx_deriving_yojson
31+
yojson
32+
batteries
3033
)
3134
(conflicts cil)
3235
)

‎goblint-cil.opam‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,9 @@ depends: [
2525
"dune" {>= "2.3.0"}
2626
"odoc" {with-doc}
2727
"stdlib-shims"
28+
"ppx_deriving_yojson"
29+
"yojson"
30+
"batteries"
2831
]
2932
conflicts: ["cil"]
3033
build: [

‎src/dune‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
(public_name goblint-cil)
55
(name cil)
66
(wrapped false) ; this should be changed, but then module paths in goblint need to be prefixed
7-
(libraries zarith findlib dynlink unix str stdlib-shims)
7+
(libraries zarith findlib dynlink unix str stdlib-shims batteries)
88
(modules (:standard \ main))
99
)
1010

‎src/ext/syntaticsearch/.merlin‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
EXCLUDE_QUERY_DIR
2+
B /home/michael/Documents/goblint-cil/cil/_opam/lib/batteries
3+
B /home/michael/Documents/goblint-cil/cil/_opam/lib/ppx_deriving/runtime
4+
B /home/michael/Documents/goblint-cil/cil/_opam/lib/ppx_deriving_yojson/runtime
5+
B /home/michael/Documents/goblint-cil/cil/_opam/lib/yojson
6+
B ../../../_build/default/src/.cil.objs/byte
7+
B ../../../_build/default/src/ext/syntaticsearch/.syntacticsearch.objs/byte
8+
S /home/michael/Documents/goblint-cil/cil/_opam/lib/batteries
9+
S /home/michael/Documents/goblint-cil/cil/_opam/lib/ppx_deriving/runtime
10+
S /home/michael/Documents/goblint-cil/cil/_opam/lib/ppx_deriving_yojson/runtime
11+
S /home/michael/Documents/goblint-cil/cil/_opam/lib/yojson
12+
S ../..
13+
S .
14+
S ../../frontc
15+
S ../../ocamlutil
16+
FLG -ppx '/home/michael/Documents/goblint-cil/cil/_build/default/.ppx/a4ea0d83c521725fd7b0167e93f2550b/ppx.exe --as-ppx --cookie '\''library-name="syntacticsearch"'\'''
17+
FLG -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -short-paths -keep-locs -warn-error -A -w -27-32-34-37-38

‎src/ext/syntaticsearch/META‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
description = "Syntactic Search in CIL programs"

‎src/ext/syntaticsearch/codeQuery.ml‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
open Yojson.Safe
2+
module Result = Ppx_deriving_yojson_runtime.Result
3+
(* JSON-query has the following form:
4+
select: ...
5+
type: ...
6+
target: ...
7+
find: ...
8+
structure: ...
9+
constraint: ... *)
10+
11+
type selectable =
12+
| Name_sel [@name "name"]
13+
| Location_sel [@name "location"] [@to_yojson fun x -> `String x]
14+
| Type_sel [@name "type"] [@to_yojson fun x -> `String x]
15+
| ID_sel [@name "id"] [@to_yojson fun x -> `String x]
16+
[@@deriving yojson]
17+
18+
type select = selectable list [@@deriving yojson]
19+
20+
type kind =
21+
| Var_k [@name "var"]
22+
| Fun_k [@name "fun"]
23+
| Datatype_k [@name "datatype"]
24+
[@@deriving yojson]
25+
26+
type target =
27+
| Name_t of string [@name "name"]
28+
| ID_t of int [@name "id"]
29+
| All_t [@name "all"]
30+
| AllGlobVar_t [@name "all_glob_var"]
31+
| Or_t of string list [@name "or"]
32+
| And_t of string list [@name "and"]
33+
[@@deriving yojson]
34+
35+
type find =
36+
| Uses_f [@name "uses"]
37+
| Decl_f [@name "decl"]
38+
| Defs_f [@name "defs"]
39+
| UsesWithVar_f of string [@name "uses_with_var"]
40+
| Returns_f [@name "returns"]
41+
[@@deriving yojson]
42+
43+
type structure =
44+
| Fun_s of string [@name "fun_name"]
45+
| Cond_s [@name "cond"]
46+
| NonCond_s [@name "non-cond"]
47+
| None_s [@name "none"]
48+
[@@deriving yojson]
49+
50+
type constr = Constraint_c of string [@name "constr"] | None_c [@name "none"]
51+
[@@deriving yojson]
52+
53+
(* Type-definition of a query for mapping use *)
54+
type query = {
55+
sel : select; [@key "select"]
56+
k : kind; [@key "type"]
57+
tar : target; [@key "target"]
58+
f : find; [@key "find"]
59+
str : (structure[@default None_s]); [@key "structure"]
60+
lim : (constr[@default None_c]); [@key "constraint"]
61+
}
62+
[@@deriving yojson]
63+
64+
(* toString-function for query *)
65+
66+
let to_string_q query = Yojson.Safe.to_string (query_to_yojson query)
67+
68+
exception Error of string
69+
70+
let parse_json_file filename =
71+
let jsonTree = from_file filename in
72+
let derived = query_of_yojson jsonTree in
73+
match derived with Result.Ok y -> y | Result.Error x -> raise (Error x)

‎src/ext/syntaticsearch/dune‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(library
2+
(public_name goblint-cil.syntacticsearch)
3+
(name syntacticsearch)
4+
(wrapped false) ; this should be changed, but then module paths in goblint need to be prefixed
5+
(libraries goblint-cil yojson ppx_deriving_yojson.runtime batteries)
6+
(preprocess (pps ppx_deriving_yojson))
7+
)

‎src/ext/syntaticsearch/funcDatatype.ml‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
open Cil
2+
3+
(* Finds definition of a user-defined type *)
4+
let find_def name file =
5+
BatList.filter_map
6+
(function
7+
| GType (info, loc) ->
8+
if String.compare name info.tname = 0 then Some ("", loc, name, -1)
9+
else None
10+
| GCompTag (info, loc) ->
11+
if String.compare name info.cname = 0 then Some ("", loc, name, -1)
12+
else None
13+
| GEnumTag (info, loc) ->
14+
if String.compare name info.ename = 0 then Some ("", loc, name, -1)
15+
else None
16+
| _ -> None)
17+
file.globals
18+
19+
(* Finds all definition of user-defined types *)
20+
let find_def_all file =
21+
BatList.filter_map
22+
(function
23+
| GType (info, loc) -> Some ("", loc, info.tname, -1)
24+
| GCompTag (info, loc) -> Some ("", loc, info.cname, -1)
25+
| GEnumTag (info, loc) -> Some ("", loc, info.ename, -1)
26+
| _ -> None)
27+
file.globals
28+
29+
let find_in_globals list name =
30+
BatList.filter_map
31+
(function
32+
| GVar (info, _, _) ->
33+
if
34+
String.compare name
35+
(String.trim (Pretty.sprint ~width:1 (d_type () info.vtype)))
36+
= 0
37+
then Some info.vid
38+
else None
39+
| _ -> None)
40+
list
41+
42+
let find_in_varinfos list name =
43+
BatList.filter_map
44+
(fun info ->
45+
if
46+
String.compare name
47+
(String.trim (Pretty.sprint ~width:1 (d_type () info.vtype)))
48+
= 0
49+
then Some info.vid
50+
else None)
51+
list
52+
53+
let find_fundec globals name =
54+
let gfun =
55+
BatList.find_opt
56+
(function
57+
| GFun (fundec, _) -> String.compare fundec.svar.vname name = 0
58+
| _ -> false)
59+
globals
60+
in
61+
match gfun with Some (GFun (fundec, _)) -> Some fundec | _ -> None
62+
63+
let find_typevar_uses_in_fun list funname file =
64+
List.flatten
65+
@@ List.map (fun x -> FuncVar.find_uses_in_fun "" x funname file false) list
66+
67+
(* Finds uses of a datatype in a function *)
68+
let find_uses_in_fun typename funname file =
69+
match find_fundec file.globals funname with
70+
| None -> []
71+
| Some f ->
72+
find_typevar_uses_in_fun
73+
( find_in_globals file.globals typename
74+
@ find_in_varinfos f.slocals typename
75+
@ find_in_varinfos f.sformals typename )
76+
f.svar.vname file
77+
78+
(* Finds all uses of a datatype in all functions *)
79+
let find_uses typename file =
80+
let list = FuncVar.find_uses_all file false in
81+
List.filter (fun (_, _, typ, _) -> String.compare typ typename = 0) list
82+
83+
(* Finds all uses of a datatype in conditions *)
84+
let find_uses_in_cond typename file =
85+
let list = FuncVar.find_uses_in_cond_all file false in
86+
List.filter (fun (_, _, typ, _) -> String.compare typ typename = 0) list
87+
88+
(* Finds all uses of a datatype in non-conditions *)
89+
let find_uses_in_noncond typename file =
90+
let list = FuncVar.find_uses_in_noncond_all file false in
91+
List.filter (fun (_, _, typ, _) -> String.compare typ typename = 0) list

0 commit comments

Comments
 (0)