Handle renaming of local variables in incremental analysis (AST)

scripts/test-incremental-multiple.sh

@@ -0,0 +1,36 @@
+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/cdomains/baseDomain.ml

@@ -115,7 +115,7 @@ struct
   let printXml f r =
     let e = XmlUtil.escape in
     BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a\n<key>\n%s\n</key>\n%a</map>\n</value>\n"
-      (e @@ CPA.name ()) CPA.printXml r.cpa
+      (e @@ (CPA.name ())) CPA.printXml r.cpa
       (e @@ PartDeps.name ()) PartDeps.printXml r.deps
       (e @@ WeakUpdates.name ()) WeakUpdates.printXml r.weak
       (e @@ PrivD.name ()) PrivD.printXml r.priv

src/framework/analyses.ml

@@ -140,6 +140,7 @@ struct
       (* Not using Node.location here to have updated locations in incremental analysis.
          See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
       let loc = UpdateCil.getLoc n in
+
       BatPrintf.fprintf f "<call id=\"%s\" file=\"%s\" line=\"%d\" order=\"%d\" column=\"%d\">\n" (Node.show_id n) loc.file loc.line loc.byte loc.column;
       BatPrintf.fprintf f "%a</call>\n" Range.printXml v
     in

src/framework/node.ml

@@ -22,21 +22,21 @@ let name () = "node"
 (** Pretty node plainly with entire stmt. *)
 let pretty_plain () = function
   | Statement s -> text "Statement " ++ dn_stmt () s
-  | Function f -> text "Function " ++ text f.svar.vname
-  | FunctionEntry f -> text "FunctionEntry " ++ text f.svar.vname
+  | 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 f.svar.vname
-  | FunctionEntry f -> text "FunctionEntry " ++ text f.svar.vname
+  | 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" fd.svar.vname
-  | FunctionEntry fd -> dprintf "entry state of %s" fd.svar.vname
+  | 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 " ^ fd.svar.vname ^ "()"
-  | FunctionEntry fd -> fd.svar.vname ^ "()"
+  | Function fd      -> "return of " ^ (fd.svar.vname) ^ "()"
+  | FunctionEntry fd -> (fd.svar.vname) ^ "()"
 
 
 let location (node: t) =

src/incremental/compareCFG.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/compareCIL.ml

@@ -1,5 +1,6 @@
 open Cil
 open MyCFG
+open CilMaps
 include CompareAST
 include CompareCFG
 
@@ -36,18 +37,45 @@ 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 local_rename_map: (string, string) Hashtbl.t = Hashtbl.create (List.length a.slocals) in
+
+  if (List.length a.slocals) = (List.length b.slocals) then
+    List.combine a.slocals b.slocals |>
+    List.map (fun x -> match x with (a, b) -> (a.vname, b.vname)) |>
+    List.iter (fun pair -> match pair with (a, b) -> Hashtbl.replace local_rename_map a b);
+
+
+  (* 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 headerSizeEqual, headerRenameMapping = rename_mapping_aware_compare a.sformals b.sformals (StringMap.empty) in
+  let actHeaderRenameMapping = (headerRenameMapping, global_rename_mapping) in
+
+  let unchangedHeader = eq_varinfo a.svar b.svar actHeaderRenameMapping && GobList.equal (eq_varinfo2 actHeaderRenameMapping) a.sformals b.sformals 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 *)
+      let sizeEqual, local_rename = rename_mapping_aware_compare a.slocals b.slocals headerRenameMapping in
+      let rename_mapping: rename_mapping = (local_rename, global_rename_mapping) in
+
+      let sameDef = unchangedHeader && sizeEqual 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 +85,44 @@ 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,_) ->
+    let identical, unchangedHeader, diffOpt = eqF f g cfgs global_rename_mapping in
+
+    identical, unchangedHeader, diffOpt
+  | 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 +134,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 +156,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/updateCil.ml

@@ -43,7 +43,7 @@ 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 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) 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/util/cilMaps.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/cilType.ml

@@ -117,6 +117,7 @@ struct
       let show = show
     end
     )
+
   let pp fmt x = Format.fprintf fmt "%s" x.vname (* for deriving show *)
 end
 

src/util/server.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

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

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

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

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

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

@@ -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;
+ }

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

@@ -0,0 +1,3 @@
+local variable a is renamed to b.
+a/b is not used.
+No semantic changes.

tests/incremental/04-var-rename/02-rename_and_shuffle.c

@@ -0,0 +1,11 @@
+#include<stdio.h>
+
+//a is renamed to c, but the usage of a is replaced by b
+int main() {
+    int a = 0;
+    int b = 1;
+
+    printf("Print %d", a);
+
+    return 0;
+}

tests/incremental/04-var-rename/02-rename_and_shuffle.json

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

tests/incremental/04-var-rename/02-rename_and_shuffle.patch

@@ -0,0 +1,15 @@
+--- tests/incremental/04-var-rename/02-rename_and_shuffle.c
++++ tests/incremental/04-var-rename/02-rename_and_shuffle.c
+@@ -2,10 +2,10 @@
+
+ //a is renamed to c, but the usage of a is replaced by b
+ int main() {
+-    int a = 0;
++    int c = 0;
+     int b = 1;
+
+-    printf("Print %d", a);
++    printf("Print %d", b);
+
+     return 0;
+ }

tests/incremental/04-var-rename/02-rename_and_shuffle.txt

@@ -0,0 +1,2 @@
+a is renamed to c, but the usage of a is replaced by b.
+Semantic changes.

tests/incremental/04-var-rename/03-rename_with_usage.c

@@ -0,0 +1,11 @@
+#include<stdio.h>
+
+//a is renamed to c, but its usages stay the same
+int main() {
+    int a = 0;
+    int b = 1;
+
+    printf("Print %d", a);
+
+    return 0;
+}

tests/incremental/04-var-rename/03-rename_with_usage.json

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