Add bit vector extract operation support to incremental SMT2 solving #6654

thomasspriggs · 2022-02-09T20:14:36Z

This PR adds support for the bit vector extract operation to the incremental SMT2 solving code. It is separated out from other additions to the bit vector theory, due to the need to add more generalised support for indexed identifiers and the dependency in turn on the back porting of std::void_t.

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.

This resolves clang-tidy warnings in the definitions of the theories due to "initialization with static storage duration may throw an exception that cannot be caught".

tautschnig · 2022-02-09T20:22:37Z

src/util/type_traits.h

+// Author: Diffblue Ltd.
+
+/// \file
+/// Back ports of utilities available in the `<type_traits>` library for C++14
+/// or C++17 to C++11. These can be replaced with the standard library versions
+/// as and when we upgrade the version CBMC is compiled with.
+
+#ifndef CPROVER_UTIL_TYPE_TRAITS_H
+#define CPROVER_UTIL_TYPE_TRAITS_H
+
+#include <type_traits>
+
+template <bool value>
+using bool_constant = std::integral_constant<bool, value>;
+
+namespace detail // NOLINT
+{
+// Implementation detail of `void_t`.
+template <typename... typest>
+struct make_voidt
+{
+  using type = void;
+};
+} // namespace detail
+
+// Back ported from C++17 STL.
+template <typename... typest>
+using void_t = typename detail::make_voidt<typest...>::type;
+
+#endif // CPROVER_UTIL_TYPE_TRAITS_H


I'd suggest to move this to the only file actually using it and also #ifdef it with compiler versions (__cplusplus). Or, at bare minimum, make the comments sufficiently detailed to explain what exactly the code should look like once we move to C++14 (as is done in file_util.h or optional.h).

I am more than happy to add extra comments detailing how to transition to using the C++17 version in preparation for the move to that standard. However given that the back ported version will compile with either standards version, is it worth complicating things with different code for different standards, based on the version in __cplusplus?

codecov · 2022-02-09T21:34:54Z

Codecov Report

Merging #6654 (30d747b) into develop (b630cc5) will increase coverage by 0.03%.
The diff coverage is 96.65%.

❗ Current head 30d747b differs from pull request most recent head 8edd58d. Consider uploading reports for the commit 8edd58d to get more accurate results

@@             Coverage Diff             @@
##           develop    #6654      +/-   ##
===========================================
+ Coverage    76.73%   76.76%   +0.03%     
===========================================
  Files         1579     1582       +3     
  Lines       181994   182357     +363     
===========================================
+ Hits        139650   139984     +334     
- Misses       42344    42373      +29

Impacted Files	Coverage Δ
...rc/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp	`76.98% <33.33%> (ø)`
src/solvers/smt2_incremental/smt_index.cpp	`86.66% <86.66%> (ø)`
...rc/solvers/smt2_incremental/smt_to_smt2_string.cpp	`94.30% <95.83%> (+0.18%)`	⬆️
src/goto-programs/remove_vector.cpp	`97.00% <100.00%> (+0.42%)`	⬆️
...solvers/smt2_incremental/smt_bit_vector_theory.cpp	`100.00% <100.00%> (ø)`
src/solvers/smt2_incremental/smt_index.h	`100.00% <100.00%> (ø)`
src/solvers/smt2_incremental/smt_terms.cpp	`95.71% <100.00%> (+0.63%)`	⬆️
src/solvers/smt2_incremental/smt_terms.h	`100.00% <100.00%> (ø)`
...solvers/smt2_incremental/smt_bit_vector_theory.cpp	`100.00% <100.00%> (ø)`
unit/solvers/smt2_incremental/smt_index.cpp	`100.00% <100.00%> (ø)`
... 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 770d791...8edd58d. Read the comment docs.

NlightNFotis

I have performed a partial review so far, but I have a couple questions.

NlightNFotis · 2022-02-10T12:05:22Z

unit/solvers/smt2_incremental/smt_index.cpp

