remove java_method_typet::final/native #4492

kroening · 2019-04-06T19:17:51Z

This removes four methods from java_method_typet. They do not belong there,
as neither 'native' nor 'final' are part of the type of the method (they are
field modifiers). They are never read.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

kroening · 2019-04-06T20:09:06Z

The string table test will work again if #4493 is merged before.

smowton · 2019-04-08T08:41:55Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -431,7 +430,7 @@ void java_bytecode_convert_methodt::convert(
  // to the symbol later.
  java_method_typet method_type =
    to_java_method_type(symbol_table.lookup_ref(method_identifier).type);
-  method_type.set_is_final(m.is_final);
+  method_type.set(ID_C_class, class_symbol.name);


Suspect this is a mis-merge; this is now done by set_declaring_class above.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d752fcf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107442981
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

Resolved

smowton · 2019-04-08T13:59:16Z

Removed my blocking flag but not approved pending @thk123 or similar checking if especially final is relevant to TG

peterschrammel

Access, final, native should be attached to symbolt instead of the type.

peterschrammel

I'm afraid this requires suggested fix and a goto-binary version bump.

thk123

I don't think I fully understand the comment "they are field modifiers". Currently methods are not stored as fields, and native and final are method modifiers:

A final method is a method that can't be overriden
a native method is one whose implementation is not in Java.

I guess they would live on the symbol annotations in the perfect world (like the owning class), but currently these annotations are stored on the method type.

Both these methods are currently used in test-gen, hence adding the tests in CBMC

kroening · 2019-05-04T14:16:40Z

@peterschrammel No, the access modifiers are not part of the method symbol either. They are properties of the field of the class.

kroening · 2019-06-18T21:00:54Z

@thk123 @peterschrammel Let me ping you on this one. Note that we do have the methods in the class, including access, final, native. This matches what a JVM would do pretty well.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 5d1d024).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/116035526
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

codecov-io · 2019-06-18T21:51:44Z

Codecov Report

Merging #4492 into develop will decrease coverage by <.01%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #4492      +/-   ##
===========================================
- Coverage    69.29%   69.29%   -0.01%     
===========================================
  Files         1306     1306              
  Lines       108263   108242      -21     
===========================================
- Hits         75023    75007      -16     
+ Misses       33240    33235       -5

