diff --git a/Cargo.toml b/Cargo.toml index dd13434..4ca6d44 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -92,6 +92,9 @@ isla-mml = { path = "isla-mml", version = "0.2.0" } isla-lib = { path = "isla-lib", version = "0.2.0" } isla-elf = { path = "isla-elf", version = "0.2.0" } +[features] +smtperf = ["isla-lib/smtperf"] + [profile.dev] opt-level = 1 diff --git a/configs/armv9p4.toml b/configs/armv9p4.toml index 93f4b74..81e5305 100644 --- a/configs/armv9p4.toml +++ b/configs/armv9p4.toml @@ -199,8 +199,6 @@ ignore = [ "EDESR" = "{ bits = 0x00000000 }" "EDECR" = "{ bits = 0x00000000 }" -"CPACR_EL1" = "{ bits = 0x0000000000000000 }" - # Avoid some extra complication "FEAT_TME_IMPLEMENTED" = false # As an alternative to the below, you could abstract the SPEBranch and diff --git a/configs/armv9p4_mmu_on.toml b/configs/armv9p4_mmu_on.toml index 127548b..73427f4 100644 --- a/configs/armv9p4_mmu_on.toml +++ b/configs/armv9p4_mmu_on.toml @@ -102,7 +102,11 @@ ignore = [ # SCR_EL3.{RW,NS} "SCR_EL3" = "{ bits = 0x0000000000000401 }" "SCTLR_EL3" = "{ bits = 0x0000000000000000 }" +"SMCR_EL1" = "{ bits = 0x0000000000000000 }" +"SMCR_EL2" = "{ bits = 0x0000000000000000 }" "SMCR_EL3" = "{ bits = 0x0000000000000000 }" +"ZCR_EL1" = "{ bits = 0x0000000000000000 }" +"ZCR_EL2" = "{ bits = 0x0000000000000000 }" "ZCR_EL3" = "{ bits = 0x0000000000000000 }" "CPTR_EL3" = "{ bits = 0x0000000000000000 }" "CNTP_CTL_EL0" = "{ bits = 0x0000000000000000 }" @@ -488,6 +492,10 @@ ignore = [ "_HDCR" = "{ bits = 0x00000000 }" "_PMCR" = "{ bits = 0x00000000 }" +"MDSCR_EL1" = "{ bits = 0x0000000000000000 }" + +"__monomorphize_descriptors" = true + # A map from register names that may appear in litmus files to Sail # register names [registers.renames] diff --git a/isla-lib/src/executor.rs b/isla-lib/src/executor.rs index 6403a33..4bf881b 100644 --- a/isla-lib/src/executor.rs +++ b/isla-lib/src/executor.rs @@ -1470,7 +1470,6 @@ pub fn start_single<'ir, B: BV, R>( let mut solver = Solver::from_checkpoint(&ctx, task.checkpoint); if let Some((def, event)) = task.fork_cond { solver.add_event(event); - solver.add(def) }; let result = run( @@ -1877,6 +1876,8 @@ pub fn trace_collector<'ir, B: BV>( mut solver: Solver, collected: &TraceQueue, ) { + solver.report_performance(shared_state.symtab.get_directory(), shared_state.symtab.files()); + match result { Ok((Run::Finished(_) | Run::Exit, _)) => { let mut events = solver.trace().to_vec(); diff --git a/isla-lib/src/ir.rs b/isla-lib/src/ir.rs index 1a04ac2..b622f80 100644 --- a/isla-lib/src/ir.rs +++ b/isla-lib/src/ir.rs @@ -47,6 +47,7 @@ use std::collections::{BTreeMap, HashMap, HashSet}; use std::fmt; use std::hash::Hash; use std::io::{Error, ErrorKind, Write}; +use std::path::{Path, PathBuf}; use std::sync::Arc; use crate::bitvector::{b64::B64, BV}; @@ -666,6 +667,7 @@ pub struct Symtab<'ir> { symbols: Vec<&'ir str>, table: HashMap<&'ir str, u32, ahash::RandomState>, next: u32, + dir: Option, files: Vec<&'ir str>, /// The Sail IR may monomorphize a tuple (A, B) into a tuple with /// two monomorphic fields. If it does so, it will leave a @@ -819,6 +821,7 @@ impl<'ir> Symtab<'ir> { symbols: Vec::with_capacity(raw.len()), table: HashMap::with_capacity_and_hasher(raw.len(), s), next: 0, + dir: None, files: files.iter().map(|f| &**f).collect(), tuple_structs: HashMap::new(), mangled_names: HashMap::new(), @@ -850,6 +853,7 @@ impl<'ir> Symtab<'ir> { symbols: Vec::new(), table: HashMap::default(), next: 0, + dir: None, files: Vec::new(), tuple_structs: HashMap::new(), mangled_names: HashMap::new(), @@ -882,6 +886,17 @@ impl<'ir> Symtab<'ir> { symtab } + pub fn set_directory(&mut self, dir: Option) { + self.dir = dir + } + + pub fn get_directory(&self) -> Option<&Path> { + match &self.dir { + Some(dir) => Some(dir.as_path()), + None => None, + } + } + pub fn lookup(&self, sym: &str) -> Name { Name::from_u32(*self.table.get(sym).unwrap_or_else(|| { eprintln!("Could not find symbol: {}", sym); diff --git a/isla-lib/src/smt.rs b/isla-lib/src/smt.rs index 68c6489..8979ab8 100644 --- a/isla-lib/src/smt.rs +++ b/isla-lib/src/smt.rs @@ -40,11 +40,15 @@ use ahash; use libc::{c_int, c_uint}; use serde::{Deserialize, Serialize}; -use petgraph::Directed; -use petgraph::graph::{Graph, NodeIndex}; -use petgraph::visit::Dfs; + +#[cfg(feature = "smtperf")] +use petgraph::{Directed, graph::{Graph, NodeIndex}, visit::Dfs}; + use z3_sys::*; +#[cfg(feature = "smtperf")] +use std::time::{Instant, Duration}; + use std::collections::{HashMap, HashSet}; use std::convert::TryInto; use std::error::Error; @@ -52,6 +56,7 @@ use std::ffi::{CStr, CString}; use std::fmt; use std::io::Write; use std::mem; +use std::path::Path; use std::ptr; use std::sync::Arc; @@ -59,7 +64,6 @@ use crate::bitvector::b64::B64; use crate::bitvector::BV; use crate::error::ExecError; use crate::ir::{Loc, Name, Symtab, Val}; -use crate::log; use crate::source_loc::SourceLoc; use crate::zencode; @@ -1260,7 +1264,10 @@ struct PerformanceInfo {} #[cfg(feature = "smtperf")] struct PerformanceInfo { - time_per_variable: HashMap, + vars: Graph<(Sym, SourceLoc), (), Directed>, + var_nodes: HashMap, + time_per_location: HashMap, + start: Instant, } impl PerformanceInfo { @@ -1272,8 +1279,103 @@ impl PerformanceInfo { #[cfg(feature = "smtperf")] fn new() -> Self { PerformanceInfo { - time_per_variable: HashMap::default() + vars: Graph::new(), + var_nodes: HashMap::default(), + time_per_location: HashMap::default(), + start: Instant::now(), + } + } + + #[cfg(not(feature = "smtperf"))] + fn add_var_node(&mut self, _: Sym, _: SourceLoc) { + () + } + + #[cfg(feature = "smtperf")] + fn add_var_node(&mut self, v: Sym, info: SourceLoc) { + let index = self.vars.add_node((v, info)); + self.var_nodes.insert(v, index); + } + + #[cfg(not(feature = "smtperf"))] + fn add_var_edge(&mut self, _: &Sym, _: &Sym) { + () + } + + #[cfg(feature = "smtperf")] + fn add_var_edge(&mut self, v1: &Sym, v2: &Sym) { + let Some(source) = self.var_nodes.get(v1) else { return }; + let Some(target) = self.var_nodes.get(v2) else { return }; + self.vars.update_edge(*source, *target, ()); + } + + #[cfg(not(feature = "smtperf"))] + fn start(&mut self) {} + + #[cfg(feature = "smtperf")] + fn start(&mut self) { + self.start = Instant::now() + } + + #[cfg(not(feature = "smtperf"))] + fn assign_cost(&mut self, _: &Exp) {} + + #[cfg(feature = "smtperf")] + fn assign_cost(&mut self, exp: &Exp) { + let elapsed = self.start.elapsed(); + + let mut edges = Vec::new(); + + // Petgraph DFS requires a single root, so we add a dummy node + // with edges to all the variables in the root expression. + let root = self.vars.add_node((Sym::from_u32(u32::MAX), SourceLoc::unknown())); + for var in exp.variables().iter() { + let Some(in_frame) = self.var_nodes.get(&var) else { continue }; + edges.push(self.vars.update_edge(root, *in_frame, ())); + } + + let mut dfs = Dfs::new(&self.vars, root); + while let Some(node) = dfs.next(&self.vars) { + if node != root { + let (_, info) = self.vars.node_weight(node).unwrap(); + *self.time_per_location.entry(*info).or_insert(Duration::ZERO) += elapsed + } + } + + // Remove the edges and dummy root we added + for edge in edges { + self.vars.remove_edge(edge); + } + self.vars.remove_node(root); + } + + #[cfg(not(feature = "smtperf"))] + fn report_performance>(&self, _: Option

, _: &[&str]) {} + + #[cfg(feature = "smtperf")] + fn report_performance>(&self, dir: Option

