Option to only destabilize access globals (instead of following all side-effects) after re-setting them to bottom

src/solvers/td3.ml

@@ -131,6 +131,8 @@ module WP =
       (* If true, incremental side-effected var restart will only restart destabilized globals (using hack).
          If false, it will restart all destabilized side-effected vars. *)
       let restart_only_globals = GobConfig.get_bool "incremental.restart.sided.only-global" in
+      let restart_only_access = GobConfig.get_bool "incremental.restart.sided.only-access" in
+      let restart_destab_with_sides = GobConfig.get_bool "incremental.restart.sided.destab-with-sides" in
 
       (* If true, wpoint will be restarted to bot when added.
          This allows incremental to avoid reusing and republishing imprecise local values due to globals (which get restarted). *)
@@ -580,7 +582,14 @@ 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)) && not (S.Var.is_write_only x) then (
+          let should_restart =
+            if restart_only_access then
+              S.Var.is_write_only x
+            else
+              (not restart_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec)) && (not (S.Var.is_write_only x))
+          in
+
+          if not (VS.is_empty w) && should_restart then (
             (* restart side-effected var *)
             restart_leaf x;
 
@@ -593,7 +602,10 @@ module WP =
                 if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
                 HM.remove stable y;
                 HM.remove superstable y;
-                destabilize_with_side ~front:false y
+                if restart_destab_with_sides then
+                  destabilize_with_side ~front:false y
+                else
+                  destabilize_normal ~front:false y
               ) w
           );
 

src/util/options.schema.json

@@ -1050,6 +1050,18 @@
                   "description": "TODO",
                   "type": "boolean",
                   "default": false
+                },
+                "only-access" : {
+                  "title" : "incremental.restart.sided.only-access",
+                  "description" : "TODO",
+                  "type" : "boolean",
+                  "default" : false
+                },
+                "destab-with-sides": {
+                  "title" : "incremental.restart.sided.destab-with-sides",
+                  "description" : "TODO",
+                  "type" : "boolean",
+                  "default" : true
                 }
               },
               "additionalProperties": false

tests/incremental/11-restart/12-mutex-simple-access.c

@@ -0,0 +1,24 @@
+// Same as 13-restart-write/01-mutex-simple
+#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;
+}

tests/incremental/11-restart/12-mutex-simple-access.json

@@ -0,0 +1,11 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": true,
+                "only-access": true,
+                "destab-with-sides": false
+            }
+        }
+    }
+}

tests/incremental/11-restart/12-mutex-simple-access.patch

@@ -0,0 +1,24 @@
+--- tests/incremental/11-restart/12-mutex-simple-access.c
++++ tests/incremental/11-restart/12-mutex-simple-access.c
+@@ -8,7 +8,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;
+ }
+@@ -16,9 +16,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;
+ }