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

* Added basic test cases for changed variable names.

* Rename detection works for simple cases

* Rename detection for method parameters, too

* Renaming of method params should work now.

* Renaming of results does work for the log files.

* Added multiple incremental runs test

* Renamed local vars are now also shown in g2html.

* Added incremental aware print statements and replaced traditional print statements with those in many places

* Renamed variable names are now displayed with their new name in g2html

* Cleanup print statements and added some docu.

* Renamed context to rename_mapping

* Replaced rename mapping lists with Hashtbls for increased performance

* cleanup print statements and code.

* cherry picked context -> rename mapping

* Replaced rename mapping lists with Hashtbls for increased performance

* Old locals are now renamed to the new local names.

* Fixed duplicate id tests

* Moved multiple incremental run tests to subdirectory.

* Removed unused currentFunctionName global state.

* Removed nothing test case

* Added include assert to tests. Removed useless test.c

* Replaced tupletostring with fancy syntax.

* Hashtbl.add is now replaced by Hashtbl.replace in many places.

* List optimization.

* method_rename_assumptions now uses varinfo map instead of string hashtable.

* Removed RenameMapping.

* Added documentation to tests in 04-var-rename

* Add comment to test-incremental-multiple.sh

* Removed syntactic noise introduced by addition and removal of RenameMapping

* Removed diffs directory in tests/incremental/04-var-rename

* function parameter names are now also updated. Cleanup code.

* eqF now uses empty rename mapping for header comparison.

* CFG comparison now verifies locals again.

Author: TimOrtel

scripts/test-incremental-multiple.sh

@@ -0,0 +1,37 @@
+#This file runs 3 incremental tests in total. As such it is similar to test-incremental.sh but performs an additional incremental run on top of it.
+test=$1
+
+base=./tests/incremental
+source=$base/${test}_1.c
+conf=$base/$test.json
+patch1=$base/${test}_1.patch
+patch2=$base/${test}_2.patch
+
+args="--enable dbg.debug --enable printstats -v"
+
+cat $source
+
+./goblint --conf $conf $args --enable incremental.save $source &> $base/$test.before.log --html
+
+patch -p0 -b <$patch1
+
+cat $source
+
+./goblint --conf $conf $args --enable incremental.load --enable incremental.save $source &> $base/$test.after.incr1.log --html
+
+patch -p0 <$patch2
+
+cat $source
+
+./goblint --conf $conf $args --enable incremental.load --enable incremental.save --set save_run $base/$test-incrementalrun $source &> $base/$test.after.incr2.log --html
+
+
+#./goblint --conf $conf $args --enable incremental.only-rename --set save_run $base/$test-originalrun $source &> $base/$test.after.scratch.log --html
+#./goblint --conf $conf --enable solverdiffs --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source --html
+
+patch -p0 -b -R <$patch2
+patch -p0 -b -R <$patch1
+# rm -r $base/$test-originalrun $base/$test-incrementalrun
+rm -r $base/$test-incrementalrun
+
+cat $source

src/incremental/compareAST.ml

@@ -1,28 +1,32 @@
 open MyCFG
 open Queue
 open Cil
+open CilMaps
 include CompareAST
 
 let eq_node (x, fun1) (y, fun2) =
+  let empty_rename_mapping: rename_mapping = (StringMap.empty, VarinfoMap.empty) in
   match x,y with
-  | Statement s1, Statement s2 -> eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2)
-  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar
-  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar
+  | Statement s1, Statement s2 -> eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2) empty_rename_mapping
+  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar empty_rename_mapping
+  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar empty_rename_mapping
   | _ -> false
 
 (* TODO: compare ASMs properly instead of simply always assuming that they are not the same *)
-let eq_edge x y = match x, y with
-  | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 && eq_exp rv1 rv2
-  | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 && GobList.equal eq_exp ars1 ars2
+let eq_edge x y =
+  let empty_rename_mapping: rename_mapping = (StringMap.empty, VarinfoMap.empty) in
+  match x, y with
+  | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 empty_rename_mapping && eq_exp rv1 rv2 empty_rename_mapping
+  | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 empty_rename_mapping && GobList.equal (eq_exp2 empty_rename_mapping) ars1 ars2
   | Proc (Some r1,f1,ars1), Proc (Some r2,f2,ars2) ->
