Skip to content

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

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 3 commits into from
Mar 4, 2022
Merged

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

merged 3 commits into from
Mar 4, 2022

Conversation

NlightNFotis
Copy link
Contributor

@NlightNFotis NlightNFotis commented Feb 23, 2022 •
edited
Loading

This PR adds regression tests for the work done in #6676 .

  • 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
Copy link

codecov bot commented Feb 23, 2022 •
edited
Loading

Codecov Report

Merging #6694 (0e2d0ef) into develop (1154f13) will increase coverage by 0.22%.
The diff coverage is 87.91%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6694      +/-   ##
===========================================
+ Coverage    76.92%   77.15%   +0.22%     
===========================================
  Files         1583     1582       -1     
  Lines       183314   182628     -686     
===========================================
- Hits        141018   140900     -118     
+ Misses       42296    41728     -568
Impacted Files Coverage Δ
jbmc/src/java_bytecode/lazy_goto_model.h 100.00% <ø> (+7.40%) ⬆️
jbmc/src/jdiff/jdiff_parse_options.h 100.00% <ø> (ø)
src/cpp/cpp_typecheck_conversions.cpp 85.14% <0.00%> (+0.10%) ⬆️
src/goto-instrument/dump_c.cpp 80.49% <0.00%> (+0.28%) ⬆️
src/goto-instrument/dump_c_class.h 100.00% <ø> (ø)
src/goto-instrument/goto_program2code.cpp 68.84% <0.00%> (+0.06%) ⬆️
src/goto-programs/string_abstraction.cpp 92.45% <ø> (-0.01%) ⬇️
src/goto-programs/xml_expr.cpp 51.21% <0.00%> (ø)
src/util/expr_util.h 100.00% <ø> (ø)
src/util/pointer_predicates.cpp 93.10% <ø> (-0.45%) ⬇️
... and 54 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 412d040...0e2d0ef. Read the comment docs.

@NlightNFotis NlightNFotis force-pushed the bitwise_ops_regression_tests branch 2 times, most recently from a7b757b to 6f008ab Compare February 24, 2022 14:52
@NlightNFotis NlightNFotis marked this pull request as ready for review February 24, 2022 14:52
@NlightNFotis NlightNFotis force-pushed the bitwise_ops_regression_tests branch 3 times, most recently from b263369 to bc2f6a2 Compare February 24, 2022 15:00
thomasspriggs
thomasspriggs reviewed Feb 24, 2022
View reviewed changes
regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc Outdated
^SIGNAL=0$
--
--
The assertions in the C file for this test are designed to be satisfiable,
Copy link
Contributor

Choose a reason for hiding this comment

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

If they are satisfied then why are the regexes checking for failure? Or do you mean than we expect a sat response back from the solver, thus leading to a verification failure?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Sorry, you're right, the wording is not ideal.

When I wrote this I had in mind the terminology from logic "the expression is satisfiable", which means that there's at least one model within the structure that satisfies the expression.

I'll reword this.

Copy link
Contributor

Choose a reason for hiding this comment

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

Your current working still doesn't make sense to me. Your regexes are now looking for SUCCESS. So surely the solver will return unsat and there will be no counter examples found?

TGWDB
TGWDB reviewed Feb 25, 2022
View reviewed changes
Copy link
Contributor

@TGWDB TGWDB left a comment

Choose a reason for hiding this comment

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

Added thumbsup on some of @thomasspriggs comments. Also the more general comment that "satisfiable" is often not clear from context and can be misleading.

@NlightNFotis NlightNFotis force-pushed the bitwise_ops_regression_tests branch from bc2f6a2 to 916ba10 Compare February 25, 2022 16:59
@NlightNFotis NlightNFotis force-pushed the bitwise_ops_regression_tests branch from 916ba10 to 4b8b8b5 Compare March 1, 2022 16:48
@NlightNFotis NlightNFotis force-pushed the bitwise_ops_regression_tests branch from 4b8b8b5 to 59fd2af Compare March 3, 2022 15:21
thomasspriggs
thomasspriggs approved these changes Mar 3, 2022
View reviewed changes
regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc
\[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE
\[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
\[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS
result_unsigned=64
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ I think you should also be able to include a regex to check that second is assigned the value 128 in the trace.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Incoming.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Done.

@NlightNFotis NlightNFotis force-pushed the bitwise_ops_regression_tests branch from 59fd2af to 0e2d0ef Compare March 3, 2022 15:29
@NlightNFotis NlightNFotis merged commit dbc5d5d into diffblue:develop Mar 4, 2022
@NlightNFotis NlightNFotis deleted the bitwise_ops_regression_tests branch March 4, 2022 11:17
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

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