Applied changes requested in PR goblint#731. compareCFG now propagates rename_mapping.

TimOrtel · TimOrtel · commit b9785ab01454 · 2022-07-12T15:55:33.000+02:00
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
@@ -63,6 +63,10 @@ let rename_mapping_to_string (rename_mapping: rename_mapping) =
 
   "(local=" ^ local_string ^ "; methods=[" ^ methods_string ^ "]; glob_vars=" ^ global_var_string ^ ")"
 
+let is_rename_mapping_empty (rename_mapping: rename_mapping) =
+  let local, methods, glob_vars, _= rename_mapping in
+  StringMap.is_empty local && VarinfoMap.is_empty methods && VarinfoMap.is_empty glob_vars
+
 let identifier_of_global glob =
   match glob with
   | GFun (fundec, l) -> {name = fundec.svar.vname; global_t = Fun}
@@ -86,9 +90,9 @@ let (&&>) (prev_result: bool * rename_mapping) (b: bool) : bool * rename_mapping
   (prev_equal && b, rename_mapping)
 
 (*Same as Goblist.eq but propagates the rename_mapping*)
-let forward_list_equal f l1 l2 (prev_result: rename_mapping) : bool * rename_mapping =
+let forward_list_equal ?(propF = (&&>>)) f l1 l2 (prev_result: rename_mapping) : bool * rename_mapping =
   if ((List.compare_lengths l1 l2) = 0) then
-    List.fold_left2 (fun (b, r) x y -> if b then f x y r else (b, r)) (true, prev_result) l1 l2
+    List.fold_left2 (fun (b, r) x y -> propF (b, r) (f x y)) (true, prev_result) l1 l2
   else false, prev_result
 
 (* hack: CIL generates new type names for anonymous types - we want to ignore these *)
diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
@@ -3,43 +3,42 @@ open Queue
 open Cil
 include CompareAST
 
-(*Non propagating version of &&>>. Discards the new rename_mapping and alwas propagates the one in prev_result*)
+(*Non propagating version of &&>>. Discards the new rename_mapping and alwas propagates the one in prev_result. However propagates the renames_on_success*)
 let (&&<>) (prev_result: bool * rename_mapping) f : bool * rename_mapping =
   let (prev_equal, prev_rm) = prev_result in
+  let (a, b, c, _) = prev_rm in
+
   if prev_equal then
-    let (r, _) = f prev_rm in
-    (r, prev_rm)
+    let (r, (_, _, _, updated_renames_on_success)) = f prev_rm in
+    (r, (a, b, c, updated_renames_on_success))
   else false, prev_rm
 
-let eq_node (x, fun1) (y, fun2) : bool =
-  let empty_rename_mapping: rename_mapping = emptyRenameMapping in
+let eq_node (x, fun1) (y, fun2) rename_mapping =
   match x,y with
-  | Statement s1, Statement s2 -> eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2) empty_rename_mapping |> fst
-  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar empty_rename_mapping |> fst
-  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar empty_rename_mapping |> fst
-  | _ -> false
+  | Statement s1, Statement s2 -> eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2) rename_mapping
+  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar rename_mapping
+  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar rename_mapping
+  | _ -> false, rename_mapping
 
 (* TODO: compare ASMs properly instead of simply always assuming that they are not the same *)
