Merge pull request #1834 from diffblue/library-preconditions

Library preconditions
diffblue · Feb 14, 2018 · 7b5dd17 · 7b5dd17
2 parents ef08ae2 + f6f45fc
commit 7b5dd17
Show file tree

Hide file tree

Showing 7 changed files with 200 additions and 122 deletions.
diff --git a/regression/cbmc/strcat1/test.desc b/regression/cbmc/strcat1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.6\] assertion strlen\(A3\) == 4: FAILURE
-\*\* 1 of 8 failed
+\*\* 1 of 9 failed
 --
 ^warning: ignoring
diff --git a/src/ansi-c/library/inet.c b/src/ansi-c/library/inet.c
@@ -12,10 +12,11 @@ in_addr_t __VERIFIER_nondet_in_addr_t();
 in_addr_t inet_addr(const char *cp)
 {
   __CPROVER_HIDE:;
-  (void)*cp;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_addr zero-termination of argument");
+  __CPROVER_precondition(__CPROVER_is_zero_string(cp),
+                         "inet_addr zero-termination of argument");
   #endif
+  (void)*cp;
 
   in_addr_t result=__VERIFIER_nondet_in_addr_t();
   return result;
@@ -37,11 +38,12 @@ int __VERIFIER_nondet_int();
 int inet_aton(const char *cp, struct in_addr *pin)
 {
   __CPROVER_HIDE:;
-  (void)*cp;
-  (void)*pin;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_aton zero-termination of name argument");
+  __CPROVER_precondition(__CPROVER_is_zero_string(cp),
+                         "inet_aton zero-termination of name argument");
   #endif
+  (void)*cp;
+  (void)*pin;
 
   int result=__VERIFIER_nondet_int();
   return result;
@@ -63,10 +65,11 @@ in_addr_t __VERIFIER_nondet_in_addr_t();
 in_addr_t inet_network(const char *cp)
 {
   __CPROVER_HIDE:;
-  (void)*cp;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_network zero-termination of name argument");
+  __CPROVER_precondition(__CPROVER_is_zero_string(cp),
+                         "inet_network zero-termination of name argument");
   #endif
+  (void)*cp;
 
   in_addr_t result=__VERIFIER_nondet_in_addr_t();
   return result;

diff --git a/src/ansi-c/library/netdb.c b/src/ansi-c/library/netdb.c
@@ -7,10 +7,11 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 struct hostent *gethostbyname(const char *name)
 {
   __CPROVER_HIDE:;
-  (void)*name;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(name), "gethostbyname zero-termination of name argument");
+  __CPROVER_precondition(__CPROVER_is_zero_string(name),
+                         "gethostbyname zero-termination of name argument");
   #endif
+  (void)*name;
 
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
   if(error) return 0;

diff --git a/src/ansi-c/library/new.c b/src/ansi-c/library/new.c
@@ -72,30 +72,32 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 inline void __delete(void *ptr)
 {
   __CPROVER_HIDE:;
+  // is it dynamic?
+  __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
+                         "delete argument must be dynamic object");
+  __CPROVER_precondition(__CPROVER_POINTER_OFFSET(ptr)==0,
+                         "delete argument must have offset zero");
+
+  // catch double delete
+  __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, "double delete");
+
+  // catch people who call delete for objects allocated with new[]
+  __CPROVER_precondition(ptr==0 ||
+                         __CPROVER_malloc_object!=ptr ||
+                         !__CPROVER_malloc_is_new_array,
+                         "delete of array object");
+
   // If ptr is NULL, no operation is performed.
   // This is a requirement by the standard, not generosity!
   if(ptr!=0)
   {
-    // is it dynamic?
-    __CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
-                     "delete argument must be dynamic object");
-    __CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,
-                     "delete argument must have offset zero");
-
-    // catch double delete
-    __CPROVER_assert(__CPROVER_deallocated!=ptr, "double delete");
-
-    // catch people who call delete for objects allocated with new[]
-    __CPROVER_assert(__CPROVER_malloc_object!=ptr ||
-                     !__CPROVER_malloc_is_new_array,
-                     "delete of array object");
-
     // non-deterministically record as deallocated
     __CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
     __CPROVER_deallocated=record?ptr:__CPROVER_deallocated;
 
     // detect memory leaks
-    if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0;
+    if(__CPROVER_memory_leak==ptr)
+      __CPROVER_memory_leak=0;
   }
 }
 
