Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt #4524

antlechner · 2019-04-12T16:19:22Z

This PR removes some parameters to constructors that are not necessary. There is no functional change.
If you think the constructor for plus_exprt that takes two exprts and a typet should be deprecated or deleted, please let me know.

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/
n/a 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).
n/a 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.

I came across a few places where the single-parameter constructor was not used yet and the information about the type of the expression was duplicated, so I tidied up all occurrences of this that I could find.

The type of the plus_exprt is the type of the lhs by default. This is always the case in the code base.

allredj

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

tautschnig

My apologies for all the additional wishlist-type requests. This is very nice cleanup, it just invites even more cleanup...

tautschnig · 2019-04-12T19:13:52Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

-    dereference_exprt old_array(this_symbol.symbol_expr(), struct_tag_type);
-    dereference_exprt new_array(local_symexpr, struct_tag_type);
+    dereference_exprt old_array{this_symbol.symbol_expr()};
+    dereference_exprt new_array{local_symexpr};


So in order to confirm that this is correct I had to read some more code, and the same is happening below: apologies that I'll come up with (almost) unrelated requests for fixes. For this one: local_symexpr is declared as a const reference, but .symbol_expr returns by value, so that's a reference to a temporary. Can you please remove the reference from local_symexpr?

tautschnig · 2019-04-12T19:15:49Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1623,7 +1623,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(

      const typecast_exprt pointer(op[0], java_array_type(statement[0]));

-      dereference_exprt array(pointer, pointer.type().subtype());
+      dereference_exprt array{pointer};
      PRECONDITION(pointer.type().subtype().id() == ID_struct_tag);


I have no idea why this PRECONDITION is important right here, but if it for some reason needs to be enforced: PRECONDITION(array.type().id() == ID_struct_tag) would be less opaque - but actually makes me wonder whether the name array is a particularly good choice?

tautschnig · 2019-04-12T21:59:11Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1623,7 +1623,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(

      const typecast_exprt pointer(op[0], java_array_type(statement[0]));

-      dereference_exprt array(pointer, pointer.type().subtype());
+      dereference_exprt array{pointer};


We should actually use either std::move(pointer) (and get rid of the const) or just do array{typecast_exprt{op[0], java_array_type(statement[0])}}. Applies here and in several other places.

tautschnig · 2019-04-12T22:03:08Z

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1102,8 +1102,7 @@ void java_object_factoryt::array_primitive_init_code(

  // *array_data_init = NONDET(TYPE [max_length_expr]);
  side_effect_expr_nondett nondet_data(array_type, location);
-  const dereference_exprt data_pointer_deref(
-    tmp_finite_array_pointer, array_type);
+  const dereference_exprt data_pointer_deref{tmp_finite_array_pointer};


~~Get rid of const and use std::move(data_pointer_deref) below.~~

tautschnig · 2019-04-12T22:03:38Z

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1303,7 +1301,7 @@ void java_object_factoryt::gen_nondet_array_init(
    is_valid_java_array(struct_type),
    "Java struct array does not conform to expectations");

-  dereference_exprt deref_expr(expr, expr.type().subtype());
+  dereference_exprt deref_expr(expr);


Braces (as introduced in all the other places)

I knew I would forget them somewhere!

tautschnig · 2019-04-12T22:07:08Z

src/goto-programs/string_abstraction.cpp

-        dereference_exprt(rhs, rhs.type().subtype()));
+  else if(lhs.type().id() == ID_pointer)
+    return value_assignments(
+      dest, target, dereference_exprt{lhs}, dereference_exprt{rhs});


Please add braces as this is (always was) a multi-line statement in the body of an if.

smowton

MT's suggestions are good, but this is also good to merge as-is in my opinion, so I'd say feel free to merge and follow up addressing those suggestions

antlechner · 2019-04-15T09:49:33Z

@tautschnig Thank you for your suggestions, I'll try to find time to make a PR for them but I have a few higher priority tasks to get through first.

tautschnig · 2019-04-15T09:57:40Z

@antlechner Oops, sorry, I should have posted on here: I think I've taken care of them in #4532.

antlechner added the cleanup label Apr 12, 2019

antlechner requested review from romainbrenguier and majakusber April 12, 2019 16:19

antlechner requested review from allredj, cesaro, chrisr-diffblue, cristina-david, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, NathanJPhillips, owen-mc-diffblue, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners April 12, 2019 16:19

antlechner force-pushed the antonia/fewer-param-constructors branch from f6f8e2f to ba7c8ac Compare April 12, 2019 16:20

antlechner mentioned this pull request Apr 12, 2019

Refactor element access of pointer arrays into a separate function #4525

Merged

2 tasks

antlechner added 2 commits April 12, 2019 18:16

Use single-parameter dereference_exprt constructor if possible

fda5ca0

I came across a few places where the single-parameter constructor was not used yet and the information about the type of the expression was duplicated, so I tidied up all occurrences of this that I could find.

Use plus_exprt constructor that does not take a type

cdb0133

The type of the plus_exprt is the type of the lhs by default. This is always the case in the code base.

antlechner force-pushed the antonia/fewer-param-constructors branch from ba7c8ac to cdb0133 Compare April 12, 2019 17:16

allredj reviewed Apr 12, 2019

View reviewed changes

tautschnig approved these changes Apr 12, 2019

View reviewed changes

smowton approved these changes Apr 13, 2019

View reviewed changes

tautschnig merged commit 21811fa into diffblue:develop Apr 13, 2019

tautschnig mentioned this pull request Apr 13, 2019

Java bytecode conversion: inline or move temporaries #4532

Merged

3 tasks

antlechner deleted the antonia/fewer-param-constructors branch April 15, 2019 09:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt #4524

Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt #4524

antlechner commented Apr 12, 2019

allredj left a comment

tautschnig left a comment

tautschnig Apr 12, 2019

tautschnig Apr 12, 2019

tautschnig Apr 12, 2019

tautschnig Apr 12, 2019 •

edited

Loading

tautschnig Apr 12, 2019

antlechner Apr 15, 2019

tautschnig Apr 12, 2019

smowton left a comment

antlechner commented Apr 15, 2019

tautschnig commented Apr 15, 2019

Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt #4524

Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt #4524

Conversation

antlechner commented Apr 12, 2019

allredj left a comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Apr 12, 2019

Choose a reason for hiding this comment

tautschnig Apr 12, 2019

Choose a reason for hiding this comment

tautschnig Apr 12, 2019

Choose a reason for hiding this comment

tautschnig Apr 12, 2019 • edited Loading

Choose a reason for hiding this comment

tautschnig Apr 12, 2019

Choose a reason for hiding this comment

antlechner Apr 15, 2019

Choose a reason for hiding this comment

tautschnig Apr 12, 2019

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

antlechner commented Apr 15, 2019

tautschnig commented Apr 15, 2019

tautschnig Apr 12, 2019 •

edited

Loading