Skip to content

Add support for subtracting a constant value from a pointer in the conversion code of new SMT backend #7124

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.

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

Merged

Conversation

NlightNFotis
Copy link
Contributor

Previously we didn't support expressions of the form a - 3 where a is a pointer,
because we thought that it wouldn't be possible to get this code as input. Some regression tests however showed us that this assumption was incorrect, so now we needed to add support for this.

  • 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 Sep 12, 2022

Codecov Report

Merging #7124 (74acb22) into develop (e6fc280) will increase coverage by 0.00%.
The diff coverage is 90.90%.

❗ Current head 74acb22 differs from pull request most recent head 731ff1f. Consider uploading reports for the commit 731ff1f to get more accurate results

@@            Coverage Diff            @@
##           develop    #7124    +/-   ##
=========================================
  Coverage    77.87%   77.88%            
=========================================
  Files         1576     1576            
  Lines       181587   181765   +178     
=========================================
+ Hits        141412   141567   +155     
- Misses       40175    40198    +23     
Impacted Files Coverage Δ
src/cpp/cpp_template_type.h 52.94% <0.00%> (-11.35%) ⬇️
src/goto-instrument/dump_c.cpp 80.86% <0.00%> (ø)
src/goto-instrument/function.cpp 0.00% <0.00%> (ø)
src/ansi-c/c_typecheck_expr.cpp 74.66% <80.00%> (-2.70%) ⬇️
src/ansi-c/c_typecheck_type.cpp 77.16% <86.66%> (+0.05%) ⬆️
.../src/java_bytecode/java_bytecode_convert_class.cpp 94.18% <100.00%> (+0.01%) ⬆️
...src/java_bytecode/java_bytecode_typecheck_type.cpp 96.00% <100.00%> (ø)
jbmc/src/java_bytecode/java_object_factory.cpp 94.40% <100.00%> (+0.02%) ⬆️
jbmc/src/java_bytecode/java_pointer_casts.cpp 92.50% <100.00%> (ø)
jbmc/src/java_bytecode/java_types.cpp 95.13% <100.00%> (+0.02%) ⬆️
... and 53 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

@NlightNFotis NlightNFotis force-pushed the fix_minus_exprt_support_incr_smt2 branch from 81cf965 to 65cc794 Compare September 12, 2022 11:00
@NlightNFotis NlightNFotis marked this pull request as ready for review September 12, 2022 14:50
@NlightNFotis NlightNFotis force-pushed the fix_minus_exprt_support_incr_smt2 branch from 65cc794 to f6cc0da Compare September 12, 2022 14:58
Copy link
Contributor

@thomasspriggs thomasspriggs left a comment

Choose a reason for hiding this comment

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

Weren't we expecting this to fix regression/cbmc-primitives/r_w_ok_bug/test.desc with the new decision procedure?

smt_term_a,
smt_bit_vector_theoryt::multiply(
smt_bit_vector_theoryt::negate(smt_term_two_32bit),
smt_term_four_32bit));
Copy link
Contributor

Choose a reason for hiding this comment

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

🚫 Missing REQUIRE(constructed_term == expected_term);

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Both this & the negate below were copy-paste fails of mine while I was cleaning up/rebasing.

Fixed now - thanks for catching this.

const auto expected_term = smt_bit_vector_theoryt::subtract(
smt_term_a,
smt_bit_vector_theoryt::multiply(
smt_bit_vector_theoryt::negate(smt_term_two_32bit),
Copy link
Contributor

Choose a reason for hiding this comment

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

What is this negate doing here?

@NlightNFotis
Copy link
Contributor Author

Weren't we expecting this to fix regression/cbmc-primitives/r_w_ok_bug/test.desc with the new decision procedure?

Yeah, it has fixed it in so far as not getting an invariant violation, but we still have some divergence from the test against the SAT backend mainly because we don't support the dynamic memory primitives yet (the assertions re dead object and deallocated dynamic object fail).

This is why I don't want to enable it (the test fails).

Do you think we can handle this situation better?

@NlightNFotis NlightNFotis force-pushed the fix_minus_exprt_support_incr_smt2 branch from f6cc0da to 74acb22 Compare September 13, 2022 09:30
@NlightNFotis NlightNFotis force-pushed the fix_minus_exprt_support_incr_smt2 branch from 74acb22 to 731ff1f Compare September 13, 2022 09:33
@NlightNFotis NlightNFotis merged commit 4085b97 into diffblue:develop Sep 13, 2022
@NlightNFotis NlightNFotis deleted the fix_minus_exprt_support_incr_smt2 branch September 13, 2022 12:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants