Merge pull request #6094 from tautschnig/remove-malloc_object

kroening · web-flow · commit d46f7059f571 · 2021-11-19T08:32:34.000Z
Remove __CPROVER_malloc_object
diff --git a/doc/architectural/memory-bounds-checking.md b/doc/architectural/memory-bounds-checking.md
@@ -30,19 +30,10 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 {
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);
-
-  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object = record_malloc ? malloc_res : __CPROVER_malloc_object;
-
   return malloc_res;
 }
 ```
 
-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`):
@@ -73,8 +64,7 @@ int main()
 ```
 
 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 of the first call to
-`malloc()` is recorded in `__CPROVER_malloc_object`.
+fail: for `p1` in `*p1`, `__CPROVER_POINTER_OFFSET` will evaluate to 1 (owing to
+the increment `p1++`, and `__CPROVER_OBJECT_SIZE` will also evaluate to 1.
+Consequently, the less-than comparison in the verification condition evaluates
+to false.
diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp
@@ -36,20 +36,6 @@ void java_internal_additions(symbol_table_baset &dest)
     dest.add(symbol);
   }
 
-  // add __CPROVER_malloc_object
-
-  {
-    symbolt symbol;
-    symbol.base_name = CPROVER_PREFIX "malloc_object";
-    symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type = pointer_type(java_void_type());
-    symbol.mode=ID_C;
-    symbol.is_lvalue=true;
-    symbol.is_state_var=true;
-    symbol.is_thread_local=true;
-    dest.add(symbol);
-  }
-
   {
     auxiliary_symbolt symbol;
     symbol.base_name = INFLIGHT_EXCEPTION_VARIABLE_BASENAME;
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc
@@ -9,8 +9,8 @@ main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
 __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_memory_leak \(\) -> TOP @ \[12\]
+__CPROVER_memory_leak \(\) -> TOP @ \[11\]
+__CPROVER_new_object \(\) -> TOP @ \[12\]
 __CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
 __CPROVER_pipe_count \(\) -> 0u @ \[15\]
 __CPROVER_rounding_mode \(\) -> 0 @ \[16\]
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc
@@ -9,8 +9,8 @@ main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
 __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_memory_leak \(\) -> TOP @ \[12\]
+__CPROVER_memory_leak \(\) -> TOP @ \[11\]
+__CPROVER_new_object \(\) -> TOP @ \[12\]
 __CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
 __CPROVER_pipe_count \(\) -> 0u @ \[15\]
 __CPROVER_rounding_mode \(\) -> 0 @ \[16\]
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc
@@ -9,8 +9,8 @@ main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
 __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_memory_leak \(\) -> TOP @ \[12\]
+__CPROVER_memory_leak \(\) -> TOP @ \[11\]
+__CPROVER_new_object \(\) -> TOP @ \[12\]
 __CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
 __CPROVER_pipe_count \(\) -> 0u @ \[15\]
 __CPROVER_rounding_mode \(\) -> 0 @ \[16\]
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc
@@ -8,8 +8,8 @@ __CPROVER_alloca_object \(\) -> TOP @ \[4\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
 __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_memory_leak \(\) -> TOP @ \[12\]
+__CPROVER_memory_leak \(\) -> TOP @ \[11\]
+__CPROVER_new_object \(\) -> TOP @ \[12\]
 __CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
 __CPROVER_pipe_count \(\) -> 0u @ \[15\]
 __CPROVER_rounding_mode \(\) -> 0 @ \[16\]
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
@@ -19,7 +19,6 @@ bool escape_domaint::is_tracked(const symbol_exprt &symbol)
   const irep_idt &identifier=symbol.get_identifier();
   if(
     identifier == CPROVER_PREFIX "memory_leak" ||
-    identifier == CPROVER_PREFIX "malloc_object" ||
     identifier == CPROVER_PREFIX "dead_object" ||
     identifier == CPROVER_PREFIX "deallocated")
   {
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -178,7 +178,7 @@ void ansi_c_internal_additions(std::string &code)
     // malloc
     "const void *" CPROVER_PREFIX "deallocated=0;\n"
     "const void *" CPROVER_PREFIX "dead_object=0;\n"
-    "const void *" CPROVER_PREFIX "malloc_object=0;\n"
+    "const void *" CPROVER_PREFIX "new_object=0;\n" // for C++
     CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
     "const void *" CPROVER_PREFIX "memory_leak=0;\n"
     "void *" CPROVER_PREFIX "allocate("
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 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 const void *__CPROVER_new_object;
 extern _Bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
 
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
@@ -111,8 +111,6 @@ __CPROVER_HIDE:;
 
   // 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_is_new_array =
     record_malloc ? 0 : __CPROVER_malloc_is_new_array;
 
@@ -175,8 +173,6 @@ __CPROVER_HIDE:;
 
   // 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_is_new_array =
     record_malloc ? 0 : __CPROVER_malloc_is_new_array;
 
@@ -207,7 +203,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_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
 
   // record alloca to detect invalid free
@@ -258,10 +253,9 @@ inline void free(void *ptr)
 
   // catch people who try to use free(...) for stuff
   // allocated with new[]
-  __CPROVER_precondition(ptr==0 ||
-                         __CPROVER_malloc_object!=ptr ||
-                         !__CPROVER_malloc_is_new_array,
-                         "free called for new[] object");
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_new_object != ptr || !__CPROVER_malloc_is_new_array,
+    "free called for new[] object");
 
   // catch people who try to use free(...) with alloca
   __CPROVER_precondition(
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
@@ -90,7 +90,7 @@ void cpp_internal_additions(std::ostream &out)
   // malloc
   out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
   out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
-  out << "const void *" CPROVER_PREFIX "malloc_object = 0;" << '\n';
+  out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n';
   out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;"
       << '\n';
   out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h
@@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 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 const void *__CPROVER_new_object;
 extern _Bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
 
diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c
@@ -13,9 +13,9 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
 
-  // non-derministically record the object size for bounds checking
+  // non-deterministically record the object for delete/delete[] checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
+  __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
   __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
 
   // detect memory leaks
@@ -40,9 +40,9 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
 
-  // non-deterministically record the object size for bounds checking
+  // non-deterministically record the object for delete/delete[] checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
+  __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
   __CPROVER_malloc_is_new_array=record_malloc?1:__CPROVER_malloc_is_new_array;
 
   // detect memory leaks
@@ -80,10 +80,9 @@ inline void __delete(void *ptr)
   __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, "double delete");
 
   // catch people who call delete for objects allocated with new[]
-  __CPROVER_precondition(ptr==0 ||
-                         __CPROVER_malloc_object!=ptr ||
-                         !__CPROVER_malloc_is_new_array,
-                         "delete of array object");
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_new_object != ptr || !__CPROVER_malloc_is_new_array,
+    "delete of array object");
 
   // If ptr is NULL, no operation is performed.
   // This is a requirement by the standard, not generosity!
@@ -120,10 +119,9 @@ inline void __delete_array(void *ptr)
                          "double delete");
 
   // catch people who call delete[] for objects allocated with new
-  __CPROVER_precondition(ptr==0 ||
-                         __CPROVER_malloc_object!=ptr ||
-                         __CPROVER_malloc_is_new_array,
-                         "delete[] of non-array object");
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_new_object != ptr || __CPROVER_malloc_is_new_array,
+    "delete[] of non-array object");
 
   if(ptr!=0)
   {
diff --git a/src/jsil/jsil_internal_additions.cpp b/src/jsil/jsil_internal_additions.cpp
@@ -39,22 +39,6 @@ void jsil_internal_additions(symbol_tablet &dest)
     dest.add(symbol);
   }
 
-  // add __CPROVER_malloc_object
-
-  {
-    symbolt symbol;
-    symbol.base_name = CPROVER_PREFIX "malloc_object";
-    symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type=pointer_type(empty_typet());
-    symbol.mode=ID_C;
-    symbol.is_lvalue=true;
-    symbol.is_state_var=true;
-    symbol.is_thread_local=true;
-    // mark as already typechecked
-    symbol.is_extern=true;
-    dest.add(symbol);
-  }
-
   // add eval
 
   {
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
@@ -40,14 +40,6 @@ exprt pointer_offset(const exprt &pointer)
   return unary_exprt(ID_pointer_offset, pointer, signed_size_type());
 }
 
-exprt malloc_object(const exprt &pointer, const namespacet &ns)
-{
-  // we check __CPROVER_malloc_object!
-  const symbolt &malloc_object_symbol=ns.lookup(CPROVER_PREFIX "malloc_object");
-
-  return same_object(pointer, malloc_object_symbol.symbol_expr());
-}
-
 exprt deallocated(const exprt &pointer, const namespacet &ns)
 {
   // we check __CPROVER_deallocated!
diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h
@@ -22,8 +22,6 @@ exprt deallocated(const exprt &pointer, const namespacet &);
 exprt dead_object(const exprt &pointer, const namespacet &);
 exprt pointer_offset(const exprt &pointer);
 exprt pointer_object(const exprt &pointer);
-DEPRECATED(SINCE(2021, 5, 6, "Unnecessary, remove any use"))
-exprt malloc_object(const exprt &pointer, const namespacet &);
 exprt object_size(const exprt &pointer);
 DEPRECATED(SINCE(2021, 5, 6, "Use is_dynamic_object_exprt instead"))
 exprt dynamic_object(const exprt &pointer);

Original file line number	Diff line number	Diff line change
`@@ -19,7 +19,6 @@ bool escape_domaint::is_tracked(const symbol_exprt &symbol)`
`19`	`19`	`const irep_idt &identifier=symbol.get_identifier();`
`20`	`20`	`if(`
`21`	`21`	`identifier == CPROVER_PREFIX "memory_leak" \|\|`
`22`		`- identifier == CPROVER_PREFIX "malloc_object" \|\|`
`23`	`22`	`identifier == CPROVER_PREFIX "dead_object" \|\|`
`24`	`23`	`identifier == CPROVER_PREFIX "deallocated")`
`25`	`24`	`{`