Generalize ID_malloc to ID_allocate with optional zero-init

tautschnig · tautschnig · commit 7495a325d8fe · 2017-11-02T12:00:55.000Z
__CPROVER_allocate takes two arguments, where the second requests
zero-initialization of the newly allocated object. Thus `calloc` can be
implemented efficiently.
diff --git a/regression/cbmc-with-incr/Malloc17/main.c b/regression/cbmc-with-incr/Malloc17/main.c
@@ -4,7 +4,7 @@ unsigned char* init1()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(1);
+  unsigned char* buffer=__CPROVER_allocate(1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(1*sizeof(unsigned char));
+  unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(sizeof(unsigned char)*1);
+  unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
diff --git a/regression/cbmc-with-incr/Malloc18/main.c b/regression/cbmc-with-incr/Malloc18/main.c
@@ -4,7 +4,7 @@ unsigned char* init()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(size);
+  unsigned char* buffer=__CPROVER_allocate(size, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
diff --git a/regression/cbmc-with-incr/Malloc19/main.c b/regression/cbmc-with-incr/Malloc19/main.c
@@ -22,7 +22,7 @@ int main()
 {
     // Create node
     struct node *nd;
-    nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
+    nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
 
     // Link node
     struct list_head *hd = &(nd->linkage);
diff --git a/regression/cbmc/Calloc1/main.c b/regression/cbmc/Calloc1/main.c
@@ -0,0 +1,9 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int *x=calloc(sizeof(int), 1);
+  assert(*x==0);
+  return 0;
+}
diff --git a/regression/cbmc/Calloc1/test.desc b/regression/cbmc/Calloc1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Malloc17/main.c b/regression/cbmc/Malloc17/main.c
@@ -4,7 +4,7 @@ unsigned char* init1()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(1);
+  unsigned char* buffer=__CPROVER_allocate(1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(1*sizeof(unsigned char));
+  unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(sizeof(unsigned char)*1);
+  unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
diff --git a/regression/cbmc/Malloc18/main.c b/regression/cbmc/Malloc18/main.c
@@ -3,7 +3,7 @@ unsigned char* init()
   unsigned long buffer_size;
   if(buffer_size!=1) return 0;
 
-  unsigned char* buffer=__CPROVER_malloc(buffer_size);
+  unsigned char* buffer=__CPROVER_allocate(buffer_size, 0);
   __CPROVER_assert(buffer!=0, "malloc did not return NULL");
 
   buffer[0]=10;
diff --git a/regression/cbmc/Malloc19/main.c b/regression/cbmc/Malloc19/main.c
@@ -22,7 +22,7 @@ int main()
 {
     // Create node
     struct node *nd;
-    nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
+    nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
 
     // Link node
     struct list_head *hd = &(nd->linkage);
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
@@ -277,7 +277,7 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
     return false;
 
   if(expr.id()==ID_side_effect &&
-     to_side_effect_expr(expr).get_statement()==ID_malloc)
+     to_side_effect_expr(expr).get_statement()==ID_allocate)
     return false;
 
   if(expr.id()==ID_symbol)
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
@@ -232,7 +232,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
     const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
     const irep_idt &statement=side_effect_expr.get_statement();
 
-    if(statement==ID_malloc)
+    if(statement==ID_allocate)
       return flagst::mk_dynamic_heap();
     else
       return flagst::mk_unknown();
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
@@ -298,7 +298,7 @@ void local_may_aliast::get_rec(
     const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
     const irep_idt &statement=side_effect_expr.get_statement();
 
-    if(statement==ID_malloc)
+    if(statement==ID_allocate)
     {
       dest.insert(objects.number(exprt(ID_dynamic_object)));
     }
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -160,7 +160,7 @@ void ansi_c_internal_additions(std::string &code)
     "void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
 
     // malloc
-    "void *__CPROVER_malloc(__CPROVER_size_t size);\n"
+    "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
     "const void *__CPROVER_deallocated=0;\n"
     "const void *__CPROVER_dead_object=0;\n"
     "const void *__CPROVER_malloc_object=0;\n"
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -2271,16 +2271,16 @@ exprt c_typecheck_baset::do_special_functions(
 
     return abs_expr;
   }
-  else if(identifier==CPROVER_PREFIX "malloc")
+  else if(identifier==CPROVER_PREFIX "allocate")
   {
-    if(expr.arguments().size()!=1)
+    if(expr.arguments().size()!=2)
     {
       err_location(f_op);
-      error() << "malloc expects one operand" << eom;
+      error() << "allocate expects two operands" << eom;
       throw 0;
     }
 
-    exprt malloc_expr=side_effect_exprt(ID_malloc);
+    exprt malloc_expr=side_effect_exprt(ID_allocate);
     malloc_expr.type()=expr.type();
     malloc_expr.add_source_location()=source_location;
     malloc_expr.operands()=expr.arguments();
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -1115,17 +1115,20 @@ std::string expr2ct::convert_pointer_object_has_type(
   return dest;
 }
 
-std::string expr2ct::convert_malloc(
+std::string expr2ct::convert_allocate(
   const exprt &src,
   unsigned &precedence)
 {
-  if(src.operands().size()!=1)
+  if(src.operands().size()!=2)
     return convert_norep(src, precedence);
 
   unsigned p0;
   std::string op0=convert_with_precedence(src.op0(), p0);
 
-  std::string dest="MALLOC";
+  unsigned p1;
+  std::string op1=convert_with_precedence(src.op1(), p1);
+
+  std::string dest="ALLOCATE";
   dest+='(';
 
   if(src.type().id()==ID_pointer &&
@@ -1135,7 +1138,7 @@ std::string expr2ct::convert_malloc(
     dest+=", ";
   }
 
-  dest+=op0;
+  dest+=op0+", "+op1;
   dest+=')';
 
   return dest;
@@ -3656,8 +3659,8 @@ std::string expr2ct::convert_with_precedence(
       return
         convert_side_effect_expr_function_call(
           to_side_effect_expr_function_call(src), precedence);
-    else if(statement==ID_malloc)
-      return convert_malloc(src, precedence=15);
+    else if(statement==ID_allocate)
+      return convert_allocate(src, precedence=15);
     else if(statement==ID_printf)
       return convert_function(src, "printf", precedence=16);
     else if(statement==ID_nondet)
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
@@ -214,7 +214,7 @@ class expr2ct
   std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
   // NOLINTNEXTLINE(whitespace/line_length)
   std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
-  std::string convert_malloc(const exprt &src, unsigned &precedence);
+  std::string convert_allocate(const exprt &src, unsigned &precedence);
   std::string convert_nondet(const exprt &src, unsigned &precedence);
   std::string convert_prob_coin(const exprt &src, unsigned &precedence);
   std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_ANSI_C_LIBRARY_CPROVER_H
 
 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
-void *__CPROVER_malloc(__CPROVER_size_t size);
+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;
diff --git a/src/ansi-c/library/new.c b/src/ansi-c/library/new.c
@@ -8,7 +8,7 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   // This just does memory allocation.
   __CPROVER_HIDE:;
   void *res;
-  res=__CPROVER_malloc(malloc_size);
+  res=__CPROVER_allocate(malloc_size, 0);
 
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
@@ -36,7 +36,7 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
   // This just does memory allocation.
   __CPROVER_HIDE:;
   void *res;
-  res=__CPROVER_malloc(size*count);
+  res=__CPROVER_allocate(size*count, 0);
 
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
@@ -60,27 +60,36 @@ inline void abort(void)
 /* FUNCTION: calloc */
 
 #undef calloc
-#undef malloc
 
-inline void *malloc(__CPROVER_size_t malloc_size);
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
+  // realistically, calloc may return NULL,
+  // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
-  void *res;
-  res=malloc(nmemb*size);
+  void *malloc_res;
+  malloc_res=__CPROVER_allocate(nmemb*size, 1);
+
+  // make sure it's not recorded as deallocated
+  __CPROVER_deallocated=(malloc_res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
+
+  // 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?nmemb*size:__CPROVER_malloc_size;
+  __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
+
+  // detect memory leaks
+  __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_memory_leak=record_may_leak?malloc_res:__CPROVER_memory_leak;
+
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_is_zero_string(res)=1;
-  __CPROVER_zero_string_length(res)=0;
-  //for(int i=0; i<nmemb*size; i++) res[i]=0;
-  #else
-  if(nmemb>1)
-    __CPROVER_array_set(res, 0);
-  else if(nmemb==1)
-    for(__CPROVER_size_t i=0; i<size; ++i)
-      ((char*)res)[i]=0;
+  __CPROVER_is_zero_string(malloc_res)=1;
+  __CPROVER_zero_string_length(malloc_res)=0;
   #endif
-  return res;
+
+  return malloc_res;
 }
 
 /* FUNCTION: malloc */
@@ -92,10 +101,10 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 inline void *malloc(__CPROVER_size_t malloc_size)
 {
   // realistically, malloc may return NULL,
-  // and __CPROVER_malloc doesn't, but no one cares
+  // and __CPROVER_allocate doesn't, but no one cares
   __CPROVER_HIDE:;
   void *malloc_res;
-  malloc_res=__CPROVER_malloc(malloc_size);
+  malloc_res=__CPROVER_allocate(malloc_size, 0);
 
   // make sure it's not recorded as deallocated
   __CPROVER_deallocated=(malloc_res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
@@ -121,7 +130,7 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
   __CPROVER_HIDE:;
   void *res;
-  res=__CPROVER_malloc(alloca_size);
+  res=__CPROVER_allocate(alloca_size, 0);
 
   // make sure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
@@ -91,7 +91,8 @@ void cpp_internal_additions(std::ostream &out)
   out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n';
 
   // malloc
-  out << "extern \"C\" void *__CPROVER_malloc(__CPROVER::size_t size);" << '\n';
+  // NOLINTNEXTLINE(whitespace/line_length)
+  out << "extern \"C\" void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);" << '\n';
   out << "extern \"C\" const void *__CPROVER_deallocated=0;" << '\n';
   out << "extern \"C\" const void *__CPROVER_malloc_object=0;" << '\n';
   out << "extern \"C\" __CPROVER::size_t __CPROVER_malloc_size;" << '\n';
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -600,8 +600,10 @@ void goto_convertt::do_java_new(
   }
 
   // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_malloc);
+  side_effect_exprt malloc_expr(ID_allocate);
   malloc_expr.copy_to_operands(object_size);
+  // could use true and git rid of the code below
+  malloc_expr.copy_to_operands(false_exprt());
   malloc_expr.type()=rhs.type();
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
@@ -656,8 +658,10 @@ void goto_convertt::do_java_new_array(
   }
 
   // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_malloc);
+  side_effect_exprt malloc_expr(ID_allocate);
   malloc_expr.copy_to_operands(object_size);
+  // code use true and get rid of the code below
+  malloc_expr.copy_to_operands(false_exprt());
   malloc_expr.type()=rhs.type();
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -761,7 +761,7 @@ void goto_convertt::convert_assign(
     do_java_new_array(lhs, to_side_effect_expr(rhs), dest);
   }
   else if(rhs.id()==ID_side_effect &&
-          rhs.get(ID_statement)==ID_malloc)
+          rhs.get(ID_statement)==ID_allocate)
   {
     // just preserve
     Forall_operands(it, rhs)
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
@@ -670,7 +670,7 @@ void goto_convertt::remove_side_effect(
   else if(statement==ID_cpp_delete ||
           statement==ID_cpp_delete_array)
     remove_cpp_delete(expr, dest, result_is_used);
-  else if(statement==ID_malloc)
+  else if(statement==ID_allocate)
     remove_malloc(expr, dest, result_is_used);
   else if(statement==ID_temporary_object)
     remove_temporary_object(expr, dest, result_is_used);
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -440,18 +440,19 @@ void interpretert::evaluate(
         error() << "nondet not implemented" << eom;
       return;
     }
-    else if(side_effect.get_statement()==ID_malloc)
+    else if(side_effect.get_statement()==ID_allocate)
     {
       if(show)
-        error() << "malloc not fully implemented "
+        error() << "heap memory allocation not fully implemented "
                 << expr.type().subtype().pretty()
                 << eom;
       std::stringstream buffer;
       num_dynamic_objects++;
-      buffer << "interpreter::malloc_object" << num_dynamic_objects;
+      buffer << "interpreter::dynamic_object" << num_dynamic_objects;
       irep_idt id(buffer.str().c_str());
       mp_integer address=build_memory_map(id, expr.type().subtype());
       // TODO: check array of type
+      // TODO: interpret zero-initialization argument
       dest.push_back(address);
       return;
     }
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def

Original file line number	Diff line number	Diff line change
`@@ -22,7 +22,7 @@ int main()`
`22`	`22`	`{`
`23`	`23`	`// Create node`
`24`	`24`	`struct node *nd;`
`25`		`- nd = (struct node *)__CPROVER_malloc(sizeof(struct node));`
	`25`	`+ nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);`
`26`	`26`
`27`	`27`	`// Link node`
`28`	`28`	`struct list_head *hd = &(nd->linkage);`