Merge pull request #8684 from tautschnig/bugfixes/goto-harness-allocate

goto-harness: use __CPROVER_(de)?allocate, not malloc/free

Author: tautschnig

jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -92,7 +92,7 @@ SCENARIO(
           CPROVER_PREFIX "assume(tmp_object_factory <= 20);",
           "char (*nondet_infinite_array_pointer)[INFINITY()];",
           "nondet_infinite_array_pointer = "
-            "ALLOCATE(char [INFINITY()], INFINITY(), false);",
+            CPROVER_PREFIX "allocate(INFINITY(), false);",
           "*nondet_infinite_array_pointer = NONDET(char [INFINITY()]);",
           "int return_array;",
           "return_array = cprover_associate_array_to_pointer_func"

regression/goto-harness/no-malloc-free/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+void test_fn(int *a)
+  // clang-format off
+  __CPROVER_requires((a == (int*)0) || __CPROVER_is_fresh(a, sizeof(*a)))
+  __CPROVER_requires((a != (int*)0) ==> (*a != 5))
+  __CPROVER_ensures((a != (int*)0) ==> (*a == 5))
+  __CPROVER_assigns(*a)
+// clang-format on
+{
+  assert((a == (int *)0) || (*a != 5));
+  if(a != (int *)0)
+  {
+    *a = 5;
+  }
+}

regression/goto-harness/no-malloc-free/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--harness-type call-function --function test_fn
+^\[test_fn.assertion.1\] line 11 assertion \(a == \(int \*\)0\) \|\| \(\*a != 5\): FAILURE$
+^\*\* 1 of \d+ failed
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+CALL.*malloc
+CALL.*free
+--
+Ensure that we do not generate calls to malloc or free.

src/ansi-c/expr2c.cpp

@@ -1156,24 +1156,30 @@ std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
   if(src.operands().size() != 2)
     return convert_norep(src, precedence);
 
-  unsigned p0;
-  std::string op0 = convert_with_precedence(to_binary_expr(src).op0(), p0);
+  const binary_exprt &binary_expr = to_binary_expr(src);
 
   unsigned p1;
-  std::string op1 = convert_with_precedence(to_binary_expr(src).op1(), p1);
+  std::string op1 = convert_with_precedence(binary_expr.op1(), p1);
 
-  std::string dest = "ALLOCATE";
+  std::string dest = CPROVER_PREFIX "allocate";
   dest += '(';
 
+  const typet &type =
+    static_cast<const typet &>(binary_expr.op0().find(ID_C_c_sizeof_type));
   if(
     src.type().id() == ID_pointer &&
-    to_pointer_type(src.type()).base_type().id() != ID_empty)
+    to_pointer_type(src.type()).base_type() == type)
   {
-    dest += convert(to_pointer_type(src.type()).base_type());
+    dest += "sizeof(" + convert(to_pointer_type(src.type()).base_type()) + ')';
     dest+=", ";
   }
+  else
+  {
+    unsigned p0;
+    dest += convert_with_precedence(binary_expr.op0(), p0);
+  }
 
-  dest += op0 + ", " + op1;
+  dest += ", " + op1;
   dest += ')';
 
   return dest;

src/goto-harness/recursive_initialization.cpp

@@ -372,24 +372,6 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr)
   return type_constructor_names.at(key);
 }
 
-symbol_exprt recursive_initializationt::get_malloc_function()
-{
-  auto malloc_sym = goto_model.symbol_table.lookup("malloc");
-  if(malloc_sym == nullptr)
-  {
-    symbolt new_malloc_sym{
-      "malloc",
-      code_typet{
-        {code_typet::parametert{size_type()}}, pointer_type(empty_typet{})},
-      initialization_config.mode};
-    new_malloc_sym.pretty_name = "malloc";
-    new_malloc_sym.base_name = "malloc";
-    goto_model.symbol_table.insert(new_malloc_sym);
-    return new_malloc_sym.symbol_expr();
-  }
-  return malloc_sym->symbol_expr();
-}
-
 bool recursive_initializationt::should_be_treated_as_array(
   const irep_idt &array_name) const
 {
@@ -630,24 +612,6 @@ std::string recursive_initializationt::type2id(const typet &type) const
     return "";
 }
 
-symbol_exprt recursive_initializationt::get_free_function()
-{
-  auto free_sym = goto_model.symbol_table.lookup("free");
-  if(free_sym == nullptr)
-  {
-    symbolt new_free_sym{
-      "free",
-      code_typet{
-        {code_typet::parametert{pointer_type(empty_typet{})}}, empty_typet{}},
-      initialization_config.mode};
-    new_free_sym.pretty_name = "free";
-    new_free_sym.base_name = "free";
-    goto_model.symbol_table.insert(new_free_sym);
-    return new_free_sym.symbol_expr();
-  }
-  return free_sym->symbol_expr();
-}
-
 code_blockt recursive_initializationt::build_pointer_constructor(
   const exprt &depth,
   const symbol_exprt &result)