-let eq_edge x y =
-  let empty_rename_mapping: rename_mapping = emptyRenameMapping in
-  let (r, _) = match x, y with
-    | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 empty_rename_mapping &&<> eq_exp rv1 rv2
-    | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 empty_rename_mapping &&<> forward_list_equal eq_exp ars1 ars2
-    | Proc (Some r1,f1,ars1), Proc (Some r2,f2,ars2) ->
-      eq_lval r1 r2 empty_rename_mapping &&<> eq_exp f1 f2 &&<> forward_list_equal eq_exp 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
-    | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 empty_rename_mapping &&> (b1 = b2)
-    | ASM _, ASM _ -> false, empty_rename_mapping
-    | Skip, Skip -> true, empty_rename_mapping
-    | VDecl v1, VDecl v2 -> eq_varinfo v1 v2 empty_rename_mapping
-    | _ -> false, empty_rename_mapping
-  in
-  r
+let eq_edge x y rename_mapping =
+  match x, y with
+  | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 rename_mapping &&<> eq_exp rv1 rv2
+  | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 rename_mapping &&<> forward_list_equal eq_exp ars1 ars2
+  | Proc (Some r1,f1,ars1), Proc (Some r2,f2,ars2) ->
+    eq_lval r1 r2 rename_mapping &&<> eq_exp f1 f2 &&<> forward_list_equal eq_exp ars1 ars2
+  | Entry f1, Entry f2 -> eq_varinfo f1.svar f2.svar rename_mapping
+  | Ret (None,fd1), Ret (None,fd2) -> eq_varinfo fd1.svar fd2.svar rename_mapping
+  | Ret (Some r1,fd1), Ret (Some r2,fd2) -> eq_exp r1 r2 rename_mapping &&<> eq_varinfo fd1.svar fd2.svar
+  | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 rename_mapping &&> (b1 = b2)
+  | ASM _, ASM _ -> false, rename_mapping
+  | Skip, Skip -> true, rename_mapping
+  | VDecl v1, VDecl v2 -> eq_varinfo v1 v2 rename_mapping
+  | _ -> false, rename_mapping
+
 
 (* The order of the edges in the list is relevant. Therefore compare them one to one without sorting first *)
-let eq_edge_list xs ys = GobList.equal eq_edge xs ys
+let eq_edge_list xs ys = forward_list_equal ~propF:(&&<>) eq_edge xs ys
 
 let to_edge_list ls = List.map (fun (loc, edge) -> edge) ls
 
@@ -52,38 +51,41 @@ type biDirectionNodeMap = {node1to2: node NH.t; node2to1: node NH.t}
  * in the succesors of fromNode2 in the new CFG. Matching node tuples are added to the waitingList to repeat the matching
  * process on their successors. If a node from the old CFG can not be matched, it is added to diff and no further
  * comparison is done for its successors. The two function entry nodes make up the tuple to start the comparison from. *)
-let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 fun2 =
+
+let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 fun2 rename_mapping : biDirectionNodeMap * unit NH.t * rename_mapping =
   let diff = NH.create 113 in
   let same = {node1to2=NH.create 113; node2to1=NH.create 113} in
   let waitingList : (node * node) t = Queue.create () in
 
-  let rec compareNext () =
-    if Queue.is_empty waitingList then ()
+  let rec compareNext () rename_mapping : rename_mapping =
+    if Queue.is_empty waitingList then rename_mapping
     else
       let fromNode1, fromNode2 = Queue.take waitingList in
       let outList1 = CfgOld.next fromNode1 in
       let outList2 = CfgNew.next fromNode2 in
 
       (* Find a matching edge and successor node for (edgeList1, toNode1) in the list of successors of fromNode2.
        * If successful, add the matching node tuple to same, else add toNode1 to the differing nodes. *)
