Skip to content

Commit

Permalink
Merge pull request #147 from goblint/fix-syntactic-search
Browse files Browse the repository at this point in the history 
Fix syntactic search
  • Loading branch information
@michael-schwarz
michael-schwarz authored Sep 15, 2023
2 parents 98598d9 + 34fecf4 commit 0d7db1c
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 102 deletions.
33 changes: 12 additions & 21 deletions src/ext/syntacticsearch/funcVar.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,37 +27,28 @@ let map_gvar f = function

let is_temporary id = Inthash.mem allTempVars id

let generate_func_loc_table cilfile =
Util.list_filter_map
(map_gfun (fun dec loc -> Some (dec.svar.vname, loc.line)))
cilfile.globals
(* fails when there is no function with name fname in cilfile *)
let get_func_loc cilfile fname =
let rec find_loc = function
| [] -> failwith ("no function with name " ^ fname ^ " found")
| GFun (fd, loc) :: l when fd.svar.vname = fname -> loc
| _ :: l -> find_loc l
in
find_loc cilfile.globals

let generate_globalvar_list cilfile =
Util.list_filter_map
(map_gvar (fun varinfo _ _ -> Some varinfo.vname))
cilfile.globals

let get_all_alphaconverted_in_fun varname funname cilfile =
let fun_loc_table = generate_func_loc_table cilfile in
let loc_start =
snd
@@ List.find (function x, _ -> String.compare x funname = 0) fun_loc_table
in
let rec iter_fun_loc list =
match list with
| (fname, _) :: xs ->
if fname = funname then
match xs with (_, line) :: _ -> line | [] -> max_int
else iter_fun_loc xs
| [] -> 0
in
let loc_end = iter_fun_loc fun_loc_table in
let fun_loc = get_func_loc cilfile funname in
let loc_within_fun loc = loc.file = fun_loc.file
&& loc.line >= fun_loc.line && (loc.line < fun_loc.endLine || fun_loc.endLine < 0) in
let tmp =
Util.list_filter_map
(function
| EnvVar varinfo, loc when loc.line >= loc_start && loc.line < loc_end
->
Some varinfo.vname
| EnvVar varinfo, loc when loc_within_fun loc-> Some varinfo.vname
| _ -> None)
(Hashtbl.find_all environment varname)
in
Expand Down
110 changes: 29 additions & 81 deletions src/ext/syntacticsearch/queryMapping.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,8 @@ let rec and_several_lists list_of_lists =

(* Naming of functions: resolve_query_[kind]_[find]_[structure] *)

exception Not_supported

