Squashed 'cbmc/' changes from 207b801..7202003

7202003 Merge branch 'develop' of github.com:diffblue/cbmc into CBMC_subtree_2018-04-10
768e8a6 Merge pull request diffblue#2009 from romainbrenguier/solvers/sparse-arrays-in-get
69f6e7b Merge pull request diffblue#2032 from tautschnig/replace-rename-performance
ec43b00 Merge pull request diffblue#2026 from tautschnig/sat-clean
64b336a Refactor interval_sparse_array::concretize
5392645 Reserve size of array in concretize
8277e92 Stop using concretize_array_expr in unit tests
1a08772 Tests where model involves long strings
a6c4010 Stop using concretize_arrays_in_expression
6d87233 Use concretize instead of fill_in_array
052d503 Use get_array in get_char_array_and_concretize
8ed138b Remove unused header
c58ac60 Avoid copy in ranged for loops over expressions
beff419 Use sparse arrays in get_array
9b286d9 Use sparse arrays in string_refinement::get
037f631 Refactor string_refinementt::get
dfc584a Add concretize function for interval_sparse_array
cb10550 Use sparse arrays in substitute_array_access
ce4c008 Remove plus_exprt_with_overflow_check
4779b25 Get rid of calls to plus_exprt_with_overflow
c40b836 Truncate string concatenations in case of overflow
c52c813 Add a sum_overflows function
0d03591 Add an `at` function for access in sparse arrays
848dd95 Add an interval_sparse_array::of_expr function
5f07bf0 Initialization of sparse array from array-list
5b4d618 Reduce number of constraints in format
ede2fa1 Clear string_dependencies in calls to dec_solve
d483c81 Initialize sparse array from array_exprt
a914153 Use map instead of vector for sparse array entries
20d2445 Remove unused rename(expr, old_id, new_id)
430d402 Use exprt::depth_iterator in rename_symbolt
54e5b85 Use a const expr to avoid unnecessary detach
6f71ff6 replace_symbolt: stop early if there is nothing to replace with
1dbb162 Clean locally built SAT solver objects
28c076b Merge pull request diffblue#2013 from LAJW/lajw/java-no-load-class
e6a9127 Merge pull request diffblue#2020 from tautschnig/sat-cleanup
70741ff Remove support for Precosat
2aa81eb Remove support for SMVSAT
a0fd3f7 Remove support for Limmat as a SAT solver
28cca9c Remove unused DIMACS parser
1d81306 Merge pull request diffblue#2015 from tautschnig/fix-smt2_solver-clean
392144d Makefiles: Place .d suffix used for dependencies in DEPEXT variable
839d32a smt2_solver.{o,d} should be removed by "make clean"
48e427a Merge pull request diffblue#1979 from romainbrenguier/regression/fix-indexOf-test
c2f3726 Merge pull request diffblue#1976 from romainbrenguier/regression/activate-dependency-tests
42ecfa2 Add --java-no-load-class option
69fb74a Merge pull request diffblue#1995 from tautschnig/byte-update-soundness
aa766ae Set string-max-length in indexOf test
988b818 Merge pull request diffblue#1990 from tautschnig/missing-header
8300147 Abort on byte_update(pointer)
4a8d9b4 Include missing header
a695814 Merge pull request diffblue#1986 from thk123/revert/1816/overlay-classes
9933b58 Revert "Merge pull request diffblue#1816 from NathanJPhillips/feature/overlay-methods"
cd9b839 Revert "Merge pull request diffblue#1982 from NathanJPhillips/bugfix/load-object-once"
58beeb4 Merge pull request diffblue#1978 from svorenova/lambda_tg2478_cont
1e3a9cd Merge pull request diffblue#1980 from NathanJPhillips/tests/irept
772b603 Merge pull request diffblue#1982 from NathanJPhillips/bugfix/load-object-once
0902ae7 Tests to demonstrate expected sharing behaviour of irept
2239ec1 Unit test of irept's public API
81ac259 Prevent test running on symex-driven lazy loading
eae194f Allow incorrect paths for jar files on the classpath without crashing
6749fd0 Tests to ensure invalid values in the classpath are ignored
3c95aa1 Prevent attempting to load any class more than once
c520331 Unit test to show java.lang.Object can be loaded from an explicit model
05a7b4a Merge pull request diffblue#1981 from smowton/smowton/cleanup/missing-docstring
e4dc2aa Merge pull request diffblue#1946 from thk123/feature/TG-1811/unit-tests-for-invokedynamic-static-lambda
2b53d3b Merge pull request diffblue#1983 from svorenova/lambda_tg2478_fix
f428247 Tidying up for lambdas
f3b1379 Merge pull request diffblue#1975 from romainbrenguier/bugfix/literal-length-TG2878
7d4441d Regression test for lambda in a package
7366fda Format class name for lambda method handles
7db42c0 Add missing Doxygen parameter description
31fa0fe Addressing review comments
2a0927c Merge pull request diffblue#1643 from NathanJPhillips/bugfix/string-solver-function-type-mistake
229d1ee Merge pull request diffblue#1977 from romainbrenguier/bugfix/string-equals-TG-2179
97a6713 Merge pull request diffblue#1816 from NathanJPhillips/feature/overlay-methods
e2d4b09 Updates for merge
674c9f0 Activate tests for StringBuffer concat in loops
a997ffb Add verification test for String.equals
1ab596d Merge commit '3b8120f3a8c9ed3a343493a44ac454ae265946c1' into develop
f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327
55d36b5 Fix code for String.equals
baf33f8 Added regression tests
9984fc1 Add ability to overlay classes with new definitions of existing methods
66c529c Tidied up java_class_loader_limitt
397c14e Correcting typos and adding documentation to unit tests
54f1c54 Adding checks for the super class of the generated class
df895d3 Temp checkin for checking components
44a5dcb Adding check for inheritance
28bfc37 Amending path to reflect new location
e27151b Correcting typo in the scenario name
d7356be Modified behaviour to find function calls
ac33761 Use raw strings to avoid unnecessary escaping
4201db9 Adding tests for static lambdas
f9adaa6 Adding tests for member methods
5f5994b Pull out the logic for getting the inital assignment
7f843a7 Add natural language explanation of the test's checks
fa27117 Introduce tests for lambdas that are member variables
8999cf6 Added utiltity for getting this member components
3e0e12e Adding tests for the other two returning lambdas that don't capture
f3ddee6 Adding tests to verify the return of the lambda wrapper method
db6756e Adding checks for parameters of the called function
d2ed92b Adding test for lambda taking array parameters
d171f64 Swap finding variable values to use regex
99c21ed Extended find pointer assignment to take a regex
5610aca Added unit test for lambda assigned
7b0cee1 Refactored test method to allow reuse
bea730d Adding utility for verifying a set of statements contains a function call
ee2179c Introduce checks the the function body for Execute calls the correct lambda
2348d10 Adding unit test for checking local lambda conversion
46fa176 Extending require utilities to be used in test
6df8d6b Extended require_goto_statements to provide meaningful errors
39282a6 Add debug information for working directory
770eb2a Remove methods without a implementation or usage
5cbb758 Merge pull request diffblue#1937 from svorenova/lambda_tg2711
8cfd9bf Merge pull request diffblue#1968 from smowton/smowton/cleanup/remove-exceptions-clarity
6ca3272 Merge pull request diffblue#1973 from karkhaz/kk-c++2a-fixes
212da75 Making members of a test utility class non-const
d57fe53 Renaming the folder with lambda unit tests
823f2a7 Adding a unit test for lambda method handles in class symbol
8b172b4 Adding a utility function for lambda method handles in struct
844bb20 Pulling out a utility function to a separate file
3585f73 Updating unit tests for parsing lambda method table
078dc0f Updating a utility function
a8ac3d4 Pass lambda method handles to method instruction conversion
bf04c93 Add lambda method handles during class conversion
a518393 Introduce lambda method handles in java class type
37afd9a Store the full method reference of lambda method handles
0a49697 Store bootstrap method index for invokedynamic instructions
56c9c02 Add test for string literals length
af958f0 Correct length field of string literals
a190534 Remove-exceptions: make lambda types explicit
b052a4d Fix warnings emitted by C++2a compiler
20eaf21 Fix type of call to forName

