New SMT2 backend: arithmetic operators implementation for fixed size bit vectors #6614

NlightNFotis · 2022-01-27T10:26:06Z

This adds implementations (and tests) for the binary arithmetic operators (and their conversion) to SMT2 data structures.

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-01-27T11:45:26Z

Codecov Report

Merging #6614 (b11a3b2) into develop (a638644) will increase coverage by 0.07%.
The diff coverage is 97.08%.

@@             Coverage Diff             @@
##           develop    #6614      +/-   ##
===========================================
+ Coverage    76.65%   76.72%   +0.07%     
===========================================
  Files         1580     1579       -1     
  Lines       181560   181935     +375     
===========================================
+ Hits        139168   139584     +416     
+ Misses       42392    42351      -41

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-programs/restrict_function_pointers.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/utils.cpp	`85.59% <80.55%> (ø)`
src/goto-programs/restrict_function_pointers.cpp	`80.27% <89.58%> (ø)`
...trument/contracts/havoc_assigns_clause_targets.cpp	`95.55% <93.33%> (ø)`
...o-instrument/contracts/instrument_spec_assigns.cpp	`95.35% <95.35%> (ø)`
src/ansi-c/c_typecheck_code.cpp	`79.92% <100.00%> (ø)`
src/goto-instrument/contracts/contracts.cpp	`90.75% <100.00%> (ø)`
...nstrument/contracts/havoc_assigns_clause_targets.h	`100.00% <100.00%> (ø)`
...oto-instrument/contracts/instrument_spec_assigns.h	`100.00% <100.00%> (ø)`
... and 22 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 3c0d865...b11a3b2. Read the comment docs.

TGWDB

Looks good. It would be nice to have unit tests of the validation of bitvector width being the same for the binary operations to ensure this is properly caught.

thomasspriggs

This an initial review of the first two commits titled - "Change order of casting and dispatching of binary_relation_exprt in convert_expr_to_smt" and "Add implementation of arithmetic operator bvadd." only, so that I can leave some initial comments. My review of the remaining commits is still to follow.

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

thomasspriggs · 2022-01-28T12:19:29Z

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+  }


⛏️ We should test that calling smt_bit_vector_theoryt::add with bit_vectors of mismatched width or on bool sorted terms fails an invariant.

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

thomasspriggs · 2022-01-28T12:37:11Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -325,8 +325,12 @@ convert_expr_to_smt(const binary_relation_exprt &binary_relation)

 static smt_termt convert_expr_to_smt(const plus_exprt &plus)
 {
-  UNIMPLEMENTED_FEATURE(


⛏️ I would prefer it if commits could be titled such that the title encompasses the entirety of what they change. The fact that you effectively have "Also add conversion of plus_exprt to smt_bit_vector_theoryt::addition" in the message body is kind of a red flag which suggests that you have combined unrelated changes together (even if one change depends of the other).

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

src/solvers/smt2_incremental/smt_bit_vector_theory.h

thomasspriggs · 2022-01-28T15:27:45Z

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);


⛏️ Tests for invariant violation on constructing with an lhs and rhs of mismatched widths and terms of bool sort please.

src/solvers/smt2_incremental/smt_bit_vector_theory.h

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

thomasspriggs · 2022-01-31T14:03:47Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -352,9 +360,11 @@ static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation)

 static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for truncation modulo expression: " +
-    truncation_modulo.pretty());


⛏️ We expect this operator to be applied only to (signed/unsigned) integer bit vectors. It might be good to document this expectation using a UNEXPECTEDCASE macro, similar to how smt2_convt::convert_mod does this.

src/solvers/smt2_incremental/smt_bit_vector_theory.h

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

thomasspriggs

I am now approving as all of my 🚫 comments have been addressed.

thomasspriggs · 2022-02-02T17:51:55Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -366,10 +366,22 @@ static smt_termt convert_expr_to_smt(const div_exprt &divide)
    can_cast_type<integer_bitvector_typet>(divide.lhs().type()) &&
    can_cast_type<integer_bitvector_typet>(divide.rhs().type());

+  bool both_operands_unsigned =


⛏️ const - Every variable which is not mutated should be declared const. I have picked this as an arbitrary example, but I think it is missing in a few places.

thomasspriggs · 2022-02-02T17:53:42Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+    else
+    {
+      return smt_bit_vector_theoryt::signed_divide(
+        convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));


💡 I suggest introducing lhs_term and rhs_term variables above this if statement, so that the calls to convert_expr_to_smt are not duplicated in the two branches.

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

