Merge commit '174d261a963adcfb058d8be83207b57701acdaf7' into CBMC_merge_2018-06-29

# Conflicts:
#	cbmc/jbmc/src/java_bytecode/java_bytecode_language.cpp
#	cbmc/jbmc/src/java_bytecode/replace_java_nondet.cpp
#	cbmc/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
#	cbmc/src/analyses/call_graph_helpers.cpp
#	cbmc/src/analyses/call_graph_helpers.h

Author: JohnDumbell

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cbmc/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;
+    }
+
+  }
+
+}

cbmc/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;
+
+}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1032,8 +1032,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" ||
@@ -1048,7 +1046,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);
@@ -1992,6 +1992,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()))},
@@ -3105,7 +3108,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),
@@ -3124,7 +3129,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);
 }

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

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