rucc_verify/
solver.rs

1//! Running the solver.
2//!
3//! The solver is a program found on PATH, not a crate. A bitvector solver taken as a dependency
4//! would be the largest thing in the tree by a wide margin, it would have to hold the 1.85
5//! minimum the workspace holds, and `spec/18-package-layout.md` section 18.3 asks for a reason
6//! before anything is added at all. Shelling out costs a process per rule, which is nothing
7//! against the solving, and it means the version in use is the version CI installed and can say.
8
9use std::io::Write;
10use std::process::{Command, Stdio};
11
12/// How long one query gets before the answer is [`Answer::Unknown`], in seconds.
13///
14/// Ninety, and the number is measured rather than picked. The most expensive rule in the tree is
15/// the `reached` rule in `crates/rucc-opt/rules/safety.rules`, the one about a walk the ranges
16/// bound, which asks about two free addresses and three bounded byte counts at sixty four bits.
17/// z3 settles it in between twelve and sixteen seconds on a laptop. A CI runner is slower than a
18/// laptop by a factor nobody controls, and the ten seconds this used to be was under that rule's
19/// cost on both, which is how a rule that is true and provable got reported as unproved and
20/// stopped the build.
21///
22/// The cost of a limit this loose is paid only by a rule that is genuinely not going to settle,
23/// and that rule stops the build either way. The cost of one too tight is a rule that is fine
24/// being reported as unproved, which reads as a real problem and is not one.
25const DEFAULT: u32 = 90;
26
27/// A solver that was found.
28#[derive(Debug, Clone)]
29pub struct Solver {
30    program: String,
31    seconds: u32,
32}
33
34/// What the solver said about one query.
35#[derive(Debug, Clone, PartialEq, Eq)]
36pub enum Answer {
37    /// No model exists, which is the answer a discharged rule gets: nothing makes the claim
38    /// false.
39    Unsat,
40    /// A model exists, and here is what the solver printed of it. The rule is wrong.
41    Sat(String),
42    /// The solver gave up, usually on time. Not a failure of the rule and not a pass either.
43    Unknown,
44}
45
46impl Solver {
47    /// Look for a solver on PATH.
48    ///
49    /// Returns nothing when there is none, which is what lets the tests skip rather than fail on
50    /// a machine that has not got one. CI has one, and that is where the answer matters.
51    #[must_use]
52    pub fn find() -> Option<Solver> {
53        for program in ["z3", "cvc5"] {
54            let found = Command::new(program).arg("--version").output();
55            if found.is_ok_and(|out| out.status.success()) {
56                return Some(Solver { program: program.to_owned(), seconds: DEFAULT });
57            }
58        }
59        None
60    }
61
62    /// How long a single query may take before the answer is [`Answer::Unknown`].
63    #[must_use]
64    pub fn within(self, seconds: u32) -> Solver {
65        Solver { seconds, ..self }
66    }
67
68    /// What the solver is called, for a report that has to name it.
69    #[must_use]
70    pub fn name(&self) -> &str {
71        &self.program
72    }
73
74    /// Ask one question.
75    ///
76    /// # Errors
77    ///
78    /// Anything that stops the solver from running or from being talked to.
79    pub fn ask(&self, query: &str) -> std::io::Result<Answer> {
80        let timeout = match self.program.as_str() {
81            "cvc5" => format!("--tlimit={}", self.seconds * 1000),
82            _ => format!("-T:{}", self.seconds),
83        };
84        let stdin = if self.program == "cvc5" { "-" } else { "-in" };
85
86        let mut child = Command::new(&self.program)
87            .arg(stdin)
88            .arg(timeout)
89            .stdin(Stdio::piped())
90            .stdout(Stdio::piped())
91            .stderr(Stdio::piped())
92            .spawn()?;
93        let Some(mut pipe) = child.stdin.take() else {
94            return Err(std::io::Error::other("the solver has no standard input"));
95        };
96        pipe.write_all(query.as_bytes())?;
97        drop(pipe);
98        let out = child.wait_with_output()?;
99        let said = String::from_utf8_lossy(&out.stdout);
100
101        // The first line is the verdict and anything after it is the model, which is only asked
102        // for when the verdict is `sat` and is the whole value of a refutation.
103        let mut lines = said.lines();
104        Ok(match lines.next().map(str::trim) {
105            Some("unsat") => Answer::Unsat,
106            Some("sat") => Answer::Sat(lines.collect::<Vec<_>>().join("\n")),
107            _ => Answer::Unknown,
108        })
109    }
110}
rucc_verify/solver.rs

rucc_verify/
solver.rs