thomasspriggs · 2022-02-02T18:11:31Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+    {
+      return smt_bit_vector_theoryt::signed_remainder(
+        convert_expr_to_smt(truncation_modulo.lhs()),
+        convert_expr_to_smt(truncation_modulo.rhs()));


💡 Factor out the common convert_expr_to_smt sub-expressions, like I suggested with your implementation for the divide operations.

Also add tests for the data structure itself and the conversion of `plus_exprt` to `smt_bit_vector_theoryt::addition`.

Also add tests for it, both the conversion of `minus_exprt` to it, and the node factory constructing the nodes appropriately.

Also add tests for its conversion from `mult_exprt` and of the factory integrity.

Along with tests of its conversion and the function application factory integrity.

In addition, modify the tests and the implementation of the conversion function to account for signed/unsigned input.

Along with tests of its conversion and the function application factory integrity.

Along with this, change the tests and implementation of the conversion function to account for signed/unsigned inputs.

Along with conversion tests and tests of the factory method integrity.

…tor_operator_arguments`. This allows the name to reflect the more general purpose deployment of this function.

NlightNFotis requested a review from thomasspriggs January 27, 2022 10:26

NlightNFotis self-assigned this Jan 27, 2022

NlightNFotis force-pushed the newsmt_additional_operators branch 6 times, most recently from 1b243b5 to 544f963 Compare January 28, 2022 10:07

NlightNFotis marked this pull request as ready for review January 28, 2022 10:09

NlightNFotis requested review from chrisr-diffblue, peterschrammel and TGWDB as code owners January 28, 2022 10:09

TGWDB approved these changes Jan 28, 2022

View reviewed changes

NlightNFotis mentioned this pull request Jan 28, 2022

[Refactor] New SMT backend: Remove X-macro implementation from smt_bit_vector_theory #6615

Merged

7 tasks

thomasspriggs suggested changes Jan 28, 2022

View reviewed changes

thomasspriggs suggested changes Jan 31, 2022

View reviewed changes

NlightNFotis force-pushed the newsmt_additional_operators branch from 544f963 to 9bbae2c Compare February 1, 2022 16:01

NlightNFotis requested a review from chris-ryder as a code owner February 1, 2022 16:01

NlightNFotis force-pushed the newsmt_additional_operators branch from 9bbae2c to 4582586 Compare February 1, 2022 16:11

thomasspriggs reviewed Feb 1, 2022

View reviewed changes

src/solvers/smt2_incremental/convert_expr_to_smt.cpp Outdated Show resolved Hide resolved

src/solvers/smt2_incremental/convert_expr_to_smt.cpp Outdated Show resolved Hide resolved

NlightNFotis force-pushed the newsmt_additional_operators branch 2 times, most recently from a31b70a to 4482566 Compare February 2, 2022 15:56

NlightNFotis requested review from kroening and tautschnig as code owners February 2, 2022 15:56

NlightNFotis force-pushed the newsmt_additional_operators branch from 4482566 to bdbb900 Compare February 2, 2022 16:00

thomasspriggs approved these changes Feb 2, 2022

View reviewed changes

NlightNFotis force-pushed the newsmt_additional_operators branch from bdbb900 to 8a75cd7 Compare February 3, 2022 11:41

Add implementation of arithmetic operator bvadd.

426aebb

Also add tests for the data structure itself and the conversion of `plus_exprt` to `smt_bit_vector_theoryt::addition`.

NlightNFotis force-pushed the newsmt_additional_operators branch from 8a75cd7 to 407f30c Compare February 3, 2022 11:56

NlightNFotis added 8 commits February 3, 2022 11:59

Add implementation of arithmetic operator bvsub.

7488488

Also add tests for it, both the conversion of `minus_exprt` to it, and the node factory constructing the nodes appropriately.

Add implementation of multiplication operator bvmul.

5538759

Also add tests for its conversion from `mult_exprt` and of the factory integrity.

Add implementation of (unsigned) division operator bvudiv.

149f7e4

Along with tests of its conversion and the function application factory integrity.

Add implementation of (signed) division operator (bvsdiv).

0c4a39b

In addition, modify the tests and the implementation of the conversion function to account for signed/unsigned input.

Add (unsigned) remainder (modulus) arithmetic operator bvurem.

f259dc0

Along with tests of its conversion and the function application factory integrity.

Add implementation of signed remainder operator (bvsrem).

a1c923c

Along with this, change the tests and implementation of the conversion function to account for signed/unsigned inputs.

Add implementation of negation (unary minus - bvneg) operator.

10a2a53

Along with conversion tests and tests of the factory method integrity.

Rename validate_bit_vector_predicate_arguments to `validate_bit_vec…

b11a3b2

…tor_operator_arguments`. This allows the name to reflect the more general purpose deployment of this function.

NlightNFotis force-pushed the newsmt_additional_operators branch from 407f30c to b11a3b2 Compare February 3, 2022 12:00

NlightNFotis merged commit 1f3801c into diffblue:develop Feb 3, 2022

NlightNFotis deleted the newsmt_additional_operators branch February 3, 2022 13:59

NlightNFotis mentioned this pull request Feb 8, 2022

Regression tests for the SMT bitvector arithmetic operator conversion #6648

Merged

7 tasks

New SMT2 backend: arithmetic operators implementation for fixed size bit vectors #6614

New SMT2 backend: arithmetic operators implementation for fixed size bit vectors #6614

Uh oh!

Conversation

NlightNFotis commented Jan 27, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

TGWDB left a comment

Choose a reason for hiding this comment

Uh oh!

thomasspriggs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thomasspriggs Jan 28, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

thomasspriggs Jan 28, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thomasspriggs Jan 28, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thomasspriggs Jan 31, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thomasspriggs left a comment

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Feb 2, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Feb 2, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thomasspriggs Feb 2, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

NlightNFotis commented Jan 27, 2022 •

edited

Loading

codecov bot commented Jan 27, 2022 •

edited

Loading