Merge pull request #836 from goblint/fix-incr-global-comparison

Group globals for comparison and updating of ids

src/incremental/compareAST.ml

@@ -1,11 +1,6 @@
 open GoblintCil
 open CilMaps
 
-(* global_type and global_t are implicitly used by GlobalMap to keep GVarDecl apart from GVar and GFun, so do not remove! *)
-type global_type = Fun | Decl | Var
-
-and global_identifier = {name: string ; global_t: global_type} [@@deriving ord]
-
 module StringMap = Map.Make(String)
 
 type method_rename_assumption = {original_method_name: string; new_method_name: string; parameter_renames: string StringMap.t}
@@ -23,10 +18,8 @@ let rename_mapping_aware_name_comparison (name1: string) (name2: string) (rename
 
   match existingAssumption with
   | Some now ->
-    (*Printf.printf "Assumption is: %s -> %s\n" original now;*)
     now = name2
   | None ->
-    (*Printf.printf "No assumption when %s, %s, %b\n" name1 name2 (name1 = name2);*)
     name1 = name2 (*Var names differ, but there is no assumption, so this can't be good*)
 
 let rename_mapping_to_string (rename_mapping: rename_mapping) =
@@ -39,18 +32,6 @@ let rename_mapping_to_string (rename_mapping: rename_mapping) =
                                String.concat ", " in
   "(local=" ^ local_string ^ "; methods=[" ^ methods_string ^ "])"
 
-let identifier_of_global glob =
-  match glob with
-  | GFun (fundec, l) -> {name = fundec.svar.vname; global_t = Fun}
-  | GVar (var, init, l) -> {name = var.vname; global_t = Var}
-  | GVarDecl (var, l) -> {name = var.vname; global_t = Decl}
-  | _ -> raise Not_found
-
-module GlobalMap = Map.Make(struct
-    type t = global_identifier [@@deriving ord]
-  end)
-
-
 (* hack: CIL generates new type names for anonymous types - we want to ignore these *)
 let compare_name (a: string) (b: string) =
   let anon_struct = "__anonstruct_" in
@@ -170,7 +151,6 @@ and eq_attribute  ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) (a:
   | Attr (name1, params1), Attr (name2, params2) -> name1 = name2 && GobList.equal (eq_attrparam ~rename_mapping ~acc ) params1 params2
 
 and eq_varinfo  (a: varinfo) (b: varinfo) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) =
-  (*Printf.printf "Comp %s with %s\n" a.vname b.vname;*)
 
   let (_, method_rename_mappings) = rename_mapping in
 
@@ -201,10 +181,7 @@ and eq_varinfo  (a: varinfo) (b: varinfo) ~(acc: (typ * typ) list) ~(rename_mapp
   let typeCheck = eq_typ_acc a.vtype b.vtype ~rename_mapping:typ_rename_mapping ~acc  in
   let attrCheck = GobList.equal (eq_attribute ~rename_mapping ~acc ) a.vattr b.vattr in
 
-  let result = isNamingOk && typeCheck && attrCheck &&
-               a.vstorage = b.vstorage && a.vglob = b.vglob && a.vaddrof = b.vaddrof in
-
-  result
+  isNamingOk && typeCheck && attrCheck && a.vstorage = b.vstorage && a.vglob = b.vglob && a.vaddrof = b.vaddrof
 (* Ignore the location, vid, vreferenced, vdescr, vdescrpure, vinline *)
 
 (* Accumulator is needed because of recursive types: we have to assume that two types we already encountered in a previous step of the recursion are equivalent *)

src/incremental/compareCIL.ml

@@ -4,20 +4,31 @@ open CilMaps
 include CompareAST
 include CompareCFG
 
+module GlobalMap = Map.Make(String)
+
+type global_def = Var of varinfo | Fun of fundec
+type global_col = {decls: varinfo option; def: global_def option}
+
+let name_of_global g = match g with
+  | GVar (v,_,_) -> v.vname
+  | GFun (f,_) -> f.svar.vname
+  | GVarDecl (v,_) -> v.vname
+  | _ -> failwith "global constructor not supported"
+
 type nodes_diff = {
   unchangedNodes: (node * node) list;
   primObsoleteNodes: node list; (** primary obsolete nodes -> all obsolete nodes are reachable from these *)
 }
 
 type unchanged_global = {
-  old: global;
-  current: global
+  old: global_col;
+  current: global_col
 }
 (** For semantically unchanged globals, still keep old and current version of global for resetting current to old. *)
 
 type changed_global = {
-  old: global;
-  current: global;
+  old: global_col;
+  current: global_col;
   unchangedHeader: bool;
   diff: nodes_diff option
 }
@@ -27,8 +38,8 @@ module VarinfoSet = Set.Make(CilType.Varinfo)
 type change_info = {
   mutable changed: changed_global list;
   mutable unchanged: unchanged_global list;
-  mutable removed: global list;
-  mutable added: global list;
+  mutable removed: global_col list;
+  mutable added: global_col list;
   mutable exclude_from_rel_destab: VarinfoSet.t;
   (** Set of functions that are to be force-reanalyzed.
       These functions are additionally included in the [changed] field, among the other changed globals. *)
@@ -104,98 +115,98 @@ let eqF (old: Cil.fundec) (current: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) opti
           if diffNodes1 = [] then (Unchanged, None)
           else (Changed, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1})
 
-let eq_glob (old: global) (current: global) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) = match old, current with
-  | GFun (f,_), GFun (g,_) -> eqF f g cfgs global_rename_mapping
-  | GVar (x, init_x, _), GVar (y, init_y, _) -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None (* ignore the init_info - a changed init of a global will lead to a different start state *)
-  | GVarDecl (x, _), GVarDecl (y, _) -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None
-  | _ -> ignore @@ Pretty.printf "Not comparable: %a and %a\n" Cil.d_global old Cil.d_global current; Changed, None
+let eq_glob (old: global_col) (current: global_col) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) =
+  match old.def, current.def with
+  | Some (Var x), Some (Var y) -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None (* ignore the init_info - a changed init of a global will lead to a different start state *)
+  | Some (Fun f), Some (Fun g) -> eqF f g cfgs global_rename_mapping
+  | None, None -> (match old.decls, current.decls with
+      | Some x, Some y -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None
+      | _, _ -> failwith "should never collect any empty entries in GlobalMap")
+  | _, _ -> Changed, None (* it is considered to be changed (not added or removed) because a global collection only exists in the map
+                             if there is at least one declaration or definition for this global *)
 
 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 =
