Fixes and improvements to dynamic memory handling

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;

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;

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);

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;
+}

regression/cbmc/Calloc1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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;

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;

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);

regression/cbmc/Malloc24/main.c

@@ -0,0 +1,47 @@
+#include <stdlib.h>
+
+struct node
+{
+    int value;
+    struct node *next;
+};
+
+struct list
+{
+  int size;
+  struct node *head;
+};
+
+void removeLast(struct list * l)
+{
+  int index = l->size - 1;
+  struct node **current;
+  for(current = &(l->head); index && *current; index--)
+    current = &(*current)->next;
+  *current = (*current)->next;
+  l->size--;
+}
+
+int main () {
+  //build a 2-nodes list
+  struct node *n0 = malloc(sizeof(struct node));
+  struct node *n1 = malloc(sizeof(struct node));
+  struct list *l = malloc(sizeof(struct list));
+  l->size = 2;
+  l->head = n0;
+
+  n0->next=n1;
+  n1->next=NULL;
+
+  //remove last node from list
+
+  //this passes
+  // struct node **current = &(l->head);
+  // current = &(*current)->next;
+  // *current = (*current)->next;
+  // l->size--;
+  //this doesn't
+  removeLast(l);
+
+  __CPROVER_assert(n0->next == NULL , "not NULL");
+}

regression/cbmc/Malloc24/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 4 --pointer-check --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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)

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();

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)));
     }

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"

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();

src/ansi-c/expr2c.cpp

@@ -1115,18 +1115,19 @@ std::string expr2ct::convert_pointer_object_has_type(
   return dest;
 }
 
-std::string expr2ct::convert_malloc(
-  const exprt &src,
-  unsigned &precedence)
+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 op0 = convert_with_precedence(src.op0(), p0);
 
-  std::string dest="MALLOC";
-  dest+='(';
+  unsigned p1;
+  std::string op1 = convert_with_precedence(src.op1(), p1);
+
+  std::string dest = "ALLOCATE";
+  dest += '(';
 
   if(src.type().id()==ID_pointer &&
      src.type().subtype().id()!=ID_empty)
@@ -1135,8 +1136,8 @@ std::string expr2ct::convert_malloc(
     dest+=", ";
   }
 
-  dest+=op0;
-  dest+=')';
+  dest += op0 + ", " + op1;
+  dest += ')';
 
   return dest;
 }
@@ -3656,8 +3657,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)

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);

src/ansi-c/library/cprover.h

@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
 #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;

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;

src/ansi-c/library/stdlib.c

@@ -60,27 +60,39 @@ 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);
-  #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;
-  #endif
-  return res;
+  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(malloc_res) = 1;
+  __CPROVER_zero_string_length(malloc_res) = 0;
+#endif
+
+  return malloc_res;
 }
 
 /* FUNCTION: malloc */
@@ -92,10 +104,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 +133,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;

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';
+  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';