Squashed 'cbmc/' changes from 7c1de91..6fd77f4

6fd77f4 Merge pull request diffblue#2472 from smowton/smowton/fix/nondet-stringbuilders
5423ea4 Merge pull request diffblue#2488 from polgreen/common_call_graph_funcs
a2a5662 Merge pull request diffblue#2263 from JohnDumbell/bugfix/nondet_direct_return
bbf0d02 Merge pull request diffblue#2482 from antlechner/antonia/direct-children-of-class
c982c21 Merge pull request diffblue#2486 from Degiorgio/jbmc-synchronoization-asymmetry-fix
8e7b6e7 Java object factory: initialize AbstractStringBuilder-derived types correctly
9af7ef1 Add tests for new class_hierarchy_grapht functions
79cad15 Fix existing class hierarchy test syntax
dbac316 Add documentation to class_hierarchyt
3ecac30 Move non-graph function below graph functions
4badd8f Add useful functions to class_hierarchy_grapht
610467e Merge pull request diffblue#2480 from smowton/smowton/admin/graph-unit-tests
2431ac0 Doxygen formatting for dependence_graph test includes
19a1ceb factor out common call graph unit test functions into header
deff59d Add tests for grapht::make_chordal and grapht::connected_subgraphs
e94208f Merge pull request diffblue#2428 from tautschnig/vs-ref
d00d833 Fix: several grapht functions were uncompilable if ever called
b9014de Merge pull request diffblue#2381 from polgreen/depth_limited_search
7c767ab Merge pull request diffblue#2485 from tautschnig/vs-unreachable
da76500 JBMC: Fixed asymmetry between synchronized blocks and methods.
5918640 Merge pull request diffblue#2487 from JohnDumbell/bugfix/add_java_load_class
d65c655 Merge pull request diffblue#2484 from tautschnig/vs-printf
91e8b89 Fix for nondet replacement on a direct return (pre-remove returns)
904132d unit tests for depth limited search on call graph
2c76d0d call graph helper interface to depth limited search
64fdb9b depht limited search for grapht
e708bfb Adds --java-load-class to tests that require it
6665c69 Remove unreachable instructions
6e4d5a7 printf does not and should not have a left-hand side
2111f7c Merge pull request diffblue#2475 from tautschnig/vs-wmm
6566d10 Merge pull request diffblue#2469 from tautschnig/vs-string2
3703974 Merge pull request diffblue#2477 from tautschnig/vs-string-abstraction
cf797da Merge pull request diffblue#2473 from tautschnig/vs-update
c07a09b Merge pull request diffblue#2476 from tautschnig/vs-cex
e504e80 Remove unused parameter in string abstraction
4d88b98 Remove unused parameter in counterexample beautification
888f168 Remove unused parameter from update_scores
461754d Remove unused parameters in goto-instrument/wmm
93300aa Use string2unsigned when reading/expecting an unsigned
1a7033a String refinement: Take a reference to avoid copy

git-subtree-dir: cbmc
git-subtree-split: 6fd77f4

Author: JohnDumbell

jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class

@@ -14,6 +14,25 @@ public void me0()
     }
   }
 
+  // expected verification success
+  public static void aStatic() throws java.io.IOException
+  {
+    Object _lock = new Object();
+    try
+    {
+      synchronized (_lock)
+      {
+        if(true)
+          throw new java.io.IOException();
+      }
+    }
+    catch (java.io.IOException e)
+    {
+      return;
+    }
+    assert false; // unreachable
+  }
+
   // expected verification success
   // --
   // base-case, no synchronization

jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc

@@ -0,0 +1,10 @@
+CORE
+A.class
+--function 'A.aStatic' --lazy-methods
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that throwing an exception from a synchronization blocks does not cause reachability issues when the java-threading flag is not specified.
+

jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc

@@ -0,0 +1,7 @@
+public class Test {
+
+  public static void testme(StringBuilder builder, StringBuffer buffer) {
+
+  }
+
+}

jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc

@@ -0,0 +1,5 @@
+package java.lang;
+
+public class AbstractStringBuilder implements CharSequence {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.class

@@ -0,0 +1,5 @@
+package java.lang;
+
+interface CharSequence {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java

@@ -0,0 +1,5 @@
+package java.lang;
+
+public class String implements CharSequence {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.class

@@ -0,0 +1,5 @@
+package java.lang;
+
+public class StringBuffer extends AbstractStringBuilder {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java

@@ -0,0 +1,5 @@
+package java.lang;
+
+public class StringBuilder extends AbstractStringBuilder {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.testme
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+type mismatch
+--
+Before cbmc#2472 this would assume that StringBuilder's direct parent was
+java.lang.Object, causing a type mismatch when --refine-strings was not in use
+(which at the time would assume that parent-child relationship)

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.java

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 Test.class --function Test.testSuccess
+--refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 23 .*: SUCCESS

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.class

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 10000 --verbosity 10 Test.class --function Test.testFail
+--refine-strings --string-max-length 10000 --verbosity 10 --function Test.testFail
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 38 .*: FAILURE

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --verbosity 10 Test.class --function Test.test
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --verbosity 10 --function Test.test
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 20 .*: SUCCESS

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.class

@@ -0,0 +1,36 @@
+public class Test {
+
+  public static void testme(StringBuilder builder, StringBuffer buffer, String str) {
+
+    // In this test the versions of String, StringBuilder and
+    // StringBuffer.class supplied have fields beyond the expected situation
+    // of either no fields at all (without --refine-strings) or only 'length'
+    // and 'data' (with --refine-strings). We check they have been nondet-
+    // initialized as expected by making sure we can reach the final
+    // 'assert false'.
+
+    if(str != null &&
+       builder != null &&
+       buffer != null &&
+       str.a != null &&
+       builder.i != null &&
+       buffer.i != null &&
+       str.a.x >= 5 &&
+       str.a.y <= -10.0f &&
+       builder.d >= 100.0 &&
+       buffer.b == true) {
+
+      assert builder instanceof StringBuilder;
+      assert buffer instanceof StringBuffer;
+      assert str instanceof String;
+
+      assert str.a instanceof A;
+      assert builder.i instanceof Integer;
+      assert buffer.i instanceof Integer;
+
+      assert false;
+    }
+
+  }
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.java

@@ -0,0 +1,8 @@
+package java.lang;
+
+public class A {
+
+  public int x;
+  public float y;
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.class

@@ -0,0 +1,7 @@
+package java.lang;
+
+public class AbstractStringBuilder implements CharSequence {
+
+  public Integer i;
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.java

@@ -0,0 +1,5 @@
+package java.lang;
+
+interface CharSequence {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc

@@ -0,0 +1,7 @@
+package java.lang;
+
+public class String implements CharSequence {
+
+  public A a;
+
+}

jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc

@@ -0,0 +1,7 @@
+package java.lang;
+
+public class StringBuffer extends AbstractStringBuilder {
+
+  public boolean b;
+
+}

jbmc/regression/jbmc-strings/StringConcat_StringII/test_fail.desc

@@ -0,0 +1,7 @@
+package java.lang;
+
+public class StringBuilder extends AbstractStringBuilder {
+
+  public double d;
+
+}

jbmc/regression/jbmc-strings/StringDependencies/test.desc

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.testme
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 23 .* SUCCESS
+assertion at file Test.java line 24 .* SUCCESS
+assertion at file Test.java line 25 .* SUCCESS
+assertion at file Test.java line 27 .* SUCCESS
+assertion at file Test.java line 28 .* SUCCESS
+assertion at file Test.java line 29 .* SUCCESS
+assertion at file Test.java line 31 .* FAILURE
+--
+type mismatch

jbmc/regression/jbmc-strings/StringModelsWithFields/Test.class

@@ -1,6 +1,6 @@
 CORE
 IntegerTests.class
--refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMySet --cover location
+-refine-strings --string-max-length 100 --function IntegerTests.testMySet --cover location
 ^EXIT=0$
 ^SIGNAL=0$
 coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED

jbmc/regression/jbmc-strings/StringModelsWithFields/Test.java

@@ -1,6 +1,6 @@
 CORE
 IntegerTests.class
--refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMyGenSet --cover location
+-refine-strings --string-max-length 100 --function IntegerTests.testMyGenSet --cover location
 ^EXIT=0$
 ^SIGNAL=0$
 coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED

jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.class

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 main.class
-package_friendly1.class package_friendly2.class --show-goto-functions
+--java-load-class package_friendly1 --java-load-class package_friendly2 --show-goto-functions
 ^main[.]main[\(].*[\)].*$
 ^package_friendly2[.]operation2[\(][\)].*$
 ^EXIT=0$

jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java

@@ -1026,8 +1026,6 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
 
     if(i_it->statement=="athrow" ||
-       i_it->statement=="monitorenter" ||
-       i_it->statement=="monitorexit" ||
        i_it->statement=="putfield" ||
        i_it->statement=="getfield" ||
        i_it->statement=="checkcast" ||
@@ -1042,7 +1040,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
        i_it->statement=="invokestatic" ||
        i_it->statement=="invokevirtual" ||
        i_it->statement=="invokespecial" ||
-       i_it->statement=="invokeinterface")
+       i_it->statement=="invokeinterface" ||
+       (threading_support && (i_it->statement=="monitorenter" ||
+       i_it->statement=="monitorexit")))
     {
       const std::vector<unsigned int> handler =
         try_catch_handler(i_it->address, method.exception_table);
@@ -1986,6 +1986,9 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
     "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
     "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
 
+  if(!threading_support || !symbol_table.has_symbol(descriptor))
+    return code_skipt();
+
   // becomes a function call
   code_typet type(
     {code_typet::parametert(java_reference_type(void_typet()))},
@@ -3099,7 +3102,9 @@ void java_bytecode_convert_method(
   bool throw_assertion_error,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
-  const class_hierarchyt &class_hierarchy)
+  const class_hierarchyt &class_hierarchy,
+  bool threading_support)
+
 {
   if(std::regex_match(
        id2string(class_symbol.name),
@@ -3118,7 +3123,8 @@ void java_bytecode_convert_method(
     throw_assertion_error,
     needed_lazy_methods,
     string_preprocess,
-    class_hierarchy);
+    class_hierarchy,
+    threading_support);
 
   java_bytecode_convert_method(class_symbol, method);
 }

jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.class

@@ -36,7 +36,8 @@ void java_bytecode_convert_method(
   bool throw_assertion_error,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
-  const class_hierarchyt &class_hierarchy);
+  const class_hierarchyt &class_hierarchy,
+  bool threading_support);
 
 void java_bytecode_convert_method_lazy(
   const symbolt &class_symbol,

jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.java

@@ -39,11 +39,13 @@ class java_bytecode_convert_methodt:public messaget
     bool throw_assertion_error,
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
     java_string_library_preprocesst &_string_preprocess,
-    const class_hierarchyt &class_hierarchy)
+    const class_hierarchyt &class_hierarchy,
+    bool threading_support)
     : messaget(_message_handler),
       symbol_table(symbol_table),
       max_array_length(_max_array_length),
       throw_assertion_error(throw_assertion_error),
+      threading_support(threading_support),
       needed_lazy_methods(std::move(needed_lazy_methods)),
       string_preprocess(_string_preprocess),
       slots_for_parameters(0),
@@ -67,6 +69,7 @@ class java_bytecode_convert_methodt:public messaget
   symbol_table_baset &symbol_table;
   const size_t max_array_length;
   const bool throw_assertion_error;
+  const bool threading_support;
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods;
 
   /// Fully qualified name of the method under translation.