Skip to content

Classify bugFinding goals with the mode-aware predicates at minimal check level #1448

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

Open
repowazdogz-droid wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Classify bugFinding goals with the mode-aware predicates at minimal check level #1448

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions Strata/Languages/Core/Verifier.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1069,6 +1069,18 @@ def label (o : VCOutcome) (property : Imperative.PropertyType)
| .unsat => "pass"
| .sat _ => "fail"
| .unknown _ | .err _ => "unknown"
else if checkMode == .bugFinding then
-- `bugFinding` runs the satisfiability check only (see the check
-- selection at `verifySingleEnv`), so matching on
-- `satisfiabilityProperty` had no case that could report a
-- non-bug: every goal came out `satisfiable` or `unknown` and was
-- then counted as failed. Classify with the mode-aware predicates
-- instead. `bugFindingAssumingCompleteSpec` runs both checks and
-- keeps its existing labels, because `bugFindingSuccess` encodes
-- only the `bugFinding` column of docs/VerificationModes.md.
if o.bugFindingFailure then "fail"
else if o.bugFindingSuccess then "no definite bug"
else "unknown"
else
match o.satisfiabilityProperty with
| .sat _ => "satisfiable"
Expand Down Expand Up @@ -1105,6 +1117,11 @@ def emoji (o : VCOutcome) (property : Imperative.PropertyType)
| .unsat => "✅"
| .sat _ => "❌"
| .unknown _ | .err _ => "❓"
else if checkMode == .bugFinding then
-- See the matching comment in `label` above.
if o.bugFindingFailure then "❌"
else if o.bugFindingSuccess then "✅"
else "❓"
else
match o.satisfiabilityProperty with
| .sat _ => "❓"
Expand Down
28 changes: 28 additions & 0 deletions StrataTest/Languages/Core/VCOutcomeTests.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,6 +146,34 @@ Sat:unknown|Val:unknown ❓ unknown, Unknown (solver timeout or incomplete), SAR
#guard outcomeToLevel .bugFindingAssumingCompleteSpec .assert (mkOutcome (.sat []) .unsat) = Strata.Sarif.Level.none
#guard outcomeToLevel .bugFindingAssumingCompleteSpec .assert (mkOutcome .unknown (.sat [])) = Strata.Sarif.Level.error

/-! ### `bugFinding` at the `minimal` check level

`bugFinding` runs the satisfiability check only, so `validityProperty` is
`unknown` on every goal. Classify with `bugFindingSuccess`/`bugFindingFailure`
so a goal that is not a definite bug is not labelled a failure. -/

#guard (mkOutcome (.sat []) .unknown).label .assert .minimal .bugFinding
= "no definite bug"
#guard (mkOutcome (.sat []) .unknown).emoji .assert .minimal .bugFinding = "✅"
#guard (mkOutcome .unsat .unknown).label .assert .minimal .bugFinding = "fail"
#guard (mkOutcome .unsat .unknown).emoji .assert .minimal .bugFinding = "❌"
#guard (mkOutcome .unknown .unknown).label .assert .minimal .bugFinding
= "unknown"
#guard (mkOutcome .unknown .unknown).emoji .assert .minimal .bugFinding = "❓"

/-! ### `minimal` labels for the other two modes are unchanged

`bugFindingAssumingCompleteSpec` runs both checks and treats any
counterexample as an error, so it keeps the satisfiability-based labels. -/

#guard (mkOutcome (.sat []) (.sat [])).label .assert .minimal
.bugFindingAssumingCompleteSpec = "satisfiable"
#guard (mkOutcome .unsat (.sat [])).label .assert .minimal
.bugFindingAssumingCompleteSpec = "fail"
#guard (mkOutcome (.sat []) .unsat).label .assert .minimal .deductive = "pass"
#guard (mkOutcome (.sat []) (.sat [])).label .assert .minimal .deductive
= "fail"

/-! ### Outcome table verification -/

private def printOutcomeRow (sat val : Imperative.SMT.Result (Ident := Core.Expression.Ident)) : IO Unit := do
Expand Down
Loading