exprt::opX cleanup #3465

kroening · 2018-11-26T10:36:00Z

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.

tautschnig · 2018-11-26T10:43:00Z

src/goto-symex/slice_by_trace.cpp

-          u_rhs.copy_to_operands(guard);
-          u_rhs.copy_to_operands(merge[j]);
-          u_rhs.op0().make_not();
+          u_rhs.add_to_operands(not_exprt(guard), merge[j]);


make_not is slightly different to this one - maybe use boolean_negate instead?

tautschnig · 2018-11-26T10:54:43Z

src/analyses/invariant_set.cpp

+        if(
+          to_bitvector_type(typecast_expr.type()).get_width() >=
+          to_bitvector_type(typecast_expr.op().type()).get_width())
+          return build_string(typecast_expr.op());


Nit pick: please add braces for readability

tautschnig · 2018-11-26T10:56:16Z

src/analyses/invariant_set.cpp

-    if(expr.type().id()==ID_signedbv ||
-       expr.type().id()==ID_unsignedbv)
+    if(
+      typecast_expr.type().id() == ID_signedbv ||


Suggestion that I shouldn't be making because out-of-scope for this PR: we use typecast_expr.type().id() and typecast_expr.op().type().id() several times in here, maybe add some temporaries?

tautschnig · 2018-11-26T10:57:06Z

src/analyses/invariant_set.cpp

@@ -137,8 +140,8 @@ std::string inv_object_storet::build_string(const exprt &expr) const

  if(expr.id()==ID_member)
  {
-    assert(expr.operands().size()==1);
-    return build_string(expr.op0())+"."+expr.get_string(ID_component_name);
+    return build_string(to_member_expr(expr).struct_op()) + "." +


I believe .struct_op() is deprecated in favour of .compound() (here and below).

tautschnig · 2018-11-26T11:01:31Z

src/analyses/invariant_set.cpp

    {
-      assert(expr.op1().operands().size()==1);
-      add_type_bounds(expr.op0(), expr.op1().op0().type());
+      assert(equal_expr.op1().operands().size() == 1);


We can safely get rid of this by using to_typecast_expr below. Repeats once more below.

That would also get rid of the use of assert rather than INVARIANT too....

tautschnig · 2018-11-26T11:01:48Z

src/analyses/invariant_set.cpp

-       get_object(expr.op1(), p.second))
+    if(
+      get_object(equal_expr.op0(), p.first) ||
+      get_object(equal_expr.op1(), p.second))


Nit pick: please add braces for readability.

tautschnig · 2018-11-26T11:02:06Z

src/analyses/invariant_set.cpp

-       get_object(expr.op1(), p.second))
+    if(
+      get_object(notequal_expr.op0(), p.first) ||
+      get_object(notequal_expr.op1(), p.second))


Nit pick: please add braces for readability.

chrisr-diffblue

I agree with the comments Michael made, but otherwise looks like a nice cleanup to me.

chrisr-diffblue · 2018-11-26T11:15:46Z

src/analyses/invariant_set.cpp

    {
-      assert(expr.op1().operands().size()==1);
-      add_type_bounds(expr.op0(), expr.op1().op0().type());
+      assert(equal_expr.op1().operands().size() == 1);


That would also get rid of the use of assert rather than INVARIANT too....

allredj

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

allredj

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

kroening added the cleanup label Nov 26, 2018

kroening requested review from chrisr-diffblue, martin-cs, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners November 26, 2018 10:36

kroening force-pushed the expr-op-cleanup branch from a991544 to b39c559 Compare November 26, 2018 10:38

tautschnig approved these changes Nov 26, 2018

View reviewed changes

tautschnig assigned kroening Nov 26, 2018

chrisr-diffblue approved these changes Nov 26, 2018

View reviewed changes

kroening force-pushed the expr-op-cleanup branch 3 times, most recently from 133bdb3 to 480544c Compare November 26, 2018 23:53

allredj reviewed Nov 27, 2018

View reviewed changes

avoid exprt::op0, exprt::op1, exprt::op2

0942e1f

kroening force-pushed the expr-op-cleanup branch from 480544c to 0942e1f Compare November 27, 2018 06:57

allredj reviewed Nov 27, 2018

View reviewed changes

tautschnig merged commit d314770 into develop Nov 27, 2018

tautschnig deleted the expr-op-cleanup branch November 27, 2018 08:28

exprt::opX cleanup #3465

exprt::opX cleanup #3465

Uh oh!

Conversation

kroening commented Nov 26, 2018

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!

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!

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

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!

Uh oh!