Use generic signature for local variables with entry in LVTT by mgudemann · Pull Request #2975 · diffblue/cbmc

mgudemann · 2018-09-18T10:38:17Z

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.

allredj

Passed Diffblue compatibility checks (cbmc commit: 574de4e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85130707

smowton

Tests situation for this?

smowton · 2018-09-19T09:14:19Z

jbmc/src/java_bytecode/java_local_variable_table.cpp

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


smowton · 2018-09-19T09:14:40Z

jbmc/src/java_bytecode/java_local_variable_table.cpp

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


Should probably invariant that these are found

mgudemann · 2018-09-20T14:02:16Z

@smowton this is used/required in TG

smowton · 2018-09-20T14:05:20Z

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 · 2018-09-20T14:08:14Z

@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.

hannes-steffenhagen-diffblue · 2018-09-20T14:10:42Z

jbmc/src/java_bytecode/java_local_variable_table.cpp

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


⛏️
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)

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 · 2018-09-20T14:11:57Z

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

hannes-steffenhagen-diffblue · 2018-09-20T14:13:05Z

jbmc/src/java_bytecode/java_local_variable_table.cpp

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


Could this go into a separate function, something along the lines of class_name_from_method_name?

allredj

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

allredj

Passed Diffblue compatibility checks (cbmc commit: 405fe5f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85435436

mgudemann · 2018-09-20T15:46:12Z

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

allredj

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

allredj

Passed Diffblue compatibility checks (cbmc commit: d13a73f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85447907

smowton

Excellent, thankyou very much for doing the extra work!

tautschnig · 2018-09-20T17:17:07Z

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 · 2018-09-20T18:41:53Z

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

allredj

Passed Diffblue compatibility checks (cbmc commit: 5a0feaa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85471472

peterschrammel

LGTM

mgudemann added the work in progress label Sep 18, 2018

mgudemann self-assigned this Sep 18, 2018

mgudemann requested review from NathanJPhillips, cesaro, cristina-david, peterschrammel, pkesseli, smowton and thk123 as code owners September 18, 2018 10:38

allredj reviewed Sep 18, 2018

View reviewed changes

tautschnig mentioned this pull request Sep 18, 2018

Store the final status of fields in componentt #2976

Merged

7 tasks

smowton reviewed Sep 19, 2018

View reviewed changes

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 removed the work in progress label Sep 20, 2018

hannes-steffenhagen-diffblue reviewed Sep 20, 2018

View reviewed changes

allredj reviewed Sep 20, 2018

View reviewed changes

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

allredj reviewed Sep 20, 2018

View reviewed changes

smowton approved these changes Sep 20, 2018

View reviewed changes

Use generic signature for local variables with entry in LVTT

0bad0d6

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.

Add unit test to check for generic local variables

5a0feaa

The test checks that a local variable has the correct generic type and instantiation.

mgudemann force-pushed the feature/jbmc/local_variables_generic_types branch from d13a73f to 5a0feaa Compare September 20, 2018 18:32

allredj reviewed Sep 20, 2018

View reviewed changes

peterschrammel approved these changes Sep 21, 2018

View reviewed changes

mgudemann merged commit 204437e into diffblue:develop Sep 21, 2018

mgudemann deleted the feature/jbmc/local_variables_generic_types branch September 21, 2018 06:46

Conversation

mgudemann commented Sep 18, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Sep 19, 2018

Choose a reason for hiding this comment

Uh oh!

smowton Sep 19, 2018

Choose a reason for hiding this comment

Uh oh!

mgudemann commented Sep 20, 2018

Uh oh!

smowton commented Sep 20, 2018

Uh oh!

mgudemann commented Sep 20, 2018

Uh oh!

hannes-steffenhagen-diffblue Sep 20, 2018

Choose a reason for hiding this comment

Uh oh!

mgudemann Sep 20, 2018

Choose a reason for hiding this comment

Uh oh!

smowton commented Sep 20, 2018

Uh oh!

hannes-steffenhagen-diffblue Sep 20, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

mgudemann commented Sep 20, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Sep 20, 2018

Uh oh!

mgudemann commented Sep 20, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

mgudemann commented Sep 18, 2018 •

edited

Loading