Conversion of bitwise `exprt`s to SMT terms in new SMT backend #6676

NlightNFotis · 2022-02-16T18:34:48Z

This PR adds support for the conversion of bitwise exprts to the various SMT terms that they correspond to.

The following operators have been implemented:

Bitwise or
Bitwise and
Bitwise not (1's complement)
Logical left shift
Logical Right shift
Arithmetic Right shift

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-02-16T19:45:30Z

Codecov Report

Merging #6676 (05e1fd6) into develop (fe903fd) will increase coverage by 0.06%.
The diff coverage is 98.83%.

@@             Coverage Diff             @@
##           develop    #6676      +/-   ##
===========================================
+ Coverage    76.82%   76.89%   +0.06%     
===========================================
  Files         1582     1582              
  Lines       182758   183170     +412     
===========================================
+ Hits        140403   140840     +437     
+ Misses       42355    42330      -25

Impacted Files	Coverage Δ
...nstrument/contracts/havoc_assigns_clause_targets.h	`100.00% <ø> (ø)`
...oto-instrument/contracts/instrument_spec_assigns.h	`94.52% <90.24%> (-5.48%)`	⬇️
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	`61.33% <97.43%> (+8.65%)`	⬆️
src/goto-instrument/contracts/contracts.cpp	`89.20% <100.00%> (-0.02%)`	⬇️
...trument/contracts/havoc_assigns_clause_targets.cpp	`97.18% <100.00%> (+1.62%)`	⬆️
...o-instrument/contracts/instrument_spec_assigns.cpp	`97.37% <100.00%> (+0.50%)`	⬆️
src/goto-programs/mm_io.cpp	`100.00% <100.00%> (ø)`
src/util/bitvector_expr.h	`94.65% <100.00%> (+1.18%)`	⬆️
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp	`100.00% <100.00%> (ø)`
src/analyses/call_graph.cpp	`72.38% <0.00%> (-0.75%)`	⬇️
... and 5 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 3410558...05e1fd6. Read the comment docs.

thomasspriggs · 2022-02-17T14:14:27Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+       bitwise_and_expr.operands().cbegin(),
+       bitwise_and_expr.operands().cend(),
+       [](exprt operand)
+       { return can_cast_type<integer_bitvector_typet>(operand.type()); }))


This would exclude C booleans which are non integer bit vectors. Is there a reason we shouldn't support using C booleans with bitwise operations?

I'm playing with this a bit and I'll get back to you on this one.