(* Resolution of datatype-oriented queries *)
let resolve_query_datatype_uses_fun query cilfile funname =
match query.tar with
Expand All @@ -60,9 +62,7 @@ let resolve_query_datatype_uses_fun query cilfile funname =
(List.map
(fun x -> FuncDatatype.find_uses_in_fun x funname cilfile)
list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_datatype_uses_none query cilfile =
match query.tar with
Expand All @@ -72,9 +72,7 @@ let resolve_query_datatype_uses_none query cilfile =
(List.map (fun x -> FuncDatatype.find_uses x cilfile) list)
| Or_t list ->
List.flatten (List.map (fun x -> FuncDatatype.find_uses x cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_datatype_uses_cond query cilfile =
match query.tar with
Expand All @@ -85,9 +83,7 @@ let resolve_query_datatype_uses_cond query cilfile =
| Or_t list ->
List.flatten
(List.map (fun x -> FuncDatatype.find_uses_in_cond x cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_datatype_uses_noncond query cilfile =
match query.tar with
Expand All @@ -98,9 +94,7 @@ let resolve_query_datatype_uses_noncond query cilfile =
| Or_t list ->
List.flatten
(List.map (fun x -> FuncDatatype.find_uses_in_cond x cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_datatype_uses query cilfile =
match query.str with
Expand All @@ -115,24 +109,18 @@ let resolve_query_datatype_defs_none query cilfile =
| Or_t list ->
List.flatten (List.map (fun x -> FuncDatatype.find_def x cilfile) list)
| All_t -> FuncDatatype.find_def_all cilfile
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_datatype_defs query cilfile =
match query.str with
| None_s -> resolve_query_datatype_defs_none query cilfile
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_datatype query cilfile =
match query.f with
| Uses_f -> resolve_query_datatype_uses query cilfile
| Defs_f -> resolve_query_datatype_defs query cilfile
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

(* Resolution of variable-oriented queries *)
let resolve_query_var_uses_fun query cilfile funname =
Expand Down Expand Up @@ -216,9 +204,7 @@ let resolve_query_var_decl_fun query cilfile funname =
(List.map
(fun x -> FuncVar.find_decl_in_fun x (-1) funname cilfile)
list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_var_decl_none query cilfile =
match query.tar with
Expand All @@ -228,18 +214,14 @@ let resolve_query_var_decl_none query cilfile =
| All_t -> FuncVar.find_decl_all cilfile
| Or_t list ->
List.flatten (List.map (fun x -> FuncVar.find_decl x (-1) cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_var_decl query cilfile =
match query.str with
| Fun_s funname -> resolve_query_var_decl_fun query cilfile funname
| None_s -> resolve_query_var_decl_none query cilfile
| NonCond_s -> resolve_query_var_decl_none query cilfile
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_var_defs_fun query cilfile funname =
match query.tar with
Expand All @@ -252,9 +234,7 @@ let resolve_query_var_defs_fun query cilfile funname =
(List.map
(fun x -> FuncVar.find_defs_in_fun x (-1) funname cilfile)
list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_var_defs_none query cilfile =
match query.tar with
Expand All @@ -264,26 +244,20 @@ let resolve_query_var_defs_none query cilfile =
| All_t -> FuncVar.find_defs_all cilfile
| Or_t list ->
List.flatten (List.map (fun x -> FuncVar.find_defs x (-1) cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_var_defs query cilfile =
match query.str with
| Fun_s funname -> resolve_query_var_defs_fun query cilfile funname
| None_s -> resolve_query_var_defs_none query cilfile
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_var query cilfile =
match query.f with
| Uses_f -> resolve_query_var_uses query cilfile
| Decl_f -> resolve_query_var_decl query cilfile
| Defs_f -> resolve_query_var_defs query cilfile
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_return_none query cilfile =
match query.tar with
Expand All @@ -293,16 +267,12 @@ let resolve_query_fun_return_none query cilfile =
| Or_t list ->
List.flatten
(List.map (fun x -> FuncFunction.find_returns x (-1) cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_return query cilfile =
match query.str with
| None_s -> resolve_query_fun_return_none query cilfile
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_defs_none query cilfile =
match query.tar with
Expand All @@ -312,16 +282,12 @@ let resolve_query_fun_defs_none query cilfile =
| Or_t list ->
List.flatten
(List.map (fun x -> FuncFunction.find_def x (-1) cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_defs query cilfile =
match query.str with
| None_s -> resolve_query_fun_defs_none query cilfile
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_uses_none query cilfile =
match query.tar with
Expand All @@ -334,9 +300,7 @@ let resolve_query_fun_uses_none query cilfile =
| Or_t list ->
List.flatten
(List.map (fun x -> FuncFunction.find_uses x (-1) cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_uses_fun query cilfile funname =
match query.tar with
Expand All @@ -353,9 +317,7 @@ let resolve_query_fun_uses_fun query cilfile funname =
(List.map
(fun x -> FuncFunction.find_uses_in_fun x (-1) funname cilfile)
list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_uses_cond query cilfile =
match query.tar with
Expand All @@ -368,9 +330,7 @@ let resolve_query_fun_uses_cond query cilfile =
| Or_t list ->
List.flatten
(List.map (fun x -> FuncFunction.find_uses_cond x (-1) cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_uses_noncond query cilfile =
match query.tar with
Expand All @@ -383,9 +343,7 @@ let resolve_query_fun_uses_noncond query cilfile =
| Or_t list ->
List.flatten
(List.map (fun x -> FuncFunction.find_uses_noncond x (-1) cilfile) list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_uses query cilfile =
match query.str with
Expand Down Expand Up @@ -415,9 +373,7 @@ let resolve_query_fun_usesvar_fun query cilfile varname strucfunname =
FuncFunction.find_usesvar_in_fun x (-1) strucfunname varname
cilfile)
list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_usesvar_none query cilfile varname =
match query.tar with
Expand All @@ -434,9 +390,7 @@ let resolve_query_fun_usesvar_none query cilfile varname =
(List.map
(fun x -> FuncFunction.find_usesvar x (-1) varname cilfile)
list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_usesvar_cond query cilfile varname =
match query.tar with
Expand All @@ -454,9 +408,7 @@ let resolve_query_fun_usesvar_cond query cilfile varname =
(List.map
(fun x -> FuncFunction.find_usesvar_cond x (-1) varname cilfile)
list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_usesvar_noncond query cilfile varname =
match query.tar with
Expand All @@ -474,9 +426,7 @@ let resolve_query_fun_usesvar_noncond query cilfile varname =
(List.map
(fun x -> FuncFunction.find_usesvar_noncond x (-1) varname cilfile)
list)
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

let resolve_query_fun_usesvar query cilfile varname =
match query.str with
Expand All @@ -492,9 +442,7 @@ let resolve_query_fun query cilfile =
| Defs_f -> resolve_query_fun_defs query cilfile
| Uses_f -> resolve_query_fun_uses query cilfile
| UsesWithVar_f varname -> resolve_query_fun_usesvar query cilfile varname
| _ ->
Printf.printf "Not supported.\n";
[ ("", loc_default, "", -1) ]
| _ -> raise Not_supported

(* Main mapping function *)
let map_query query cilfile =
Expand Down

0 comments on commit 0d7db1c

Please sign in to comment.