CONTRACTS: is_fresh now tracks separation at the byte level instead of whole objects

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc

@@ -1,9 +1,7 @@
 CORE dfcc-only
 main.c
---no-malloc-may-fail --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
-^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$
+--no-malloc-may-fail --dfcc main --enforce-contract foo
 ^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
-^\*\* 2 of \d+ failed
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/main.c

@@ -0,0 +1,37 @@
+#include <stdlib.h>
+int nondet_int();
+
+void foo(int *a, int **b_out, int **c_out)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(a, 2*sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(b_out, sizeof(int*)))
+__CPROVER_requires(__CPROVER_is_fresh(c_out, sizeof(int*)))
+__CPROVER_ensures(__CPROVER_is_fresh(*b_out, sizeof(int)))
+__CPROVER_ensures(__CPROVER_is_fresh(*c_out, sizeof(int)))
+__CPROVER_assigns(*b_out, *c_out)
+__CPROVER_ensures(**b_out == a[0])
+__CPROVER_ensures(**c_out == a[1])
+// clang-format on
+{
+  if(nondet_int())
+  {
+    *b_out = malloc(sizeof(int));
+    __CPROVER_assume(*b_out != NULL);
+    *c_out = malloc(sizeof(int));
+    __CPROVER_assume(*c_out != NULL);
+  }
+  else
+  {
+    *b_out = malloc(2 * sizeof(int));
+    __CPROVER_assume(*b_out != NULL);
+    *c_out = *b_out; // not separated, expect failure
+  }
+  **b_out = a[0];
+  **c_out = a[1];
+}
+
+int main()
+{
+  int *a, **b_out, **c_out;
+  foo(a, b_out, c_out);
+}

regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/test.desc

@@ -0,0 +1,12 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when __CPROVER_is_fresh is asserted in ensures clauses
+in contract checking mode, it detects byte interval separation failure
+within the same object.

regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/main.c

@@ -0,0 +1,37 @@
+#include <stdlib.h>
+int nondet_int();
+
+void foo(int *a, int **b_out, int **c_out)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(a, 2*sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(b_out, sizeof(int*)))
+__CPROVER_requires(__CPROVER_is_fresh(c_out, sizeof(int*)))
+__CPROVER_ensures(__CPROVER_is_fresh(*b_out, sizeof(int)))
+__CPROVER_ensures(__CPROVER_is_fresh(*c_out, sizeof(int)))
+__CPROVER_assigns(*b_out, *c_out)
+__CPROVER_ensures(**b_out == a[0])
+__CPROVER_ensures(**c_out == a[1])
+// clang-format on
+{
+  if(nondet_int())
+  {
+    *b_out = malloc(sizeof(int));
+    __CPROVER_assume(*b_out != NULL);
+    *c_out = malloc(sizeof(int));
+    __CPROVER_assume(*c_out != NULL);
+  }
+  else
+  {
+    *b_out = malloc(2 * sizeof(int));
+    __CPROVER_assume(*b_out != NULL);
+    *c_out = *b_out + 1;
+  }
+  **b_out = a[0];
+  **c_out = a[1];
+}
+
+int main()
+{
+  int *a, **b_out, **c_out;
+  foo(a, b_out, c_out);
+}

regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/test.desc

@@ -0,0 +1,12 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that when __CPROVER_is_fresh is asserted in ensures clauses
+in contract checking mode, it allows both objet level separation and byte
+interval separation within the same object.

regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/main.c

@@ -0,0 +1,36 @@
+#include <stdlib.h>
+
+void foo(int *a, int *b)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(a, 3*sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(b, 3*sizeof(int)))
+__CPROVER_assigns(__CPROVER_object_upto(a, 3*sizeof(int)))
+__CPROVER_ensures(a[0] == b[0])
+__CPROVER_ensures(a[1] == b[1])
+__CPROVER_ensures(a[2] == b[2])
+;
+
+int nondet_int();
+
+void bar()
+{
+  int a[6];
+  int b[3];
+  // c is either either a slice of `a` that overlaps a[0..2] or `b`
+  int *c = nondet_int() ? &a[0] + 2: &b[0];
+  int old_c0 = c[0];
+  int old_c1 = c[1];
+  int old_c2 = c[2];
+  foo(a, c); // failure of preconditions
+  __CPROVER_assert(a[0] == c[0], "same value 0");
+  __CPROVER_assert(a[1] == c[1], "same value 1");
+  __CPROVER_assert(a[2] == c[2], "same value 2");
+  __CPROVER_assert(old_c0 == c[0], "unmodified 0");
+  __CPROVER_assert(old_c1 == c[1], "unmodified 1");
+  __CPROVER_assert(old_c2 == c[2], "unmodified 2");
+}
+
+int main()
+{
+  bar();
+}

regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/test.desc

@@ -0,0 +1,13 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract bar --replace-call-with-contract foo
+^\[bar.assertion.\d+\].* unmodified 0: FAILURE$
+^\[foo.precondition.\d+\].*Check requires clause of contract contract::foo for function foo: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when __CPROVER_is_fresh is asserted in requires clauses
+in contract replacement mode, it detects byte interval separation failure within
+the same object.

regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/main.c

