Merge pull request #4278 from tautschnig/enable-concurrency-tests

tautschnig · web-flow · commit af7124fc8306 · 2019-02-26T12:24:13.000Z
Enable cbmc-concurrency regression tests by default
diff --git a/regression/CMakeLists.txt b/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)
diff --git a/regression/Makefile b/regression/Makefile
@@ -7,6 +7,7 @@ DIRS = cbmc \
        ansi-c \
        goto-instrument \
        cpp \
+       cbmc-concurrency \
        cbmc-cover \
        goto-instrument-typedef \
        smt2_solver \
diff --git a/regression/cbmc-concurrency/CMakeLists.txt b/regression/cbmc-concurrency/CMakeLists.txt
@@ -0,0 +1,13 @@
+if((NOT WIN32) AND (NOT APPLE))
+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()
diff --git a/regression/cbmc-concurrency/Makefile b/regression/cbmc-concurrency/Makefile
@@ -1,10 +1,19 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(filter-out OSX MSVC,$(BUILD_ENV_)),)
+	# no POSIX threads on Windows
+	# for OSX we'd need sound handling of pointers in multi-threaded programs
+	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 \
diff --git a/regression/cbmc-concurrency/atomic_section_sc6/test.desc b/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
diff --git a/regression/cbmc-concurrency/conditional_spawn1/test.desc b/regression/cbmc-concurrency/conditional_spawn1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/deadlock1/test.desc b/regression/cbmc-concurrency/deadlock1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/deadlock2/test.desc b/regression/cbmc-concurrency/deadlock2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/malloc1/main.c b/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);
diff --git a/regression/cbmc-concurrency/malloc2/main.c b/regression/cbmc-concurrency/malloc2/main.c
@@ -1,5 +1,4 @@
 #include <stdlib.h>
-#include <pthread.h>
 
 _Bool set_done;
 int *ptr;
diff --git a/regression/cbmc-concurrency/memory_barrier1/test.desc b/regression/cbmc-concurrency/memory_barrier1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --unwind 1 --no-unwinding-assertions
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/memory_barrier2/main.c b/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;
diff --git a/regression/cbmc-concurrency/memory_barrier2/test.desc b/regression/cbmc-concurrency/memory_barrier2/test.desc
@@ -6,3 +6,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Some past change broke this test such that we now report verification failures.
diff --git a/regression/cbmc-concurrency/mutex2/test.desc b/regression/cbmc-concurrency/mutex2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 -DMUTEX
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_array1/test.desc b/regression/cbmc-concurrency/norace_array1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_array2/test.desc b/regression/cbmc-concurrency/norace_array2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_scalar1/test.desc b/regression/cbmc-concurrency/norace_scalar1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_struct1/test.desc b/regression/cbmc-concurrency/norace_struct1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/pthread_create_tso1/test.desc b/regression/cbmc-concurrency/pthread_create_tso1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --mm tso
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/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
diff --git a/regression/cbmc-concurrency/pthread_join2/test.desc b/regression/cbmc-concurrency/pthread_join2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --unwind 2
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/sc6/test.desc b/regression/cbmc-concurrency/sc6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc b/regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --error-label ERROR
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc b/regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 --error-label ERROR
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/thread_chain_posix1/test.desc b/regression/cbmc-concurrency/thread_chain_posix1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc-concurrency/thread_chain_posix2/test.desc b/regression/cbmc-concurrency/thread_chain_posix2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG pthread
 main.c
 -D_ENABLE_CHAIN_ --unwind 2
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/thread_chain_posix3/test.desc b/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$
diff --git a/regression/cbmc-concurrency/thread_local1/test.desc b/regression/cbmc-concurrency/thread_local1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/trace1/test.desc b/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
diff --git a/regression/cbmc-concurrency/uf_with_threads1/test.desc b/regression/cbmc-concurrency/uf_with_threads1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -1065,15 +1065,14 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    goto_programt::targett t=dest.add_instruction(OTHER);
-    t->source_location=function.source_location();
-    t->code.set(ID_statement, ID_fence);
-
+    codet fence(ID_fence);
     forall_expr(it, arguments)
     {
       const irep_idt kind=get_string_constant(*it);
-      t->code.set(kind, true);
+      fence.set(kind, true);
     }
+
+    dest.add(goto_programt::make_other(fence, function.source_location()));
   }
   else if(identifier=="__builtin_prefetch")
   {
@@ -1268,10 +1267,9 @@ void goto_convertt::do_function_call_symbol(
     t3->code=code_assignt(deref_ptr, op_expr);
 
     // this instruction implies an mfence, i.e., WRfence
-    goto_programt::targett t4=dest.add_instruction(OTHER);
-    t4->source_location=function.source_location();
-    t4->code=codet(ID_fence);
-    t4->code.set(ID_WRfence, true);
+    codet fence(ID_fence);
+    fence.set(ID_WRfence, true);
+    dest.add(goto_programt::make_other(fence, function.source_location()));
 
     goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
     t5->source_location=function.source_location();
@@ -1339,10 +1337,9 @@ void goto_convertt::do_function_call_symbol(
     }
 
     // this instruction implies an mfence, i.e., WRfence
-    goto_programt::targett t4=dest.add_instruction(OTHER);
-    t4->source_location=function.source_location();
-    t4->code=codet(ID_fence);
-    t4->code.set(ID_WRfence, true);
+    codet fence(ID_fence);
+    fence.set(ID_WRfence, true);
+    dest.add(goto_programt::make_other(fence, function.source_location()));
 
     goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
     t5->source_location=function.source_location();
@@ -1410,10 +1407,9 @@ void goto_convertt::do_function_call_symbol(
     t3->code=code_assignt(deref_ptr, if_expr);
 
     // this instruction implies an mfence, i.e., WRfence
-    goto_programt::targett t4=dest.add_instruction(OTHER);
-    t4->source_location=function.source_location();
-    t4->code=codet(ID_fence);
-    t4->code.set(ID_WRfence, true);
+    codet fence(ID_fence);
+    fence.set(ID_WRfence, true);
+    dest.add(goto_programt::make_other(fence, function.source_location()));
 
     goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
     t5->source_location=function.source_location();
@@ -1471,10 +1467,9 @@ void goto_convertt::do_function_call_symbol(
     t3->code=code_assignt(deref_ptr, if_expr);
 
     // this instruction implies an mfence, i.e., WRfence
-    goto_programt::targett t4=dest.add_instruction(OTHER);
-    t4->source_location=function.source_location();
-    t4->code=codet(ID_fence);
-    t4->code.set(ID_WRfence, true);
+    codet fence(ID_fence);
+    fence.set(ID_WRfence, true);
+    dest.add(goto_programt::make_other(fence, function.source_location()));
 
     goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
     t5->source_location=function.source_location();

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE pthread`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=10$`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,4 @@`
`1`	`1`	`#include <stdlib.h>`
`2`		`-#include <pthread.h>`
`3`	`2`
`4`	`3`	`_Bool set_done;`
`5`	`4`	`int *ptr;`