+  let addGlobal map global  =
     try
-      let ident = identifier_of_global global in
-      let old_global = GlobalMap.find ident map in
+      let name, col = match global with
+        | GVar (v,_,_) -> v.vname, {decls = None; def = Some (Var v)}
+        | GFun (f,_) -> f.svar.vname, {decls = None; def = Some (Fun f)}
+        | GVarDecl (v,_) -> v.vname, {decls = Some v; def = None}
+        | _ -> raise Not_found in
+      let merge_d def1 def2 = match def1, def2 with
+        | Some d, None -> Some d
+        | None, Some d -> Some d
+        | None, None -> None
+        | _ -> failwith "there can only be one definition and one declaration per global" in
+      let merge_global_col entry = match entry with
+        | None -> Some col
+        | Some col' -> Some {decls = merge_d col.decls col'.decls; def = merge_d col.def col'.def} in
+      GlobalMap.update name merge_global_col map;
+    with
+      Not_found -> 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 |>
+  (* 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 generate_global_rename_mapping name current_global =
+    try
+      let old_global = GlobalMap.find name oldMap in
+      match old_global.def, current_global.def with
+      | Some (Fun f1), Some (Fun f2) ->
+        let renamed_params: string StringMap.t = if (List.length f1.sformals) = (List.length f2.sformals) then
+            let mappings = List.combine f1.sformals f2.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})
+        if not (f1.svar.vname = f2.svar.vname) || (StringMap.cardinal renamed_params) > 0 then
+          Some (f1.svar, {original_method_name = f1.svar.vname; new_method_name = f2.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
-      let gid_to_string gid = match gid.global_t with
-        | Var -> "Var " ^ gid.name
-        | Decl -> "Decl " ^ gid.name
-        | Fun -> "Fun " ^ gid.name in
-      if GlobalMap.mem gid map then failwith ("Duplicate global identifier: " ^ gid_to_string gid) else GlobalMap.add gid global map
-    with
-      Not_found -> map
-  in
+  let global_rename_mapping: method_rename_assumptions = GlobalMap.fold (fun name global_col current_global_rename_mapping ->
+      match generate_global_rename_mapping name global_col with
+      | Some (funVar, rename_mapping) -> VarinfoMap.add funVar rename_mapping current_global_rename_mapping
+      | None -> current_global_rename_mapping
+    ) newMap VarinfoMap.empty in
 
   let changes = empty_change_info () in
   global_typ_acc := [];
-  let findChanges map global global_rename_mapping =
+  let findChanges map name current_global global_rename_mapping =
     try
-      let ident = identifier_of_global global in
-      let old_global = GlobalMap.find ident map in
+      let old_global = GlobalMap.find name map in
       (* Do a (recursive) equal comparison ignoring location information *)
-      let change_status, diff = eq old_global global cfgs global_rename_mapping in
+      let change_status, diff = eq old_global current_global cfgs global_rename_mapping in
       let append_to_changed ~unchangedHeader =
-        changes.changed <- {current = global; old = old_global; unchangedHeader; diff} :: changes.changed
+        changes.changed <- {current = current_global; old = old_global; unchangedHeader; diff} :: changes.changed
       in
       match change_status with
       | Changed ->
         append_to_changed ~unchangedHeader:true
-      | Unchanged -> changes.unchanged <- {current = global; old = old_global} :: changes.unchanged
+      | Unchanged -> changes.unchanged <- {current = current_global; old = old_global} :: changes.unchanged
       | ChangedFunHeader f
       | ForceReanalyze f ->
         changes.exclude_from_rel_destab <- VarinfoSet.add f.svar changes.exclude_from_rel_destab;
         append_to_changed ~unchangedHeader:false;
-    with Not_found -> () (* Global was no variable or function, it does not belong into the map *)
-  in
-  let checkExists map global =
-    match identifier_of_global global with
-    | name -> GlobalMap.mem name map
-    | exception Not_found -> true (* return true, so isn't considered a change *)
-  in
-  (* 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
+    with Not_found -> changes.removed <- current_global::changes.removed (* Global could not be found in old map -> added *)
   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 -> findChanges oldMap glob global_rename_mapping);
+  GlobalMap.iter (fun name glob_col -> findChanges oldMap name glob_col global_rename_mapping) newMap;
 
   (* 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));
-  Cil.iterGlobals oldAST (fun glob -> if not (checkExists newMap glob) then changes.removed <- (glob::changes.removed));
+  GlobalMap.iter (fun name glob -> if not (GlobalMap.mem name newMap) then changes.removed <- (glob::changes.removed)) oldMap;
   changes
 
 (** Given an (optional) equality function between [Cil.global]s, an old and a new [Cil.file], this function computes a [change_info],

src/incremental/updateCil.ml

@@ -52,11 +52,12 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
   in
   let reset_globals (glob: unchanged_global) =
     try
-      match glob.current, glob.old with
-      | GFun (nw, _), GFun (old, _) -> reset_fun nw old
-      | GVar (nw, _, _), GVar (old, _, _) -> reset_var nw old
-      | GVarDecl (nw, _), GVarDecl (old, _) -> reset_var nw old
-      | _ -> ()
+      match glob.current.def, glob.old.def with
+      | Some (Fun nw), Some (Fun old) -> reset_fun nw old
+      | Some (Var nw), Some (Var old) -> reset_var nw old
+      | _, _ -> match glob.current.decls, glob.old.decls with
+        | Some nw, Some old -> reset_var nw old
+        | _, _ -> ()
     with Failure m -> ()
   in
   let assign_same_id fallstmts (old_n, n) = match old_n, n with
@@ -88,9 +89,16 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
       List.iter (reset_changed_stmt (List.map snd d.unchangedNodes)) f.sallstmts;
       List.iter (assign_same_id f.sallstmts) d.unchangedNodes
   in
+  let update_var (v: varinfo) =
+    v.vid <- make_vid ()
+  in
   let reset_changed_globals (changed: changed_global) =
-    match (changed.current, changed.old) with
-    | GFun (nw, _), GFun (old, _) -> reset_changed_fun nw old changed.unchangedHeader changed.diff
+    match (changed.current.def, changed.old.def) with
+    | Some (Fun nw), Some (Fun old) -> reset_changed_fun nw old changed.unchangedHeader changed.diff
+    | Some (Var nw), Some (Var old) -> update_var nw
+    | None, None -> (match (changed.current.decls, changed.old.decls) with
+        | Some nw, Some old -> update_var nw
+        | _ -> ())
     | _ -> ()
   in
   let update_fun (f: fundec) =
@@ -99,16 +107,14 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
     List.iter (fun f -> f.vid <- make_vid ()) f.sformals;
     List.iter (fun s -> s.sid <- make_sid ()) f.sallstmts;
   in
-  let update_var (v: varinfo) =
-    v.vid <- make_vid ()
-  in
-  let update_globals (glob: global) =
+  let update_globals (glob: global_col) =
     try
-      match glob with
-      | GFun (nw, _) -> update_fun nw
-      | GVar (nw, _, _) -> update_var nw
-      | GVarDecl (nw, _) -> update_var nw
-      | _ -> ()
+      match glob.def with
+      | Some (Fun nw) -> update_fun nw
+      | Some (Var nw) -> update_var nw
+      | _ -> match glob.decls with
+        | Some v1 -> update_var v1
+        | _ -> ()
     with Failure m -> ()
   in
   List.iter reset_globals changes.unchanged;

src/solvers/td3.ml

@@ -472,21 +472,21 @@ module WP =
             destabilize_normal;
 
         let changed_funs = List.filter_map (function
-            | {old = GFun (f, _); diff = None; _} ->
+            | {old = {def = Some (Fun f); _}; diff = None; _} ->
               print_endline ("Completely changed function: " ^ f.svar.vname);
               Some f
             | _ -> None
           ) S.increment.changes.changed
         in
         let part_changed_funs = List.filter_map (function
-            | {old = GFun (f, _); diff = Some nd; _} ->
+            | {old = {def = Some (Fun f); _}; diff = Some nd; _} ->
               print_endline ("Partially changed function: " ^ f.svar.vname);
               Some (f, nd.primObsoleteNodes, nd.unchangedNodes)
             | _ -> None
           ) S.increment.changes.changed
         in
         let removed_funs = List.filter_map (function
-            | GFun (f, _) ->
+            | {def = Some (Fun f); _} ->
               print_endline ("Removed function: " ^ f.svar.vname);
               Some f
             | _ -> None

src/util/server.ml

@@ -157,8 +157,8 @@ 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
-    | GFun (fdec, _) when CompareCIL.should_reanalyze fdec -> CompareCIL.ForceReanalyze fdec, None
+  let eq (glob: CompareCIL.global_col) _ _ _ = match glob.def with
+    | Some (Fun fdec) when CompareCIL.should_reanalyze fdec -> CompareCIL.ForceReanalyze fdec, None
     | _ -> Unchanged, None
   in
   CompareCIL.compareCilFiles ~eq file file