WIP Add some information about new option to the manual

Author: hannes-steffenhagen-diffblue

doc/cbmc-user-manual.md

@@ -2014,6 +2014,162 @@ Flag                         |  Check
 `--uninitialized-check`      |  add checks for uninitialized locals (experimental)
 `--error-label label`        |  check that given label is unreachable
 
+#### Generating/Replacing function bodies
+
+Sometimes implementations for called functions are not available in the goto
+program, or it is desirable to replace bodies of functions with certain
+predetermined stubs (for example to confirm that these functions are never
+called, or to indicate that these functions will never return). For this purpose
+goto-instrument provides the `--generate-function-body` and
+`--replace-function-body` options, that take a regular expression (in
+[ECMAScript syntax](http://en.cppreference.com/w/cpp/regex/ecmascript)) that
+describes the names of the functions to generate or replace, the difference
+being that `--generate-function-body` will only generate bodies of functions
+that do not already have one, whereas `--replace-function-body` will do this and
+in addition also replace existing bodies of functions with the stub.
+
+The shape of the stub itself can be chosen with the `--replace-function-body-options`
+parameter, which can take the following values:
+
+ Option                      | Result
+-----------------------------|-------------------------------------------------------------
+ `nondet-return`             | Do nothing and return a nondet result (this is the default)
+ `empty`                     | Delete the body of the function
+ `assert-false`              | Make the body contain an assert(false)
+ `assume-false`              | Make the body contain an assume(false)
+ `assert-false-assume-false` | Combines assert-false and assume-false
+ `havoc`                     | Set the contents of parameters and globals to nondet
+
+The various combinations of assert-false and assume-false can be used to
+indicate that functions shouldn't be called, that they will never return or
+both.
+
+Example: We have a program like this:
+    
+    // error_example.c
+    #include <stdlib.h>
+    
+    void api_error(void);
+    void internal_error(void);
+    
+    int main(void)
+    {
+      int arr[10] = {1,2,3,4,5, 6, 7, 8, 9, 10};
+      int sum = 0;
+      for(int i = 1; i < 10; ++i)
+      {
+        sum += arr[i];
+      }
+      if(sum != 55)
+      {
+        // we made a mistake when calculating the sum
+        internal_error();
+      }
+      if(rand() < 0)
+      {
+        // we think this cannot happen
+        api_error();
+      }
+      return 0;
+    }
+
+Now, we can compile the program and detect that the error functions are indeed
+called by invoking these commands
+
+    goto-cc error_example.c -o error_example.goto
+    # Replace all functions ending with _error
+    # (Excluding those starting with __)
+    # With ones that have an assert(false) body
+    goto-instrument error_example.goto error_example_replaced.goto \
+      --replace-function-body '(?!__).*_error' \
+      --replace-function-body-options assert-false
+    cbmc error_example_replaced.goto
+
+Which gets us the output
+
+> ** Results:
+> [internal_error.assertion.1] assertion false: FAILURE
+> [api_error.assertion.1] assertion false: FAILURE
+> 
+> 
+> ** 2 of 2 failed (2 iterations)
+> VERIFICATION FAILED
+
+As opposed to the verification success we would have gotten without the
+replacement
+
+
+The havoc option takes further parameters `globals` and `params` with this
+syntax: `havoc[,globals:<regex>][,params:<regex>]` (where the square brackets
+indicate an optional part). The regular expressions have the same format as the
+those for the `--replace-function-body` and `--generate-function-body` options
+and indicate which globals and function parameters should be set to nondet. All
+regular expressions require exact matches (i.e. the regular expression `ab?`
+will match 'a' and 'b' but not 'adrian' or 'bertha').
+
+Example: With a C program like this
+
+    struct Complex {
+      double real;
+      double imag;
+    };
+    
+    struct Complex AGlobalComplex;
+    int do_something_with_complex(struct Complex *complex);
+
+And the command line
+
+    goto-instrument in.goto out.goto
+      --replace-function-body do_something_with_complex
+      --replace-function-body-options
+        'havoc,params:.*,globals:AGlobalComplex'
+
+The goto code equivalent of the following will be generated:
+
+    int do_something_with_complex(struct Complex *complex)
+    {
+      if(complex)
+      {
+        complex->real = nondet_double();
+        complex->imag = nondet_double();
+      }
+      return nondet_int();
+    }
+
+A note on limitations: Because only static information is used for code
+generation, arrays of unknown size and pointers will not be affected by this;
+Which means that for code like this:
+
+    struct Node {
+      int val;
+      struct Node *next;
+    };
+    
+    void do_something_with_node(struct Node *node);
+
+Code like this will be generated:
+
+    void do_something_with_node(struct Node *node)
+    {
+       if(node)
+       {
+         node->val = nondet_int();
+         node->next = nondet_0();
+       }
+    }
+
+Note that no attempt to follow the `next` pointer is made. If an array of
+unknown (or 0) size is encountered, a diagnostic is emitted and the array
+is not further examined.
+
+Some care must be taken when choosing the regular expressions for globals and
+functions. Names starting with `__` are reserved for internal purposes; For
+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 `__`.
+
+
 \subsection man_instrumentation-api The CPROVER API Reference
 
 The following sections summarize the functions available to programs