git-subtree-dir: cbmc
git-subtree-split: 7202003985a99fb6563cf4d0fb8e7f2c727cc040

Author: Owen Jones

regression/cbmc-java/lambda3/LambdaTest/Lamb1.class

@@ -0,0 +1,16 @@
+package LambdaTest;
+
+interface Lamb1 {
+  public Integer lambFunc1(Integer x);
+}
+
+class Test {
+
+  public static Integer recvLambda(Integer y, Integer z) {
+    Lamb1 lmb1 = (x) -> x = y + z; // Initializing in a lambda statement
+    if (lmb1 != null && z != null) {
+      return lmb1.lambFunc1(y);
+    }
+    return lmb1.lambFunc1(z);
+  }
+}

regression/cbmc-java/lambda3/LambdaTest/Test.class

@@ -0,0 +1,8 @@
+CORE
+LambdaTest/Test.class
+--show-symbol-table --function LambdaTest.Test.recvLambda
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This is to verify that parsing lambdas in a package does not crash.

regression/cbmc-java/lambda3/LambdaTest/Test.java

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5  --verbosity 10  --property "java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1"
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5  --verbosity 10  --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-java/lambda3/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 Test.class
 --refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5  --verbosity 10
 ^EXIT=10$

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5  --verbosity 10 --property "java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1"
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5  --verbosity 10 --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 5  --verbosity 10
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 Test.class
 --refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.stringNonDet --depth 10000 --unwind 5 --verbosity 10
 ^EXIT=10$

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc

