From 0dfafbee7a8621a0efd655e75f7099b9f0390ccd Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 16 Sep 2019 19:05:39 +0100 Subject: [PATCH 01/13] Rename method_in_context to method_context The new name makes it clearer that this field defines a context, not a method. --- jbmc/src/java_bytecode/java_bytecode_language.cpp | 4 ++-- jbmc/src/java_bytecode/java_bytecode_language.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index c5f46b549e7..4a948e321ac 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -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; } @@ -1174,7 +1174,7 @@ bool java_bytecode_languaget::convert_single_method( 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))) + if(method_context && !(*method_context)(id2string(function_id))) { return false; } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index dacfdd80089..e32eb935c3d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -297,7 +297,7 @@ class java_bytecode_languaget:public languaget std::unordered_map references; /// If set, method bodies are only elaborated if they pass the filter - optionalt method_in_context; + optionalt method_context; }; std::unique_ptr new_java_bytecode_language(); From 60ad2147477f013ea75e962c9be856c50144110a Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 16 Sep 2019 19:10:20 +0100 Subject: [PATCH 02/13] Move method context check before symbol value assignment The previous check was right at the beginning of convert_single_method, meaning that for an "excluded" method, we would have never entered java_bytecode_convert_method, which assigns more than just the symbol value (body of a method), e.g. parameter identifiers. The only information that we want to omit for excluded methods is their bodies / symbol values. This is why the new check is just before the assignment of symbol values, making sure that parameter identifiers and other meta-information of the method are correctly assigned for excluded methods. --- .../java_bytecode_convert_method.cpp | 16 +++++++++++----- .../java_bytecode/java_bytecode_convert_method.h | 4 +++- .../java_bytecode_convert_method_class.h | 12 +++++++++--- .../src/java_bytecode/java_bytecode_language.cpp | 9 ++------- 4 files changed, 25 insertions(+), 16 deletions(-) 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 4a948e321ac..253d6703893 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -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_context && !(*method_context)(id2string(function_id))) - { - return false; - } - const symbolt &symbol = symbol_table.lookup_ref(function_id); // Nothing to do if body is already loaded @@ -1312,7 +1306,8 @@ 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; } From de8fa1a8332633fb55c07bb85e1d14009536bac7 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Thu, 19 Sep 2019 12:22:25 +0100 Subject: [PATCH 03/13] Amend condition for when stub method body should be made There are three types of method symbols that we expect here: 1) symbols for regular methods, i.e. the bytecode of the method is available and the method is in the supplied context 2) symbols for opaque methods, i.e. the bytecode of the method is not available 3) symbols for excluded methods, i.e. the bytecode of the method is available but the method is not in the supplied context The previous check was correct for 1) and 2): we do not want to create stub bodies ("return nondet") for regular methods but we do want to create them for opaque methods. The new check makes sure that stub bodies are also created for excluded methods (3). Previously the value of those symbols was just left as nil, meaning the (type of the) return value of the method was not constrained in any way. --- jbmc/src/java_bytecode/java_bytecode_language.cpp | 2 +- jbmc/src/java_bytecode/java_bytecode_language.h | 2 ++ jbmc/src/jbmc/jbmc_parse_options.cpp | 6 +++++- jbmc/src/jbmc/jbmc_parse_options.h | 5 +++++ 4 files changed, 13 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 253d6703893..c6c9a54e542 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; diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index e32eb935c3d..8fa7d586f4a 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -304,4 +304,6 @@ 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 From f7c0ed16337a51c80ce5635e698a94397e6af400 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Thu, 19 Sep 2019 15:25:07 +0100 Subject: [PATCH 04/13] Remove unused variable assignment --- src/goto-programs/lazy_goto_functions_map.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index 1d0b151f573..71cb639659e 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -192,7 +192,6 @@ class lazy_goto_functions_mapt final { // 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( From 3302020674f13cef5f9a88921007839a6aceca71 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Thu, 19 Sep 2019 15:28:07 +0100 Subject: [PATCH 05/13] Move convert call above body_provided check The previous version would have not called convert_single_method on excluded methods, meaning they would have missed some meta-information, e.g. parameter identifiers. --- src/goto-programs/lazy_goto_functions_map.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index 71cb639659e..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,9 +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); - // Create goto_functiont goto_convert_functionst convert_functions( function_symbol_table, message_handler); From f9b3b44486e5d92ca9813af94ae182f1bbf31b4b Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Thu, 19 Sep 2019 15:30:20 +0100 Subject: [PATCH 06/13] Protect needed_lazy_methods access in an if-block If we are not using CI lazy methods here (as could happen after the change from the previous commit that makes sure convert_single_method is run for all methods), needed_lazy_methods is an empty optional and we cannot access it. --- .../java_bytecode/java_bytecode_language.cpp | 37 ++++++++++--------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index c6c9a54e542..c799eea7da3 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1312,24 +1312,27 @@ bool java_bytecode_languaget::convert_single_method( 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."); From d53520cd61320cf51d87d763a5d6e36189683622 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Tue, 17 Sep 2019 14:21:20 +0100 Subject: [PATCH 07/13] Remove "WARNING: no body for function" regexes These lines appear in the output for methods whose body is empty/nil. For excluded methods, we now have "return nondet" bodies as we do for stubs, so the warnings are no longer printed. --- .../jbmc/context-include-exclude/test_exclude_from_all.desc | 6 +----- .../context-include-exclude/test_exclude_from_include.desc | 6 +----- .../jbmc/context-include-exclude/test_include.desc | 6 +----- 3 files changed, 3 insertions(+), 15 deletions(-) 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..3298ee6cdf0 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 @@ -6,11 +6,7 @@ Main.class .* 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 -- -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..5fa76a53b06 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 @@ -6,12 +6,8 @@ Main.class .* 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 -- -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 .* -- 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_include.desc b/jbmc/regression/jbmc/context-include-exclude/test_include.desc index 2c668f72d7d..0149e2b7f9b 100644 --- a/jbmc/regression/jbmc/context-include-exclude/test_include.desc +++ b/jbmc/regression/jbmc/context-include-exclude/test_include.desc @@ -6,11 +6,7 @@ Main.class .* 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 -- -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. From 202919b1d8fff3251b81c2c0ee6f696e08be34cc Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Tue, 17 Sep 2019 14:28:58 +0100 Subject: [PATCH 08/13] Add context-include tests for package and absent prefix The tests in this commit would have all passed without the previous fixes already and are just added for completeness. The tested prefixes are a prefix of a package and a prefix that does not match anything on the classpath. --- .../jbmc/context-include-exclude/Main.class | Bin 1079 -> 973 bytes .../jbmc/context-include-exclude/Main.java | 3 +++ .../org/cprover/other/MyOther.class | Bin 0 -> 264 bytes .../org/cprover/other/MyOther.java | 6 ++++++ .../test_exclude_absent.desc | 14 ++++++++++++++ .../test_exclude_from_all.desc | 7 ++++--- .../test_exclude_from_include.desc | 5 +++-- .../test_exclude_package_prefix.desc | 14 ++++++++++++++ .../context-include-exclude/test_include.desc | 7 ++++--- .../test_include_all.desc | 5 +++-- 10 files changed, 51 insertions(+), 10 deletions(-) create mode 100644 jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.class create mode 100644 jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java create mode 100644 jbmc/regression/jbmc/context-include-exclude/test_exclude_absent.desc create mode 100644 jbmc/regression/jbmc/context-include-exclude/test_exclude_package_prefix.desc diff --git a/jbmc/regression/jbmc/context-include-exclude/Main.class b/jbmc/regression/jbmc/context-include-exclude/Main.class index a17b12bf3a392036838e1ca9d4cbbee9f738a755..6a7b61ea575bf89bd873c9f3ee40dbf298e49291 100644 GIT binary patch delta 625 zcmZWmO-~b16g_X4>6^a3N~i5mD76Kl@+noU2qqE}SkjOH8`i3F??KL+plL9Z-1Fw%`_4V*zK;7_F8#Xs{u4kIuN0CfDkM;n7*goL zunCV8Mlh;S#^X3^V-n*EaTFyc6eckxG2LEVZl4Zilk2Tu^HVL@-3Z=o*Cn2iCL9;@ zuT$_e29OuXG@2hOo4d`%e!W?#9WHGLdwUuw%xF~bRN|SYki5hTjXC5s9-ue;EJkB5 zHRiDpUJAc`)fZliT6v(GsnPlv@vRyZaJSyqcUoJm!?0vk*Alb^h*ZB}Dxj}@dg^0) z4)z}wq(n{#iGCsIE|bmjE??lzi9uu9%AYZIJI-*<;J@Wmqb|TpCoZ6mA?;JxJzwFT f^O^2c{@s)r?!eM-1PcX2&fPvIDw2%Q#4O^sbX8ao literal 1079 zcmZuv%Tg0T6g{1p$t1%dAtA^kz5x>iB8vDRAQoa(tOOUaD1p_GOohQ@hMEj0ehM3x zZrrF-kFHJ8pd@>~8sW-cOx#Og3*hiX6KfO@VaD^XvKQmhbJ@e!jfB(4Yo_h<6-s1Uf5$ zRefEywn8#G`e}$jthrmZgAI@J)NC=wez8Ke(bi~GyluZ~KXas_xFkIxd79`#!o(1U z$?Y6ac|L98J|5_JXrh2&6P>sq(08ix$zOjLec$s5F1zcPH8F?B0*TX`FV;8hYH&=C zjw^MW8@f-b{pWxW6^ir*PMb>wn_79Kv2sOLq_;&4t80`wSSwW~( zT;o?U`J+UlPfFoR1-l@@xtqH@qhQoV4m`_QJwDuYL9uk9@_vko6Y~=v)?_sJtlUD!D zCDUqJJCl@@l#tR0p~*9Zj6o-X7>UGjnF=S-fkhHsrAA44?wA((&>z;n!T<(II)(}| zTt!&@9G6(Du*XweVNT_47FW5_=o%aYN9iR1X39ecJlR7^QiUfsb-N z<6Pp5bCD1n1RpuEeJZR2x|7B}I`*KeAD}8-UtQOqR>8u~P2n__k|rPsi580e?mFm**^yxse5W*4ffRWFA1dTd zV&#Q7XYM^8cjor<^$lQ*b^;%1jAo1$A)2U4*=K@3%+`e9MQytn%W( zlbYJd$|`$dW;n}cgk-5trj%3V;`HsZusdl+`}~}z2oMsw+H6I6H2N%!&@L5siqLVK zIONqEe7!TU#>jx8wgn=?)vP+9zK17u6!ZHtkK`lM;$dj|7efhp Date: Tue, 17 Sep 2019 14:32:29 +0100 Subject: [PATCH 09/13] Add tests for properties of excluded methods The tests from the previous commit show that the right methods are excluded. The tests from this commit show that an excluded method has the right properties: meta-information such as parameter types and identifiers should be preserved, while the real method should not be loaded and a stub-like "return nondet" body should be used instead. The tests from this commit would not have passed without the fixes from this PR. --- .../ExcludedProperties.class | Bin 0 -> 1038 bytes .../ExcludedProperties.java | 30 ++++++++++++++++++ .../org/cprover/other/Child.class | Bin 0 -> 262 bytes .../org/cprover/other/Child.java | 6 ++++ .../org/cprover/other/MyOther.class | Bin 264 -> 386 bytes .../org/cprover/other/MyOther.java | 2 ++ .../org/cprover/other/Parent.class | Bin 0 -> 298 bytes .../org/cprover/other/Parent.java | 8 +++++ .../test_excluded_deleted_original_body.desc | 12 +++++++ .../test_excluded_has_nondet_body.desc | 15 +++++++++ .../test_excluded_has_parameter_info.desc | 13 ++++++++ 11 files changed, 86 insertions(+) create mode 100644 jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.class create mode 100644 jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.java create mode 100644 jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.class create mode 100644 jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.java create mode 100644 jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.class create mode 100644 jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.java create mode 100644 jbmc/regression/jbmc/context-include-exclude/test_excluded_deleted_original_body.desc create mode 100644 jbmc/regression/jbmc/context-include-exclude/test_excluded_has_nondet_body.desc create mode 100644 jbmc/regression/jbmc/context-include-exclude/test_excluded_has_parameter_info.desc 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 0000000000000000000000000000000000000000..2cbbff93d99f9e1fd35a5deff3548d83530bda95 GIT binary patch literal 1038 zcmZuw-%ry}6#nj3=++hX0|#R;bcni5rD{lgfEW#;A%YOMn8;h#-axTym)n-epWAP5hgP@wEG;&NR8b{mwn#_nmWYfByRP1;7gKC{Qt{U>>C;6fDTNs6gr> zmt>R`$XJwdS;mrrE4V7-8pG6*?s;7Jmg{&AEl+RS++<*T4C8B-WBK+`?^!%usfxdB_c)VRn>h`*!cD%uaHuwAqp1F;}OYnHxB z^kyMiI|X|m9z>4T@h*rYrUpkJBNm}^nfw`Is~-^WAY07j-yroF(u-4!eGLg>5y2$l zv`-LG5=HWGp-Xy>A|oU}Abs5|w=9CkpI*_Gzkm4T^ACmQl5t57{rrr-nHcKBd G6n_J7AkpUl literal 0 HcmV?d00001 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/org/cprover/other/Child.class b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.class new file mode 100644 index 0000000000000000000000000000000000000000..0f08a2b20b1887c81ab4d72b6e4becb2acfac094 GIT binary patch literal 262 zcmZXOy$%6E6ot>-U)G`|5`_+hZIq&sNF*W>qF+qx2s<*_^;8;_MBxEEl(@4cQ+#LU zo-dR8{ybj*hNuUy5&Ee5s1dx8Ol3AE*xlZS;7rtB5bAT8iba0j3cZfEC!W}8elDaL zAy}zg@5EG^BA6udv>zPfYaGIXOK2#4h;|pPu0lsDOPGa2X#O|LSc^162NrK-js@NV pF4N;zo0B-*{sVO93&Cf4#n5J!P-Ysn#c5Q_z5RIRv%oZ{d;xo?Emi;k literal 0 HcmV?d00001 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 index cdf866d3453d0843695f8d39b0ba05be10820cfd..fc48dc97b4a4ac83294f444453b5305e967e0b9a 100644 GIT binary patch delta 264 zcmeBRYGRf>^>5cc1_lNb1`#d>Rt5of20<?D8DSVNI$5cc1_lNb27WFEW(FR123~dszKOCn6Psn2Sr}L+?lBT(0!n}Y69Xdy yPzXq}O=e^ivtpAuKzU9E4j=}~0C`eC8YIdjwFXEsG9c7}^m2h@7`OoklnUek 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 index da2911c081e..21eb0d5f453 100644 --- a/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java +++ b/jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java @@ -3,4 +3,6 @@ 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 0000000000000000000000000000000000000000..1f8e6b62ec687e0a1f2e11c183ac75b62a1d8bc3 GIT binary patch literal 298 zcmX|*KT88a5XIlzU$eQGXqq$@He#;GHI`x{2!Wu2l78>9#toOf>%!qR>3p) de9Uwg*_f4?t(L-6vCC*Dk1d+Y@``~j&wFQNbd literal 0 HcmV?d00001 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_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". From a61441c78aac586459b979e32a3b2a3def830455 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Tue, 17 Sep 2019 16:31:33 +0100 Subject: [PATCH 10/13] Move load_goto_model... declaration to end of file This is consistent with the location of the definition in the cpp file. --- jbmc/unit/java-testing-utils/load_java_class.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/jbmc/unit/java-testing-utils/load_java_class.h b/jbmc/unit/java-testing-utils/load_java_class.h index cb6e5c4a661..95180e9e087 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,9 @@ symbol_tablet load_java_class_lazy( 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 = ""); + #endif // CPROVER_JAVA_TESTING_UTILS_LOAD_JAVA_CLASS_H From 1f2dfcfd8487dd77adbaba54343e7fbb81324cf2 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Tue, 17 Sep 2019 18:02:40 +0100 Subject: [PATCH 11/13] Split load_goto_model_from_java_class into two functions The new overload allows specifying the command-line options to run jbmc with. For example, we will be able to specify that --context-include should be used. --- .../java-testing-utils/load_java_class.cpp | 27 +++++++++++++++---- .../unit/java-testing-utils/load_java_class.h | 9 +++++++ 2 files changed, 31 insertions(+), 5 deletions(-) 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 95180e9e087..02d0a78ed27 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.h +++ b/jbmc/unit/java-testing-utils/load_java_class.h @@ -50,6 +50,15 @@ 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, From 331e0bc95ae50007e3923e3d25dc348054be4d8c Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Tue, 17 Sep 2019 18:01:56 +0100 Subject: [PATCH 12/13] Add unit tests for preserving meta-information of excluded methods These unit tests complement the regression tests in jbmc/regression/jbmc/context-include-exclude that were added in a previous commit to check for properties of excluded methods. Some properties, like information about accessibility and final and static status, is easier to check in unit-style tests. --- jbmc/unit/Makefile | 1 + .../ClassWithDifferentModifiers.class | Bin 0 -> 977 bytes .../ClassWithDifferentModifiers.java | 18 ++++ .../context_excluded.cpp | 98 ++++++++++++++++++ 4 files changed, 117 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_language/context_excluded.cpp 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_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class new file mode 100644 index 0000000000000000000000000000000000000000..47961b187b575aec3a03fcb564fabe92406308eb GIT binary patch literal 977 zcmaJ;O>fgc5Pj>|apJf%UkxUuNeczi2I!@ns1T^3Qbh_#K~$8JV{gh9*GBfHKc*MB zap3|;Eus?K`ArBhYnmp?0Uu`Pip7yDIWqpsYB z7o01wdeJcU_?A$77dHcvyes6Jju;Gh%tN^o`C=e=oZM9kY|Ns_F#jK%jTv0BaTyMS zGgkd*w93bE9K|-Sz_C$RW*&}-RU2*GW+;w3p7jq%6s>ifN`FiH^m!s;?qAGQx`s)* zr#&pu6>YjaD>{k_c_wHIieyU^Ezry8HC9i-J}V%~WV30KA&&~G + +#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()); + } + } + } +} From ceb297d08d845989b4ee865eb676657cd2733aaa Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Wed, 18 Sep 2019 11:46:09 +0100 Subject: [PATCH 13/13] Add documentation for context-include/exclude --- jbmc/src/java_bytecode/java_bytecode_language.h | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 8fa7d586f4a..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,7 +299,13 @@ 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 + /// 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; };