CONTRACTS: is_fresh now checks separation of byte-intervals instead o…

…f whole objects.

When assumed, is_fresh still builds distinct objects.
When asserted, it allows for either distinct objects,
or distinct byte intervals within the same object.
A function foo(int *a, int *b) that requires is_fresh(a)
and is_fresh(b) is checked under the assumption that
a and b are distinct objects, but can still be used in contexts
where a and b are distinct slices within the same base object.
This is sound because the function is checked under the stronger
precondition and hence is proved to not perform any operation
that requires that a and b be in the same object, such as pointer
differences or comparisons.

regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/main.c

@@ -0,0 +1,34 @@
+#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,34 @@
+#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,7 @@ 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 +1339,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 +1397,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 +1434,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 +1452,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;