Refinements to `class_method_descriptor_exprt` #5145

thomasspriggs · 2019-10-03T10:11:37Z

This PR renames the components of class_method_descriptor_exprt, in order to make their purpose clearer. The constructor of this class and its getters are documented and validation is added.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
~~The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/~~ N/A (No user visible behaviour.)
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).~~ N/A (None 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.

The class as stored in an `class_method_descriptor_exprt` is actually a unique identifier of the class in the symbol table. Therefore it makes sense to refer to it as a `class_id` rather than just as a name.

Because it is preferable to use the interface provided.

This is specifically the name of the method only. Not any other part of the expression.

The component to which a `class_method_descriptor_exprt` is referring to is specifically a particular overload of a method. The particular overload is distinguished based on a mangling process. Therefore `mangled_method_name` more accurately describes that this component is the the mangled name of a method, as opposed to any other kind of class component such as a field.

This makes it possible to find the code for constructing the identifier for a `class_method_descriptor_exprt` by looking at `class_method_descriptor_exprt` only. Where as previously it would have been neccessary to search for all places where the contructor was used.

To complete the documentation of each of the getters.

In order to ensure we an invalid expression is never constructed or cast to.

As the expresion is now checked on construction and casting, we no longer need check for its validity in the places where it is used.

To complete the complete the documentation of the constructor.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 89d2d73).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/130227916

thk123

Couple of questions but lgtm. But the 💡 seems to be like a really strong improvement

src/util/std_expr.h

thk123 · 2019-10-03T13:42:27Z

jbmc/src/java_bytecode/ci_lazy_methods.cpp

-    const irep_idt method_name = get_virtual_method_target(
-      instantiated_classes, call_basename, call_class, symbol_table);
-    CHECK_RETURN(!method_name.empty());
+    const irep_idt &method_name = virtual_function.mangled_method_name();


⛏️ keep one rename per commit in future

❓ method_name and method_id is confusing as to what is the difference between them. Perhaps method_name and resolved_method_symbol_id?

Would it be an improvement if I renamed the method_name variable to mangled_method_name?

src/util/std_expr.h

smowton

One suggestion

smowton · 2019-10-03T13:54:51Z

jbmc/src/java_bytecode/ci_lazy_methods.cpp

-    const irep_idt method_name = get_virtual_method_target(
-      instantiated_classes, call_basename, call_class, symbol_table);
-    CHECK_RETURN(!method_name.empty());
+    const irep_idt &method_name = virtual_function.mangled_method_name();


Might be easier if we used method_base_name and mangled_method_base_name, making it clear that neither includes the package/class qualifiers?

To me, base_name means "not mangled". So mangled_method_base_name would read as a contradiction.

hannes-steffenhagen-diffblue · 2019-12-03T11:22:43Z

src/util/std_expr.h

  }
 };

+inline void validate_expr(const class class_method_descriptor_exprt &value)


I’m not sure what the class keyword is doing here. Seems redundant?

It isn't redundant. It is an inline forward declaration of the class_method_descriptor_exprt class. The forward declaration of this validate_expr function needs to be before the definition of the class_method_descriptor_exprt class because it is used from inside the classes constructor. The class also needs to be forward declared in order for the function forward declaration to be valid. So the two forward declarations break a cyclic dependency problem and can't be removed without either re-introducing the problem, or defining the constructor out of line instead of in-line. I could remove the keyword class from this line of code and put class class_method_descriptor_exprt; on the proceeding line, but this was a little more succinct.

FWIW coding guidelines say forward declarations should be put at the top of the file with the includes

Ah, I'll try and remember for next time.

src/util/std_expr.h

thomasspriggs added 8 commits October 3, 2019 10:52

Rename class_name in class_method_descriptor_exprt to class_id

bfbcffd

The class as stored in an `class_method_descriptor_exprt` is actually a unique identifier of the class in the symbol table. Therefore it makes sense to refer to it as a `class_id` rather than just as a name.

Replace direct access to ID_C_class

2ac75d2

Because it is preferable to use the interface provided.

Rename base_name to base_method_name

944a3f3

This is specifically the name of the method only. Not any other part of the expression.

Document identifier of class_method_descriptor_exprt

05930c3

To complete the documentation of each of the getters.

Validate class_method_descriptor_exprt thoroughly

dd07600

In order to ensure we an invalid expression is never constructed or cast to.

Remove external checks of class_method_descriptor_exprt

d2d7736

As the expresion is now checked on construction and casting, we no longer need check for its validity in the places where it is used.

thomasspriggs requested review from cesaro, cristina-david, kroening, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners October 3, 2019 10:11

thomasspriggs force-pushed the tas/virtual-function-expr branch from 92e1859 to d2d7736 Compare October 3, 2019 10:12

thomasspriggs requested a review from JohnDumbell October 3, 2019 11:12

Document _type of class_method_descriptor_exprt

89d2d73

To complete the complete the documentation of the constructor.

allredj reviewed Oct 3, 2019

View reviewed changes

thk123 reviewed Oct 3, 2019

View reviewed changes

smowton approved these changes Oct 3, 2019

View reviewed changes

hannes-steffenhagen-diffblue reviewed Dec 3, 2019

View reviewed changes

thk123 approved these changes Dec 3, 2019

View reviewed changes

thomasspriggs merged commit 5e95689 into diffblue:develop Dec 3, 2019

thomasspriggs deleted the tas/virtual-function-expr branch December 3, 2019 13:31

Refinements to class_method_descriptor_exprt #5145

Refinements to class_method_descriptor_exprt #5145

Uh oh!

Conversation

thomasspriggs commented Oct 3, 2019 • 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!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Refinements to `class_method_descriptor_exprt` #5145

Refinements to `class_method_descriptor_exprt` #5145

thomasspriggs commented Oct 3, 2019 •

edited

Loading