Merge pull request #6498 from tautschnig/setjmp-overapprox

tautschnig · web-flow · commit cc8321e2428c · 2021-12-03T21:53:32.000+01:00
C library: model currently supported behaviour of longjmp
diff --git a/regression/cbmc-library/CMakeLists.txt b/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()
diff --git a/regression/cbmc-library/Makefile b/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) '{}' \;
diff --git a/regression/cbmc-library/_longjmp-01/main.c b/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;
 }
diff --git a/regression/cbmc-library/_longjmp-01/test.desc b/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
diff --git a/regression/cbmc-library/longjmp-01/main.c b/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;
 }
diff --git a/regression/cbmc-library/longjmp-01/test.desc b/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
diff --git a/regression/cbmc-library/pthread_barrier_destroy-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_barrier_init-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_barrier_wait-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_cancel-01/test.desc b/regression/cbmc-library/pthread_cancel-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+KNOWNBUG unix
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/pthread_cond_broadcast-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_cond_init-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_cond_signal-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_cond_wait-01/test.desc b/regression/cbmc-library/pthread_cond_wait-01/test.desc
@@ -1,4 +1,4 @@
-CORE pthread
+CORE unix
 main.c
 --bounds-check
 ^EXIT=10$
diff --git a/regression/cbmc-library/pthread_create-01/test.desc b/regression/cbmc-library/pthread_create-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+KNOWNBUG unix
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/pthread_exit-01/test.desc b/regression/cbmc-library/pthread_exit-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+KNOWNBUG unix
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/pthread_join-01/test.desc b/regression/cbmc-library/pthread_join-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+KNOWNBUG unix
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/pthread_mutex_destroy-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_mutex_init-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_mutex_lock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_mutex_trylock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_mutex_unlock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_mutexattr_settype-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_rwlock_destroy-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_rwlock_init-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_rwlock_rdlock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_rwlock_tryrdlock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_rwlock_trywrlock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_rwlock_unlock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_rwlock_wrlock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_spin_lock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_spin_trylock-01/test.desc b/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$
diff --git a/regression/cbmc-library/pthread_spin_unlock-01/test.desc b/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$
diff --git a/regression/cbmc-library/setjmp-01/main.c b/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;
 }
diff --git a/regression/cbmc-library/setjmp-01/test.desc b/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
diff --git a/regression/cbmc-library/siglongjmp-01/main.c b/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;
 }
diff --git a/regression/cbmc-library/siglongjmp-01/test.desc b/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
diff --git a/regression/cbmc-library/sigsetjmp-01/main.c b/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;
+}
diff --git a/regression/cbmc-library/sigsetjmp-01/test.desc b/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
diff --git a/src/ansi-c/library/setjmp.c b/src/ansi-c/library/setjmp.c

Original file line number	Diff line number	Diff line change
`@@ -7,7 +7,7 @@ add_test_pl_tests(`
`7`	`7`	`"$<TARGET_FILE:cbmc>"`
`8`	`8`	`"cbmc-library"`
`9`	`9`	`"$<TARGET_FILE:cbmc>"`
`10`		`- "-C;-X;pthread"`
	`10`	`+ "-C;-X;unix"`
`11`	`11`	`"CORE"`
`12`	`12`	`)`
`13`	`13`	`endif()`
Original file line number	Diff line number	Diff line change
`@@ -1,9 +1,10 @@`
`1`		`-#include <assert.h>`
`2`	`1`	`#include <setjmp.h>`
`3`	`2`
	`3`	`+static jmp_buf env;`
	`4`	`+`
`4`	`5`	`int main()`
`5`	`6`	`{`
`6`		`- _longjmp();`
`7`		`- assert(0);`
	`7`	`+ _longjmp(env, 1);`
	`8`	`+ __CPROVER_assert(0, "unreachable");`
`8`	`9`	`return 0;`
`9`	`10`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG pthread`
	`1`	`+KNOWNBUG unix`
`2`	`2`	`main.c`
`3`	`3`	`--pointer-check --bounds-check`
`4`	`4`	`^EXIT=0$`