Skip to content

Add an Array sort in the new SMT backend #6965

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Jun 27, 2022
Merged

Add an Array sort in the new SMT backend #6965

merged 1 commit into from
Jun 27, 2022

Conversation

NlightNFotis
Copy link
Contributor

Along with that, add unit tests the sort and its printing.

Co-authored-by: Fotis Koutoulakis [email protected]
Co-authored-by: Enrico Steffinlongo [email protected]

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

@NlightNFotis NlightNFotis marked this pull request as ready for review June 23, 2022 14:47
@NlightNFotis NlightNFotis force-pushed the array_declaration_conversion branch from 52e8111 to 498f3b5 Compare June 23, 2022 15:00
@codecov
Copy link

codecov bot commented Jun 23, 2022 •
edited
Loading

Codecov Report

Merging #6965 (3d485f8) into develop (4e141a5) will increase coverage by 0.03%.
The diff coverage is 77.33%.

@@             Coverage Diff             @@
##           develop    #6965      +/-   ##
===========================================
+ Coverage    77.79%   77.83%   +0.03%     
===========================================
  Files         1568     1569       +1     
  Lines       180329   180429     +100     
===========================================
+ Hits        140290   140432     +142     
+ Misses       40039    39997      -42
Impacted Files Coverage Δ
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp 87.71% <0.00%> (-0.62%) ⬇️
src/solvers/smt2_incremental/smt_sorts.def 66.66% <0.00%> (-33.34%) ⬇️
unit/solvers/smt2_incremental/smt_sorts.cpp 82.00% <76.47%> (-5.76%) ⬇️
src/solvers/smt2_incremental/smt_sorts.cpp 100.00% <100.00%> (ø)
src/solvers/smt2_incremental/smt_sorts.h 100.00% <100.00%> (ø)
...rc/solvers/smt2_incremental/smt_to_smt2_string.cpp 94.40% <100.00%> (+0.10%) ⬆️
...it/solvers/smt2_incremental/smt_to_smt2_string.cpp 100.00% <100.00%> (ø)
src/analyses/locals.h 85.71% <0.00%> (-14.29%) ⬇️
src/solvers/lowering/byte_operators.cpp 92.60% <0.00%> (-0.11%) ⬇️
src/util/config.h 57.14% <0.00%> (ø)
... and 21 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 e78eacf...3d485f8. Read the comment docs.

TGWDB
TGWDB reviewed Jun 24, 2022
View reviewed changes
unit/solvers/smt2_incremental/smt_sorts.cpp Outdated
Comment on lines 133 to 143
const smt_array_sortt array_sort{smt_bool_sortt{}, smt_bool_sortt{}};
CHECK(array_sort != bool_sort1);
CHECK(array_sort != bit_vector8);
const smt_array_sortt array_sort_bv{bit_vector16, bit_vector16};
CHECK(array_sort_bv != array_sort);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also need some equality tests, including of different argument sorts (and recursive array of array sorts)?

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp
Comment on lines +24 to +26
CHECK(
smt_to_smt2_string(smt_array_sortt{smt_bool_sortt{}, smt_bool_sortt{}}) ==
"(Array Bool Bool)");
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good to check more than one single sort here, recursive and bitvector sorts would be good to check.

@NlightNFotis NlightNFotis force-pushed the array_declaration_conversion branch from 498f3b5 to 11efae6 Compare June 24, 2022 10:56
thomasspriggs
thomasspriggs suggested changes Jun 24, 2022
View reviewed changes
unit/solvers/smt2_incremental/smt_sorts.cpp
REQUIRE_FALSE(visitor.bit_vec_visited);
REQUIRE(visitor.array_visited);

smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{32}}.accept(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 I suggest you use GENERATE or GENERATE_REF as needed to duplicate the test with differing index and element sorts. That way you don't need to duplicate the requirements for each test.

@NlightNFotis NlightNFotis force-pushed the array_declaration_conversion branch from 11efae6 to e0ace86 Compare June 24, 2022 15:58
@NlightNFotis
Copy link
Contributor Author

@thomasspriggs @TGWDB We have now addressed all of your concerns, could you please have another look at this PR?

thomasspriggs
thomasspriggs reviewed Jun 24, 2022
View reviewed changes
src/solvers/smt2_incremental/smt_sorts.cpp Outdated
@@ -70,7 +89,6 @@ void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
return visitor.visit(static_cast<const smt_##the_id##_sortt &>(sort));
#include "smt_sorts.def"
#undef SORT_ID
UNREACHABLE;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🚫 This should not be deleted as it is indeed unreachable for well-formed sorts.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh yes, sorry this was a mistake - will re-add it ASAP.

@NlightNFotis NlightNFotis force-pushed the array_declaration_conversion branch from e0ace86 to a5fc2df Compare June 24, 2022 16:05
thomasspriggs
thomasspriggs reviewed Jun 24, 2022
View reviewed changes
src/solvers/smt2_incremental/smt_sorts.h Outdated
const smt_sortt &index_sort,
const smt_sortt &element_sort);
const smt_sortt &get_index_sort() const;
const smt_sortt &get_element_sort() const;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you rename get_index_sort and get_element_sort to element_sort and element_sort respectively? This would make it more consistent with the naming conventions used for getters elsewhere such as smt_bit_vector_sortt::bit_width. This comment should have been in my initial review, but it went awol somewhere, sorry.

@NlightNFotis
Add an Array sort in the new SMT backend, along with unit tests for…
3d485f8 
… the sort and its printing.

Co-authored-by: Fotis Koutoulakis <[email protected]>
Co-authored-by: Enrico Steffinlongo <[email protected]>
@NlightNFotis NlightNFotis force-pushed the array_declaration_conversion branch from a5fc2df to 3d485f8 Compare June 27, 2022 11:11
@NlightNFotis NlightNFotis merged commit 91eac8a into diffblue:develop Jun 27, 2022
@NlightNFotis NlightNFotis deleted the array_declaration_conversion branch June 27, 2022 13:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@thomasspriggs thomasspriggs thomasspriggs approved these changes

@TGWDB TGWDB TGWDB approved these changes

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@chris-ryder chris-ryder Awaiting requested review from chris-ryder

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@NlightNFotis @thomasspriggs @TGWDB