TD3: Eliminate Some Recursive Toxic Trash (namely the directly recursive one)

src/config/options.schema.json

@@ -2521,6 +2521,12 @@
                   "description": "side-effects that no longer occur are narrowed with bot.",
                   "type": "boolean",
                   "default": false
+                },
+                "eliminate-cyclic-dead": {
+                  "title": "solvers.td3.narrow-globs.eliminate-cyclic-dead",
+                  "description": "Collect recursive garbage.",
+                  "type": "boolean",
+                  "default": false
                 }
               },
               "additionalProperties": false

src/constraint/constrSys.ml

@@ -50,6 +50,8 @@ 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. *)
@@ -67,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).
@@ -212,6 +215,11 @@ struct
   let postmortem = function
     | `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

@@ -553,4 +553,7 @@ struct
   let postmortem = function
     | FunctionEntry fd, c -> [(Function fd, c)]
     | _ -> []
+
+  let must_same_context (_,cx) (_,cy) = S.C.equal cx cy
+
 end

src/solver/td3UpdateRule.ml

@@ -110,6 +110,7 @@ module Narrow:S =
     let narrow_globs_gas_default = GobConfig.get_int "solvers.td3.narrow-globs.narrow-gas"
     let narrow_globs_gas_default = if narrow_globs_gas_default < 0 then None else Some (narrow_globs_gas_default, D_Widen)
     let narrow_globs_eliminate_dead = GobConfig.get_bool "solvers.td3.narrow-globs.eliminate-dead"
+    let narrow_globs_eliminate_cyclic_dead = GobConfig.get_bool "solvers.td3.narrow-globs.eliminate-cyclic-dead"
 
     let get_wrapper ~solve_widen ~init ~stable ~data ~sides ~add_sides ~rho ~destabilize ~(side:?x:S.v -> S.v -> S.d -> unit) ~assert_can_receive_side =
       let eq_wrapper x eqx  =
@@ -186,10 +187,32 @@ module Narrow:S =
                 let start_value = HM.find_default data.narrow_globs_start_values y (S.Dom.bot()) in
                 S.Dom.join combined start_value
               in
+              let combined_side_elim_dead y =
+                if HM.mem data.narrow_globs_start_values 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 ())
+              in
+
               let y_oldval = HM.find rho y in
               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_globs_eliminate_cyclic_dead then
+                  combined_side_elim_dead y
                 else
                   combined_side y
               in

tests/regression/84-dividedsides/23-dead-side-effect-cycle.c

@@ -0,0 +1,33 @@
+// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable solvers.td3.narrow-globs.eliminate-dead  --enable solvers.td3.narrow-globs.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

@@ -47,6 +47,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)