Skip to content

Commit be58114

Browse files
tautschnigtautschnig
committed
Add regression tests from goto-instrument-wmm-full.tgz
Make all regression tests from the archive available (yet marking them as THOROUGH or KNOWNBUG to avoid including them by default). This avoids having an unused archive file bit-rotting in the repository. This commit was generated as follows: ``` set -e cd regression/goto-instrument-wmm-core/ tar xzf ../goto-instrument-wmm-full.tgz --strip-components=1 for f in $(tar tzf ../goto-instrument-wmm-full.tgz | sed 's#^goto-instrument-wmm-full/##') do [ -f $f ] || continue if git status --porcelain $f | grep -q '^?' then if [[ $(basename $f) == "test.desc" ]] then sed -i '1s/^CORE$/THOROUGH/' $f if ! grep -q EXIT $f then if grep -q "VERIFICATION FAILED" $f then sed -i '/SIGNAL=0/ i ^EXIT=10$' $f else sed -i '/SIGNAL=0/ i ^EXIT=0$' $f fi fi elif [[ $f =~ \.c$ ]] then clang-format -i $f fi git add $f else git checkout -- $f fi done git rm ../goto-instrument-wmm-full.tgz git commit -F - <<EOF Add regression tests from goto-instrument-wmm-full.tgz Make all regression tests from the archive available (yet marking them as THOROUGH or KNOWNBUG to avoid including them by default). This avoids having an unused archive file bit-rotting in the repository. This commit was generated as follows: \`\`\` $(<../../script.sh) \`\`\` EOF ```
1 parent d1da518 commit be58114

File tree

9,439 files changed

+371401
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

9,439 files changed

