Change goto_checkt::address_check() dynamic memory bounds checking

This changes the dynamic memory bounds checking predicate in address_check().
It now uses OBJECT_SIZE() instead of the variables __CPROVER_malloc_size and
__CPROVER_malloc_object that are set in the malloc() model. This also means that
the predicates __CPROVER_r_ok()/__CPROVER_w_ok() will be more precise. In the
previous approach, the following assertion could not be proven for example:

void main() { char *c = malloc(1); assert(!__CPROVER_r_ok(c, 2)); }

Author: danpoe

regression/cbmc/r_w_ok5/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char c[2];
+  assert(__CPROVER_r_ok(c, 2));
+  assert(!__CPROVER_r_ok(c, 2));
+  assert(__CPROVER_r_ok(c, 3));
+  assert(!__CPROVER_r_ok(c, 3));
+
+  char *p = malloc(2);
+  assert(__CPROVER_r_ok(c, 2));
+  assert(!__CPROVER_r_ok(c, 2));
+  assert(__CPROVER_r_ok(p, 3));
+  assert(!__CPROVER_r_ok(p, 3));
+}

regression/cbmc/r_w_ok5/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+
+\[main.assertion.1\] .*: SUCCESS
+\[main.assertion.2\] .*: FAILURE
+\[main.assertion.3\] .*: FAILURE
+\[main.assertion.4\] .*: SUCCESS
+\[main.assertion.5\] .*: SUCCESS
+\[main.assertion.6\] .*: FAILURE
+\[main.assertion.7\] .*: FAILURE
+\[main.assertion.8\] .*: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/r_w_ok6/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p;
+  int choice;
+
+  if(choice)
+  {
+    p = malloc(2);
+  }
+  else
+  {
+    p = malloc(3);
+  }
+
+  assert(__CPROVER_r_ok(p, 2));
+  assert(!__CPROVER_r_ok(p, 2));
+
+  assert(__CPROVER_r_ok(p, 3));
+  assert(!__CPROVER_r_ok(p, 3));
+
+  assert(__CPROVER_r_ok(p, 4));
+  assert(!__CPROVER_r_ok(p, 4));
+}

regression/cbmc/r_w_ok6/test.desc

@@ -0,0 +1,16 @@
+CORE broken-smt-backend
+main.c
+
+\[main.assertion.1\] .*: SUCCESS
+\[main.assertion.2\] .*: FAILURE
+\[main.assertion.3\] .*: FAILURE
+\[main.assertion.4\] .*: FAILURE
+\[main.assertion.5\] .*: FAILURE
+\[main.assertion.6\] .*: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test checks that __CPROVER_r_ok() gives the correct result when the given
+pointer can point to different memory segments of different sizes

regression/cbmc/r_w_ok7/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+int main()
+{
+  size_t x;
+  size_t y;
+  uint8_t *a;
+
+  __CPROVER_assume(x > 0);
+  __CPROVER_assume(y > x);
+
+  a = malloc(sizeof(uint8_t) * x);
+
+  assert(__CPROVER_w_ok(a, x));
+  assert(!__CPROVER_w_ok(a, y));
+}

regression/cbmc/r_w_ok7/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+\[main.assertion.1\] .*: SUCCESS
+\[main.assertion.2\] .*: SUCCESS
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test checks that __CPROVER_r_ok() works with nondet sizes

regression/cbmc/r_w_ok8/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *x = malloc(2);
+  int *y = malloc(2);
+  assert(!__CPROVER_r_ok(x, 3));
+  assert(__CPROVER_r_ok(x, 3) == __CPROVER_r_ok(y, 3));
+}

regression/cbmc/r_w_ok8/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+
+\[main.assertion.1\] .*: SUCCESS
+\[main.assertion.2\] .*: SUCCESS
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test checks that two usages of the primitive __CPROVER_r_ok() can be false
+simultaneously in the encoding of the program. Previously, at most one call
+could be false at a time. This was imprecise, however, it was sufficient to
+guarantee soundness when the __CPROVER_r_ok() primitive was used directly in an
+assertion (i.e., as assert(__CPROVER_r_ok(p, size)). See issue #5194.

src/analyses/goto_check.cpp

@@ -1249,15 +1249,15 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
 
     if(flags.is_unknown() || flags.is_dynamic_heap())
     {
-      const or_exprt dynamic_bounds_violation(
-        dynamic_object_lower_bound(address, nil_exprt()),
-        dynamic_object_upper_bound(address, ns, size));
+      const or_exprt object_bounds_violation(
+        object_lower_bound(address, nil_exprt()),
+        object_upper_bound(address, size));
 
       conditions.push_back(conditiont(
         or_exprt(
           in_bounds_of_some_explicit_allocation,
           implies_exprt(
-            malloc_object(address, ns), not_exprt(dynamic_bounds_violation))),
+            dynamic_object(address), not_exprt(object_bounds_violation))),
         "pointer outside dynamic object bounds"));
     }