@@ -108,22 +110,25 @@ inline void __delete_array(void *ptr)
   __CPROVER_HIDE:;
   // If ptr is NULL, no operation is performed.
   // This is a requirement by the standard, not generosity!
-  if(ptr!=0)
-  {
-    // is it dynamic?
-    __CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
-                     "delete argument must be dynamic object");
-    __CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,
-                     "delete argument must have offset zero");
 
-    // catch double delete
-    __CPROVER_assert(__CPROVER_deallocated!=ptr, "double delete");
+  // is it dynamic?
+  __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
+                         "delete argument must be dynamic object");
+  __CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,
+                         "delete argument must have offset zero");
 
-    // catch people who call delete[] for objects allocated with new
-    __CPROVER_assert(__CPROVER_malloc_object!=ptr ||
-                     __CPROVER_malloc_is_new_array,
-                     "delete[] of non-array object");
+  // catch double delete
+  __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
+                         "double delete");
 
+  // catch people who call delete[] for objects allocated with new
+  __CPROVER_precondition(ptr==0 ||
+                         __CPROVER_malloc_object!=ptr ||
+                         __CPROVER_malloc_is_new_array,
+                         "delete[] of non-array object");
+
+  if(ptr!=0)
+  {
     // non-deterministically record as deallocated
     __CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
     __CPROVER_deallocated=record?ptr:__CPROVER_deallocated;

diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
@@ -162,24 +162,26 @@ inline void free(void *ptr)
   __CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,
                          "free argument has offset zero");
 
-  if(ptr!=0)
-  {
-    // catch double free
-    if(__CPROVER_deallocated==ptr)
-      __CPROVER_assert(0, "double free");
+  // catch double free
+  __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
+                         "double free");
 
-    // catch people who try to use free(...) for stuff
-    // allocated with new[]
-    __CPROVER_assert(__CPROVER_malloc_object!=ptr ||
-                     !__CPROVER_malloc_is_new_array,
-                     "free called for new[] object");
+  // catch people who try to use free(...) for stuff
+  // allocated with new[]
+  __CPROVER_precondition(ptr==0 ||
+                         __CPROVER_malloc_object!=ptr ||
+                         !__CPROVER_malloc_is_new_array,
+                         "free called for new[] object");
 
+  if(ptr!=0)
+  {
     // non-deterministically record as deallocated
     __CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
     if(record) __CPROVER_deallocated=ptr;
 
     // detect memory leaks
-    if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0;
+    if(__CPROVER_memory_leak==ptr)
+      __CPROVER_memory_leak=0;
   }
 }
 
@@ -206,7 +208,7 @@ inline long strtol(const char *nptr, char **endptr, int base)
 {
   __CPROVER_HIDE:;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(nptr),
+  __CPROVER_precondition(__CPROVER_is_zero_string(nptr),
     "zero-termination of argument of strtol");
   #endif
 
@@ -329,7 +331,7 @@ inline char *getenv(const char *name)
 
   (void)*name;
   #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(name),
+  __CPROVER_precondition(__CPROVER_is_zero_string(name),
     "zero-termination of argument of getenv");
   #endif
 
@@ -367,6 +369,9 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
 {
   __CPROVER_HIDE:;
 
+  __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
+                         "realloc argument is dynamic object");
+
   // if ptr is NULL, this behaves like malloc
   if(ptr==0)
     return malloc(malloc_size);
@@ -379,9 +384,6 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
     return malloc(1);
   }
 
-  __CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
-                   "realloc argument is dynamic object");
-
   // this shouldn't move if the new size isn't bigger
   void *res;
   res=malloc(malloc_size);