[WIP] Concurrency with pointers

regression/book-examples/account/C10.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE no-new-smt gcc-only
 account.c
 
 ^EXIT=10$

regression/cbmc-concurrency/CMakeLists.txt

@@ -1,4 +1,4 @@
-if((NOT WIN32) AND (NOT APPLE) AND (NOT (CMAKE_SYSTEM_NAME STREQUAL "FreeBSD")))
+if(NOT WIN32)
 add_test_pl_tests(
     "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
 )

regression/cbmc-concurrency/Makefile

@@ -3,9 +3,8 @@ default: tests.log
 include ../../src/config.inc
 include ../../src/common
 
-ifeq ($(filter-out OSX MSVC FreeBSD,$(BUILD_ENV_)),)
+ifeq ($(filter-out MSVC,$(BUILD_ENV_)),)
 	# no POSIX threads on Windows
-	# for OSX and FreeBSD we'd need sound handling of pointers in multi-threaded programs
 	no_pthread = -X pthread
 endif
 

regression/cbmc-concurrency/dirty_local1/test.desc

@@ -1,8 +1,9 @@
 CORE
 main.c
 --no-standard-checks
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
 --
 ^warning: ignoring
+pointer handling for concurrency is unsound

regression/cbmc-concurrency/global_pointer1/detect_unsoundness.desc

@@ -0,0 +1,9 @@
+CORE pthread
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+pointer handling for concurrency is unsound

regression/cbmc-concurrency/global_pointer1/main.c

@@ -7,12 +7,16 @@ int g;
 void *thread1(void * arg)
 {
   v = &g;
+  return NULL;
 }
 
 void *thread2(void *arg)
 {
   assert(v == &g);
+#ifndef NO_DEREF
   *v = 1;
+#endif
+  return NULL;
 }
 
 int main()
@@ -26,7 +30,9 @@ int main()
   pthread_join(t2, 0);
 
   assert(v == &g);
+#ifndef NO_DEREF
   assert(*v == 1);
+#endif
 
   return 0;
 }

regression/cbmc-concurrency/global_pointer1/no_deref.desc

@@ -0,0 +1,8 @@
+CORE pthread
+main.c
+-DNO_DEREF
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-concurrency/global_pointer1/test.desc

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

regression/cbmc-concurrency/malloc1/test.desc

@@ -1,8 +1,9 @@
 CORE
 main.c
 --no-malloc-may-fail
+^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+pointer handling for concurrency is unsound

regression/cbmc-concurrency/malloc2/test.desc

@@ -1,8 +1,9 @@
 CORE
 main.c
 --no-malloc-may-fail
-^EXIT=0$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+pointer handling for concurrency is unsound

regression/cbmc-concurrency/may_alias1/main.c

@@ -0,0 +1,13 @@
+int *object;
+_Bool create_object;
+void allocator(void) {
+  __CPROVER_assume(create_object);
+  object = __CPROVER_allocate(sizeof(int), 1);
+  create_object = 0;
+}
+int main() {
+  __CPROVER_ASYNC_1: allocator();
+  create_object = 1;
+  __CPROVER_assume(create_object == 0);
+  *object = 42;
+}

regression/cbmc-concurrency/may_alias1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--no-malloc-may-fail
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+pointer handling for concurrency is unsound
+^warning: ignoring

regression/cbmc-concurrency/may_alias2/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int *ptr;
+int val;
+_Bool done;
+
+void writer(void)
+{
+  val = 42;
+  ptr = &val;
+  done = 1;
+}
+
+int main(void)
+{
+  __CPROVER_ASYNC_1: writer();
+  __CPROVER_assume(done == 1);
+  assert(*ptr == 42);
+}

regression/cbmc-concurrency/may_alias2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=(0|10)$
+^SIGNAL=0$
+--
+pointer handling for concurrency is unsound
+^warning: ignoring

regression/cbmc-concurrency/may_alias3/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int *shared_ptr;
+_Bool flag;
+
+void thread1(void)
+{
+  int local = 0;
+  shared_ptr = &local;
+  flag = 1;
+}
+
+int main(void)
+{
+  int x = 10;
+  shared_ptr = &x;
+  __CPROVER_ASYNC_1: thread1();
+  __CPROVER_assume(flag == 1);
+  assert(*shared_ptr == 10);
+}

regression/cbmc-concurrency/may_alias3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=(0|10)$
+^SIGNAL=0$
+--
+pointer handling for concurrency is unsound
+^warning: ignoring

regression/cbmc-concurrency/may_alias_byte_extract/main.c

@@ -0,0 +1,20 @@
+// Test char* accessing an int through shared pointer (byte_extract).
+#include <assert.h>
+
+char *shared_ptr;
+int val;
+_Bool done;
+
+void writer(void)
+{
+  val = 0x42;
+  shared_ptr = (char *)&val;
+  done = 1;
+}
+
+int main(void)
+{
+  __CPROVER_ASYNC_1: writer();
+  __CPROVER_assume(done == 1);
+  assert(*shared_ptr == 0x42);
+}

