Enable cbmc-concurrency regression tests by default

For some reason we had not included these in our standard set of regression
tests, and sure enough they got out of sync and one actual regression happened.

Author: tautschnig

regression/CMakeLists.txt

@@ -29,6 +29,7 @@ add_subdirectory(goto-analyzer)
 add_subdirectory(ansi-c)
 add_subdirectory(goto-instrument)
 add_subdirectory(cpp)
+add_subdirectory(cbmc-concurrency)
 add_subdirectory(cbmc-cover)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(smt2_solver)

regression/Makefile

@@ -7,6 +7,7 @@ DIRS = cbmc \
        ansi-c \
        goto-instrument \
        cpp \
+       cbmc-concurrency \
        cbmc-cover \
        goto-instrument-typedef \
        smt2_solver \

regression/cbmc-concurrency/CMakeLists.txt

@@ -0,0 +1,13 @@
+if(NOT WIN32)
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)
+else()
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+    "cbmc-concurrency"
+    "$<TARGET_FILE:cbmc>"
+    "-C;-X;pthread"
+    "CORE"
+)
+endif()

regression/cbmc-concurrency/Makefile

@@ -1,10 +1,17 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	no_pthread = -X pthread
+endif
+
 test:
-	@../test.pl -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
 
 tests.log: ../test.pl
-	@../test.pl -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
 
 show:
 	@for dir in *; do \

regression/cbmc-concurrency/atomic_section_sc6/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
 
-^EXIT=10$
+^EXIT=6$
 ^SIGNAL=0$
-^file main.c line 12 function spawn: start_thread in atomic section detected$
+^spawning threads out of atomic sections is not allowed
 --
 ^warning: ignoring

regression/cbmc-concurrency/conditional_spawn1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$

regression/cbmc-concurrency/deadlock1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/deadlock2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$

regression/cbmc-concurrency/malloc1/main.c

@@ -1,5 +1,4 @@
 #include <stdlib.h>
-#include <pthread.h>
 
 #define BUG
 
@@ -13,12 +12,9 @@ void* set_x(void* arg) {
 }
 
 int main() {
-  pthread_t thread;
   x = malloc(sizeof(int));
   #ifdef BUG
   __CPROVER_ASYNC_1: set_x(NULL);
-  //pthread_create(&thread,NULL,set_x,NULL);
-  //pthread_join(thread,NULL);
   __CPROVER_assume(set_done);
   #else
   set_x(NULL);

regression/cbmc-concurrency/malloc2/main.c

@@ -1,5 +1,4 @@
 #include <stdlib.h>
-#include <pthread.h>
 
 _Bool set_done;
 int *ptr;

regression/cbmc-concurrency/memory_barrier1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --unwind 1 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-concurrency/memory_barrier2/main.c

@@ -9,7 +9,11 @@ volatile int flag1 = 0, flag2 = 0; // boolean flags
 void* thr1(void * arg) { // frontend produces 12 transitions from this thread. It would be better if it would produce only 8!
   flag1 = 1;
   turn = 1;
+#ifdef __GNUC__
   __asm__ __volatile__ ("mfence": : :"memory");
+#else
+  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
+#endif
   __CPROVER_assume(! (flag2==1 && turn==1) );
   // begin: critical section
   x = 0;
@@ -21,7 +25,11 @@ void* thr1(void * arg) { // frontend produces 12 transitions from this thread. I
 void* thr2(void * arg) {
   flag2 = 1;
   turn = 0;
+#ifdef __GNUC__
   __asm__ __volatile__ ("mfence": : :"memory");
+#else
+  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
+#endif
   __CPROVER_assume(! (flag1==1 && turn==0) );
   // begin: critical section
   x = 1;

regression/cbmc-concurrency/memory_barrier2/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --mm tso
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Some past change broke this test such that we now report verification failures.

regression/cbmc-concurrency/mutex2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 -DMUTEX
 ^EXIT=0$

regression/cbmc-concurrency/norace_array1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/norace_array2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/norace_scalar1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/norace_struct1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/pthread_create_tso1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --mm tso
 ^EXIT=0$

regression/cbmc-concurrency/pthread_join1/test.desc

@@ -1,10 +1,10 @@
-CORE
+CORE pthread
 main.c
 --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.1\] assertion i==1: FAILURE$
-^\[main\.assertion\.2\] assertion i==2: SUCCESS$
+^\[main\.assertion\.1\] line 21 assertion i==1: FAILURE$
+^\[main\.assertion\.2\] line 22 assertion i==2: SUCCESS$
 ^\*\* 1 of 2 failed 
 --
 ^warning: ignoring

regression/cbmc-concurrency/pthread_join2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --unwind 2
 ^EXIT=10$

regression/cbmc-concurrency/sc6/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --error-label ERROR
 ^EXIT=0$

regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --error-label ERROR
 ^EXIT=10$

regression/cbmc-concurrency/thread_chain_posix1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$

regression/cbmc-concurrency/thread_chain_posix2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 -D_ENABLE_CHAIN_ --unwind 2
 ^EXIT=0$

regression/cbmc-concurrency/thread_chain_posix3/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 -D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2
 ^EXIT=10$

regression/cbmc-concurrency/thread_local1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/trace1/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^[[:space:]]*r2=1u \(.*\)$
+^[[:space:]]*r2=1u(l)? \(.*\)$
 --
 ^warning: ignoring

regression/cbmc-concurrency/uf_with_threads1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$