@@ -1,3 +1,6 @@
+// Uses CProverString, must be compiled with ../cprover/CProverString.java
+import org.cprover.*;
+
 public class Test {
     public static void check(int i, String s) {
         String t = "Hello World";
@@ -15,4 +18,49 @@ else if (i==4)
         else if (i==5)
             assert(s.equals(x));
     }
+
+    public static boolean referenceImplementation(String s, Object o) {
+        if (! (o instanceof String))
+            return false;
+
+        String s2 = (String) o;
+        if (s.length() != s2.length())
+            return false;
+
+        for (int i = 0; i < s.length(); i++) {
+            if (CProverString.charAt(s, i) != CProverString.charAt(s2, i))
+                return false;
+        }
+
+        return true;
+    }
+
+    public static boolean verifyNonNull(String s, Object o) {
+        // Filter
+        if (s == null || o == null)
+            return false;
+
+        // Act
+        boolean result = s.equals(o);
+        boolean referenceResult = referenceImplementation(s, o);
+
+        // Assert
+        assert result == referenceResult;
+
+        // Return
+        return result;
+    }
+
+    public static boolean verify(String s, Object o) {
+        // Act
+        boolean result = s.equals(o);
+        boolean referenceResult = referenceImplementation(s, o);
+
+        // Assert
+        assert result == referenceResult;
+
+        // Return
+        return result;
+    }
+
 }

regression/jbmc-strings/StringConcat/test_string_nondet.desc

@@ -3,10 +3,10 @@ Test.class
 --refine-strings --string-max-length 40 --function Test.check
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 6 .* SUCCESS
-assertion at file Test.java line 8 .* FAILURE
-assertion at file Test.java line 10 .* SUCCESS
-assertion at file Test.java line 12 .* FAILURE
-assertion at file Test.java line 14 .* SUCCESS
-assertion at file Test.java line 16 .* FAILURE
+assertion at file Test.java line 9 .* SUCCESS
+assertion at file Test.java line 11 .* FAILURE
+assertion at file Test.java line 13 .* SUCCESS
+assertion at file Test.java line 15 .* FAILURE
+assertion at file Test.java line 17 .* SUCCESS
+assertion at file Test.java line 19 .* FAILURE
 --

regression/jbmc-strings/StringEquals/Test.class

@@ -0,0 +1,11 @@
+KNOWNBUG
+Test.class
+--refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --java-throw-runtime-exceptions
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 60 .* SUCCESS
+--
+--
+null case not handled currently
+TG-2179
+

