Merge pull request #795 from tautschnig/array-replace

Implement C library string functions via array_{copy,replace,set}

Author: Daniel Kroening

regression/cbmc/byte_update8/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x=0x01020304;
+  short *p=((short*)&x)+1;
+  *p=0xABCD;
+  assert(x==0xABCD0304);
+  p=(short*)(((char*)&x)+1);
+  *p=0xABCD;
+  assert(x==0xABABCD04);
+}

regression/cbmc/byte_update8/test.desc

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

regression/cbmc/byte_update9/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x=0x01020304;
+  short *p=((short*)&x)+1;
+  *p=0xABCD;
+  assert(x==0x0102ABCD);
+  p=(short*)(((char*)&x)+1);
+  *p=0xABCD;
+  assert(x==0x01ABCDCD);
+}

regression/cbmc/byte_update9/test.desc

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

regression/cbmc/little-endian-array1/main.c

@@ -0,0 +1,30 @@
+#include <stdlib.h>
+
+int *array;
+
+int main()
+{
+  unsigned size;
+  __CPROVER_assume(size==1);
+
+  // produce unbounded array that does not have byte granularity
+  array=malloc(size*sizeof(int));
+  array[0]=0x01020304;
+
+  int array0=array[0];
+  __CPROVER_assert(array0==0x01020304, "array[0] matches");
+
+  char *p=(char *)array;
+  char p0=p[0];
+  char p1=p[1];
+  char p2=p[2];
+  char p3=p[3];
+  __CPROVER_assert(p0==4, "p[0] matches");
+  __CPROVER_assert(p1==3, "p[1] matches");
+  __CPROVER_assert(p2==2, "p[2] matches");
+  __CPROVER_assert(p3==1, "p[3] matches");
+
+  unsigned short *q=(unsigned short *)array;
+  unsigned short q0=q[0];
+  __CPROVER_assert(q0==0x0304, "p[0,1] matches");
+}

regression/cbmc/little-endian-array1/test.desc

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

regression/cbmc/memset1/main.c

@@ -0,0 +1,29 @@
+#include <string.h>
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int A[5];
+  memset(A, 0, sizeof(int)*5);
+  assert(A[0]==0);
+  assert(A[1]==0);
+  assert(A[2]==0);
+  assert(A[3]==0);
+  assert(A[4]==0);
+
+  A[3]=42;
+  memset(A, 0xFFFFFF01, sizeof(int)*3);
+  assert(A[0]==0x01010101);
+  assert(A[1]==0x01010111);
+  assert(A[2]==0x01010101);
+  assert(A[3]==42);
+  assert(A[4]==0);
+
+  int *B=malloc(sizeof(int)*2);
+  memset(B, 2, sizeof(int)*2);
+  assert(B[0]==0x02020202);
+  assert(B[1]==0x02020202);
+
+  return 0;
+}

regression/cbmc/memset1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE
+\*\* 1 of 12 failed \(2 iterations\)
+--
+^warning: ignoring

src/ansi-c/ansi_c_internal_additions.cpp

@@ -244,7 +244,11 @@ void ansi_c_internal_additions(std::string &code)
     // arrays
     // NOLINTNEXTLINE(whitespace/line_length)
     "__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
+    // overwrite all of *dest (possibly using nondet values), even
+    // if *src is smaller
     "void __CPROVER_array_copy(const void *dest, const void *src);\n"
+    // replace at most size-of-*src bytes in *dest
+    "void __CPROVER_array_replace(const void *dest, const void *src);\n"
     "void __CPROVER_array_set(const void *dest, ...);\n"
 
     // k-induction

src/ansi-c/c_typecheck_expr.cpp

@@ -2473,10 +2473,12 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt pointer_offset_expr=exprt(ID_pointer_offset, expr.type());
-    pointer_offset_expr.operands()=expr.arguments();
+    exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
     pointer_offset_expr.add_source_location()=source_location;
 
+    if(expr.type()!=pointer_offset_expr.type())
+      pointer_offset_expr.make_typecast(expr.type());
+
     return pointer_offset_expr;
   }
   else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")

src/ansi-c/expr2c.cpp

@@ -3824,6 +3824,9 @@ std::string expr2ct::convert_code(
   if(statement==ID_array_copy)
     return convert_code_array_copy(src, indent);
 
+  if(statement==ID_array_replace)
+    return convert_code_array_replace(src, indent);
+
   if(statement=="set_may" ||
      statement=="set_must")
     return
@@ -4225,6 +4228,39 @@ std::string expr2ct::convert_code_array_copy(
 
 /*******************************************************************\
 
+Function: expr2ct::convert_code_array_replace
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2ct::convert_code_array_replace(
+  const codet &src,
+  unsigned indent)
+{
+  std::string dest=indent_str(indent)+"ARRAY_REPLACE(";
+
+  forall_operands(it, src)
+  {
+    unsigned p;
+    std::string arg_str=convert_with_precedence(*it, p);
+
+    if(it!=src.operands().begin())
+      dest+=", ";
+    dest+=arg_str;
+  }
+
+  dest+=");";
+
+  return dest;
+}
+
+/*******************************************************************\
+
 Function: expr2ct::convert_code_assert
 
   Inputs:
@@ -4673,9 +4709,6 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()=="buffer_size")
     return convert_function(src, "BUFFER_SIZE", precedence=16);
 
-  else if(src.id()==ID_pointer_offset)
-    return convert_function(src, "POINTER_OFFSET", precedence=16);
-
   else if(src.id()==ID_isnan)
     return convert_function(src, "isnan", precedence=16);
 

src/ansi-c/expr2c_class.h

@@ -204,6 +204,7 @@ class expr2ct
   std::string convert_code_output(const codet &src, unsigned indent);
   std::string convert_code_array_set(const codet &src, unsigned indent);
   std::string convert_code_array_copy(const codet &src, unsigned indent);
+  std::string convert_code_array_replace(const codet &src, unsigned indent);
 
   virtual std::string convert_with_precedence(
     const exprt &src, unsigned &precedence);

src/ansi-c/library/cprover.h

@@ -52,7 +52,7 @@ void CBMC_trace(int lvl, const char *event, ...);
 #endif
 
 // pointers
-//unsigned __CPROVER_POINTER_OBJECT(const void *p);
+unsigned __CPROVER_POINTER_OBJECT(const void *p);
 signed __CPROVER_POINTER_OFFSET(const void *p);
 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
 #if 0
@@ -104,7 +104,8 @@ float __CPROVER_fabsf(float);
 // arrays
 //__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
 void __CPROVER_array_copy(const void *dest, const void *src);
-//void __CPROVER_array_set(const void *dest, ...);
+void __CPROVER_array_set(const void *dest, ...);
+void __CPROVER_array_replace(const void *dest, const void *src);
 
 #if 0
 // k-induction

src/ansi-c/library/stdlib.c

@@ -67,17 +67,18 @@ inline void *malloc(__CPROVER_size_t malloc_size);
 inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
   __CPROVER_HIDE:;
-  __CPROVER_size_t total_size=nmemb*size;
   void *res;
-  res=malloc(total_size);
+  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
-  // there should be memset here
-  //char *p=res;
-  //for(int i=0; i<total_size; i++) p[i]=0;
+  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;
 }