Skip to content

Add support for dynamic object sizes in old smt decision procedure #7768

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

thomasspriggs
Copy link
Contributor

@thomasspriggs thomasspriggs commented Jun 15, 2023

This PR adds support for dynamic object sizes in old SMT backend. This fixes #7690

  • 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 Jun 15, 2023

Codecov Report

Patch coverage: 100.00% and project coverage change: +0.21 🎉

Comparison is base (ce831a0) 77.59% compared to head (2fdec1a) 77.80%.

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7768      +/-   ##
===========================================
+ Coverage    77.59%   77.80%   +0.21%     
===========================================
  Files         1693     1693              
  Lines       193309   193308       -1     
===========================================
+ Hits        149997   150407     +410     
+ Misses       43312    42901     -411     
Impacted Files Coverage Δ
src/solvers/smt2/smt2_conv.cpp 67.37% <100.00%> (-0.01%) ⬇️

... and 86 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

thomasspriggs and others added 3 commits June 15, 2023 20:08
The old SMT backend simply ignored the sizes of dynamically sized
objects instead of actually defining the size. This allowed the solver
to just choose whichever size it liked in order to reach an outcome
of SAT, rather than applying any bounds which had been applied to the
size. Actually translating the size where the expression is non-constant
should fix various observable behaviors related to object sizes and
bounds.
This is also fixed by support for dynamic object sizes.
@thomasspriggs thomasspriggs force-pushed the tas/old_smt_dynamic_sizes branch from fa13384 to 5da3a04 Compare June 15, 2023 19:15
@thomasspriggs thomasspriggs marked this pull request as ready for review June 15, 2023 19:15
@thomasspriggs thomasspriggs merged commit b1d78e2 into diffblue:develop Jun 16, 2023
@thomasspriggs thomasspriggs deleted the tas/old_smt_dynamic_sizes branch June 16, 2023 10:50
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.

Spurious pointer check violation with smt2 backend and z3 4.12.1
3 participants