Impacted Files	Coverage Δ
...de/java_bytecode_convert_method/convert_method.cpp	`100% <ø> (ø)`	⬆️
...src/java_bytecode/java_bytecode_convert_method.cpp	`97.48% <ø> (-0.01%)`	⬇️
jbmc/src/java_bytecode/java_types.h	`100% <ø> (ø)`	⬆️
src/solvers/flattening/boolbv_get.cpp	`78.66% <0%> (+3.33%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 9643ec2...2c3cb15. Read the comment docs.

thk123 · 2019-06-19T09:13:12Z

@kroening ~~Happy to discuss this but don't feel like I've got an answer to my question?~~

As this PR currently stands we lose the ability to know if a particular method is marked as final - which we need in TG. I think I agree that it belongs on the symbol for the method, not on the type itself (both a final and non-final method can be assigned into the interface), but as it stands I don't think we have a way to store this kind of information on the symbol.

Re-read your new comment - I see your suggesting getting this info out of the class type. This could work - I'll have a look how much work it would be.

kroening · 2019-06-19T14:00:22Z

Note that this would create some consistency in the approach: one would do the same for fields and for methods.
A thing that bugs me is that as of now static fields are not in the class type. I'll separately look into that.

jeannielynnmoulton

This information does not appear to be available via java_class_typet methods() yet. methods() is empty.

This line
https://github.com/diffblue/cbmc/pull/4492/files#diff-985ab35118d62c4f1961c30173211fb6L2245
(and this test
https://github.com/diffblue/cbmc/pull/4492/files#diff-4831c2334c252ee2ff67d6334690fb09L172)
contains important information in test-gen for mocking.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 2c3cb15).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121239512
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

This removes four methods from java_method_typet. They do not belong there, as neither 'native' nor 'final' are part of the type of the method (they are field modifiers). They are never read.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 6abaf25).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121878421
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

kroening requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners April 6, 2019 19:17

kroening added cleanup Java Front End labels Apr 6, 2019

kroening changed the title ~~remove java_method_typet::final/native~~ remove java_method_typet::final/native [depends on: #4493] Apr 6, 2019

smowton previously requested changes Apr 8, 2019

View reviewed changes

kroening force-pushed the cleanup_java_method_type branch 2 times, most recently from 64cafa2 to d752fcf Compare April 8, 2019 09:19

allredj reviewed Apr 8, 2019

View reviewed changes

tautschnig changed the title ~~remove java_method_typet::final/native [depends on: #4493]~~ remove java_method_typet::final/native Apr 8, 2019

tautschnig assigned smowton Apr 8, 2019

peterschrammel reviewed Apr 8, 2019

View reviewed changes

peterschrammel requested changes Apr 8, 2019

View reviewed changes

thk123 suggested changes Apr 9, 2019

View reviewed changes

peterschrammel assigned kroening and unassigned smowton Apr 10, 2019

kroening force-pushed the cleanup_java_method_type branch from d752fcf to abc4eac Compare May 1, 2019 15:11

kroening force-pushed the cleanup_java_method_type branch from abc4eac to 0fcc497 Compare May 4, 2019 14:17

kroening assigned thk123 and peterschrammel and unassigned kroening May 4, 2019

kroening force-pushed the cleanup_java_method_type branch from 0fcc497 to 5d1d024 Compare June 18, 2019 20:59

allredj reviewed Jun 18, 2019

View reviewed changes

jeannielynnmoulton suggested changes Jul 2, 2019

View reviewed changes

kroening force-pushed the cleanup_java_method_type branch from 5d1d024 to 2c3cb15 Compare July 30, 2019 10:58

allredj reviewed Jul 30, 2019

View reviewed changes

remove java_method_typet::final/native

6abaf25

This removes four methods from java_method_typet. They do not belong there, as neither 'native' nor 'final' are part of the type of the method (they are field modifiers). They are never read.

kroening force-pushed the cleanup_java_method_type branch from 2c3cb15 to 6abaf25 Compare August 4, 2019 15:02

allredj reviewed Aug 4, 2019

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

remove java_method_typet::final/native #4492

remove java_method_typet::final/native #4492

kroening commented Apr 6, 2019

kroening commented Apr 6, 2019

smowton Apr 8, 2019

kroening Apr 8, 2019

allredj left a comment

smowton commented Apr 8, 2019

peterschrammel left a comment

peterschrammel left a comment •

edited

Loading

thk123 left a comment

kroening commented May 4, 2019

kroening commented Jun 18, 2019

allredj left a comment

codecov-io commented Jun 18, 2019 •

edited

Loading

thk123 commented Jun 19, 2019 •

edited

Loading

kroening commented Jun 19, 2019

jeannielynnmoulton left a comment

allredj left a comment

allredj left a comment

remove java_method_typet::final/native #4492

Are you sure you want to change the base?

remove java_method_typet::final/native #4492

Conversation

kroening commented Apr 6, 2019

kroening commented Apr 6, 2019

smowton Apr 8, 2019

Choose a reason for hiding this comment

kroening Apr 8, 2019

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

smowton commented Apr 8, 2019

peterschrammel left a comment

Choose a reason for hiding this comment

peterschrammel left a comment • edited Loading

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

kroening commented May 4, 2019

kroening commented Jun 18, 2019

allredj left a comment

Choose a reason for hiding this comment

codecov-io commented Jun 18, 2019 • edited Loading

Codecov Report

thk123 commented Jun 19, 2019 • edited Loading

kroening commented Jun 19, 2019

jeannielynnmoulton left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

peterschrammel left a comment •

edited

Loading

codecov-io commented Jun 18, 2019 •

edited

Loading

thk123 commented Jun 19, 2019 •

edited

Loading