+TEST_CASE("Test smt_indext.pretty is accessible.", "[core][smt2_incremental]")
+{
+  const smt_indext index = smt_numeral_indext{42};
+  REQUIRE(index.pretty(0, 0) == "smt_numeral_index\n  * value: 42");


This is based on the assumption that .pretty() is always going to return text of a specific format.

I'm not sure if this assumption is always supposed to hold.

If the aim of the test is to make sure that pretty() is accessible, why not just make sure that it's not the empty string? And if you need to make sure that the value is there, make a substring search on that?

Yes, this test would need to be updated if pretty were to change the formatting returned. I'll just check for non-empty instead, to make this less brittle.

NlightNFotis · 2022-02-10T12:06:16Z

unit/solvers/smt2_incremental/smt_index.cpp

+  }
+  SECTION("Symbol")
+  {
+    REQUIRE(smt_symbol_indext{"foo"}.identifier() == "foo");


What happens if you create a smt_symbol_indext{""}?

Then the constructed instant will contain the empty string. Are you suggesting an additional invariant?

This is implemented using sfinae to detect if the supplied `functiont` has an `indices` member function or not, so that it is unneccessary to add an `indices` member function which returns the empty collections of indicies for the cases where `function` needs a simple (non indexed) identifier. `type_traits.h` is in `solvers/smt2_incremental/` because this is the only part of the codebase where it is currently used and keeping it here means the PR with this commit should need fewer code reviewer approvals.

Because adding an include in the following commit will cause clang-format to re-order the includes. Doing the reorder in advance makes it possible to review the re-ordering and the additional include separately.

NlightNFotis

Looks good overall, just a couple of questions.

src/solvers/smt2_incremental/smt_terms.cpp

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

NlightNFotis

My concerns have been adequately addressed.

Mark smt_function_application_termt::factoryt as noexcept

21a0a85

This resolves clang-tidy warnings in the definitions of the theories due to "initialization with static storage duration may throw an exception that cannot be caught".

thomasspriggs requested review from chris-ryder, kroening, NlightNFotis, peterschrammel, tautschnig and TGWDB as code owners February 9, 2022 20:14

tautschnig reviewed Feb 9, 2022

View reviewed changes

NlightNFotis reviewed Feb 10, 2022

View reviewed changes

thomasspriggs added 2 commits February 10, 2022 14:21

Add indexed identifier support to smt_identifier_termt

d1c5bf7

Implement printing for indexed identifiers

d90f98c

thomasspriggs force-pushed the tas/smt_bv_extract branch from de618c0 to 6edaf35 Compare February 10, 2022 14:22

thomasspriggs added 5 commits February 10, 2022 18:23

Add SMT bit vector theory extract function

b4862bd

Reorder includes in smt_to_smt2_string unit test

f520e9e

Because adding an include in the following commit will cause clang-format to re-order the includes. Doing the reorder in advance makes it possible to review the re-ordering and the additional include separately.

Test printing of bit vector extract

aac7993

Disallow construction of smt_symbol_indext with empty string

8edd58d

thomasspriggs force-pushed the tas/smt_bv_extract branch from 30d747b to 8edd58d Compare February 10, 2022 18:26

NlightNFotis reviewed Feb 11, 2022

View reviewed changes

src/solvers/smt2_incremental/smt_terms.cpp Show resolved Hide resolved

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp Show resolved Hide resolved

NlightNFotis approved these changes Feb 11, 2022

View reviewed changes

thomasspriggs merged commit e831f43 into diffblue:develop Feb 11, 2022

thomasspriggs deleted the tas/smt_bv_extract branch February 11, 2022 15:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add bit vector extract operation support to incremental SMT2 solving #6654

Add bit vector extract operation support to incremental SMT2 solving #6654

Uh oh!

thomasspriggs commented Feb 9, 2022

Uh oh!

tautschnig Feb 9, 2022

Uh oh!

thomasspriggs Feb 10, 2022 •

edited

Loading

Uh oh!

codecov bot commented Feb 9, 2022 •

edited

Loading

Uh oh!

NlightNFotis left a comment

Uh oh!

NlightNFotis Feb 10, 2022

Uh oh!

thomasspriggs Feb 10, 2022

Uh oh!

NlightNFotis Feb 10, 2022

Uh oh!

thomasspriggs Feb 10, 2022

Uh oh!

NlightNFotis left a comment

Uh oh!

Uh oh!

Uh oh!

NlightNFotis left a comment

Uh oh!

Uh oh!

Add bit vector extract operation support to incremental SMT2 solving #6654

Add bit vector extract operation support to incremental SMT2 solving #6654

Uh oh!

Conversation

thomasspriggs commented Feb 9, 2022

Uh oh!

tautschnig Feb 9, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Feb 10, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Feb 10, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Feb 10, 2022

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Feb 10, 2022

Choose a reason for hiding this comment

Uh oh!

thomasspriggs Feb 10, 2022

Choose a reason for hiding this comment

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thomasspriggs Feb 10, 2022 •

edited

Loading

codecov bot commented Feb 9, 2022 •

edited

Loading