-    eq_lval r1 r2 && eq_exp f1 f2 && GobList.equal eq_exp ars1 ars2
-  | Entry f1, Entry f2 -> eq_varinfo f1.svar f2.svar
-  | Ret (None,fd1), Ret (None,fd2) -> eq_varinfo fd1.svar fd2.svar
-  | Ret (Some r1,fd1), Ret (Some r2,fd2) -> eq_exp r1 r2 && eq_varinfo fd1.svar fd2.svar
-  | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 && b1 = b2
+    eq_lval r1 r2 empty_rename_mapping && eq_exp f1 f2 empty_rename_mapping && GobList.equal (eq_exp2 empty_rename_mapping) ars1 ars2
+  | Entry f1, Entry f2 -> eq_varinfo f1.svar f2.svar empty_rename_mapping
+  | Ret (None,fd1), Ret (None,fd2) -> eq_varinfo fd1.svar fd2.svar empty_rename_mapping
+  | Ret (Some r1,fd1), Ret (Some r2,fd2) -> eq_exp r1 r2 empty_rename_mapping && eq_varinfo fd1.svar fd2.svar empty_rename_mapping
+  | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 empty_rename_mapping && b1 = b2
   | ASM _, ASM _ -> false
   | Skip, Skip -> true
-  | VDecl v1, VDecl v2 -> eq_varinfo v1 v2
+  | VDecl v1, VDecl v2 -> eq_varinfo v1 v2 empty_rename_mapping
   | _ -> false
 
 (* The order of the edges in the list is relevant. Therefore compare them one to one without sorting first *)

src/incremental/compareCFG.ml

@@ -1,5 +1,6 @@
 open Cil
 open MyCFG
+open CilMaps
 include CompareAST
 include CompareCFG
 
@@ -36,18 +37,51 @@ let should_reanalyze (fdec: Cil.fundec) =
 (* If some CFGs of the two functions to be compared are provided, a fine-grained CFG comparison is done that also determines which
  * nodes of the function changed. If on the other hand no CFGs are provided, the "old" AST comparison on the CIL.file is
  * used for functions. Then no information is collected regarding which parts/nodes of the function changed. *)
-let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) =
-  let unchangedHeader = eq_varinfo a.svar b.svar && GobList.equal eq_varinfo a.sformals b.sformals in
+let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) =
+  let emptyRenameMapping = (StringMap.empty, VarinfoMap.empty) in
+
+  (* Compares the two varinfo lists, returning as a first element, if the size of the two lists are equal,
+   * and as a second a rename_mapping, holding the rename assumptions *)
+  let rec rename_mapping_aware_compare (alocals: varinfo list) (blocals: varinfo list) (rename_mapping: string StringMap.t) = match alocals, blocals with
+    | [], [] -> true, rename_mapping
+    | origLocal :: als, nowLocal :: bls ->
+      let new_mapping = StringMap.add origLocal.vname nowLocal.vname rename_mapping in
+
+      (*TODO: maybe optimize this with eq_varinfo*)
+      rename_mapping_aware_compare als bls new_mapping
+    | _, _ -> false, rename_mapping
+  in
+
+  let unchangedHeader, headerRenameMapping = match cfgs with
+    | None -> (
+        let headerSizeEqual, headerRenameMapping = rename_mapping_aware_compare a.sformals b.sformals (StringMap.empty) in
+        let actHeaderRenameMapping = (headerRenameMapping, global_rename_mapping) in
+        eq_varinfo a.svar b.svar actHeaderRenameMapping && GobList.equal (eq_varinfo2 actHeaderRenameMapping) a.sformals b.sformals, headerRenameMapping
+      )
+    | Some _ -> (
+        eq_varinfo a.svar b.svar emptyRenameMapping && GobList.equal (eq_varinfo2 emptyRenameMapping) a.sformals b.sformals, StringMap.empty
+      )
+  in
+
   let identical, diffOpt =
     if should_reanalyze a then
       false, None
     else
