[TG-9294][UFC] Fix context-include/exclude jbmc options

jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.java

@@ -0,0 +1,30 @@
+import org.cprover.other.MyOther;
+import org.cprover.other.Parent;
+import org.cprover.other.Child;
+
+public class ExcludedProperties {
+
+  public static void parameters() {
+    int i = MyOther.identity(21);
+    assert (i == 21);
+  }
+
+  public static void compileTimeReturnType() {
+    Parent p = MyOther.subclass();
+    assert (p == null || p instanceof Parent);
+    if (p == null) {
+      assert false; // reachable with "return nondet" body
+    } else {
+      if (p.num() == 1) {
+        assert false; // reachable with "return nondet" body
+      } else {
+        assert false; // reachable with "return nondet" body
+      }
+    }
+  }
+
+  public static void runtimeReturnType() {
+    Parent p = MyOther.subclass();
+    assert (p == null || p instanceof Child);
+  }
+}

jbmc/regression/jbmc/context-include-exclude/Main.java

@@ -1,4 +1,5 @@
 import org.cprover.MyClass;
+import org.cprover.other.MyOther;
 
 public class Main {
   public static void main(String[] args) {
@@ -7,9 +8,11 @@ public static void main(String[] args) {
     MyClass m = new MyClass(y);
     int z = m.get();
     int w = MyClass.Inner.doIt(z);
+    int u = MyOther.identity(w);
     assert(x == y);
     assert(y == z);
     assert(z == w);
+    assert (w == u);
   }
 
   public static int myMethod(int x) {

jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.java

@@ -0,0 +1,6 @@
+package org.cprover.other;
+
+public class Child extends Parent {
+
+  public int num() { return 2; }
+}

jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java

@@ -0,0 +1,8 @@
+package org.cprover.other;
+
+public class MyOther {
+
+  public static int identity(int x) { return x; }
+
+  public static Parent subclass() { return new Child(); }
+}

jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.java

@@ -0,0 +1,8 @@
+package org.cprover.other;
+
+public class Parent {
+
+  int field = 1;
+
+  public int num() { return field; }
+}

jbmc/regression/jbmc/context-include-exclude/test_exclude_absent.desc

@@ -0,0 +1,14 @@
+CORE
+Main.class
+--context-exclude org.cprover.oh
+^EXIT=0$
+^SIGNAL=0$
+.* line 12 assertion at file Main.java line 12 .*: SUCCESS
+.* line 13 assertion at file Main.java line 13 .*: SUCCESS
+.* line 14 assertion at file Main.java line 14 .*: SUCCESS
+.* line 15 assertion at file Main.java line 15 .*: SUCCESS
+--
+WARNING: no body for function .*
+--
+Tests that when --context-exclude is given a package prefix that does not occur
+anywhere on the classpath, it has no effect.

jbmc/regression/jbmc/context-include-exclude/test_exclude_from_all.desc

@@ -3,14 +3,11 @@ Main.class
 --context-exclude 'org.cprover.MyClass$Inner.'
 ^EXIT=10$
 ^SIGNAL=0$
-.* line 10 assertion at file Main.java line 10 .*: SUCCESS
-.* line 11 assertion at file Main.java line 11 .*: SUCCESS
-.* line 12 assertion at file Main.java line 12 .*: FAILURE
-WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
+.* line 12 assertion at file Main.java line 12 .*: SUCCESS
+.* line 13 assertion at file Main.java line 13 .*: SUCCESS
+.* line 14 assertion at file Main.java line 14 .*: FAILURE
+.* line 15 assertion at file Main.java line 15 .*: SUCCESS
 --
-WARNING: no body for function .*clinit_wrapper
-WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
-WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
-WARNING: no body for function java::Main\.myMethod:\(I\)I
+WARNING: no body for function .*
 --
 Tests that no methods except those in the specified class are excluded.

jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc

@@ -3,15 +3,12 @@ Main.class
 --context-include Main.main --context-include 'Main.<clinit' --context-include org.cprover.MyClass --context-exclude 'org.cprover.MyClass$Inner.'
 ^EXIT=10$
 ^SIGNAL=0$
-.* line 10 assertion at file Main.java line 10 .*: FAILURE
-.* line 11 assertion at file Main.java line 11 .*: SUCCESS
 .* line 12 assertion at file Main.java line 12 .*: FAILURE
-WARNING: no body for function java::Main\.myMethod:\(I\)I
-WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
+.* line 13 assertion at file Main.java line 13 .*: SUCCESS
+.* line 14 assertion at file Main.java line 14 .*: FAILURE
+.* line 15 assertion at file Main.java line 15 .*: FAILURE
 --
-WARNING: no body for function .*clinit_wrapper
-WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
-WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
+WARNING: no body for function .*
 --
 Tests that only the specified methods and classes are included, while
 the inner class from MyClass is excluded.

jbmc/regression/jbmc/context-include-exclude/test_exclude_package_prefix.desc

@@ -0,0 +1,14 @@
+CORE
+Main.class
+--context-include Main --context-include org.cprover --context-exclude org.cprover.ot
+^EXIT=10$
+^SIGNAL=0$
+.* line 12 assertion at file Main.java line 12 .*: SUCCESS
+.* line 13 assertion at file Main.java line 13 .*: SUCCESS
+.* line 14 assertion at file Main.java line 14 .*: SUCCESS
+.* line 15 assertion at file Main.java line 15 .*: FAILURE
+--
+WARNING: no body for function .*
+--
+Tests that --context-exclude works with an argument that is the prefix of a
+package name.

jbmc/regression/jbmc/context-include-exclude/test_excluded_deleted_original_body.desc

@@ -0,0 +1,12 @@
+CORE
+ExcludedProperties.class
+--context-exclude org.cprover.other --function ExcludedProperties.runtimeReturnType
+^EXIT=10$
+^SIGNAL=0$
+.* line 28 assertion at file ExcludedProperties.java line 28.*: FAILURE
+--
+--
+Test that for an excluded method, we do not convert its "real" body from the
+bytecode.
+We instead assign it a "return nondet" body as for stubbed methods, which is
+tested by test_excluded_has_nondet_body.desc.

jbmc/regression/jbmc/context-include-exclude/test_excluded_has_nondet_body.desc

@@ -0,0 +1,15 @@
+CORE
+ExcludedProperties.class
+--context-exclude org.cprover.other --function ExcludedProperties.compileTimeReturnType
+^EXIT=10$
+^SIGNAL=0$
+.* line 14 assertion at file ExcludedProperties.java line 14 .*: SUCCESS
+.* line 16 assertion at file ExcludedProperties.java line 16 .*: FAILURE
+.* line 19 assertion at file ExcludedProperties.java line 19 .*: FAILURE
+.* line 21 assertion at file ExcludedProperties.java line 21 .*: FAILURE
+--
+--
+Test that for an excluded method, we keep the information about the
+(compile-time) return type of the method and return a nondet object of that
+type, or null.
+Note that we do this in the same way as for stubbed methods.

jbmc/regression/jbmc/context-include-exclude/test_excluded_has_parameter_info.desc

@@ -0,0 +1,13 @@
+CORE
+ExcludedProperties.class
+--context-exclude org.cprover.other --show-symbol-table --function ExcludedProperties.parameters
+^EXIT=0$
+^SIGNAL=0$
+java::org\.cprover\.other\.MyOther\.identity:\(I\)I::arg0i
+--
+java::org\.cprover\.other\.MyOther\.identity:\(I\)I::stub
+--
+Test that for an excluded method, we still create a symbol for its parameter(s)
+just like for non-excluded methods.
+Only the body of excluded methods should be missing, not their signature or
+other "meta-information".

jbmc/regression/jbmc/context-include-exclude/test_include.desc

@@ -3,14 +3,11 @@ Main.class
 --context-include Main.
 ^EXIT=10$
 ^SIGNAL=0$
-.* line 10 assertion at file Main.java line 10 .*: SUCCESS
-.* line 11 assertion at file Main.java line 11 .*: FAILURE
-.* line 12 assertion at file Main.java line 12 .*: FAILURE
-WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
-WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
-WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
+.* line 12 assertion at file Main.java line 12 .*: SUCCESS
+.* line 13 assertion at file Main.java line 13 .*: FAILURE
+.* line 14 assertion at file Main.java line 14 .*: FAILURE
+.* line 15 assertion at file Main.java line 15 .*: FAILURE
 --
-WARNING: no body for function .*clinit_wrapper
-WARNING: no body for function java::Main\.myMethod:\(I\)I
+WARNING: no body for function .*
 --
 Tests that only methods from the specified class are included.

jbmc/regression/jbmc/context-include-exclude/test_include_all.desc

@@ -3,9 +3,10 @@ Main.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-.* line 10 assertion at file Main.java line 10 .*: SUCCESS
-.* line 11 assertion at file Main.java line 11 .*: SUCCESS
 .* line 12 assertion at file Main.java line 12 .*: SUCCESS
+.* line 13 assertion at file Main.java line 13 .*: SUCCESS
+.* line 14 assertion at file Main.java line 14 .*: SUCCESS
+.* line 15 assertion at file Main.java line 15 .*: SUCCESS
 --
 WARNING: no body for function .*
 --

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -425,7 +425,8 @@ static irep_idt get_method_identifier(
 
 void java_bytecode_convert_methodt::convert(
   const symbolt &class_symbol,
-  const methodt &m)
+  const methodt &m,
+  const optionalt<prefix_filtert> &method_context)
 {
   // Construct the fully qualified method name
   // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
@@ -605,8 +606,12 @@ void java_bytecode_convert_methodt::convert(
   if((!m.is_abstract) && (!m.is_native))
   {
     code_blockt code(convert_parameter_annotations(m, method_type));
-    code.append(convert_instructions(m));
-    method_symbol.value = std::move(code);
+    // Do not convert if method is not in context
+    if(!method_context || (*method_context)(id2string(method_identifier)))
+    {
+      code.append(convert_instructions(m));
+      method_symbol.value = std::move(code);
+    }
   }
 }
 
@@ -3184,7 +3189,8 @@ void java_bytecode_convert_method(
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
-  bool threading_support)
+  bool threading_support,
+  const optionalt<prefix_filtert> &method_context)
 
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
@@ -3197,7 +3203,7 @@ void java_bytecode_convert_method(
     class_hierarchy,
     threading_support);
 
-  java_bytecode_convert_method(class_symbol, method);
+  java_bytecode_convert_method(class_symbol, method, method_context);
 }
 
 /// Returns true iff method \p methodid from class \p classname is

jbmc/src/java_bytecode/java_bytecode_convert_method.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 
 class class_hierarchyt;
+class prefix_filtert;
 
 void java_bytecode_initialize_parameter_names(
   symbolt &method_symbol,
@@ -37,7 +38,8 @@ void java_bytecode_convert_method(
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
-  bool threading_support);
+  bool threading_support,
+  const optionalt<prefix_filtert> &method_context);
 
 void create_method_stub_symbol(
   const irep_idt &identifier,

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -61,9 +61,12 @@ class java_bytecode_convert_methodt:public messaget
   typedef methodt::local_variable_tablet local_variable_tablet;
   typedef methodt::local_variablet local_variablet;
 
-  void operator()(const symbolt &class_symbol, const methodt &method)
+  void operator()(
+    const symbolt &class_symbol,
+    const methodt &method,
+    const optionalt<prefix_filtert> &method_context)
   {
-    convert(class_symbol, method);
+    convert(class_symbol, method, method_context);
   }
 
   typedef uint16_t method_offsett;
@@ -290,7 +293,10 @@ class java_bytecode_convert_methodt:public messaget
     bool allow_merge = true);
 
   // conversion
-  void convert(const symbolt &class_symbol, const methodt &);
+  void convert(
+    const symbolt &class_symbol,
+    const methodt &,
+    const optionalt<prefix_filtert> &method_context);
 
   code_blockt convert_parameter_annotations(
     const methodt &method,

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -104,7 +104,7 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
   }
 }
 
-static prefix_filtert get_context(const optionst &options)
+prefix_filtert get_context(const optionst &options)
 {
   std::vector<std::string> context_include;
   std::vector<std::string> context_exclude;
@@ -245,7 +245,7 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
     options.get_bool_option("ignore-manifest-main-class");
 
   if(options.is_set("context-include") || options.is_set("context-exclude"))
-    method_in_context = get_context(options);
+    method_context = get_context(options);
 
   language_options_initialized=true;
 }
@@ -1173,12 +1173,6 @@ bool java_bytecode_languaget::convert_single_method(
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
 {
-  // Do not convert if method is not in context
-  if(method_in_context && !(*method_in_context)(id2string(function_id)))
-  {
-    return false;
-  }
-
   const symbolt &symbol = symbol_table.lookup_ref(function_id);
 
   // Nothing to do if body is already loaded
@@ -1312,29 +1306,33 @@ bool java_bytecode_languaget::convert_single_method(
       std::move(needed_lazy_methods),
       string_preprocess,
       class_hierarchy,
-      threading_support);
+      threading_support,
+      method_context);
     INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
     return false;
   }
 
-  // The return of an opaque function is a source of an otherwise invisible
-  // instantiation, so here we ensure we've loaded the appropriate classes.
-  const java_method_typet function_type = to_java_method_type(symbol.type);
-  if(
-    const pointer_typet *pointer_return_type =
-      type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
+  if(needed_lazy_methods)
   {
-    // If the return type is abstract, we won't forcibly instantiate it here
-    // otherwise this can cause abstract methods to be explictly called
-    // TODO(tkiley): Arguably no abstract class should ever be added to
-    // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
-    // TODO(tkiley): investigation
-    namespacet ns{symbol_table};
-    const java_class_typet &underlying_type =
-      to_java_class_type(ns.follow(pointer_return_type->subtype()));
-
-    if(!underlying_type.is_abstract())
-      needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
+    // The return of an opaque function is a source of an otherwise invisible
+    // instantiation, so here we ensure we've loaded the appropriate classes.
+    const java_method_typet function_type = to_java_method_type(symbol.type);
+    if(
+      const pointer_typet *pointer_return_type =
+        type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
+    {
+      // If the return type is abstract, we won't forcibly instantiate it here
+      // otherwise this can cause abstract methods to be explictly called
+      // TODO(tkiley): Arguably no abstract class should ever be added to
+      // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
+      // TODO(tkiley): investigation
+      namespacet ns{symbol_table};
+      const java_class_typet &underlying_type =
+        to_java_class_type(ns.follow(pointer_return_type->subtype()));
+
+      if(!underlying_type.is_abstract())
+        needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
+    }
   }
 
   INVARIANT(declaring_class(symbol), "Method must have a declaring class.");