bounds of heap objects now tracked using object_size()

Author: Daniel Kroening

regression/cbmc/Malloc23/test.desc

@@ -3,10 +3,10 @@ main.c
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-pointer outside dynamic object bounds in \*p: FAILURE
-pointer outside dynamic object bounds in \*p: FAILURE
-pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
-pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
+pointer outside object bounds in \*p: FAILURE
+pointer outside object bounds in \*p: FAILURE
+pointer outside object bounds in p2\[.*1\]: FAILURE
+pointer outside object bounds in p2\[.*0\]: FAILURE
 \*\* 4 of [0-9]+ failed
 --
 ^warning: ignoring

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -3,7 +3,7 @@ main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$
 ^SIGNAL=0$
-array\.List dynamic object upper bound in p->List\[2\]: FAILURE
+array\.List object upper bound in p->List\[2\]: FAILURE
 \*\* 1 of 14 failed
 --
 ^warning: ignoring

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -3,7 +3,7 @@ main.i
 --bounds-check --32
 ^EXIT=10$
 ^SIGNAL=0$
-array\.List dynamic object upper bound in p->List\[2\]: FAILURE
+array\.List object upper bound in p->List\[2\]: FAILURE
 \*\* 1 of 11 failed 
 --
 ^warning: ignoring

regression/cbmc/pointer-extra-checks/test.desc

@@ -7,7 +7,7 @@ main.c
 ^\[main.pointer_dereference.2\] dereference failure: dead object in \*q: SUCCESS$
 ^\[main.pointer_dereference.3\] dereference failure: pointer outside object bounds in \*q: SUCCESS$
 ^\[main.pointer_dereference.4\] dereference failure: deallocated dynamic object in \*r: SUCCESS$
-^\[main.pointer_dereference.5\] dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
+^\[main.pointer_dereference.5\] dereference failure: pointer outside object bounds in \*r: SUCCESS$
 ^\[main.pointer_dereference.6\] dereference failure: pointer uninitialized in \*s: FAILURE$
 ^VERIFICATION FAILED$
 --
@@ -16,23 +16,19 @@ main.c
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*p:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*p:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*p:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*p:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*p:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*q:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*q:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*q:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*q:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*q:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*r:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*r:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*r:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*r:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*r:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*s:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*s:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*s:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*s:
-^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*s:
 ^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*s:
 --
 This test ensures that local_bitvector_analysis is correctly labelling obvious

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: 5, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, 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: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 10, function calls: 2$
 --
 ^warning: ignoring

src/analyses/goto_check.cpp

@@ -1031,27 +1031,16 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
         not_exprt(dead_object(address, ns)), "dead object"));
     }
 
-    if(flags.is_unknown() || flags.is_dynamic_heap())
-    {
-      const or_exprt dynamic_bounds_violation(
-        dynamic_object_lower_bound(address, ns, nil_exprt()),
-        dynamic_object_upper_bound(address, ns, size));
-
-      conditions.push_back(conditiont(
-        implies_exprt(malloc_object(address, ns), not_exprt(dynamic_bounds_violation)),
-        "pointer outside dynamic object bounds"));
-    }
-
     if(
       flags.is_unknown() || flags.is_dynamic_local() ||
-      flags.is_static_lifetime())
+      flags.is_dynamic_heap() || flags.is_static_lifetime())
     {
       const or_exprt object_bounds_violation(
         object_lower_bound(address, ns, nil_exprt()),
         object_upper_bound(address, ns, size));
 
       conditions.push_back(conditiont(
-        implies_exprt(not_exprt(dynamic_object(address)), not_exprt(object_bounds_violation)),
+        not_exprt(object_bounds_violation),
         "pointer outside object bounds"));
     }
 
@@ -1152,11 +1141,7 @@ void goto_checkt::bounds_check(
     const exprt &pointer=
       to_dereference_expr(ode.root_object()).pointer();
 
-    if_exprt size(
-      dynamic_object(pointer),
-      typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
-      object_size(pointer));
-
+    auto size=object_size(pointer);
     plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
 
     assert(effective_offset.op0().type()==effective_offset.op1().type());
@@ -1173,7 +1158,7 @@ void goto_checkt::bounds_check(
 
     add_guarded_claim(
       precond,
-      name+" dynamic object upper bound",
+      name+" object upper bound",
       "array bounds",
       expr.find_source_location(),
       expr,

src/ansi-c/ansi_c_internal_additions.cpp

@@ -144,7 +144,6 @@ void ansi_c_internal_additions(std::string &code)
     "const void *__CPROVER_deallocated=0;\n"
     "const void *__CPROVER_dead_object=0;\n"
     "const void *__CPROVER_malloc_object=0;\n"
-    "__CPROVER_size_t __CPROVER_malloc_size;\n"
     "__CPROVER_bool __CPROVER_malloc_is_new_array=0;\n" // for C++
     "const void *__CPROVER_memory_leak=0;\n"
     "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"

src/ansi-c/library/cprover.h

@@ -13,7 +13,6 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_malloc_object;
-extern __CPROVER_size_t __CPROVER_malloc_size;
 extern _Bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
 

src/ansi-c/library/stdlib.c

@@ -79,7 +79,6 @@ inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
   __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_object =
     record_malloc ? malloc_res : __CPROVER_malloc_object;
-  __CPROVER_malloc_size = record_malloc ? nmemb * size : __CPROVER_malloc_size;
   __CPROVER_malloc_is_new_array =
     record_malloc ? 0 : __CPROVER_malloc_is_new_array;
 
@@ -115,7 +114,6 @@ inline void *malloc(__CPROVER_size_t malloc_size)
   // record the object size for non-determistic bounds checking
   __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;
   __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
 
   // detect memory leaks
@@ -141,7 +139,6 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
   // record the object size for non-determistic bounds checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
-  __CPROVER_malloc_size=record_malloc?alloca_size:__CPROVER_malloc_size;
   __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
 
   return res;