Merge pull request diffblue#381 from diffblue/smowton/merge/develop-2018-04-19

Smowton/merge/develop 2018 04 19

Author: smowton

CMakeLists.txt

@@ -35,7 +35,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     #   Ensure NDEBUG is not set for release builds
     set(CMAKE_CXX_FLAGS_RELEASE "-O2")
     #   Enable lots of warnings
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     #   This would be the place to enable warnings for Windows builds, although
     #   config.inc doesn't seem to do that currently

cbmc/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
 ===
 

cbmc/CMakeLists.txt

@@ -25,7 +25,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     #   Ensure NDEBUG is not set for release builds
     set(CMAKE_CXX_FLAGS_RELEASE "-O2")
     #   Enable lots of warnings
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     #   This would be the place to enable warnings for Windows builds, although
     #   config.inc doesn't seem to do that currently
@@ -78,7 +78,6 @@ set_target_properties(
     mmcc
     pointer-analysis
     solvers
-    string_utils
     test-bigint
     testing-utils
     unit

cbmc/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

cbmc/regression/cbmc-java/annotations1/ClassAnnotation.class

@@ -0,0 +1,23 @@
+@interface ClassAnnotation {
+}
+
+@interface MethodAnnotation {
+}
+
+@interface FieldAnnotation {
+}
+
+@ClassAnnotation
+public class annotations
+{
+    @FieldAnnotation
+    public int x;
+
+    @FieldAnnotation
+    public static int y;
+
+    @MethodAnnotation
+    public void main()
+    {
+    }
+}

cbmc/regression/cbmc-java/annotations1/FieldAnnotation.class

@@ -0,0 +1,12 @@
+CORE
+annotations.class
+--verbosity 10 --show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations
+^Type\.\.\.\.\.\.\.\.: @java::MethodAnnotation \(struct annotations \*\) -> void$
+^Type\.\.\.\.\.\.\.\.: @java::FieldAnnotation int$
+--
+--
+The purpose of the test is ensuring that annotations can be shown in the symbol
+table.

cbmc/regression/cbmc-java/annotations1/MethodAnnotation.class

@@ -0,0 +1,3 @@
+public class Test {
+    public void main() {}
+}

cbmc/regression/cbmc-java/annotations1/annotations.class

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--classpath ./NotHere.jar
+^EXIT=6$
+^SIGNAL=0$
+^the program has no entry point$
+^failed to load class `Test'$
+--
+--
+symex-driven lazy loading should emit "the program has no entry point" but currently doesn't

cbmc/regression/cbmc-java/annotations1/annotations.java

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--classpath ./NotHere
+^EXIT=6$
+^SIGNAL=0$
+^the program has no entry point$
+^failed to load class `Test'$
+--
+--
+symex-driven lazy loading should emit "the program has no entry point" but currently doesn't

cbmc/regression/cbmc-java/annotations1/show_annotation_symbol.desc

@@ -0,0 +1,14 @@
+public class Test
+{
+  public int x;
+
+  public static void main(String[] args)
+  {
+    assert(false);
+  }
+
+  public static void notOverlain()
+  {
+    assert(true);
+  }
+}

cbmc/regression/cbmc-java/invalid_classpath/Test.class

@@ -0,0 +1,4 @@
+package com.diffblue;
+
+public @interface OverlayClassImplementation {
+}

cbmc/regression/cbmc-java/invalid_classpath/Test.java

@@ -0,0 +1,4 @@
+package com.diffblue;
+
+public @interface OverlayMethodImplementation {
+}

cbmc/regression/cbmc-java/invalid_classpath/test-jar.desc

@@ -0,0 +1,14 @@
+import com.diffblue.OverlayClassImplementation;
+import com.diffblue.OverlayMethodImplementation;
+
+@OverlayClassImplementation
+public class Test
+{
+  public int x;
+
+  @OverlayMethodImplementation
+  public static void main(String[] args)
+  {
+    assert(true);
+  }
+}

cbmc/regression/cbmc-java/invalid_classpath/test-path.desc

@@ -0,0 +1,17 @@
+CORE
+Test.class
+--classpath `./format_classpath.sh . annotations correct-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Adding symbol from overlay class:  field 'x'$
+^Adding symbol from overlay class:  method 'java::Test\.<init>:\(\)V'$
+^Field definition for java::Test\.x already loaded from overlay class$
+^Adding symbol from overlay class:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$

cbmc/regression/cbmc-java/overlay-class/Test.class

@@ -0,0 +1,17 @@
+CORE
+Test.class
+--classpath `./format_classpath.sh . annotations . correct-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^Adding symbol from overlay class:  field 'x'$
+^Adding symbol from overlay class:  method 'java::Test\.<init>:\(\)V'$
+^Field definition for java::Test\.x already loaded from overlay class$
+^Adding symbol from overlay class:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$

cbmc/regression/cbmc-java/overlay-class/Test.java

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+unameOut="$(uname -s)"
+case "${unameOut}" in
+    CYGWIN*)    separator=";";;
+    MINGW*)     separator=";";;
+    MSYS*)      separator=";";;
+    Windows*)   separator=";";;
+    *)          separator=":"
+esac
+
+echo -n `IFS=$separator; echo "$*"`

cbmc/regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayClassImplementation.class

@@ -0,0 +1,16 @@
+CORE
+Test.class
+--classpath `./format_classpath.sh annotations correct-overlay .` --verbosity 10
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Adding symbol:  field 'x'$
+^Adding symbol:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^Adding symbol from overlay class
+exists in an overlay class without being marked as an overlay and also exists in the underlying class

cbmc/regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayClassImplementation.java

@@ -0,0 +1,11 @@
+import com.diffblue.OverlayClassImplementation;
+import com.diffblue.OverlayMethodImplementation;
+
+public class Test
+{
+  @OverlayMethodImplementation
+  public static void main(String[] args)
+  {
+    assert(false);
+  }
+}