Add separate overflow expr classes #6744

thomasspriggs · 2022-03-22T16:30:21Z

This PR adds separate overflow expr classes. It is split out from #6736 so that the expr and smt changes can be reviewed separately.

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

codecov · 2022-03-22T18:15:15Z

Codecov Report

Merging #6744 (c0f179c) into develop (69eded9) will increase coverage by 0.00%.
The diff coverage is 90.37%.

@@           Coverage Diff            @@
##           develop    #6744   +/-   ##
========================================
  Coverage    76.86%   76.87%           
========================================
  Files         1589     1590    +1     
  Lines       183809   183887   +78     
========================================
+ Hits        141293   141364   +71     
- Misses       42516    42523    +7

Impacted Files	Coverage Δ
src/ansi-c/goto_check_c.cpp	`91.61% <0.00%> (ø)`
src/solvers/flattening/boolbv_overflow.cpp	`50.58% <69.69%> (+1.80%)`	⬆️
src/util/bitvector_expr.h	`96.73% <95.23%> (-0.30%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`77.06% <100.00%> (ø)`
src/ansi-c/expr2c.cpp	`66.62% <100.00%> (-0.02%)`	⬇️
src/solvers/flattening/boolbv.cpp	`80.56% <100.00%> (-0.06%)`	⬇️
src/solvers/smt2/smt2_conv.cpp	`67.48% <100.00%> (+0.02%)`	⬆️
src/util/simplify_expr.cpp	`85.72% <100.00%> (ø)`
unit/util/bitvector_expr.cpp	`100.00% <100.00%> (ø)`
src/util/pointer_predicates.h	`75.00% <0.00%> (-25.00%)`	⬇️
... and 3 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 4987df3...c0f179c. Read the comment docs.

peterschrammel · 2022-03-22T18:29:54Z

src/util/bitvector_expr.h

@@ -778,6 +794,66 @@ inline binary_overflow_exprt &to_binary_overflow_expr(exprt &expr)
  return ret;
 }

+class plus_overflow_exprt : public binary_overflow_exprt


Shouldn't these classes be used somewhere in the existing code?

I had previously taken a look and it seems we consistently take shortcuts by creating binary_overflow_exprts with a computed id.

I have now pushed additional commits which use the new classes throughout the existing code where the IDs were previously being checked.

tautschnig · 2022-03-23T09:52:23Z

src/solvers/flattening/boolbv_overflow.cpp

+  const auto plus_or_minus_conversion =
+    [&](
+      const binary_overflow_exprt &overflow_expr,
+      const std::function<literalt(
+        bv_utilst *, const bvt &, const bvt &, bv_utilst::representationt)>
+        &bv_util_overflow) {
+      const bvt &bv0 = convert_bv(overflow_expr.lhs());
+      const bvt &bv1 = convert_bv(overflow_expr.rhs());
+
+      if(bv0.size() != bv1.size())
+        return SUB::convert_rest(expr);
+
+      bv_utilst::representationt rep =
+        overflow_expr.lhs().type().id() == ID_signedbv
+          ? bv_utilst::representationt::SIGNED
+          : bv_utilst::representationt::UNSIGNED;
+
+      return bv_util_overflow(&bv_utils, bv0, bv1, rep);
+    };
+  if(
+    const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
  {
-    const auto &overflow_expr = to_binary_expr(expr);
-
-    const bvt &bv0 = convert_bv(overflow_expr.lhs());
-    const bvt &bv1 = convert_bv(overflow_expr.rhs());
-
-    if(bv0.size()!=bv1.size())
-      return SUB::convert_rest(expr);
-
-    bv_utilst::representationt rep =
-      overflow_expr.lhs().type().id() == ID_signedbv
-        ? bv_utilst::representationt::SIGNED
-        : bv_utilst::representationt::UNSIGNED;
-
-    return expr.id()==ID_overflow_minus?
-      bv_utils.overflow_sub(bv0, bv1, rep):
-      bv_utils.overflow_add(bv0, bv1, rep);
+    return plus_or_minus_conversion(*plus_overflow, &bv_utilst::overflow_add);
+  }
+  if(const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
+  {
+    return plus_or_minus_conversion(*minus, &bv_utilst::overflow_sub);


I don't think the lambda helps readability here. I'd perhaps favour two branches with almost identical code, or else a slightly larger refactor: all the branches in boolbvt::convert_overflow need to convert the operands, perhaps also need to determine signed/unsigned representation. And we might opt to be consistent in whether we support (multiply) or don't support (other cases) operands of different width. (I have no idea why we would support them.)

I agree that the more ideal refactor would be to remove more of the duplication between all of the branches here. However given that I have approvals on this PR and I have other work which is based on top of this, I am going to merge this as-is and then come back to refactoring boolbvt::convert_overflow as a follow-up PR. That way the larger refactor can be considered in isolation.

Thinking about mismatched operand widths, I think there is the potential for a simpler/smaller formula for multiplying two operands of mismatched but shorter widths instead of 2 operands of matched but larger widths due to being extended to match. Any potential benefits to this are speculation on my part and it seems like a case which may be rare in source code or even always eliminated by implicit type casts before we reach this stage.

NlightNFotis · 2022-03-23T10:39:01Z

src/util/bitvector_expr.h

@@ -707,6 +707,10 @@ class binary_overflow_exprt : public binary_predicate_exprt
  binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
    : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
  {
+    INVARIANT(


I quite like this.

I favour things being correct by construction, and subsequently, for the invariants to be set as early as possible.

thomasspriggs added 3 commits March 22, 2022 15:53

Add binary_predicate_exprt sub classes

19db9a0

Add binary_predicate_exprt sub class unit tests

0f6ae1c

Add invariant on kind used to construct binary_overflow_exprt

5d7c21c

thomasspriggs requested review from kroening, tautschnig and peterschrammel as code owners March 22, 2022 16:30

thomasspriggs mentioned this pull request Mar 22, 2022

Add conversion of overflow expressions into terms for the new incremental SMT support #6736

Merged

7 tasks

TGWDB approved these changes Mar 22, 2022

View reviewed changes

peterschrammel reviewed Mar 22, 2022

View reviewed changes

thomasspriggs added 14 commits March 22, 2022 20:08

Use mult_overflow_exprt in boolbvt::convert_overflow

ce025e1

Use shl_overflow_exprt in boolbvt::convert_overflow

defc6d4

Use plus/minus_overflow_exprt in boolbvt::convert_overflow

0d36c43

Use binary_overflow_exprt in expr2ct::convert_with_precedence

636ffa8

Use binary_overflow_exprt in boolbvt::convert_rest

d4b17bd

Use plus/minus_overflow_exprt in smt2_convt

533a902

Use mult_overflow_exprt in smt2_convt

fdc0fc8

Use minus_overflow_exprt in simplify_overflow_binary

12a4451

Use mult_overflow_exprt in simplify_overflow_binary

4e3e8b9

Use plus_overflow_exprt in simplify_overflow_binary

24c9da7

Use shl_overflow_exprt in simplify_overflow_binary

7936b57

Use binary_overflow_exprt in simplify_exprt::simplify_node

98c80dc

Add unary_minus_overflow_exprt

631aeb4

Use unary_minus_overflow_exprt

c0f179c

thomasspriggs requested review from martin-cs, NlightNFotis and chris-ryder as code owners March 22, 2022 21:18

tautschnig approved these changes Mar 23, 2022

View reviewed changes

tautschnig assigned thomasspriggs Mar 23, 2022

peterschrammel approved these changes Mar 23, 2022

View reviewed changes

NlightNFotis approved these changes Mar 23, 2022

View reviewed changes

thomasspriggs merged commit 4996426 into diffblue:develop Mar 23, 2022

thomasspriggs mentioned this pull request Mar 23, 2022

Refactor boolbvt::convert_overflow #6752

Merged

7 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add separate overflow expr classes #6744

Add separate overflow expr classes #6744

Uh oh!

thomasspriggs commented Mar 22, 2022

Uh oh!

codecov bot commented Mar 22, 2022 •

edited

Loading

Uh oh!

peterschrammel Mar 22, 2022

Uh oh!

tautschnig Mar 22, 2022

Uh oh!

thomasspriggs Mar 22, 2022

Uh oh!

tautschnig Mar 23, 2022

Uh oh!

thomasspriggs Mar 23, 2022

Uh oh!

thomasspriggs Mar 23, 2022

Uh oh!

NlightNFotis Mar 23, 2022

Uh oh!

Uh oh!

Add separate overflow expr classes #6744

Add separate overflow expr classes #6744

Uh oh!

Conversation

thomasspriggs commented Mar 22, 2022

Uh oh!

codecov bot commented Mar 22, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

peterschrammel Mar 22, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Mar 22, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Mar 22, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Mar 23, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Mar 23, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Mar 23, 2022

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Mar 23, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Mar 22, 2022 •

edited

Loading