-      let findMatch (edgeList1, toNode1) =
-        let rec aux remSuc = match remSuc with
-          | [] -> NH.replace diff toNode1 ()
+      let findMatch (edgeList1, toNode1) rename_mapping : rename_mapping =
+        let rec aux remSuc rename_mapping : rename_mapping = match remSuc with
+          | [] -> NH.replace diff toNode1 (); rename_mapping
           | (locEdgeList2, toNode2)::remSuc' ->
             let edgeList2 = to_edge_list locEdgeList2 in
             (* TODO: don't allow pseudo return node to be equal to normal return node, could make function unchanged, but have different sallstmts *)
-            if eq_node (toNode1, fun1) (toNode2, fun2) && eq_edge_list edgeList1 edgeList2 then
+            let (isEq, updatedRenameMapping) = (true, rename_mapping) &&>> eq_node (toNode1, fun1) (toNode2, fun2) &&>> eq_edge_list edgeList1 edgeList2 in
+            if isEq then
               begin
                 match NH.find_opt same.node1to2 toNode1 with
-                | Some n2 -> if not (Node.equal n2 toNode2) then NH.replace diff toNode1 ()
-                | None -> NH.replace same.node1to2 toNode1 toNode2; NH.replace same.node2to1 toNode2 toNode1; Queue.add (toNode1, toNode2) waitingList
+                | Some n2 -> if not (Node.equal n2 toNode2) then NH.replace diff toNode1 (); updatedRenameMapping
+                | None -> NH.replace same.node1to2 toNode1 toNode2; NH.replace same.node2to1 toNode2 toNode1; Queue.add (toNode1, toNode2) waitingList;
+                  updatedRenameMapping
               end
-            else aux remSuc' in
-        aux outList2 in
+            else aux remSuc' updatedRenameMapping in
+        aux outList2 rename_mapping in
       (* For a toNode1 from the list of successors of fromNode1, check whether it might have duplicate matches.
        * In that case declare toNode1 as differing node. Else, try finding a match in the list of successors
        * of fromNode2 in the new CFG using findMatch. *)
-      let iterOuts (locEdgeList1, toNode1) =
+      let iterOuts (locEdgeList1, toNode1) rename_mapping : rename_mapping =
         let edgeList1 = to_edge_list locEdgeList1 in
         (* Differentiate between a possibly duplicate Test(1,false) edge and a single occurence. In the first
          * case the edge is directly added to the diff set to avoid undetected ambiguities during the recursive
@@ -94,13 +96,18 @@ let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 f
         let posAmbigEdge edgeList = let findTestFalseEdge (ll,_) = testFalseEdge (snd (List.hd ll)) in
           let numDuplicates l = List.length (List.find_all findTestFalseEdge l) in
           testFalseEdge (List.hd edgeList) && (numDuplicates outList1 > 1 || numDuplicates outList2 > 1) in
-        if posAmbigEdge edgeList1 then NH.replace diff toNode1 ()
-        else findMatch (edgeList1, toNode1) in
-      List.iter iterOuts outList1; compareNext () in
+        if posAmbigEdge edgeList1 then (NH.replace diff toNode1 (); rename_mapping)
+        else findMatch (edgeList1, toNode1) rename_mapping in
+      let updatedRenameMapping = List.fold_left (fun rm e -> iterOuts e rm) rename_mapping outList1 in
+      compareNext () updatedRenameMapping
+  in
 
   let entryNode1, entryNode2 = (FunctionEntry fun1, FunctionEntry fun2) in
-  NH.replace same.node1to2 entryNode1 entryNode2; NH.replace same.node2to1 entryNode2 entryNode1;
-  Queue.push (entryNode1,entryNode2) waitingList; compareNext (); (same, diff)
+  NH.replace same.node1to2 entryNode1 entryNode2;
+  NH.replace same.node2to1 entryNode2 entryNode1;
+  Queue.push (entryNode1,entryNode2) waitingList;
+  let updatedRenameMapping = compareNext () rename_mapping in
+  same, diff, updatedRenameMapping
 
 (* This is the second phase of the CFG comparison of functions. It removes the nodes from the matching node set 'same'
  * that have an incoming backedge in the new CFG that can be reached from a differing new node. This is important to
@@ -123,7 +130,8 @@ let reexamine f1 f2 (same : biDirectionNodeMap) (diffNodes1 : unit NH.t) (module
   repeat ();
   NH.to_seq same.node1to2, NH.to_seq_keys diffNodes1
 
-let compareFun (module CfgOld : CfgForward) (module CfgNew : CfgBidir) fun1 fun2 =
-  let same, diff = Stats.time "compare-phase1" (fun () -> compareCfgs (module CfgOld) (module CfgNew) fun1 fun2) () in
+
+let compareFun (module CfgOld : CfgForward) (module CfgNew : CfgBidir) fun1 fun2 rename_mapping : (node * node) list * node list * rename_mapping =
+  let same, diff, rename_mapping = Stats.time "compare-phase1" (fun () -> compareCfgs (module CfgOld) (module CfgNew) fun1 fun2 rename_mapping) () in
   let unchanged, diffNodes1 = Stats.time "compare-phase2" (fun () -> reexamine fun1 fun2 same diff (module CfgOld) (module CfgNew)) () in
-  List.of_seq unchanged, List.of_seq diffNodes1
+  List.of_seq unchanged, List.of_seq diffNodes1, rename_mapping
diff --git a/src/incremental/compareGlobals.ml b/src/incremental/compareGlobals.ml
@@ -1,5 +1,6 @@
 open Cil
 open MyCFG
+open CilMaps
 include CompareAST
 include CompareCFG
 
@@ -47,19 +48,43 @@ let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) (glo
     | _, _ -> false, rename_mapping
   in
 
-  let headerSizeEqual, headerRenameMapping = rename_mapping_aware_compare a.sformals b.sformals (StringMap.empty) in
-  let actHeaderRenameMapping: rename_mapping = (headerRenameMapping, global_function_rename_mapping, global_var_rename_mapping, ([], [])) in
+  let unchangedHeader, headerRenameMapping, renamesOnSuccessHeader = match cfgs with
+    | None -> (
+        let headerSizeEqual, headerRenameMapping = rename_mapping_aware_compare a.sformals b.sformals (StringMap.empty) in
+        let actHeaderRenameMapping: rename_mapping = (headerRenameMapping, global_function_rename_mapping, global_var_rename_mapping, ([], [])) in
+
+        let (unchangedHeader, (_, _, _, renamesOnSuccessHeader)) = eq_varinfo a.svar b.svar actHeaderRenameMapping &&>>
+                                                                   forward_list_equal eq_varinfo a.sformals b.sformals in
+        unchangedHeader, headerRenameMapping, renamesOnSuccessHeader
+      )
+    | Some _ -> (
+        let unchangedHeader, headerRenameMapping = eq_varinfo a.svar b.svar emptyRenameMapping &&>>
+                                                   forward_list_equal eq_varinfo a.sformals b.sformals in
+        let (_, _, _, renamesOnSuccessHeader) = headerRenameMapping in
+
+        (unchangedHeader && is_rename_mapping_empty headerRenameMapping), StringMap.empty, renamesOnSuccessHeader
+      )
+  in
 
-  let (unchangedHeader, (_, _, _, renamesOnSuccessHeader)) = eq_varinfo a.svar b.svar actHeaderRenameMapping &&>> forward_list_equal eq_varinfo a.sformals b.sformals in
   let identical, diffOpt, (_, renamed_method_dependencies, renamed_global_vars_dependencies, renamesOnSuccess) =
     if should_reanalyze a then
       false, None, emptyRenameMapping
     else
       (* 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_function_rename_mapping, global_var_rename_mapping, renamesOnSuccessHeader) in
+      (*flag: when running on cfg, true iff the locals are identical; on ast: if the size of the locals stayed the same*)
+      let flag, rename_mapping =
+        match cfgs with
+        | None -> (
+            let sizeEqual, local_rename = rename_mapping_aware_compare a.slocals b.slocals headerRenameMapping in
+            sizeEqual, (local_rename, global_function_rename_mapping, global_var_rename_mapping, renamesOnSuccessHeader)
+          )
+        | Some _ -> (
+            let isEqual, rename_mapping = forward_list_equal eq_varinfo a.slocals b.slocals (StringMap.empty, VarinfoMap.empty, VarinfoMap.empty, renamesOnSuccessHeader) in
+            isEqual && is_rename_mapping_empty rename_mapping, rename_mapping
+          )
+      in
 
-      let sameDef = unchangedHeader && sizeEqual in
+      let sameDef = unchangedHeader && flag in
       if not sameDef then
         (false, None, emptyRenameMapping)
       else
@@ -70,8 +95,8 @@ let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) (glo
         | 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
-          let matches, diffNodes1 = compareFun (module CfgOld) (module CfgNew) a b in
-          if diffNodes1 = [] then (true, None, emptyRenameMapping)
-          else (false, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1}, emptyRenameMapping)
+          let matches, diffNodes1, updated_rename_mapping = compareFun (module CfgOld) (module CfgNew) a b rename_mapping in
+          if diffNodes1 = [] then (true, None, updated_rename_mapping)
+          else (false, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1}, updated_rename_mapping)
   in
   identical, unchangedHeader, diffOpt, renamed_method_dependencies, renamed_global_vars_dependencies, renamesOnSuccess
diff --git a/src/incremental/updateCil.ml b/src/incremental/updateCil.ml
@@ -45,7 +45,7 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
     old_f.svar.vname <- f.svar.vname;
     f.svar.vid <- old_f.svar.vid;
     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 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;
 
