Skip to content

Commit ba77b29

Browse files
michael-schwarzmichael-schwarz
authored
Merge pull request #112 from superbr4in/master
Add Semantic Search
2 parents eff8260 + 0ac3f5a commit ba77b29

File tree

2 files changed

+200
-0
lines changed

2 files changed

+200
-0
lines changed

‎src/transform/expressionEvaluation.ml‎

Lines changed: 199 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,199 @@
1+
open Batteries
2+
3+
let transformation_identifier = "expeval"
4+
let transformation_query_file_name_identifier = "trans." ^ transformation_identifier ^ ".query_file_name"
5+
6+
module ExpEval : Transform.S =
7+
struct
8+
9+
let (~?) exception_function =
10+
try Some (exception_function ()) with
11+
| _ -> None
12+
let (~!) value_option =
13+
match value_option with
14+
| Some value -> value
15+
| None -> raise Exit
16+
17+
let is_debug () =
18+
GobConfig.get_bool "dbg.verbose"
19+
20+
let string_of_evaluation_result evaluation_result =
21+
match evaluation_result with
22+
| Some value -> if value then "TRUE" else "FALSE"
23+
| None -> "UNKNOWN"
24+
let string_of_statement statement =
25+
statement
26+
(* Pretty print *)
27+
|> Cil.d_stmt ()
28+
|> Pretty.sprint ~width:0
29+
(* Split into lines *)
30+
|> String.split_on_char '\n'
31+
(* Remove preprocessor directives *)
32+
|> List.filter (fun line -> line.[0] <> '#')
33+
(* Remove indentation *)
34+
|> List.map String.trim
35+
(* Concatenate lines into one *)
36+
|> List.fold_left (^) ""
37+
38+
class evaluator (file : Cil.file) (ask : Cil.location -> Queries.t -> Queries.Result.t) =
39+
object (self)
40+
41+
val global_variables =
42+
file.globals
43+
|> List.filter_map (function Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v) | _ -> None)
44+
val statements =
45+
file.globals
46+
|> List.filter_map (function Cil.GFun (f, _) -> Some f | _ -> None)
47+
(* Take all statements *)
48+
|> List.map (fun (f : Cil.fundec) -> f.sallstmts |> List.map (fun s -> f, s))
49+
|> List.flatten
50+
(* Add locations *)
51+
|> List.map (fun (f, (s : Cil.stmt)) -> (Cil.get_stmtLoc s.skind, f, s))
52+
(* Filter artificial ones by impossible location *)
53+
|> List.filter (fun ((l : Cil.location), _, _) -> l.line >= 0)
54+
(* Create hash table *)
55+
|> List.fold_left (fun ss (l, f, s) -> Hashtbl.add ss l (f, s); ss) (Hashtbl.create 0)
56+
57+
method evaluate location expression_string =
58+
(* Compute the available local variables *)
59+
let local_variables =
60+
match Hashtbl.find_option statements location with
61+
| Some (function_definition, _) -> function_definition.slocals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v)
62+
| None -> []
63+
in
64+
(* Parse expression *)
65+
match ~? (fun () -> Formatcil.cExp expression_string (local_variables @ global_variables)) with
66+
(* Expression unparseable at this location *)
67+
| None ->
68+
if is_debug () then print_endline "| (Unparseable)";
69+
Some false
70+
(* Successfully parsed expression *)
71+
| Some expression ->
72+
(* Evaluate at (directly before) the location *)
73+
match self#try_ask location expression with
74+
(* Dead code or not listed as part of the control flow *)
75+
| None ->
76+
if is_debug () then print_endline "| (Unreachable)";
77+
Some false
78+
(* Valid location *)
79+
| Some value_before ->
80+
(* Use the last listed matching statement; TODO: use Hashtbl.find_all to consider other matching statements *)
81+
let _, statement = Hashtbl.find statements location in
82+
(* Use the first evaluable successor; TODO: consider other successors *)
83+
let succeeding_statement = ref None in
84+
let successor_evaluation =
85+
List.find_map_opt
86+
begin
87+
fun (s : Cil.stmt) ->
88+
succeeding_statement := Some s;
89+
(* Evaluate at (directly before) a succeeding location *)
90+
self#try_ask (Cil.get_stmtLoc s.skind) expression
91+
end
92+
statement.succs
93+
in
94+
(* Prefer successor evaluation *)
95+
match successor_evaluation with
96+
| None ->
97+
if is_debug () then
98+
begin
99+
print_endline ("| /*" ^ (value_before |> string_of_evaluation_result) ^ "*/" ^ (statement |> string_of_statement))
100+
end;
101+
value_before
102+
| Some value_after ->
103+
if is_debug () then
104+
begin
105+
print_endline ("| " ^ (statement |> string_of_statement) ^ "/*" ^ (value_after |> string_of_evaluation_result) ^ "*/");
106+
print_endline ("| " ^ (~! !succeeding_statement |> string_of_statement))
107+
end;
108+
value_after
109+
110+
method private try_ask location expression =
111+
match ~? (fun () -> ask location (Queries.EvalInt expression)) with
112+
(* Evaluable: Definite *)
113+
| Some `Int value -> Some (Some (value <> Int64.zero))
114+
(* Evaluable: Inconclusive *)
115+
| Some `Top -> Some None
116+
(* Inapplicable: Unreachable *)
117+
| Some `Bot -> None
118+
(* Inapplicable: Unlisted *)
119+
| None -> None
120+
(* Unexpected result *)
121+
| Some _ -> raise Exit
122+
123+
end
124+
125+
type query =
126+
{
127+
128+
kind : CodeQuery.kind;
129+
target : CodeQuery.target;
130+
find : CodeQuery.find;
131+
structure : (CodeQuery.structure [@default None_s]);
132+
limitation : (CodeQuery.constr [@default None_c]);
133+
134+
expression : string;
135+
mode : [ `Must | `May ];
136+
137+
} [@@deriving yojson]
138+
139+
let string_of_location (location : Cil.location) =
140+
location.file ^ ":" ^ (location.line |> string_of_int) ^ " [" ^ (location.byte |> string_of_int) ^ "]"
141+
142+
let location_file_compare (location_1 : Cil.location) (location_2 : Cil.location) = compare location_1.file location_2.file
143+
let location_byte_compare (location_1 : Cil.location) (location_2 : Cil.location) = compare location_1.byte location_2.byte
144+
145+
let transform (ask : Cil.location -> Queries.t -> Queries.Result.t) (file : Cil.file) =
146+
(* Parse query file *)
147+
let query_file_name = GobConfig.get_string transformation_query_file_name_identifier in
148+
match ~? (fun () -> Yojson.Safe.from_file query_file_name) with
149+
| None ->
150+
prerr_endline ("Invalid JSON query file: \"" ^ query_file_name ^ "\"")
151+
| Some query_yojson ->
152+
match query_yojson |> query_of_yojson with
153+
| Error message ->
154+
prerr_endline ("Unable to parse JSON query file: \"" ^ query_file_name ^ "\" (" ^ message ^ ")")
155+
| Ok query ->
156+
if is_debug () then
157+
print_endline ("Successfully parsed JSON query file: \"" ^ query_file_name ^ "\"");
158+
(* Create an evaluator *)
159+
let evaluator = new evaluator file ask in
160+
(* Syntactic query *)
161+
let query_syntactic : CodeQuery.query =
162+
{
163+
sel = [];
164+
k = query.kind;
165+
tar = query.target;
166+
f = query.find;
167+
str = query.structure;
168+
lim = query.limitation;
169+
}
170+
in
171+
let locations =
172+
QueryMapping.map_query query_syntactic file
173+
(* Use only locations *)
174+
|> List.map (fun (_, l, _, _) -> l)
175+
(* Group by source files *)
176+
|> List.group location_file_compare
177+
(* Sort and remove duplicates *)
178+
|> List.map (fun ls -> List.sort_uniq location_byte_compare ls)
179+
(* Ungroup *)
180+
|> List.flatten
181+
in
182+
(* Semantic queries *)
183+
let evaluate location =
184+
match evaluator#evaluate location query.expression with
185+
| Some value ->
186+
if value then
187+
print_endline (location |> string_of_location)
188+
else if is_debug () then
189+
print_endline ((location |> string_of_location) ^ " x")
190+
| None ->
191+
if query.mode = `May || is_debug () then
192+
print_endline ((location |> string_of_location) ^ " ?")
193+
in
194+
List.iter evaluate locations
195+
196+
end
197+
198+
let _ =
199+
Transform.register transformation_identifier (module ExpEval)

‎src/util/defaults.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,7 @@ let _ = ()
138138
(* {4 category [Transformations]} *)
139139
let _ = ()
140140
; reg Transformations "trans.activated" "[]" "Lists of activated transformations in this phase. Transformations happen after analyses."
141+
; reg Transformations "trans.expeval.query_file_name" "''" "Path to the JSON file containing an expression evaluation query."
141142

142143
(* {4 category [Experimental]} *)
143144
let _ = ()

0 commit comments

Comments
 (0)