Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Handle renaming of local variables in incremental analysis (AST) #731

Merged
merged 40 commits into from
Jul 11, 2022
Merged
Changes from 1 commit
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
4256428
Added basic test cases for changed variable names.
TimOrtel Mar 17, 2022
27dd10f
Rename detection works for simple cases
TimOrtel Mar 18, 2022
6bc0fca
Rename detection for method parameters, too
TimOrtel Apr 3, 2022
ca6670b
Renaming of method params should work now.
TimOrtel Apr 5, 2022
c1e165c
Renaming of results does work for the log files.
TimOrtel Apr 18, 2022
d589278
Added multiple incremental runs test
TimOrtel Apr 19, 2022
9eb3f87
Renamed local vars are now also shown in g2html.
TimOrtel Apr 20, 2022
d652715
Added incremental aware print statements and replaced traditional pri…
TimOrtel May 3, 2022
08da3fb
Renamed variable names are now displayed with their new name in g2html
TimOrtel May 4, 2022
3a11fb9
Cleanup print statements and added some docu.
TimOrtel May 9, 2022
26d0702
Merge remote-tracking branch 'upstream/master' into dev-local-var-rename
TimOrtel May 9, 2022
b7fac89
Renamed context to rename_mapping
TimOrtel May 9, 2022
abf871b
Replaced rename mapping lists with Hashtbls for increased performance
TimOrtel May 9, 2022
4745a3f
cleanup print statements and code.
TimOrtel May 14, 2022
7d702f7
Merge upstream master
TimOrtel May 14, 2022
c645c68
cherry picked context -> rename mapping
TimOrtel May 14, 2022
aed7a3a
Replaced rename mapping lists with Hashtbls for increased performance
TimOrtel May 9, 2022
9e95ddb
Old locals are now renamed to the new local names.
TimOrtel May 14, 2022
7e89ec2
Fixed duplicate id tests
TimOrtel May 16, 2022
0c6b9c4
Moved multiple incremental run tests to subdirectory.
TimOrtel Jun 8, 2022
d5979f1
Merge Branch Without Rename Mapping
TimOrtel Jun 10, 2022
37e5703
Merged upstream master
TimOrtel Jun 10, 2022
3b60fb7
Removed unused currentFunctionName global state.
TimOrtel Jun 15, 2022
fd691c5
Removed nothing test case
TimOrtel Jun 15, 2022
686a3da
Added include assert to tests. Removed useless test.c
TimOrtel Jun 15, 2022
0a0ee34
Replaced tupletostring with fancy syntax.
TimOrtel Jun 15, 2022
8b28e89
Hashtbl.add is now replaced by Hashtbl.replace in many places.
TimOrtel Jun 15, 2022
77bd926
List optimization.
TimOrtel Jun 15, 2022
7371dc9
method_rename_assumptions now uses varinfo map instead of string hash…
TimOrtel Jun 20, 2022
7b320c9
Removed RenameMapping.
TimOrtel Jun 20, 2022
40281fe
Added documentation to tests in 04-var-rename
TimOrtel Jun 21, 2022
60468d4
Add comment to test-incremental-multiple.sh
TimOrtel Jun 15, 2022
9c8e226
Merge remote-tracking branch 'upstream/master' into dev-local-var-rename
TimOrtel Jun 22, 2022
a9d297c
Removed syntactic noise introduced by addition and removal of RenameM…
TimOrtel Jun 22, 2022
31283c9
Removed diffs directory in tests/incremental/04-var-rename
TimOrtel Jun 22, 2022
b3487ba
Merge remote-tracking branch 'upstream/master' into dev-local-var-rename
TimOrtel Jul 4, 2022
a3f48fa
function parameter names are now also updated. Cleanup code.
TimOrtel Jul 5, 2022
6fe1202
eqF now uses empty rename mapping for header comparison.
TimOrtel Jul 5, 2022
8b5fbd9
Merge remote-tracking branch 'upstream/master' into dev-local-var-rename
TimOrtel Jul 6, 2022
fd3f228
CFG comparison now verifies locals again.
TimOrtel Jul 7, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Removed RenameMapping.
TimOrtel committed Jun 20, 2022
commit 7b320c993fd001d480d279a5d796b483fb50303b
2 changes: 1 addition & 1 deletion src/analyses/apron/apronAnalysis.apron.ml
Original file line number Diff line number Diff line change
@@ -146,7 +146,7 @@ struct
if !GU.global_initialization && e = MyCFG.unknown_exp then
st (* ignore extern inits because there's no body before assign, so the apron env is empty... *)
else (
if M.tracing then M.traceli "apron" "assign %a = %a\n" RenameMapping.d_lval lv d_exp e;
if M.tracing then M.traceli "apron" "assign %a = %a\n" d_lval lv d_exp e;
let ask = Analyses.ask_of_ctx ctx in
let r = assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
assign_from_globals_wrapper ask ctx.global st e (fun apr' e' ->
14 changes: 7 additions & 7 deletions src/analyses/arinc.ml
Original file line number Diff line number Diff line change
@@ -137,7 +137,7 @@ struct
let return_code_is_success z = Cilint.is_zero_cilint z || Cilint.compare_cilint z Cilint.one_cilint = 0
let str_return_code i = if return_code_is_success i then "SUCCESS" else "ERROR"
let str_return_dlval (v,o as dlval) =
sprint RenameMapping.d_lval (Lval.CilLval.to_lval dlval) ^ "_" ^ string_of_int v.vdecl.line |>
sprint d_lval (Lval.CilLval.to_lval dlval) ^ "_" ^ string_of_int v.vdecl.line |>
Str.global_replace (Str.regexp "[^a-zA-Z0-9]") "_"
let add_return_dlval env kind dlval =
ArincUtil.add_return_var env.procid kind (str_return_dlval dlval)
@@ -152,17 +152,17 @@ struct
| a when not (Queries.LS.is_top a) && Queries.LS.cardinal a > 0 ->
let top_elt = (dummyFunDec.svar, `NoOffset) in
let a' = if Queries.LS.mem top_elt a then (
M.debug "mayPointTo: query result for %a contains TOP!" RenameMapping.d_exp exp; (* UNSOUND *)
M.debug "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
Queries.LS.remove top_elt a
) else a
in
Queries.LS.elements a'
| v ->
M.debug "mayPointTo: query result for %a is %a" RenameMapping.d_exp exp Queries.LS.pretty v;
M.debug "mayPointTo: query result for %a is %a" d_exp exp Queries.LS.pretty v;
(*failwith "mayPointTo"*)
[]
let iterMayPointTo ctx exp f = mayPointTo ctx exp |> List.iter f
let debugMayPointTo ctx exp = M.debug "%a mayPointTo %a" RenameMapping.d_exp exp (Pretty.d_list ", " Lval.CilLval.pretty) (mayPointTo ctx exp)
let debugMayPointTo ctx exp = M.debug "%a mayPointTo %a" d_exp exp (Pretty.d_list ", " Lval.CilLval.pretty) (mayPointTo ctx exp)


(* transfer functions *)
@@ -184,7 +184,7 @@ struct
let edges_added = ref false in
let f dlval =
(* M.debug @@ "assign: MayPointTo " ^ sprint d_plainlval lval ^ ": " ^ sprint d_plainexp (Lval.CilLval.to_exp dlval); *)
let is_ret_type = try is_return_code_type @@ Lval.CilLval.to_exp dlval with Cilfacade.TypeOfError Index_NonArray -> M.debug "assign: Cilfacade.typeOf %a threw exception Errormsg.Error \"Bug: typeOffset: Index on a non-array\". Will assume this is a return type to remain sound." RenameMapping.d_exp (Lval.CilLval.to_exp dlval); true in
let is_ret_type = try is_return_code_type @@ Lval.CilLval.to_exp dlval with Cilfacade.TypeOfError Index_NonArray -> M.debug "assign: Cilfacade.typeOf %a threw exception Errormsg.Error \"Bug: typeOffset: Index on a non-array\". Will assume this is a return type to remain sound." d_exp (Lval.CilLval.to_exp dlval); true in
if (not is_ret_type) || Lval.CilLval.has_index dlval then () else
let dlval = global_dlval dlval "assign" in
edges_added := true;
@@ -320,7 +320,7 @@ struct
let is_creating_fun = startsWith (Functions.prefix^"Create") f.vname in
if M.tracing && is_arinc_fun then (
(* M.tracel "arinc" "found %s(%s)\n" f.vname args_str *)
M.debug "found %s(%a) in %s" f.vname (Pretty.d_list ", " RenameMapping.d_exp) arglist env.fundec.svar.vname
M.debug "found %s(%a) in %s" f.vname (Pretty.d_list ", " d_exp) arglist env.fundec.svar.vname
);
let is_error_handler = env.pname = pname_ErrorHandler in
let eval_int exp =
@@ -339,7 +339,7 @@ struct
(* call assign for all analyses (we only need base)! *)
| AddrOf lval -> ctx.emit (Assign {lval; exp = mkAddrOf @@ var id})
(* TODO not needed for the given code, but we could use Queries.MayPointTo exp in this case *)
| _ -> failwith @@ "Could not assign id. Expected &id. Found "^sprint RenameMapping.d_exp exp
| _ -> failwith @@ "Could not assign id. Expected &id. Found "^sprint d_exp exp
in
let assign_id_by_name resource_type name id =
assign_id id (get_id (resource_type, eval_str name))
2 changes: 1 addition & 1 deletion src/analyses/spec.ml
Original file line number Diff line number Diff line change
@@ -256,7 +256,7 @@ struct
D.warn @@ "changed pointer "^D.string_of_key k1^" (no longer safe)";
(* saveOpened ~unknown:true k1 *) m |> D.unknown k1
| _ -> (* no change in D for other things *)
M.debug "assign (none in D): %a = %a [%a]" RenameMapping.d_lval lval d_exp rval d_plainexp rval;
M.debug "assign (none in D): %a = %a [%a]" d_lval lval d_exp rval d_plainexp rval;
m

(*
4 changes: 2 additions & 2 deletions src/cdomains/basetype.ml
Original file line number Diff line number Diff line change
@@ -26,8 +26,8 @@ struct
let show x =
if RichVarinfo.BiVarinfoMap.Collection.mem_varinfo x then
let description = RichVarinfo.BiVarinfoMap.Collection.describe_varinfo x in
"(" ^ RenameMapping.show_varinfo x ^ ", " ^ description ^ ")"
else RenameMapping.show_varinfo x
"(" ^ x.vname ^ ", " ^ description ^ ")"
else x.vname
let pretty () x = Pretty.text (show x)
type group = Global | Local | Parameter | Temp [@@deriving show { with_path = false }]
let (%) = Batteries.(%)
4 changes: 2 additions & 2 deletions src/cdomains/lval.ml
Original file line number Diff line number Diff line change
@@ -223,8 +223,8 @@ struct
let short_addr (x, o) =
if RichVarinfo.BiVarinfoMap.Collection.mem_varinfo x then
let description = RichVarinfo.BiVarinfoMap.Collection.describe_varinfo x in
"(" ^ RenameMapping.show_varinfo x ^ ", " ^ description ^ ")" ^ short_offs o
else RenameMapping.show_varinfo x ^ short_offs o
"(" ^ x.vname ^ ", " ^ description ^ ")" ^ short_offs o
else x.vname ^ short_offs o

let show = function
| Addr (x, o)-> short_addr (x, o)
2 changes: 1 addition & 1 deletion src/cdomains/symbLocksDomain.ml
Original file line number Diff line number Diff line change
@@ -184,7 +184,7 @@ struct

let ee_to_str x =
match x with
| EVar v -> RenameMapping.show_varinfo v
| EVar v -> v.vname
| EAddr -> "&"
| EDeref -> "*"
| EField f -> f.fname
14 changes: 7 additions & 7 deletions src/framework/analyses.ml
Original file line number Diff line number Diff line change
@@ -31,7 +31,7 @@ struct

let printXml f n =
let l = Node.location n in
BatPrintf.fprintf f "<call id=\"%s\" file=\"%s\" fun=\"%s\" line=\"%d\" order=\"%d\" column=\"%d\">\n" (Node.show_id n) l.file (RenameMapping.show_varinfo (Node.find_fundec n).svar) l.line l.byte l.column
BatPrintf.fprintf f "<call id=\"%s\" file=\"%s\" fun=\"%s\" line=\"%d\" order=\"%d\" column=\"%d\">\n" (Node.show_id n) l.file (Node.find_fundec n).svar.vname l.line l.byte l.column

let var_id = Node.show_id
end
@@ -105,7 +105,7 @@ struct
See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
let x = UpdateCil.getLoc a in
let f = Node.find_fundec a in
CilType.Location.show x ^ "(" ^ RenameMapping.show_varinfo f.svar ^ ")"
CilType.Location.show x ^ "(" ^ f.svar.vname ^ ")"

include Printable.SimpleShow (
struct
@@ -179,9 +179,9 @@ struct
let module SH = BatHashtbl.Make (Basetype.RawStrings) in
let file2funs = SH.create 100 in
let funs2node = SH.create 100 in
iter (fun n _ -> SH.add funs2node (RenameMapping.show_varinfo (Node.find_fundec n).svar) n) (Lazy.force table);
iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table);
iterGlobals file (function
| GFun (fd,loc) -> SH.add file2funs loc.file (RenameMapping.show_varinfo fd.svar)
| GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname
| _ -> ()
);
let p_node f n = BatPrintf.fprintf f "%s" (Node.show_id n) in
@@ -227,9 +227,9 @@ struct
let module SH = BatHashtbl.Make (Basetype.RawStrings) in
let file2funs = SH.create 100 in
let funs2node = SH.create 100 in
iter (fun n _ -> SH.add funs2node (RenameMapping.show_varinfo (Node.find_fundec n).svar) n) (Lazy.force table);
iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table);
iterGlobals file (function
| GFun (fd,loc) -> SH.add file2funs loc.file (RenameMapping.show_varinfo fd.svar)
| GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname
| _ -> ()
);
let p_enum p f xs = BatEnum.print ~first:"[\n " ~last:"\n]" ~sep:",\n " p f xs in
@@ -519,7 +519,7 @@ struct
your analysis to be path sensitive, do override this. To obtain a behavior
where all paths are kept apart, set this to D.equal x y *)

let call_descr f _ = RenameMapping.show_varinfo f.svar
let call_descr f _ = f.svar.vname
(* prettier name for equation variables --- currently base can do this and
MCP just forwards it to Base.*)

6 changes: 3 additions & 3 deletions src/framework/constraints.ml
Original file line number Diff line number Diff line change
@@ -363,7 +363,7 @@ struct
if ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.context.widen" ~keepAttr:"widen" ~removeAttr:"no-widen" f then (
let v_old = M.find f.svar m in (* S.D.bot () if not found *)
let v_new = S.D.widen v_old (S.D.join v_old v_cur) in
Messages.(if tracing && not (S.D.equal v_old v_new) then tracel "widen-context" "enter results in new context for function %s\n" (RenameMapping.show_varinfo f.svar));
Messages.(if tracing && not (S.D.equal v_old v_new) then tracel "widen-context" "enter results in new context for function %s\n" f.svar.vname);
v_new, M.add f.svar v_new m
)
else
@@ -501,7 +501,7 @@ struct
ignore (getl (Function fd, c))
| exception Not_found ->
(* unknown function *)
M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" (RenameMapping.show_varinfo f)
M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname
(* actual implementation (e.g. invalidation) is done by threadenter *)
) ds
in
@@ -631,7 +631,7 @@ struct
let one_function f =
match Cilfacade.find_varinfo_fundec f with
| fd when LibraryFunctions.use_special f.vname ->
M.warn "Using special for defined function %s" (RenameMapping.show_varinfo f);
M.warn "Using special for defined function %s" f.vname;
tf_special_call ctx lv f args
| fd ->
tf_normal_call ctx lv e fd args getl sidel getg sideg
16 changes: 8 additions & 8 deletions src/framework/node.ml
Original file line number Diff line number Diff line change
@@ -22,21 +22,21 @@ let name () = "node"
(** Pretty node plainly with entire stmt. *)
let pretty_plain () = function
| Statement s -> text "Statement " ++ dn_stmt () s
TimOrtel marked this conversation as resolved.
Show resolved Hide resolved
| Function f -> text "Function " ++ text (RenameMapping.show_varinfo f.svar)
| FunctionEntry f -> text "FunctionEntry " ++ text (RenameMapping.show_varinfo f.svar)
| Function f -> text "Function " ++ text (f.svar.vname)
| FunctionEntry f -> text "FunctionEntry " ++ text (f.svar.vname)

(* TODO: remove this? *)
(** Pretty node plainly with stmt location. *)
let pretty_plain_short () = function
| Statement s -> text "Statement @ " ++ CilType.Location.pretty () (Cilfacade.get_stmtLoc s)
| Function f -> text "Function " ++ text (RenameMapping.show_varinfo f.svar)
| FunctionEntry f -> text "FunctionEntry " ++ text (RenameMapping.show_varinfo f.svar)
| Function f -> text "Function " ++ text (f.svar.vname)
| FunctionEntry f -> text "FunctionEntry " ++ text (f.svar.vname)

(** Pretty node for solver variable tracing with short stmt. *)
let pretty_trace () = function
| Statement stmt -> dprintf "node %d \"%a\"" stmt.sid Cilfacade.stmt_pretty_short stmt
| Function fd -> dprintf "call of %s" (RenameMapping.show_varinfo fd.svar)
| FunctionEntry fd -> dprintf "entry state of %s" (RenameMapping.show_varinfo fd.svar)
| Function fd -> dprintf "call of %s" (fd.svar.vname)
| FunctionEntry fd -> dprintf "entry state of %s" (fd.svar.vname)

(** Output functions for Printable interface *)
let pretty () x = pretty_trace () x
@@ -56,8 +56,8 @@ let show_id = function
(** Show node label for CFG. *)
let show_cfg = function
| Statement stmt -> string_of_int stmt.sid (* doesn't use this but defaults to no label and uses ID from show_id instead *)
| Function fd -> "return of " ^ (RenameMapping.show_varinfo fd.svar) ^ "()"
| FunctionEntry fd -> (RenameMapping.show_varinfo fd.svar) ^ "()"
| Function fd -> "return of " ^ (fd.svar.vname) ^ "()"
| FunctionEntry fd -> (fd.svar.vname) ^ "()"


let location (node: t) =
94 changes: 0 additions & 94 deletions src/incremental/renameMapping.ml

This file was deleted.