Use array_{copy,replace,set} in C library to avoid loops

Author: tautschnig

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)*sizeof(A));
+  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/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;
 }

src/ansi-c/library/string.c

@@ -535,7 +535,10 @@ inline void *memcpy(void *dst, const void *src, size_t n)
   #else
   __CPROVER_assert(__CPROVER_POINTER_OBJECT(dst)!=
                    __CPROVER_POINTER_OBJECT(src), "memcpy src/dst overlap");
-  for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
+  //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
+  char src_n[n];
+  __CPROVER_array_copy(src_n, (char*)src);
+  __CPROVER_array_replace((char*)dst, src_n);
   #endif
   return dst;
 }
@@ -563,7 +566,10 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
   __CPROVER_assert(__CPROVER_POINTER_OBJECT(dst)!=
                    __CPROVER_POINTER_OBJECT(src), "memcpy src/dst overlap");
   (void)size;
-  for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
+  //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
+  char src_n[n];
+  __CPROVER_array_copy(src_n, (char*)src);
+  __CPROVER_array_replace((char*)dst, src_n);
   #endif
   return dst;
 }
@@ -596,8 +602,11 @@ inline void *memset(void *s, int c, size_t n)
   else
     __CPROVER_is_zero_string(s)=0;
   #else
-  char *sp=s;
-  for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
+  //char *sp=s;
+  //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
+  unsigned char s_n[n];
+  __CPROVER_array_set(s_n, (unsigned char)c);
+  __CPROVER_array_replace((unsigned char*)s, s_n);
   #endif
   return s;
 }
@@ -625,8 +634,11 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_
     __CPROVER_is_zero_string(s)=0;
   #else
   (void)size;
-  char *sp=s;
-  for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
+  //char *sp=s;
+  //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
+  unsigned char s_n[n];
+  __CPROVER_array_set(s_n, (unsigned char)c);
+  __CPROVER_array_replace((unsigned char*)s, s_n);
   #endif
   return s;
 }
@@ -655,14 +667,9 @@ inline void *memmove(void *dest, const void *src, size_t n)
   else
     __CPROVER_is_zero_string(dest)=0;
   #else
-  if((const char *)dest>=(const char *)src+n)
-  {
-    for(__CPROVER_size_t i=0; i<n; i++) ((char *)dest)[i]=((const char *)src)[i];
-  }
-  else
-  {
-    for(__CPROVER_size_t i=n; i>0; i--) ((char *)dest)[i-1]=((const char *)src)[i-1];
-  }
+  char src_n[n];
+  __CPROVER_array_copy(src_n, (char*)src);
+  __CPROVER_array_replace((char*)dest, src_n);
   #endif
   return dest;
 }

src/ansi-c/library/unistd.c

@@ -198,14 +198,19 @@ ssize_t read(int fildes, void *buf, size_t nbyte)
   if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
   {
     ssize_t nread;
-    size_t i;
     __CPROVER_assume(0<=nread && (size_t)nread<=nbyte);
 
+#if 0
+    size_t i;
     for(i=0; i<nbyte; i++)
     {
       char nondet_char;
       ((char *)buf)[i]=nondet_char;
     }
+#else
+    char nondet_bytes[nbyte];
+    __CPROVER_array_replace((char*)buf, nondet_bytes);
+#endif
 
     __CPROVER_bool error;
     return error ? -1 : nread;