Merge pull request #6838 from tautschnig/cleanup/malloc-0

Document and use malloc(0) behaviour

Author: kroening

doc/cprover-manual/memory-primitives.md

@@ -90,6 +90,63 @@ point into another memory object (such as could happen when running on a real
 machine). To verify that pointers stay within the bounds of their pointees, the
 CBMC option `--pointer-overflow-check` can be used.
 
+### Malloc modelling
+
+CBMC ships a model of `malloc` that seeks to emulate the behaviour of the C
+standard library. This model is configurable to suit the assumptions the
+software under scrutiny may be making. One common assumption, matched by CBMC's
+default configuration, is that dynamic memory allocation always succeeds and
+`malloc` never returns a `NULL` pointer. Code making such an assumption will
+look as follows:
+
+```C
+int *p = malloc(sizeof(int));
+*p = 42; // unconditional dereference, no check for p being NULL
+```
+
+This extends to the case of `malloc(0)`, and CBMC returns a valid pointer to an
+object. The size of that object is zero, implying that any attempt to read from
+or write to this object will result in an out-of-bounds access. The ensuing
+undefined behaviour can be detected by running CBMC with `--pointer-check`.
+
+In an actual execution, however, memory allocation may fail for a number of
+reasons and `malloc` would return a NULL pointer. CBMC's model can, therefore,
+also be configured to fail allocating memory when the requested allocation size
+is larger than representable under CBMC's object-offset model (as described in
+[Memory and pointers in CBMC](#memory-and-pointers-in-cbmc)), or even
+non-deterministically fail (for any size). Any such failure can either result in
+calls to `malloc` returning `NULL`, or reporting such a call as a failed
+property. The following command line options facilitate the above failure
+configurations:
+
+|Flag                    |  Check                                            |
+|------------------------|---------------------------------------------------|
+| `--malloc-fail-null`   |  return NULL when emulating an allocation failure |
+| `--malloc-may-fail`    |  non-deterministically fail to allocate           |
+
+Note that the use of `--malloc-may-fail` also requires `--malloc-fail-null`. The
+following code example demonstrates the effect of these options:
+
+```C
+int error = 0;
+int *p = malloc(sizeof(int));
+if(p != NULL)
+  *p = 42;
+else
+  error = 1;
+```
+
+Under CBMC's default model of `malloc`, the `else` branch is unreachable.
+When running CBMC with `--malloc-fail-null --malloc-may-fail`, `p` would
+non-deterministically be set to `NULL`, making all branches in the above code
+reachable.
+
+These malloc failure options need to be set when the C library model is added to
+the program. Typically this is upon invoking CBMC, but if the user has chosen to
+do so via \ref goto-instrument (using `goto-instrument --add-library`), then the
+malloc failure mode needs to be specified with that `goto-instrument`
+invocation, i.e., as an option to `goto-instrument`.
+
 ## Uninitialized pointers
 
 In verification tools, uninitialized variables are typically treated as having a

doc/cprover-manual/properties.md

@@ -394,30 +394,3 @@ example, replacing functions or setting global variables with the `__CPROVER`
 prefix might make analysis impossible. To avoid doing this by accident, negative
 lookahead can be used. For example, `(?!__).*` matches all names not starting
 with `__`.
-
-### Malloc failure mode
-
-|Flag                    |  Check                                          |
-|------------------------|-------------------------------------------------|
-| `--malloc-fail-null`   |  in case malloc fails return NULL               |
-| `--malloc-fail-assert` |  in case malloc fails report as failed property |
-| `--malloc-may-fail`    |  malloc may non-deterministically fail          |
-
-Calling `malloc` may fail for a number of reasons and the function may return a
-NULL pointer. The users can choose if and how they want the `malloc`-related
-failures to occur. The option `--malloc-fail-null` results in `malloc` returning
-the NULL pointer when failing. The option `--malloc-fail-assert` places
-additional properties inside `malloc` that are checked and if failing the
-verification is terminated (by `assume(false)`). One such property is that the
-allocated size is not too large, i.e. internally representable. When neither of
-those two options are used, CBMC will assume that `malloc` does not fail.
-
-Malloc may also fail for external reasons which are not modelled by CProver. If
-you want to replicate this behaviour use the option `--malloc-may-fail` in
-conjunction with one of the above modes of failure.
-
-These malloc failure options need to be set when the C library model is added to
-the program. Typically this is upon invoking CBMC, but if the user has chosen to
-do so via `goto-instrument --add-library`, then the malloc failure mode needs to
-be specified with that `goto-instrument` invocation, i.e., as an option to
-`goto-instrument`.

src/ansi-c/library/stdlib.c

@@ -503,7 +503,7 @@ void *realloc(void *ptr, __CPROVER_size_t malloc_size)
   if(malloc_size==0)
   {
     free(ptr);
-    return malloc(1);
+    return malloc(0);
   }
 
   // this shouldn't move if the new size isn't bigger