Add ASV book CBMC examples

peterschrammel · peterschrammel · commit 958103697499 · 2023-09-28T21:59:19.000+01:00
to make sure they actually work.

account.c with C10.desc currently doesn't work due
to unsound pointer handling with concurrency.
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
@@ -92,6 +92,7 @@ add_subdirectory(cbmc-sequentialization)
 add_subdirectory(cpp-linter)
 add_subdirectory(catch-framework)
 add_subdirectory(libcprover-cpp)
+add_subdirectory(book-examples)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)
diff --git a/regression/Makefile b/regression/Makefile
@@ -63,6 +63,7 @@ DIRS = cbmc-shadow-memory \
        cpp-linter \
        catch-framework \
        libcprover-cpp \
+       book-examples \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)
diff --git a/regression/book-examples/CMakeLists.txt b/regression/book-examples/CMakeLists.txt
@@ -0,0 +1,48 @@
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  set(gcc_only -X gcc-only)
+  set(gcc_only_string "-X;gcc-only;")
+  set(exclude_win_broken_tests -X winbug)
+  # We add the string at the end of the exclusion list, so it must not
+  # have the `;` at the end or it bugs out.
+  set(exclude_win_broken_tests_string "-X;winbug")
+else()
+  set(gcc_only "")
+  set(gcc_only_string "")
+  set(exclude_win_broken_tests "")
+  set(exclude_win_broken_tests_string "")
+endif()
+
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
+)
+
+add_test_pl_profile(
+    "cbmc-paths-lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
+    "CORE"
+)
+
+add_test_pl_profile(
+    "cbmc-cprover-smt2"
+    "$<TARGET_FILE:cbmc> --cprover-smt2"
+    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
+    "CORE"
+)
+
+# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+add_test_pl_profile(
+  "cbmc-new-smt-backend"
+  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
+  "${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
+  "CORE"
+)
+
+# solver appears on the PATH in Windows already
+if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+  set_property(
+    TEST "cbmc-cprover-smt2-CORE"
+    PROPERTY ENVIRONMENT
+      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+  )
+endif()
diff --git a/regression/book-examples/Makefile b/regression/book-examples/Makefile
@@ -0,0 +1,43 @@
+default: test
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+GCC_ONLY = -X gcc-only
+else
+GCC_ONLY =
+endif
+
+test:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+
+test-cprover-smt2:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
+					  -s cprover-smt2 $(GCC_ONLY)
+
+test-z3:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
+					  -s z3 $(GCC_ONLY)
+
+test-paths-lifo:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
+					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
+					  -s paths-lifo $(GCC_ONLY)
+
+test-new-smt-backend:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
+					  -I new-smt-backend \
+					  -s new-smt-backend $(GCC_ONLY)
+
+tests.log: ../test.pl test
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) export-symex-ready-goto/exported.symex.ready.goto
+	$(RM) tests*.log
diff --git a/regression/book-examples/abs/C1.desc b/regression/book-examples/abs/C1.desc
@@ -0,0 +1,6 @@
+CORE
+abs.c
+--function abs
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/book-examples/abs/C13.desc b/regression/book-examples/abs/C13.desc
@@ -0,0 +1,5 @@
+CORE
+abs.c
+--function abs --signed-overflow-check --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
diff --git a/regression/book-examples/abs/C2.desc b/regression/book-examples/abs/C2.desc
@@ -0,0 +1,6 @@
+CORE
+abs.c
+--function abs --signed-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/book-examples/abs/C3.desc b/regression/book-examples/abs/C3.desc
@@ -0,0 +1,6 @@
+CORE
+abs.c
+--function abs --signed-overflow-check --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/book-examples/abs/abs.c b/regression/book-examples/abs/abs.c
@@ -0,0 +1,11 @@
+int abs(int x)
+{
+  int y = x;
+
+  if(x < 0)
+  {
+    y = -x;
+  }
+
+  return y;
+}
diff --git a/regression/book-examples/account/C10.desc b/regression/book-examples/account/C10.desc
@@ -0,0 +1,6 @@
+KNOWNBUG
+account.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/book-examples/account/account.c b/regression/book-examples/account/account.c
@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <pthread.h>
+
+pthread_mutex_t mutex;
+int balance = 1000;
+
+void *transaction(void *amount)
+{
+  // pthread_mutex_lock(&mutex);
+  int current = balance;
+  current += *(int *)amount;
+  balance = current;
+  // pthread_mutex_unlock(&mutex);
+  return 0;
+}
+
+int main()
+{
+  pthread_t t1, t2;
+  pthread_mutex_init(&mutex, 0);
+
+  int amount1 = -3000;
+  pthread_create(&t1, 0, transaction, &amount1);
+  int amount2 = 8000;
+  pthread_create(&t2, 0, transaction, &amount2);
+
+  pthread_join(t1, 0);
+  pthread_join(t2, 0);
+  assert(balance == 6000);
+
+  pthread_mutex_destroy(&mutex);
+  return 0;
+}
diff --git a/regression/book-examples/binsearch/C4.desc b/regression/book-examples/binsearch/C4.desc
@@ -0,0 +1,6 @@
+CORE
+binsearch.c
+--function binsearch --unwind 6 --bounds-check --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
diff --git a/regression/book-examples/binsearch/binsearch.c b/regression/book-examples/binsearch/binsearch.c
@@ -0,0 +1,19 @@
+int binsearch(int x)
+{
+  int a[16];
+  signed low = 0, high = 16;
+
+  while(low < high)
+  {
+    signed middle = low + ((high - low) >> 1);
+
+    if(a[middle] < x)
+      high = middle;
+    else if(a[middle] > x)
+      low = middle + 1;
+    else // a[middle]==x
+      return middle;
+  }
+
+  return -1;
+}
diff --git a/regression/book-examples/lock/depth.desc b/regression/book-examples/lock/depth.desc
@@ -0,0 +1,6 @@
+CORE
+lock.c
+--depth 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/book-examples/lock/lock.c b/regression/book-examples/lock/lock.c
@@ -0,0 +1,42 @@
+_Bool nondet_bool();
+unsigned int nondet_unsigned_int();
+_Bool LOCK = 0;
+
+_Bool lock()
+{
+  if(nondet_bool())
+  {
+    assert(!LOCK);
+    LOCK = 1;
+    return 1;
+  }
+
+  return 0;
+}
+
+void unlock()
+{
+  assert(LOCK);
+  LOCK = 0;
+}
+
+int main()
+{
+  unsigned got_lock = 0;
+  unsigned times = nondet_unsigned_int();
+
+  while(times > 0)
+  {
+    if(lock())
+    {
+      got_lock++;
+      /* critical section */
+    }
+
+    if(got_lock != 0)
+      unlock();
+
+    got_lock--;
+    times--;
+  }
+}
diff --git a/regression/book-examples/lock/unwind1.desc b/regression/book-examples/lock/unwind1.desc
@@ -0,0 +1,6 @@
+CORE
+lock.c
+--unwind 1
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/book-examples/lock/unwind2.desc b/regression/book-examples/lock/unwind2.desc
@@ -0,0 +1,6 @@
+CORE
+lock.c
+--unwind 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/book-examples/login/C5.desc b/regression/book-examples/login/C5.desc
@@ -0,0 +1,6 @@
+CORE
+login.c
+--unwind 20 --bounds-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/book-examples/login/C6.desc b/regression/book-examples/login/C6.desc
@@ -0,0 +1,6 @@
+CORE
+login.c
+--show-properties --bounds-check --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+Property main\.array_bounds\.\d
diff --git a/regression/book-examples/login/C7.desc b/regression/book-examples/login/C7.desc
@@ -0,0 +1,5 @@
+CORE
+login.c
+--unwind 20 --show-vcc --bounds-check --pointer-check
+^EXIT=0$
+^SIGNAL=0$
diff --git a/regression/book-examples/login/C8.desc b/regression/book-examples/login/C8.desc
@@ -0,0 +1,6 @@
+CORE
+login.c
+--unwind 20 --bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/book-examples/login/C9.desc b/regression/book-examples/login/C9.desc
@@ -0,0 +1,6 @@
+CORE
+login.c
+--unwind 20 --bounds-check --pointer-check --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
diff --git a/regression/book-examples/login/login.c b/regression/book-examples/login/login.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  char password[8] = {'s', 'e', 'c', 'r', 'e', 't', '!', '\0'};
+  char buffer[16] = {
+    '\0',
+  };
+  int tmp;
+  int index = 0;
+
+  printf("Enter your name: ");
+  while((tmp = getchar()) != '\n')
+  {
+    buffer[index] = tmp;
+    ++index;
+  }
+
+  printf("%s\n", buffer);
+
+  return 0;
+}
diff --git a/regression/book-examples/pid/C11.desc b/regression/book-examples/pid/C11.desc
@@ -0,0 +1,6 @@
+CORE
+pid.c
+--cover mcdc --unwind 6
+^EXIT=0$
+^SIGNAL=0$
+coverage results
diff --git a/regression/book-examples/pid/pid.c b/regression/book-examples/pid/pid.c
