Skip to content

Commit 215cb1d

Browse files
sim642sim642
authored
Merge pull request #1707 from goblint/tm-inv-transfer
Update 56-witness/*-tm-inv-tranfer* tests
2 parents 61390c4 + 28e40b9 commit 215cb1d

6 files changed

+132
-1140
lines changed

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

+2-13
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,20 @@
1-
// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 0 --enable ana.int.interval --set ana.base.privatization protection
1+
// PARAM: --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization protection
22
#include <pthread.h>
33
#include <goblint.h>
44

55
int g = 40; // matches expected precise read
66
pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
7-
pthread_mutex_t C = PTHREAD_MUTEX_INITIALIZER;
87

98
void *t_fun(void *arg) {
109
pthread_mutex_lock(&B);
11-
pthread_mutex_lock(&C);
1210
g = 42;
13-
pthread_mutex_unlock(&C);
14-
pthread_mutex_lock(&C);
1511
g = 41;
16-
pthread_mutex_unlock(&C);
1712
pthread_mutex_unlock(&B);
1813
return NULL;
1914
}
2015

2116
void *t_fun2(void *arg) {
22-
pthread_mutex_lock(&C);
2317
g = 41;
24-
pthread_mutex_unlock(&C);
2518
return NULL;
2619
}
2720

@@ -31,16 +24,12 @@ int main(void) {
3124
pthread_create(&id2, NULL, t_fun2, NULL);
3225

3326
pthread_mutex_lock(&B);
34-
pthread_mutex_lock(&C);
3527
__goblint_check(g >= 40);
3628
__goblint_check(g <= 41); // UNKNOWN (lacks expressivity)
37-
pthread_mutex_unlock(&C);
3829
pthread_mutex_unlock(&B);
3930

40-
pthread_mutex_lock(&C);
4131
__goblint_check(g >= 40);
42-
__goblint_check(g <= 42); // UNKNOWN (widen)
43-
pthread_mutex_unlock(&C);
32+
__goblint_check(g <= 42); // unknown with widening
4433

4534
return 0;
4635
}

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

+2-13
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,20 @@
1-
// PARAM: --set solvers.td3.side_widen always --enable ana.int.interval --set ana.base.privatization mine
1+
// PARAM: --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization mine
22
#include <pthread.h>
33
#include <goblint.h>
44

55
int g = 40; // matches expected precise read
66
pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
7-
pthread_mutex_t C = PTHREAD_MUTEX_INITIALIZER;
87

98
void *t_fun(void *arg) {
109
pthread_mutex_lock(&B);
11-
pthread_mutex_lock(&C);
1210
g = 42;
13-
pthread_mutex_unlock(&C);
14-
pthread_mutex_lock(&C);
1511
g = 41;
16-
pthread_mutex_unlock(&C);
1712
pthread_mutex_unlock(&B);
1813
return NULL;
1914
}
2015

2116
void *t_fun2(void *arg) {
22-
pthread_mutex_lock(&C);
2317
g = 41;
24-
pthread_mutex_unlock(&C);
2518
return NULL;
2619
}
2720

@@ -31,16 +24,12 @@ int main(void) {
3124
pthread_create(&id2, NULL, t_fun2, NULL);
3225

3326
pthread_mutex_lock(&B);
34-
pthread_mutex_lock(&C);
3527
__goblint_check(g >= 40);
3628
__goblint_check(g <= 41);
37-
pthread_mutex_unlock(&C);
3829
pthread_mutex_unlock(&B);
3930

40-
pthread_mutex_lock(&C);
41-
__goblint_check(g >= 40); // TODO why?
31+
__goblint_check(g >= 40); // unknown with widening
4232
__goblint_check(g <= 42);
43-
pthread_mutex_unlock(&C);
4433

4534
return 0;
4635
}

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

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
- entry_type: invariant_set
2+
metadata:
3+
format_version: "2.0"
4+
uuid: a3819e93-2ad6-42fd-aee8-f25aac0eb212
5+
creation_time: 2025-03-07T15:04:22Z
6+
producer:
7+
name: Vesal Vojdani
8+
version: n/a
9+
task:
10+
input_files:
11+
- 62-tm-inv-transfer-protection-witness.c
12+
input_file_hashes:
13+
62-tm-inv-transfer-protection-witness.c: 139627d4167e48c2399f0a6359e533d8ac7597e9b4155c58ddcb2b7bfe780088
14+
data_model: LP64
15+
language: C
16+
content:
17+
- invariant:
18+
type: location_invariant
19+
location:
20+
file_name: 62-tm-inv-transfer-protection-witness.c
21+
line: 27
22+
column: 3
23+
function: main
24+
value: 40 <= g && g <= 41
25+
format: c_expression
26+
- invariant:
27+
type: location_invariant
28+
location:
29+
file_name: 62-tm-inv-transfer-protection-witness.c
30+
line: 31
31+
column: 3
32+
function: main
33+
value: 40 <= g && g <= 42
34+
format: c_expression

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

+1-12
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,20 @@
1-
// 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
1+
// 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
22
#include <pthread.h>
33
#include <goblint.h>
44

55
int g = 40; // matches expected precise read
66
pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
7-
pthread_mutex_t C = PTHREAD_MUTEX_INITIALIZER;
87

98
void *t_fun(void *arg) {
109
pthread_mutex_lock(&B);
11-
pthread_mutex_lock(&C);
1210
g = 42;
13-
pthread_mutex_unlock(&C);
14-
pthread_mutex_lock(&C);
1511
g = 41;
16-
pthread_mutex_unlock(&C);
1712
pthread_mutex_unlock(&B);
1813
return NULL;
1914
}
2015

2116
void *t_fun2(void *arg) {
22-
pthread_mutex_lock(&C);
2317
g = 41;
24-
pthread_mutex_unlock(&C);
2518
return NULL;
2619
}
2720

@@ -31,16 +24,12 @@ int main(void) {
3124
pthread_create(&id2, NULL, t_fun2, NULL);
3225

3326
pthread_mutex_lock(&B);
34-
pthread_mutex_lock(&C);
3527
__goblint_check(g >= 40);
3628
__goblint_check(g <= 41); // UNKNOWN (lacks expressivity)
37-
pthread_mutex_unlock(&C);
3829
pthread_mutex_unlock(&B);
3930

40-
pthread_mutex_lock(&C);
4131
__goblint_check(g >= 40);
4232
__goblint_check(g <= 42);
43-
pthread_mutex_unlock(&C);
4433

4534
return 0;
4635
}

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

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
Same as regression test, but with manually written witness from Simmo's PhD thesis:
2+
3+
$ 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
4+
[Info][Witness] unassume invariant: 40 <= g && g <= 41 (62-tm-inv-transfer-protection-witness.c:26:3-26:25)
5+
[Success][Assert] Assertion "g >= 40" will succeed (62-tm-inv-transfer-protection-witness.c:27:3-27:27)
6+
[Warning][Assert] Assertion "g <= 41" is unknown. (62-tm-inv-transfer-protection-witness.c:28:3-28:27)
7+
[Info][Witness] unassume invariant: 40 <= g && g <= 42 (62-tm-inv-transfer-protection-witness.c:29:3-29:27)
8+
[Success][Assert] Assertion "g >= 40" will succeed (62-tm-inv-transfer-protection-witness.c:31:3-31:27)
9+
[Success][Assert] Assertion "g <= 42" will succeed (62-tm-inv-transfer-protection-witness.c:32:3-32:27)
10+
[Info][Deadcode] Logical lines of code (LLoC) summary:
11+
live: 19
12+
dead: 0
13+
total lines: 19
14+
[Warning][Race] Memory location g (race with conf. 110): (62-tm-inv-transfer-protection-witness.c:5:5-5:11)
15+
write with [lock:{B}, thread:[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40]] (conf. 110) (exp: & g) (62-tm-inv-transfer-protection-witness.c:10:3-10:9)
16+
write with [lock:{B}, thread:[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40]] (conf. 110) (exp: & g) (62-tm-inv-transfer-protection-witness.c:11:3-11:9)
17+
write with thread:[main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42] (conf. 110) (exp: & g) (62-tm-inv-transfer-protection-witness.c:17:3-17:9)
18+
read with [mhp:{created={[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40], [main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42]}}, lock:{B}, thread:[main]] (conf. 110) (exp: & g) (62-tm-inv-transfer-protection-witness.c:27:3-27:27)
19+
read with [mhp:{created={[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40], [main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42]}}, lock:{B}, thread:[main]] (conf. 110) (exp: & g) (62-tm-inv-transfer-protection-witness.c:28:3-28:27)
20+
read with [mhp:{created={[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40], [main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42]}}, thread:[main]] (conf. 110) (exp: & g) (62-tm-inv-transfer-protection-witness.c:31:3-31:27)
21+
read with [mhp:{created={[main, t_fun@62-tm-inv-transfer-protection-witness.c:23:3-23:40], [main, t_fun2@62-tm-inv-transfer-protection-witness.c:24:3-24:42]}}, thread:[main]] (conf. 110) (exp: & g) (62-tm-inv-transfer-protection-witness.c:32:3-32:27)
22+
[Info][Race] Memory locations race summary:
23+
safe: 0
24+
vulnerable: 0
25+
unsafe: 1
26+
total memory locations: 1
27+

0 commit comments

Comments
 (0)