Copy over #1729

Author: michael-schwarz

src/config/options.schema.json

@@ -2546,6 +2546,12 @@
                   "type": "boolean",
                   "default": false
                 },
+                "eliminate-cyclic-dead": {
+                  "title": "solvers.td3.narrow-sides.eliminate-cyclic-dead",
+                  "description": "Collect recursive garbage.",
+                  "type": "boolean",
+                  "default": false
+                },
                 "apinis": {
                   "title": "solvers.td3.narrow-sides.apinis",
                   "description": "apply warrowing to globals instead of contributions; Enabling this option is incompatible with stable and immediate-growth and ignores conservative-widen and narrow-gas.",

src/constraint/constrSys.ml

@@ -51,6 +51,7 @@ sig
   (** Compute incremental constraint system change from old solution. *)
 
   val postmortem: v -> v list
+  val must_same_context: v -> v -> bool
 end
 
 (** Any system of side-effecting equations over lattices. *)
@@ -68,6 +69,7 @@ sig
   val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit
   val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info
   val postmortem: LVar.t -> LVar.t list
+  val must_same_context: LVar.t -> LVar.t -> bool
 end
 
 (** A solver is something that can translate a system into a solution (hash-table).
@@ -218,6 +220,11 @@ struct
     match leaf with
     | `L g -> List.map (fun x -> `L x) @@ S.postmortem g
     | _ -> []
+
+  let must_same_context x y =
+    match x, y with
+    | `L x, `L y -> S.must_same_context x y
+    | _ -> false
 end
 
 (** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *)

src/framework/constraints.ml

@@ -554,6 +554,8 @@ struct
     match leaf with
     | FunctionEntry fd, c -> [(Function fd, c)]
     | _ -> []
+
+  let must_same_context (_,cx) (_,cy) = S.C.equal cx cy
 end
 
 

src/solver/td3.ml

@@ -286,6 +286,7 @@ module Base =
       let narrow_sides_gas_default = GobConfig.get_int "solvers.td3.narrow-sides.narrow-gas" in
       let narrow_sides_gas_default = if narrow_sides_gas_default < 0 then None else Some (narrow_sides_gas_default, D_Widen) in
       let narrow_sides_eliminate_dead = GobConfig.get_bool "solvers.td3.narrow-sides.eliminate-dead" in
+      let narrow_sides_eliminate_cyclic_dead = GobConfig.get_bool "solvers.td3.narrow-sides.eliminate-cyclic-dead" in
       let apinis = GobConfig.get_bool "solvers.td3.narrow-sides.apinis" in
       let narrow_sides_stats = GobConfig.get_bool "solvers.td3.narrow-sides.stats" in
 
@@ -481,6 +482,24 @@ module Base =
           | None -> S.Dom.bot () in
         let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot()) in
         S.Dom.join combined orphaned
+      and combined_side_elim_dead narrow_gas x y =
+        if HM.mem orphan_side_effects y then
+          (* If there is a start value, then we cannot get this back to bot anyway *)
+          combined_side y
+        else
+          let contribs = Option.get @@ HM.find_option data.divided_side_effects y in
+          let find_fundec v = Node.find_fundec (S.Var.node y) in
+          let y_fundec = find_fundec y  in
+          let has_outside_contrib = HM.exists (fun k _ -> (not @@ S.Var.equal k x) && ((not @@ CilType.Fundec.equal y_fundec (find_fundec k)) || (not @@ S.must_same_context y k))) contribs in
+          if has_outside_contrib then
+            (* If there is a contribution from outside the fundec, we cannot eliminate it *)
+            combined_side y
+          else
+            (* We can eliminate the contribution *)
+          if narrow_gas = None then
+            (HM.clear contribs; S.Dom.bot ())
+          else
+            (HM.map_inplace (fun _ (value, gas) -> (S.Dom.bot(), gas)) contribs; S.Dom.bot ())
       and side_acc acc changed x y d =
         let new_acc = match HM.find_option acc y with
           | Some acc -> if not @@ S.Dom.leq d acc then Some (S.Dom.join acc d) else None
@@ -623,6 +642,8 @@ module Base =
                 let y_newval = if S.Dom.leq old_side new_side then
                     (* If new side is strictly greater than the old one, the value of y can only increase. *)
                     S.Dom.join y_oldval new_side
+                  else if S.Dom.is_bot new_side && narrow_sides_eliminate_cyclic_dead then
+                    combined_side_elim_dead narrow_gas x y
                   else
                     combined_side y in
                 if not (S.Dom.equal y_newval y_oldval) then (

tests/regression/95-divided/23-dead-side-effect-cycle.c

@@ -0,0 +1,33 @@
+// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.eliminate-dead --enable solvers.td3.narrow-sides.eliminate-cyclic-dead --enable ana.base.priv.protection.changes-only
+#include <pthread.h>
+#include <goblint.h>
+
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+int a = 0;
+int b = 0;
+
+void annoy() {
+  b = 1;
+  if(b == 1) {
+    annoy();
+  }
+}
+
+void* f(void *d) {
+  pthread_mutex_lock(&mutex);
+  if (a < 10) {
+    a++;
+  }
+  if (a > 20) {
+    annoy();
+  }
+  pthread_mutex_unlock(&mutex);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, f, NULL);
+  __goblint_check(!b); //NORACE
+  return 0;
+}

tests/unit/solver/solverTest.ml

@@ -48,6 +48,7 @@ module ConstrSys = struct
   let iter_vars _ _ _ _ _ = ()
   let sys_change _ _ = {obsolete = []; delete = []; reluctant = []; restart = []}
   let postmortem _ = []
+  let must_same_context _ _ = false
 end
 
 module LH = BatHashtbl.Make (ConstrSys.LVar)