Update 56-witness/*-tm-inv-tranfer* tests

tests/regression/56-witness/60-tm-inv-transfer-protection.c

@@ -1,27 +1,20 @@
-// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 0 --enable ana.int.interval --set ana.base.privatization protection
+// PARAM: --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization protection
 #include <pthread.h>
 #include <goblint.h>
 
 int g = 40; // matches expected precise read
 pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t C = PTHREAD_MUTEX_INITIALIZER;
 
 void *t_fun(void *arg) {
   pthread_mutex_lock(&B);
-  pthread_mutex_lock(&C);
   g = 42;
-  pthread_mutex_unlock(&C);
-  pthread_mutex_lock(&C);
   g = 41;
-  pthread_mutex_unlock(&C);
   pthread_mutex_unlock(&B);
   return NULL;
 }
 
 void *t_fun2(void *arg) {
-  pthread_mutex_lock(&C);
   g = 41;
-  pthread_mutex_unlock(&C);
   return NULL;
 }
 
@@ -31,16 +24,12 @@ int main(void) {
   pthread_create(&id2, NULL, t_fun2, NULL);
 
   pthread_mutex_lock(&B);
-  pthread_mutex_lock(&C);
   __goblint_check(g >= 40);
   __goblint_check(g <= 41); // UNKNOWN (lacks expressivity)
-  pthread_mutex_unlock(&C);
   pthread_mutex_unlock(&B);
 
-  pthread_mutex_lock(&C);
   __goblint_check(g >= 40);
-  __goblint_check(g <= 42); // UNKNOWN (widen)
-  pthread_mutex_unlock(&C);
+  __goblint_check(g <= 42); // unknown with widening
 
   return 0;
 }

tests/regression/56-witness/61-tm-inv-transfer-mine.c

@@ -1,27 +1,20 @@
-// PARAM: --set solvers.td3.side_widen always --enable ana.int.interval --set ana.base.privatization mine
+// PARAM: --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization mine
 #include <pthread.h>
 #include <goblint.h>
 
 int g = 40; // matches expected precise read
 pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t C = PTHREAD_MUTEX_INITIALIZER;
 
 void *t_fun(void *arg) {
   pthread_mutex_lock(&B);
-  pthread_mutex_lock(&C);
   g = 42;
-  pthread_mutex_unlock(&C);
-  pthread_mutex_lock(&C);
   g = 41;
-  pthread_mutex_unlock(&C);
   pthread_mutex_unlock(&B);
   return NULL;
 }
 
 void *t_fun2(void *arg) {
-  pthread_mutex_lock(&C);
   g = 41;
-  pthread_mutex_unlock(&C);
   return NULL;
 }
 
@@ -31,16 +24,12 @@ int main(void) {
   pthread_create(&id2, NULL, t_fun2, NULL);
 
   pthread_mutex_lock(&B);
-  pthread_mutex_lock(&C);
   __goblint_check(g >= 40);
   __goblint_check(g <= 41);
-  pthread_mutex_unlock(&C);
   pthread_mutex_unlock(&B);
 
-  pthread_mutex_lock(&C);
-  __goblint_check(g >= 40); // TODO why?
+  __goblint_check(g >= 40); // unknown with widening
   __goblint_check(g <= 42);
-  pthread_mutex_unlock(&C);
 
   return 0;
 }

tests/regression/56-witness/62-tm-inv-transfer-protection-witness-manual.yml

@@ -0,0 +1,34 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: a3819e93-2ad6-42fd-aee8-f25aac0eb212
+    creation_time: 2025-03-07T15:04:22Z
+    producer:
+      name: Vesal Vojdani
+      version: n/a
+    task:
+      input_files:
+      - 62-tm-inv-transfer-protection-witness.c
+      input_file_hashes:
+        62-tm-inv-transfer-protection-witness.c: 139627d4167e48c2399f0a6359e533d8ac7597e9b4155c58ddcb2b7bfe780088
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 62-tm-inv-transfer-protection-witness.c
+        line: 27
+        column: 3
+        function: main
+      value: 40 <= g && g <= 41
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 62-tm-inv-transfer-protection-witness.c
+        line: 31
+        column: 3
+        function: main
+      value: 40 <= g && g <= 42
+      format: c_expression

tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c

@@ -1,27 +1,20 @@
-// PARAM: --set solvers.td3.side_widen always --enable ana.int.interval --set ana.base.privatization protection --set "ana.activated[+]" unassume --set witness.yaml.unassume 62-tm-inv-transfer-protection-witness.yml --enable ana.widen.tokens
+// PARAM: --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization protection --set "ana.activated[+]" unassume --set witness.yaml.unassume 62-tm-inv-transfer-protection-witness.yml --enable ana.widen.tokens
 #include <pthread.h>
 #include <goblint.h>
 
 int g = 40; // matches expected precise read
 pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t C = PTHREAD_MUTEX_INITIALIZER;
 
 void *t_fun(void *arg) {
   pthread_mutex_lock(&B);
-  pthread_mutex_lock(&C);
   g = 42;
-  pthread_mutex_unlock(&C);
-  pthread_mutex_lock(&C);
   g = 41;
-  pthread_mutex_unlock(&C);
   pthread_mutex_unlock(&B);
   return NULL;
 }
 
 void *t_fun2(void *arg) {
-  pthread_mutex_lock(&C);
   g = 41;
-  pthread_mutex_unlock(&C);
   return NULL;
 }
 
@@ -31,16 +24,12 @@ int main(void) {
   pthread_create(&id2, NULL, t_fun2, NULL);
 
   pthread_mutex_lock(&B);
-  pthread_mutex_lock(&C);
   __goblint_check(g >= 40);
   __goblint_check(g <= 41); // UNKNOWN (lacks expressivity)
-  pthread_mutex_unlock(&C);
   pthread_mutex_unlock(&B);
 
-  pthread_mutex_lock(&C);
   __goblint_check(g >= 40);
   __goblint_check(g <= 42);
-  pthread_mutex_unlock(&C);
 
   return 0;
 }

tests/regression/56-witness/62-tm-inv-transfer-protection-witness.t

@@ -0,0 +1,27 @@
+Same as regression test, but with manually written witness from Simmo's PhD thesis:
+
+  $ goblint --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization protection --set "ana.activated[+]" unassume --set witness.yaml.unassume 62-tm-inv-transfer-protection-witness-manual.yml --enable ana.widen.tokens 62-tm-inv-transfer-protection-witness.c
+  [Info][Witness] unassume invariant: 40 <= g && g <= 41 (62-tm-inv-transfer-protection-witness.c:26:3-26:25)
+  [Success][Assert] Assertion "g >= 40" will succeed (62-tm-inv-transfer-protection-witness.c:27:3-27:27)
+  [Warning][Assert] Assertion "g <= 41" is unknown. (62-tm-inv-transfer-protection-witness.c:28:3-28:27)
+  [Info][Witness] unassume invariant: 40 <= g && g <= 42 (62-tm-inv-transfer-protection-witness.c:29:3-29:27)
+  [Success][Assert] Assertion "g >= 40" will succeed (62-tm-inv-transfer-protection-witness.c:31:3-31:27)
+  [Success][Assert] Assertion "g <= 42" will succeed (62-tm-inv-transfer-protection-witness.c:32:3-32:27)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 19
+    dead: 0
+    total lines: 19
+  [Warning][Race] Memory location g (race with conf. 110): (62-tm-inv-transfer-protection-witness.c:5:5-5:11)
+    write with [lock:{B}, thread:[main, [email protected]:23:3-23:40]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:10:3-10:9)
+    write with [lock:{B}, thread:[main, [email protected]:23:3-23:40]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:11:3-11:9)
+    write with thread:[main, [email protected]:24:3-24:42] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:17:3-17:9)
+    read with [mhp:{created={[main, [email protected]:23:3-23:40], [main, [email protected]:24:3-24:42]}}, lock:{B}, thread:[main]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:27:3-27:27)
+    read with [mhp:{created={[main, [email protected]:23:3-23:40], [main, [email protected]:24:3-24:42]}}, lock:{B}, thread:[main]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:28:3-28:27)
+    read with [mhp:{created={[main, [email protected]:23:3-23:40], [main, [email protected]:24:3-24:42]}}, thread:[main]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:31:3-31:27)
+    read with [mhp:{created={[main, [email protected]:23:3-23:40], [main, [email protected]:24:3-24:42]}}, thread:[main]] (conf. 110)  (exp: & g) (62-tm-inv-transfer-protection-witness.c:32:3-32:27)
+  [Info][Race] Memory locations race summary:
+    safe: 0
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 1
+