Add option to generate function body to goto-instrument

Author: hannes-steffenhagen-diffblue

CHANGELOG

@@ -1,3 +1,10 @@
+5.9
+===
+* GOTO-INSTRUMENT: --generate-function-body can be used to
+  generate bodies for functions that don't have a body
+  in the goto code. This supercedes the functionality
+  of --undefined-function-is-assume-false
+
 5.8
 ===
 

doc/cbmc-user-manual.md

@@ -2014,6 +2014,164 @@ Flag                         |  Check
 `--uninitialized-check`      |  add checks for uninitialized locals (experimental)
 `--error-label label`        |  check that given label is unreachable
 
+#### Generating 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` option, that takes a
+regular expression (in [ECMAScript syntax]
+(http://en.cppreference.com/w/cpp/regex/ecmascript)) that describes the names of
+the functions to generate. Note that this will only generate bodies for
+functions that do not already have one; If one wishes to replace the body of a
+function with an existing definition, the `--remove-function-body` option can be
+used to remove the body of the function prior to generating a new one.
+
+The shape of the stub itself can be chosen with the
+`--generate-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)
+ `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 \
+      --generate-function-body '(?!__).*_error' \
+      --generate-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
+generation.
+
+
+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 `--generate-function-body` option and indicate which globals and
+function parameters should be set to nondet. All regular expressions require
+exact matches (i.e. the regular expression `a|b` 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
+      --generate-function-body do_something_with_complex
+      --generate-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();
+      }
+      AGlobalComplex.real = nondet_double();
+      AGlobalComplex.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

regression/goto-instrument/generate-function-body-assert-false-assume-false/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+void crashes_program(void);
+
+int main(void)
+{
+  int flag;
+  if(flag)
+  {
+    crashes_program();
+    assert(0);
+  }
+  return 0;
+}

regression/goto-instrument/generate-function-body-assert-false-assume-false/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body crashes_program --generate-function-body-options assert-false-assume-false
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion 0: SUCCESS$
+^\[crashes_program.assertion.1\] assertion false: FAILURE$

regression/goto-instrument/generate-function-body-assert-false/main.c

@@ -0,0 +1,6 @@
+void do_not_call_this(void);
+
+int main(void)
+{
+  do_not_call_this();
+}

regression/goto-instrument/generate-function-body-assert-false/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body do_not_call_this --generate-function-body-options assert-false
+^EXIT=10$
+^SIGNAL=0$
+^\[do_not_call_this.assertion.1\] assertion false: FAILURE$
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-assume-false/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+void will_not_return(void);
+
+int main(void)
+{
+  will_not_return();
+  assert(0);
+}

regression/goto-instrument/generate-function-body-assume-false/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body will_not_return --generate-function-body-options assume-false
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-complex-struct/main.c

@@ -0,0 +1,45 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct ComplexStruct
+{
+  struct
+  {
+    int some_variable;
+    const int some_constant;
+  } struct_contents;
+  union {
+    int some_integer;
+    double some_double;
+  } union_contents;
+  struct ComplexStruct *pointer_contents;
+};
+
+void havoc_complex_struct(struct ComplexStruct *p);
+
+int main(void)
+{
+  struct ComplexStruct child_struct = {{11, 21}, {.some_integer = 31}, NULL};
+  struct ComplexStruct main_struct = {
+    {10, 20}, {.some_double = 13.0}, &child_struct};
+  assert(main_struct.pointer_contents->struct_contents.some_variable == 11);
+  assert(main_struct.struct_contents.some_variable == 10);
+  assert(main_struct.struct_contents.some_constant == 20);
+  assert(
+    main_struct.union_contents.some_double < 14.0 &&
+    main_struct.union_contents.some_double > 12.0);
+
+  havoc_complex_struct(&main_struct);
+
+  // everything (except constants) in the main struct was havocced
+  assert(main_struct.pointer_contents->struct_contents.some_variable == 11);
+  assert(main_struct.struct_contents.some_variable == 10);
+  assert(main_struct.struct_contents.some_constant == 20);
+  assert(
+    main_struct.union_contents.some_double < 14.0 &&
+    main_struct.union_contents.some_double > 12.0);
+  // the child struct was NOT havocced because we can't follow pointers
+  assert(child_struct.struct_contents.some_variable == 11);
+  assert(child_struct.union_contents.some_integer == 31);
+  assert(!child_struct.pointer_contents);
+}

regression/goto-instrument/generate-function-body-complex-struct/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--generate-function-body 'havoc_complex_struct' --generate-function-body-options 'havoc,params:.*'
+^SIGNAL=0$
+^EXIT=10$
+\[main.assertion.1\] assertion main_struct.pointer_contents->struct_contents.some_variable == 11: SUCCESS
+\[main.assertion.2\] assertion main_struct.struct_contents.some_variable == 10: SUCCESS
+\[main.assertion.3\] assertion main_struct.struct_contents.some_constant == 20: SUCCESS
+\[main.assertion.4\] assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: SUCCESS
+\[main.assertion.5\] assertion main_struct.pointer_contents->struct_contents.some_variable == 11: FAILURE
+\[main.assertion.6\] assertion main_struct.struct_contents.some_variable == 10: FAILURE
+\[main.assertion.7\] assertion main_struct.struct_contents.some_constant == 20: SUCCESS
+\[main.assertion.8\] assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: FAILURE
+\[main.assertion.9\] assertion child_struct.struct_contents.some_variable == 11: SUCCESS
+\[main.assertion.10\] assertion child_struct.union_contents.some_integer == 31: SUCCESS
+\[main.assertion.11\] assertion !child_struct.pointer_contents: SUCCESS
+^VERIFICATION FAILED$

regression/goto-instrument/generate-function-body-const-pointer-to-non-const/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void change_pointer_target_of_const_pointer(
+  int *const constant_pointer_to_nonconst);
+
+int main(void)
+{
+  int x = 10;
+  change_pointer_target_of_const_pointer(&x);
+  assert(x == 10);
+  return 0;
+}

regression/goto-instrument/generate-function-body-const-pointer-to-non-const/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--generate-function-body change_pointer_target_of_const_pointer --generate-function-body-options havoc,params:.*
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion x == 10: FAILURE$
+--

regression/goto-instrument/generate-function-body-havoc-globals/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int global = 10;
+const int constant_global = 10;
+
+void touches_globals(void);
+
+int main(void)
+{
+  touches_globals();
+  assert(global == 10);
+  assert(constant_global == 10);
+}

regression/goto-instrument/generate-function-body-havoc-globals/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--generate-function-body touches_globals --generate-function-body-options 'havoc,globals:(?!__).*'
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion global == 10: FAILURE$
+^\[main.assertion.2\] assertion constant_global == 10: SUCCESS$
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void touches_parameter(int *param, const int *const_param);
+
+int main(void)
+{
+  int parameter = 10;
+  int constant_parameter = 10;
+  touches_parameter(&parameter, &constant_parameter);
+  assert(parameter == 10);
+  assert(constant_parameter == 10);
+}

regression/goto-instrument/generate-function-body-havoc-params/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--generate-function-body touches_parameter --generate-function-body-options 'havoc,params:.*'
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] assertion parameter == 10: FAILURE$
+^\[main.assertion.2\] assertion constant_parameter == 10: SUCCESS$
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-pointer-to-pointer-to-const/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+void change_target_of_pointer_to_pointer_to_const(
+  const int **pointer_to_pointer_to_const);
+
+int main(void)
+{
+  int x = 10;
+  int *px = &x;
+  assert(*px == 10);
+  change_target_of_pointer_to_pointer_to_const(&px);
+  assert(x == 10);
+  assert(*px == 10);
+}

regression/goto-instrument/generate-function-body-pointer-to-pointer-to-const/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--generate-function-body change_target_of_pointer_to_pointer_to_const --generate-function-body-options havoc,params:.*
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] assertion \*px == 10: SUCCESS$
+^\[main.assertion.2\] assertion x == 10: SUCCESS$
+^\[main.assertion.3\] assertion \*px == 10: FAILURE$
+--