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

uc-crux-llvm: Track more sources of unsoundness #1036

Merged
merged 8 commits into from
Sep 28, 2022
Merged

uc-crux-llvm: Track more sources of unsoundness #1036

merged 8 commits into from
Sep 28, 2022

Conversation

langston-barrett
Copy link
Contributor

Fixes #932, #907. The upshot is that in situations like #907, UC-Crux will faithfully report conditions that may lead it to claim that there is a bug when, in fact, there isn't. Here's the new output for the test case in that ticket:

[Crux] Attempting to prove verification conditions.
[UC-Crux-LLVM] Results for do_getline
[UC-Crux-LLVM] Found likely bugs
[UC-Crux-LLVM] In addition to any assumptions listed above, the following sources of unsoundness may invalidate this claim that there is a bug:
[UC-Crux-LLVM] The following unsound overrides (built-in functions) were used:
[UC-Crux-LLVM]   Execution of the following functions was skipped:
[UC-Crux-LLVM]   - getline
[UC-Crux-LLVM]   The following unsound specifications were applied:
[UC-Crux-LLVM] Read from data that concretely wasn't a pointer at getline.c:8:5

@langston-barrett langston-barrett self-assigned this Sep 1, 2022
@langston-barrett langston-barrett added the uc-crux Issues specific to under-constrained crux label Sep 1, 2022
@langston-barrett langston-barrett requested review from kquick and removed request for travitch September 27, 2022 20:09
@langston-barrett
uc-crux-llvm: Track sources of unsoundness for bug-finding
99bdd1f 
Previously, only sources of unsoundness for verification were reported to the
user when making a safety claim. Now, sources of unsoundness for bug-finding
will be reported when making a claim that there is a bug.
kquick
kquick approved these changes Sep 27, 2022
View reviewed changes
Copy link
Member

@kquick kquick left a comment

Choose a reason for hiding this comment

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

Based on a general review, this looks good. I had some minor comments, and haven't attempted to run and verify this, but it looks reasonable to me.

uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs Outdated Show resolved Hide resolved
uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs Show resolved Hide resolved
uc-crux-llvm/src/UCCrux/LLVM/Run/Unsoundness.hs Outdated Show resolved Hide resolved
uc-crux-llvm/src/UCCrux/LLVM/Run/Unsoundness.hs Show resolved Hide resolved
uc-crux-llvm/src/UCCrux/LLVM/Soundness.hs Show resolved Hide resolved
@langston-barrett langston-barrett merged commit 77a8fb6 into master Sep 28, 2022
@langston-barrett langston-barrett deleted the lb/track-unsoundness branch September 28, 2022 15:47
@langston-barrett langston-barrett mentioned this pull request Sep 28, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kquick kquick kquick approved these changes

Assignees

@langston-barrett langston-barrett

Labels
uc-crux Issues specific to under-constrained crux
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

uc-crux-llvm: Track sources of unsoundness for bug-finding
2 participants
@langston-barrett @kquick