, files: &[&str]) { + let mut times: Vec<(SourceLoc, Duration)> = Vec::new(); + + for (&info, &duration) in self.time_per_location.iter() { + if !info.is_unknown() { + times.push((info, duration)) + } + } + + times.sort_by(|(_, d1), (_, d2)| d2.cmp(d1)); + + let mut msg = String::new(); + + for (n, (info, duration)) in times.iter().enumerate() { + if n >= 10 { + break + } + + msg += &info.message(dir.as_ref(), files, &format!("#{} time: {}ms", n + 1, duration.as_millis()), false, true); + msg += "\n" } + + eprint!("{}", msg) } } @@ -1328,9 +1430,6 @@ impl PerformanceInfo { /// assert!(solver.check_sat() == SmtResult::Unsat); pub struct Solver<'ctx, B> { trace: Trace, - vars: Graph, - var_nodes: HashMap, - memory_vars: HashSet, next_var: u32, def_attrs: DefAttrs, cycles: i128, @@ -1340,7 +1439,6 @@ pub struct Solver<'ctx, B> { z3_solver: Z3_solver, ctx: &'ctx Context, performance_info: PerformanceInfo, - reset_duration: std::time::Duration, } impl<'ctx, B> Drop for Solver<'ctx, B> { @@ -1565,9 +1663,6 @@ impl<'ctx, B: BV> Solver<'ctx, B> { Solver { ctx, z3_solver, - vars: Graph::new(), - var_nodes: HashMap::default(), - memory_vars: HashSet::default(), next_var: 0, def_attrs: DefAttrs::default(), cycles: 0, @@ -1576,11 +1671,14 @@ impl<'ctx, B: BV> Solver<'ctx, B> { func_decls: HashMap::new(), enums: Enums::new(ctx), performance_info: PerformanceInfo::new(), - reset_duration: std::time::Duration::ZERO, } } } + pub fn report_performance>(&self, dir: Option

, files: &[&str]) { + self.performance_info.report_performance(dir, files) + } + pub fn fresh(&mut self) -> Sym { let n = self.next_var; self.next_var += 1; @@ -1747,46 +1845,41 @@ impl<'ctx, B: BV> Solver<'ctx, B> { EnumId { id } } - fn add_var_node(&mut self, v: Sym) { - let index = self.vars.add_node(v); - self.var_nodes.insert(v, index); - } - - fn add_var_edge(&mut self, v1: &Sym, v2: &Sym) { - let Some(source) = self.var_nodes.get(v1) else { return }; - let Some(target) = self.var_nodes.get(v2) else { return }; - self.vars.update_edge(*source, *target, ()); - } - - fn add_internal(&mut self, def: &Def) { + fn add_internal(&mut self, def: &Def, info: SourceLoc) { match &def { Def::Assert(exp) => { let vars = exp.variables(); - for v1 in vars.iter() { - for v2 in vars.iter() { - if v1 != v2 { - self.add_var_edge(v1, v2) + if cfg!(feature = "smtperf") { + for v1 in vars.iter() { + for v2 in vars.iter() { + if v1 != v2 { + self.performance_info.add_var_edge(v1, v2) + } } } } self.z3_assert(exp) } Def::DeclareConst(v, ty) => { - self.add_var_node(*v); + self.performance_info.add_var_node(*v, info); let fd = FuncDecl::new(self.ctx, *v, &self.enums, &[], ty); self.decls.insert(*v, Ast::mk_constant(&fd)); } Def::DeclareFun(v, arg_tys, result_ty) => { - self.add_var_node(*v); + if cfg!(feature = "smtperf") { + self.performance_info.add_var_node(*v, info); + } let fd = FuncDecl::new(self.ctx, *v, &self.enums, arg_tys, result_ty); self.func_decls.insert(*v, fd); } Def::DefineConst(v, exp) => { - self.add_var_node(*v); - for used in exp.variables().iter() { - self.add_var_edge(v, used); - self.add_var_edge(used, v) - }; + if cfg!(feature = "smtperf") { + self.performance_info.add_var_node(*v, info); + for used in exp.variables().iter() { + self.performance_info.add_var_edge(v, used); + self.performance_info.add_var_edge(used, v) + }; + } let mut ast = self.translate_exp(exp); ast.simplify(); self.decls.insert(*v, ast); @@ -1854,12 +1947,12 @@ impl<'ctx, B: BV> Solver<'ctx, B> { } pub fn add(&mut self, def: Def) { - self.add_internal(&def); + self.add_internal(&def, SourceLoc::unknown()); self.trace.head.push(Event::Smt(def, self.def_attrs, SourceLoc::unknown())) } pub fn add_with_location(&mut self, def: Def, info: SourceLoc) { - self.add_internal(&def); + self.add_internal(&def, info); self.trace.head.push(Event::Smt(def, self.def_attrs, info)) } @@ -1899,13 +1992,12 @@ impl<'ctx, B: BV> Solver<'ctx, B> { } fn add_event_internal(&mut self, event: &Event) { - if let Event::Smt(def, _, _) = event { - self.add_internal(def) + if let Event::Smt(def, _, info) = event { + self.add_internal(def, *info) }; } pub fn add_event(&mut self, event: Event) { - //event.collect_memory_symbolic_variables(&mut self.memory_vars); self.add_event_internal(&event); self.trace.head.push(event) } @@ -1918,73 +2010,73 @@ impl<'ctx, B: BV> Solver<'ctx, B> { self.add_event(Event::Function { name, call: false }) } - pub fn reset(&mut self, mut vars: HashSet) { - let start = std::time::Instant::now(); - unsafe { - Z3_solver_reset(self.ctx.z3_ctx, self.z3_solver) - } - - let mut edges = Vec::new(); - let root = self.vars.add_node(Sym::from_u32(u32::MAX)); - for var in vars.iter().cloned().chain(self.memory_vars.iter().cloned()) { - let Some(in_frame) = self.var_nodes.get(&var) else { continue }; - edges.push(self.vars.update_edge(root, *in_frame, ())); - } - - let mut dfs = Dfs::new(&self.vars, root); - while let Some(node) = dfs.next(&self.vars) { - vars.insert(*self.vars.node_weight(node).unwrap()); - } - - let mut current_head = &self.trace.head; - let mut current_tail = self.trace.tail.as_ref(); - let mut total = 0; - let mut removed = 0; - let mut totalv = 0; - let mut removedv = 0; - loop { - 'outer: for def in current_head.iter().rev() { - match def { - Event::Smt(Def::Assert(exp), _, _) => { - total += 1; - for var in exp.variables() { - if vars.contains(&var) { - let ast = self.translate_exp(exp); - unsafe { - Z3_solver_assert(self.ctx.z3_ctx, self.z3_solver, ast.z3_ast); - } - continue 'outer - } - } - removed += 1; - } - Event::Smt(Def::DeclareConst(v, _), _, _) => { - totalv += 1; - if !vars.contains(v) { - self.func_decls.remove(v); - removedv += 1; - } - } - _ => (), - } - } - match current_tail { - Some(trace) => { - current_head = &trace.head; - current_tail = trace.tail.as_ref(); - } - None => break, - } - }; - - for edge in edges { - self.vars.remove_edge(edge); - } - self.vars.remove_node(root); - - self.reset_duration = self.reset_duration + start.elapsed(); - log!(log::VERBOSE, format!("Spent {:?} resetting {} {}", self.reset_duration, removed as f32 / total as f32, removedv as f32 / totalv as f32)); - } + // pub fn reset(&mut self, mut vars: HashSet) { + // let start = std::time::Instant::now(); + // unsafe { + // Z3_solver_reset(self.ctx.z3_ctx, self.z3_solver) + // } + + // let mut edges = Vec::new(); + // let root = self.vars.add_node(Sym::from_u32(u32::MAX)); + // for var in vars.iter().cloned().chain(self.memory_vars.iter().cloned()) { + // let Some(in_frame) = self.var_nodes.get(&var) else { continue }; + // edges.push(self.vars.update_edge(root, *in_frame, ())); + // } + + // let mut dfs = Dfs::new(&self.vars, root); + // while let Some(node) = dfs.next(&self.vars) { + // vars.insert(*self.vars.node_weight(node).unwrap()); + // } + + // let mut current_head = &self.trace.head; + // let mut current_tail = self.trace.tail.as_ref(); + // let mut total = 0; + // let mut removed = 0; + // let mut totalv = 0; + // let mut removedv = 0; + // loop { + // 'outer: for def in current_head.iter().rev() { + // match def { + // Event::Smt(Def::Assert(exp), _, _) => { + // total += 1; + // for var in exp.variables() { + // if vars.contains(&var) { + // let ast = self.translate_exp(exp); + // unsafe { + // Z3_solver_assert(self.ctx.z3_ctx, self.z3_solver, ast.z3_ast); + // } + // continue 'outer + // } + // } + // removed += 1; + // } + // Event::Smt(Def::DeclareConst(v, _), _, _) => { + // totalv += 1; + // if !vars.contains(v) { + // self.func_decls.remove(v); + // removedv += 1; + // } + // } + // _ => (), + // } + // } + // match current_tail { + // Some(trace) => { + // current_head = &trace.head; + // current_tail = trace.tail.as_ref(); + // } + // None => break, + // } + // }; + + // for edge in edges { + // self.vars.remove_edge(edge); + // } + // self.vars.remove_node(root); + + // self.reset_duration = self.reset_duration + start.elapsed(); + // log!(log::VERBOSE, format!("Spent {:?} resetting {} {}", self.reset_duration, removed as f32 / total as f32, removedv as f32 / totalv as f32)); + // } fn replay(&mut self, num: usize, trace: Arc>>) { // Some extra work would be required to replay on top of @@ -2020,17 +2112,22 @@ impl<'ctx, B: BV> Solver<'ctx, B> { } pub fn check_sat_with(&mut self, exp: &Exp, _info: SourceLoc) -> SmtResult { + self.performance_info.start(); + let ast = self.translate_exp(exp); - unsafe { - let result = Z3_solver_check_assumptions(self.ctx.z3_ctx, self.z3_solver, 1, &ast.z3_ast); - if result == Z3_L_TRUE { + let result = unsafe { + let z3_result = Z3_solver_check_assumptions(self.ctx.z3_ctx, self.z3_solver, 1, &ast.z3_ast); + if z3_result == Z3_L_TRUE { Sat - } else if result == Z3_L_FALSE { + } else if z3_result == Z3_L_FALSE { Unsat } else { Unknown } - } + }; + + self.performance_info.assign_cost(exp); + result } pub fn trace(&self) -> &Trace { diff --git a/isla-lib/src/source_loc.rs b/isla-lib/src/source_loc.rs index ac11ba5..c47fef7 100644 --- a/isla-lib/src/source_loc.rs +++ b/isla-lib/src/source_loc.rs @@ -39,7 +39,7 @@ pub static GREEN: &str = "\x1b[0;32m"; pub static BLUE: &str = "\x1b[0;34m"; pub static NO_COLOR: &str = "\x1b[0m"; -#[derive(Copy, Clone, Debug, Serialize, Deserialize)] +#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash)] pub struct SourceLoc { file: i16, line1: u32, @@ -53,6 +53,10 @@ impl SourceLoc { SourceLoc { file: -1, line1: 0, char1: 0, line2: 0, char2: 0 } } + pub fn is_unknown(self) -> bool { + self.file == -1 + } + pub(crate) fn unknown_unique(n: u32) -> Self { SourceLoc { file: -1, line1: n, char1: 0, line2: 0, char2: 0 } } @@ -261,7 +265,7 @@ impl SourceLoc { let no_color = if use_colors { NO_COLOR } else { "" }; let (short_error, error_sep) = - if is_error { (format!("{}error{}: {}", red, no_color, message), "\n") } else { ("".to_string(), "") }; + if is_error { (format!("{}error{}: {}", red, no_color, message), "\n") } else { (message.to_string(), "\n") }; let file = TryInto::::try_into(self.file).ok().and_then(|i| files.get(i)); if file.is_none() { diff --git a/src/opts.rs b/src/opts.rs index 92c91e4..29ac8e5 100644 --- a/src/opts.rs +++ b/src/opts.rs @@ -531,6 +531,7 @@ pub fn parse_with_arch<'ir, B: BV>( } let source_path = matches.opt_str("source").map(PathBuf::from); + symtab.set_directory(source_path.clone()); CommonOpts { num_threads, arch, symtab, type_info, isa_config, source_path } }