Skip to content

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

Conversation

mgudemann
Copy link
Contributor

@mgudemann mgudemann commented Sep 18, 2018

  • Each commit message has a non-empty body, explaining why the change was made.
  • My contribution is formatted in line with CODING_STANDARD.md.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Copy link
Contributor

@allredj allredj left a 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

Copy link
Contributor

@smowton smowton left a 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);
Copy link
Contributor

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(":(");
Copy link
Contributor

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

@mgudemann mgudemann force-pushed the feature/jbmc/local_variables_generic_types branch 2 times, most recently from 16d2572 to 405fe5f Compare September 20, 2018 13:00
@mgudemann
Copy link
Contributor Author

@smowton this is used/required in TG

@smowton
Copy link
Contributor

smowton commented Sep 20, 2018

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

@mgudemann
Copy link
Contributor Author

@smowton I don't think this change is visible to put it into a regression test, I could probably do a unit test.
Effectively the change is transparent for any code that doesn't make use of generic types.

INVARIANT(
method_name_end != std::string::npos &&
class_name_end != std::string::npos,
"Java method name does not have the right format.");

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)

Copy link
Contributor Author

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.

@smowton
Copy link
Contributor

smowton commented Sep 20, 2018

Can you see the result in --show-symbol-table, in the types of symbols generated for local variables, for example?

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);

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?

Copy link
Contributor

@allredj allredj left a 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).

Copy link
Contributor

@allredj allredj left a 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

@mgudemann mgudemann force-pushed the feature/jbmc/local_variables_generic_types branch from a76b03d to d13a73f Compare September 20, 2018 15:16
@mgudemann
Copy link
Contributor Author

@smowton @hannes-steffenhagen-diffblue added a unit test and adressed comments

Copy link
Contributor

@allredj allredj left a 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).

Copy link
Contributor

@allredj allredj left a 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

Copy link
Contributor

@smowton smowton left a 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!

@tautschnig
Copy link
Collaborator

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.
@mgudemann mgudemann force-pushed the feature/jbmc/local_variables_generic_types branch from d13a73f to 5a0feaa Compare September 20, 2018 18:32
@mgudemann
Copy link
Contributor Author

@tautschnig if you didn't understand, then we'd very likely have a problem!

Copy link
Contributor

@allredj allredj left a 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

Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@mgudemann mgudemann merged commit 204437e into diffblue:develop Sep 21, 2018
@mgudemann mgudemann deleted the feature/jbmc/local_variables_generic_types branch September 21, 2018 06:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants