From 8ffbdc65b7cf571d95396760205a1f4a8ac22f24 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 8 Mar 2022 16:33:08 +0200
Subject: [PATCH 01/26] Add incremental race fix test which needs global
 restart

---
 .../incremental/11-restart/12-mutex-simple.c  | 23 ++++++++++++++++++
 .../11-restart/12-mutex-simple.json           |  9 +++++++
 .../11-restart/12-mutex-simple.patch          | 24 +++++++++++++++++++
 3 files changed, 56 insertions(+)
 create mode 100644 tests/incremental/11-restart/12-mutex-simple.c
 create mode 100644 tests/incremental/11-restart/12-mutex-simple.json
 create mode 100644 tests/incremental/11-restart/12-mutex-simple.patch

diff --git a/tests/incremental/11-restart/12-mutex-simple.c b/tests/incremental/11-restart/12-mutex-simple.c
new file mode 100644
index 0000000000..82c1642a93
--- /dev/null
+++ b/tests/incremental/11-restart/12-mutex-simple.c
@@ -0,0 +1,23 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/incremental/11-restart/12-mutex-simple.json b/tests/incremental/11-restart/12-mutex-simple.json
new file mode 100644
index 0000000000..daff0678ce
--- /dev/null
+++ b/tests/incremental/11-restart/12-mutex-simple.json
@@ -0,0 +1,9 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/tests/incremental/11-restart/12-mutex-simple.patch b/tests/incremental/11-restart/12-mutex-simple.patch
new file mode 100644
index 0000000000..14913c581d
--- /dev/null
+++ b/tests/incremental/11-restart/12-mutex-simple.patch
@@ -0,0 +1,24 @@
+--- tests/incremental/11-restart/12-mutex-simple.c
++++ tests/incremental/11-restart/12-mutex-simple.c
+@@ -7,7 +7,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+ void *t_fun(void *arg) {
+   pthread_mutex_lock(&mutex1);
+-  myglobal=myglobal+1; // RACE!
++  myglobal=myglobal+1; // NORACE
+   pthread_mutex_unlock(&mutex1);
+   return NULL;
+ }
+@@ -15,9 +15,9 @@ void *t_fun(void *arg) {
+ int main(void) {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+-  pthread_mutex_lock(&mutex2);
+-  myglobal=myglobal+1; // RACE!
+-  pthread_mutex_unlock(&mutex2);
++  pthread_mutex_lock(&mutex1);
++  myglobal=myglobal+1; // NORACE
++  pthread_mutex_unlock(&mutex1);
+   pthread_join (id, NULL);
+   return 0;
+ }

From fa99c7bf7a91f9a0cef764e97de4e31503325416 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 8 Mar 2022 16:33:30 +0200
Subject: [PATCH 02/26] Disable dbg.compare_runs.glob in test-incremental.sh

---
 scripts/test-incremental.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/test-incremental.sh b/scripts/test-incremental.sh
index 29198669ac..fa95f25f42 100755
--- a/scripts/test-incremental.sh
+++ b/scripts/test-incremental.sh
@@ -19,7 +19,7 @@ patch -p0 -b <$patch
 
 ./goblint --conf $conf $args --enable incremental.load --set save_run $base/$test-incrementalrun $source &> $base/$test.after.incr.log
 ./goblint --conf $conf $args --enable incremental.only-rename --set save_run $base/$test-originalrun $source &> $base/$test.after.scratch.log
-./goblint --conf $conf --enable solverdiffs --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source
+./goblint --conf $conf --disable dbg.compare_runs.glob --enable solverdiffs --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source
 
 patch -p0 -b -R <$patch
 rm -r $base/$test-originalrun $base/$test-incrementalrun

From 4ac2da7580d2fc94076a9b757866c16943e6551d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 9 Mar 2022 18:48:13 +0200
Subject: [PATCH 03/26] Remove unused Basetype.Variables functions

---
 src/cdomains/basetype.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/cdomains/basetype.ml b/src/cdomains/basetype.ml
index 4db41612cf..bfe3a592d2 100644
--- a/src/cdomains/basetype.ml
+++ b/src/cdomains/basetype.ml
@@ -40,8 +40,6 @@ struct
     | _ -> Local
   let name () = "variables"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
-  let var_id _ = "globals"
-  let node _ = MyCFG.Function Cil.dummyFunDec
 
   let arbitrary () = MyCheck.Arbitrary.varinfo
 end

From e122956b0404f541060d97d5e043c6403bd64d4e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 12:33:43 +0200
Subject: [PATCH 04/26] Add write-only sides rho to optimize access restarting

---
 src/analyses/accessAnalysis.ml |  1 +
 src/framework/analyses.ml      |  2 +-
 src/framework/constraints.ml   |  2 +-
 src/solvers/postSolver.ml      | 43 ++++++++++++++++++++--------------
 src/solvers/td3.ml             | 42 ++++++++++++++++++++++++++++-----
 5 files changed, 64 insertions(+), 26 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index a646d9d3a1..88b3dfec18 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -25,6 +25,7 @@ struct
   module V =
   struct
     include Printable.Either (V0) (CilType.Varinfo)
+    let name () = "access" (* HACK: incremental accesses rely on this! *)
     let access x = `Left x
     let vars x = `Right x
   end
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index b71371e051..5183113cf0 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -71,7 +71,7 @@ struct
   let contexts x = `Right x
 
   (* from Basetype.Variables *)
-  let var_id _ = "globals"
+  let var_id = show (* HACK: incremental accesses rely on this! *)
   let node _ = MyCFG.Function Cil.dummyFunDec
   let pretty_trace = pretty
 end
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 204ad649ad..14543ec4b6 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -808,7 +808,7 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve
 
     let solve box xs vs =
       let vh = Sol.solve box xs vs in
-      Post.post xs vs vh;
+      Post.post xs vs vh (VH.create 0);
       (vh, ())
   end
 
diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
index 4b6e016f03..9c7b0810f6 100644
--- a/src/solvers/postSolver.ml
+++ b/src/solvers/postSolver.ml
@@ -9,8 +9,8 @@ sig
   module VH: Hashtbl.S with type key = S.v
 
   val init: unit -> unit
-  val one_side: vh:S.Dom.t VH.t -> x:S.v -> y:S.v -> d:S.Dom.t -> unit
-  val one_constraint: vh:S.Dom.t VH.t -> x:S.v -> rhs:S.Dom.t -> unit
+  val one_side: vh:S.Dom.t VH.t -> vhw:S.Dom.t VH.t VH.t -> x:S.v -> y:S.v -> d:S.Dom.t -> unit
+  val one_constraint: vh:S.Dom.t VH.t -> vhw:S.Dom.t VH.t VH.t -> x:S.v -> rhs:S.Dom.t -> unit
   val finalize: vh:S.Dom.t VH.t -> reachable:unit VH.t -> unit
 end
 
@@ -26,8 +26,8 @@ module Unit: F =
     module S = S
     module VH = VH
     let init () = ()
-    let one_side ~vh ~x ~y ~d = ()
-    let one_constraint ~vh ~x ~rhs = ()
+    let one_side ~vh ~vhw ~x ~y ~d = ()
+    let one_constraint ~vh ~vhw ~x ~rhs = ()
     let finalize ~vh ~reachable = ()
   end
 
@@ -40,12 +40,12 @@ struct
   let init () =
     PS1.init ();
     PS2.init ()
-  let one_side ~vh ~x ~y ~d =
-    PS1.one_side ~vh ~x ~y ~d;
-    PS2.one_side ~vh ~x ~y ~d
-  let one_constraint ~vh ~x ~rhs =
-    PS1.one_constraint ~vh ~x ~rhs;
-    PS2.one_constraint ~vh ~x ~rhs
+  let one_side ~vh ~vhw ~x ~y ~d =
+    PS1.one_side ~vh ~vhw ~x ~y ~d;
+    PS2.one_side ~vh ~vhw ~x ~y ~d
+  let one_constraint ~vh ~vhw ~x ~rhs =
+    PS1.one_constraint ~vh ~vhw ~x ~rhs;
+    PS2.one_constraint ~vh ~vhw ~x ~rhs
   let finalize ~vh ~reachable =
     PS1.finalize ~vh ~reachable;
     PS2.finalize ~vh ~reachable
@@ -83,14 +83,21 @@ module Verify: F =
       Goblintutil.verified := Some false;
       ignore (Pretty.printf "Fixpoint not reached at %a\nOrigin: %a\n @[Solver computed:\n%a\nSide-effect:\n%a\nDifference: %a\n@]" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs))
 
-    let one_side ~vh ~x ~y ~d =
+    let one_side ~vh ~vhw ~x ~y ~d =
+      (* HACK: incremental accesses insanity! *)
+      (* ignore (Pretty.printf "one_side %s: %a\n" (S.Var.var_id y) S.Dom.pretty d); *)
+      let is_acc = String.starts_with (S.Var.var_id y) "access:" in
       let y_lhs = try VH.find vh y with Not_found -> S.Dom.bot () in
-      if not (S.Dom.leq d y_lhs) then
+      if is_acc then (
+        VH.replace vh y (S.Dom.join y_lhs d);
+        VH.modify_def (VH.create 1) x (fun w -> VH.add w y d; w) vhw (* inner add intentional *)
+      )
+      else if not (S.Dom.leq d y_lhs) then
         complain_side x y ~lhs:y_lhs ~rhs:d
       else
         VH.replace vh y (S.Dom.join y_lhs d) (* HACK: allow warnings/accesses to be added *)
 
-    let one_constraint ~vh ~x ~rhs =
+    let one_constraint ~vh ~vhw ~x ~rhs =
       let lhs = try VH.find vh x with Not_found -> S.Dom.bot () in
       if not (S.Dom.leq rhs lhs) then
         complain_constraint x ~lhs ~rhs
@@ -173,7 +180,7 @@ struct
   module S = PS.S
   module VH = PS.VH
 
-  let post xs vs vh =
+  let post xs vs vh vhw =
     if get_bool "dbg.verbose" then
       print_endline "Postsolving\n";
 
@@ -200,12 +207,12 @@ struct
         try VH.find vh y with Not_found -> S.Dom.bot ()
       in
       let set y d =
-        PS.one_side ~vh ~x ~y ~d;
+        PS.one_side ~vh ~vhw ~x ~y ~d;
         (* check before recursing *)
         one_var y
       in
       let rhs = f get set in
-      PS.one_constraint ~vh ~x ~rhs
+      PS.one_constraint ~vh ~vhw ~x ~rhs
     in
     List.iter one_var vs;
 
@@ -252,7 +259,7 @@ struct
       in
       Some (List.reduce compose postsolvers)
 
-  let post xs vs vh =
+  let post xs vs vh vhw =
     match postsolver_opt with
     | None -> ()
     | Some (module PS) ->
@@ -263,7 +270,7 @@ struct
       end
       in
       let module M = MakeIncr (IncrPS) in
-      M.post xs vs vh
+      M.post xs vs vh vhw
 end
 
 (** Make complete (non-incremental) postsolving function from list of postsolvers.
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index f65891539f..adc5016fc8 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -34,6 +34,7 @@ module WP =
       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;
+      mutable rho_write: S.Dom.t HM.t HM.t;
     }
 
     type marshal = solver_data
@@ -48,6 +49,7 @@ module WP =
       side_dep = HM.create 10;
       side_infl = HM.create 10;
       var_messages = HM.create 10;
+      rho_write = HM.create 10;
     }
 
     let print_data data str =
@@ -130,6 +132,7 @@ module WP =
       let superstable = HM.copy stable in
 
       let var_messages = data.var_messages in
+      let rho_write = data.rho_write in
 
       let abort = GobConfig.get_bool "solvers.td3.abort" in
       let destab_infl = HM.create 10 in
@@ -955,16 +958,27 @@ module WP =
       struct
         include PostSolver.Unit (S) (HM)
 
-        let one_side ~vh ~x ~y ~d =
+        let one_side ~vh ~vhw ~x ~y ~d =
           HM.replace side_dep y (VS.add x (try HM.find side_dep y with Not_found -> VS.empty));
           HM.replace side_infl x (VS.add y (try HM.find side_infl x with Not_found -> VS.empty));
       end
       in
 
-      if incr_verify then
-        HM.filteri_inplace (fun x _ -> HM.mem superstable x) var_messages
-      else
+      (* restart write-only *)
+      HM.iter (fun x w ->
+          HM.iter (fun y d ->
+              HM.replace rho y (S.Dom.bot ());
+            ) w
+        ) rho_write;
+
+      if incr_verify then (
+        HM.filteri_inplace (fun x _ -> HM.mem superstable x) var_messages;
+        HM.filteri_inplace (fun x _ -> HM.mem superstable x) rho_write
+      )
+      else (
         HM.clear var_messages;
+        HM.clear rho_write
+      );
 
       let module IncrWarn: PostSolver.S with module S = S and module VH = HM =
       struct
@@ -978,6 +992,13 @@ module WP =
             HM.iter (fun _ m ->
                 Messages.add m
               ) var_messages;
+            (* retrigger *)
+            HM.iter (fun x w ->
+                HM.iter (fun y d ->
+                    let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in
+                    HM.replace rho y (S.Dom.join old_d d)
+                  ) w
+              ) rho_write
           );
 
           (* hook to collect new messages *)
@@ -1009,11 +1030,11 @@ module WP =
 
       let module Post = PostSolver.MakeIncrList (MakeIncrListArg) in
 
-      Post.post st vs rho;
+      Post.post st vs rho rho_write;
 
       print_data data "Data after postsolve";
 
-      {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages}
+      {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write}
 
     let solve box st vs =
       let reuse_stable = GobConfig.get_bool "incremental.stable" in
@@ -1078,6 +1099,15 @@ module WP =
               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.replace w' (S.Var.relift y) (S.Dom.relift d)
+                ) w;
+              HM.replace rho_write' (S.Var.relift x) w';
+            ) data.rho_write;
+          data.rho_write <- rho_write';
         );
         if not reuse_stable then (
           print_endline "Destabilizing everything!";

From 490c4d62c4b779614ef8cd1b98e0b2f498c3d68e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 12:52:39 +0200
Subject: [PATCH 05/26] Add is_write_only function to solver unknowns

---
 src/analyses/accessAnalysis.ml            |  3 +-
 src/analyses/apron/apronAnalysis.apron.ml |  6 +-
 src/analyses/arinc.ml                     |  6 +-
 src/analyses/base.ml                      |  1 +
 src/analyses/extract_arinc.ml             |  6 +-
 src/analyses/mCP.ml                       |  4 +-
 src/analyses/mCPRegistry.ml               | 89 ++++++++++++++++++++++-
 src/analyses/mutexAnalysis.ml             |  6 +-
 src/analyses/region.ml                    |  6 +-
 src/analyses/threadAnalysis.ml            |  6 +-
 src/analyses/threadJoins.ml               |  6 +-
 src/domains/printable.ml                  |  6 ++
 src/framework/analyses.ml                 | 17 ++++-
 src/framework/constraints.ml              |  7 ++
 src/solvers/postSolver.ml                 |  6 +-
 15 files changed, 154 insertions(+), 21 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 88b3dfec18..68a0fe5053 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -25,9 +25,10 @@ struct
   module V =
   struct
     include Printable.Either (V0) (CilType.Varinfo)
-    let name () = "access" (* HACK: incremental accesses rely on this! *)
+    let name () = "access"
     let access x = `Left x
     let vars x = `Right x
+    let is_write_only _ = true
   end
 
   module V0Set = SetDomain.Make (V0)
diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index 1ca0d81e61..69a20833f6 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -16,7 +16,11 @@ struct
   module D = ApronComponents (AD) (Priv.D)
   module G = Priv.G
   module C = D
-  module V = Priv.V
+  module V =
+  struct
+    include Priv.V
+    let is_write_only _ = false
+  end
 
   open AD
   open (ApronDomain: (sig module V: (module type of ApronDomain.V) end)) (* open only V from ApronDomain (to shadow V of Spec), but don't open D (to not shadow D here) *)
diff --git a/src/analyses/arinc.ml b/src/analyses/arinc.ml
index fe2679cc50..b2b70fdacb 100644
--- a/src/analyses/arinc.ml
+++ b/src/analyses/arinc.ml
@@ -91,7 +91,11 @@ struct
   module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (ArincDomain.D)) (* set of created tasks to spawn when going multithreaded *)
   module G = Tasks
   module C = D
-  module V = Printable.UnitConf (struct let name = "tasks" end)
+  module V =
+  struct
+    include Printable.UnitConf (struct let name = "tasks" end)
+    let is_write_only _ = false
+  end
 
   let context fd d = { d with pred = Pred.bot (); ctx = Ctx.bot () }
 
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index c351083e54..7a3d3bba8b 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -47,6 +47,7 @@ struct
     include Printable.Either (Priv.V) (ThreadIdDomain.Thread)
     let priv x = `Left x
     let thread x = `Right x
+    let is_write_only _ = false
   end
 
   module G =
diff --git a/src/analyses/extract_arinc.ml b/src/analyses/extract_arinc.ml
index 03a231bcc4..1faeee50cc 100644
--- a/src/analyses/extract_arinc.ml
+++ b/src/analyses/extract_arinc.ml
@@ -33,7 +33,11 @@ struct
   module C = D
   module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (D)) (* set of created tasks to spawn when going multithreaded *)
   module G = Tasks
-  module V = Printable.UnitConf (struct let name = "tasks" end)
+  module V =
+  struct
+    include Printable.UnitConf (struct let name = "tasks" end)
+    let is_write_only _ = false
+  end
 
   type pname = string (* process name *)
   type fname = string (* function name *)
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 8b0aa92ae9..a136f278e6 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -13,12 +13,12 @@ module MCP2 : Analyses.Spec
   with module D = DomListLattice (LocalDomainListSpec)
    and module G = DomVariantLattice (GlobalDomainListSpec)
    and module C = DomListPrintable (ContextListSpec)
-   and module V = DomVariantPrintable (VarListSpec) =
+   and module V = DomVariantPrintableW (VarListSpec) =
 struct
   module D = DomListLattice (LocalDomainListSpec)
   module G = DomVariantLattice (GlobalDomainListSpec)
   module C = DomListPrintable (ContextListSpec)
-  module V = DomVariantPrintable (VarListSpec)
+  module V = DomVariantPrintableW (VarListSpec)
 
   open List open Obj
   let v_of n v = (n, repr v)
diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index 57e03dff5b..0e9d49b061 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -7,7 +7,7 @@ type spec_modules = { name : string
                     ; dom  : (module Lattice.S)
                     ; glob : (module Lattice.S)
                     ; cont : (module Printable.S)
-                    ; var  : (module Printable.S)
+                    ; var  : (module Printable.W)
                     ; acc  : (module MCPA) }
 
 let activated  : (int * spec_modules) list ref = ref []
@@ -25,7 +25,7 @@ let register_analysis =
             ; dom  = (module S.D : Lattice.S)
             ; glob = (module S.G : Lattice.S)
             ; cont = (module S.C : Printable.S)
-            ; var  = (module S.V : Printable.S)
+            ; var  = (module S.V : Printable.W)
             ; acc  = (module S.A : MCPA)
             }
     in
@@ -45,6 +45,12 @@ sig
   val domain_list : unit -> (int * (module Printable.S)) list
 end
 
+module type DomainListPrintableWSpec =
+sig
+  val assoc_dom : int -> (module Printable.W)
+  val domain_list : unit -> (int * (module Printable.W)) list
+end
+
 module type DomainListMCPASpec =
 sig
   val assoc_dom : int -> (module MCPA)
@@ -239,6 +245,83 @@ struct
     QCheck.oneof arbs
 end
 
+(* TODO: deduplicate *)
+module DomVariantPrintableW (DLSpec : DomainListPrintableWSpec)
+  : Printable.W with type t = int * unknown
+=
+struct
+  include Printable.Std (* for default invariant, tag, ... *)
+
+  open DLSpec
+  open List
+  open Obj
+
+  type t = int * unknown
+
+  let unop_map f ((n, d):t) =
+    f n (assoc_dom n) d
+
+  let pretty () = unop_map (fun n (module S: Printable.W) x ->
+      Pretty.dprintf "%s:%a" (S.name ()) S.pretty (obj x)
+    )
+
+  let show = unop_map (fun n (module S: Printable.W) x ->
+      let analysis_name = find_spec_name n in
+      analysis_name ^ ":" ^ S.show (obj x)
+    )
+
+  let is_write_only = unop_map (fun n (module S: Printable.W) x ->
+      S.is_write_only (obj x)
+    )
+
+  let to_yojson x =
+    `Assoc [
+      unop_map (fun n (module S: Printable.W) x ->
+          let name = find_spec_name n in
+          (name, S.to_yojson (obj x))
+        ) x
+    ]
+
+  let equal (n1, x1) (n2, x2) =
+    n1 = n2 && (
+      let module S = (val assoc_dom n1) in
+      S.equal (obj x1) (obj x2)
+    )
+
+  let compare (n1, x1) (n2, x2) =
+    let r = Stdlib.compare n1 n2 in
+    if r <> 0 then
+      r
+    else
+      let module S = (val assoc_dom n1) in
+      S.compare (obj x1) (obj x2)
+
+  let hash = unop_map (fun n (module S: Printable.W) x ->
+      Hashtbl.hash (n, S.hash (obj x))
+    )
+
+  let name () =
+    let domain_name (n, (module S: Printable.W)) =
+      let analysis_name = find_spec_name n in
+      analysis_name ^ ":" ^ S.name ()
+    in
+    IO.to_string (List.print ~first:"" ~last:"" ~sep:" | " String.print) (map domain_name @@ domain_list ())
+
+  let printXml f = unop_map (fun n (module S: Printable.W) x ->
+      BatPrintf.fprintf f "<analysis name=\"%s\">\n" (find_spec_name n);
+      S.printXml f (obj x);
+      BatPrintf.fprintf f "</analysis>\n"
+    )
+
+  let invariant c = unop_map (fun n (module S: Printable.W) x ->
+      S.invariant c (obj x)
+    )
+
+  let arbitrary () =
+    let arbs = map (fun (n, (module S: Printable.W)) -> QCheck.map ~rev:(fun (_, o) -> obj o) (fun x -> (n, repr x)) @@ S.arbitrary ()) @@ domain_list () in
+    QCheck.oneof arbs
+end
+
 module DomListLattice (DLSpec : DomainListLatticeSpec)
   : Lattice.S with type t = (int * unknown) list
 =
@@ -339,7 +422,7 @@ struct
   let domain_list () = List.map (fun (n,p) -> n, p.cont) !activated_ctx_sens
 end
 
-module VarListSpec : DomainListPrintableSpec =
+module VarListSpec : DomainListPrintableWSpec =
 struct
   let assoc_dom n = (find_spec n).var
   let domain_list () = List.map (fun (n,p) -> n, p.var) !activated
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 806d7be280..3451f43b46 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -34,7 +34,11 @@ struct
 
   (** We do not add global state, so just lift from [BS]*)
   module G = P.G
-  module V = VarinfoV
+  module V =
+  struct
+    include VarinfoV
+    let is_write_only _ = false
+  end
 
   let should_join x y = D.equal x y
 
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 9c326117de..a2c5a4d963 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -14,7 +14,11 @@ struct
   module D = RegionDomain.RegionDom
   module G = RegPart
   module C = D
-  module V = Printable.UnitConf (struct let name = "partitions" end)
+  module V =
+  struct
+    include Printable.UnitConf (struct let name = "partitions" end)
+    let is_write_only _ = false
+  end
 
   let regions exp part st : Lval.CilLval.t list =
     match st with
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 184395f50a..4951d1cd9b 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -14,7 +14,11 @@ struct
   module D = ConcDomain.CreatedThreadSet
   module C = D
   module G = ConcDomain.ThreadCreation
-  module V = T
+  module V =
+  struct
+    include T
+    let is_write_only _ = false
+  end
 
   let should_join = D.equal
 
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index ad7ed42379..c2e680571b 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -14,7 +14,11 @@ struct
   module D = MustTIDs
   module C = D
   module G = MustTIDs
-  module V = TID
+  module V =
+  struct
+    include TID
+    let is_write_only _ = false
+  end
 
   (* transfer functions *)
   let return ctx (exp:exp option) (f:fundec) : D.t =
diff --git a/src/domains/printable.ml b/src/domains/printable.ml
index d95d0e78c1..291ecf1f2b 100644
--- a/src/domains/printable.ml
+++ b/src/domains/printable.ml
@@ -32,6 +32,12 @@ sig
   val relift: t -> t
 end
 
+module type W =
+sig
+  include S
+  val is_write_only: t -> bool (* TODO: move elsewhere *)
+end
+
 module Empty: S =
 struct
   type t = | [@@deriving eq, ord, hash]
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 5183113cf0..fb70515883 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -21,6 +21,7 @@ sig
   val printXml : 'a BatInnerIO.output -> t -> unit
   val var_id   : t -> string
   val node      : t -> MyCFG.node
+  val is_write_only: t -> bool
   val relift    : t -> t (* needed only for incremental+hashcons to re-hashcons contexts after loading *)
 end
 
@@ -62,18 +63,22 @@ struct
 
   let var_id (n,_) = Var.var_id n
   let node (n,_) = n
+  let is_write_only _ = false
 end
 
-module GVarF (V: Printable.S) =
+module GVarF (V: Printable.W) =
 struct
   include Printable.Either (V) (CilType.Fundec)
   let spec x = `Left x
   let contexts x = `Right x
 
   (* from Basetype.Variables *)
-  let var_id = show (* HACK: incremental accesses rely on this! *)
+  let var_id = show
   let node _ = MyCFG.Function Cil.dummyFunDec
   let pretty_trace = pretty
+  let is_write_only = function
+    | `Left x -> V.is_write_only x
+    | `Right _ -> true
 end
 
 module GVarG (G: Lattice.S) (C: Printable.S) =
@@ -366,7 +371,7 @@ sig
   module D : Lattice.S
   module G : Lattice.S
   module C : Printable.S
-  module V: Printable.S (** Global constraint variables. *)
+  module V: Printable.W (** Global constraint variables. *)
 
   val name : unit -> string
 
@@ -557,7 +562,11 @@ struct
 end
 
 module VarinfoV = CilType.Varinfo (* TODO: or Basetype.Variables? *)
-module EmptyV = Printable.Empty
+module EmptyV =
+struct
+  include Printable.Empty
+  let is_write_only _ = false
+end
 
 module UnitA =
 struct
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 14543ec4b6..5c6c1b1f21 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -839,6 +839,10 @@ struct
   let node = function
     | `L a -> LV.node a
     | `G a -> GV.node a
+
+  let is_write_only = function
+    | `L a -> LV.is_write_only a
+    | `G a -> GV.is_write_only a
 end
 
 (** Translate a [GlobConstrSys] into a [EqConstrSys] *)
@@ -1107,6 +1111,9 @@ struct
     include Printable.Either (S.V) (Node)
     let s x = `Left x
     let node x = `Right x
+    let is_write_only = function
+      | `Left x -> S.V.is_write_only x
+      | `Right _ -> true
   end
 
   module EM =
diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
index 9c7b0810f6..bbedb604a9 100644
--- a/src/solvers/postSolver.ml
+++ b/src/solvers/postSolver.ml
@@ -84,11 +84,9 @@ module Verify: F =
       ignore (Pretty.printf "Fixpoint not reached at %a\nOrigin: %a\n @[Solver computed:\n%a\nSide-effect:\n%a\nDifference: %a\n@]" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs))
 
     let one_side ~vh ~vhw ~x ~y ~d =
