Java frontend: treat CProver stubbed methods more like normal stubs #4258
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
smowton
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli and
thk123
as code owners
tautschnig
approved these changes
Feb 22, 2019
| ^SIGNAL=0$ | ||
| -- | ||
| -- | ||
| This calls to CProver.startThread, which are special-cased by the Java front-end (which omits the method's body |
| -- | ||
| -- | ||
| This calls to CProver.startThread, which are special-cased by the Java front-end (which omits the method's body | ||
| in hope of the front-end handling it like a stub), but which don't get their parameter names assigned by the usual |
There was a problem hiding this comment.
s/don't/doesn't/ s/their/its/
thk123
approved these changes
Feb 22, 2019
| @@ -406,8 +415,9 @@ void java_bytecode_convert_methodt::convert( | |||
| // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table | |||
| // to retrieve the symbol (constructed by java_bytecode_convert_method_lazy) | |||
| // associated to the method | |||
| const irep_idt method_identifier= | |||
| id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor; | |||
| const irep_idt method_identifier = | |||
There was a problem hiding this comment.
I mean not your code, but why do we have a local variable method_identifier that then is immediately assigned into method_id, perhaps just directly assign?
smowton
force-pushed
the
smowton/fix/java-fake-stubs-parameter-identifiers
branch
from
73a2c88 to
1681dfa
Compare
smowton
changed the title
|
@tautschnig @thk123 that solution didn't work for symex-driven-lazy-loading, so I completely changed my approach; see updated description. |
thk123
approved these changes
Feb 22, 2019
tautschnig
approved these changes
Feb 22, 2019
| static irep_idt org_cprover_CProver_name = "org.cprover.CProver"; | ||
| return | ||
| (class_name == org_cprover_CProver_name && | ||
| cprover_methods_to_ignore.count(id2string(method.name))) || |
There was a problem hiding this comment.
nit-pick: Visual Studio would like to have an explicit != 0 with .count(...).
We already tried to ignore org.cprover.CProver methods such as nondetInt, relying upon the front-end to supply stub bodies if desired based on their type. However, by creating symbols for them as for normal (non-stub) methods, but then refusing to provide a body or advertise them as normal methods, we failed to set up their type properly (specifically the parameter names), as they were neither set like a stub (upon symbol creation, upon discovery by a caller) or like a normal method (during java_bytecode_convert_method). By refusing to create the symbol at all, this treats the special CProver methods more like normal stubs: their symbols are now created on demand. It is also no longer necessary for java_bytecode_languaget::methods_provided to special case them, as they are not added to method_bytecodet either, again matching "real" stub methods more closely.
smowton
force-pushed
the
smowton/fix/java-fake-stubs-parameter-identifiers
branch
from
1681dfa to
4c724de
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We already tried to ignore org.cprover.CProver methods such as nondetInt, relying upon
the front-end to supply stub bodies if desired based on their type. However, by creating
symbols for them as for normal (non-stub) methods, but then refusing to provide a body or
advertise them as normal methods, we failed to set up their type properly (specifically
the parameter names), as they were neither set like a stub (upon symbol creation, upon
discovery by a caller) or like a normal method (during java_bytecode_convert_method). By
refusing to create the symbol at all, this treats the special CProver methods more like
normal stubs: their symbols are now created on demand.
It is also no longer necessary for java_bytecode_languaget::methods_provided to special
case them, as they are not added to method_bytecodet either, again matching "real" stub
methods more closely.