diff --git a/jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.class b/jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.class new file mode 100644 index 00000000000..2cbbff93d99 Binary files /dev/null and b/jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.class differ diff --git a/jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.java b/jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.java new file mode 100644 index 00000000000..0dd7a779fc9 --- /dev/null +++ b/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); + } +} diff --git a/jbmc/regression/jbmc/context-include-exclude/Main.class b/jbmc/regression/jbmc/context-include-exclude/Main.class index a17b12bf3a3..6a7b61ea575 100644 Binary files a/jbmc/regression/jbmc/context-include-exclude/Main.class and b/jbmc/regression/jbmc/context-include-exclude/Main.class differ diff --git a/jbmc/regression/jbmc/context-include-exclude/Main.java b/jbmc/regression/jbmc/context-include-exclude/Main.java index c3cce0dbadd..cf075aa844f 100644 --- a/jbmc/regression/jbmc/context-include-exclude/Main.java +++ b/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) { diff --git a/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.class b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.class new file mode 100644 index 00000000000..0f08a2b20b1 Binary files /dev/null and b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.class differ diff --git a/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.java b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.java new file mode 100644 index 00000000000..274ad52085c --- /dev/null +++ b/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; } +} diff --git a/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.class b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.class new file mode 100644 index 00000000000..fc48dc97b4a Binary files /dev/null and b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.class differ diff --git a/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java new file mode 100644 index 00000000000..21eb0d5f453 --- /dev/null +++ b/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(); } +} diff --git a/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.class b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.class new file mode 100644 index 00000000000..1f8e6b62ec6 Binary files /dev/null and b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.class differ diff --git a/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.java b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.java new file mode 100644 index 00000000000..28186418098 --- /dev/null +++ b/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; } +} diff --git a/jbmc/regression/jbmc/context-include-exclude/test_exclude_absent.desc b/jbmc/regression/jbmc/context-include-exclude/test_exclude_absent.desc new file mode 100644 index 00000000000..4a4f87d920b --- /dev/null +++ b/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. diff --git a/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_all.desc b/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_all.desc index 0905ff245ea..8c0b0f86db0 100644 --- a/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_all.desc +++ b/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\.:\(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. diff --git a/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc b/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc index a104ea43729..d281b854e9c 100644 --- a/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc +++ b/jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc @@ -3,15 +3,12 @@ Main.class --context-include Main.main --context-include 'Main.:\(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. diff --git a/jbmc/regression/jbmc/context-include-exclude/test_exclude_package_prefix.desc b/jbmc/regression/jbmc/context-include-exclude/test_exclude_package_prefix.desc new file mode 100644 index 00000000000..0132aa64a1c --- /dev/null +++ b/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. diff --git a/jbmc/regression/jbmc/context-include-exclude/test_excluded_deleted_original_body.desc b/jbmc/regression/jbmc/context-include-exclude/test_excluded_deleted_original_body.desc new file mode 100644 index 00000000000..d9c605fe39f --- /dev/null +++ b/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. diff --git a/jbmc/regression/jbmc/context-include-exclude/test_excluded_has_nondet_body.desc b/jbmc/regression/jbmc/context-include-exclude/test_excluded_has_nondet_body.desc new file mode 100644 index 00000000000..a052421c0e4 --- /dev/null +++ b/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. diff --git a/jbmc/regression/jbmc/context-include-exclude/test_excluded_has_parameter_info.desc b/jbmc/regression/jbmc/context-include-exclude/test_excluded_has_parameter_info.desc new file mode 100644 index 00000000000..7d7130bef33 --- /dev/null +++ b/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". diff --git a/jbmc/regression/jbmc/context-include-exclude/test_include.desc b/jbmc/regression/jbmc/context-include-exclude/test_include.desc index 2c668f72d7d..fad97ae8eee 100644 --- a/jbmc/regression/jbmc/context-include-exclude/test_include.desc +++ b/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\.:\(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. diff --git a/jbmc/regression/jbmc/context-include-exclude/test_include_all.desc b/jbmc/regression/jbmc/context-include-exclude/test_include_all.desc index 8ed5b761f1d..e777d081ca1 100644 --- a/jbmc/regression/jbmc/context-include-exclude/test_include_all.desc +++ b/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 .* -- diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index cf4c4ccd83f..654ecf44ce9 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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 &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 needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, - bool threading_support) + bool threading_support, + const optionalt &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 diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/jbmc/src/java_bytecode/java_bytecode_convert_method.h index 7df52892628..9e7da326674 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.h @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include 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 needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, - bool threading_support); + bool threading_support, + const optionalt &method_context); void create_method_stub_symbol( const irep_idt &identifier, diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index c10af8c214d..d7f31044704 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/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 &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 &method_context); code_blockt convert_parameter_annotations( const methodt &method, diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index c5f46b549e7..c799eea7da3 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/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 context_include; std::vector 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 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(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(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."); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index dacfdd80089..b2c71721518 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -81,6 +81,9 @@ Author: Daniel Kroening, kroening@kroening.com " loaded.\n" \ " --context-include i only analyze code matching specification i that\n" /* NOLINT(*) */ \ " --context-exclude e does not match specification e.\n" \ + " All other methods are excluded, i.e. we load their\n" /* NOLINT(*) */ \ + " signatures and meta-information, but not their\n" /* NOLINT(*) */ \ + " bodies.\n" \ " A specification is any prefix of a package, class\n" /* NOLINT(*) */ \ " or method name, e.g. \"org.cprover.\" or\n" /* NOLINT(*) */ \ " \"org.cprover.MyClass.\" or\n" \ @@ -296,12 +299,20 @@ class java_bytecode_languaget:public languaget /// IDs of such objects to symbols that store their values. std::unordered_map references; - /// If set, method bodies are only elaborated if they pass the filter - optionalt method_in_context; + /// If set, method bodies are only elaborated if they pass the filter. + /// Methods that do not pass the filter are "excluded": their symbols will + /// include all the meta-information that is available from the bytecode + /// (parameter types, return type, accessibility etc.) but the value of the + /// symbol (corresponding to the body of the method) will be replaced with the + /// same kind of "return nondet null or instance of return type" body that we + /// use for stubbed methods. The original method body will never be loaded. + optionalt method_context; }; std::unique_ptr new_java_bytecode_language(); void parse_java_language_options(const cmdlinet &cmd, optionst &options); +prefix_filtert get_context(const optionst &options); + #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 2be68f579eb..ac54928b9d0 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -690,6 +690,8 @@ int jbmc_parse_optionst::get_goto_program( std::unique_ptr &goto_model_ptr, const optionst &options) { + if(options.is_set("context-include") || options.is_set("context-exclude")) + method_context = get_context(options); lazy_goto_modelt lazy_goto_model = lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler); lazy_goto_model.initialize(cmdline.args, options); @@ -1009,7 +1011,9 @@ bool jbmc_parse_optionst::generate_function_body( // Provide a simple stub implementation for any function we don't have a // bytecode implementation for: - if(body_available) + if( + body_available && + (!method_context || (*method_context)(id2string(function_name)))) return false; if(!can_generate_function_body(function_name)) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 4a628ede020..c685f6c4a36 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -133,6 +133,11 @@ class jbmc_parse_optionst : public parse_options_baset const optionst &); bool show_loaded_functions(const abstract_goto_modelt &goto_model); bool show_loaded_symbols(const abstract_goto_modelt &goto_model); + + /// See java_bytecode_languaget::method_context. + /// The two fields are initialized in exactly the same way. + /// TODO Refactor this so it only needs to be computed once, in one place. + optionalt method_context; }; #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 5a9966ece15..4d9cc0dba96 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -22,6 +22,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_convert_method/convert_method.cpp \ java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp \ java_bytecode/java_bytecode_language/language.cpp \ + java_bytecode/java_bytecode_language/context_excluded.cpp \ java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \ java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \ java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \ diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp index e5cd0bf5e4c..eac5c681e03 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.cpp +++ b/jbmc/unit/java-testing-utils/load_java_class.cpp @@ -179,20 +179,37 @@ symbol_tablet load_java_class( java_class_name, class_path, main, std::move(java_lang), command_line); } -/// See \ref load_goto_model_from_java_class -/// With the command line configured to disable lazy loading and string -/// refinement and the language set to be the default java_bytecode language goto_modelt load_goto_model_from_java_class( const std::string &java_class_name, const std::string &class_path, + const std::vector &command_line_flags, + const std::unordered_map &command_line_options, const std::string &main) { free_form_cmdlinet command_line; - command_line.add_flag("no-lazy-methods"); - command_line.add_flag("no-refine-strings"); + for(const auto &flag : command_line_flags) + command_line.add_flag(flag); + for(const auto &option : command_line_options) + command_line.add_option(option.first, option.second); std::unique_ptr lang = new_java_bytecode_language(); return load_goto_model_from_java_class( java_class_name, class_path, main, std::move(lang), command_line); } + +/// See \ref load_goto_model_from_java_class +/// With the command line configured to disable lazy loading and string +/// refinement and the language set to be the default java_bytecode language +goto_modelt load_goto_model_from_java_class( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main) +{ + return load_goto_model_from_java_class( + java_class_name, + class_path, + {"no-lazy-methods", "no-refine-strings"}, + {}, + main); +} diff --git a/jbmc/unit/java-testing-utils/load_java_class.h b/jbmc/unit/java-testing-utils/load_java_class.h index cb6e5c4a661..02d0a78ed27 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.h +++ b/jbmc/unit/java-testing-utils/load_java_class.h @@ -25,11 +25,6 @@ symbol_tablet load_java_class( const std::string &class_path, const std::string &main = ""); -goto_modelt load_goto_model_from_java_class( - const std::string &java_class_name, - const std::string &class_path, - const std::string &main = ""); - symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path, @@ -55,4 +50,18 @@ symbol_tablet load_java_class_lazy( const std::string &class_path, const std::string &main); +/// Overload of load_goto_model_from_java_class with configurable command-line +/// options. +goto_modelt load_goto_model_from_java_class( + const std::string &java_class_name, + const std::string &class_path, + const std::vector &command_line_flags, + const std::unordered_map &command_line_options, + const std::string &main = ""); + +goto_modelt load_goto_model_from_java_class( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main = ""); + #endif // CPROVER_JAVA_TESTING_UTILS_LOAD_JAVA_CLASS_H diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class new file mode 100644 index 00000000000..47961b187b5 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java new file mode 100644 index 00000000000..382b93b21f1 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java @@ -0,0 +1,18 @@ +public class ClassWithDifferentModifiers { + + public static void main(String[] args) { + ClassWithDifferentModifiers guineaPig = new ClassWithDifferentModifiers(); + assert guineaPig.testPublicInstance() == 1; + assert guineaPig.testPrivateStatic() == 2; + assert guineaPig.testProtectedFinalInstance() == 3; + assert guineaPig.testDefaultFinalStatic() == 4; + } + + public int testPublicInstance() { return 1; } + + private static int testPrivateStatic() { return 2; } + + protected final int testProtectedFinalInstance() { return 3; } + + final static int testDefaultFinalStatic() { return 4; } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/context_excluded.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/context_excluded.cpp new file mode 100644 index 00000000000..1c39c2a7581 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_language/context_excluded.cpp @@ -0,0 +1,98 @@ +/*******************************************************************\ + +Module: Unit tests for java_bytecode_language. + +Author: Diffblue Limited. + +\*******************************************************************/ + +#include + +#include + +#include +#include + +SCENARIO( + "Exclude a method using context-include/exclude", + "[core][java_bytecode][java_bytecode_language]") +{ + GIVEN("A class with all methods excluded except for main") + { + const symbol_tablet symbol_table = + load_goto_model_from_java_class( + "ClassWithDifferentModifiers", + "./java_bytecode/java_bytecode_language", + {}, + {{"context-include", "ClassWithDifferentModifiers.main"}}) + .get_symbol_table(); + + WHEN("Converting the methods of this class") + { + const auto public_instance_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testPublicInstance:()I"); + REQUIRE(public_instance_symbol); + const auto public_instance_type = + type_try_dynamic_cast(public_instance_symbol->type); + + const auto private_static_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testPrivateStatic:()I"); + REQUIRE(private_static_symbol); + const auto private_static_type = + type_try_dynamic_cast(private_static_symbol->type); + + const auto protected_final_instance_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testProtectedFinalInstance:()I"); + REQUIRE(protected_final_instance_symbol); + const auto protected_final_instance_type = + type_try_dynamic_cast( + protected_final_instance_symbol->type); + + const auto default_final_static_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testDefaultFinalStatic:()I"); + REQUIRE(default_final_static_symbol); + const auto default_final_static_type = + type_try_dynamic_cast( + default_final_static_symbol->type); + THEN( + "Symbol values for excluded methods are nil as the lazy_goto_modelt " + "for unit tests does not generate stub/exclude bodies.") + { + REQUIRE(public_instance_symbol->value.is_nil()); + REQUIRE(private_static_symbol->value.is_nil()); + REQUIRE(protected_final_instance_symbol->value.is_nil()); + REQUIRE(default_final_static_symbol->value.is_nil()); + } + THEN( + "Types of excluded methods are stored as java_method_typets in the " + "symbol table.") + { + REQUIRE(public_instance_type); + REQUIRE(private_static_type); + REQUIRE(protected_final_instance_type); + REQUIRE(default_final_static_type); + } + THEN("Access modifiers of excluded methods are preserved.") + { + REQUIRE(public_instance_type->get_access() == ID_public); + REQUIRE(private_static_type->get_access() == ID_private); + REQUIRE(protected_final_instance_type->get_access() == ID_protected); + REQUIRE(default_final_static_type->get_access() == ID_default); + } + THEN("Static/Instance meta-information of excluded methods is preserved.") + { + REQUIRE_FALSE(public_instance_type->get_bool(ID_is_static)); + REQUIRE(private_static_type->get_bool(ID_is_static)); + REQUIRE_FALSE(protected_final_instance_type->get_bool(ID_is_static)); + REQUIRE(default_final_static_type->get_bool(ID_is_static)); + } + THEN("Final/Non-final meta-information of excluded methods is preserved.") + { + REQUIRE_FALSE(public_instance_type->get_is_final()); + REQUIRE_FALSE(private_static_type->get_is_final()); + REQUIRE(protected_final_instance_type->get_is_final()); + REQUIRE(default_final_static_type->get_is_final()); + } + } + } +} diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index 1d0b151f573..50b30598b82 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -173,6 +173,9 @@ class lazy_goto_functions_mapt final const key_type &name, symbol_table_baset &function_symbol_table) const { + // Fill in symbol table entry body if not already done + language_files.convert_lazy_method(name, function_symbol_table); + underlying_mapt::iterator it=goto_functions.find(name); if(it!=goto_functions.end()) return *it; @@ -190,10 +193,6 @@ class lazy_goto_functions_mapt final // Second chance: see if language_filest can provide a body: if(!body_provided) { - // Fill in symbol table entry body if not already done - language_files.convert_lazy_method(name, function_symbol_table); - body_provided = function_symbol_table.lookup_ref(name).value.is_not_nil(); - // Create goto_functiont goto_convert_functionst convert_functions( function_symbol_table, message_handler);