-      let sameDef = unchangedHeader && GobList.equal eq_varinfo a.slocals b.slocals in
+      (* Here the local variables are checked to be equal *)
+      (*flag: when running on cfg, true iff the locals are identical; on ast: if the size of the locals stayed the same*)
+      let flag, local_rename =
+        match cfgs with
+        | None -> rename_mapping_aware_compare a.slocals b.slocals headerRenameMapping
+        | Some _ -> GobList.equal (eq_varinfo2 emptyRenameMapping) a.slocals b.slocals, StringMap.empty
+      in
+      let rename_mapping: rename_mapping = (local_rename, global_rename_mapping) in
+
+      let sameDef = unchangedHeader && flag in
       if not sameDef then
         (false, None)
       else
         match cfgs with
-        | None -> eq_block (a.sbody, a) (b.sbody, b), None
+        | None -> eq_block (a.sbody, a) (b.sbody, b) rename_mapping, None
         | Some (cfgOld, (cfgNew, cfgNewBack)) ->
           let module CfgOld : MyCFG.CfgForward = struct let next = cfgOld end in
           let module CfgNew : MyCFG.CfgBidir = struct let prev = cfgNewBack let next = cfgNew end in
@@ -57,17 +91,41 @@ let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) =
   in
   identical, unchangedHeader, diffOpt
 
-let eq_glob (a: global) (b: global) (cfgs : (cfg * (cfg * cfg)) option) = match a, b with
-  | GFun (f,_), GFun (g,_) -> eqF f g cfgs
-  | GVar (x, init_x, _), GVar (y, init_y, _) -> eq_varinfo x y, false, None (* ignore the init_info - a changed init of a global will lead to a different start state *)
-  | GVarDecl (x, _), GVarDecl (y, _) -> eq_varinfo x y, false, None
+let eq_glob (a: global) (b: global) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) = match a, b with
+  | GFun (f,_), GFun (g,_) -> eqF f g cfgs global_rename_mapping
+  | GVar (x, init_x, _), GVar (y, init_y, _) -> eq_varinfo x y (StringMap.empty, VarinfoMap.empty), false, None (* ignore the init_info - a changed init of a global will lead to a different start state *)
+  | GVarDecl (x, _), GVarDecl (y, _) -> eq_varinfo x y (StringMap.empty, VarinfoMap.empty), false, None
   | _ -> ignore @@ Pretty.printf "Not comparable: %a and %a\n" Cil.d_global a Cil.d_global b; false, false, None
 
 let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
   let cfgs = if GobConfig.get_string "incremental.compare" = "cfg"
     then Some (CfgTools.getCFG oldAST |> fst, CfgTools.getCFG newAST)
     else None in
 
+  let generate_global_rename_mapping map global =
+    try
+      let ident = identifier_of_global global in
+      let old_global = GlobalMap.find ident map in
+
+      match old_global, global with
+      | GFun(f, _), GFun (g, _) ->
+        let renamed_params: string StringMap.t = if (List.length f.sformals) = (List.length g.sformals) then
+            let mappings = List.combine f.sformals g.sformals |>
+                           List.filter (fun (original, now) -> not (original.vname = now.vname)) |>
+                           List.map (fun (original, now) -> (original.vname, now.vname)) |>
+                           List.to_seq
+            in
+
+            StringMap.add_seq mappings StringMap.empty
+          else StringMap.empty in
+
+        if not (f.svar.vname = g.svar.vname) || (StringMap.cardinal renamed_params) > 0 then
+          Some (f.svar, {original_method_name=f.svar.vname; new_method_name=g.svar.vname; parameter_renames=renamed_params})
+        else None
+      | _, _ -> None
+    with Not_found -> None
+  in
+
   let addGlobal map global  =
     try
       let gid = identifier_of_global global in
@@ -79,14 +137,15 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
     with
       Not_found -> map
   in
+
   let changes = empty_change_info () in
   global_typ_acc := [];
-  let checkUnchanged map global =
+  let findChanges map global global_rename_mapping =
     try
       let ident = identifier_of_global global in
       let old_global = GlobalMap.find ident map in
       (* Do a (recursive) equal comparison ignoring location information *)