regression/jbmc-strings/StringEquals/Test.java

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --string-max-input-length 20 --string-max-length 100 --unwind 30 --function Test.verifyNonNull
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 48 .* SUCCESS

regression/jbmc-strings/StringEquals/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --java-assume-inputs-non-null
+--refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --string-max-length 100 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/jbmc-strings/StringEquals/test_verify.desc

@@ -0,0 +1,12 @@
+public class Test {
+    public static int check(int i) {
+        String s = "\u0000";
+
+        if (i == 0)
+            assert(s.length() == 1);
+        else if (i == 1)
+            assert(s.length() != 1);
+
+        return s.length();
+    }
+}

regression/jbmc-strings/StringEquals/test_verify_non_null.desc

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings  --function Test.check
+assertion at file Test.java line 6 .* SUCCESS
+assertion at file Test.java line 8 .* FAILURE
+^EXIT=10$
+^SIGNAL=0$

regression/jbmc-strings/StringIndexOf/test.desc

@@ -0,0 +1,41 @@
+import org.cprover.CProverString;
+
+public class Test {
+    public static void check(String s, String t) {
+        // Filter
+        if(s == null || t == null)
+            return;
+
+        // Act
+        String u = s.concat(t);
+
+        // Filter out
+        if(u.length() < 3_000_000)
+            return;
+        if(CProverString.charAt(u, 500_000) != 'a')
+            return;
+        if(CProverString.charAt(u, 2_000_000) != 'b')
+            return;
+
+        // Assert
+        assert(false);
+    }
+
+    public static void checkAbort(String s, String t) {
+        // Filter
+        if(s == null || t == null)
+            return;
+
+        // Act
+        String u = s.concat(t);
+
+        // Filter out
+        if(u.length() < 67_108_864)
+            return;
+        if(CProverString.charAt(u, 2_000_000) != 'b')
+            return;
+
+        // Assert
+        assert(false);
+    }
+}

regression/jbmc-strings/literal-length/Test.class

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --function Test.check --string-max-input-length 2000000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 21 .* FAILURE
+--
+--
+This checks that the solver manage to violate assertions even when this requires
+some very long strings, as long as they don't exceed the arbitrary limit that
+is set by the solver (64M characters).

regression/jbmc-strings/literal-length/Test.java

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--refine-strings --function Test.checkAbort
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+This tests should abort, because concretizing a string of the required
+length may take to much memory.

regression/jbmc-strings/literal-length/test.desc

@@ -627,6 +627,8 @@ void bmct::setup_unwind()
 /// \param message: used for logging
 /// \param driver_configure_bmc: function provided by the driver program,
 ///   which applies driver-specific configuration to a bmct before running.
+/// \param callback_after_symex: optional callback to be run after symex.
+///   See class member `bmct::driver_callback_after_symex` for details.
 int bmct::do_language_agnostic_bmc(
   const optionst &opts,
   abstract_goto_modelt &model,

regression/jbmc-strings/long_string/Test.class

@@ -27,6 +27,7 @@ ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD,$(BUILD_ENV_)),)
   # Linux-ish
   LIBEXT = .a
   OBJEXT = .o
+  DEPEXT = .d
 ifeq ($(BUILD_ENV_),MinGW)
   EXEEXT = .exe
 else
@@ -99,6 +100,7 @@ else ifeq ($(BUILD_ENV_),Cygwin)
   # use these for Cygwin:
   LIBEXT = .a
   OBJEXT = .o
+  DEPEXT = .d
   EXEEXT = .exe
   CFLAGS ?= -Wall -O2
   CXXFLAGS ?= -Wall -O2
@@ -131,6 +133,7 @@ else ifeq ($(BUILD_ENV_),MSVC)
   # use these for Visual Studio:
   LIBEXT = .lib
   OBJEXT = .obj
+  DEPEXT = .dep
   EXEEXT = .exe
   CFLAGS ?= /W3 /O2 /GF
   CXXFLAGS ?= /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF
@@ -159,18 +162,14 @@ else
 endif
 
 # select default solver to be minisat2 if no other is specified
-ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT),)
   MINISAT2 = ../../minisat-2.2.1
 endif
 
 ifneq ($(IPASIR),)
   CP_CXXFLAGS += -DHAVE_IPASIR
 endif
 
-ifneq ($(PRECOSAT),)
-  CP_CXXFLAGS += -DHAVE_PRECOSAT
-endif
-
 ifneq ($(PICOSAT),)
   CP_CXXFLAGS += -DHAVE_PICOSAT
 endif
@@ -213,7 +212,7 @@ CP_CXXFLAGS += $(CXXFLAGS) $(INCLUDES)
 OBJ += $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC)))
 OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
 
-.SUFFIXES: .cc .d .cpp
+.SUFFIXES: .cc $(DEPEXT) .cpp
 
 %.o:%.cpp
 	$(CXX) -c $(CP_CXXFLAGS) -o $@ $<
@@ -236,9 +235,9 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
 
 clean:
 	$(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \
-		$(patsubst %.cpp, %.d, $(filter %.cpp, $(SRC))) \
+		$(patsubst %.cpp, %$(DEPEXT), $(filter %.cpp, $(SRC))) \
 		$(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \
-		$(patsubst %.cc, %.d, $(filter %.cc, $(SRC))) \
+		$(patsubst %.cc, %$(DEPEXT), $(filter %.cc, $(SRC))) \
 		$(CLEANFILES)
 
 .PHONY: first_target clean all
@@ -255,7 +254,7 @@ sources: Makefile
 # include .depend
 # endif
 
-D_FILES1 = $(SRC:.c=.d)
-D_FILES = $(D_FILES1:.cpp=.d)
+D_FILES1 = $(SRC:.c=$(DEPEXT))
+D_FILES = $(D_FILES1:.cpp=$(DEPEXT))
 
 -include $(D_FILES)

regression/jbmc-strings/long_string/Test.java

@@ -24,7 +24,6 @@ endif
 #LIB_GLPK = -lglpk
 
 # SAT-solvers we have
-#PRECOSAT = ../../precosat-576-7e5e66f-120112
 #PICOSAT = ../../picosat-959
 #LINGELING = ../../lingeling-587f-4882048-110513
 #CHAFF = ../../zChaff
@@ -33,16 +32,11 @@ endif
 #MINISAT2 = ../../minisat-2.2.1
 #IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
-#SMVSAT =
 
 # Extra library for SAT solver. This should link to the archive file to be used
 # when linking against an IPASIR solver.
 LIBSOLVER =
 
-ifneq ($(PRECOSAT),)
-  CP_CXXFLAGS += -DSATCHECK_PRECOSAT
-endif
-
 ifneq ($(PICOSAT),)
   CP_CXXFLAGS += -DSATCHECK_PICOSAT
 endif
@@ -71,10 +65,6 @@ ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DSATCHECK_GLUCOSE
 endif
 
-ifneq ($(SMVSAT),)
-  CP_CXXFLAGS += -DSATCHECK_SMVSAT
-endif
-
 # Signing identity for MacOS Gatekeeper
 
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"

regression/jbmc-strings/long_string/test.desc

@@ -588,8 +588,6 @@ void cpp_typecheck_resolvet::make_constructors(
 {
   resolve_identifierst new_identifiers;
 
-  resolve_identifierst::iterator next;
-
   for(resolve_identifierst::iterator
       it=identifiers.begin();
       it!=identifiers.end();

regression/jbmc-strings/long_string/test_abort.desc

@@ -21,6 +21,7 @@ class message_handlert;
 class cover_blocks_baset
 {
 public:
+  virtual ~cover_blocks_baset() = default;
   /// \param t a goto instruction
   /// \return the block number of the block
   ///         the given goto instruction is part of

src/cbmc/bmc.cpp

@@ -25,6 +25,7 @@ class goal_filterst;
 class cover_instrumenter_baset
 {
 public:
+  virtual ~cover_instrumenter_baset() = default;
   cover_instrumenter_baset(
     const symbol_tablet &_symbol_table,
     const goal_filterst &_goal_filters,