Merge pull request #6498 from tautschnig/setjmp-overapprox

C library: model currently supported behaviour of longjmp

Author: tautschnig

regression/cbmc-library/CMakeLists.txt

@@ -7,7 +7,7 @@ add_test_pl_tests(
     "$<TARGET_FILE:cbmc>"
     "cbmc-library"
     "$<TARGET_FILE:cbmc>"
-    "-C;-X;pthread"
+    "-C;-X;unix"
     "CORE"
 )
 endif()

regression/cbmc-library/Makefile

@@ -4,14 +4,14 @@ include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
-	no_pthread = -X pthread
+	unix_only = -X unix
 endif
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread)
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only)
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;

regression/cbmc-library/_longjmp-01/main.c

@@ -1,9 +1,10 @@
-#include <assert.h>
 #include <setjmp.h>
 
+static jmp_buf env;
+
 int main()
 {
-  _longjmp();
-  assert(0);
+  _longjmp(env, 1);
+  __CPROVER_assert(0, "unreachable");
   return 0;
 }

regression/cbmc-library/_longjmp-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+^\[_longjmp.assertion.1\] line 12 _longjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/longjmp-01/main.c

@@ -1,9 +1,10 @@
-#include <assert.h>
 #include <setjmp.h>
 
+static jmp_buf env;
+
 int main()
 {
-  longjmp();
-  assert(0);
+  longjmp(env, 1);
+  __CPROVER_assert(0, "unreachable");
   return 0;
 }

regression/cbmc-library/longjmp-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+^\[longjmp.assertion.1\] line 12 longjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/pthread_barrier_destroy-01/test.desc

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

regression/cbmc-library/pthread_barrier_init-01/test.desc

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

regression/cbmc-library/pthread_barrier_wait-01/test.desc

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

regression/cbmc-library/pthread_cancel-01/test.desc

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

regression/cbmc-library/pthread_cond_broadcast-01/test.desc

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

regression/cbmc-library/pthread_cond_init-01/test.desc

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

regression/cbmc-library/pthread_cond_signal-01/test.desc

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

regression/cbmc-library/pthread_cond_wait-01/test.desc

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

regression/cbmc-library/pthread_create-01/test.desc

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

regression/cbmc-library/pthread_exit-01/test.desc

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

regression/cbmc-library/pthread_join-01/test.desc

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

regression/cbmc-library/pthread_mutex_destroy-01/test.desc

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

regression/cbmc-library/pthread_mutex_init-01/test.desc

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

regression/cbmc-library/pthread_mutex_lock-01/test.desc

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

regression/cbmc-library/pthread_mutex_trylock-01/test.desc

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

regression/cbmc-library/pthread_mutex_unlock-01/test.desc

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

regression/cbmc-library/pthread_mutexattr_settype-01/test.desc

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

regression/cbmc-library/pthread_rwlock_destroy-01/test.desc

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

regression/cbmc-library/pthread_rwlock_init-01/test.desc

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

regression/cbmc-library/pthread_rwlock_rdlock-01/test.desc

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

regression/cbmc-library/pthread_rwlock_tryrdlock-01/test.desc

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

regression/cbmc-library/pthread_rwlock_trywrlock-01/test.desc

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

regression/cbmc-library/pthread_rwlock_unlock-01/test.desc

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

regression/cbmc-library/pthread_rwlock_wrlock-01/test.desc

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

regression/cbmc-library/pthread_spin_lock-01/test.desc

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

regression/cbmc-library/pthread_spin_trylock-01/test.desc

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

regression/cbmc-library/pthread_spin_unlock-01/test.desc

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

regression/cbmc-library/setjmp-01/main.c

@@ -1,9 +1,12 @@
-#include <assert.h>
 #include <setjmp.h>
 
+static jmp_buf env;
+
 int main()
 {
-  setjmp();
-  assert(0);
+  if(setjmp(env))
+    __CPROVER_assert(0, "reached via longjmp");
+  else
+    __CPROVER_assert(0, "setjmp called directly");
   return 0;
 }

regression/cbmc-library/setjmp-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+^\[main.assertion.1\] line 8 reached via longjmp: SUCCESS$
+^\[main.assertion.2\] line 10 setjmp called directly: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/siglongjmp-01/main.c

@@ -1,9 +1,10 @@
-#include <assert.h>
 #include <setjmp.h>
 
+static sigjmp_buf env;
+
 int main()
 {
-  siglongjmp();
-  assert(0);
+  siglongjmp(env, 1);
+  __CPROVER_assert(0, "unreachable");
   return 0;
 }

regression/cbmc-library/siglongjmp-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE unix
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+^\[siglongjmp.assertion.1\] line 14 siglongjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/sigsetjmp-01/main.c

@@ -0,0 +1,12 @@
+#include <setjmp.h>
+
+static sigjmp_buf env;
+
+int main()
+{
+  if(sigsetjmp(env, 0))
+    __CPROVER_assert(0, "reached via siglongjmp");
+  else
+    __CPROVER_assert(0, "sigsetjmp called directly");
+  return 0;
+}

regression/cbmc-library/sigsetjmp-01/test.desc

@@ -0,0 +1,10 @@
+CORE unix
+main.c
+--pointer-check --bounds-check
+^\[main.assertion.1\] line 8 reached via siglongjmp: SUCCESS$
+^\[main.assertion.2\] line 10 sigsetjmp called directly: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring