fix accesses to exprt::opX() in solvers/ #5025

kroening · 2019-08-15T13:44:59Z

This improves type safety.

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

allredj

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

smowton

Blocking for one breaking change, otherwise suggested optional improvements

smowton · 2019-08-15T17:01:51Z

src/solvers/flattening/arrays.cpp

-    DATA_INVARIANT(
-      a.operands().size()==1,
-      "typecast must have one operand");
+    const auto &typecast_op = to_typecast_expr(a);


I'd expect typecast_op to be to_typecast_expr(a).op(). Just typecast_expr?

smowton · 2019-08-15T17:03:05Z

src/solvers/flattening/arrays.cpp

-      a.op0().type().id()==ID_array,
-      ("unexpected array type cast from "+
-       a.op0().type().id_string()).c_str());
+      typecast_op.type().id() == ID_array,


Looks like you really did want typecast(...).op() above, this is a change of behaviour

indeed -- fixed

src/solvers/flattening/boolbv_quantifier.cpp

src/solvers/flattening/bv_pointers.cpp

smowton · 2019-08-15T17:18:36Z

src/solvers/smt2/smt2_conv.cpp

-             expr.op0().type().id()==ID_floatbv)))
+  else if(
+    !use_FPA_theory && expr.operands().size() >= 1 &&
+    (expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||


Suggest clang-format-off, the old style was much easier to read

smowton · 2019-08-15T17:22:53Z

src/solvers/strings/string_constraint_generator_main.cpp

-    arg.op0().op0().operands().size() == 2 &&
-    arg.op0().op0().op0().id() == ID_string_constant)
+    arg.operands().size() == 1 &&
+    to_unary_expr(arg).op().operands().size() == 1 &&


Any idea what this is expecting? The chain of op0s without checking what unary operation it's looking at seems suspicious

I think it's an equality whose lhs is an address_of string_constant -- @romainbrenguier ?

this could have been an address_of although I can't be sure now. This is most likely dead code, as this is for C programs, for which the solver is not tested currently, and wouldn't work without some clean-up.

allredj

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

codecov-io · 2019-08-15T22:27:36Z

Codecov Report

Merging #5025 into develop will increase coverage by <.01%.
The diff coverage is 73.15%.

@@             Coverage Diff             @@
##           develop    #5025      +/-   ##
===========================================
+ Coverage    67.33%   67.33%   +<.01%     
===========================================
  Files         1155     1155              
  Lines        94669    94684      +15     
===========================================
+ Hits         63744    63755      +11     
- Misses       30925    30929       +4

Flag	Coverage Δ
#cproversmt2	`42.64% <38.91%> (-0.01%)`	⬇️
#regression	`63.82% <54.08%> (ø)`	⬆️
#unit	`31.97% <18.47%> (+0.01%)`	⬆️

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.h	`100% <ø> (ø)`	⬆️
src/solvers/flattening/boolbv.h	`78.57% <ø> (ø)`	⬆️
src/solvers/refinement/bv_refinement.h	`100% <ø> (ø)`	⬆️
...lvers/strings/string_constraint_generator_main.cpp	`84% <0%> (-0.49%)`	⬇️
src/solvers/qbf/qdimacs_core.cpp	`0% <0%> (ø)`	⬆️
src/solvers/flattening/boolbv_update.cpp	`0% <0%> (ø)`	⬆️
...olvers/flattening/boolbv_constraint_select_one.cpp	`0% <0%> (ø)`	⬆️
src/solvers/flattening/boolbv_add_sub.cpp	`50% <100%> (+0.87%)`	⬆️
src/solvers/flattening/boolbv_bitwise.cpp	`90.32% <100%> (ø)`	⬆️
src/solvers/flattening/boolbv_ieee_float_rel.cpp	`86.66% <100%> (ø)`	⬆️
... and 19 more

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 001b6f9...8a6f9aa. Read the comment docs.

romainbrenguier · 2019-08-16T09:33:09Z

src/solvers/flattening/boolbv_bv_rel.cpp

-        #else
-        literalt literal=bv_utils.rel(bv0, expr.id(), bv1, rep);
+#else
+      literalt literal = bv_utils.rel(bv0, expr.id(), bv1, rep);


maybe this part of the code should be removed instead of reformatted

romainbrenguier · 2019-08-16T09:41:00Z

src/solvers/strings/string_constraint_generator_main.cpp

-    arg.op0().op0().operands().size() == 2 &&
-    arg.op0().op0().op0().id() == ID_string_constant)
+    arg.operands().size() == 1 &&
+    to_unary_expr(arg).op().operands().size() == 1 &&


this could have been an address_of although I can't be sure now. This is most likely dead code, as this is for C programs, for which the solver is not tested currently, and wouldn't work without some clean-up.

martin-cs

There are a number of locations where lhs() and rhs() can be used to make the code clearer and to remove the number of calls to op0() and op1() making them easier to locate and eliminate.

martin-cs · 2019-08-21T15:29:41Z

src/solvers/flattening/arrays.cpp

-    DATA_INVARIANT(
-      a.operands().size()==1,
-      "typecast must have one operand");
+    const auto &typecast_op = to_typecast_expr(a).op();


This is a definite improvement.

martin-cs · 2019-08-21T15:34:40Z

src/solvers/flattening/boolbv.cpp

@@ -201,7 +201,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
    if(expr.operands().size()!=1)
      return conversion_failed(expr);

-    std::size_t op_width=boolbv_width(expr.op0().type());
+    std::size_t op_width = boolbv_width(to_unary_expr(expr).op().type());


I'm not sure that width is a unary_exprt...

I'm not sure there's anything wrong here?

martin-cs · 2019-08-21T15:37:21Z

src/solvers/flattening/boolbv_add_sub.cpp

@@ -41,7 +41,7 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
    !operands.empty(),
    "operator " + expr.id_string() + " takes at least one operand");

-  const exprt &op0=expr.op0();
+  const exprt &op0 = to_multi_ary_expr(expr).op0();


Still has an op0 but probably unavoidable.

src/solvers/flattening/boolbv_bv_rel.cpp

martin-cs · 2019-08-21T15:41:51Z

src/solvers/flattening/boolbv_floatbv_op.cpp

-
-  if(operands.size()!=3)
-    throw "operator "+expr.id_string()+" takes three operands";
-
  const exprt &lhs = expr.op0();


For completeness and to make it easier to find remaining uses, these could be lhs(), rhs() and rounding_mode().

martin-cs · 2019-08-21T15:46:13Z

src/solvers/floatbv/float_bv.cpp

+  {
+    const auto &float_expr = to_ieee_float_op_expr(expr);
+    return div(
+      float_expr.op0(),


src/solvers/lowering/byte_operators.cpp

martin-cs · 2019-08-21T15:47:23Z

src/solvers/prop/bdd_expr.cpp

-    bddt op0 = from_expr_rec(bin_expr.op0());
-    bddt op1 = from_expr_rec(bin_expr.op1());
+    bddt op0 = from_expr_rec(to_binary_expr(bin_expr).op0());
+    bddt op1 = from_expr_rec(to_binary_expr(bin_expr).op1());


lhs() and rhs()

martin-cs · 2019-08-21T15:47:41Z

src/solvers/prop/prop_conv_solver.cpp

-            return;
-          }
+          const auto &implies_expr = to_implies_expr(expr);
+          literalt l0 = convert(implies_expr.op0());


lhs() and rhs()

Same as above -- will do a PR for a binary_infix_exprt.

src/solvers/qbf/qdimacs_core.cpp

This is follow up from #5025. A clear desire is visible to use .lhs() and .rhs() on binary expressions, say minus_exprt.

allredj

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

allredj

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

allredj

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

allredj

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

allredj

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

src/solvers/flattening/arrays.cpp

tautschnig · 2019-11-05T10:06:25Z

src/solvers/flattening/boolbv.cpp

@@ -201,7 +201,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
    if(expr.operands().size()!=1)
      return conversion_failed(expr);

-    std::size_t op_width=boolbv_width(expr.op0().type());
+    std::size_t op_width = boolbv_width(to_unary_expr(expr).op().type());


I'm not sure there's anything wrong here?

tautschnig · 2019-11-05T10:09:28Z

src/solvers/flattening/boolbv.cpp

-    DATA_INVARIANT(expr.operands().size() == 1, "isnan expects one operand");
-    const bvt &bv=convert_bv(operands[0]);
+    const auto &op = to_unary_expr(expr).op();
+    const bvt &bv = convert_bv(op);


It seems the original code had operands declared somewhere. In the code review it's hard to see where that is, but can you please make sure its declaration is removed as it shouldn't be of any use anymore?

sure, removed

src/solvers/flattening/boolbv_bitwise.cpp

tautschnig · 2019-11-05T10:12:56Z

src/solvers/flattening/boolbv_overflow.cpp

-    bv_utilst::representationt rep=
-      expr.op0().type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
-                                          bv_utilst::representationt::UNSIGNED;
+    bv_utilst::representationt rep = operands[0].type().id() == ID_signedbv


I'm not sure the use of operands[0] is an improvement?

replaced by binary_exprt

src/solvers/smt2/smt2_conv.cpp

allredj

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

This improves type safety.

allredj

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

kroening added Solvers cleanup labels Aug 15, 2019

allredj reviewed Aug 15, 2019

View reviewed changes

kroening marked this pull request as ready for review August 15, 2019 16:04

kroening requested review from chrisr-diffblue, martin-cs, peterschrammel, romainbrenguier, smowton and tautschnig as code owners August 15, 2019 16:04

smowton suggested changes Aug 15, 2019

View reviewed changes

This was referenced Aug 15, 2019

fix accesses to exprt::opX() in pointer-analysis/ #5027

Merged

fix accesses to exprt::opX() in goto-programs/ #5026

Merged

kroening force-pushed the solvers-opX branch from 56cf656 to 0b62e99 Compare August 15, 2019 21:31

allredj reviewed Aug 15, 2019

View reviewed changes

smowton approved these changes Aug 16, 2019

View reviewed changes

romainbrenguier approved these changes Aug 16, 2019

View reviewed changes

martin-cs reviewed Aug 21, 2019

View reviewed changes

kroening force-pushed the solvers-opX branch from 0b62e99 to 0d4e7b7 Compare August 21, 2019 16:09

kroening pushed a commit that referenced this pull request Aug 21, 2019

offer .lhs() and .rhs() for all binary expressions

dfb9421

This is follow up from #5025. A clear desire is visible to use .lhs() and .rhs() on binary expressions, say minus_exprt.

kroening mentioned this pull request Aug 21, 2019

offer .lhs() and .rhs() for all binary expressions #5044

Merged

3 tasks

allredj reviewed Aug 21, 2019

View reviewed changes

peterschrammel approved these changes Sep 1, 2019

View reviewed changes

peterschrammel assigned martin-cs Sep 1, 2019

kroening force-pushed the solvers-opX branch from 0d4e7b7 to 47099cd Compare September 23, 2019 09:48

allredj reviewed Sep 23, 2019

View reviewed changes

kroening force-pushed the solvers-opX branch from 47099cd to 7342799 Compare October 10, 2019 13:17

allredj reviewed Oct 10, 2019

View reviewed changes

kroening force-pushed the solvers-opX branch from 7342799 to c29fcd8 Compare October 12, 2019 08:41

allredj reviewed Oct 12, 2019

View reviewed changes

kroening assigned tautschnig and chrisr-diffblue and unassigned martin-cs Oct 20, 2019

kroening force-pushed the solvers-opX branch from c29fcd8 to 0a3c6a5 Compare October 21, 2019 00:02

allredj reviewed Oct 21, 2019

View reviewed changes

tautschnig approved these changes Nov 5, 2019

View reviewed changes

kroening requested a review from martin-cs November 5, 2019 10:21

kroening assigned martin-cs and unassigned tautschnig Nov 5, 2019

kroening force-pushed the solvers-opX branch from 0a3c6a5 to 8a6f9aa Compare November 5, 2019 14:21

allredj reviewed Nov 5, 2019

View reviewed changes

Daniel Kroening added 2 commits November 7, 2019 16:29

fix accesses to exprt::opX() in solvers/

cefce97

This improves type safety.

remove unnecessary .c_str()

dbf0058

kroening force-pushed the solvers-opX branch from 8a6f9aa to dbf0058 Compare November 7, 2019 16:29

allredj reviewed Nov 7, 2019

View reviewed changes

kroening merged commit ee79ae2 into develop Nov 7, 2019

kroening deleted the solvers-opX branch November 7, 2019 19:25

fix accesses to exprt::opX() in solvers/ #5025

fix accesses to exprt::opX() in solvers/ #5025

Uh oh!

Conversation

kroening commented Aug 15, 2019

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!

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!

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!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Aug 15, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs 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!

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!

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!

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!

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!

codecov-io commented Aug 15, 2019 •

edited

Loading