483 lines
18 KiB
Rust
483 lines
18 KiB
Rust
//! `flowrsc prove` on real exports, with a stand-in `cargo` that plays Kani: it answers
|
|
//! `cargo kani --version` and `cargo fetch --locked`, and for `cargo kani` writes Kani's JSON
|
|
//! export for the harness it is asked for, as told (proved, a cover not reached, a check
|
|
//! failed), then holds on, sleeps or allocates as told. So the runner's whole path is run here
|
|
//! (the record, the budget, the contract) without Kani; the real Kani runs it on the build host
|
|
//! (`flowrsc prove` on an export, and `tools/kani-programs.sh` on the corpus).
|
|
#![cfg(unix)]
|
|
|
|
use std::os::unix::fs::PermissionsExt;
|
|
use std::path::{Path, PathBuf};
|
|
|
|
use flowrs_appshell::export::{self, FirmwareOptions};
|
|
use flowrs_appshell::form::{self, Status};
|
|
use flowrs_cli::prove::{self, Options, Stopped, judge, verdict};
|
|
use flowrs_connect::ScaffoldFile;
|
|
use flowrs_core::codegen::mcu::McuTarget;
|
|
use flowrs_core::codegen::proof::{KANI_INSTALL, KANI_PIN, Record};
|
|
|
|
const FAKE: &str = r#"#!/bin/bash
|
|
# A stand-in for cargo that plays Kani; its instructions are files beside it.
|
|
D="$(cd "$(dirname "$0")" && pwd)"
|
|
if [ "$1 ${2:-}" = "kani --version" ]; then
|
|
[ -f "$D/no-kani" ] && { echo "error: no such command: kani" >&2; exit 101; }
|
|
echo "Kani Rust Verifier $(cat "$D/version" 2>/dev/null || echo 0.68.0) (cargo plugin)"
|
|
exit 0
|
|
fi
|
|
if [ "$1 ${2:-}" = "fetch --locked" ]; then exit 0; fi
|
|
[ "$1" = kani ] || exit 1
|
|
echo "$@" > "$D/invoked"
|
|
pwd > "$D/cwd"
|
|
h=""; j=""; prev=""
|
|
for a in "$@"; do
|
|
[ "$prev" = "--harness" ] && h="$a"
|
|
[ "$prev" = "--export-json" ] && j="$a"
|
|
prev="$a"
|
|
done
|
|
result=$(cat "$D/result" 2>/dev/null || echo proved)
|
|
first=Success; second=Satisfied; status=Success
|
|
[ "$result" = failed ] && { first=Failure; status=Failure; }
|
|
[ "$result" = uncovered ] && second=Unsatisfiable
|
|
cat > "$j" <<EOF
|
|
{"tools": {"kani": "0.68.0", "cbmc": "6.11.0 (stand-in)", "rustc": "rustc (stand-in)"},
|
|
"error_details": [{"harness_id": "$h", "has_errors": false}],
|
|
"verification_results": {"summary": {}, "results": [{"harness_id": "$h", "status": "$status", "duration_ms": 1234,
|
|
"checks": [
|
|
{"status": "$first", "description": "attempt to add with overflow", "category": "arithmetic_overflow"},
|
|
{"status": "Success", "description": "index out of bounds: the length is less than or equal to the given index", "category": "assertion"},
|
|
{"status": "Unreachable", "description": "unreachable code", "category": "unreachable"},
|
|
{"status": "Satisfied", "description": "a pass runs to its end", "category": "cover"},
|
|
{"status": "$second", "description": "a pass fails, into the safe state", "category": "cover"}
|
|
]}]}}
|
|
EOF
|
|
[ -f "$D/sleep" ] && sleep "$(cat "$D/sleep")"
|
|
[ -f "$D/alloc" ] && perl -e '$x = "a" x (300 * 1024 * 1024); sleep 30'
|
|
exit 0
|
|
"#;
|
|
|
|
/// A firmware graph flowRS's proof table does not hold (the e2e fixture with one more output),
|
|
/// so its export ships its harness not run.
|
|
fn not_in_the_table() -> String {
|
|
let root = Path::new(env!("CARGO_MANIFEST_DIR")).join("../..");
|
|
let mcu_io = std::fs::read_to_string(root.join("e2e/fixtures/firmware/mcu_io.fdsl")).unwrap();
|
|
format!("{mcu_io}let n9 = embedded.gpio.digital_out {{ pin: 12 }};\n")
|
|
}
|
|
|
|
struct Bench {
|
|
_tmp: tempfile::TempDir,
|
|
dir: PathBuf,
|
|
fake: PathBuf,
|
|
}
|
|
|
|
impl Bench {
|
|
fn new(target: McuTarget) -> Bench {
|
|
let tmp = tempfile::tempdir().unwrap();
|
|
let dir = tmp.path().join("export");
|
|
let done = export::firmware_document(
|
|
¬_in_the_table(),
|
|
Some("other.fdsl"),
|
|
&FirmwareOptions {
|
|
name: None,
|
|
board: "nucleo_f401re".into(),
|
|
target,
|
|
},
|
|
None,
|
|
)
|
|
.unwrap();
|
|
export::write(&done.scaffold, &dir).unwrap();
|
|
let fake_dir = tmp.path().join("fake");
|
|
std::fs::create_dir_all(&fake_dir).unwrap();
|
|
let fake = fake_dir.join("cargo");
|
|
std::fs::write(&fake, FAKE).unwrap();
|
|
std::fs::set_permissions(&fake, std::fs::Permissions::from_mode(0o755)).unwrap();
|
|
Bench {
|
|
_tmp: tmp,
|
|
dir,
|
|
fake,
|
|
}
|
|
}
|
|
|
|
fn tell(&self, file: &str, what: &str) {
|
|
std::fs::write(self.fake.parent().unwrap().join(file), what).unwrap();
|
|
}
|
|
|
|
fn invoked(&self) -> bool {
|
|
self.fake.parent().unwrap().join("invoked").exists()
|
|
}
|
|
|
|
fn opts(&self) -> Options {
|
|
let mut o = Options::new(
|
|
&self.dir,
|
|
prove::DEFAULT_MEM_GB,
|
|
prove::DEFAULT_TIMEOUT_S,
|
|
None,
|
|
);
|
|
o.cargo.clone_from(&self.fake);
|
|
o
|
|
}
|
|
|
|
fn run(&self, o: &Options) -> (i32, String, String) {
|
|
let (mut out, mut err) = (Vec::new(), Vec::new());
|
|
let code = prove::prove(o, &mut out, &mut err);
|
|
(
|
|
code,
|
|
String::from_utf8(out).unwrap(),
|
|
String::from_utf8(err).unwrap(),
|
|
)
|
|
}
|
|
|
|
fn read(&self, rel: &str) -> String {
|
|
std::fs::read_to_string(self.dir.join(rel)).unwrap()
|
|
}
|
|
|
|
fn record(&self) -> Record {
|
|
Record::parse(&self.read("proof/proofs.json")).unwrap()
|
|
}
|
|
|
|
/// The export's files row 13 is computed from, as they are now.
|
|
fn files(&self) -> Vec<ScaffoldFile> {
|
|
[
|
|
form::FILE,
|
|
"src/main.rs",
|
|
form::PROOF_RECORD,
|
|
form::PROOF_HARNESS,
|
|
]
|
|
.into_iter()
|
|
.map(|p| ScaffoldFile {
|
|
path: p.into(),
|
|
contents: self.read(p),
|
|
})
|
|
.collect()
|
|
}
|
|
|
|
fn row(&self) -> form::Property {
|
|
form::validate_export(&self.files())
|
|
.unwrap_or_else(|e| panic!("{e:?}"))
|
|
.property("no_panic_proof")
|
|
.unwrap()
|
|
.clone()
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn an_export_of_another_program_ships_its_harness_not_run() {
|
|
let b = Bench::new(McuTarget::Rtic);
|
|
let r = b.record();
|
|
assert_eq!(r.harnesses[0].status, "not_run");
|
|
assert!(r.kani.is_none() && r.run.is_none());
|
|
let row = b.row();
|
|
assert_eq!(row.status, Status::NotYet);
|
|
assert!(row.reason.contains("flowrsc prove"), "{}", row.reason);
|
|
// The README says how to prove it, with the runner's own budget and the pinned Kani.
|
|
let readme = b.read("README.md");
|
|
assert!(readme.contains("## Prove it"), "{readme}");
|
|
assert!(readme.contains("flowrsc prove ."));
|
|
assert!(readme.contains(KANI_INSTALL));
|
|
assert!(readme.contains(&format!(
|
|
"{} GB and {} s by default",
|
|
prove::DEFAULT_MEM_GB,
|
|
prove::DEFAULT_TIMEOUT_S
|
|
)));
|
|
for a in &r.assumptions {
|
|
assert!(readme.contains(&a[..20]), "{a}");
|
|
}
|
|
// The harness is a member of the project's workspace, on the vendored flowrs-hal, which
|
|
// carries the modules a build under Kani compiles (its own proofs), or it would not build.
|
|
assert!(b.read("Cargo.toml").contains("members = [\"proof\"]"));
|
|
assert!(
|
|
b.read("proof/Cargo.toml")
|
|
.contains("path = \"../vendor/flowrs-hal\"")
|
|
);
|
|
for f in [
|
|
"vendor/flowrs-hal/src/rt/proofs.rs",
|
|
"vendor/flowrs-hal/src/can/proofs.rs",
|
|
] {
|
|
assert!(b.dir.join(f).exists(), "no {f}");
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn a_run_that_proves_this_program_makes_its_row_live() {
|
|
for target in McuTarget::ALL {
|
|
let b = Bench::new(target);
|
|
let readme_before = b.read("README.md");
|
|
let (code, out, err) = b.run(&b.opts());
|
|
assert_eq!(code, 0, "{out}\n{err}");
|
|
let r = b.record();
|
|
let h = &r.harnesses[0];
|
|
assert_eq!(h.status, "proved");
|
|
assert_eq!(h.covers.unwrap().satisfied, 2);
|
|
assert_eq!(h.checks.unwrap().unreachable, 1);
|
|
assert_eq!(r.kani.as_ref().unwrap().version.as_deref(), Some(KANI_PIN));
|
|
let run = r.run.as_ref().unwrap();
|
|
assert_eq!(run["by"], "flowrsc prove");
|
|
assert_eq!(h.budget.unwrap().mem_gb, Some(prove::DEFAULT_MEM_GB));
|
|
// Kani ran in proof/, on exactly the harness the record names, within its limit.
|
|
let invoked = std::fs::read_to_string(b.fake.parent().unwrap().join("invoked")).unwrap();
|
|
assert!(invoked.contains(&format!("--harness {} --exact", h.name.as_deref().unwrap())));
|
|
assert!(invoked.contains("-Z restrict-vtable"), "{invoked}");
|
|
// The corpus's arguments, every one: codegen::proof::KANI_ARGS.
|
|
assert!(
|
|
invoked.contains(&flowrs_core::codegen::proof::KANI_ARGS.join(" ")),
|
|
"{invoked}"
|
|
);
|
|
assert!(invoked.contains("--no-overflow-checks"), "{invoked}");
|
|
// Kani runs in proof/: the JSON's path it is handed is absolute, so it lands where
|
|
// prove reads it whatever directory prove was given.
|
|
assert!(invoked.contains("--export-json /"), "{invoked}");
|
|
assert!(invoked.contains(&format!("--harness-timeout {}s", prove::DEFAULT_TIMEOUT_S)));
|
|
let cwd = std::fs::read_to_string(b.fake.parent().unwrap().join("cwd")).unwrap();
|
|
assert!(cwd.trim_end().ends_with("export/proof"), "{cwd}");
|
|
// Row 13 is live, the contract holds to the files, the README's section follows it.
|
|
let row = b.row();
|
|
assert_eq!(row.status, Status::Live, "{}", row.reason);
|
|
assert!(
|
|
row.reason.contains("Run by flowrsc prove"),
|
|
"{}",
|
|
row.reason
|
|
);
|
|
let c = form::validate(&b.read(form::FILE)).unwrap();
|
|
let readme = b.read("README.md");
|
|
assert_ne!(readme, readme_before);
|
|
assert!(readme.contains(&form::readme_section(&c)));
|
|
// It says what it proved and what it assumes.
|
|
assert!(out.contains("result: proved"), "{out}");
|
|
for a in &r.assumptions {
|
|
assert!(out.contains(a.as_str()), "{a}");
|
|
}
|
|
assert!(out.contains("FORM.json row 13 (no panic): live"), "{out}");
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn a_run_past_its_wall_clock_is_never_proved() {
|
|
let b = Bench::new(McuTarget::Rtic);
|
|
// Kani wrote "proved", then the run went on past its wall clock.
|
|
b.tell("sleep", "30");
|
|
let mut o = b.opts();
|
|
o.wall_s = 2;
|
|
let start = std::time::Instant::now();
|
|
let (code, out, err) = b.run(&o);
|
|
assert!(start.elapsed().as_secs() < 20, "the run was not stopped");
|
|
assert_eq!(code, 1, "{out}\n{err}");
|
|
let h = &b.record().harnesses[0];
|
|
assert_eq!(h.status, "budget_exceeded");
|
|
assert!(h.reason.as_deref().unwrap().contains("wall clock"), "{h:?}");
|
|
let row = b.row();
|
|
assert_eq!(row.status, Status::NotYet);
|
|
assert!(row.reason.contains("budget"), "{}", row.reason);
|
|
}
|
|
|
|
#[test]
|
|
fn a_run_past_its_memory_is_never_proved() {
|
|
let b = Bench::new(McuTarget::Embassy);
|
|
b.tell("alloc", "");
|
|
let mut o = b.opts();
|
|
o.total_kib = 50 * 1024;
|
|
let (code, out, err) = b.run(&o);
|
|
assert_eq!(code, 1, "{out}\n{err}");
|
|
let h = &b.record().harnesses[0];
|
|
assert_eq!(h.status, "budget_exceeded", "{h:?}");
|
|
assert!(h.reason.as_deref().unwrap().starts_with("memory"), "{h:?}");
|
|
assert_eq!(b.row().status, Status::NotYet);
|
|
}
|
|
|
|
#[test]
|
|
fn an_unreached_cover_or_a_counterexample_is_not_a_proof() {
|
|
for (result, status, why) in [
|
|
("uncovered", "not_proved", "vacuous"),
|
|
("failed", "failed", "attempt to add with overflow"),
|
|
] {
|
|
let b = Bench::new(McuTarget::Rtic);
|
|
b.tell("result", result);
|
|
let (code, out, err) = b.run(&b.opts());
|
|
assert_eq!(code, 1, "{out}\n{err}");
|
|
let h = &b.record().harnesses[0];
|
|
assert_eq!(h.status, status);
|
|
assert!(h.reason.as_deref().unwrap().contains(why), "{h:?}");
|
|
assert_eq!(b.row().status, Status::NotYet, "{result}");
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn without_the_pinned_kani_it_says_how_to_install_it_and_runs_nothing() {
|
|
for (tell, says) in [("no-kani", "not installed"), ("version", "Kani 0.67.0")] {
|
|
let b = Bench::new(McuTarget::Rtic);
|
|
b.tell(tell, "0.67.0");
|
|
let before = b.read("proof/proofs.json");
|
|
let (code, _, err) = b.run(&b.opts());
|
|
assert_eq!(code, 2, "{err}");
|
|
assert!(err.contains(says), "{err}");
|
|
assert!(err.contains(KANI_INSTALL), "{err}");
|
|
assert!(!b.invoked());
|
|
assert_eq!(b.read("proof/proofs.json"), before);
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn a_harness_that_is_not_the_records_is_refused_before_anything_runs() {
|
|
let b = Bench::new(McuTarget::Rtic);
|
|
let lib = b
|
|
.read("proof/src/lib.rs")
|
|
.replace("kani::cover!(r.is_err()", "let _ = (r.is_err()");
|
|
std::fs::write(b.dir.join("proof/src/lib.rs"), lib).unwrap();
|
|
let (code, _, err) = b.run(&b.opts());
|
|
assert_eq!(code, 1, "{err}");
|
|
assert!(err.contains("not the harness the record names"), "{err}");
|
|
assert!(!b.invoked());
|
|
}
|
|
|
|
/// A program that speaks a typed link: its loops are bounded by elapsed time, so no harness can
|
|
/// prove it; `prove` says why and runs nothing, and its row says the same.
|
|
#[test]
|
|
fn a_program_no_harness_can_prove_says_why_and_is_never_run() {
|
|
use flowrs_core::codegen::link::{LinkChannel, LinkEnd, LinkPlan, WireTy};
|
|
use flowrs_core::codegen::mcu::{Options as Lower, lower_with};
|
|
use flowrs_core::codegen::proof::{ProgramMeta, program_proof};
|
|
let b = Bench::new(McuTarget::Rtic);
|
|
let mut g = flowrs_core::graph::ir::Graph::new();
|
|
let adc = g.add_node("embedded.adc", 0.0, 0.0);
|
|
let plan = LinkPlan {
|
|
uart: 0,
|
|
baud: 1_000_000,
|
|
timeout_ms: 10_000,
|
|
cdc: false,
|
|
order: None,
|
|
channels: vec![LinkChannel {
|
|
id: 1,
|
|
name: "raw".into(),
|
|
ty: WireTy::U16,
|
|
end: LinkEnd::Send {
|
|
node: adc,
|
|
port: "raw".into(),
|
|
},
|
|
iface: None,
|
|
fragments: 1,
|
|
stamped: false,
|
|
}],
|
|
};
|
|
let l = lower_with(
|
|
&g,
|
|
McuTarget::Rtic,
|
|
&Lower {
|
|
probes: false,
|
|
board: None,
|
|
link: Some(&plan),
|
|
},
|
|
)
|
|
.unwrap();
|
|
let p = program_proof(
|
|
&l,
|
|
McuTarget::Rtic,
|
|
&ProgramMeta {
|
|
board: "nucleo_f401re".into(),
|
|
chip: "stm32f401re".into(),
|
|
family: "STM32F4".into(),
|
|
graph: None,
|
|
},
|
|
);
|
|
assert!(p.harness.is_none());
|
|
std::fs::write(b.dir.join("proof/proofs.json"), &p.manifest).unwrap();
|
|
// The export's contract, recomputed for that record, as an exporter of it would write it.
|
|
let mut c = form::validate(&b.read(form::FILE)).unwrap();
|
|
form::reassess_no_panic(&mut c, &b.files());
|
|
std::fs::write(b.dir.join(form::FILE), c.to_json()).unwrap();
|
|
let row = b.row();
|
|
assert_eq!(row.status, Status::NotYet);
|
|
assert!(
|
|
row.reason.contains("no harness can prove"),
|
|
"{}",
|
|
row.reason
|
|
);
|
|
let (code, out, err) = b.run(&b.opts());
|
|
assert_eq!(code, 1, "{out}\n{err}");
|
|
assert!(out.contains("cannot be proved"), "{out}");
|
|
assert!(out.contains("clock"), "{out}");
|
|
assert!(!out.contains("result: proved"));
|
|
assert!(!b.invoked());
|
|
}
|
|
|
|
#[test]
|
|
fn the_watcher_stops_a_solver_or_a_run_past_its_cap() {
|
|
// pid ppid rss(KiB) command
|
|
let ps = "\
|
|
1 0 100 /sbin/launchd
|
|
500 1 1000 /bin/bash ./cargo kani
|
|
501 500 2000 /usr/bin/kani-driver
|
|
502 501 9000000 /opt/kani/bin/cbmc --json-ui x.out
|
|
503 501 300 /opt/kani/bin/goto-instrument y.out
|
|
900 1 99999999 /usr/bin/cbmc somebody-elses.out
|
|
";
|
|
// The solver past its 8 GB cap (9,000,000 KiB is 8.6 GB): stopped, as the solver's.
|
|
let (total, solver, stop) = judge(ps, 500, 8 * 1024 * 1024, 12 * 1024 * 1024);
|
|
assert_eq!(solver, 9_000_000);
|
|
assert_eq!(total, 1000 + 2000 + 9_000_000 + 300);
|
|
assert!(
|
|
matches!(stop, Some(Stopped::Solver { kib: 9_000_000, .. })),
|
|
"{stop:?}"
|
|
);
|
|
// Under its cap but the run as a whole past its own.
|
|
let (_, _, stop) = judge(ps, 500, 10 * 1024 * 1024, 8 * 1024 * 1024);
|
|
assert!(matches!(stop, Some(Stopped::Run { .. })), "{stop:?}");
|
|
// Within both: nothing stopped. Another run's solver (pid 900) is not this run's.
|
|
let (_, _, stop) = judge(ps, 500, 10 * 1024 * 1024, 12 * 1024 * 1024);
|
|
assert_eq!(stop, None);
|
|
}
|
|
|
|
#[test]
|
|
fn a_stopped_run_is_budget_exceeded_whatever_kani_wrote() {
|
|
let proved = serde_json::json!({
|
|
"verification_results": {"results": [{
|
|
"harness_id": "proof::p", "status": "Success", "duration_ms": 10,
|
|
"checks": [
|
|
{"status": "Success", "description": "x", "category": "assertion"},
|
|
{"status": "Satisfied", "description": "a", "category": "cover"},
|
|
{"status": "Satisfied", "description": "b", "category": "cover"}
|
|
]
|
|
}]}
|
|
});
|
|
assert_eq!(
|
|
verdict(Some(&proved), "proof::p", None, 600).status,
|
|
"proved"
|
|
);
|
|
for s in [
|
|
Stopped::Solver {
|
|
kib: 9 << 20,
|
|
cap_kib: 8 << 20,
|
|
},
|
|
Stopped::Run {
|
|
kib: 13 << 20,
|
|
cap_kib: 12 << 20,
|
|
},
|
|
Stopped::Wall { secs: 1500 },
|
|
] {
|
|
let v = verdict(Some(&proved), "proof::p", Some(s), 600);
|
|
assert_eq!(v.status, "budget_exceeded", "{s:?}");
|
|
}
|
|
// Kani's own time limit, and no result at all.
|
|
let timeout = serde_json::json!({
|
|
"error_details": [{"harness_id": "proof::p", "exit_status": "timeout"}],
|
|
"verification_results": {"results": [{"harness_id": "proof::p", "status": "Failure", "checks": []}]}
|
|
});
|
|
let v = verdict(Some(&timeout), "proof::p", None, 600);
|
|
assert_eq!(v.status, "budget_exceeded");
|
|
assert!(v.reason.unwrap().contains("600 s"));
|
|
assert_eq!(verdict(None, "proof::p", None, 600).status, "not_proved");
|
|
assert_eq!(
|
|
verdict(Some(&proved), "proof::q", None, 600).status,
|
|
"not_proved"
|
|
);
|
|
// An unwinding assertion is a loop past its bound, not a proof.
|
|
let unwound = serde_json::json!({
|
|
"verification_results": {"results": [{
|
|
"harness_id": "proof::p", "status": "Failure",
|
|
"checks": [
|
|
{"status": "Failure", "description": "unwinding assertion loop 0", "category": "unwind"},
|
|
{"status": "Satisfied", "description": "a", "category": "cover"}
|
|
]
|
|
}]}
|
|
});
|
|
let v = verdict(Some(&unwound), "proof::p", None, 600);
|
|
assert_eq!(v.status, "not_proved");
|
|
assert!(v.reason.unwrap().contains("unwinding"));
|
|
}
|