regression/cbmc-concurrency/may_alias_byte_extract/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+pointer handling for concurrency is unsound
+^warning: ignoring
+--
+Tests different-size type access: char* reading from an int through
+a shared pointer. The byte_extract mechanism reinterprets the int
+value as a char.

regression/cbmc-concurrency/may_alias_dynamic/main.c

@@ -0,0 +1,19 @@
+// Test shared pointer to malloc'd object (the original issue #790 example).
+int *object;
+_Bool create_object;
+
+void allocator(void)
+{
+  __CPROVER_assume(create_object);
+  object = __CPROVER_allocate(sizeof(int), 1);
+  *object = 42;
+  create_object = 0;
+}
+
+int main()
+{
+  __CPROVER_ASYNC_1: allocator();
+  create_object = 1;
+  __CPROVER_assume(create_object == 0);
+  __CPROVER_assert(*object == 42, "object value");
+}

regression/cbmc-concurrency/may_alias_dynamic/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--no-malloc-may-fail
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+pointer handling for concurrency is unsound
+^warning: ignoring
+--
+Tests the original issue #790 example: allocator thread creates an
+object via __CPROVER_allocate and writes through the shared pointer.

regression/cbmc-concurrency/may_alias_local_ptr/main.c

@@ -0,0 +1,29 @@
+// Test that local pointers derived from shared sources are handled
+// correctly by the may-alias mechanism.
+#include <assert.h>
+
+int *shared_ptr;
+int val1, val2;
+_Bool done;
+
+void writer(void)
+{
+  val1 = 42;
+  val2 = 99;
+  shared_ptr = &val2;
+  done = 1;
+}
+
+int main(void)
+{
+  shared_ptr = &val1;
+  __CPROVER_ASYNC_1: writer();
+  __CPROVER_assume(done == 1);
+
+  // Direct dereference of shared pointer
+  assert(*shared_ptr == 42);
+
+  // Copy to local, then dereference — must also detect the bug
+  int *local_ptr = shared_ptr;
+  assert(*local_ptr == 42);
+}

regression/cbmc-concurrency/may_alias_local_ptr/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+pointer handling for concurrency is unsound
+^warning: ignoring
+--
+Tests that local pointers derived from shared sources are handled by
+the may-alias mechanism. Both *shared_ptr and *local_ptr should fail
+because the writer thread changes shared_ptr to point to val2 (=99).

regression/cbmc-concurrency/may_alias_no_false_positive/main.c

@@ -0,0 +1,22 @@
+// Verify that may-alias does NOT trigger for non-shared pointers.
+// This sequential program must verify successfully — no false positives.
+#include <assert.h>
+#include <stdlib.h>
+
+int main(void)
+{
+  int x = 42;
+  int *p = &x;
+  assert(*p == 42);
+
+  int *q = malloc(sizeof(int));
+  if(q)
+  {
+    *q = 99;
+    assert(*q == 99);
+  }
+
+  int arr[3] = {1, 2, 3};
+  int *r = &arr[1];
+  assert(*r == 2);
+}

regression/cbmc-concurrency/may_alias_no_false_positive/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+pointer handling for concurrency is unsound
+^warning: ignoring
+--
+Verify that may-alias does NOT trigger for non-shared pointers in
+sequential code. All assertions must succeed — no false positives.

regression/cbmc-concurrency/may_alias_refine/main.c

@@ -0,0 +1,20 @@
+// Test --refine-concurrency produces correct results.
+#include <assert.h>
+
+int *shared_ptr;
+int val;
+_Bool done;
+
+void writer(void)
+{
+  val = 42;
+  shared_ptr = &val;
+  done = 1;
+}
+
+int main(void)
+{
+  __CPROVER_ASYNC_1: writer();
+  __CPROVER_assume(done == 1);
+  assert(*shared_ptr == 42);
+}

regression/cbmc-concurrency/may_alias_refine/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--refine-concurrency
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+pointer handling for concurrency is unsound
+^warning: ignoring
+--
+Tests that --refine-concurrency produces correct results for a
+concurrent program with shared pointer dereferences.

regression/cbmc-concurrency/may_alias_soundness/main.c

@@ -0,0 +1,23 @@
+// Soundness test: the assertion MUST fail.
+// writer() sets ptr to &val2 (which is 99), so *ptr != 42 is possible.
+#include <assert.h>
+
+int *ptr;
+int val1, val2;
+_Bool done;
+
+void writer(void)
+{
+  val1 = 42;
+  val2 = 99;
+  ptr = &val2;
+  done = 1;
+}
+
+int main(void)
+{
+  ptr = &val1;
+  __CPROVER_ASYNC_1: writer();
+  __CPROVER_assume(done == 1);
+  assert(*ptr == 42);
+}