From 8f6cf6cde4a99f89f24a6635fde28f291b9ee10e Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Mon, 19 Sep 2022 16:18:58 +0200
Subject: [PATCH 1/8] drafting the per-global comparison

---
 src/incremental/compareAST.ml |  18 +-----
 src/incremental/compareCIL.ml | 115 +++++++++++++++++++++-------------
 2 files changed, 72 insertions(+), 61 deletions(-)

diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 55453369f2..6808c452ae 100644
--- a/src/incremental/compareAST.ml
+++ b/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}
@@ -39,18 +34,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
@@ -174,6 +157,7 @@ and eq_attribute (rename_mapping: rename_mapping) (a: attribute) (b: attribute)
 
 and eq_varinfo2 (rename_mapping: rename_mapping) (a: varinfo) (b: varinfo) = eq_varinfo a b rename_mapping
 
+(* TODO introduce default parameter for rename_mapping *)
 and eq_varinfo (a: varinfo) (b: varinfo) (rename_mapping: rename_mapping) =
   (*Printf.printf "Comp %s with %s\n" a.vname b.vname;*)
 
diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 6d70a229a9..956b2c5ef5 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -4,20 +4,32 @@ open CilMaps
 include CompareAST
 include CompareCFG
 
+(* global_type and global_t are implicitly used by GlobalMap to keep GVarDecl apart from GVar and GFun, so do not remove! *)
+module GlobalMap = Map.Make(String)
+
+type global_def = Var of varinfo | Fun of fundec
+and global_col = {decls: varinfo list; 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
 }
@@ -104,26 +116,55 @@ let eqF (old: Cil.fundec) (current: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) opti
           if diffNodes1 = [] then (Changed, 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 (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 (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 v1), Some (Var v2) -> unchanged_to_change_status (eq_varinfo v1 v2 (StringMap.empty, VarinfoMap.empty)), None
+  | Some (Fun f1), Some (Fun f2) -> eqF f1 f2 cfgs global_rename_mapping
+  | None, None -> (match old.decls, current.decls with
+      | v1::ls1, v2::ls2 -> unchanged_to_change_status (eq_varinfo v1 v2 (StringMap.empty, VarinfoMap.empty)), None (* TODO how to compare declarations? Iterate? *)
+      | _, _ -> 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  = (* TODO: check consistency of id's *)
     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 = []; def = Some (Var v)}
+        | GFun (f,_) -> f.svar.vname, {decls = []; def = Some (Fun f)}
+        | GVarDecl (v,_) -> v.vname, {decls = [v]; def = None}
+        | _ -> failwith "no definition or declaration of global" in
+      let merge_def def1 def2 = match def1, def2 with
+        | Some d, None -> Some d
+        | None, Some d -> Some d
+        | None, None -> None
+        | _ -> failwith "there can be only one definition per global" in
+      let merge_global_col entry = match entry with
+        | None -> Some col
+        | Some col' -> Some {decls = col.decls @ col'.decls; def = merge_def col.def col'.def} in
+      GlobalMap.update name merge_global_col map;
+    with
+      Not_found -> map
+  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
 
-      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 |>
+  let generate_global_rename_mapping global =
+    try
+      let name = name_of_global global in
+      let old_global = GlobalMap.find name oldMap in
+      let current_global = GlobalMap.find name newMap 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
@@ -132,40 +173,36 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
             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
+  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 global with
+      | Some (funVar, rename_mapping) -> VarinfoMap.add funVar rename_mapping current_global_rename_mapping
+      | None -> current_global_rename_mapping
+    ) VarinfoMap.empty
   in
 
   let changes = empty_change_info () in
   global_typ_acc := [];
   let findChanges map global global_rename_mapping =
     try
-      let ident = identifier_of_global global in
-      let old_global = GlobalMap.find ident map in
+      let name = name_of_global global in
+      let old_global = GlobalMap.find name map in
+      let current_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;
@@ -173,20 +210,10 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
     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
+    match name_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
-  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. *)

From a8ca548b84e00809f745ac6f89442d98699d3899 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Mon, 19 Sep 2022 17:05:45 +0200
Subject: [PATCH 2/8] adjust updating of ids and solver data preparation

---
 src/incremental/compareCIL.ml | 37 +++++++++++------------------------
 src/incremental/updateCil.ml  | 29 +++++++++++++++------------
 src/solvers/td3.ml            |  6 +++---
 src/util/server.ml            |  4 ++--
 4 files changed, 32 insertions(+), 44 deletions(-)

diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 956b2c5ef5..b6dfe250ce 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -39,8 +39,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. *)
@@ -137,7 +137,7 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
         | GVar (v,_,_) -> v.vname, {decls = []; def = Some (Var v)}
         | GFun (f,_) -> f.svar.vname, {decls = []; def = Some (Fun f)}
         | GVarDecl (v,_) -> v.vname, {decls = [v]; def = None}
