From 1e673061360738e7dd140f083e66cc20efd5eade Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 15 Feb 2022 18:00:15 +0200
Subject: [PATCH 01/12] Pass incremental data to solver via argument instead of
 constraint system module

---
 src/framework/analyses.ml     | 4 ++--
 src/framework/constraints.ml  | 8 ++++----
 src/framework/control.ml      | 6 +++---
 src/solvers/selector.ml       | 4 ++--
 src/solvers/td3.ml            | 6 +++---
 unittest/solver/solverTest.ml | 2 +-
 6 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 1cbe6d61af..7e9a462e5f 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -550,7 +550,7 @@ module type GenericEqBoxIncrSolverBase =
     (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs],
         reached from starting values [xs].
         As a second component the solver returns data structures for incremental serialization. *)
-    val solve : (S.v -> S.d -> S.d -> S.d) -> (S.v*S.d) list -> S.v list -> S.d H.t * marshal
+    val solve : (S.v -> S.d -> S.d -> S.d) -> (S.v*S.d) list -> S.v list -> marshal option -> S.d H.t * marshal
   end
 
 (** (Incremental) solver argument, indicating which postsolving should be performed by the solver. *)
@@ -588,7 +588,7 @@ module type GenericGlobSolver =
     (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs],
         reached from starting values [xs].
         As a second component the solver returns data structures for incremental serialization. *)
-    val solve : (S.LVar.t*S.D.t) list -> (S.GVar.t*S.G.t) list -> S.LVar.t list -> (S.D.t LH.t * S.G.t GH.t) * marshal
+    val solve : (S.LVar.t*S.D.t) list -> (S.GVar.t*S.G.t) list -> S.LVar.t list -> marshal option -> (S.D.t LH.t * S.G.t GH.t) * marshal
   end
 
 module ResultType2 (S:Spec) =
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index ae8c9f465b..741818f2e9 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -795,7 +795,7 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve
 
     type marshal = unit
 
-    let solve box xs vs =
+    let solve box xs vs _ =
       let vh = Sol.solve box xs vs in
       Post.post xs vs vh;
       (vh, ())
@@ -925,7 +925,7 @@ end
 
 (** Transforms a [GenericEqBoxIncrSolver] into a [GenericGlobSolver]. *)
 module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase)
-  : GenericGlobSolver
+  (* : GenericGlobSolver *)
   = functor (S:GlobConstrSys) ->
     functor (LH:Hashtbl.S with type key=S.LVar.t) ->
     functor (GH:Hashtbl.S with type key=S.GVar.t) ->
@@ -939,11 +939,11 @@ module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase)
 
       type marshal = Sol'.marshal
 
