diff --git a/.gitignore b/.gitignore index 475d2a6befda..0165f5801ed9 100644 --- a/.gitignore +++ b/.gitignore @@ -35,3 +35,5 @@ testcase*.json perf.data* miri-wast/ report/ +# Local SMT query cache for the ISLE verifier (see cranelift/isle/veri/verify.sh). +cranelift/isle/veri/cache/ diff --git a/Cargo.lock b/Cargo.lock index 489dc0d49cd8..d672181083fc 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -883,6 +883,7 @@ dependencies = [ "clap", "cranelift-codegen-meta", "cranelift-isle", + "cranelift-isle-veri-caching", "cranelift-isle-veri-test-macros", "easy-smt", "env_logger 0.11.5", @@ -915,6 +916,18 @@ dependencies = [ "url", ] +[[package]] +name = "cranelift-isle-veri-caching" +version = "0.1.0" +dependencies = [ + "easy-smt", + "log", + "serde", + "serde_json", + "sha2", + "tempfile", +] + [[package]] name = "cranelift-isle-veri-isaspec" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index 0a8ef05bc7f6..09127c14842c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -186,6 +186,7 @@ members = [ "cranelift/isle/islec", "cranelift/isle/veri/aslp", "cranelift/isle/veri/isaspec", + "cranelift/isle/veri/caching", "cranelift/isle/veri/test-macros", "cranelift/isle/veri/veri", "cranelift/serde", diff --git a/cranelift/isle/veri/caching/Cargo.toml b/cranelift/isle/veri/caching/Cargo.toml new file mode 100644 index 000000000000..e331d43cd3fb --- /dev/null +++ b/cranelift/isle/veri/caching/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "cranelift-isle-veri-caching" +version = "0.1.0" +edition.workspace = true +publish = false +description = "Transparent caching layer over easy-smt for the ISLE verifier" + +[dependencies] +easy-smt = "0.3.2" +log = { workspace = true } +serde = { workspace = true, features = ['derive'] } +serde_json = { workspace = true } +sha2 = "0.10" + +[dev-dependencies] +tempfile = { workspace = true } diff --git a/cranelift/isle/veri/caching/src/cache.rs b/cranelift/isle/veri/caching/src/cache.rs new file mode 100644 index 000000000000..e8bb3dff77ef --- /dev/null +++ b/cranelift/isle/veri/caching/src/cache.rs @@ -0,0 +1,384 @@ +//! Persistent store of SMT query responses. + +use std::{ + io, + path::{Path, PathBuf}, + sync::atomic::{AtomicUsize, Ordering::Relaxed}, +}; + +use serde::{Deserialize, Serialize}; +use sha2::Digest; + +/// Modes of cache operation. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum CacheMode { + /// Read-only, enforcing. Use cached results from the source cache; fail the + /// run on a cache miss. Never invokes the solver. + ReadOnlyEnforcing, + /// Read-write. Use cached results found in either the source or the + /// destination cache; on a miss, invoke the solver and write the new + /// result to the destination. Results found only in the source are also + /// copied into the destination, so the destination ends up holding exactly + /// the entries the run used — enabling cache garbage collection (a rebuild + /// that drops unused entries). + ReadWrite, +} + +impl std::str::FromStr for CacheMode { + type Err = String; + + fn from_str(s: &str) -> Result { + match s { + "read-only-enforcing" => Ok(CacheMode::ReadOnlyEnforcing), + "read-write" => Ok(CacheMode::ReadWrite), + _ => Err(format!( + "unknown cache mode '{s}' (expected 'read-only-enforcing' or 'read-write')" + )), + } + } +} + +impl std::fmt::Display for CacheMode { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.write_str(match self { + CacheMode::ReadOnlyEnforcing => "read-only-enforcing", + CacheMode::ReadWrite => "read-write", + }) + } +} + +/// A cache entry storing the response to a single SMT query. +#[derive(Serialize, Deserialize, Debug, Clone)] +struct CacheEntry { + /// Full SHA-256 hex digest of the solver name + replay script + query. + key_sha256: String, + /// Which solver was used (e.g., "cvc5" or "z3"). + solver: String, + /// The solver's response, as a JSON s-expression tree: atoms are strings, + /// lists are arrays (see [`crate::convert`]). + response: serde_json::Value, +} + +impl CacheEntry { + fn short_key(&self) -> &str { + &self.key_sha256[..12] + } +} + +/// Statistics accumulated during a run. +#[derive(Debug, Default)] +struct CacheStats { + hits: AtomicUsize, + misses: AtomicUsize, + stores: AtomicUsize, + retained: AtomicUsize, +} + +/// Persistent cache store backed by directories of JSON files. +/// +/// A cache has an optional read-only `source` directory and an optional +/// read-write `destination` directory. Lookups consult the destination first, +/// then the source. In [`CacheMode::ReadWrite`], a result found only in the +/// source is copied into the destination, so that after a full run the +/// destination contains exactly the entries the run used — the basis for a +/// garbage-collecting cache rebuild. +pub struct Cache { + /// Read-only source directory consulted for cache hits. + source: Option, + /// Destination directory: consulted for hits, and where entries are + /// written — both freshly-computed results and hits retained from + /// `source`. + dest: Option, + /// Operating mode. + mode: CacheMode, + /// Runtime statistics. + stats: CacheStats, +} + +impl Cache { + /// Open a cache with the given source and destination directories and mode. + /// + /// The destination directory (if any) is created if it doesn't exist. The + /// source directory is treated as read-only and is not created. + pub fn open(source: Option, dest: Option, mode: CacheMode) -> Self { + if let Some(dest) = &dest { + std::fs::create_dir_all(dest).unwrap_or_else(|e| { + panic!("failed to create cache directory {}: {e}", dest.display()) + }); + } + Self { + source, + dest, + mode, + stats: CacheStats::default(), + } + } + + /// The mode this cache operates in. + pub fn mode(&self) -> CacheMode { + self.mode + } + + /// Compute the cache key for a query. + /// + /// The key is the SHA-256 hash of `"{solver}\n{script}"`, where `script` + /// is the replay script of the path so far followed by the query command. + fn compute_key(solver: &str, script: &str) -> String { + let mut hash = sha2::Sha256::new(); + hash.update(solver.as_bytes()); + hash.update(b"\n"); + hash.update(script.as_bytes()); + format!("{:x}", hash.finalize()) + } + + /// Look up a cached entry by key in a specific directory. + /// + /// - `Ok(Some(entry))` on cache hit (file exists and full hash matches) + /// - `Ok(None)` on cache miss (no file, parse error, or hash mismatch) + /// - `Err(e)` on unexpected I/O errors + fn lookup_in(dir: &Path, expected_sha256: &str) -> io::Result> { + let short_key = &expected_sha256[..12]; + let path = dir.join(format!("{short_key}.json")); + + let contents = match std::fs::read_to_string(&path) { + Ok(contents) => contents, + Err(e) if e.kind() == io::ErrorKind::NotFound => return Ok(None), + Err(e) => return Err(e), + }; + + let entry: CacheEntry = match serde_json::from_str(&contents) { + Ok(entry) => entry, + Err(e) => { + log::warn!( + "cache entry {} has corrupted JSON: {e} — treating as miss", + path.display() + ); + return Ok(None); + } + }; + + // Verify the full hash to rule out collisions and corruption. + if entry.key_sha256 != expected_sha256 { + log::warn!( + "cache hash mismatch for key {short_key}: \ + expected {expected_sha256}, got {}", + entry.key_sha256 + ); + return Ok(None); + } + + Ok(Some(entry)) + } + + /// Write a cache entry into `dir`, using an atomic temp-file + rename to + /// prevent corruption from concurrent writes. + fn write_entry(dir: &Path, entry: &CacheEntry) -> io::Result<()> { + let path = dir.join(format!("{}.json", entry.short_key())); + let contents = serde_json::to_string_pretty(entry) + .map_err(|e| io::Error::new(io::ErrorKind::InvalidData, e))?; + + // Write to a temp file first, then rename for atomicity. The temp file + // name is made unique per write so concurrent writers (including two + // threads racing to persist the same key) don't clobber each other's + // temp file. + static TMP_SEQ: AtomicUsize = AtomicUsize::new(0); + let seq = TMP_SEQ.fetch_add(1, Relaxed); + let tmp_path = path.with_extension(format!("{}.{seq}.tmp", std::process::id())); + std::fs::write(&tmp_path, &contents)?; + std::fs::rename(&tmp_path, &path)?; + + Ok(()) + } + + /// Look up the cached response for a query against `solver` whose full + /// replay script (path plus query command) is `script`. + /// + /// Consults the destination cache first, then the source. In read-write + /// mode, a result found only in the source is copied into the destination + /// (so the destination accumulates exactly the entries the run used). + /// + /// Returns the response on a hit, `None` on a miss. A miss in + /// [`CacheMode::ReadOnlyEnforcing`] is reported by the caller, which has + /// the context to produce a useful error. + pub(crate) fn lookup( + &self, + solver: &str, + script: &str, + ) -> io::Result> { + let key = Self::compute_key(solver, script); + + // Destination first: freshly-written or already-retained entries. + if let Some(dest) = &self.dest + && let Some(entry) = Self::lookup_in(dest, &key)? + { + self.stats.hits.fetch_add(1, Relaxed); + return Ok(Some(entry.response)); + } + + // Then the read-only source. Retain any hit into the destination so + // that the destination ends up holding exactly the used entries. + if let Some(source) = &self.source + && let Some(entry) = Self::lookup_in(source, &key)? + { + self.stats.hits.fetch_add(1, Relaxed); + if let Some(dest) = &self.dest { + Self::write_entry(dest, &entry)?; + self.stats.retained.fetch_add(1, Relaxed); + } + return Ok(Some(entry.response)); + } + + self.stats.misses.fetch_add(1, Relaxed); + Ok(None) + } + + /// Store a freshly-computed response into the destination cache. + /// + /// No-op if there is no destination directory. + pub(crate) fn store( + &self, + solver: &str, + script: &str, + response: &serde_json::Value, + ) -> io::Result<()> { + let Some(dest) = &self.dest else { + return Ok(()); + }; + let key = Self::compute_key(solver, script); + let entry = CacheEntry { + key_sha256: key, + solver: solver.to_string(), + response: response.clone(), + }; + Self::write_entry(dest, &entry)?; + self.stats.stores.fetch_add(1, Relaxed); + Ok(()) + } + + /// Count the number of cache entry files (`*.json`) in a directory. + fn count_entries(dir: &Path) -> usize { + std::fs::read_dir(dir) + .map(|rd| { + rd.filter_map(|e| e.ok()) + .filter(|e| e.path().extension().is_some_and(|x| x == "json")) + .count() + }) + .unwrap_or(0) + } + + /// Print cache statistics summary to stdout. + pub fn print_stats(&self) { + let (hits, misses, stores, retained) = self.snapshot_stats(); + let total = hits + misses; + let hit_pct = if total > 0 { + hits as f64 / total as f64 * 100.0 + } else { + 0.0 + }; + let miss_pct = 100.0 - hit_pct; + + let dir_str = |d: &Option| match d { + Some(p) => p.display().to_string(), + None => "(none)".to_string(), + }; + + println!("========================== Cache statistics ==========================="); + println!("Mode: {}", self.mode); + println!("Source: {}", dir_str(&self.source)); + println!("Destination: {}", dir_str(&self.dest)); + println!("Hits: {hits} ({hit_pct:.1}%)"); + println!("Misses: {misses} ({miss_pct:.1}%)"); + println!("New entries: {stores}"); + println!("Retained: {retained}"); + + // When rebuilding into a fresh destination, report how many source + // entries went unused (and are therefore dropped by the rebuild). + if let (Some(source), Some(dest)) = (&self.source, &self.dest) + && source != dest + { + let source_count = Self::count_entries(source); + let dropped = source_count.saturating_sub(retained); + println!("Source entries: {source_count}"); + println!("Dropped (unused):{dropped:>4}"); + } + println!("========================================================================"); + } + + /// Get a snapshot of current stats as (hits, misses, stores, retained). + pub fn snapshot_stats(&self) -> (usize, usize, usize, usize) { + ( + self.stats.hits.load(Relaxed), + self.stats.misses.load(Relaxed), + self.stats.stores.load(Relaxed), + self.stats.retained.load(Relaxed), + ) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use serde_json::json; + + #[test] + fn test_roundtrip() { + let dir = tempfile::tempdir().unwrap(); + let cache = Cache::open(None, Some(dir.path().to_path_buf()), CacheMode::ReadWrite); + + cache + .store("cvc5", "(set-logic ALL)\n(check-sat)", &json!("unsat")) + .expect("store should succeed"); + + let result = cache + .lookup("cvc5", "(set-logic ALL)\n(check-sat)") + .expect("lookup should succeed"); + assert_eq!(result, Some(json!("unsat"))); + + // A different path is a different key. + let result = cache + .lookup("cvc5", "(set-logic QF_BV)\n(check-sat)") + .expect("lookup should succeed"); + assert_eq!(result, None); + + // A different solver is a different key. + let result = cache + .lookup("z3", "(set-logic ALL)\n(check-sat)") + .expect("lookup should succeed"); + assert_eq!(result, None); + } + + #[test] + fn test_retain_from_source() { + let source = tempfile::tempdir().unwrap(); + let dest = tempfile::tempdir().unwrap(); + + // Populate a source cache with one entry. + { + let seed = Cache::open( + None, + Some(source.path().to_path_buf()), + CacheMode::ReadWrite, + ); + seed.store("cvc5", "(check-sat)", &json!("sat")) + .expect("seed store should succeed"); + } + + // Read-write with a fresh destination: a source hit is retained into + // the destination (garbage-collecting rebuild). + let cache = Cache::open( + Some(source.path().to_path_buf()), + Some(dest.path().to_path_buf()), + CacheMode::ReadWrite, + ); + let result = cache + .lookup("cvc5", "(check-sat)") + .expect("lookup should succeed"); + assert_eq!(result, Some(json!("sat"))); + + let (hits, misses, stores, retained) = cache.snapshot_stats(); + assert_eq!((hits, misses, stores, retained), (1, 0, 0, 1)); + + // The entry now exists in the destination too. + assert_eq!(Cache::count_entries(dest.path()), 1); + } +} diff --git a/cranelift/isle/veri/caching/src/context.rs b/cranelift/isle/veri/caching/src/context.rs new file mode 100644 index 000000000000..78a66ab3c3df --- /dev/null +++ b/cranelift/isle/veri/caching/src/context.rs @@ -0,0 +1,882 @@ +//! The caching SMT context: an [`easy_smt::Context`]-compatible wrapper. + +use std::{ + ffi::OsString, + io, + sync::{Arc, Mutex}, +}; + +use easy_smt::{Response, SExpr, SExprData}; + +use crate::{ + cache::{Cache, CacheMode}, + convert, +}; + +/// Builder for a caching [`Context`], mirroring [`easy_smt::ContextBuilder`]. +/// +/// Unlike `easy_smt`, configuring a solver here does *not* spawn it at +/// [`build`](Self::build) time: the solver is launched lazily, on the first +/// query that misses the cache. +#[derive(Default)] +pub struct ContextBuilder { + solver: Option, + solver_args: Vec, + replay_file: Option>, + cache: Option>, +} + +impl ContextBuilder { + /// Construct a new builder with the default configuration. + pub fn new() -> Self { + Self::default() + } + + /// Configure the solver that will be used on a cache miss. + pub fn solver

