Skip to content

Commit c923c3d

Browse files
tautschnigtautschnig
authored
Merge pull request #5937 from tautschnig/wmm-tests
Enable regression tests of weak memory model instrumentation
2 parents e010007 + 947b913 commit c923c3d

File tree

9,567 files changed

+371702
-144
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,567 files changed

+371702
-144
lines changed

‎regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ add_subdirectory(cbmc-incr-oneloop)
3535
add_subdirectory(cbmc-incr)
3636
add_subdirectory(cbmc-with-incr)
3737
add_subdirectory(array-refinement-with-incr)
38+
add_subdirectory(goto-instrument-wmm-core)
3839
add_subdirectory(goto-instrument-typedef)
3940
add_subdirectory(smt2_solver)
4041
add_subdirectory(smt2_strings)

‎regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ DIRS = cbmc \
1313
cbmc-incr \
1414
cbmc-with-incr \
1515
array-refinement-with-incr \
16+
goto-instrument-wmm-core \
1617
goto-instrument-typedef \
1718
smt2_solver \
1819
smt2_strings \

‎regression/goto-instrument-wmm-core/CMakeLists.txt

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
if(WIN32)
2+
set(is_windows true)
3+
else()
4+
set(is_windows false)
5+
endif()
6+
7+
add_test_pl_tests(
8+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}" -X glpk
9+
)

‎regression/goto-instrument-wmm-core/Makefile

Lines changed: 23 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,40 @@
11
default: tests.log
22

3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
is_windows=true
9+
else
10+
exe=../../../src/goto-cc/goto-cc
11+
is_windows=false
12+
endif
13+
314
testalpha:
4-
@../test.pl -c ../chain.sh -C
15+
@../test.pl -C -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
516

617
testbeta:
7-
@../test.pl -c ../chain.sh -T
18+
@../test.pl -T -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
819

920
testimpr:
10-
@../test.pl -c ../chain.sh -K
21+
@../test.pl -K -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
1122

1223
testnew:
13-
@../test.pl -c ../chain.sh -F
24+
@../test.pl -F -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
1425

1526
test:
16-
@../test.pl -c ../chain.sh
27+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
1728

18-
tests.log: ../test.pl
19-
@../test.pl -c ../chain.sh
29+
tests.log:
30+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X glpk
2031

2132
clean:
22-
@for dir in *; do \
23-
if [ -d "$$dir" ]; then \
24-
$(RM) $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
25-
fi; \
26-
done;
33+
find . -name '*.out' -execdir $(RM) '{}' \;
34+
find . -name '*.gb' -execdir $(RM) '{}' \;
35+
find . -name '*.dot' -execdir $(RM) '{}' \;
36+
find . -mindepth 2 -name '*.txt' -execdir $(RM) '{}' \;
37+
$(RM) tests.log
2738

2839
show:
2940
@for dir in *; do \

‎regression/goto-instrument-wmm-core/chain.sh

Lines changed: 17 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
11
#!/bin/bash
22

3-
src=../../../src
4-
goto_cc=$src/goto-cc/goto-cc
5-
goto_instrument=$src/goto-instrument/goto-instrument
6-
cbmc=$src/cbmc/cbmc
3+
set -e
4+
5+
goto_cc=$1
6+
goto_instrument=$2
7+
cbmc=$3
8+
is_windows=$4
9+
10+
shift 4
711

812
function usage() {
913
echo "Usage: chain architecture [strategy] test_file.c"
@@ -24,8 +28,8 @@ else
2428
usage
2529
fi
2630

27-
arch=${arch,,}
28-
strategy=${strategy,,}
31+
arch=$(echo $arch | tr A-Z a-z)
32+
strategy=$(echo $strategy | tr A-Z a-z)
2933

3034
if [[ "tso|pso|rmo|power|arm|sc|cav11|" =~ "$arch|" ]]
3135
then
@@ -54,6 +58,10 @@ else
5458
flag=
5559
fi
5660

57-
timeout 180.0s $goto_cc -o $name.gb $name.c
58-
timeout 180.0s $goto_instrument $flag $name.gb ${name}_$arch.gb $strat
59-
timeout 180.0s $cbmc ${name}_$arch.gb
61+
if [[ "${is_windows}" == "true" ]]; then
62+
$goto_cc "${name}.c" "/Fe${name}.gb"
63+
else
64+
$goto_cc -o "${name}.gb" "${name}.c"
65+
fi
66+
perl -e 'alarm shift @ARGV; exec @ARGV' 180 "$goto_instrument" $flag "$name.gb" "${name}_$arch.gb" $strat
67+
perl -e 'alarm shift @ARGV; exec @ARGV' 180 "$cbmc" "${name}_$arch.gb"

‎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+
KNOWNBUG
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+
KNOWNBUG
2+
aclwdrr000.c
3+
POWER OPC
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)