-        | _ -> failwith "no definition or declaration of global" in
+        | _ -> raise Not_found in
       let merge_def def1 def2 = match def1, def2 with
         | Some d, None -> Some d
         | None, Some d -> Some d
@@ -155,12 +155,9 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
   let oldMap = Cil.foldGlobals oldAST addGlobal GlobalMap.empty in
   let newMap = Cil.foldGlobals newAST addGlobal GlobalMap.empty in
 
-  let generate_global_rename_mapping global =
+  let generate_global_rename_mapping name current_global =
     try
-      let name = name_of_global global in
       let old_global = GlobalMap.find name oldMap in
-      let current_global = GlobalMap.find name newMap 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
@@ -169,10 +166,8 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
                            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 (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
@@ -180,20 +175,17 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
     with Not_found -> None
   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 global with
+  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
-    ) VarinfoMap.empty
-  in
+    ) 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 name = name_of_global global in
       let old_global = GlobalMap.find name map in
-      let current_global = GlobalMap.find name map in
       (* Do a (recursive) equal comparison ignoring location information *)
       let change_status, diff = eq old_global current_global cfgs global_rename_mapping in
       let append_to_changed ~unchangedHeader =
@@ -207,22 +199,15 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
       | 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 name_of_global global with
-    | name -> GlobalMap.mem name map
-    | exception Not_found -> true (* return true, so isn't considered a change *)
+    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],
diff --git a/src/incremental/updateCil.ml b/src/incremental/updateCil.ml
index d7fe25f438..e4b0c96e43 100644
--- a/src/incremental/updateCil.ml
+++ b/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
+        | nw::ls1, old::ls2 -> reset_var nw old
+        | _, _ -> ()
     with Failure m -> ()
   in
   let assign_same_id fallstmts (old_n, n) = match old_n, n with
@@ -89,8 +90,9 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
       List.iter (assign_same_id f.sallstmts) d.unchangedNodes
   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
+    (* why ids of global variables not adapted? *)
     | _ -> ()
   in
   let update_fun (f: fundec) =
@@ -102,13 +104,14 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
   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
+        | v1::ls1 -> update_var v1
+        | _ -> ()
     with Failure m -> ()
   in
   List.iter reset_globals changes.unchanged;
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 082ca94e7c..d62e008e01 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -460,21 +460,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
diff --git a/src/util/server.ml b/src/util/server.ml
index 13a9cb738a..82f045b795 100644
--- a/src/util/server.ml
+++ b/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

From ffb21ae19dc4caa197657b0c3bea1f5efe895e2a Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Tue, 20 Sep 2022 12:58:07 +0200
Subject: [PATCH 3/8] only one declaration per global

---
 src/incremental/compareCIL.ml | 16 ++++++++--------
 src/incremental/updateCil.ml  |  4 ++--
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index b6dfe250ce..8e3847d413 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -8,7 +8,7 @@ include CompareCFG
 module GlobalMap = Map.Make(String)
 
 type global_def = Var of varinfo | Fun of fundec
-and global_col = {decls: varinfo list; def: global_def option}
+and global_col = {decls: varinfo option; def: global_def option}
 
 let name_of_global g = match g with
   | GVar (v,_,_) -> v.vname