-      (* HACK: incremental accesses insanity! *)
-      (* ignore (Pretty.printf "one_side %s: %a\n" (S.Var.var_id y) S.Dom.pretty d); *)
-      let is_acc = String.starts_with (S.Var.var_id y) "access:" in
       let y_lhs = try VH.find vh y with Not_found -> S.Dom.bot () in
-      if is_acc then (
+      if S.Var.is_write_only y then (
+        (* HACK: incremental accesses etc insanity! *)
         VH.replace vh y (S.Dom.join y_lhs d);
         VH.modify_def (VH.create 1) x (fun w -> VH.add w y d; w) vhw (* inner add intentional *)
       )

From 7ffb6c81f5b744c05002414566c970cabca54723 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 13:01:15 +0200
Subject: [PATCH 06/26] Remove postsolving write-only validation hacks

---
 src/analyses/accessAnalysis.ml | 20 ++++----------------
 src/framework/analyses.ml      |  1 -
 src/framework/constraints.ml   | 15 +++------------
 src/solvers/postSolver.ml      |  2 --
 4 files changed, 7 insertions(+), 31 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 68a0fe5053..e8d4b720e3 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -46,8 +46,6 @@ struct
       | _ -> failwith "Access.vars"
     let create_access access = `Lifted1 access
     let create_vars vars = `Lifted2 vars
-
-    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
 
   let safe       = ref 0
@@ -62,24 +60,14 @@ struct
   let side_vars ctx lv_opt ty =
     match lv_opt with
     | Some (v, _) ->
-      let d =
-        if !GU.should_warn then
-          G.create_vars (V0Set.singleton (lv_opt, ty))
-        else
-          G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
-      in
-      ctx.sideg (V.vars v) d;
+      if !GU.should_warn then
+        ctx.sideg (V.vars v) (G.create_vars (V0Set.singleton (lv_opt, ty)))
     | None ->
       ()
 
   let side_access ctx ty lv_opt (conf, w, loc, e, a) =
-    let d =
-      if !GU.should_warn then
-        G.create_access (Access.AS.singleton (conf, w, loc, e, a))
-      else
-        G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
-    in
-    ctx.sideg (V.access (lv_opt, ty)) d;
+    if !GU.should_warn then
+      ctx.sideg (V.access (lv_opt, ty)) (G.create_access (Access.AS.singleton (conf, w, loc, e, a)));
     side_vars ctx lv_opt ty
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (w:bool) (reach:bool) (conf:int) (e:exp) =
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index fb70515883..9cb6235584 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -91,7 +91,6 @@ struct
         let printXml f c = BatPrintf.fprintf f "<value>%a</value>" printXml c (* wrap in <value> for HTML printing *)
       end
       )