-      let solve ls gs l =
+      let solve ls gs l old_data =
         let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls
                  @ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in
         let sv = List.map (fun x -> `L x) l in
-        let hm, solver_data = Sol'.solve EqSys.box vs sv in
+        let hm, solver_data = Sol'.solve EqSys.box vs sv old_data in
         Splitter.split_solution hm, solver_data
     end
 
diff --git a/src/framework/control.ml b/src/framework/control.ml
index fa2e4e3fee..1060de3474 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -420,7 +420,7 @@ struct
 
       let lh, gh = if load_run <> "" then (
           let module S2' = (GlobSolverFromEqSolver (Generic.LoadRunIncrSolver (PostSolverArg))) (EQSys) (LHT) (GHT) in
-          let (r2, _) = S2'.solve entrystates entrystates_global startvars' in
+          let (r2, _) = S2'.solve entrystates entrystates_global startvars' None in (* TODO: has incremental data? *)
           r2
         ) else if compare_runs <> [] then (
           match compare_runs with
@@ -463,7 +463,7 @@ struct
           if get_bool "dbg.verbose" then
             print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ ".");
           Goblintutil.should_warn := get_string "warn_at" = "early" || gobview;
-          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' in
+          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' (Option.map (fun {solver_data; _} -> solver_data) Inc.increment.old_data) in
           if GobConfig.get_bool "incremental.save" then
             Serialize.Cache.(update_data SolverData solver_data);
           if save_run_str <> "" then (
@@ -512,7 +512,7 @@ struct
           end
           in
           let module S2' = (GlobSolverFromEqSolver (S2 (PostSolverArg2))) (EQSys) (LHT) (GHT) in
-          let (r2, _) = S2'.solve entrystates entrystates_global startvars' in
+          let (r2, _) = S2'.solve entrystates entrystates_global startvars' None in (* TODO: has incremental data? *)
           CompareGlobSys.compare (get_string "solver", get_string "comparesolver") (lh,gh) (r2)
         in
         compare_with (Selector.choose_solver (get_string "comparesolver"))
diff --git a/src/solvers/selector.ml b/src/solvers/selector.ml
index 856ceaca91..cc75ed96e8 100644
--- a/src/solvers/selector.ml
+++ b/src/solvers/selector.ml
@@ -22,10 +22,10 @@ module Make =
   struct
     type marshal = Obj.t (* cannot use Sol.marshal because cannot unpack first-class module in applicative functor *)
 
-    let solve box xs vs =
+    let solve box xs vs (old_data: marshal option) =
       let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in
       let module F = Sol (Arg) (S) (VH) in
-      let (vh, marshal) = F.solve box xs vs in
+      let (vh, marshal) = F.solve box xs vs (Option.map Obj.obj old_data) in
       (vh, Obj.repr marshal)
   end
 
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 0eccc5c679..82aad16db1 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -997,12 +997,12 @@ module WP =
       verify_data data;
       {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}
 
-    let solve box st vs =
+    let solve box st vs (old_data: marshal option) =
       let reuse_stable = GobConfig.get_bool "incremental.stable" in
       let reuse_wpoint = GobConfig.get_bool "incremental.wpoint" in
       if GobConfig.get_bool "incremental.load" then (
-        let loaded, data = match S.increment.old_data with
-          | Some d -> true, Obj.obj d.solver_data
+        let loaded, data = match old_data with
+          | Some d -> true, d
           | _ -> false, create_empty_data ()
         in
         (* This hack is for fixing hashconsing.
diff --git a/unittest/solver/solverTest.ml b/unittest/solver/solverTest.ml
index 6668aacceb..574b42f4cf 100644
--- a/unittest/solver/solverTest.ml
+++ b/unittest/solver/solverTest.ml
@@ -60,7 +60,7 @@ module Solver = Constraints.GlobSolverFromEqSolver (Constraints.EqIncrSolverFrom
 
 let test1 _ =
   let id x = x in
-  let ((sol, gsol), _) = Solver.solve [] [] ["w"] in
+  let ((sol, gsol), _) = Solver.solve [] [] ["w"] None in
   assert_equal ~printer:id "42" (Int.show (GH.find gsol "g"));
   assert_equal ~printer:id "42" (Int.show (LH.find sol "x"));
   assert_equal ~printer:id "8"  (Int.show (LH.find sol "y"));

From 166357344e2cff1f0d982154a3b31bbef41e41c8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 16 Feb 2022 10:46:35 +0200
Subject: [PATCH 02/12] Remove analyzed_data record

---
 src/framework/analyses.ml | 8 ++------
 src/framework/control.ml  | 2 +-
 src/maingoblint.ml        | 6 +++---
 src/util/server.ml        | 8 ++++----
 4 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 7e9a462e5f..1043980c86 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -476,14 +476,10 @@ sig
   val access: (D.t, G.t, C.t, V.t) ctx -> Queries.access -> A.t
 end
 
-type analyzed_data = {
-  solver_data: Obj.t;
-}
-
 type increment_data = {
   server: bool;
 
-  old_data: analyzed_data option;
+  solver_data: Obj.t option;
   changes: CompareCIL.change_info;
 
   (* Globals for which the constraint
@@ -493,7 +489,7 @@ type increment_data = {
 
 let empty_increment_data ?(server=false) () = {
   server;
-  old_data = None;
+  solver_data = None;
   changes = CompareCIL.empty_change_info ();
   restarting = []
 }
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 1060de3474..61f2255dcf 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -463,7 +463,7 @@ struct
           if get_bool "dbg.verbose" then
             print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ ".");
           Goblintutil.should_warn := get_string "warn_at" = "early" || gobview;
-          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' (Option.map (fun {solver_data; _} -> solver_data) Inc.increment.old_data) in
+          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' Inc.increment.solver_data in
           if GobConfig.get_bool "incremental.save" then
             Serialize.Cache.(update_data SolverData solver_data);
           if save_run_str <> "" then (
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 5ee6dac72d..1625db9286 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -562,11 +562,11 @@ let diff_and_rename current_file =
       Serialize.Cache.(update_data CilFile current_file);
       Serialize.Cache.(update_data VersionData max_ids);
     end;
-    let old_data = match old_file, solver_data with
-      | Some cil_file, Some solver_data -> Some ({solver_data}: Analyses.analyzed_data)
+    let solver_data = match old_file, solver_data with
+      | Some cil_file, Some solver_data -> Some solver_data
       | _, _ -> None
     in
-    {server = false; Analyses.changes = changes; restarting; old_data}
+    {server = false; Analyses.changes = changes; restarting; solver_data}
   in change_info
 
 let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *)
diff --git a/src/util/server.ml b/src/util/server.ml
index 580cbc9d84..a351d7aff3 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -167,15 +167,15 @@ let increment_data (s: t) file reparsed = match Serialize.Cache.get_opt_data Sol
   | Some solver_data when reparsed ->
     let s_file = Option.get s.file in
     let changes = CompareCIL.compareCilFiles s_file file in
-    let old_data = Some { Analyses.solver_data } in
+    let solver_data = Some solver_data in
     s.max_ids <- UpdateCil.update_ids s_file s.max_ids file changes;
     (* TODO: get globals for restarting from config *)
-    { server = true; Analyses.changes; old_data; restarting = [] }, false
+    { server = true; Analyses.changes; solver_data; restarting = [] }, false
   | Some solver_data ->
     let changes = virtual_changes file in
-    let old_data = Some { Analyses.solver_data } in
+    let solver_data = Some solver_data in
     (* TODO: get globals for restarting from config *)
-    { server = true; Analyses.changes; old_data; restarting = [] }, false
+    { server = true; Analyses.changes; solver_data; restarting = [] }, false
   | _ -> Analyses.empty_increment_data ~server:true (), true
 
 let analyze ?(reset=false) (s: t) =

From bf81e95972410387c22bbfdf2f7fe51a95b08139 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 16 Feb 2022 10:55:23 +0200
Subject: [PATCH 03/12] Make incremental_data optional

---
 src/framework/analyses.ml    | 13 +++----------
 src/framework/constraints.ml |  2 +-
 src/framework/control.ml     |  2 +-
 src/goblint.ml               |  2 +-
 src/maingoblint.ml           | 10 ++++------
 src/solvers/td3.ml           | 20 +++++++++++++-------
 src/util/server.ml           |  8 +++-----
 7 files changed, 26 insertions(+), 31 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 1043980c86..3a682ec525 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -479,7 +479,7 @@ end
 type increment_data = {
   server: bool;
 
-  solver_data: Obj.t option;
+  solver_data: Obj.t;
   changes: CompareCIL.change_info;
 
   (* Globals for which the constraint
@@ -487,13 +487,6 @@ type increment_data = {
   restarting: VarQuery.t list;
 }
 
-let empty_increment_data ?(server=false) () = {
-  server;
-  solver_data = None;
-  changes = CompareCIL.empty_change_info ();
-  restarting = []
-}
-
 (** A side-effecting system. *)
 module type MonSystem =
 sig
@@ -514,7 +507,7 @@ sig
   val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m
 
   (** Data used for incremental analysis *)
-  val increment : increment_data
+  val increment : increment_data option
 
   val iter_vars: (v -> d) -> VarQuery.t -> v VarQuery.f -> unit
 end
@@ -530,7 +523,7 @@ sig
 
   module D : Lattice.S
   module G : Lattice.S
-  val increment : increment_data
+  val increment : increment_data option
   val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option
   val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit
 end
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 741818f2e9..b4b1d1a86c 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -434,7 +434,7 @@ end
 
 module type Increment =
 sig
-  val increment: increment_data
+  val increment: increment_data option
 end
 
 (** The main point of this file---generating a [GlobConstrSys] from a [Spec]. *)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 61f2255dcf..a8eb5530eb 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -463,7 +463,7 @@ struct
           if get_bool "dbg.verbose" then
             print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ ".");
           Goblintutil.should_warn := get_string "warn_at" = "early" || gobview;
-          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' Inc.increment.solver_data in
+          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' (Option.map (fun {solver_data; _} -> solver_data) Inc.increment) in
           if GobConfig.get_bool "incremental.save" then
             Serialize.Cache.(update_data SolverData solver_data);
           if save_run_str <> "" then (
diff --git a/src/goblint.ml b/src/goblint.ml
index 8dc2e3b00f..893160022d 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -56,7 +56,7 @@ let main () =
         if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then
           diff_and_rename file
         else
-          Analyses.empty_increment_data ()
+          None
       in
       if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;
       file |> do_analyze changeInfo;
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 1625db9286..dd8001606b 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -526,7 +526,7 @@ let handle_extraspecials () =
 (* Detects changes and renames vids and sids. *)
 let diff_and_rename current_file =
   (* Create change info, either from old results, or from scratch if there are no previous results. *)
-  let change_info: Analyses.increment_data =
+  let change_info: Analyses.increment_data option =
     let warn m = eprint_color ("{yellow}Warning: "^m) in
     if GobConfig.get_bool "incremental.load" && not (Serialize.results_exist ()) then begin
       warn "incremental.load is activated but no data exists that can be loaded."
@@ -562,11 +562,9 @@ let diff_and_rename current_file =
       Serialize.Cache.(update_data CilFile current_file);
       Serialize.Cache.(update_data VersionData max_ids);
     end;
-    let solver_data = match old_file, solver_data with
-      | Some cil_file, Some solver_data -> Some solver_data
-      | _, _ -> None
-    in
-    {server = false; Analyses.changes = changes; restarting; solver_data}
+    match old_file, solver_data with
+    | Some cil_file, Some solver_data -> Some {server = false; Analyses.changes = changes; restarting; solver_data}
+    | _, _ -> None
   in change_info
 
 let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *)
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 82aad16db1..f979c8ae4e 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -371,7 +371,10 @@ module WP =
       let restart_write_only = GobConfig.get_bool "incremental.restart.write-only" in
 
       if GobConfig.get_bool "incremental.load" then (
-        let c = S.increment.changes in
+        let c = match S.increment with
+          | Some {changes; _} -> changes
+          | None -> empty_change_info ()
+        in
         List.(Printf.printf "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed));
 
         let restart_leaf x =
@@ -476,21 +479,21 @@ module WP =
               print_endline ("Completely changed function: " ^ f.svar.vname);
               Some f
             | _ -> None
-          ) S.increment.changes.changed
+          ) c.changed
         in
         let part_changed_funs = List.filter_map (function
             | {old = GFun (f, _); diff = Some nd; _} ->
               print_endline ("Partially changed function: " ^ f.svar.vname);
               Some (f, nd.primObsoleteNodes, nd.unchangedNodes)
             | _ -> None
-          ) S.increment.changes.changed
+          ) c.changed
         in
         let removed_funs = List.filter_map (function
             | GFun (f, _) ->
               print_endline ("Removed function: " ^ f.svar.vname);
               Some f
             | _ -> None
-          ) S.increment.changes.removed
+          ) c.removed
         in
 
         let mark_node hm f node =
@@ -504,7 +507,7 @@ module WP =
         let reanalyze_entry f =
           (* destabilize the entry points of a changed function when reluctant is off,
              or the function is to be force-reanalyzed  *)
-          (not reluctant) || CompareCIL.VarinfoSet.mem f.svar S.increment.changes.exclude_from_rel_destab
+          (not reluctant) || CompareCIL.VarinfoSet.mem f.svar c.exclude_from_rel_destab
         in
         let obsolete_ret = HM.create 103 in
         let obsolete_entry = HM.create 103 in
@@ -630,7 +633,10 @@ module WP =
           destabilize_normal x
 
         in
-        let globals_to_restart = S.increment.restarting in
+        let globals_to_restart = match S.increment with
+          | Some {restarting; _} -> restarting
+          | None -> []
+        in
         let get x = try HM.find rho x with Not_found -> S.Dom.bot () in
 
         List.iter
@@ -1020,7 +1026,7 @@ module WP =
          * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have
          *   the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values).
          *)
-        if loaded && S.increment.server then (
+        if loaded && (match S.increment with Some {server; _} -> server | None -> false) then (
           data.rho <- HM.copy data.rho;
           data.stable <- HM.copy data.stable;
           data.wpoint <- HM.copy data.wpoint;
diff --git a/src/util/server.ml b/src/util/server.ml
index a351d7aff3..44000d19be 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -167,16 +167,14 @@ let increment_data (s: t) file reparsed = match Serialize.Cache.get_opt_data Sol
   | Some solver_data when reparsed ->
     let s_file = Option.get s.file in
     let changes = CompareCIL.compareCilFiles s_file file in
-    let solver_data = Some solver_data in
     s.max_ids <- UpdateCil.update_ids s_file s.max_ids file changes;
     (* TODO: get globals for restarting from config *)
-    { server = true; Analyses.changes; solver_data; restarting = [] }, false
+    Some { server = true; Analyses.changes; solver_data; restarting = [] }, false
   | Some solver_data ->
     let changes = virtual_changes file in
-    let solver_data = Some solver_data in
     (* TODO: get globals for restarting from config *)
-    { server = true; Analyses.changes; solver_data; restarting = [] }, false
-  | _ -> Analyses.empty_increment_data ~server:true (), true
+    Some { server = true; Analyses.changes; solver_data; restarting = [] }, false
+  | _ -> None, true
 
 let analyze ?(reset=false) (s: t) =
   Messages.Table.(MH.clear messages_table);

From 4dfc6c9552d28cda6d83d126fc4b4a96468a18ba Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 3 Oct 2022 13:57:36 +0300
Subject: [PATCH 04/12] Fix partial Stats.time in Control

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

diff --git a/src/framework/control.ml b/src/framework/control.ml
index a8eb5530eb..6848d24649 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -463,7 +463,7 @@ struct
           if get_bool "dbg.verbose" then
             print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ ".");
           Goblintutil.should_warn := get_string "warn_at" = "early" || gobview;
-          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' (Option.map (fun {solver_data; _} -> solver_data) Inc.increment) in
+          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global startvars') (Option.map (fun {solver_data; _} -> solver_data) Inc.increment) in
           if GobConfig.get_bool "incremental.save" then
             Serialize.Cache.(update_data SolverData solver_data);
           if save_run_str <> "" then (

From 22999cf578101b792cfebf10438b3a15ac88f108 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 3 Oct 2022 14:11:46 +0300
Subject: [PATCH 05/12] Extract copy_marshal and relift_marshal in TD3

---
 src/solvers/td3.ml | 139 +++++++++++++++++++++++----------------------
 1 file changed, 72 insertions(+), 67 deletions(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index f979c8ae4e..c48710a6a2 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -71,6 +71,73 @@ module WP =
         (* vice versa doesn't currently hold, because stable is not pruned *)
       )
 
+    let copy_marshal (data: marshal): unit = (* TODO: should return new marshal? *)
+      data.rho <- HM.copy data.rho;
+      data.stable <- HM.copy data.stable;
+      data.wpoint <- HM.copy data.wpoint;
+      data.infl <- HM.copy data.infl;
+      data.side_infl <- HM.copy data.side_infl;
+      data.side_dep <- HM.copy data.side_dep;
+      (* data.st is immutable, no need to copy *)
+      data.var_messages <- HM.copy data.var_messages;
+      data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *)
+      data.dep <- HM.copy data.dep
+
+    let relift_marshal (data: marshal): unit = (* TODO: should return new marshal? *)
+      let rho' = HM.create (HM.length data.rho) in
+      HM.iter (fun k v ->
+          (* call hashcons on contexts and abstract values; results in new tags *)
+          let k' = S.Var.relift k in
+          let v' = S.Dom.relift v in
+          HM.replace rho' k' v';
+        ) data.rho;
+      data.rho <- rho';
+      let stable' = HM.create (HM.length data.stable) in
+      HM.iter (fun k v ->
+          HM.replace stable' (S.Var.relift k) v
+        ) data.stable;
+      data.stable <- stable';
+      let wpoint' = HM.create (HM.length data.wpoint) in
+      HM.iter (fun k v ->
+          HM.replace wpoint' (S.Var.relift k) v
+        ) data.wpoint;
+      data.wpoint <- wpoint';
+      let infl' = HM.create (HM.length data.infl) in
+      HM.iter (fun k v ->
+          HM.replace infl' (S.Var.relift k) (VS.map S.Var.relift v)
+        ) data.infl;
+      data.infl <- infl';
+      let side_infl' = HM.create (HM.length data.side_infl) in
+      HM.iter (fun k v ->
+          HM.replace side_infl' (S.Var.relift k) (VS.map S.Var.relift v)
+        ) data.side_infl;
+      data.side_infl <- side_infl';
+      let side_dep' = HM.create (HM.length data.side_dep) in
+      HM.iter (fun k v ->
+          HM.replace side_dep' (S.Var.relift k) (VS.map S.Var.relift v)
+        ) data.side_dep;
+      data.side_dep <- side_dep';
+      data.st <- List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st;
+      let var_messages' = HM.create (HM.length data.var_messages) in
+      HM.iter (fun k v ->
+          HM.add var_messages' (S.Var.relift k) v (* var_messages contains duplicate keys, so must add not replace! *)
+        ) data.var_messages;
+      data.var_messages <- var_messages';
+      let rho_write' = HM.create (HM.length data.rho_write) in
+      HM.iter (fun x w ->
+          let w' = HM.create (HM.length w) in
+          HM.iter (fun y d ->
+              HM.add w' (S.Var.relift y) (S.Dom.relift d) (* w contains duplicate keys, so must add not replace! *)
+            ) w;
+          HM.replace rho_write' (S.Var.relift x) w';
+        ) data.rho_write;
+      data.rho_write <- rho_write';
+      let dep' = HM.create (HM.length data.dep) in
+      HM.iter (fun k v ->
+          HM.replace dep' (S.Var.relift k) (VS.map S.Var.relift v)
+        ) data.dep;
+      data.dep <- dep'
+
     let exists_key f hm = HM.fold (fun k _ a -> a || f k) hm false
 
     module P =
@@ -1026,73 +1093,11 @@ module WP =
          * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have
          *   the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values).
          *)
-        if loaded && (match S.increment with Some {server; _} -> server | None -> false) then (
-          data.rho <- HM.copy data.rho;
-          data.stable <- HM.copy data.stable;
-          data.wpoint <- HM.copy data.wpoint;
-          data.infl <- HM.copy data.infl;
-          data.side_infl <- HM.copy data.side_infl;
-          data.side_dep <- HM.copy data.side_dep;
-          (* data.st is immutable, no need to copy *)
-          data.var_messages <- HM.copy data.var_messages;
-          data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *)
-          data.dep <- HM.copy data.dep;
-        )
-        else if loaded && GobConfig.get_bool "ana.opt.hashcons" then (
-          let rho' = HM.create (HM.length data.rho) in
-          HM.iter (fun k v ->
-              (* call hashcons on contexts and abstract values; results in new tags *)
-              let k' = S.Var.relift k in
-              let v' = S.Dom.relift v in
-              HM.replace rho' k' v';
-            ) data.rho;
-          data.rho <- rho';
-          let stable' = HM.create (HM.length data.stable) in
-          HM.iter (fun k v ->
-              HM.replace stable' (S.Var.relift k) v
-            ) data.stable;
-          data.stable <- stable';
-          let wpoint' = HM.create (HM.length data.wpoint) in
-          HM.iter (fun k v ->
-              HM.replace wpoint' (S.Var.relift k) v
-            ) data.wpoint;
-          data.wpoint <- wpoint';
-          let infl' = HM.create (HM.length data.infl) in
-          HM.iter (fun k v ->
-              HM.replace infl' (S.Var.relift k) (VS.map S.Var.relift v)
-            ) data.infl;
-          data.infl <- infl';
-          let side_infl' = HM.create (HM.length data.side_infl) in
-          HM.iter (fun k v ->
-              HM.replace side_infl' (S.Var.relift k) (VS.map S.Var.relift v)
-            ) data.side_infl;
-          data.side_infl <- side_infl';
-          let side_dep' = HM.create (HM.length data.side_dep) in
-          HM.iter (fun k v ->
-              HM.replace side_dep' (S.Var.relift k) (VS.map S.Var.relift v)
-            ) data.side_dep;
-          data.side_dep <- side_dep';
-          data.st <- List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st;
-          let var_messages' = HM.create (HM.length data.var_messages) in
-          HM.iter (fun k v ->
-              HM.add var_messages' (S.Var.relift k) v (* var_messages contains duplicate keys, so must add not replace! *)
-            ) data.var_messages;
-          data.var_messages <- var_messages';
-          let rho_write' = HM.create (HM.length data.rho_write) in
-          HM.iter (fun x w ->
-              let w' = HM.create (HM.length w) in
-              HM.iter (fun y d ->
-                  HM.add w' (S.Var.relift y) (S.Dom.relift d) (* w contains duplicate keys, so must add not replace! *)
-                ) w;
-              HM.replace rho_write' (S.Var.relift x) w';
-            ) data.rho_write;
-          data.rho_write <- rho_write';
-          let dep' = HM.create (HM.length data.dep) in
-          HM.iter (fun k v ->
-              HM.replace dep' (S.Var.relift k) (VS.map S.Var.relift v)
-            ) data.dep;
-          data.dep <- dep';
-        );
+        if loaded && (match S.increment with Some {server; _} -> server | None -> false) then
+          copy_marshal data
+        else if loaded && GobConfig.get_bool "ana.opt.hashcons" then
+          relift_marshal data;
+
         if not reuse_stable then (
           print_endline "Destabilizing everything!";
           data.stable <- HM.create 10;

From 8d8cd542930e04153b36b94129c604176aaa7260 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 3 Oct 2022 14:15:17 +0300
Subject: [PATCH 06/12] Add copy_marshal and relift_marshal to solver signature

---
 src/framework/analyses.ml    |  3 +++
 src/framework/constraints.ml |  2 ++
 src/solvers/selector.ml      | 10 ++++++++++
 3 files changed, 15 insertions(+)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 3a682ec525..9bfef55d97 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -536,6 +536,9 @@ module type GenericEqBoxIncrSolverBase =
   sig
     type marshal
 
+    val copy_marshal: marshal -> unit
+    val relift_marshal: marshal -> unit
+
     (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs],
         reached from starting values [xs].
         As a second component the solver returns data structures for incremental serialization. *)
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index b4b1d1a86c..8f7fd0cb71 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -794,6 +794,8 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve
     module Post = PostSolver.MakeList (PostSolver.ListArgFromStdArg (S) (VH) (Arg))
 
     type marshal = unit
+    let copy_marshal () = ()
+    let relift_marshal () = ()
 
     let solve box xs vs _ =
       let vh = Sol.solve box xs vs in
diff --git a/src/solvers/selector.ml b/src/solvers/selector.ml
index cc75ed96e8..ec6131e85c 100644
--- a/src/solvers/selector.ml
+++ b/src/solvers/selector.ml
@@ -22,6 +22,16 @@ module Make =
   struct
     type marshal = Obj.t (* cannot use Sol.marshal because cannot unpack first-class module in applicative functor *)
 
+    let copy_marshal (marshal: marshal) =
+      let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in
+      let module F = Sol (Arg) (S) (VH) in
+      F.copy_marshal (Obj.obj marshal)
+
+    let relift_marshal (marshal: marshal) =
+      let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in
+      let module F = Sol (Arg) (S) (VH) in
+      F.relift_marshal (Obj.obj marshal)
+
     let solve box xs vs (old_data: marshal option) =
       let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in
       let module F = Sol (Arg) (S) (VH) in

From 75e1dba1c518e38b16276b4f439309ba99704d65 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 3 Oct 2022 14:57:47 +0300
Subject: [PATCH 07/12] Move solver data relifting out of TD3

---
 src/framework/analyses.ml    |  3 +++
 src/framework/constraints.ml |  3 +++
 src/framework/control.ml     | 12 +++++++++++-
 src/solvers/td3.ml           |  4 ----
 4 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 9bfef55d97..23fd282c0e 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -577,6 +577,9 @@ module type GenericGlobSolver =
   sig
     type marshal
 
+    val copy_marshal: marshal -> unit
+    val relift_marshal: marshal -> unit
+
     (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs],
         reached from starting values [xs].
         As a second component the solver returns data structures for incremental serialization. *)
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 8f7fd0cb71..c05d84f81e 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -941,6 +941,9 @@ module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase)
 
       type marshal = Sol'.marshal
 
+      let copy_marshal = Sol'.copy_marshal
+      let relift_marshal = Sol'.relift_marshal
+
       let solve ls gs l old_data =
         let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls
                  @ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 6848d24649..f2318c00c1 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -460,10 +460,20 @@ struct
             r1 (* return the result of the first run for further options -- maybe better to exit early since compare_runs is its own mode. Only excluded verify below since it's on by default. *)
           | _ -> failwith "Currently only two runs can be compared!";
         ) else (
+          let solver_data =
+            match Inc.increment with
+            | Some {solver_data; server; _} ->
+              if server then
+                Slvr.copy_marshal solver_data
+              else if GobConfig.get_bool "ana.opt.hashcons" then
+                Slvr.relift_marshal solver_data;
+              Some solver_data
+            | None -> None
+          in
           if get_bool "dbg.verbose" then
             print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ ".");
           Goblintutil.should_warn := get_string "warn_at" = "early" || gobview;
-          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global startvars') (Option.map (fun {solver_data; _} -> solver_data) Inc.increment) in
+          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global startvars') solver_data in
           if GobConfig.get_bool "incremental.save" then
             Serialize.Cache.(update_data SolverData solver_data);
           if save_run_str <> "" then (
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index c48710a6a2..4ed8558b05 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -1093,10 +1093,6 @@ module WP =
          * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have
          *   the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values).
          *)
-        if loaded && (match S.increment with Some {server; _} -> server | None -> false) then
-          copy_marshal data
-        else if loaded && GobConfig.get_bool "ana.opt.hashcons" then
-          relift_marshal data;
 
         if not reuse_stable then (
           print_endline "Destabilizing everything!";

From e48b348ad26a3fa386cacfe7cb0d76ab1fb3d11a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 3 Oct 2022 15:06:20 +0300
Subject: [PATCH 08/12] Clean up incremental solve wrapping in TD3

---
 src/solvers/td3.ml | 74 +++++++++++++++++++++-------------------------
 1 file changed, 33 insertions(+), 41 deletions(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 4ed8558b05..1f0b89096d 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -83,6 +83,21 @@ module WP =
       data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *)
       data.dep <- HM.copy data.dep
 
+    (* This hack is for fixing hashconsing.
+     * If hashcons is enabled now, then it also was for the loaded values (otherwise it would crash). If it is off, we don't need to do anything.
+     * HashconsLifter uses BatHashcons.hashcons on Lattice operations like join, so we call join (with bot) to make sure that the old values will populate the empty hashcons table via side-effects and at the same time get new tags that are conform with its state.
+     * The tags are used for `equals` and `compare` to avoid structural comparisons. TODO could this be replaced by `==` (if values are shared by hashcons they should be physically equal)?
+     * We have to replace all tags since they are not derived from the value (like hash) but are incremented starting with 1, i.e. dependent on the order in which lattice operations for different values are called, which will very likely be different for an incremental run.
+     * If we didn't do this, during solve, a rhs might give the same value as from the old rho but it wouldn't be detected as equal since the tags would be different.
+     * In the worst case, every rhs would yield the same value, but we would destabilize for every var in rho until we replaced all values (just with new tags).
+     * The other problem is that we would likely use more memory since values from old rho would not be shared with the same values in the hashcons table. So we would keep old values in memory until they are replace in rho and eventually garbage collected.
+     *)
+    (* Another problem are the tags for the context part of a S.Var.t.
+     * This will cause problems when old and new vars interact or when new S.Dom values are used as context:
+     * - reachability is a problem since it marks vars reachable with a new tag, which will remove vars with the same context but old tag from rho.
+     * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have
+     *   the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values).
+     *)
     let relift_marshal (data: marshal): unit = (* TODO: should return new marshal? *)
       let rho' = HM.create (HM.length data.rho) in
       HM.iter (fun k v ->
@@ -152,7 +167,23 @@ module WP =
     module CurrentVarS = Constraints.CurrentVarEqConstrSys (S)
     module S = CurrentVarS.S
 
-    let solve box st vs data =
+    let solve box st vs marshal =
+      let reuse_stable = GobConfig.get_bool "incremental.stable" in
+      let reuse_wpoint = GobConfig.get_bool "incremental.wpoint" in
+      let data =
+        match marshal with
+        | Some data ->
+          if not reuse_stable then (
+            print_endline "Destabilizing everything!";
+            data.stable <- HM.create 10;
+            data.infl <- HM.create 10
+          );
+          if not reuse_wpoint then data.wpoint <- HM.create 10;
+          data
+        | None ->
+          create_empty_data ()
+      in
+
       let term  = GobConfig.get_bool "solvers.td3.term" in
       let side_widen = GobConfig.get_string "solvers.td3.side_widen" in
       let space = GobConfig.get_bool "solvers.td3.space" in
@@ -1068,46 +1099,7 @@ module WP =
       print_data data "Data after postsolve";
 
       verify_data data;
-      {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}
-
-    let solve box st vs (old_data: marshal option) =
-      let reuse_stable = GobConfig.get_bool "incremental.stable" in
-      let reuse_wpoint = GobConfig.get_bool "incremental.wpoint" in
-      if GobConfig.get_bool "incremental.load" then (
-        let loaded, data = match old_data with
-          | Some d -> true, d
-          | _ -> false, create_empty_data ()
-        in
-        (* This hack is for fixing hashconsing.
-         * If hashcons is enabled now, then it also was for the loaded values (otherwise it would crash). If it is off, we don't need to do anything.
-         * HashconsLifter uses BatHashcons.hashcons on Lattice operations like join, so we call join (with bot) to make sure that the old values will populate the empty hashcons table via side-effects and at the same time get new tags that are conform with its state.
-         * The tags are used for `equals` and `compare` to avoid structural comparisons. TODO could this be replaced by `==` (if values are shared by hashcons they should be physically equal)?
-         * We have to replace all tags since they are not derived from the value (like hash) but are incremented starting with 1, i.e. dependent on the order in which lattice operations for different values are called, which will very likely be different for an incremental run.
-         * If we didn't do this, during solve, a rhs might give the same value as from the old rho but it wouldn't be detected as equal since the tags would be different.
-         * In the worst case, every rhs would yield the same value, but we would destabilize for every var in rho until we replaced all values (just with new tags).
-         * The other problem is that we would likely use more memory since values from old rho would not be shared with the same values in the hashcons table. So we would keep old values in memory until they are replace in rho and eventually garbage collected.
-         *)
-        (* Another problem are the tags for the context part of a S.Var.t.
-         * This will cause problems when old and new vars interact or when new S.Dom values are used as context:
-         * - reachability is a problem since it marks vars reachable with a new tag, which will remove vars with the same context but old tag from rho.
-         * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have
-         *   the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values).
-         *)
-
-        if not reuse_stable then (
-          print_endline "Destabilizing everything!";
-          data.stable <- HM.create 10;
-          data.infl <- HM.create 10
-        );
-        if not reuse_wpoint then data.wpoint <- HM.create 10;
-        let result = solve box st vs data in
-        result.rho, result
-      )
-      else (
-        let data = create_empty_data () in
-        let result = solve box st vs data in
-        result.rho, result
-      )
+      (rho, {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep})
   end
 
 let _ =

From 16831e69405800f752c275ad2eae854645cceca1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 3 Oct 2022 16:03:35 +0300
Subject: [PATCH 09/12] Make TD3 solver data record immutable

---
 src/framework/analyses.ml |   8 +--
 src/framework/control.ml  |   7 +--
 src/solvers/selector.ml   |   4 +-
 src/solvers/td3.ml        | 108 +++++++++++++++++++-------------------
 4 files changed, 64 insertions(+), 63 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 23fd282c0e..58a64373df 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -536,8 +536,8 @@ module type GenericEqBoxIncrSolverBase =
   sig
     type marshal
 
-    val copy_marshal: marshal -> unit
-    val relift_marshal: marshal -> unit
+    val copy_marshal: marshal -> marshal
+    val relift_marshal: marshal -> marshal
 
     (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs],
         reached from starting values [xs].
@@ -577,8 +577,8 @@ module type GenericGlobSolver =
   sig
     type marshal
 
-    val copy_marshal: marshal -> unit
-    val relift_marshal: marshal -> unit
+    val copy_marshal: marshal -> marshal
+    val relift_marshal: marshal -> marshal
 
     (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs],
         reached from starting values [xs].
diff --git a/src/framework/control.ml b/src/framework/control.ml
index f2318c00c1..7d4166b88f 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -464,10 +464,11 @@ struct
             match Inc.increment with
             | Some {solver_data; server; _} ->
               if server then
-                Slvr.copy_marshal solver_data
+                Some (Slvr.copy_marshal solver_data) (* Copy, so that we can abort and reuse old data unmodified. *)
               else if GobConfig.get_bool "ana.opt.hashcons" then
-                Slvr.relift_marshal solver_data;
-              Some solver_data
+                Some (Slvr.relift_marshal solver_data)
+              else
+                Some solver_data
             | None -> None
           in
           if get_bool "dbg.verbose" then
diff --git a/src/solvers/selector.ml b/src/solvers/selector.ml
index ec6131e85c..082c11b410 100644
--- a/src/solvers/selector.ml
+++ b/src/solvers/selector.ml
@@ -25,12 +25,12 @@ module Make =
     let copy_marshal (marshal: marshal) =
       let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in
       let module F = Sol (Arg) (S) (VH) in
-      F.copy_marshal (Obj.obj marshal)
+      Obj.repr (F.copy_marshal (Obj.obj marshal))
 
     let relift_marshal (marshal: marshal) =
       let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in
       let module F = Sol (Arg) (S) (VH) in
-      F.relift_marshal (Obj.obj marshal)
+      Obj.repr (F.relift_marshal (Obj.obj marshal))
 
     let solve box xs vs (old_data: marshal option) =
       let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 1f0b89096d..8b04612390 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -25,17 +25,17 @@ module WP =
     module VS = Set.Make (S.Var)
 
     type solver_data = {
-      mutable st: (S.Var.t * S.Dom.t) list; (* needed to destabilize start functions if their start state changed because of some changed global initializer *)
-      mutable infl: VS.t HM.t;
-      mutable sides: VS.t HM.t;
-      mutable rho: S.Dom.t HM.t;
-      mutable wpoint: unit HM.t;
-      mutable stable: unit HM.t;
-      mutable side_dep: VS.t HM.t; (** Dependencies of side-effected variables. Knowing these allows restarting them and re-triggering all side effects. *)
-      mutable side_infl: VS.t HM.t; (** Influences to side-effected variables. Not normally in [infl], but used for restarting them. *)
-      mutable var_messages: Message.t HM.t; (** Messages from right-hand sides of variables. Used for incremental postsolving. *)
-      mutable rho_write: S.Dom.t HM.t HM.t; (** Side effects from variables to write-only variables with values. Used for fast incremental restarting of write-only variables. *)
-      mutable dep: VS.t HM.t; (** Dependencies of variables. Inverse of [infl]. Used for fast pre-reachable pruning in incremental postsolving. *)
+      st: (S.Var.t * S.Dom.t) list; (* needed to destabilize start functions if their start state changed because of some changed global initializer *)
+      infl: VS.t HM.t;
+      sides: VS.t HM.t;
+      rho: S.Dom.t HM.t;
+      wpoint: unit HM.t;
+      stable: unit HM.t;
+      side_dep: VS.t HM.t; (** Dependencies of side-effected variables. Knowing these allows restarting them and re-triggering all side effects. *)
+      side_infl: VS.t HM.t; (** Influences to side-effected variables. Not normally in [infl], but used for restarting them. *)
+      var_messages: Message.t HM.t; (** Messages from right-hand sides of variables. Used for incremental postsolving. *)
+      rho_write: S.Dom.t HM.t HM.t; (** Side effects from variables to write-only variables with values. Used for fast incremental restarting of write-only variables. *)
+      dep: VS.t HM.t; (** Dependencies of variables. Inverse of [infl]. Used for fast pre-reachable pruning in incremental postsolving. *)
     }
 
     type marshal = solver_data
@@ -71,17 +71,20 @@ module WP =
         (* vice versa doesn't currently hold, because stable is not pruned *)
       )
 
-    let copy_marshal (data: marshal): unit = (* TODO: should return new marshal? *)
-      data.rho <- HM.copy data.rho;
-      data.stable <- HM.copy data.stable;
-      data.wpoint <- HM.copy data.wpoint;
-      data.infl <- HM.copy data.infl;
-      data.side_infl <- HM.copy data.side_infl;
-      data.side_dep <- HM.copy data.side_dep;
-      (* data.st is immutable, no need to copy *)
-      data.var_messages <- HM.copy data.var_messages;
-      data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *)
-      data.dep <- HM.copy data.dep
+    let copy_marshal (data: marshal): marshal =
+      {
+        rho = HM.copy data.rho;
+        stable = HM.copy data.stable;
+        wpoint = HM.copy data.wpoint;
+        infl = HM.copy data.infl;
+        sides = HM.copy data.sides;
+        side_infl = HM.copy data.side_infl;
+        side_dep = HM.copy data.side_dep;
+        st = data.st; (* data.st is immutable *)
+        var_messages = HM.copy data.var_messages;
+        rho_write = HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *)
+        dep = HM.copy data.dep;
+      }
 
     (* This hack is for fixing hashconsing.
      * If hashcons is enabled now, then it also was for the loaded values (otherwise it would crash). If it is off, we don't need to do anything.
@@ -98,60 +101,56 @@ module WP =
      * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have
      *   the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values).
      *)
-    let relift_marshal (data: marshal): unit = (* TODO: should return new marshal? *)
-      let rho' = HM.create (HM.length data.rho) in
+    let relift_marshal (data: marshal): marshal =
+      let rho = HM.create (HM.length data.rho) in
       HM.iter (fun k v ->
           (* call hashcons on contexts and abstract values; results in new tags *)
           let k' = S.Var.relift k in
           let v' = S.Dom.relift v in
-          HM.replace rho' k' v';
+          HM.replace rho k' v';
         ) data.rho;
-      data.rho <- rho';
-      let stable' = HM.create (HM.length data.stable) in
+      let stable = HM.create (HM.length data.stable) in
       HM.iter (fun k v ->
-          HM.replace stable' (S.Var.relift k) v
+          HM.replace stable (S.Var.relift k) v
         ) data.stable;
-      data.stable <- stable';
-      let wpoint' = HM.create (HM.length data.wpoint) in
+      let wpoint = HM.create (HM.length data.wpoint) in
       HM.iter (fun k v ->
-          HM.replace wpoint' (S.Var.relift k) v
+          HM.replace wpoint (S.Var.relift k) v
         ) data.wpoint;
-      data.wpoint <- wpoint';
-      let infl' = HM.create (HM.length data.infl) in
+      let infl = HM.create (HM.length data.infl) in
       HM.iter (fun k v ->
-          HM.replace infl' (S.Var.relift k) (VS.map S.Var.relift v)
+          HM.replace infl (S.Var.relift k) (VS.map S.Var.relift v)
         ) data.infl;
-      data.infl <- infl';
-      let side_infl' = HM.create (HM.length data.side_infl) in
+      let sides = HM.create (HM.length data.sides) in
       HM.iter (fun k v ->
-          HM.replace side_infl' (S.Var.relift k) (VS.map S.Var.relift v)
+          HM.replace sides (S.Var.relift k) (VS.map S.Var.relift v)
+        ) data.sides;
+      let side_infl = HM.create (HM.length data.side_infl) in
+      HM.iter (fun k v ->
+          HM.replace side_infl (S.Var.relift k) (VS.map S.Var.relift v)
         ) data.side_infl;
-      data.side_infl <- side_infl';
-      let side_dep' = HM.create (HM.length data.side_dep) in
+      let side_dep = HM.create (HM.length data.side_dep) in
       HM.iter (fun k v ->
-          HM.replace side_dep' (S.Var.relift k) (VS.map S.Var.relift v)
+          HM.replace side_dep (S.Var.relift k) (VS.map S.Var.relift v)
         ) data.side_dep;
-      data.side_dep <- side_dep';
-      data.st <- List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st;
-      let var_messages' = HM.create (HM.length data.var_messages) in
+      let st = List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st in
+      let var_messages = HM.create (HM.length data.var_messages) in
       HM.iter (fun k v ->
-          HM.add var_messages' (S.Var.relift k) v (* var_messages contains duplicate keys, so must add not replace! *)
+          HM.add var_messages (S.Var.relift k) v (* var_messages contains duplicate keys, so must add not replace! *)
         ) data.var_messages;
-      data.var_messages <- var_messages';
-      let rho_write' = HM.create (HM.length data.rho_write) in
+      let rho_write = HM.create (HM.length data.rho_write) in
       HM.iter (fun x w ->
           let w' = HM.create (HM.length w) in
           HM.iter (fun y d ->
               HM.add w' (S.Var.relift y) (S.Dom.relift d) (* w contains duplicate keys, so must add not replace! *)
             ) w;
-          HM.replace rho_write' (S.Var.relift x) w';
+          HM.replace rho_write (S.Var.relift x) w';
         ) data.rho_write;
-      data.rho_write <- rho_write';
-      let dep' = HM.create (HM.length data.dep) in
+      let dep = HM.create (HM.length data.dep) in
       HM.iter (fun k v ->
-          HM.replace dep' (S.Var.relift k) (VS.map S.Var.relift v)
+          HM.replace dep (S.Var.relift k) (VS.map S.Var.relift v)
         ) data.dep;
-      data.dep <- dep'
+      {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}
 
     let exists_key f hm = HM.fold (fun k _ a -> a || f k) hm false
 
@@ -175,10 +174,11 @@ module WP =
         | Some data ->
           if not reuse_stable then (
             print_endline "Destabilizing everything!";
-            data.stable <- HM.create 10;
-            data.infl <- HM.create 10
+            HM.clear data.stable;
+            HM.clear data.infl
           );
-          if not reuse_wpoint then data.wpoint <- HM.create 10;
+          if not reuse_wpoint then
+            HM.clear data.wpoint;
           data
         | None ->
           create_empty_data ()

From f2b4c7f2c3c7fcb37bcc0cf4f5a73d337d4ccf23 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 16 Nov 2022 17:47:31 +0200
Subject: [PATCH 10/12] Adapt Gobview to incremental data changes

---
 gobview | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gobview b/gobview
index 19dbe2df33..9593d5f436 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 19dbe2df3321fdc21ccd918414800051801b35e7
+Subproject commit 9593d5f436a668978fa51ed85b04ff90fdb2a0bd

From ff5b73108964ce3aed4ffa065c388236ca968ef3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 16 Nov 2022 17:49:30 +0200
Subject: [PATCH 11/12] Fix incremental data in SolverTest

---
 unittest/solver/solverTest.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/unittest/solver/solverTest.ml b/unittest/solver/solverTest.ml
index 574b42f4cf..38316eeae9 100644
--- a/unittest/solver/solverTest.ml
+++ b/unittest/solver/solverTest.ml
@@ -29,7 +29,7 @@ module ConstrSys = struct
   module D = Int
   module G = IntR
 
-  let increment = Analyses.empty_increment_data ()
+  let increment = None
 
   (*
     1. x := g

From 632c4e0814c7ceb69d79b0c11e368384dc62679b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Nov 2022 22:15:27 +0200
Subject: [PATCH 12/12] Remove commented out GlobSolverFromEqSolver signature

---
 src/framework/constraints.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index c05d84f81e..63b94df82d 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -927,7 +927,6 @@ end
 
 (** Transforms a [GenericEqBoxIncrSolver] into a [GenericGlobSolver]. *)
 module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase)
-  (* : GenericGlobSolver *)
   = functor (S:GlobConstrSys) ->
     functor (LH:Hashtbl.S with type key=S.LVar.t) ->
     functor (GH:Hashtbl.S with type key=S.GVar.t) ->