@@ -121,7 +121,7 @@ let eq_glob (old: global_col) (current: global_col) (cfgs : (cfg * (cfg * cfg))
   | Some (Var v1), Some (Var v2) -> unchanged_to_change_status (eq_varinfo v1 v2 (StringMap.empty, VarinfoMap.empty)), None
   | Some (Fun f1), Some (Fun f2) -> eqF f1 f2 cfgs global_rename_mapping
   | None, None -> (match old.decls, current.decls with
-      | v1::ls1, v2::ls2 -> unchanged_to_change_status (eq_varinfo v1 v2 (StringMap.empty, VarinfoMap.empty)), None (* TODO how to compare declarations? Iterate? *)
+      | Some v1, Some v2 -> unchanged_to_change_status (eq_varinfo v1 v2 (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 *)
@@ -134,18 +134,18 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
   let addGlobal map global  = (* TODO: check consistency of id's *)
     try
       let name, col = match global with
-        | GVar (v,_,_) -> v.vname, {decls = []; def = Some (Var v)}
-        | GFun (f,_) -> f.svar.vname, {decls = []; def = Some (Fun f)}
-        | GVarDecl (v,_) -> v.vname, {decls = [v]; def = None}
+        | 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_def def1 def2 = match def1, def2 with
+      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 be only one definition per global" in
+        | _ -> 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 = col.decls @ col'.decls; def = merge_def col.def col'.def} in
+        | 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
diff --git a/src/incremental/updateCil.ml b/src/incremental/updateCil.ml
index e4b0c96e43..c6aae8d5b4 100644
--- a/src/incremental/updateCil.ml
+++ b/src/incremental/updateCil.ml
@@ -56,7 +56,7 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
       | 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
-        | nw::ls1, old::ls2 -> reset_var nw old
+        | Some nw, Some old -> reset_var nw old
         | _, _ -> ()
     with Failure m -> ()
   in
@@ -110,7 +110,7 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
       | Some (Fun nw) -> update_fun nw
       | Some (Var nw) -> update_var nw
       | _ -> match glob.decls with
-        | v1::ls1 -> update_var v1
+        | Some v1 -> update_var v1
         | _ -> ()
     with Failure m -> ()
   in

From 029278afe1f2e26ff1a065dd8d94bdde17b40a82 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Tue, 20 Sep 2022 15:51:06 +0200
Subject: [PATCH 4/8] cleanup

---
 src/incremental/compareCIL.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 8e3847d413..306a8f8723 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -131,7 +131,7 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
     then Some (CfgTools.getCFG oldAST |> fst, CfgTools.getCFG newAST)
     else None in
 
-  let addGlobal map global  = (* TODO: check consistency of id's *)
+  let addGlobal map global  =
     try
       let name, col = match global with
         | GVar (v,_,_) -> v.vname, {decls = None; def = Some (Var v)}

From ccf64229354d1bbc55c095a78774f772bfa1931a Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Fri, 23 Sep 2022 09:58:27 +0200
Subject: [PATCH 5/8] remove outdated comment

---
 src/incremental/compareCIL.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 306a8f8723..3845ace1b3 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -4,7 +4,6 @@ open CilMaps
 include CompareAST
 include CompareCFG
 
-(* global_type and global_t are implicitly used by GlobalMap to keep GVarDecl apart from GVar and GFun, so do not remove! *)
 module GlobalMap = Map.Make(String)
 
 type global_def = Var of varinfo | Fun of fundec

From 765faf8e86d44168b07c36677267c2b31ec1e049 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Tue, 27 Sep 2022 16:39:32 +0200
Subject: [PATCH 6/8] update ids of changed globals

---
 src/incremental/compareCIL.ml |  2 +-
 src/incremental/updateCil.ml  | 11 +++++++----
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 3845ace1b3..0de3efca6c 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -7,7 +7,7 @@ include CompareCFG
 module GlobalMap = Map.Make(String)
 
 type global_def = Var of varinfo | Fun of fundec
-and global_col = {decls: varinfo option; def: global_def option}
+type global_col = {decls: varinfo option; def: global_def option}
 
 let name_of_global g = match g with
   | GVar (v,_,_) -> v.vname
diff --git a/src/incremental/updateCil.ml b/src/incremental/updateCil.ml
index c6aae8d5b4..2f9628b4c1 100644
--- a/src/incremental/updateCil.ml
+++ b/src/incremental/updateCil.ml
@@ -89,10 +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.def, changed.old.def) with
     | Some (Fun nw), Some (Fun old) -> reset_changed_fun nw old changed.unchangedHeader changed.diff
-    (* why ids of global variables not adapted? *)
+    | 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) =
@@ -101,9 +107,6 @@ 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_col) =
     try
       match glob.def with

From a49710d59cd2337fecefc1ebae1f4ae76eb5acfa Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Tue, 27 Sep 2022 17:01:10 +0200
Subject: [PATCH 7/8] cleanup

---
 src/incremental/compareAST.ml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 6808c452ae..977868c62e 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -18,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) =
@@ -159,8 +157,6 @@ and eq_varinfo2 (rename_mapping: rename_mapping) (a: varinfo) (b: varinfo) = eq_
 
 (* TODO introduce default parameter for rename_mapping *)
 and eq_varinfo (a: varinfo) (b: varinfo) (rename_mapping: rename_mapping) =
-  (*Printf.printf "Comp %s with %s\n" a.vname b.vname;*)
-
   let (_, method_rename_mappings) = rename_mapping in
 
   (*When we compare function names, we can directly compare the naming from the rename_mapping if it exists.*)
@@ -190,12 +186,7 @@ and eq_varinfo (a: varinfo) (b: varinfo) (rename_mapping: rename_mapping) =
   let typeCheck = eq_typ a.vtype b.vtype typ_rename_mapping in
   let attrCheck = GobList.equal (eq_attribute rename_mapping) a.vattr b.vattr in
 
-  (*let _ = Printf.printf "Comparing vars: %s = %s\n" a.vname b.vname in *)
-  (*a.vname = b.vname*)
-  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 *)

From 4114bfd625c523ed221888500b6536b277fffb8b Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Tue, 15 Nov 2022 17:03:39 +0100
Subject: [PATCH 8/8] explicitly ignore extra record fields

---
 src/solvers/td3.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 7bf9c29d1c..ebfc014a2b 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -460,21 +460,21 @@ module WP =
             destabilize_normal;
 
         let changed_funs = List.filter_map (function
-            | {old = {def = Some (Fun 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 = {def = Some (Fun 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
-            | {def = Some (Fun f)} ->
+            | {def = Some (Fun f); _} ->
               print_endline ("Removed function: " ^ f.svar.vname);
               Some f
             | _ -> None