-      let identical, unchangedHeader, diff = eq old_global global cfgs in
+      let identical, unchangedHeader, diff = eq old_global global cfgs global_rename_mapping in
       if identical
       then changes.unchanged <- {current = global; old = old_global} :: changes.unchanged
       else changes.changed <- {current = global; old = old_global; unchangedHeader; diff} :: changes.changed
@@ -100,10 +159,18 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
   (* Store a map from functionNames in the old file to the function definition*)
   let oldMap = Cil.foldGlobals oldAST addGlobal GlobalMap.empty in
   let newMap = Cil.foldGlobals newAST addGlobal GlobalMap.empty in
+
+  let global_rename_mapping: method_rename_assumptions = Cil.foldGlobals newAST (fun (current_global_rename_mapping: method_rename_assumption VarinfoMap.t) global ->
+      match generate_global_rename_mapping oldMap global with
+      | Some (funVar, rename_mapping) -> VarinfoMap.add funVar rename_mapping current_global_rename_mapping
+      | None -> current_global_rename_mapping
+    ) VarinfoMap.empty
+  in
+
   (*  For each function in the new file, check whether a function with the same name
       already existed in the old version, and whether it is the same function. *)
   Cil.iterGlobals newAST
-    (fun glob -> checkUnchanged oldMap glob);
+    (fun glob -> findChanges oldMap glob global_rename_mapping);
 
   (* We check whether functions have been added or removed *)
   Cil.iterGlobals newAST (fun glob -> if not (checkExists oldMap glob) then changes.added <- (glob::changes.added));

src/incremental/compareCIL.ml

@@ -43,8 +43,8 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
   in
   let reset_fun (f: fundec) (old_f: fundec) =
     f.svar.vid <- old_f.svar.vid;
-    List.iter2 (fun l o_l -> l.vid <- o_l.vid) f.slocals old_f.slocals;
-    List.iter2 (fun lo o_f -> lo.vid <- o_f.vid) f.sformals old_f.sformals;
+    List.iter2 (fun l o_l -> l.vid <- o_l.vid; o_l.vname <- l.vname) f.slocals old_f.slocals;
+    List.iter2 (fun lo o_f -> lo.vid <- o_f.vid; o_f.vname <- lo.vname) f.sformals old_f.sformals;
     List.iter2 (fun s o_s -> s.sid <- o_s.sid) f.sallstmts old_f.sallstmts;
     List.iter (fun s -> store_node_location (Statement s) (Cilfacade.get_stmtLoc s)) f.sallstmts;
 

src/incremental/updateCil.ml

@@ -0,0 +1,11 @@
+open Cil
+
+module VarinfoOrdered = struct
+  type t = varinfo
+
+  (*x.svar.uid cannot be used, as they may overlap between old and now AST*)
+  let compare (x: varinfo) (y: varinfo) = String.compare x.vname y.vname
+end
+
+
+module VarinfoMap = Map.Make(VarinfoOrdered)

src/util/cilMaps.ml

@@ -117,7 +117,7 @@ let reparse (s: t) =
 
 (* Only called when the file has not been reparsed, so we can skip the expensive CFG comparison. *)
 let virtual_changes file =
-  let eq (glob: Cil.global) _ _ = match glob with
+  let eq (glob: Cil.global) _ _ _ = match glob with
     | GFun (fdec, _) -> not (CompareCIL.should_reanalyze fdec), false, None
     | _ -> true, false, None
   in

src/util/server.ml

@@ -0,0 +1,4 @@
+int main() {
+    int a = 0;
+    return 0;
+}

tests/incremental/04-var-rename/01-unused_rename.c

@@ -0,0 +1,3 @@
+{
+    
+}

tests/incremental/04-var-rename/01-unused_rename.json

@@ -0,0 +1,8 @@
+--- tests/incremental/04-var-rename/01-unused_rename.c
++++ tests/incremental/04-var-rename/01-unused_rename.c
+@@ -1,4 +1,4 @@
+ int main() {
+-    int a = 0;
++    int b = 0;
+     return 0;
+ }