-    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
 
   include Lattice.Lift2 (G) (CSet) (Printable.DefaultNames)
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 5c6c1b1f21..d6f6a0d37b 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -484,13 +484,8 @@ struct
     | _ -> S.sync ctx `Normal
 
   let side_context sideg f c =
-    let d =
-      if !GU.postsolving then
-        G.create_contexts (G.CSet.singleton c)
-      else
-        G.create_contexts (G.CSet.empty ()) (* HACK: just to pass validation with MCP DomVariantLattice *)
-    in
-    sideg (GVar.contexts f) d
+    if !GU.postsolving then
+      sideg (GVar.contexts f) (G.create_contexts (G.CSet.singleton c))
 
   let common_ctx var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) ctx * D.t list ref * (lval option * varinfo * exp list * D.t) list ref =
     let r = ref [] in
@@ -1116,11 +1111,7 @@ struct
       | `Right _ -> true
   end
 
-  module EM =
-  struct
-    include MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools)
-    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
-  end
+  module EM = MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools)
 
   module G =
   struct
diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
index bbedb604a9..db6f074174 100644
--- a/src/solvers/postSolver.ml
+++ b/src/solvers/postSolver.ml
@@ -92,8 +92,6 @@ module Verify: F =
       )
       else if not (S.Dom.leq d y_lhs) then
         complain_side x y ~lhs:y_lhs ~rhs:d
