Squashed 'cbmc/' changes from 768e8a6..ad62682

ad62682 Merge pull request diffblue#2071 from thk123/refactor/split-string-unit-tests
fc8ba88 Revert to aborting precondition for function inputs
3e2ab6f Merge pull request diffblue#2080 from diffblue/java-bytecode-dependency
6ff1eec cbmc: remove dependency on java_bytecode
0bff19b Merge pull request diffblue#2049 from karkhaz/kk-factor-goto-model-processing
79e3b25 Merge pull request diffblue#2084 from tautschnig/has_subtype-test
cd45b0b Test has_subtype on recursive data types
85ac315 Merge pull request diffblue#2082 from thomasspriggs/default_dstring_hash
28c2e8b Merge pull request diffblue#2065 from tautschnig/be-constructor
afa6023 Merge pull request diffblue#2061 from tautschnig/simplify-extractbits
014d151 Factor out getting & processing goto-model
06b3adc Merge pull request diffblue#2077 from peterschrammel/stable-tmp-var-names
0b3170d Stabilize clinit wrapper function type parameters
3cd8bf4 Temporary vars tests for goto-diff
9f0626c  Prefix temporary var names with function id
ca678aa More permissive regression tests regarding tmp var suffixes
47951ca Merge pull request diffblue#2079 from romainbrenguier/bugfix/has-subtype-recursion
dd73b1a Specify default hash function of `dstringt` to STL.
fe8e589 Avoid infinite recursion in has_subtype
00b9bf6 Merge pull request diffblue#2051 from svorenova/generics_tg2717
cd4bfc3 Merge pull request diffblue#2078 from romainbrenguier/bool-literal-in-while-loop
67ea889 Use bool literal in while loop
d229ad9 Merge pull request diffblue#2056 from diffblue/fix-regression-cbmc-memcpy1
506faf0 Refactor a function for base existence
617d388 Utility functions for generic types
c07e6ca Update generic specialization map when replacing pointers
ed26d0a Merge pull request diffblue#2058 from peterschrammel/stable-disjuncts
b663734 Simplify extractbits(concatenation(...))
b091560 Typing and refactoring of simplify_extractbits
49ad1bd Merge pull request diffblue#974 from tautschnig/fix-assert-encoding
16e9599 Merge pull request diffblue#2063 from tautschnig/has-subtype
950f58b Merge pull request diffblue#2060 from tautschnig/opt-local-map
4222a94 Regression tests for unstable instanceof and virtual method disjuncts
b44589e Make disjuncts in instanceof removal independent of class loading
3afff86 Make disjuncts in virtual method removal independent of class loading
a385d9b Allowed split_string to be used on whitespace if not also trying to strip
fe4a642 Merge pull request diffblue#2062 from tautschnig/no-has-deref
145f474 Adding tests for empty string edge cases
07009d4 Refactored test to run all combinations
252c24c Migrate old string utils unit tests
e87edbf Removing wrong elements from the make file
b165c52 make test work on 32-bit Linux
b804570 Merge pull request diffblue#2048 from JohnDumbell/improvement/adding_null_object_id
61f14d8 Merge pull request diffblue#1962 from owen-jones-diffblue/owen-jones-diffblue/simplify-replace-java-nondet
fdee7e8 Merge pull request diffblue#2059 from tautschnig/generalise-test
4625cc5 Extend global has_subexpr to take a predicate as has_subtype does
e9ebd59 has_subtype(type, pred, ns) to search for contained type matching pred
1f1f67f Merge pull request diffblue#1889 from hannes-steffenhagen-diffblue/develop-feature_generate_function_bodies
048c188 Add unit test for java_replace_nondet
0fe48c9 Make remove_java_nondet work before remove_returns
bcc4dc4 Use byte_extract_exprt constructor
a1814a3 Get rid of thin (and duplicate) has_dereference wrapper
4122a28 Test to demonstrate assert bug on alpine
d44bfd3 Also simplify assert structure found on alpine linux
c5cde18 Do not generate redundant if statements in assert expansions
4fb0603 Make is_skip publicly available and use constant argument
5832ffd Negative numbers should also pass the test
3c23b28 Consistently disable simplify_exprt::local_replace_map
da63652 Merge pull request diffblue#2054 from romainbrenguier/bugfix/clear-equations
d77f6a2 Merge pull request diffblue#1831 from NathanJPhillips/feature/class-annotations
60c8296 Clear string_refinement equations (not dependencies)
314ed53 Correcting the value of ID_null_object
751a882 Factor out default CBMC options to static method
6f24009 Can now test for an option being set in optionst
9a8d937 Add to_annotated_type and enable type_checked_cast for annotated_typet
ca77b4e Add test for added annotations
b06a27d Introduce abstract qualifierst base class
e6fb3bf Pretty printing of java_class_typet
e22b95b Fix spurious virtual function related keywords
3ac6d17 Add type_dynamic_cast and friends for java_class_typet
ce1f4d2 Add annotations to java_class_typet, its methods and fields
f84753d Merge pull request diffblue#2042 from hannes-steffenhagen-diffblue/add_deprecate_macro
7a38669 Merge pull request diffblue#2017 from NathanJPhillips/feature/overlay-classes
75a4aec Revert "the deprecation will need to wait until codebase is clean"
67735b5 Disable deprecation warnings by default
0764f77 Merge pull request diffblue#2036 from romainbrenguier/id_array_list
690b606 Merge pull request diffblue#2039 from peterschrammel/fix-duplicate-msg-json-ui
bba17d9 the deprecation will need to wait until codebase is clean
822c757 Regression test for redundant JSON message output
de0644d Only force end of previous message if there actually is one.
5a637bf Merge pull request diffblue#2037 from hannes-steffenhagen-diffblue/add_deprecate_macro
bff456a Merge pull request diffblue#2040 from tautschnig/remove-swp
87ebe90 Remove vim temp file
228c019 Fix duplicate message output in json-ui
0a2c43e Add DEPRECATED to functions documented as \deprecated
47f4b35 interval_sparse_arrayt constructor from array-list
026c4ca Declare an array_list_exprt class
50a2696 Define ID_array_list
513b67a Merge pull request diffblue#2038 from romainbrenguier/bugfix/assign-at-malloc-site
c207106 Test with array of strings
60183a3 Assign string at malloc site
116fffd Add DEPRECATED macro to mark deprecated functions and variables
7952f2c Add option to generate function body to goto-instrument
3d4183a Add ability to overlay classes with new definitions of existing methods
dbc2f71 Improve code and error message in infer_opaque_type_fields
7c0ea4d Tidied up java_class_loader_limitt

git-subtree-dir: cbmc
git-subtree-split: ad62682

Author: smowton

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

CMakeLists.txt

@@ -22,7 +22,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
@@ -75,7 +75,6 @@ set_target_properties(
     mmcc
     pointer-analysis
     solvers
-    string_utils
     test-bigint
     testing-utils
     unit

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/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()
+    {
+    }
+}

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.

regression/cbmc-java/annotations1/MethodAnnotation.class

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

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

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

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);
+  }
+}

regression/cbmc-java/invalid_classpath/Test.class

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

regression/cbmc-java/invalid_classpath/Test.java

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

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);
+  }
+}

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$

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$

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 "$*"`

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

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);
+  }
+}

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

@@ -0,0 +1,16 @@
+CORE
+Test.class
+--classpath `./format_classpath.sh . annotations unmarked-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file unmarked-overlay[\\/]Test\.class$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^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 class Test marked with OverlayClassImplementation but found before original definition$
+^Adding symbol from overlay class
+exists in an overlay class without being marked as an overlay and also exists in the underlying class