@@ -724,10 +688,13 @@ code_blockt recursive_initializationt::build_pointer_constructor(
 
   then_case.add(code_declt{local_result});
   const namespacet ns{goto_model.symbol_table};
-  then_case.add(code_function_callt{
+  then_case.add(code_assignt{
     local_result,
-    get_malloc_function(),
-    {*size_of_expr(non_const_pointer_type.base_type(), ns)}});
+    side_effect_exprt{
+      ID_allocate,
+      {*size_of_expr(non_const_pointer_type.base_type(), ns), false_exprt{}},
+      non_const_pointer_type,
+      source_locationt::nil()}});
   initialize(
     dereference_exprt{local_result},
     plus_exprt{depth, from_integer(1, depth.type())},
@@ -869,10 +836,16 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
   {
     body.add(code_ifthenelset{
       equal_exprt{nondet_size, from_integer(array_size, nondet_size.type())},
-      code_function_callt{local_result,
-                          get_malloc_function(),
-                          {mult_exprt{from_integer(array_size, size_type()),
-                                      *size_of_expr(element_type, ns)}}}});
+      code_assignt{
+        local_result,
+        side_effect_exprt{
+          ID_allocate,
+          {mult_exprt{
+             from_integer(array_size, size_type()),
+             *size_of_expr(element_type, ns)},
+           false_exprt{}},
+          mutable_dynamic_array_type,
+          source_locationt::nil()}}});
   }
 
   const symbol_exprt &index_iter = get_fresh_local_symexpr("index");
@@ -942,18 +915,35 @@ bool recursive_initializationt::needs_freeing(const exprt &expr) const
   return true;
 }
 
+code_blockt
+recursive_initializationt::deallocate_code(const exprt &pointer) const
+{
+  code_blockt block;
+  const auto should_track =
+    get_fresh_local_typed_symexpr("mark_deallocated", bool_typet{});
+  block.add(code_declt{should_track});
+  const symbol_exprt deallocated = goto_model.get_symbol_table()
+                                     .lookup_ref(CPROVER_PREFIX "deallocated")
+                                     .symbol_expr();
+  block.add(code_ifthenelset{
+    should_track,
+    code_assignt{
+      deallocated,
+      typecast_exprt::conditional_cast(pointer, deallocated.type())}});
+  return block;
+}
+
 void recursive_initializationt::free_if_possible(
   const exprt &expr,
   code_blockt &body)
 {
   PRECONDITION(expr.id() == ID_symbol);
   const auto expr_id = to_symbol_expr(expr).get_identifier();
   const auto maybe_cluster_index = find_equal_cluster(expr_id);
-  const auto call_free = code_function_callt{get_free_function(), {expr}};
   if(!maybe_cluster_index.has_value())
   {
     // not in any equality cluster -> just free
-    body.add(call_free);
+    body.add(deallocate_code(expr));
     return;
   }
 
@@ -965,7 +955,7 @@ void recursive_initializationt::free_if_possible(
     // in equality cluster but not common origin -> free if not equal to origin
     const auto condition =
       notequal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]};
-    body.add(code_ifthenelset{condition, call_free});
+    body.add(code_ifthenelset{condition, deallocate_code(expr)});
   }
   else
   {
@@ -979,7 +969,7 @@ void recursive_initializationt::free_cluster_origins(code_blockt &body)
 {
   for(auto const &origin : common_arguments_origins)
   {
-    body.add(code_function_callt{get_free_function(), {*origin}});
+    body.add(deallocate_code(*origin));
   }
 }
 

src/goto-harness/recursive_initialization.h

@@ -98,11 +98,6 @@ class recursive_initializationt
   /// \param body: The code block to write initialisation code to.
   void initialize(const exprt &lhs, const exprt &depth, code_blockt &body);
 
-  /// Get the `free` function as symbol expression, and inserts it into the
-  ///   goto-model if it doesn't exist already.
-  /// \return the symbol expression for the `free` function
-  symbol_exprt get_free_function();
-
   static bool is_initialization_allowed(const symbolt &symbol)
   {
     auto const symbol_name = id2string(symbol.name);
@@ -125,11 +120,6 @@ class recursive_initializationt
   type_constructor_namest type_constructor_names;
   std::vector<std::optional<exprt>> common_arguments_origins;
 
-  /// Get the malloc function as symbol exprt,
-  /// and inserts it into the goto-model if it doesn't
-  /// exist already.
-  symbol_exprt get_malloc_function();
-
   bool should_be_treated_as_array(const irep_idt &pointer_name) const;
   std::optional<equal_cluster_idt>
   find_equal_cluster(const irep_idt &name) const;
@@ -275,6 +265,10 @@ class recursive_initializationt
     const exprt &depth,
     code_blockt &body,
     const std::vector<irep_idt> &selection_spec);
+
+  /// Generate code mimicking __CPROVER_deallocate (which is what C's free
+  /// calls) with \p pointer as argument.
+  code_blockt deallocate_code(const exprt &pointer) const;
 };
 
 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H