-      else
-        VH.replace vh y (S.Dom.join y_lhs d) (* HACK: allow warnings/accesses to be added *)
 
     let one_constraint ~vh ~vhw ~x ~rhs =
       let lhs = try VH.find vh x with Not_found -> S.Dom.bot () in

From 4e4bd9e556ef36be8bbf344238c2b50115412b72 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 14:24:51 +0200
Subject: [PATCH 07/26] Rename Printable.W -> Analyses.SpecSysVar

---
 src/analyses/mCPRegistry.ml | 28 ++++++++++++++--------------
 src/domains/printable.ml    |  6 ------
 src/framework/analyses.ml   | 18 +++++++++++++++---
 3 files changed, 29 insertions(+), 23 deletions(-)

diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index 0e9d49b061..bda4b1059f 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -7,7 +7,7 @@ type spec_modules = { name : string
                     ; dom  : (module Lattice.S)
                     ; glob : (module Lattice.S)
                     ; cont : (module Printable.S)
-                    ; var  : (module Printable.W)
+                    ; var  : (module SpecSysVar)
                     ; acc  : (module MCPA) }
 
 let activated  : (int * spec_modules) list ref = ref []
@@ -25,7 +25,7 @@ let register_analysis =
             ; dom  = (module S.D : Lattice.S)
             ; glob = (module S.G : Lattice.S)
             ; cont = (module S.C : Printable.S)
-            ; var  = (module S.V : Printable.W)
+            ; var  = (module S.V : SpecSysVar)
             ; acc  = (module S.A : MCPA)
             }
     in
@@ -47,8 +47,8 @@ end
 
 module type DomainListPrintableWSpec =
 sig
-  val assoc_dom : int -> (module Printable.W)
-  val domain_list : unit -> (int * (module Printable.W)) list
+  val assoc_dom : int -> (module SpecSysVar)
+  val domain_list : unit -> (int * (module SpecSysVar)) list
 end
 
 module type DomainListMCPASpec =
@@ -247,7 +247,7 @@ end
 
 (* TODO: deduplicate *)
 module DomVariantPrintableW (DLSpec : DomainListPrintableWSpec)
-  : Printable.W with type t = int * unknown
+  : SpecSysVar with type t = int * unknown
 =
 struct
   include Printable.Std (* for default invariant, tag, ... *)
@@ -261,22 +261,22 @@ struct
   let unop_map f ((n, d):t) =
     f n (assoc_dom n) d
 