+371401
-0
lines changed

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_CAV11_ERROR/aclwdrr000.c

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
void fence()
2+
{
3+
asm("sync");
4+
}
5+
void lwfence()
6+
{
7+
asm("lwsync");
8+
}
9+
void isync()
10+
{
11+
asm("isync");
12+
}
13+
14+
int __unbuffered_cnt = 0;
15+
int __unbuffered_p0_r1 = 0;
16+
int __unbuffered_p0_r3 = 0;
17+
int __unbuffered_p1_r1 = 0;
18+
int __unbuffered_p2_r1 = 0;
19+
int __unbuffered_p2_r3 = 0;
20+
int x = 0;
21+
int y = 0;
22+
23+
void *P0(void *arg)
24+
{
25+
__unbuffered_p0_r1 = 1;
26+
y = __unbuffered_p0_r1;
27+
fence();
28+
__unbuffered_p0_r3 = 1;
29+
x = __unbuffered_p0_r3;
30+
// Instrumentation for CPROVER
31+
fence();
32+
__unbuffered_cnt++;
33+
}
34+
35+
void *P1(void *arg)
36+
{
37+
__unbuffered_p1_r1 = 2;
38+
x = __unbuffered_p1_r1;
39+
// Instrumentation for CPROVER
40+
fence();
41+
__unbuffered_cnt++;
42+
}
43+
44+
void *P2(void *arg)
45+
{
46+
__unbuffered_p2_r1 = x;
47+
lwfence();
48+
__unbuffered_p2_r3 = y;
49+
// Instrumentation for CPROVER
50+
fence();
51+
__unbuffered_cnt++;
52+
}
53+
54+
int main()
55+
{
56+
__CPROVER_ASYNC_0:
57+
P0(0);
58+
__CPROVER_ASYNC_1:
59+
P1(0);
60+
__CPROVER_ASYNC_2:
61+
P2(0);
62+
__CPROVER_assume(__unbuffered_cnt == 3);
63+
fence();
64+
// EXPECT:exists
65+
__CPROVER_assert(
66+
!(x == 2 && __unbuffered_p2_r1 == 2 && __unbuffered_p2_r3 == 0),
67+
"Program proven to be relaxed for PPC, model checker says YES.");
68+
return 0;
69+
}

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_CAV11_ERROR/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
aclwdrr000.c
3+
CAV11 ERROR
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_POWER_ALL/aclwdrr000.c

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
void fence()
2+
{
3+
asm("sync");
4+
}
5+
void lwfence()
6+
{
7+
asm("lwsync");
8+
}
9+
void isync()
10+
{
11+
asm("isync");
12+
}
13+
14+
int __unbuffered_cnt = 0;
15+
int __unbuffered_p0_r1 = 0;
16+
int __unbuffered_p0_r3 = 0;
17+
int __unbuffered_p1_r1 = 0;
18+
int __unbuffered_p2_r1 = 0;
19+
int __unbuffered_p2_r3 = 0;
20+
int x = 0;
21+
int y = 0;
22+
23+
void *P0(void *arg)
24+
{
25+
__unbuffered_p0_r1 = 1;
26+
y = __unbuffered_p0_r1;
27+
fence();
28+
__unbuffered_p0_r3 = 1;
29+
x = __unbuffered_p0_r3;
30+
// Instrumentation for CPROVER
31+
fence();
32+
__unbuffered_cnt++;
33+
}
34+
35+
void *P1(void *arg)
36+
{
37+
__unbuffered_p1_r1 = 2;
38+
x = __unbuffered_p1_r1;
39+
// Instrumentation for CPROVER
40+
fence();
41+
__unbuffered_cnt++;
42+
}
43+
44+
void *P2(void *arg)
45+
{
46+
__unbuffered_p2_r1 = x;
47+
lwfence();
48+
__unbuffered_p2_r3 = y;
49+
// Instrumentation for CPROVER
50+
fence();
51+
__unbuffered_cnt++;
52+
}
53+
54+
int main()
55+
{
56+
__CPROVER_ASYNC_0:
57+
P0(0);
58+
__CPROVER_ASYNC_1:
59+
P1(0);
60+
__CPROVER_ASYNC_2:
61+
P2(0);
62+
__CPROVER_assume(__unbuffered_cnt == 3);
63+
fence();
64+
// EXPECT:exists
65+
__CPROVER_assert(
66+
!(x == 2 && __unbuffered_p2_r1 == 2 && __unbuffered_p2_r3 == 0),
67+
"Program proven to be relaxed for PPC, model checker says YES.");
68+
return 0;
69+
}

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_POWER_ALL/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
THOROUGH
2+
aclwdrr000.c
3+
POWER ALL
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_POWER_OPC/aclwdrr000.c

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
void fence()
2+
{
3+
asm("sync");
4+
}
5+
void lwfence()
6+
{
7+
asm("lwsync");
8+
}
9+
void isync()
10+
{
11+
asm("isync");
12+
}
13+
14+
int __unbuffered_cnt = 0;
15+
int __unbuffered_p0_r1 = 0;
16+
int __unbuffered_p0_r3 = 0;
17+
int __unbuffered_p1_r1 = 0;
18+
int __unbuffered_p2_r1 = 0;
19+
int __unbuffered_p2_r3 = 0;
20+
int x = 0;
21+
int y = 0;
22+
23+
void *P0(void *arg)
24+
{
25+
__unbuffered_p0_r1 = 1;
26+
y = __unbuffered_p0_r1;
27+
fence();
28+
__unbuffered_p0_r3 = 1;
29+
x = __unbuffered_p0_r3;
30+
// Instrumentation for CPROVER
31+
fence();
32+
__unbuffered_cnt++;
33+
}
34+
35+
void *P1(void *arg)
36+
{
37+
__unbuffered_p1_r1 = 2;
38+
x = __unbuffered_p1_r1;
39+
// Instrumentation for CPROVER
40+
fence();
41+
__unbuffered_cnt++;
42+
}
43+
44+
void *P2(void *arg)
45+
{
46+
__unbuffered_p2_r1 = x;
47+
lwfence();
48+
__unbuffered_p2_r3 = y;
49+
// Instrumentation for CPROVER
50+
fence();
51+
__unbuffered_cnt++;
52+
}
53+
54+
int main()
55+
{
56+
__CPROVER_ASYNC_0:
57+
P0(0);
58+
__CPROVER_ASYNC_1:
59+
P1(0);
60+
__CPROVER_ASYNC_2:
61+
P2(0);
62+
__CPROVER_assume(__unbuffered_cnt == 3);
63+
fence();
64+
// EXPECT:exists
65+
__CPROVER_assert(
66+
!(x == 2 && __unbuffered_p2_r1 == 2 && __unbuffered_p2_r3 == 0),
67+
"Program proven to be relaxed for PPC, model checker says YES.");
68+
return 0;
69+
}

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_POWER_OPC/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
THOROUGH
2+
aclwdrr000.c
3+
POWER OPC
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_POWER_OPT/aclwdrr000.c

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
void fence()
2+
{
3+
asm("sync");
4+
}
5+
void lwfence()
6+
{
7+
asm("lwsync");
8+
}
9+
void isync()
10+
{
11+
asm("isync");
12+
}
13+
14+
int __unbuffered_cnt = 0;
15+
int __unbuffered_p0_r1 = 0;
16+
int __unbuffered_p0_r3 = 0;
17+
int __unbuffered_p1_r1 = 0;
18+
int __unbuffered_p2_r1 = 0;
19+
int __unbuffered_p2_r3 = 0;
20+
int x = 0;
21+
int y = 0;
22+
23+
void *P0(void *arg)
24+
{
25+
__unbuffered_p0_r1 = 1;
26+
y = __unbuffered_p0_r1;
27+
fence();
28+
__unbuffered_p0_r3 = 1;
29+
x = __unbuffered_p0_r3;
30+
// Instrumentation for CPROVER
31+
fence();
32+
__unbuffered_cnt++;
33+
}
34+
35+
void *P1(void *arg)
36+
{
37+
__unbuffered_p1_r1 = 2;
38+
x = __unbuffered_p1_r1;
39+
// Instrumentation for CPROVER
40+
fence();
41+
__unbuffered_cnt++;
42+
}
43+
44+
void *P2(void *arg)
45+
{
46+
__unbuffered_p2_r1 = x;
47+
lwfence();
48+
__unbuffered_p2_r3 = y;
49+
// Instrumentation for CPROVER
50+
fence();
51+
__unbuffered_cnt++;
52+
}
53+
54+
int main()
55+
{
56+
__CPROVER_ASYNC_0:
57+
P0(0);
58+
__CPROVER_ASYNC_1:
59+
P1(0);
60+
__CPROVER_ASYNC_2:
61+
P2(0);
62+
__CPROVER_assume(__unbuffered_cnt == 3);
63+
fence();
64+
// EXPECT:exists
65+
__CPROVER_assert(
66+
!(x == 2 && __unbuffered_p2_r1 == 2 && __unbuffered_p2_r3 == 0),
67+
"Program proven to be relaxed for PPC, model checker says YES.");
68+
return 0;
69+
}

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_POWER_OPT/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
THOROUGH
2+
aclwdrr000.c
3+
POWER OPT
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_PSO_ALL/aclwdrr000.c

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
void fence()
2+
{
3+
asm("sync");
4+
}
5+
void lwfence()
6+
{
7+
asm("lwsync");
8+
}
9+
void isync()
10+
{
11+
asm("isync");
12+
}
13+
14+
int __unbuffered_cnt = 0;
15+
int __unbuffered_p0_r1 = 0;
16+
int __unbuffered_p0_r3 = 0;
17+
int __unbuffered_p1_r1 = 0;
18+
int __unbuffered_p2_r1 = 0;
19+
int __unbuffered_p2_r3 = 0;
20+
int x = 0;
21+
int y = 0;
22+
23+
void *P0(void *arg)
24+
{
25+
__unbuffered_p0_r1 = 1;
26+
y = __unbuffered_p0_r1;
27+
fence();
28+
__unbuffered_p0_r3 = 1;
29+
x = __unbuffered_p0_r3;
30+
// Instrumentation for CPROVER
31+
fence();
32+
__unbuffered_cnt++;
33+
}
34+
35+
void *P1(void *arg)
36+
{
37+
__unbuffered_p1_r1 = 2;
38+
x = __unbuffered_p1_r1;
39+
// Instrumentation for CPROVER
40+
fence();
41+
__unbuffered_cnt++;
42+
}
43+
44+
void *P2(void *arg)
45+
{
46+
__unbuffered_p2_r1 = x;
47+
lwfence();
48+
__unbuffered_p2_r3 = y;
49+
// Instrumentation for CPROVER
50+
fence();
51+
__unbuffered_cnt++;
52+
}
53+
54+
int main()
55+
{
56+
__CPROVER_ASYNC_0:
57+
P0(0);
58+
__CPROVER_ASYNC_1:
59+
P1(0);
60+
__CPROVER_ASYNC_2:
61+
P2(0);
62+
__CPROVER_assume(__unbuffered_cnt == 3);
63+
fence();
64+
// EXPECT:exists
65+
__CPROVER_assert(
66+
!(x == 2 && __unbuffered_p2_r1 == 2 && __unbuffered_p2_r3 == 0),
67+
"Program proven to be relaxed for PPC, model checker says YES.");
68+
return 0;
69+
}

‎regression/goto-instrument-wmm-core/ppc_aclwdrr000_PSO_ALL/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
THOROUGH
2+
aclwdrr000.c
3+
PSO ALL
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)