Merge pull request #6500 from remi-delmas-3000/assigns-clauses-malloc-zero

Handle malloc(0) and malloc(__CPROVER_max_malloc_size) in assigns clause instrumentation

Author: tautschnig

regression/contracts/assigns-enforce-malloc-zero/main.c

@@ -0,0 +1,31 @@
+#include <stdlib.h>
+
+// returns the index at which the write was performed if any
+// -1 otherwise
+int foo(char *a, int size)
+  // clang-format off
+  __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
+  __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size))
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
+  __CPROVER_ensures(
+    a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
+// clang-format on
+{
+  if(!a)
+    return -1;
+  int i;
+  if(0 <= i && i < size)
+  {
+    a[i] = 0;
+    return i;
+  }
+  return -1;
+}
+
+int main()
+{
+  size_t size;
+  char *a;
+  foo(a, size);
+  return 0;
+}

regression/contracts/assigns-enforce-malloc-zero/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-contract foo _ --malloc-may-fail --malloc-fail-null
+^EXIT=0$
+^SIGNAL=0$
+^\[foo\.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that objects of size zero or __CPROVER_max_malloc_size
+do not cause spurious falsifications in assigns clause instrumentation
+in contract enforcement mode.

regression/contracts/assigns-replace-malloc-zero/main.c

@@ -0,0 +1,37 @@
+#include <stdlib.h>
+
+// returns the index at which the write was performed if any
+// -1 otherwise
+int foo(char *a, int size)
+  // clang-format off
+__CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
+__CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size))
+__CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
+__CPROVER_ensures(
+    a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
+// clang-format on
+{
+  if(!a)
+    return -1;
+  int i;
+  if(0 <= i && i < size)
+  {
+    a[i] = 0;
+    return i;
+  }
+  return -1;
+}
+
+int main()
+{
+  int size;
+  if(size < 0)
+    size = 0;
+  if(size > __CPROVER_max_malloc_size)
+    size = __CPROVER_max_malloc_size;
+  char *a = malloc(size * sizeof(*a));
+  int res = foo(a, size);
+  if(a && res >= 0)
+    __CPROVER_assert(a[res] == 0, "expecting SUCCESS");
+  return 0;
+}

regression/contracts/assigns-replace-malloc-zero/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that objects of size zero or of __CPROVER_max_malloc_size
+do not cause spurious falsifications in assigns clause instrumentation
+in contract replacement mode.

src/goto-instrument/contracts/assigns.cpp

@@ -133,8 +133,7 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
 
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
-    minus_exprt{plus_exprt{slice.first, slice.second},
-                from_integer(1, slice.second.type())},
+    plus_exprt{slice.first, slice.second},
     location_overflow_check));
   instructions.destructive_append(skip_program);