-  let pretty () = unop_map (fun n (module S: Printable.W) x ->
+  let pretty () = unop_map (fun n (module S: SpecSysVar) x ->
       Pretty.dprintf "%s:%a" (S.name ()) S.pretty (obj x)
     )
 
-  let show = unop_map (fun n (module S: Printable.W) x ->
+  let show = unop_map (fun n (module S: SpecSysVar) x ->
       let analysis_name = find_spec_name n in
       analysis_name ^ ":" ^ S.show (obj x)
     )
 
-  let is_write_only = unop_map (fun n (module S: Printable.W) x ->
+  let is_write_only = unop_map (fun n (module S: SpecSysVar) x ->
       S.is_write_only (obj x)
     )
 
   let to_yojson x =
     `Assoc [
-      unop_map (fun n (module S: Printable.W) x ->
+      unop_map (fun n (module S: SpecSysVar) x ->
           let name = find_spec_name n in
           (name, S.to_yojson (obj x))
         ) x
@@ -296,29 +296,29 @@ struct
       let module S = (val assoc_dom n1) in
       S.compare (obj x1) (obj x2)
 
-  let hash = unop_map (fun n (module S: Printable.W) x ->
+  let hash = unop_map (fun n (module S: SpecSysVar) x ->
       Hashtbl.hash (n, S.hash (obj x))
     )
 
   let name () =
-    let domain_name (n, (module S: Printable.W)) =
+    let domain_name (n, (module S: SpecSysVar)) =
       let analysis_name = find_spec_name n in
       analysis_name ^ ":" ^ S.name ()
     in
     IO.to_string (List.print ~first:"" ~last:"" ~sep:" | " String.print) (map domain_name @@ domain_list ())
 
-  let printXml f = unop_map (fun n (module S: Printable.W) x ->
+  let printXml f = unop_map (fun n (module S: SpecSysVar) x ->
       BatPrintf.fprintf f "<analysis name=\"%s\">\n" (find_spec_name n);
       S.printXml f (obj x);
       BatPrintf.fprintf f "</analysis>\n"
     )
 
-  let invariant c = unop_map (fun n (module S: Printable.W) x ->
+  let invariant c = unop_map (fun n (module S: SpecSysVar) x ->
       S.invariant c (obj x)
     )
 
   let arbitrary () =
-    let arbs = map (fun (n, (module S: Printable.W)) -> QCheck.map ~rev:(fun (_, o) -> obj o) (fun x -> (n, repr x)) @@ S.arbitrary ()) @@ domain_list () in
+    let arbs = map (fun (n, (module S: SpecSysVar)) -> QCheck.map ~rev:(fun (_, o) -> obj o) (fun x -> (n, repr x)) @@ S.arbitrary ()) @@ domain_list () in
     QCheck.oneof arbs
 end
 
diff --git a/src/domains/printable.ml b/src/domains/printable.ml
index 291ecf1f2b..d95d0e78c1 100644
--- a/src/domains/printable.ml
+++ b/src/domains/printable.ml
@@ -32,12 +32,6 @@ sig
   val relift: t -> t
 end
 
-module type W =
-sig
-  include S
-  val is_write_only: t -> bool (* TODO: move elsewhere *)
-end
-
 module Empty: S =
 struct
   type t = | [@@deriving eq, ord, hash]
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 9cb6235584..d3282baa9a 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -12,16 +12,22 @@ module M  = Messages
   * other functions. *)
 type fundecs = fundec list * fundec list * fundec list
 
+module type SysVar =
+sig
+  type t
+  val is_write_only: t -> bool
+end
+
 module type VarType =
 sig
   include Hashtbl.HashedType
+  include SysVar with type t := t
   val pretty_trace: unit -> t -> doc
   val compare : t -> t -> int
 
   val printXml : 'a BatInnerIO.output -> t -> unit
   val var_id   : t -> string
   val node      : t -> MyCFG.node
-  val is_write_only: t -> bool
   val relift    : t -> t (* needed only for incremental+hashcons to re-hashcons contexts after loading *)
 end
 
@@ -66,7 +72,13 @@ struct
   let is_write_only _ = false
 end
 
-module GVarF (V: Printable.W) =
+module type SpecSysVar =
+sig
+  include Printable.S
+  include SysVar with type t := t
+end
+
+module GVarF (V: SpecSysVar) =
 struct
   include Printable.Either (V) (CilType.Fundec)
   let spec x = `Left x
@@ -370,7 +382,7 @@ sig
   module D : Lattice.S
   module G : Lattice.S
   module C : Printable.S
-  module V: Printable.W (** Global constraint variables. *)
+  module V: SpecSysVar (** Global constraint variables. *)
 
   val name : unit -> string
 

From 75caf5438585ad04ce323af3ac2d1d1e37f20a6f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 14:29:12 +0200
Subject: [PATCH 08/26] Extract default is_write_only to StdV

---
 src/analyses/apron/apronAnalysis.apron.ml |  2 +-
 src/analyses/arinc.ml                     |  2 +-
 src/analyses/base.ml                      |  2 +-
 src/analyses/extract_arinc.ml             |  2 +-
 src/analyses/mutexAnalysis.ml             |  6 +-----
 src/analyses/region.ml                    |  2 +-
 src/analyses/threadAnalysis.ml            |  2 +-
 src/analyses/threadJoins.ml               |  2 +-
 src/framework/analyses.ml                 | 14 ++++++++++++--
 9 files changed, 20 insertions(+), 14 deletions(-)

diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index 69a20833f6..3846afd31b 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -19,7 +19,7 @@ struct
   module V =
   struct
     include Priv.V
-    let is_write_only _ = false
+    include StdV
   end
 
   open AD
diff --git a/src/analyses/arinc.ml b/src/analyses/arinc.ml
index b2b70fdacb..78fb97f8b3 100644
--- a/src/analyses/arinc.ml
+++ b/src/analyses/arinc.ml
@@ -94,7 +94,7 @@ struct
   module V =
   struct
     include Printable.UnitConf (struct let name = "tasks" end)
-    let is_write_only _ = false
+    include StdV
   end
 
   let context fd d = { d with pred = Pred.bot (); ctx = Ctx.bot () }
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 7a3d3bba8b..85188a20b7 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -47,7 +47,7 @@ struct
     include Printable.Either (Priv.V) (ThreadIdDomain.Thread)
     let priv x = `Left x
     let thread x = `Right x
-    let is_write_only _ = false
+    include StdV
   end
 
   module G =
diff --git a/src/analyses/extract_arinc.ml b/src/analyses/extract_arinc.ml
index 1faeee50cc..32b4eb7e03 100644
--- a/src/analyses/extract_arinc.ml
+++ b/src/analyses/extract_arinc.ml
@@ -36,7 +36,7 @@ struct
   module V =
   struct
     include Printable.UnitConf (struct let name = "tasks" end)
-    let is_write_only _ = false
+    include StdV
   end
 
   type pname = string (* process name *)
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 3451f43b46..806d7be280 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -34,11 +34,7 @@ struct
 
   (** We do not add global state, so just lift from [BS]*)
   module G = P.G
-  module V =
-  struct
-    include VarinfoV
-    let is_write_only _ = false
-  end
+  module V = VarinfoV
 
   let should_join x y = D.equal x y
 
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index a2c5a4d963..f062ffbb1a 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -17,7 +17,7 @@ struct
   module V =
   struct
     include Printable.UnitConf (struct let name = "partitions" end)
-    let is_write_only _ = false
+    include StdV
   end
 
   let regions exp part st : Lval.CilLval.t list =
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 4951d1cd9b..fabf2c3b3d 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -17,7 +17,7 @@ struct
   module V =
   struct
     include T
-    let is_write_only _ = false
+    include StdV
   end
 
   let should_join = D.equal
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index c2e680571b..4638f6417e 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -17,7 +17,7 @@ struct
   module V =
   struct
     include TID
-    let is_write_only _ = false
+    include StdV
   end
 
   (* transfer functions *)
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index d3282baa9a..50cb13d3dd 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -572,11 +572,21 @@ struct
     BatPrintf.fprintf f "<context>\n%a</context>\n%a" C.printXml c D.printXml d
 end
 
-module VarinfoV = CilType.Varinfo (* TODO: or Basetype.Variables? *)
+module StdV =
+struct
+  let is_write_only _ = false
+end
+
+module VarinfoV =
+struct
+  include CilType.Varinfo (* TODO: or Basetype.Variables? *)
+  include StdV
+end
+
 module EmptyV =
 struct
   include Printable.Empty
-  let is_write_only _ = false
+  include StdV
 end
 
 module UnitA =

From 92fd35f33ce7420cc6a364fd7da034a3bba2874d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 14:35:23 +0200
Subject: [PATCH 09/26] Deduplicate DomVariantSysVar

---
 src/analyses/mCP.ml         |  4 +-
 src/analyses/mCPRegistry.ml | 80 ++++++++-----------------------------
 2 files changed, 18 insertions(+), 66 deletions(-)

diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index a136f278e6..ad3731b9ad 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -13,12 +13,12 @@ module MCP2 : Analyses.Spec
   with module D = DomListLattice (LocalDomainListSpec)
    and module G = DomVariantLattice (GlobalDomainListSpec)
    and module C = DomListPrintable (ContextListSpec)
-   and module V = DomVariantPrintableW (VarListSpec) =
+   and module V = DomVariantSysVar (VarListSpec) =
 struct
   module D = DomListLattice (LocalDomainListSpec)
   module G = DomVariantLattice (GlobalDomainListSpec)
   module C = DomListPrintable (ContextListSpec)
-  module V = DomVariantPrintableW (VarListSpec)
+  module V = DomVariantSysVar (VarListSpec)
 
   open List open Obj
   let v_of n v = (n, repr v)
diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index bda4b1059f..89f1f16d8a 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -45,7 +45,7 @@ sig
   val domain_list : unit -> (int * (module Printable.S)) list
 end
 
-module type DomainListPrintableWSpec =
+module type DomainListSysVarSpec =
 sig
   val assoc_dom : int -> (module SpecSysVar)
   val domain_list : unit -> (int * (module SpecSysVar)) list
@@ -87,6 +87,18 @@ struct
     List.map (fun (x,y) -> (x,f y)) (D.domain_list ())
 end
 
+module PrintableOfSysVarSpec (D:DomainListSysVarSpec) : DomainListPrintableSpec =
+struct
+  let assoc_dom n =
+    let f (module L:SpecSysVar) = (module L : Printable.S)
+    in
+    f (D.assoc_dom n)
+
+  let domain_list () =
+    let f (module L:SpecSysVar) = (module L : Printable.S) in
+    List.map (fun (x,y) -> (x,f y)) (D.domain_list ())
+end
+
 module DomListPrintable (DLSpec : DomainListPrintableSpec)
   : Printable.S with type t = (int * unknown) list
 =
@@ -245,81 +257,21 @@ struct
     QCheck.oneof arbs
 end
 
-(* TODO: deduplicate *)
-module DomVariantPrintableW (DLSpec : DomainListPrintableWSpec)
+module DomVariantSysVar (DLSpec : DomainListSysVarSpec)
   : SpecSysVar with type t = int * unknown
 =
 struct
-  include Printable.Std (* for default invariant, tag, ... *)
-
   open DLSpec
-  open List
   open Obj
 
-  type t = int * unknown
+  include DomVariantPrintable (PrintableOfSysVarSpec (DLSpec))
 
   let unop_map f ((n, d):t) =
     f n (assoc_dom n) d
 
-  let pretty () = unop_map (fun n (module S: SpecSysVar) x ->
-      Pretty.dprintf "%s:%a" (S.name ()) S.pretty (obj x)
-    )
-
-  let show = unop_map (fun n (module S: SpecSysVar) x ->
-      let analysis_name = find_spec_name n in
-      analysis_name ^ ":" ^ S.show (obj x)
-    )
-
   let is_write_only = unop_map (fun n (module S: SpecSysVar) x ->
       S.is_write_only (obj x)
     )
-
-  let to_yojson x =
-    `Assoc [
-      unop_map (fun n (module S: SpecSysVar) x ->
-          let name = find_spec_name n in
-          (name, S.to_yojson (obj x))
-        ) x
-    ]
-
-  let equal (n1, x1) (n2, x2) =
-    n1 = n2 && (
-      let module S = (val assoc_dom n1) in
-      S.equal (obj x1) (obj x2)
-    )
-
-  let compare (n1, x1) (n2, x2) =
-    let r = Stdlib.compare n1 n2 in
-    if r <> 0 then
-      r
-    else
-      let module S = (val assoc_dom n1) in
-      S.compare (obj x1) (obj x2)
-
-  let hash = unop_map (fun n (module S: SpecSysVar) x ->
-      Hashtbl.hash (n, S.hash (obj x))
-    )
-
-  let name () =
-    let domain_name (n, (module S: SpecSysVar)) =
-      let analysis_name = find_spec_name n in
-      analysis_name ^ ":" ^ S.name ()
-    in
-    IO.to_string (List.print ~first:"" ~last:"" ~sep:" | " String.print) (map domain_name @@ domain_list ())
-
-  let printXml f = unop_map (fun n (module S: SpecSysVar) x ->
-      BatPrintf.fprintf f "<analysis name=\"%s\">\n" (find_spec_name n);
-      S.printXml f (obj x);
-      BatPrintf.fprintf f "</analysis>\n"
-    )
-
-  let invariant c = unop_map (fun n (module S: SpecSysVar) x ->
-      S.invariant c (obj x)
-    )
-
-  let arbitrary () =
-    let arbs = map (fun (n, (module S: SpecSysVar)) -> QCheck.map ~rev:(fun (_, o) -> obj o) (fun x -> (n, repr x)) @@ S.arbitrary ()) @@ domain_list () in
-    QCheck.oneof arbs
 end
 
 module DomListLattice (DLSpec : DomainListLatticeSpec)
@@ -422,7 +374,7 @@ struct
   let domain_list () = List.map (fun (n,p) -> n, p.cont) !activated_ctx_sens
 end
 
-module VarListSpec : DomainListPrintableWSpec =
+module VarListSpec : DomainListSysVarSpec =
 struct
   let assoc_dom n = (find_spec n).var
   let domain_list () = List.map (fun (n,p) -> n, p.var) !activated

From 61b965487c98de4fb7b60d674d894384561988b6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 14:47:19 +0200
Subject: [PATCH 10/26] Extract IncrWrite postsolver in TD3

---
 src/solvers/postSolver.ml | 31 +++++++++++++++----------------
 src/solvers/td3.ml        | 35 ++++++++++++++++++++++++++---------
 2 files changed, 41 insertions(+), 25 deletions(-)

diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
index db6f074174..27b230e9c0 100644
--- a/src/solvers/postSolver.ml
+++ b/src/solvers/postSolver.ml
@@ -9,8 +9,8 @@ sig
   module VH: Hashtbl.S with type key = S.v
 
   val init: unit -> unit
-  val one_side: vh:S.Dom.t VH.t -> vhw:S.Dom.t VH.t VH.t -> x:S.v -> y:S.v -> d:S.Dom.t -> unit
-  val one_constraint: vh:S.Dom.t VH.t -> vhw:S.Dom.t VH.t VH.t -> x:S.v -> rhs:S.Dom.t -> unit
+  val one_side: vh:S.Dom.t VH.t -> x:S.v -> y:S.v -> d:S.Dom.t -> unit
+  val one_constraint: vh:S.Dom.t VH.t -> x:S.v -> rhs:S.Dom.t -> unit
   val finalize: vh:S.Dom.t VH.t -> reachable:unit VH.t -> unit
 end
 
@@ -26,8 +26,8 @@ module Unit: F =
     module S = S
     module VH = VH
     let init () = ()
-    let one_side ~vh ~vhw ~x ~y ~d = ()
-    let one_constraint ~vh ~vhw ~x ~rhs = ()
+    let one_side ~vh ~x ~y ~d = ()
+    let one_constraint ~vh ~x ~rhs = ()
     let finalize ~vh ~reachable = ()
   end
 
@@ -40,12 +40,12 @@ struct
   let init () =
     PS1.init ();
     PS2.init ()
-  let one_side ~vh ~vhw ~x ~y ~d =
-    PS1.one_side ~vh ~vhw ~x ~y ~d;
-    PS2.one_side ~vh ~vhw ~x ~y ~d
-  let one_constraint ~vh ~vhw ~x ~rhs =
-    PS1.one_constraint ~vh ~vhw ~x ~rhs;
-    PS2.one_constraint ~vh ~vhw ~x ~rhs
+  let one_side ~vh ~x ~y ~d =
+    PS1.one_side ~vh ~x ~y ~d;
+    PS2.one_side ~vh ~x ~y ~d
+  let one_constraint ~vh ~x ~rhs =
+    PS1.one_constraint ~vh ~x ~rhs;
+    PS2.one_constraint ~vh ~x ~rhs
   let finalize ~vh ~reachable =
     PS1.finalize ~vh ~reachable;
     PS2.finalize ~vh ~reachable
@@ -83,17 +83,16 @@ module Verify: F =
       Goblintutil.verified := Some false;
       ignore (Pretty.printf "Fixpoint not reached at %a\nOrigin: %a\n @[Solver computed:\n%a\nSide-effect:\n%a\nDifference: %a\n@]" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs))
 
-    let one_side ~vh ~vhw ~x ~y ~d =
+    let one_side ~vh ~x ~y ~d =
       let y_lhs = try VH.find vh y with Not_found -> S.Dom.bot () in
       if S.Var.is_write_only y then (
         (* HACK: incremental accesses etc insanity! *)
-        VH.replace vh y (S.Dom.join y_lhs d);
-        VH.modify_def (VH.create 1) x (fun w -> VH.add w y d; w) vhw (* inner add intentional *)
+        VH.replace vh y (S.Dom.join y_lhs d)
       )
       else if not (S.Dom.leq d y_lhs) then
         complain_side x y ~lhs:y_lhs ~rhs:d
 
-    let one_constraint ~vh ~vhw ~x ~rhs =
+    let one_constraint ~vh ~x ~rhs =
       let lhs = try VH.find vh x with Not_found -> S.Dom.bot () in
       if not (S.Dom.leq rhs lhs) then
         complain_constraint x ~lhs ~rhs
@@ -203,12 +202,12 @@ struct
         try VH.find vh y with Not_found -> S.Dom.bot ()
       in
       let set y d =
-        PS.one_side ~vh ~vhw ~x ~y ~d;
+        PS.one_side ~vh ~x ~y ~d;
         (* check before recursing *)
         one_var y
       in
       let rhs = f get set in
-      PS.one_constraint ~vh ~vhw ~x ~rhs
+      PS.one_constraint ~vh ~x ~rhs
     in
     List.iter one_var vs;
 
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index adc5016fc8..c96e04d38b 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -958,7 +958,7 @@ module WP =
       struct
         include PostSolver.Unit (S) (HM)
 
-        let one_side ~vh ~vhw ~x ~y ~d =
+        let one_side ~vh ~x ~y ~d =
           HM.replace side_dep y (VS.add x (try HM.find side_dep y with Not_found -> VS.empty));
           HM.replace side_infl x (VS.add y (try HM.find side_infl x with Not_found -> VS.empty));
       end
@@ -992,13 +992,6 @@ module WP =
             HM.iter (fun _ m ->
                 Messages.add m
               ) var_messages;
-            (* retrigger *)
-            HM.iter (fun x w ->
-                HM.iter (fun y d ->
-                    let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in
-                    HM.replace rho y (S.Dom.join old_d d)
-                  ) w
-              ) rho_write
           );
 
           (* hook to collect new messages *)
@@ -1009,6 +1002,30 @@ module WP =
           );
       end
       in
+
+      let module IncrWrite: PostSolver.S with module S = S and module VH = HM =
+      struct
+        include PostSolver.Unit (S) (HM)
+
+        let init () =
+          (* retrigger superstable side writes *)
+          if incr_verify then (
+            HM.iter (fun x w ->
+                HM.iter (fun y d ->
+                    let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in
+                    HM.replace rho y (S.Dom.join old_d d)
+                  ) w
+              ) rho_write
+          )
+
+        let one_side ~vh ~x ~y ~d =
+          if S.Var.is_write_only y then (
+            (* HACK: incremental accesses etc insanity! *)
+            VH.modify_def (VH.create 1) x (fun w -> VH.add w y d; w) rho_write (* inner add intentional *)
+          )
+      end
+      in
+
       let module MakeIncrListArg =
       struct
         module Arg =
@@ -1018,7 +1035,7 @@ module WP =
         end
         include PostSolver.ListArgFromStdArg (S) (HM) (Arg)
 
-        let postsolvers = (module IncrPrune: M) :: (module SideInfl: M) :: (module IncrWarn: M) :: postsolvers
+        let postsolvers = (module IncrPrune: M) :: (module SideInfl: M) :: (module IncrWrite: M) :: (module IncrWarn: M) :: postsolvers
 
         let init_reachable ~vh =
           if incr_verify then

From 56baff8b3b26f4684bb869f6d9a7855cef68a52e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 14:51:03 +0200
Subject: [PATCH 11/26] Add incremental pruning of rho_write in TD3

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

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index c96e04d38b..5334e68f4b 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -949,6 +949,18 @@ module WP =
           filter_vs_hm infl;
           filter_vs_hm side_infl;
           filter_vs_hm side_dep;
+
+          VH.filteri_inplace (fun x w ->
+              if VH.mem reachable x then (
+                VH.filteri_inplace (fun y _ ->
+                    VH.mem reachable y
+                  ) w;
+                true
+              )
+              else
+                false
+            ) rho_write
+
           (* TODO: prune other data structures? *)
       end
       in

From 8f394f33129a3e3d45156a48ff4b3ef7854a0844 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 14:57:44 +0200
Subject: [PATCH 12/26] Optimize IncrWrite.one_side

---
 src/solvers/td3.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 5334e68f4b..04c8aea35a 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -1032,8 +1032,15 @@ module WP =
 
         let one_side ~vh ~x ~y ~d =
           if S.Var.is_write_only y then (
-            (* HACK: incremental accesses etc insanity! *)
-            VH.modify_def (VH.create 1) x (fun w -> VH.add w y d; w) rho_write (* inner add intentional *)
+            let w =
+              try
+                VH.find rho_write x
+              with Not_found ->
+                let w = VH.create 1 in (* only create on demand, modify_def would eagerly allocate *)
+                VH.replace rho_write x w;
+                w
+            in
+            VH.add w y d (* intentional add *)
           )
       end
       in

From e87a91b561143f3c19eb2fc1b6a4a81d4cb14252 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 14:58:53 +0200
Subject: [PATCH 13/26] Remove now-unused rho_write argument from postsolver

---
 src/framework/constraints.ml | 2 +-
 src/solvers/postSolver.ml    | 6 +++---
 src/solvers/td3.ml           | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index d6f6a0d37b..bdf5722faf 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -803,7 +803,7 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve
 
     let solve box xs vs =
       let vh = Sol.solve box xs vs in
-      Post.post xs vs vh (VH.create 0);
+      Post.post xs vs vh;
       (vh, ())
   end
 
diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
index 27b230e9c0..95e5bf968b 100644
--- a/src/solvers/postSolver.ml
+++ b/src/solvers/postSolver.ml
@@ -175,7 +175,7 @@ struct
   module S = PS.S
   module VH = PS.VH
 
-  let post xs vs vh vhw =
+  let post xs vs vh =
     if get_bool "dbg.verbose" then
       print_endline "Postsolving\n";
 
@@ -254,7 +254,7 @@ struct
       in
       Some (List.reduce compose postsolvers)
 
-  let post xs vs vh vhw =
+  let post xs vs vh =
     match postsolver_opt with
     | None -> ()
     | Some (module PS) ->
@@ -265,7 +265,7 @@ struct
       end
       in
       let module M = MakeIncr (IncrPS) in
-      M.post xs vs vh vhw
+      M.post xs vs vh
 end
 
 (** Make complete (non-incremental) postsolving function from list of postsolvers.
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 04c8aea35a..abb991dbab 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -1066,7 +1066,7 @@ module WP =
 
       let module Post = PostSolver.MakeIncrList (MakeIncrListArg) in
 
-      Post.post st vs rho rho_write;
+      Post.post st vs rho;
 
       print_data data "Data after postsolve";
 

From df2e20551b379cf175ea73c73bfce01bd457849e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 15:00:16 +0200
Subject: [PATCH 14/26] Update Verify postsolver comment about hack

---
 src/solvers/postSolver.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
index 95e5bf968b..f664cd2589 100644
--- a/src/solvers/postSolver.ml
+++ b/src/solvers/postSolver.ml
@@ -85,10 +85,8 @@ module Verify: F =
 
     let one_side ~vh ~x ~y ~d =
       let y_lhs = try VH.find vh y with Not_found -> S.Dom.bot () in
-      if S.Var.is_write_only y then (
-        (* HACK: incremental accesses etc insanity! *)
-        VH.replace vh y (S.Dom.join y_lhs d)
-      )
+      if S.Var.is_write_only y then
+        VH.replace vh y (S.Dom.join y_lhs d) (* HACK: allow warnings/accesses to be added without complaining *)
       else if not (S.Dom.leq d y_lhs) then
         complain_side x y ~lhs:y_lhs ~rhs:d
 

From 3ea3f9e32481b62bca6343cb88d9858fd2cb76ad Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 15:04:01 +0200
Subject: [PATCH 15/26] Prevent unnecessary write-only side restarting

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

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index abb991dbab..3848c0dd0c 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -553,7 +553,7 @@ module WP =
           let w = HM.find_default side_dep x VS.empty in
           HM.remove side_dep x;
 
-          if not (VS.is_empty w) && (not restart_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec)) then (
+          if not (VS.is_empty w) && (not restart_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec)) && not (S.Var.is_write_only x) then (
             (* restart side-effected var *)
             restart_leaf x;
 

From b98ee7f6170635d743835176f18faabb02c98a1c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 15:07:34 +0200
Subject: [PATCH 16/26] Fix SolverTest compilation

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

diff --git a/unittest/solver/solverTest.ml b/unittest/solver/solverTest.ml
index 7d8cd41858..1751ffcee2 100644
--- a/unittest/solver/solverTest.ml
+++ b/unittest/solver/solverTest.ml
@@ -16,6 +16,7 @@ struct
   let line_nr _ = 1
   let node _ = failwith "no node"
   let relift x = x
+  let is_write_only _ = false
 end
 
 (* domain is (reversed) integers *)

From 44d206ab871a32d2d1e288f3f9b13ed4c1733882 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 15:11:48 +0200
Subject: [PATCH 17/26] Add incremental test with access through wrapper
 function

---
 .../11-restart/13-mutex-simple-wrap.c         | 27 +++++++++++++++++++
 .../11-restart/13-mutex-simple-wrap.json      |  9 +++++++
 .../11-restart/13-mutex-simple-wrap.patch     | 22 +++++++++++++++
 3 files changed, 58 insertions(+)
 create mode 100644 tests/incremental/11-restart/13-mutex-simple-wrap.c
 create mode 100644 tests/incremental/11-restart/13-mutex-simple-wrap.json
 create mode 100644 tests/incremental/11-restart/13-mutex-simple-wrap.patch

diff --git a/tests/incremental/11-restart/13-mutex-simple-wrap.c b/tests/incremental/11-restart/13-mutex-simple-wrap.c
new file mode 100644
index 0000000000..53ff298524
--- /dev/null
+++ b/tests/incremental/11-restart/13-mutex-simple-wrap.c
@@ -0,0 +1,27 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void wrap() {
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  wrap();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/incremental/11-restart/13-mutex-simple-wrap.json b/tests/incremental/11-restart/13-mutex-simple-wrap.json
new file mode 100644
index 0000000000..daff0678ce
--- /dev/null
+++ b/tests/incremental/11-restart/13-mutex-simple-wrap.json
@@ -0,0 +1,9 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/tests/incremental/11-restart/13-mutex-simple-wrap.patch b/tests/incremental/11-restart/13-mutex-simple-wrap.patch
new file mode 100644
index 0000000000..89e713a9c3
--- /dev/null
+++ b/tests/incremental/11-restart/13-mutex-simple-wrap.patch
@@ -0,0 +1,22 @@
+--- tests/incremental/11-restart/13-mutex-simple-wrap.c
++++ tests/incremental/11-restart/13-mutex-simple-wrap.c
+@@ -7,15 +7,15 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+ void *t_fun(void *arg) {
+   pthread_mutex_lock(&mutex1);
+-  myglobal=myglobal+1; // RACE!
++  myglobal=myglobal+1; // NORACE
+   pthread_mutex_unlock(&mutex1);
+   return NULL;
+ }
+
+ void wrap() {
+-  pthread_mutex_lock(&mutex2);
+-  myglobal=myglobal+1; // RACE!
+-  pthread_mutex_unlock(&mutex2);
++  pthread_mutex_lock(&mutex1);
++  myglobal=myglobal+1; // NORACE
++  pthread_mutex_unlock(&mutex1);
+ }
+
+ int main(void) {

From e86b9da21494cf704a76ef86c7661951151a5f90 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 15:13:38 +0200
Subject: [PATCH 18/26] Move write-only sided restart incremental tests to
 13-restart-write

---
 .../12-mutex-simple.c => 13-restart-write/01-mutex-simple.c}  | 0
 .../01-mutex-simple.json}                                     | 0
 .../01-mutex-simple.patch}                                    | 4 ++--
 .../02-mutex-simple-wrap.c}                                   | 0
 .../02-mutex-simple-wrap.json}                                | 0
 .../02-mutex-simple-wrap.patch}                               | 4 ++--
 6 files changed, 4 insertions(+), 4 deletions(-)
 rename tests/incremental/{11-restart/12-mutex-simple.c => 13-restart-write/01-mutex-simple.c} (100%)
 rename tests/incremental/{11-restart/12-mutex-simple.json => 13-restart-write/01-mutex-simple.json} (100%)
 rename tests/incremental/{11-restart/12-mutex-simple.patch => 13-restart-write/01-mutex-simple.patch} (84%)
 rename tests/incremental/{11-restart/13-mutex-simple-wrap.c => 13-restart-write/02-mutex-simple-wrap.c} (100%)
 rename tests/incremental/{11-restart/13-mutex-simple-wrap.json => 13-restart-write/02-mutex-simple-wrap.json} (100%)
 rename tests/incremental/{11-restart/13-mutex-simple-wrap.patch => 13-restart-write/02-mutex-simple-wrap.patch} (79%)

diff --git a/tests/incremental/11-restart/12-mutex-simple.c b/tests/incremental/13-restart-write/01-mutex-simple.c
similarity index 100%
rename from tests/incremental/11-restart/12-mutex-simple.c
rename to tests/incremental/13-restart-write/01-mutex-simple.c
diff --git a/tests/incremental/11-restart/12-mutex-simple.json b/tests/incremental/13-restart-write/01-mutex-simple.json
similarity index 100%
rename from tests/incremental/11-restart/12-mutex-simple.json
rename to tests/incremental/13-restart-write/01-mutex-simple.json
diff --git a/tests/incremental/11-restart/12-mutex-simple.patch b/tests/incremental/13-restart-write/01-mutex-simple.patch
similarity index 84%
rename from tests/incremental/11-restart/12-mutex-simple.patch
rename to tests/incremental/13-restart-write/01-mutex-simple.patch
index 14913c581d..156312b915 100644
--- a/tests/incremental/11-restart/12-mutex-simple.patch
+++ b/tests/incremental/13-restart-write/01-mutex-simple.patch
@@ -1,5 +1,5 @@
---- tests/incremental/11-restart/12-mutex-simple.c
-+++ tests/incremental/11-restart/12-mutex-simple.c
+--- tests/incremental/13-restart-write/01-mutex-simple.c
++++ tests/incremental/13-restart-write/01-mutex-simple.c
 @@ -7,7 +7,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
  void *t_fun(void *arg) {
diff --git a/tests/incremental/11-restart/13-mutex-simple-wrap.c b/tests/incremental/13-restart-write/02-mutex-simple-wrap.c
similarity index 100%
rename from tests/incremental/11-restart/13-mutex-simple-wrap.c
rename to tests/incremental/13-restart-write/02-mutex-simple-wrap.c
diff --git a/tests/incremental/11-restart/13-mutex-simple-wrap.json b/tests/incremental/13-restart-write/02-mutex-simple-wrap.json
similarity index 100%
rename from tests/incremental/11-restart/13-mutex-simple-wrap.json
rename to tests/incremental/13-restart-write/02-mutex-simple-wrap.json
diff --git a/tests/incremental/11-restart/13-mutex-simple-wrap.patch b/tests/incremental/13-restart-write/02-mutex-simple-wrap.patch
similarity index 79%
rename from tests/incremental/11-restart/13-mutex-simple-wrap.patch
rename to tests/incremental/13-restart-write/02-mutex-simple-wrap.patch
index 89e713a9c3..e38d432722 100644
--- a/tests/incremental/11-restart/13-mutex-simple-wrap.patch
+++ b/tests/incremental/13-restart-write/02-mutex-simple-wrap.patch
@@ -1,5 +1,5 @@
---- tests/incremental/11-restart/13-mutex-simple-wrap.c
-+++ tests/incremental/11-restart/13-mutex-simple-wrap.c
+--- tests/incremental/13-restart-write/02-mutex-simple-wrap.c
++++ tests/incremental/13-restart-write/02-mutex-simple-wrap.c
 @@ -7,15 +7,15 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
  void *t_fun(void *arg) {

From 1d011ccb3cf77a43d3d95af34d6c7a6d3edc9bb9 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 17:35:57 +0200
Subject: [PATCH 19/26] Add incremental test
 13-restart-write/03-mutex-simple-nochange

This checks that race warnings don't all disappear.
---
 .../03-mutex-simple-nochange.c                | 23 +++++++++++++++++++
 .../03-mutex-simple-nochange.json             |  9 ++++++++
 .../03-mutex-simple-nochange.patch            |  0
 3 files changed, 32 insertions(+)
 create mode 100644 tests/incremental/13-restart-write/03-mutex-simple-nochange.c
 create mode 100644 tests/incremental/13-restart-write/03-mutex-simple-nochange.json
 create mode 100644 tests/incremental/13-restart-write/03-mutex-simple-nochange.patch

diff --git a/tests/incremental/13-restart-write/03-mutex-simple-nochange.c b/tests/incremental/13-restart-write/03-mutex-simple-nochange.c
new file mode 100644
index 0000000000..82c1642a93
--- /dev/null
+++ b/tests/incremental/13-restart-write/03-mutex-simple-nochange.c
@@ -0,0 +1,23 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/incremental/13-restart-write/03-mutex-simple-nochange.json b/tests/incremental/13-restart-write/03-mutex-simple-nochange.json
new file mode 100644
index 0000000000..daff0678ce
--- /dev/null
+++ b/tests/incremental/13-restart-write/03-mutex-simple-nochange.json
@@ -0,0 +1,9 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/tests/incremental/13-restart-write/03-mutex-simple-nochange.patch b/tests/incremental/13-restart-write/03-mutex-simple-nochange.patch
new file mode 100644
index 0000000000..e69de29bb2

From 1aafc7798447401b2a8cd5b2c5ddccd4d5e2027a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 17:30:14 +0200
Subject: [PATCH 20/26] Update commented-out debug prints for write-only
 incremental restarting

---
 src/framework/control.ml | 2 +-
 src/solvers/td3.ml       | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index e55dcb018f..e3676e5477 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -598,7 +598,7 @@ struct
       CfgTools.dead_code_cfg file (module Cfg : CfgBidir) liveness;
 
     let warn_global g v =
-      (* ignore (Pretty.printf "warn_global %a %a\n" CilType.Varinfo.pretty g EQSys.G.pretty v); *)
+      (* ignore (Pretty.printf "warn_global %a %a\n" EQSys.GVar.pretty_trace g EQSys.G.pretty v); *)
       (* build a ctx for using the query system *)
       let rec ctx =
         { ask    = (fun (type a) (q: a Queries.t) -> Spec.query ctx q)
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 3848c0dd0c..f1f5714291 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -1025,6 +1025,7 @@ module WP =
             HM.iter (fun x w ->
                 HM.iter (fun y d ->
                     let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in
+                    (* ignore (Pretty.printf "rho_write retrigger %a %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old_d S.Dom.pretty d); *)
                     HM.replace rho y (S.Dom.join old_d d)
                   ) w
               ) rho_write
@@ -1032,6 +1033,7 @@ module WP =
 
         let one_side ~vh ~x ~y ~d =
           if S.Var.is_write_only y then (
+            (* ignore (Pretty.printf "rho_write collect %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty d); *)
             let w =
               try
                 VH.find rho_write x

From d224f50e13cecc94eb60500a9ce2e4e119fd88cb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 17:30:29 +0200
Subject: [PATCH 21/26] Enable allglobs in test-incremental.sh

---
 scripts/test-incremental.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/test-incremental.sh b/scripts/test-incremental.sh
index fa95f25f42..5541afb55d 100755
--- a/scripts/test-incremental.sh
+++ b/scripts/test-incremental.sh
@@ -11,7 +11,7 @@ source=$base/$test.c
 conf=$base/$test.json
 patch=$base/$test.patch
 
-args="--enable dbg.debug --enable printstats -v"
+args="--enable dbg.debug --enable printstats -v --enable allglobs"
 
 ./goblint --conf $conf $args --enable incremental.save $source &> $base/$test.before.log
 

From faaf8d7f5aa67bdf9c67aef8b1cf4fcfe6c80aa6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 17:33:34 +0200
Subject: [PATCH 22/26] Fix retriggered superstable write sides not being
 reachable

This caused them to be incorrectly pruned.
---
 src/solvers/td3.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index f1f5714291..9940efc3f8 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -992,6 +992,13 @@ module WP =
         HM.clear rho_write
       );
 
+      let init_reachable =
+        if incr_verify then
+          HM.copy superstable (* consider superstable reached: stop recursion (evaluation) and keep from being pruned *)
+        else
+          HM.create 0 (* doesn't matter, not used *)
+      in
+
       let module IncrWarn: PostSolver.S with module S = S and module VH = HM =
       struct
         include PostSolver.Warn (S) (HM)
@@ -1026,7 +1033,8 @@ module WP =
                 HM.iter (fun y d ->
                     let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in
                     (* ignore (Pretty.printf "rho_write retrigger %a %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old_d S.Dom.pretty d); *)
-                    HM.replace rho y (S.Dom.join old_d d)
+                    HM.replace rho y (S.Dom.join old_d d);
+                    HM.replace init_reachable y ();
                   ) w
               ) rho_write
           )
@@ -1060,7 +1068,7 @@ module WP =
 
         let init_reachable ~vh =
           if incr_verify then
-            HM.copy superstable (* consider superstable reached: stop recursion (evaluation) and keep from being pruned *)
+            init_reachable
           else
             HM.create (HM.length vh)
       end

From 37a330f4def2b2fc67ad6ad31b90c2f3ece94996 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 17:38:31 +0200
Subject: [PATCH 23/26] Add incremental test
 11-restart/07-local-wpoint-nochange

One read access disappears due to broken rho_write relift.
---
 .../11-restart/07-local-wpoint-nochange.c     | 23 +++++++++++++++++++
 .../11-restart/07-local-wpoint-nochange.json  | 10 ++++++++
 .../11-restart/07-local-wpoint-nochange.patch |  0
 3 files changed, 33 insertions(+)
 create mode 100644 tests/incremental/11-restart/07-local-wpoint-nochange.c
 create mode 100644 tests/incremental/11-restart/07-local-wpoint-nochange.json
 create mode 100644 tests/incremental/11-restart/07-local-wpoint-nochange.patch

diff --git a/tests/incremental/11-restart/07-local-wpoint-nochange.c b/tests/incremental/11-restart/07-local-wpoint-nochange.c
new file mode 100644
index 0000000000..747693452a
--- /dev/null
+++ b/tests/incremental/11-restart/07-local-wpoint-nochange.c
@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <pthread.h>
+
+int g = 1;
+
+void* t_fun(void *arg) {
+    g = 0;
+    return NULL;
+}
+
+int main() {
+    pthread_t id;
+    pthread_create(&id, NULL, t_fun, NULL); // just go multithreaded
+
+    int x;
+    x = g;
+    while (1) {
+        assert(x == 1); // UNKNOWN before, UNKNOWN after
+        x = g;
+    }
+
+    return 0;
+}
\ No newline at end of file
diff --git a/tests/incremental/11-restart/07-local-wpoint-nochange.json b/tests/incremental/11-restart/07-local-wpoint-nochange.json
new file mode 100644
index 0000000000..ff773f6993
--- /dev/null
+++ b/tests/incremental/11-restart/07-local-wpoint-nochange.json
@@ -0,0 +1,10 @@
+{
+    "ana": {
+        "int": {
+            "interval": true
+        }
+    },
+    "incremental": {
+        "wpoint": false
+    }
+}
\ No newline at end of file
diff --git a/tests/incremental/11-restart/07-local-wpoint-nochange.patch b/tests/incremental/11-restart/07-local-wpoint-nochange.patch
new file mode 100644
index 0000000000..e69de29bb2

From 4b23cc72608ab52c552f46ae10ea549e7c482139 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 17:33:55 +0200
Subject: [PATCH 24/26] Fix rho_write relift in TD3

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

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 9940efc3f8..d9f7163d34 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -1149,7 +1149,7 @@ module WP =
           HM.iter (fun x w ->
               let w' = HM.create (HM.length w) in
               HM.iter (fun y d ->
-                  HM.replace w' (S.Var.relift y) (S.Dom.relift 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;

From 574185faa963d47a826526c61b25558c31cd0f55 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 10 Mar 2022 17:35:15 +0200
Subject: [PATCH 25/26] Add write-only sides to stable

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

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index d9f7163d34..235e0e2b74 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -1035,6 +1035,7 @@ module WP =
                     (* ignore (Pretty.printf "rho_write retrigger %a %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old_d S.Dom.pretty d); *)
                     HM.replace rho y (S.Dom.join old_d d);
                     HM.replace init_reachable y ();
+                    HM.replace stable y (); (* make stable just in case, so following incremental load would have in superstable *)
                   ) w
               ) rho_write
           )
@@ -1042,6 +1043,7 @@ module WP =
         let one_side ~vh ~x ~y ~d =
           if S.Var.is_write_only y then (
             (* ignore (Pretty.printf "rho_write collect %a %a %a\n" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty d); *)
+            HM.replace stable y (); (* make stable just in case, so following incremental load would have in superstable *)
             let w =
               try
                 VH.find rho_write x

From f98796399d2d55f1a0c500688de99767a8a4f830 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 11 Mar 2022 13:39:43 +0200
Subject: [PATCH 26/26] Document TD3 IncrWrite postsolver

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

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 235e0e2b74..868fa0c3cd 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -1022,6 +1022,8 @@ module WP =
       end
       in
 
+      (** Incremental write-only side effect restart handling:
+          retriggers superstable ones (after restarting above) and collects new (non-superstable) ones. *)
       let module IncrWrite: PostSolver.S with module S = S and module VH = HM =
       struct
         include PostSolver.Unit (S) (HM)