thomasspriggs · 2022-02-17T14:59:08Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+  {
+    UNIMPLEMENTED_FEATURE(
+      "Bitwise \"AND\" conversion requires that all operands have the same "
+      "sort" +


This use of UNIMPLEMENTED_FEATURE macro doesn't read well to me. The previous version would make sense in the new context. However the new text describes a condition, not an unimplemented feature. The condition in the text does not match the condition in the code either.

The std::all_of check is checking the types, not the sorts. Which is an important distinction as the exprs have types, whereas the smt terms have sorts.

The text refers to all operands having the same sort, but this condition can be reached if all the operands have the same, but unimplemented type, such as bool_typet as an arbitrarily chosen example.

My preference for resolving this comment would be that you just leave the original UNIMPLEMENTED_FEATURE macro unchanged and put your new code above it, rather than putting it in an else block, or changing its text.
This comment also applies to other sections marked with a 🐸 emoji.

I can see your point about the wording, and of course I'm happy to change it to the previous wording inside the UNIMPLEMENTED_FEATURE macro, but I see no benefit to removing the else block.

To the contrary, I have a very keen preference for the else block to stay there, because it makes the structure of the code more obvious.

Both with and without the else branch, the function handles two potential cases so far (one in which we can process the type of the input parameter, and one in which we don't). The presence of the else branch makes this fact explicit, revealing this hidden structure, compared to relying to the default behaviour of having the function fall through to an unimplemented feature macro to signify.

I'm open to changing this if there exist readability/technical issues that make the change you suggest superior to the existing structure.

thomasspriggs · 2022-02-17T15:10:08Z

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -416,3 +416,75 @@ TEST_CASE(
    REQUIRE_THROWS(convert_expr_to_smt(unary_minus_exprt{true_exprt{}}));
  }
 }
+
+SCENARIO(


Why are your new tests using SCENARIO, GIVEN, WHEN and THEN rather than TEST_CASE and SECTION like the existing tests? It seems really wordy to me rather than adding that much extra value. But that could just be a personal preference thing. It does mean that the tests for similar features are now written in a mixture of styles, which could make it more difficult to compare them.

Hi Thomas, these are BDD style tests.

I found this useful when I was approaching this given that I implemented this in a Test-Driven/Behaviour-Driven style.

In catch-2, SCENARIO, GIVEN, WHEN, etc all map to SECTION, but I find them superior in at least to ways:

The behaviour intent reads better, allowing the test to document the expected behaviour in a way that reads naturally.

The testing failures get reported in a much better way (in my opinion), allowing a developer to understand exactly what's going wrong. A test failure using these looks like this:

------------------------------------------------------------------------------- Scenario: Arithmetic Right-shift expressions are converted to SMT terms Given: An integer bitvector When: We construct an ashr_exprt and with a shift of 0 places Then: When we convert it, we should be getting an arithmetic shift-right term ------------------------------------------------------------------------------- /Users/fotiskoutoulakis/Devel/cbmc/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp:793 ............................................................................... /Users/fotiskoutoulakis/Devel/cbmc/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp:803: FAILED: REQUIRE( constructed_term == expected_term )

Compared to a normal SECTION test, which gives none of the above context information.

Now granted, part of that might contain an element of style preference, but given that the tests are relatively exhaustive (in terms of behaviour driven by them) and it's a bit late in the development cycle of this PR, I suggest we don't change the tests now.

If you are very heavily opposed to them, we could change them as part of another PR.

I am happy for the style to stay as is. I don't think the bike-shedding involved here is really worth spending time on.

With either style of test, if I see a failing test either the only piece of information I need is the general area of functionality, or I am likely need to do some interactive debugging and I can see what the test context is from the code anyway. Therefore I think the situations in which the added context will be useful are limited. Which is why I feel dubious about the benefit of the added contextual information, in exchange for the code bloat.

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

thomasspriggs · 2022-02-17T16:37:13Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(


thomasspriggs · 2022-02-17T16:39:23Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(


thomasspriggs · 2022-02-17T16:43:17Z

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

+
+    // Both of the above tests have been testing the positive case so far -
+    // where everything goes more or less how we expect. Let's see how it does
+    // with a negative case - where one of the terms is bad or otherwise


⛏️ This comment seems "chatty" rather than actually useful. This isn't part of a slide presentation 😉

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

…ile. The rationale for that is that it's going to be used by functions that need to see it defined within the translation unit, and at its current location it's invisible to some of the functions defined above that.

thomasspriggs · 2022-02-23T13:15:40Z

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -416,3 +416,75 @@ TEST_CASE(
    REQUIRE_THROWS(convert_expr_to_smt(unary_minus_exprt{true_exprt{}}));
  }
 }
+
+SCENARIO(


I am happy for the style to stay as is. I don't think the bike-shedding involved here is really worth spending time on.

With either style of test, if I see a failing test either the only piece of information I need is the general area of functionality, or I am likely need to do some interactive debugging and I can see what the test context is from the code anyway. Therefore I think the situations in which the added context will be useful are limited. Which is why I feel dubious about the benefit of the added contextual information, in exchange for the code bloat.

thomasspriggs · 2022-02-23T13:27:16Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

+/// \param expr: The expression of which the operands we evaluate for type
+///   equality.
+template <typename target_typet>
+static bool operands_are_of_same_type(const exprt &expr)


⛏️ I'd suggest removing the word same from the name of this function because it does not in fact check the operands have the same (equal) type. For example - operands_are_of_same_type<bitvector_typet>(expr), will pass if expr has operands of types bv_typet{8} and bv_typet{16} even though these 2 types are distinct. This is not a short coming of our validation because the bit vector theory operators check for matched widths. But it does mean that the current name of this function is somewhat misleading.

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

… function.

tautschnig approved these changes Feb 16, 2022

View reviewed changes

tautschnig assigned NlightNFotis Feb 16, 2022

TGWDB approved these changes Feb 17, 2022

View reviewed changes

NlightNFotis force-pushed the bitwise_ops branch 3 times, most recently from 251b047 to 48d1e7e Compare February 17, 2022 16:00

NlightNFotis marked this pull request as ready for review February 17, 2022 16:01

NlightNFotis requested review from peterschrammel, thomasspriggs, chris-ryder and kroening as code owners February 17, 2022 16:01

thomasspriggs suggested changes Feb 17, 2022

View reviewed changes

NlightNFotis force-pushed the bitwise_ops branch from 48d1e7e to 3509c42 Compare February 23, 2022 10:37

NlightNFotis added 7 commits February 23, 2022 11:11

Conversion of bitwise and expressions to SMT terms.

8b35bf7

Conversion of bitor_exprt to bvor.

f09c9f9

Conversion of bitxor_expr to bvxor SMT terms.

f6a832f

Conversion of bitnot_exprt to bvnot SMT terms.

67c2503

Conversion of left bit shift expression to bvshl.

98783da

Conversion of logical and arithmetic right shift expressions to SMT.

0652b4e

NlightNFotis mentioned this pull request Feb 23, 2022

Regression tests for Bitwise Operators Conversion in new SMT backend #6694

Merged

7 tasks

thomasspriggs approved these changes Feb 23, 2022

View reviewed changes

Refactor the std::all_of checks in several bitwise operators into a…

05e1fd6

… function.

NlightNFotis force-pushed the bitwise_ops branch from 3509c42 to 05e1fd6 Compare February 23, 2022 18:08

NlightNFotis merged commit 643037e into diffblue:develop Feb 23, 2022

NlightNFotis deleted the bitwise_ops branch February 23, 2022 21:39

Conversion of bitwise exprts to SMT terms in new SMT backend #6676

Conversion of bitwise exprts to SMT terms in new SMT backend #6676

Uh oh!

Conversation

NlightNFotis commented Feb 16, 2022

Uh oh!

codecov bot commented Feb 16, 2022 • 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!

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!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Conversion of bitwise `exprt`s to SMT terms in new SMT backend #6676

Conversion of bitwise `exprt`s to SMT terms in new SMT backend #6676

codecov bot commented Feb 16, 2022 •

edited

Loading