(&mut self, program: P) -> &mut Self + where + P: Into, + { + self.solver = Some(program.into()); + self + } + + /// Configure the arguments that will be passed to the solver. + pub fn solver_args(&mut self, args: A) -> &mut Self + where + A: IntoIterator, + A::Item: Into, + { + self.solver_args = args.into_iter().map(|a| a.into()).collect(); + self + } + + /// An optional file (or anything else that is `std::io::Write`-able) where + /// all commands sent to a live solver are tee'd to. Nothing is written if + /// every query is served from the cache. + pub fn replay_file(&mut self, replay_file: Option) -> &mut Self + where + W: 'static + io::Write + Send, + { + self.replay_file = replay_file.map(|w| Box::new(w) as _); + self + } + + /// Configure the query cache. Without a cache every query is a miss, so + /// the context behaves like a (lazily spawned) plain solver context. + pub fn cache(&mut self, cache: Arc) -> &mut Self { + self.cache = Some(cache); + self + } + + /// Finish configuring the context and build it. No solver is spawned. + pub fn build(&mut self) -> io::Result { + Ok(Context { + inner: easy_smt::ContextBuilder::new().build()?, + solver: self.solver.take(), + solver_args: std::mem::take(&mut self.solver_args), + replay_file: self.replay_file.take().map(|w| Arc::new(Mutex::new(w))), + cache: self.cache.take(), + frames: vec![Vec::new()], + live: None, + pending: None, + }) + } +} + +/// A shared handle to the replay file, so that each lazily spawned solver +/// context (there may be several over this context's lifetime) can tee into +/// the same underlying writer. +struct SharedWriter(Arc>>); + +impl io::Write for SharedWriter { + fn write(&mut self, buf: &[u8]) -> io::Result { + self.0.lock().unwrap().write(buf) + } + + fn flush(&mut self) -> io::Result<()> { + self.0.lock().unwrap().flush() + } +} + +/// One command on the recorded path: the expression (in the wrapper context's +/// arena, for replaying into a spawned solver) and its display text (for +/// deriving cache keys). +struct PathCmd { + expr: SExpr, + text: String, +} + +/// An SMT-LIB2 context with transparent query caching. +/// +/// Expression-building methods are those of [`easy_smt::Context`], available +/// through `Deref`. Command methods (`assert`, `push`, `check`, `raw_send`, +/// ...) are intercepted: the tree-path of commands up to the current point is +/// recorded, queries are answered from the cache when possible, and a real +/// solver is spawned — and the recorded path played into it — only on a cache +/// miss. +pub struct Context { + /// Solver-less easy-smt context, used as the s-expression arena. + inner: easy_smt::Context, + /// Solver program to launch on a cache miss. + solver: Option, + /// Arguments for the solver program. + solver_args: Vec, + /// Shared replay tee for all solver sessions of this context. + replay_file: Option>>>, + /// The query cache. `None` disables caching (every query misses). + cache: Option>, + /// The tree-path of commands: a stack of frames delimited by `push`/`pop`. + /// `frames[0]` is the base frame; each later frame corresponds to an open + /// `push`. + frames: Vec>, + /// Live solver session, if one has been spawned by a cache miss. Its state + /// always mirrors a replay of `frames`; it is dropped whenever that stops + /// being maintainable by appending (on `pop`, or when a query is answered + /// from the cache instead of being forwarded). + live: Option, + /// Response queued by `raw_send` for the next `raw_recv`. + pending: Option, +} + +impl Context { + // --- raw command interface, mirroring `easy_smt::Context`. + + /// Directly send a command to the (logical) solver. + /// + /// The command is processed immediately — recorded, answered from cache, + /// or forwarded to a live solver — and its response is queued for the next + /// [`raw_recv`](Self::raw_recv), which must be called before the next + /// `raw_send`. + pub fn raw_send(&mut self, cmd: SExpr) -> io::Result<()> { + if self.pending.is_some() { + return Err(io::Error::other( + "raw_send called with an unconsumed pending response", + )); + } + let resp = self.dispatch(cmd)?; + self.pending = Some(resp); + Ok(()) + } + + /// Receive the response to the last [`raw_send`](Self::raw_send). + pub fn raw_recv(&mut self) -> io::Result { + self.pending + .take() + .ok_or_else(|| io::Error::other("raw_recv called with no pending response")) + } + + // --- high-level command interface, mirroring `easy_smt::Context`. + + pub fn set_option(&mut self, name: K, value: SExpr) -> io::Result<()> + where + K: Into + AsRef, + { + let cmd = self.inner.list(vec![ + self.inner.atoms().set_option, + self.inner.atom(name), + value, + ]); + self.ack(cmd) + } + + pub fn set_logic + AsRef>(&mut self, logic: L) -> io::Result<()> { + let cmd = self + .inner + .list(vec![self.inner.atoms().set_logic, self.inner.atom(logic)]); + self.ack(cmd) + } + + pub fn declare_sort + AsRef>( + &mut self, + symbol: S, + arity: i32, + ) -> io::Result { + let symbol = self.inner.atom(symbol); + let arity = self.inner.numeral(arity); + let cmd = self + .inner + .list(vec![self.inner.atoms().declare_sort, symbol, arity]); + self.ack(cmd)?; + Ok(symbol) + } + + /// Declare a new constant with the provided sort. + pub fn declare_const + AsRef>( + &mut self, + name: S, + sort: SExpr, + ) -> io::Result { + let name = self.inner.atom(name); + let cmd = self + .inner + .list(vec![self.inner.atoms().declare_const, name, sort]); + self.ack(cmd)?; + Ok(name) + } + + /// Declares a new, uninterpreted function symbol. + pub fn declare_fun + AsRef>( + &mut self, + name: S, + args: Vec, + out: SExpr, + ) -> io::Result { + let name = self.inner.atom(name); + let cmd = self.inner.list(vec![ + self.inner.atoms().declare_fun, + name, + self.inner.list(args), + out, + ]); + self.ack(cmd)?; + Ok(name) + } + + /// Defines a new function with a body. + pub fn define_fun + AsRef>( + &mut self, + name: S, + args: Vec<(S, SExpr)>, + out: SExpr, + body: SExpr, + ) -> io::Result { + let name = self.inner.atom(name); + let args = args + .into_iter() + .map(|(n, s)| self.inner.list(vec![self.inner.atom(n), s])) + .collect(); + let cmd = self.inner.list(vec![ + self.inner.atoms().define_fun, + name, + self.inner.list(args), + out, + body, + ]); + self.ack(cmd)?; + Ok(name) + } + + /// Define a constant with a value. A convenience wrapper over + /// [`Self::define_fun`] since constants are nullary functions. + pub fn define_const + AsRef>( + &mut self, + name: S, + out: SExpr, + body: SExpr, + ) -> io::Result { + self.define_fun(name, vec![], out, body) + } + + pub fn assert(&mut self, expr: SExpr) -> io::Result<()> { + let cmd = self.inner.list(vec![self.inner.atoms().assert, expr]); + self.ack(cmd) + } + + /// Push a new context frame. Same as SMT-LIB's `push` command. + pub fn push(&mut self) -> io::Result<()> { + let cmd = self.inner.list(vec![self.inner.atoms().push]); + self.ack(cmd) + } + + pub fn push_many(&mut self, n: usize) -> io::Result<()> { + let cmd = self + .inner + .list(vec![self.inner.atoms().push, self.inner.numeral(n)]); + self.ack(cmd) + } + + /// Pop a context frame. Same as SMT-LIB's `pop` command. + pub fn pop(&mut self) -> io::Result<()> { + let cmd = self.inner.list(vec![self.inner.atoms().pop]); + self.ack(cmd) + } + + pub fn pop_many(&mut self, n: usize) -> io::Result<()> { + let cmd = self + .inner + .list(vec![self.inner.atoms().pop, self.inner.numeral(n)]); + self.ack(cmd) + } + + /// Assert `check-sat` for the current context. + pub fn check(&mut self) -> io::Result { + let cmd = self.inner.list(vec![self.inner.atoms().check_sat]); + let resp = self.dispatch(cmd)?; + self.response(resp) + } + + /// Assert `check-sat-assuming` with the given list of assumptions. + pub fn check_assuming( + &mut self, + props: impl IntoIterator, + ) -> io::Result { + let args = self.inner.list(props.into_iter().collect()); + let cmd = self + .inner + .list(vec![self.inner.atoms().check_sat_assuming, args]); + let resp = self.dispatch(cmd)?; + self.response(resp) + } + + /// Get a model out from the solver. Only meaningful after a `check-sat` + /// query that returned `sat`. + pub fn get_model(&mut self) -> io::Result { + let cmd = self.inner.list(vec![self.inner.atoms().get_model]); + self.dispatch(cmd) + } + + /// Get bindings for values in the model. Only meaningful after a + /// `check-sat` query that returned `sat`. + pub fn get_value(&mut self, vals: Vec) -> io::Result> { + if vals.is_empty() { + return Ok(vec![]); + } + let cmd = self + .inner + .list(vec![self.inner.atoms().get_value, self.inner.list(vals)]); + let resp = self.dispatch(cmd)?; + match self.inner.get(resp) { + SExprData::List(pairs) => { + let mut res = Vec::with_capacity(pairs.len()); + for expr in pairs { + match self.inner.get(*expr) { + SExprData::List(pair) if pair.len() == 2 => { + res.push((pair[0], pair[1])); + } + _ => { + return Err(io::Error::new( + io::ErrorKind::InvalidData, + "failed to parse get-value response", + )); + } + } + } + Ok(res) + } + _ => Err(io::Error::new( + io::ErrorKind::InvalidData, + "failed to parse get-value response", + )), + } + } + + /// Returns the names of the formulas involved in a contradiction. + pub fn get_unsat_core(&mut self) -> io::Result { + let cmd = self.inner.list(vec![self.inner.atoms().get_unsat_core]); + self.dispatch(cmd) + } + + /// Instruct the (logical) solver to exit. If no live solver is running, + /// this is a no-op. + pub fn exit(&mut self) -> io::Result<()> { + let cmd = self.inner.list(vec![self.inner.atoms().exit]); + let _ = self.dispatch(cmd)?; + Ok(()) + } + + // --- internals. + + /// Process one command: record it on the path and produce its response, + /// consulting the cache and live solver as appropriate. + fn dispatch(&mut self, cmd: SExpr) -> io::Result { + enum Kind { + Frame, + Query, + Exit, + Ack, + } + + let (kind, arg) = { + // Classify by head atom. A bare atom command (rare) is treated + // like a single-element list. + let (head, arg) = match self.inner.get(cmd) { + SExprData::Atom(a) => (Some(a), None), + SExprData::List(items) => ( + items.first().and_then(|e| self.inner.get_atom(*e)), + items.get(1).and_then(|e| self.inner.get_atom(*e)), + ), + SExprData::String(_) => (None, None), + }; + let arg: Option = arg.and_then(|a| a.parse().ok()); + let kind = match head { + Some("push") | Some("pop") => Kind::Frame, + Some( + "check-sat" | "check-sat-using" | "check-sat-assuming" | "get-value" + | "get-model" | "get-unsat-core" | "get-info" | "get-proof", + ) => Kind::Query, + Some("exit") => Kind::Exit, + _ => Kind::Ack, + }; + (kind, arg) + }; + + let text = self.inner.display(cmd).to_string(); + match kind { + Kind::Frame => { + let n = arg.unwrap_or(1); + if text.starts_with("(push") { + self.frame_push(n, cmd) + } else { + self.frame_pop(n) + } + } + Kind::Query => self.query(cmd, &text), + Kind::Exit => self.exit_live(), + Kind::Ack => self.ack_command(cmd, text), + } + } + + /// Handle a `push`: open `n` new frames. + fn frame_push(&mut self, n: usize, cmd: SExpr) -> io::Result { + for _ in 0..n { + self.frames.push(Vec::new()); + } + if self.live.is_some() { + self.forward(cmd)?; + } + Ok(self.inner.atoms().success) + } + + /// Handle a `pop`: discard the top `n` frames. + /// + /// Any live solver is dropped: the caching layer deliberately does not + /// reuse internal solver state across a pop. A later miss respawns a + /// solver and replays the (now shorter) path. + fn frame_pop(&mut self, n: usize) -> io::Result { + if self.frames.len() <= n { + return Err(io::Error::other(format!( + "pop {n} with only {} frame(s) open", + self.frames.len() - 1 + ))); + } + self.frames.truncate(self.frames.len() - n); + self.drop_live("pop"); + Ok(self.inner.atoms().success) + } + + /// Handle a query: serve from cache or from a (lazily spawned) solver. + fn query(&mut self, cmd: SExpr, text: &str) -> io::Result { + let script = self.script_with(text); + let solver_name = self.solver_name(); + + // Consult the cache first, even if a live solver is running from an + // earlier miss: a hit avoids re-solving. Serving a hit desyncs any + // live solver (it has not seen this query), so drop it. + if let Some(cache) = &self.cache { + if let Some(response) = cache.lookup(&solver_name, &script)? { + self.drop_live("cache hit"); + self.record(cmd, text); + return convert::from_json(&self.inner, &response); + } + if cache.mode() == CacheMode::ReadOnlyEnforcing { + return Err(io::Error::other(format!( + "SMT cache miss in read-only-enforcing mode: no cached response \ + for query {text}", + ))); + } + } + + // Miss: make sure a live solver exists with the path played into it, + // then forward the query. + if self.live.is_none() { + self.spawn_and_replay()?; + } + let response = self.forward(cmd)?; + if let Some(cache) = &self.cache { + cache.store( + &solver_name, + &script, + &convert::to_json(&self.inner, response), + )?; + } + self.record(cmd, text); + Ok(response) + } + + /// Handle an acknowledged command (declare, assert, set-logic, ...): + /// record it on the path, forwarding to the live solver if there is one. + fn ack_command(&mut self, cmd: SExpr, text: String) -> io::Result { + if self.live.is_some() { + let response = self.forward(cmd)?; + self.record(cmd, &text); + return Ok(response); + } + self.record(cmd, &text); + Ok(self.inner.atoms().success) + } + + /// Handle `exit`: shut down any live solver. Never spawns one. + fn exit_live(&mut self) -> io::Result { + if let Some(mut live) = self.live.take() { + // Attempt a clean shutdown; the subprocess is killed on drop + // regardless. + let _ = live.exit(); + } + Ok(self.inner.atoms().success) + } + + /// Send one command to the live solver and return its response, copied + /// back into this context's arena. + fn forward(&mut self, cmd: SExpr) -> io::Result { + let live = self.live.as_ref().expect("forward requires a live solver"); + let sent = convert::copy(&self.inner, live, cmd); + let live = self.live.as_mut().unwrap(); + live.raw_send(sent)?; + let resp = live.raw_recv()?; + Ok(convert::copy(live, &self.inner, resp)) + } + + /// Append a command to the innermost open frame. + fn record(&mut self, expr: SExpr, text: &str) { + self.frames + .last_mut() + .expect("base frame always exists") + .push(PathCmd { + expr, + text: text.to_string(), + }); + } + + /// The replay commands for the current path: the base frame's commands, + /// then for each open frame a `(push)` followed by that frame's commands. + fn replay_cmds(&self) -> Vec { + let push = self.inner.list(vec![self.inner.atoms().push]); + let mut cmds = Vec::new(); + for (i, frame) in self.frames.iter().enumerate() { + if i > 0 { + cmds.push(push); + } + cmds.extend(frame.iter().map(|c| c.expr)); + } + cmds + } + + /// The cache-key script: the display text of the replay commands followed + /// by the query command. + fn script_with(&self, query: &str) -> String { + let mut script = String::new(); + for (i, frame) in self.frames.iter().enumerate() { + if i > 0 { + script.push_str("(push)\n"); + } + for c in frame { + script.push_str(&c.text); + script.push('\n'); + } + } + script.push_str(query); + script + } + + /// The solver's name for cache-key purposes: the file name of the solver + /// program (e.g. "cvc5"), so that keys do not depend on install paths or + /// invocation arguments (such as per-query timeouts). + fn solver_name(&self) -> String { + self.solver + .as_ref() + .and_then(|p| std::path::Path::new(p).file_name()) + .map(|n| n.to_string_lossy().into_owned()) + .unwrap_or_default() + } + + /// Spawn a solver subprocess and play the recorded path into it. + fn spawn_and_replay(&mut self) -> io::Result<()> { + let program = self + .solver + .clone() + .ok_or_else(|| io::Error::other("cache miss but no solver is configured"))?; + + let replay_cmds = self.replay_cmds(); + if let Some(replay) = &self.replay_file { + // Sessions are separated in the replay tee so that a replay file + // containing several solver sessions remains readable. + let _ = writeln!( + replay.lock().unwrap(), + "; [cache] solver session start: replaying {} command(s)", + replay_cmds.len() + ); + } + + let mut builder = easy_smt::ContextBuilder::new(); + builder + .solver(program) + .solver_args(self.solver_args.clone()); + if let Some(replay) = &self.replay_file { + builder.replay_file(Some(SharedWriter(replay.clone()))); + } + // `build` spawns the subprocess and sets the standard options + // (:print-success, :produce-models), so every subsequent command — + // including replayed ones — elicits exactly one response. + let mut live = builder.build()?; + + for cmd in replay_cmds { + let sent = convert::copy(&self.inner, &live, cmd); + live.raw_send(sent)?; + let resp = live.raw_recv()?; + // Replayed commands answer `success` (acks) or a query answer + // (`sat`/`unsat`/...), both of which are discarded; an `(error + // ...)` response means the replayed state is broken. + if let SExprData::List(items) = live.get(resp) + && items.first().and_then(|e| live.get_atom(*e)) == Some("error") + { + let display = live.display(resp).to_string(); + let cmd = self.inner.display(cmd); + return Err(io::Error::other(format!( + "solver error while replaying cached path at {cmd}: {display}", + ))); + } + } + + self.live = Some(live); + Ok(()) + } + + /// Drop the live solver, if any. + fn drop_live(&mut self, why: &str) { + if let Some(live) = self.live.take() { + drop(live); + if let Some(replay) = &self.replay_file { + let _ = writeln!(replay.lock().unwrap(), "; [cache] solver dropped ({why})"); + } + log::debug!("dropped live solver ({why})"); + } + } + + /// Issue a command whose expected response is `success`. + fn ack(&mut self, cmd: SExpr) -> io::Result<()> { + let resp = self.dispatch(cmd)?; + if resp == self.inner.atoms().success { + Ok(()) + } else { + Err(io::Error::other(format!( + "unexpected solver response: {}", + self.inner.display(resp) + ))) + } + } + + /// Interpret a response as a check-sat [`Response`]. + fn response(&self, resp: SExpr) -> io::Result { + let atoms = self.inner.atoms(); + if resp == atoms.sat { + Ok(Response::Sat) + } else if resp == atoms.unsat { + Ok(Response::Unsat) + } else if resp == atoms.unknown { + Ok(Response::Unknown) + } else { + Err(io::Error::other(format!( + "unexpected result from solver: {}", + self.inner.display(resp) + ))) + } + } +} + +use std::io::Write as _; + +/// All `&self` expression-building and inspection methods of +/// [`easy_smt::Context`] (`atom`, `list`, `numeral`, `display`, `get`, +/// `atoms`, the sort constructors, and the operator helpers) are available +/// directly on [`Context`] through deref. +/// +/// The deref target is deliberately immutable: `easy_smt`'s *command* methods +/// take `&mut self` and are therefore unreachable through it. The caching +/// interceptions above are the only way to issue commands. +impl std::ops::Deref for Context { + type Target = easy_smt::Context; + + fn deref(&self) -> &easy_smt::Context { + &self.inner + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::cache::{Cache, CacheMode}; + use std::path::PathBuf; + + /// Build a context around a solver that cannot possibly be spawned, so + /// tests prove that fully cached runs never launch a solver. + fn unspawnable_context(cache: Option>) -> Context { + let mut builder = ContextBuilder::new(); + builder + .solver("/nonexistent/definitely-not-a-solver") + .solver_args(["--nope"]); + if let Some(cache) = cache { + builder.cache(cache); + } + builder.build().unwrap() + } + + /// Drive a small verification-shaped session against a context: + /// prelude, declaration, an assert, then a pushed frame with a check-sat + /// and (on sat) a get-value, then pop and exit. Returns the check + /// response and the get-value bindings. + fn session(ctx: &mut Context) -> io::Result<(Response, Vec<(String, String)>)> { + ctx.set_logic("ALL")?; + let bv8 = ctx.bit_vec_sort(ctx.numeral(8)); + let x = ctx.declare_const("x", bv8)?; + let zero = ctx.binary(8, 0); + ctx.assert(ctx.eq(x, zero))?; + ctx.push()?; + let not_eq = ctx.not(ctx.eq(x, zero)); + ctx.assert(not_eq)?; + let resp = ctx.check()?; + let values = if resp == Response::Sat { + ctx.get_value(vec![x])? + .into_iter() + .map(|(k, v)| (ctx.display(k).to_string(), ctx.display(v).to_string())) + .collect() + } else { + vec![] + }; + ctx.pop()?; + ctx.exit()?; + Ok((resp, values)) + } + + /// A path to a fake solver: a shell script that speaks just enough of the + /// SMT-LIB2 protocol (with :print-success) to answer a session. + #[cfg(unix)] + fn fake_solver(dir: &std::path::Path) -> PathBuf { + use std::os::unix::fs::PermissionsExt; + let path = dir.join("fake-solver.sh"); + std::fs::write( + &path, + r#"#!/bin/sh +while IFS= read -r line; do + case "$line" in + "(check-sat)") echo "sat" ;; + "(get-value"*) echo "((x #b00000000))" ;; + "(exit)") echo "success"; exit 0 ;; + *) echo "success" ;; + esac +done +"#, + ) + .unwrap(); + std::fs::set_permissions(&path, std::fs::Permissions::from_mode(0o755)).unwrap(); + path + } + + /// End-to-end: a first session against a (fake) live solver populates the + /// cache; a second session with an unspawnable solver is served entirely + /// from the cache, including the get-value model. + #[cfg(unix)] + #[test] + fn test_populate_then_replay_from_cache() { + let dir = tempfile::tempdir().unwrap(); + let cache_dir = dir.path().join("cache"); + let cache = Arc::new(Cache::open( + None, + Some(cache_dir.clone()), + CacheMode::ReadWrite, + )); + + // First run: misses; spawns the fake solver. + let mut ctx = ContextBuilder::new() + .solver(fake_solver(dir.path())) + .cache(cache.clone()) + .build() + .unwrap(); + let (resp, values) = session(&mut ctx).unwrap(); + assert_eq!(resp, Response::Sat); + assert_eq!(values, vec![("x".to_string(), "#b00000000".to_string())]); + let (hits, misses, stores, _) = cache.snapshot_stats(); + assert_eq!((hits, misses, stores), (0, 2, 2)); + + // Second run: everything is served from the cache; the "solver" is + // unspawnable, but must be named like the fake solver so the cache + // keys match. No solver is launched. + let unspawnable = PathBuf::from("/nonexistent/dir/fake-solver.sh"); + let cache = Arc::new(Cache::open( + Some(cache_dir), + None, + CacheMode::ReadOnlyEnforcing, + )); + let mut ctx = ContextBuilder::new() + .solver(unspawnable) + .cache(cache.clone()) + .build() + .unwrap(); + let (resp, values) = session(&mut ctx).unwrap(); + assert_eq!(resp, Response::Sat); + assert_eq!(values, vec![("x".to_string(), "#b00000000".to_string())]); + let (hits, misses, _, _) = cache.snapshot_stats(); + assert_eq!((hits, misses), (2, 0)); + } + + /// The same query issued under different paths (different asserted state) + /// gets different cache entries. + #[cfg(unix)] + #[test] + fn test_path_distinguishes_queries() { + let dir = tempfile::tempdir().unwrap(); + let cache = Arc::new(Cache::open( + None, + Some(dir.path().join("cache")), + CacheMode::ReadWrite, + )); + + let mut ctx = ContextBuilder::new() + .solver(fake_solver(dir.path())) + .cache(cache.clone()) + .build() + .unwrap(); + ctx.set_logic("ALL").unwrap(); + ctx.push().unwrap(); + ctx.assert(ctx.true_()).unwrap(); + ctx.check().unwrap(); + ctx.pop().unwrap(); + ctx.push().unwrap(); + ctx.assert(ctx.false_()).unwrap(); + // Different frame contents: this is a distinct cacheable point, not a + // hit on the previous check. + ctx.check().unwrap(); + ctx.exit().unwrap(); + + let (hits, misses, stores, _) = cache.snapshot_stats(); + assert_eq!((hits, misses, stores), (0, 2, 2)); + } + + /// A cache miss in read-only-enforcing mode is an error and does not + /// attempt to spawn a solver. + #[test] + fn test_read_only_enforcing_miss() { + let dir = tempfile::tempdir().unwrap(); + let cache = Arc::new(Cache::open( + Some(dir.path().to_path_buf()), + None, + CacheMode::ReadOnlyEnforcing, + )); + let mut ctx = unspawnable_context(Some(cache)); + ctx.set_logic("ALL").unwrap(); + let err = ctx.check().unwrap_err(); + assert!(err.to_string().contains("read-only-enforcing")); + } + + /// Non-query commands never spawn a solver, even without a cache. + #[test] + fn test_no_spawn_without_query() { + let mut ctx = unspawnable_context(None); + ctx.set_logic("ALL").unwrap(); + let sort = ctx.declare_sort("S", 0).unwrap(); + let c = ctx.declare_const("c", sort).unwrap(); + ctx.assert(ctx.eq(c, c)).unwrap(); + ctx.push().unwrap(); + ctx.pop().unwrap(); + ctx.exit().unwrap(); + } + + /// Unbalanced pops are reported. + #[test] + fn test_unbalanced_pop() { + let mut ctx = unspawnable_context(None); + ctx.push().unwrap(); + ctx.pop().unwrap(); + assert!(ctx.pop().is_err()); + } +} diff --git a/cranelift/isle/veri/caching/src/convert.rs b/cranelift/isle/veri/caching/src/convert.rs new file mode 100644 index 000000000000..8d31aae1fec7 --- /dev/null +++ b/cranelift/isle/veri/caching/src/convert.rs @@ -0,0 +1,123 @@ +//! S-expression conversions: between two contexts' arenas, and to/from a +//! JSON tree for cache storage. +//! +//! These walks are what let the caching layer avoid parsing SMT-LIB2 text: +//! recorded commands are replayed into a freshly spawned solver context by +//! copying their trees across arenas, and cached responses are stored as JSON +//! trees (atoms as strings, lists as arrays) rather than display text. + +use std::io; + +use easy_smt::{Context, SExpr, SExprData}; +use serde_json::Value; + +/// Copy an s-expression from `src`'s arena into `dst`'s arena. +/// +/// String literals (which only ever appear in solver *responses*, e.g. +/// `(error "msg")`) are copied as verbatim quoted atoms: they display +/// identically, and no caller inspects them structurally. +pub fn copy(src: &Context, dst: &Context, expr: SExpr) -> SExpr { + match src.get(expr) { + SExprData::Atom(a) => dst.atom(a), + SExprData::String(s) => dst.atom(format!("\"{s}\"")), + SExprData::List(items) => { + let items = items.to_vec(); + let copied = items.into_iter().map(|e| copy(src, dst, e)).collect(); + dst.list(copied) + } + } +} + +/// Encode an s-expression as a JSON tree: atoms as strings, lists as arrays. +pub fn to_json(ctx: &Context, expr: SExpr) -> Value { + match ctx.get(expr) { + SExprData::Atom(a) => Value::String(a.to_string()), + SExprData::String(s) => Value::String(format!("\"{s}\"")), + SExprData::List(items) => { + let items = items.to_vec(); + Value::Array(items.into_iter().map(|e| to_json(ctx, e)).collect()) + } + } +} + +/// Rebuild an s-expression in `ctx`'s arena from a JSON tree. +pub fn from_json(ctx: &Context, value: &Value) -> io::Result { + match value { + Value::String(s) => Ok(ctx.atom(s)), + Value::Array(items) => { + let exprs = items + .iter() + .map(|v| from_json(ctx, v)) + .collect::>>()?; + Ok(ctx.list(exprs)) + } + _ => Err(io::Error::new( + io::ErrorKind::InvalidData, + format!("invalid cached s-expression: {value}"), + )), + } +} + +#[cfg(test)] +mod tests { + use super::*; + use easy_smt::ContextBuilder; + use serde_json::json; + + #[test] + fn test_copy_across_arenas() { + let a = ContextBuilder::new().build().unwrap(); + let b = ContextBuilder::new().build().unwrap(); + + let expr = a.list(vec![ + a.atom("declare-const"), + a.atom("e0"), + a.bit_vec_sort(a.numeral(64)), + ]); + let copied = copy(&a, &b, expr); + assert_eq!( + b.display(copied).to_string(), + "(declare-const e0 (_ BitVec 64))" + ); + // Copied atoms are interned in the destination: they compare equal to + // atoms built there directly. + let sat = copy(&a, &b, a.atoms().sat); + assert_eq!(sat, b.atoms().sat); + } + + #[test] + fn test_json_roundtrip() { + let ctx = ContextBuilder::new().build().unwrap(); + + let expr = ctx.list(vec![ + ctx.list(vec![ctx.atom("e0"), ctx.atom("#b0101")]), + ctx.list(vec![ + ctx.atom("e1"), + ctx.list(vec![ + ctx.atom("as"), + ctx.atom("@a"), + ctx.atom("Unspecified"), + ]), + ]), + ]); + let value = to_json(&ctx, expr); + assert_eq!( + value, + json!([["e0", "#b0101"], ["e1", ["as", "@a", "Unspecified"]]]) + ); + let back = from_json(&ctx, &value).unwrap(); + assert_eq!(ctx.display(back).to_string(), ctx.display(expr).to_string()); + + // Atoms rebuilt from JSON are interned normally. + let sat = from_json(&ctx, &json!("sat")).unwrap(); + assert_eq!(sat, ctx.atoms().sat); + } + + #[test] + fn test_from_json_rejects_non_sexpr() { + let ctx = ContextBuilder::new().build().unwrap(); + assert!(from_json(&ctx, &json!(42)).is_err()); + assert!(from_json(&ctx, &json!({"a": 1})).is_err()); + assert!(from_json(&ctx, &json!(null)).is_err()); + } +} diff --git a/cranelift/isle/veri/caching/src/lib.rs b/cranelift/isle/veri/caching/src/lib.rs new file mode 100644 index 000000000000..51dfac2ca6fc --- /dev/null +++ b/cranelift/isle/veri/caching/src/lib.rs @@ -0,0 +1,43 @@ +//! A transparent caching layer over [`easy_smt`]. +//! +//! This crate exposes a [`Context`] and [`ContextBuilder`] with the same API +//! as [`easy_smt::Context`] and [`easy_smt::ContextBuilder`], so a client can +//! switch to it by changing imports. The layer adds persistent caching of +//! solver query results: +//! +//! - The context tracks the *tree-path* of commands issued so far: a stack of +//! frames delimited by `push`/`pop`, each holding the commands (declares, +//! asserts, ...) issued within it. A `pop` discards its frame, so the path +//! always reflects exactly the definitions visible to the solver at this +//! point. +//! +//! - Any command that produces an interesting response — `check-sat`, +//! `get-value`, `get-model`, and friends — is a cacheable point. Its cache +//! key is derived from the solver name, the replay script of the current +//! path, and the command itself; the cached value is the solver's response. +//! +//! - No solver subprocess is spawned until a query actually *misses* the +//! cache. On a miss, a solver is launched and the recorded path is played +//! into it to reconstruct the state, then the query is forwarded. The live +//! solver is kept only while the path grows monotonically (so a `get-value` +//! immediately after a missed `check-sat` does not re-solve); it is dropped +//! on `pop` rather than reusing internal solver state across context +//! frames. +//! +//! The cache itself ([`Cache`]) is a directory of JSON files with an optional +//! read-only source and a read-write destination, and supports a +//! read-only-enforcing mode that fails on any miss without ever invoking a +//! solver. See [`CacheMode`]. + +mod cache; +mod context; +mod convert; + +pub use cache::{Cache, CacheMode}; +pub use context::{Context, ContextBuilder}; + +// Re-export the easy-smt surface that clients use alongside the context, so +// that switching to this crate is a pure import change. +pub use easy_smt::{ + DisplayExpr, IntoBinary, IntoDecimal, IntoNumeral, KnownAtoms, Response, SExpr, SExprData, +}; diff --git a/cranelift/isle/veri/veri/Cargo.toml b/cranelift/isle/veri/veri/Cargo.toml index c558e13adaf9..51011c201375 100644 --- a/cranelift/isle/veri/veri/Cargo.toml +++ b/cranelift/isle/veri/veri/Cargo.toml @@ -6,6 +6,7 @@ publish = false [dependencies] cranelift-isle = { version = "*", path = "../../isle/", features = ["fancy-errors", "logging"] } +cranelift-isle-veri-caching = { path = "../caching" } cranelift-codegen-meta = { version = "*", path = "../../../codegen/meta", features = ["spec"] } log = { workspace = true } env_logger = { workspace = true } diff --git a/cranelift/isle/veri/veri/src/bin/veri.rs b/cranelift/isle/veri/veri/src/bin/veri.rs index 0f7dfc94a124..f8794ade5a46 100644 --- a/cranelift/isle/veri/veri/src/bin/veri.rs +++ b/cranelift/isle/veri/veri/src/bin/veri.rs @@ -1,10 +1,12 @@ use std::path::Path; +use std::sync::Arc; use std::time::Duration; use anyhow::{Context as _, Result, format_err}; use clap::{ArgAction, Parser}; use cranelift_codegen_meta::{generate_isle, isle::get_isle_compilations}; use cranelift_isle_veri::runner::{Filter, Runner, SolverBackend, SolverRule}; +use cranelift_isle_veri_caching::{Cache, CacheMode}; /// Configuration file applied by default when no `--config` is given. const DEFAULT_CONFIG: &str = "cranelift/isle/veri/configs/aarch64-fast.args"; @@ -96,6 +98,32 @@ struct Opts { /// Dump debug output. #[arg(long)] debug: bool, + + /// Read cached SMT query results from this directory (read-only). + /// + /// Cache hits found here are served without invoking the solver. In + /// `read-write` mode, entries used from the source are also copied into + /// the destination (see `--cache-dest-dir`). + #[arg(long)] + cache_source_dir: Option, + + /// Write (and read) cached SMT query results in this directory. + /// + /// New results (solver invocations on a cache miss) are written here, as + /// are entries retained from the source. Required in `read-write` mode. + #[arg(long)] + cache_dest_dir: Option, + + /// Cache mode. + /// + /// - `read-write` (default): serve hits from the source and destination + /// caches; on a miss, invoke the solver and write the result to the + /// destination. Requires `--cache-dest-dir`. + /// - `read-only-enforcing`: serve hits from the source cache only and fail + /// the run on any miss (never invokes the solver). Requires + /// `--cache-source-dir`. + #[arg(long, default_value = "read-write")] + cache_mode: CacheMode, } impl Opts { @@ -263,6 +291,30 @@ fn main() -> Result<()> { runner.skip_solver(opts.skip_solver); runner.debug(opts.debug); + // Setup caching if any cache directory is provided. + let caching = opts.cache_source_dir.is_some() || opts.cache_dest_dir.is_some(); + if caching { + match opts.cache_mode { + CacheMode::ReadOnlyEnforcing if opts.cache_source_dir.is_none() => { + return Err(format_err!( + "--cache-mode read-only-enforcing requires --cache-source-dir" + )); + } + CacheMode::ReadWrite if opts.cache_dest_dir.is_none() => { + return Err(format_err!( + "--cache-mode read-write requires --cache-dest-dir" + )); + } + _ => {} + } + let cache = Cache::open( + opts.cache_source_dir.clone(), + opts.cache_dest_dir.clone(), + opts.cache_mode, + ); + runner.set_cache(Arc::new(cache)); + } + // Summarize what is being excluded and where output is going before // starting verification. println!("========================== Verification configuration ========================="); @@ -308,6 +360,19 @@ fn main() -> Result<()> { } println!("=========================="); + // Print cache config. + if caching { + let dir_str = |d: &Option| match d { + Some(p) => p.display().to_string(), + None => "(none)".to_string(), + }; + println!("Cache mode: {:?}", opts.cache_mode); + println!("Cache source: {}", dir_str(&opts.cache_source_dir)); + println!("Cache destination: {}", dir_str(&opts.cache_dest_dir)); + } else { + println!("Cache: off"); + } + runner.run()?; Ok(()) diff --git a/cranelift/isle/veri/veri/src/encoded/cls.rs b/cranelift/isle/veri/veri/src/encoded/cls.rs index 5dd89e6e81e0..cfd8eafbefc2 100644 --- a/cranelift/isle/veri/veri/src/encoded/cls.rs +++ b/cranelift/isle/veri/veri/src/encoded/cls.rs @@ -1,5 +1,5 @@ // Adapted from https://stackoverflow.com/questions/23856596/how-to-count-leading-zeros-in-a-32-bit-unsigned-integer -use easy_smt::*; +use cranelift_isle_veri_caching::*; fn declare(smt: &mut Context, name: String, val: SExpr) -> SExpr { smt.declare_const(name.clone(), val).unwrap(); diff --git a/cranelift/isle/veri/veri/src/encoded/clz.rs b/cranelift/isle/veri/veri/src/encoded/clz.rs index d54588cf4920..6aaf257fa024 100644 --- a/cranelift/isle/veri/veri/src/encoded/clz.rs +++ b/cranelift/isle/veri/veri/src/encoded/clz.rs @@ -1,5 +1,5 @@ // Adapted from https://stackoverflow.com/questions/23856596/how-to-count-leading-zeros-in-a-32-bit-unsigned-integer -use easy_smt::*; +use cranelift_isle_veri_caching::*; fn declare(smt: &mut Context, name: String, val: SExpr) -> SExpr { smt.declare_const(name.clone(), val).unwrap(); diff --git a/cranelift/isle/veri/veri/src/encoded/popcnt.rs b/cranelift/isle/veri/veri/src/encoded/popcnt.rs index 47f27c3cd55b..418c77c4b7c9 100644 --- a/cranelift/isle/veri/veri/src/encoded/popcnt.rs +++ b/cranelift/isle/veri/veri/src/encoded/popcnt.rs @@ -1,4 +1,4 @@ -use easy_smt::*; +use cranelift_isle_veri_caching::*; fn declare(smt: &mut Context, name: String, val: SExpr) -> SExpr { smt.declare_const(name.clone(), val).unwrap(); diff --git a/cranelift/isle/veri/veri/src/encoded/rev.rs b/cranelift/isle/veri/veri/src/encoded/rev.rs index 98b30952fdd6..e1433542d7b1 100644 --- a/cranelift/isle/veri/veri/src/encoded/rev.rs +++ b/cranelift/isle/veri/veri/src/encoded/rev.rs @@ -1,4 +1,4 @@ -use easy_smt::*; +use cranelift_isle_veri_caching::*; fn declare(smt: &mut Context, name: String, val: SExpr) -> SExpr { smt.declare_const(name.clone(), val).unwrap(); diff --git a/cranelift/isle/veri/veri/src/runner.rs b/cranelift/isle/veri/veri/src/runner.rs index 5fb8d70ca271..14446841ccdc 100644 --- a/cranelift/isle/veri/veri/src/runner.rs +++ b/cranelift/isle/veri/veri/src/runner.rs @@ -4,7 +4,7 @@ use std::{ io::Write, path::{Path, PathBuf}, str::FromStr, - sync::Mutex, + sync::{Arc, Mutex}, time::{self, Duration}, }; @@ -13,6 +13,7 @@ use cranelift_isle::{ sema::{Term, TermId}, trie_again::RuleSet, }; +use cranelift_isle_veri_caching::{self as caching, Cache}; use rayon::prelude::*; use serde::Serialize; @@ -489,6 +490,9 @@ pub struct Runner { skip_solver: bool, results_to_log_dir: bool, debug: bool, + + /// Shared cache of SMT query results (None = no caching). + cache: Option>, } impl Runner { @@ -508,6 +512,7 @@ impl Runner { results_to_log_dir: false, skip_solver: false, debug: false, + cache: None, }) } @@ -598,6 +603,11 @@ impl Runner { self.debug = debug; } + /// Enable caching with the given cache. + pub fn set_cache(&mut self, cache: Arc) { + self.cache = Some(cache); + } + pub fn run(&self) -> Result { // Clean log directory. if self.log_dir.exists() { @@ -887,6 +897,11 @@ impl Runner { // fails below. summary.print(); + // Print cache stats if caching is enabled. + if let Some(cache) = &self.cache { + cache.print_stats(); + } + // Verification failures and un-processable expansions are both overall // errors so that callers (the `veri` binary and tests) observe them via // the returned `Result`. @@ -1125,15 +1140,22 @@ impl Runner { ) -> Result { let start = time::Instant::now(); - // Solve. + // Build the SMT context through the caching layer: commands are + // recorded as they are issued, queries are answered from the cache + // when possible, and a solver subprocess is spawned — with the + // recorded state played into it — only on a cache miss. let binary = solver_backend.prog(); let args = solver_backend.args(self.timeout); let replay_file = Self::open_log_file(log_dir.clone(), "solver.smt2")?; - let smt = easy_smt::ContextBuilder::new() + let mut smt_builder = caching::ContextBuilder::new(); + smt_builder .solver(binary) .solver_args(&args) - .replay_file(Some(replay_file)) - .build()?; + .replay_file(Some(replay_file)); + if let Some(cache) = &self.cache { + smt_builder.cache(cache.clone()); + } + let smt = smt_builder.build()?; let mut solver = Solver::new(smt, &self.prog, conditions, assignment)?; solver.set_dialect(solver_backend.dialect()); diff --git a/cranelift/isle/veri/veri/src/solver.rs b/cranelift/isle/veri/veri/src/solver.rs index 0b8f526516db..c29bb4eeff45 100644 --- a/cranelift/isle/veri/veri/src/solver.rs +++ b/cranelift/isle/veri/veri/src/solver.rs @@ -1,7 +1,7 @@ use std::{cmp::Ordering, collections::HashSet, iter::zip}; use anyhow::{Context as _, Error, Result, bail, format_err}; -use easy_smt::{Context, Response, SExpr, SExprData}; +use cranelift_isle_veri_caching::{Context, Response, SExpr, SExprData}; use num_bigint::BigUint; use num_traits::Num as _; diff --git a/cranelift/isle/veri/verify.sh b/cranelift/isle/veri/verify.sh new file mode 100755 index 000000000000..ea4e3dc649a1 --- /dev/null +++ b/cranelift/isle/veri/verify.sh @@ -0,0 +1,101 @@ +#!/bin/bash +# +# Driver for VeriISLE verification with the SMT query cache. +# +# The cache lives locally at cranelift/isle/veri/cache (gitignored). Sharing +# the cache across runs in CI (via artifacts) is planned separately; for now +# these modes manage a local cache only. +# +# Usage: +# ./cranelift/isle/veri/verify.sh [MODE] +# +# Modes: +# cache-only Verify purely from the local cache, in read-only, enforcing +# mode. Fails on any cache miss and never invokes an SMT +# solver. Use this to validate that a previously generated +# cache fully covers the current backends. +# +# rebuild-cache Regenerate the cache: read from the existing cache, write +# only the entries actually used into a fresh directory, then +# swap it in. Unused entries are dropped (garbage collected). +# Cache misses are computed by invoking the SMT solver, so +# this requires z3 and/or cvc5 to be installed. +# +# (no argument) Local development: use and update the cache in-place. +# Serves cached results where possible and invokes the solver +# on misses, writing new entries back to the cache. +# +set -euo pipefail +cd "$(git rev-parse --show-toplevel)" + +MODE="${1:-local}" + +CACHE_DIR="cranelift/isle/veri/cache" +CONFIGS=( + cranelift/isle/veri/configs/aarch64.args + cranelift/isle/veri/configs/x64-iadd-base-case.args +) + +# Run the verifier for every configuration, forwarding the given cache flags. +run_all() { + for config in "${CONFIGS[@]}"; do + echo "=== veri: $config ===" + cargo run -p cranelift-isle-veri --release --bin veri -- --config "$config" "$@" + done +} + +case "$MODE" in +cache-only) + echo "=== Verifying from cache (read-only, enforcing; no solver) ===" + if [ ! -d "$CACHE_DIR" ]; then + echo "ERROR: cache directory does not exist: $CACHE_DIR" >&2 + echo "Generate it first (requires z3 and/or cvc5):" >&2 + echo " ./cranelift/isle/veri/verify.sh rebuild-cache" >&2 + exit 1 + fi + if ! run_all --cache-source-dir "$CACHE_DIR" --cache-mode read-only-enforcing; then + cat >&2 <&2 + echo " (no argument runs a local, in-place read-write verification)" >&2 + exit 1 + ;; +esac