Move solver variable graph behind smtperf feature

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
 

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

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]

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<B>,
     collected: &TraceQueue<B>,
 ) {
+    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();

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<PathBuf>,
     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<PathBuf>) {
+        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);