Add Kani verifier backend#1
Merged
Merged
Conversation
Kani drives CBMC, so `kani --output-format old --cbmc-args --trace` emits CBMC's own output. kani_spec derives from cbmc_spec via dataclasses.replace, reusing its stack-trace/counterexample/severity parsing and overriding only detect, success, block, error_type and message. Registered before cbmc in SPECS because Kani's output also carries a `CBMC version` banner. - native-format runs (no CBMC trace) surface a hint to re-run with the old-format trace flags, mirroring cbmc's --trace hint - reachability_check properties Kani injects are dropped - KANI_CHECK_ID markers stripped from messages; error_type is the property class from the trace header (spans generic fn names with spaces) - 11 regression fixtures, 10 sourced from model-checking/kani tests/, plus unit tests for the kani-specific behaviours
Kani only produces pf-parseable output in the legacy CBMC format, so document the required -Z unstable-options --no-assertion-reach-checks --output-format old --cbmc-args --trace invocation and what each flag is for.
The old-format `VERIFICATION` line is unreliable with reachability checks on: a passing run prints `VERIFICATION FAILED` because each `reachability_check` property "fails" precisely when its assertion is reachable (normal). The earlier workaround, `--no-assertion-reach-checks`, disables detection of unreachable, vacuously-passing assertions and so weakens verification. Instead derive the verdict from the per-check statuses in CBMC's `** Results:` section (negate_success): a real failure is a non-`reachability_check` check with `: FAILURE`, or the native `VERIFICATION:- FAILED` line. This keeps reachability checks enabled while still reporting the verdict correctly. Fixtures regenerated with the checks on; a passing harness now verifies as such despite the raw `VERIFICATION FAILED`.
The property class in `Trace for <fn>.<class>.<n>:` and in the `** Results:` check lines can be uppercase (e.g. `NaN`) or hyphenated (CBMC-style `division-by-zero`), but the class charset was `[a-z_]+`. That mislabelled such an error_type as "Unknown" and — since the same charset feeds the verdict pattern (negate_success) — a run that failed only on such a check matched nothing and was silently reported as successful. Broaden the class charset to `[A-Za-z][\w-]*` in both error_type and success, with a NaN regression guard.
…ixtures CBMC's stack-trace and counterexample regexes matched the function name as a single `\S+` token, so any Rust trace whose monomorphized name contains a space (e.g. `std::slice::from_raw_parts_mut::<'_, i32>`, `<i8 as kani::Arbitrary>::any`, `kani::...::offset::<i32, *const i32, isize>`) failed to match and was silently dropped — losing violation locations and counterexample states. Broaden to `.+?` up to ` line ` (also correct for CBMC's own C++ demangled template names). Regenerated the affected fixtures, which recover the dropped data (e.g. slice_out_of_bounds counterexample 117 -> 526 states, pointer_offset_overflow safety_check location no longer empty). Also convert the kani unit tests that fed log strings and asserted on the parse into data-driven regression fixtures (add slice_from_raw, float_nan); keep only what the regression suite can't express: auto-detection and the missing-flag hint (hints are excluded from serialized output).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds Kani as a supported verifier backend.
Kani runs CBMC internally, so
kani_specderives fromcbmc_specand targetskani --output-format old --cbmc-args --trace, reusing CBMC's trace/counterexampleparsing and overriding only what differs.
** Results:statuses, so reachabilitychecks stay enabled (they catch unreachable, vacuously-passing assertions) even
though old-format Kani prints
VERIFICATION FAILEDfor a passing run.cbmcinSPECS(Kani output also carries aCBMC versionbanner) and available on the
pfCLI + auto-detection.Durability fixes found via an independent-oracle validation over real Kani programs:
uppercase/hyphenated property classes (
NaN,division-by-zero), and function namescontaining spaces (Rust generics like
std::slice::from_raw_parts_mut::<'_, i32>)that were dropping violation locations and counterexample states.
Tests: 13 regression fixtures (real logs + expected JSON, mostly sourced from
model-checking/kani
tests/); unit tests cover only what the suite can't express(auto-detection, and the missing-flag hint which is excluded from serialized output).