[TG-9294][UFC] Fix context-include/exclude jbmc options #5115
Conversation
antlechner
requested review from
peterschrammel,
romainbrenguier and
segun3d
antlechner
requested review from
cesaro,
cristina-david,
kroening,
NathanJPhillips,
pkesseli,
smowton,
tautschnig and
thk123
as code owners
antlechner
changed the title
| void operator()( | ||
| const symbolt &class_symbol, | ||
| const methodt &method, | ||
| const optionalt<prefix_filtert> method_context) |
jbmc/src/jbmc/jbmc_parse_options.cpp
Outdated
| INVARIANT( | ||
| symbol, | ||
| "Tried to generate a stub body for function that is not in the symbol " | ||
| "table: " + |
There was a problem hiding this comment.
⛏️ the invariant message should rather be formulated to state what should normally be true.
There was a problem hiding this comment.
The commit that this was in has been removed as it wasn't compatible with symex-driven lazy loading. 🚗
| typedef std::function<bool( | ||
| const irep_idt &function_name, | ||
| symbol_table_baset &symbol_table, | ||
| goto_functiont &function)> |
There was a problem hiding this comment.
⛏️ using is preferred
| @@ -7,6 +7,5 @@ Main.class | |||
| .* line 11 assertion at file Main.java line 11 .*: SUCCESS | |||
| .* line 12 assertion at file Main.java line 12 .*: SUCCESS | |||
| -- | |||
| WARNING: no body for function .* | |||
There was a problem hiding this comment.
❓ is this one removed because it is useless, or does the warning now appear?
There was a problem hiding this comment.
Because it's (probably) useless. There is a test in a later commit that checks that the body of an excluded method is a stub-style "return nondet" body. Do you think it still makes sense to check for WARNING: ... as a negative regex everywhere?
There was a problem hiding this comment.
If there is no way this warning could be produced for any input then it can be removed, otherwise it's probably safer to keep it in just in case.
There was a problem hiding this comment.
I'm keeping it as a negative regex here now, and also added it as a negative regex in all existing tests and the new tests for exclude package and exclude absent.
antlechner
force-pushed
the
antonia/context-include
branch
3 times, most recently
from
ce883b8 to
e54b2cc
Compare
| --context-exclude org.cprover.other --function ExcludedProperties.runtimeReturnType | ||
| ^EXIT=10$ | ||
| ^SIGNAL=0$ | ||
| .* line 30 assertion at file ExcludedProperties.java line 30.*: FAILURE |
There was a problem hiding this comment.
❓ there is no assertion line 30, as far as I can see, I mean 28?
There was a problem hiding this comment.
As discussed, this was a result of a late clang-format run (30 was correct before clang-format) and should be fixed now.
| @@ -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( | |||
There was a problem hiding this comment.
⛏️ should be documented
There was a problem hiding this comment.
It is documented in the header file.
| const auto public_instance_type = | ||
| type_try_dynamic_cast<java_method_typet>(public_instance_symbol.type); | ||
| REQUIRE(public_instance_type); | ||
| REQUIRE(id2string(public_instance_type->get(ID_access)) == "public"); |
There was a problem hiding this comment.
⛏️ compare to ID_public, and use get_access 💎
| THEN( | ||
| "Meta-information of excluded methods is preserved. Symbol values are " | ||
| "nil as the lazy_goto_modelt for unit tests does not generate " | ||
| "stub/exclude bodies.") |
There was a problem hiding this comment.
⛏️ it would be nice to have several THEN sections to structure the test and make it easier to identify what goes wrong when something does.
There was a problem hiding this comment.
Now grouped into several THEN sections where each is about one property of excluded method symbols.
| const auto private_static_type = | ||
| type_try_dynamic_cast<java_method_typet>(private_static_symbol.type); | ||
| REQUIRE(private_static_type); | ||
| REQUIRE(id2string(private_static_type->get(ID_access)) == "private"); |
| default_final_static_symbol.type); | ||
| REQUIRE(default_final_static_type); | ||
| REQUIRE( | ||
| id2string(default_final_static_type->get(ID_access)) == "default"); |
| "stub/exclude bodies.") | ||
| { | ||
| const auto &public_instance_symbol = symbol_table.lookup_ref( | ||
| "java::ClassWithDifferentModifiers.testPublicInstance:()I"); |
There was a problem hiding this comment.
⛏️ would be better to use lookup and REQUIRE the result to be non-null 🦈
There was a problem hiding this comment.
Done. The REQUIREs had to go into the WHEN part, is that ok?
| REQUIRE_FALSE(public_instance_type->get_is_final()); | ||
|
|
||
| const auto &private_static_symbol = symbol_table.lookup_ref( | ||
| "java::ClassWithDifferentModifiers.testPrivateStatic:()I"); |
| REQUIRE_FALSE(private_static_type->get_is_final()); | ||
|
|
||
| const auto &protected_final_instance_symbol = symbol_table.lookup_ref( | ||
| "java::ClassWithDifferentModifiers.testProtectedFinalInstance:()I"); |
| REQUIRE(protected_final_instance_type->get_is_final()); | ||
|
|
||
| const auto &default_final_static_symbol = symbol_table.lookup_ref( | ||
| "java::ClassWithDifferentModifiers.testDefaultFinalStatic:()I"); |
|
It turns out my second fix (for assigning stub-like bodies to excluded methods) is too general and incompatible with symex-driven lazy loading. I will add an "in progress" label, and remove it once I've finished fixing that commit. |
antlechner
force-pushed
the
antonia/context-include
branch
2 times, most recently
from
b155932 to
67d8f97
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: cbf5320).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128352945
antlechner
force-pushed
the
antonia/context-include
branch
from
cbf5320 to
c5f02e4
Compare
The new name makes it clearer that this field defines a context, not a method.
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.
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.
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.
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.
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.
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.
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.
This is consistent with the location of the definition in the cpp file.
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.
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.
antlechner
force-pushed
the
antonia/context-include
branch
from
c5f02e4 to
ceb297d
Compare
|
@romainbrenguier I addressed your comments. I also fixed the issue with symex-driven lazy loading. A previous commit has been replaced with three new commits for the fix: Could you please review these new commits? |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: ceb297d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/128380227
Codecov Report
@@ Coverage Diff @@
## develop #5115 +/- ##
===========================================
+ Coverage 66.94% 69.73% +2.79%
===========================================
Files 1145 1323 +178
Lines 93627 109474 +15847
===========================================
+ Hits 62674 76339 +13665
- Misses 30953 33135 +2182
Continue to review full report at Codecov.
|
| @@ -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)); | |||
There was a problem hiding this comment.
Why is this line outside the if?
There was a problem hiding this comment.
Yes, it should be inside. Antonia is away for three days, so I've made a follow-up PR to make this change: #5121
| @@ -690,6 +690,8 @@ int jbmc_parse_optionst::get_goto_program( | |||
| std::unique_ptr<abstract_goto_modelt> &goto_model_ptr, | |||
| const optionst &options) | |||
| { | |||
| if(options.is_set("context-include") || options.is_set("context-exclude")) | |||
There was a problem hiding this comment.
It's ugly to repeat that here, but probably can't be fixed without cleaning up the language interface.
The specification I was given by @peterschrammel about how
--context-include/excludeshould work is the following:--context-includeand--context-excludeboth take a prefix of a Java package, class or method as an argument--context-includeand not matching a prefix in--context-excludeare "included", all other methods are "excluded".--context-include/excludearen't used. Equivalently,--context-includecan be seen as including everything by default (i.e. if not specified on the command line), and--context-excludecan be seen as including nothing by default.The last specification was not implemented properly. We left out some meta-information (e.g. parameter identifiers) and left the body as nil rather than assigning a stub-like body. This PR fixes both parts of this specification.