-
Notifications
You must be signed in to change notification settings - Fork 274
Use generic signature for local variables with entry in LVTT #2975
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Use generic signature for local variables with entry in LVTT #2975
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: 574de4e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85130707
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Tests situation for this?
// TODO: might need changing once descriptor/signature issue is resolved | ||
t=java_type_from_string(v.var.descriptor); | ||
|
||
const std::string method_name = id2string(method_id); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
const ref
t=java_type_from_string(v.var.descriptor); | ||
|
||
const std::string method_name = id2string(method_id); | ||
const size_t method_name_end = method_name.rfind(":("); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should probably invariant that these are found
16d2572
to
405fe5f
Compare
@smowton this is used/required in TG |
And its tests aren't portable here? As it stands, as with anything only used in TG but supported in the CBMC main repository, there's a danger we break it without realising |
@smowton I don't think this change is visible to put it into a regression test, I could probably do a unit test. |
INVARIANT( | ||
method_name_end != std::string::npos && | ||
class_name_end != std::string::npos, | ||
"Java method name does not have the right format."); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
⛏️
Invariant string should describe why the invariant is true, not what happened when it failed - I.e. in this case it'd be something like "Always true because the syntax of Java method names looks like this".
Also, is it safe to assume that we won't have been fed a nonsensical class file or one with a weird new format here? (I'm guessing this isn't something that's likely to change, genuine question though)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
the current hypothesis is that we get a class file that is compiled from a java source by a java compiler
We have already had class files generated by compilers for other languages that did break some hypotheses.
Can you see the result in |
method_name_end != std::string::npos && | ||
class_name_end != std::string::npos, | ||
"Java method name does not have the right format."); | ||
const std::string class_name = method_name.substr(0, class_name_end); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could this go into a separate function, something along the lines of class_name_from_method_name
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR failed Diffblue compatibility checks (cbmc commit: 16d2572).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85430988
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: 405fe5f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85435436
a76b03d
to
d13a73f
Compare
@smowton @hannes-steffenhagen-diffblue added a unit test and adressed comments |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR failed Diffblue compatibility checks (cbmc commit: a76b03d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85444852
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: d13a73f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85447907
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Excellent, thankyou very much for doing the extra work!
I really like how this one evolved from a commit message that I wasn't able to decipher to a PR that even I understand. |
This uses the generic type information of the local variable type table for the type of local variables. Before, no local variable was considered to a have generic type.
The test checks that a local variable has the correct generic type and instantiation.
d13a73f
to
5a0feaa
Compare
@tautschnig if you didn't understand, then we'd very likely have a problem! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: 5a0feaa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85471472
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
Uh oh!
There was an error while loading. Please reload this page.