Merge pull request #6086 from tautschnig/remove-malloc_size

Remove __CPROVER_malloc_size

Author: tautschnig

doc/architectural/memory-bounds-checking.md

@@ -33,28 +33,27 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 
   __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_object = record_malloc ? malloc_res : __CPROVER_malloc_object;
-  __CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size;
 
   return malloc_res;
 }
 ```
 
-Both internal variables `__CPROVER_malloc_object` and `__CPROVER_malloc_size`
-are initialized to 0 in the `__CPROVER_initialize()` function of a goto program.
-The nondeterministic switch controls whether the address and size of the memory
-block allocated in this particular invocation of `malloc()` are recorded.
+The internal variable `__CPROVER_malloc_object`
+is initialized to 0 in the `__CPROVER_initialize()` function of a goto program.
+The nondeterministic switch controls whether the address of the memory
+block allocated in this particular invocation of `malloc()` is recorded.
 
 When the option `--pointer-check` is used, cbmc generates the following
 verification condition for each pointer dereference expression (e.g.,
 `*pointer`):
 
 ```C
-__CPROVER_POINTER_OBJECT(pointer) == __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object) ==>
-__CPROVER_POINTER_OFFSET(pointer) >= 0 && __CPROVER_POINTER_OFFSET(pointer) < __CPROVER_malloc_size
+__CPROVER_POINTER_OFFSET(pointer) >= 0 &&
+__CPROVER_POINTER_OFFSET(pointer) < __CPROVER_OBJECT_SIZE(pointer)
 ```
 
-The primitives `__CPROVER_POINTER_OBJECT()` and `__CPROVER_POINTER_OFFSET()` extract
-the object id, and pointer offset, respectively. Similar conditions are
+The primitives `__CPROVER_POINTER_OFFSET()` and `__CPROVER_OBJECT_SIZE()` extract
+the pointer offset and size of the object pointed to, respectively. Similar conditions are
 generated for `assert(__CPROVER_r_ok(pointer, size))` and
 `assert(__CPROVER_w_ok(pointer, size))`.
 
@@ -77,9 +76,5 @@ Here the verification condition generated for the pointer dereference should
 fail. In the approach outlined above it indeed can, as one can choose true for
 `__VERIFIER_nondet___CPROVER_bool()` in the first call
 to `malloc()`, and false for `__VERIFIER_nondet___CPROVER_bool()` in the second
-call to `malloc()`. Thus, the object address and size of the first call to
-`malloc()` are recorded in `__CPROVER_malloc_object` and `__CPROVER_malloc_size`
-respectively. Thus, the premise of the implication in the verification condition
-above is true, while the conclusion is false, hence the overall condition is
-false.
-
+call to `malloc()`. Thus, the object address of the first call to
+`malloc()` is recorded in `__CPROVER_malloc_object`.

regression/cbmc-with-incr/Pointer_byte_extract8/main.c

@@ -12,14 +12,11 @@ typedef struct
   Union List[1];
 } __attribute__((packed)) Struct3;
 
-extern size_t __CPROVER_malloc_size;
-
 int main()
 {
   Struct3 *p = malloc (sizeof (int) + 2 * sizeof(Union));
   p->Count = 3;
   int po=0;
-  size_t m=__CPROVER_malloc_size;
 
   // this should be fine
   p->List[0].a = 555;

regression/contracts/function_check_mem_01/main.c

@@ -7,21 +7,16 @@
 
 #include <stddef.h>
 
-#define __CPROVER_VALID_MEM(ptr, size) \
-  __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \
-  !__CPROVER_invalid_pointer((ptr)) && \
-  __CPROVER_POINTER_OBJECT((ptr)) != \
-  __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \
-  __CPROVER_POINTER_OBJECT((ptr)) != \
-  __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) && \
-  (__builtin_object_size((ptr), 1) >= (size) && \
-  __CPROVER_POINTER_OFFSET((ptr)) >= 0l || \
-   __CPROVER_DYNAMIC_OBJECT((ptr))) && \
-  (__CPROVER_POINTER_OFFSET((ptr)) >= 0 && \
-   __CPROVER_malloc_size >= (size) + __CPROVER_POINTER_OFFSET((ptr)) || \
-   __CPROVER_POINTER_OBJECT((ptr)) != \
-   __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object))
-    
+#define __CPROVER_VALID_MEM(ptr, size)                                         \
+  __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) &&         \
+    !__CPROVER_invalid_pointer((ptr)) &&                                       \
+    __CPROVER_POINTER_OBJECT((ptr)) !=                                         \
+      __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) &&                       \
+    __CPROVER_POINTER_OBJECT((ptr)) !=                                         \
+      __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) &&                       \
+    (__builtin_object_size((ptr), 1) >= (size) &&                              \
+     __CPROVER_POINTER_OFFSET((ptr)) >= 0l)
+
 typedef struct bar
 {
   int x;

regression/goto-analyzer/constant_propagation_01/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_04/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring