Skip to content
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

crucible_llvm_verify produces trivial proof obligations for alignment constraints #586

Closed
brianhuffman opened this issue Nov 12, 2019 · 0 comments · Fixed by GaloisInc/crucible#343
Closed

crucible_llvm_verify produces trivial proof obligations for alignment constraints #586

brianhuffman opened this issue Nov 12, 2019 · 0 comments · Fixed by GaloisInc/crucible#343

Comments

@brianhuffman
Copy link
Contributor

Here's an example of a proof goal arising from an alignment constraint:

  (Prelude.bvEq 2 (Prelude.bvNat 2 0)
    (Prelude.slice Prelude.Bool 62 2 0 (Prelude.bvMul 64 (Prelude.bvNat 64 4) x)))

Basically, it says that the 2 least-significant bits of 4 * x should be zero. This kind of goal should be simplified away during symbolic simulation, and should not show up as a saw-script proof goal.
brianhuffman pushed a commit to GaloisInc/crucible that referenced this issue Nov 13, 2019
Add special case to bvSelect for truncating a WeightedSum of bitvec…
a3fa370 
…tors.

Truncating a WeightedSum of bitvectors now truncates all the integer
coefficients in the weighted sum, removing those that reduce to 0.
This is useful for simplifying e.g. alignment constraints.

Fixes GaloisInc/saw-script#586.
@brianhuffman brianhuffman mentioned this issue Nov 13, 2019
Merged
robdockins pushed a commit to GaloisInc/what4 that referenced this issue Feb 26, 2020
Add special case to bvSelect for truncating a WeightedSum of bitvec…
2beb635 
…tors.

Truncating a WeightedSum of bitvectors now truncates all the integer
coefficients in the weighted sum, removing those that reduce to 0.
This is useful for simplifying e.g. alignment constraints.

Fixes GaloisInc/saw-script#586.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Add special case to bvSelect for truncating a WeightedSum of bitvectors GaloisInc/crucible
1 participant
@brianhuffman