@@ -0,0 +1,36 @@
+#include <stdlib.h>
+
+void foo(int *a, int *b)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(a, 3*sizeof(int)))
+__CPROVER_requires(__CPROVER_is_fresh(b, 3*sizeof(int)))
+__CPROVER_assigns(__CPROVER_object_upto(a, 3*sizeof(int)))
+__CPROVER_ensures(a[0] == b[0])
+__CPROVER_ensures(a[1] == b[1])
+__CPROVER_ensures(a[2] == b[2])
+;
+
+int nondet_int();
+
+void bar()
+{
+  int a[6];
+  int b[3];
+  // c is either either a slice of `a` disjoint from a[0..2] or `b`
+  int *c = nondet_int() ? &a[0] + 3: &b[0];
+  int old_c0 = c[0];
+  int old_c1 = c[1];
+  int old_c2 = c[2];
+  foo(a, c); // success of preconditions
+  __CPROVER_assert(a[0] == c[0], "same value 0");
+  __CPROVER_assert(a[1] == c[1], "same value 1");
+  __CPROVER_assert(a[2] == c[2], "same value 2");
+  __CPROVER_assert(old_c0 == c[0], "unmodified 0");
+  __CPROVER_assert(old_c1 == c[1], "unmodified 1");
+  __CPROVER_assert(old_c2 == c[2], "unmodified 2");
+}
+
+int main()
+{
+  bar();
+}

regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract bar --replace-call-with-contract foo _ --z3 --slice-formula
+^\[foo.precondition.\d+\].*Check requires clause of contract contract::foo for function foo: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that when __CPROVER_is_fresh in preconditions replacement checks
+succeed when separation and size are as expected.

src/ansi-c/library/cprover_contracts.c

@@ -72,13 +72,7 @@ typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t;
 /// pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract.
 typedef struct
 {
-  /// \brief Nondet variable ranging over the set of objects allocated
-  /// by __CPROVER_contracts_is_fresh. Used to check separation constraints
-  /// in __CPROVER_contracts_is_fresh.
-  void *fresh_ptr;
-  /// \brief Nondet variable ranging over the set of locations storing
-  /// pointers on which predicates were assumed/asserted. Used to ensure
-  /// that at most one predicate is assumed per pointer.
+  __CPROVER_contracts_car_t fresh_car;
   void **ptr_pred;
 } __CPROVER_contracts_ptr_pred_ctx_t;
 
@@ -419,7 +413,8 @@ void __CPROVER_contracts_ptr_pred_ctx_init(
   __CPROVER_contracts_ptr_pred_ctx_ptr_t set)
 {
 __CPROVER_HIDE:;
-  set->fresh_ptr = (void *)0;
+  set->fresh_car = (__CPROVER_contracts_car_t){
+    .is_writable = 0, .size = 0, .lb = (void *)0, .ub = (void *)0};
   set->ptr_pred = (void **)0;
 }
 
@@ -1345,10 +1340,10 @@ __CPROVER_HIDE:;
       __VERIFIER_nondet___CPROVER_bool()
         ? elem
         : write_set->linked_ptr_pred_ctx->ptr_pred;
-    write_set->linked_ptr_pred_ctx->fresh_ptr =
+    write_set->linked_ptr_pred_ctx->fresh_car =
       __VERIFIER_nondet___CPROVER_bool()
-        ? ptr
-        : write_set->linked_ptr_pred_ctx->fresh_ptr;
+        ? __CPROVER_contracts_car_create(ptr, size)
+        : write_set->linked_ptr_pred_ctx->fresh_car;
 
     // record the object size for non-determistic bounds checking
     __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
@@ -1403,10 +1398,10 @@ __CPROVER_HIDE:;
       __VERIFIER_nondet___CPROVER_bool()
         ? elem
         : write_set->linked_ptr_pred_ctx->ptr_pred;
-    write_set->linked_ptr_pred_ctx->fresh_ptr =
+    write_set->linked_ptr_pred_ctx->fresh_car =
       __VERIFIER_nondet___CPROVER_bool()
-        ? ptr
-        : write_set->linked_ptr_pred_ctx->fresh_ptr;
+        ? __CPROVER_contracts_car_create(ptr, size)
+        : write_set->linked_ptr_pred_ctx->fresh_car;
 
     // record the object size for non-determistic bounds checking
     __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
@@ -1440,11 +1435,15 @@ __CPROVER_HIDE:;
         (write_set->assume_ensures_ctx == 0),
       "only one context flag at a time");
 #endif
+    // check separation
     void *ptr = *elem;
+    __CPROVER_contracts_car_t car = __CPROVER_contracts_car_create(ptr, size);
+    __CPROVER_contracts_car_t fresh_car =
+      write_set->linked_ptr_pred_ctx->fresh_car;
     if(
-      ptr != (void *)0 &&
-      !__CPROVER_same_object(write_set->linked_ptr_pred_ctx->fresh_ptr, ptr) &&
-      __CPROVER_r_ok(ptr, size))
+      ptr != (void *)0 && __CPROVER_r_ok(ptr, size) &&
+      (!__CPROVER_same_object(car.lb, fresh_car.lb) ||
+       (car.ub <= fresh_car.lb) || (fresh_car.ub <= car.lb)))
     {
       __CPROVER_assert(
         write_set->linked_ptr_pred_ctx->ptr_pred != elem,
@@ -1454,10 +1453,10 @@ __CPROVER_HIDE:;
         __VERIFIER_nondet___CPROVER_bool()
           ? elem
           : write_set->linked_ptr_pred_ctx->ptr_pred;
-      write_set->linked_ptr_pred_ctx->fresh_ptr =
+      write_set->linked_ptr_pred_ctx->fresh_car =
         __VERIFIER_nondet___CPROVER_bool()
-          ? ptr
-          : write_set->linked_ptr_pred_ctx->fresh_ptr;
+          ? car
+          : write_set->linked_ptr_pred_ctx->fresh_car;
       return 1;
     }
     return 0;