From c265e278e56750c48547f3077acc237c6b507bad Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 27 Jun 2024 12:24:07 +0100 Subject: [PATCH] Allow cycles with no opcode Run rustfmt --- build.rs | 12 +- isla-axiomatic/src/axiomatic.rs | 165 +++++++++++------------ isla-axiomatic/src/footprint_analysis.rs | 65 ++++++--- isla-axiomatic/src/graph/graph_events.rs | 8 +- isla-axiomatic/src/litmus.rs | 25 ++-- isla-axiomatic/src/litmus/exp.rs | 86 +++++------- isla-axiomatic/src/page_table.rs | 12 +- isla-axiomatic/src/run_litmus.rs | 12 +- isla-axiomatic/src/smt_events.rs | 63 +++++---- isla-axiomatic/src/smt_relations.rs | 8 +- isla-cat/src/smt.rs | 2 +- isla-lib/src/executor.rs | 47 ++++++- isla-lib/src/executor/frame.rs | 15 +-- isla-lib/src/ir.rs | 6 +- isla-lib/src/probe.rs | 14 +- isla-lib/src/simplify.rs | 10 +- isla-lib/src/smt.rs | 1 - isla-mml/src/accessor.rs | 10 +- isla-mml/src/smt.rs | 4 +- src/axiomatic.rs | 58 ++++---- src/opts.rs | 2 +- 21 files changed, 344 insertions(+), 281 deletions(-) diff --git a/build.rs b/build.rs index a39dfa9..664976a 100644 --- a/build.rs +++ b/build.rs @@ -59,12 +59,12 @@ fn main() { println!("cargo:rerun-if-changed=libz3.a"); let target = std::env::var("TARGET").unwrap(); - let cxx = - if target.contains("apple") { // sigh. - "c++".to_string() - } else { - "stdc++".to_string() - }; + let cxx = if target.contains("apple") { + // sigh. + "c++".to_string() + } else { + "stdc++".to_string() + }; println!("cargo:rustc-link-lib=static={}", cxx); println!("cargo:rustc-link-lib=static:+bundle=z3"); diff --git a/isla-axiomatic/src/axiomatic.rs b/isla-axiomatic/src/axiomatic.rs index ebb2f9b..9852f56 100644 --- a/isla-axiomatic/src/axiomatic.rs +++ b/isla-axiomatic/src/axiomatic.rs @@ -36,21 +36,21 @@ use std::fmt; use isla_lib::bitvector::BV; use isla_lib::config::ISAConfig; +use isla_lib::error::IslaError; use isla_lib::ir::{Name, SharedState, Val}; use isla_lib::memory::Memory; use isla_lib::smt::{smtlib::Def, smtlib::Ty, EvPath, Event, Sym}; -use isla_lib::error::IslaError; use isla_lib::source_loc::SourceLoc; use isla_mml::accessor::ModelEvent; use isla_mml::memory_model; -use crate::litmus::Litmus; +use crate::graph::GraphOpts; use crate::litmus::exp::Loc as LitmusLoc; +use crate::litmus::Litmus; +use crate::page_table::VirtualAddress; use crate::sexp::SexpVal; use crate::smt_model::Model; -use crate::graph::GraphOpts; -use crate::page_table::VirtualAddress; pub type ThreadId = usize; @@ -121,7 +121,9 @@ impl<'ev, B: BV> Iterator for Candidates<'ev, B> { #[derive(Debug)] pub struct AxEvent<'ev, B> { /// The opcode for the instruction that contained the underlying event - pub opcode: B, + /// An axiomatic event may have no opcode if it occurred in a cycle that + /// ended prior to ifetch. + pub opcode: Option, /// The place of the event in the instruction-order (the sequence /// of instructions as they appear in the trace) for it's thread pub instruction_index: usize, @@ -164,7 +166,7 @@ impl<'ev, B: BV> ModelEvent<'ev, B> for AxEvent<'ev, B> { self.index_set } - fn opcode(&self) -> B { + fn opcode(&self) -> Option { self.opcode } } @@ -383,7 +385,7 @@ pub mod relations { pub fn amo( ev1: &AxEvent, ev2: &AxEvent, - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, ) -> bool { is_read(ev1) @@ -426,12 +428,12 @@ pub mod relations { ev1.thread_id != ev2.thread_id } - pub type DepRel = fn(&AxEvent, &AxEvent, &[Vec], &HashMap) -> bool; + pub type DepRel = fn(&AxEvent, &AxEvent, &[Vec>], &HashMap) -> bool; pub fn addr( ev1: &AxEvent, ev2: &AxEvent, - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, ) -> bool { !ev1.is_ifetch @@ -443,7 +445,7 @@ pub mod relations { pub fn data( ev1: &AxEvent, ev2: &AxEvent, - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, ) -> bool { !ev1.is_ifetch @@ -455,7 +457,7 @@ pub mod relations { pub fn ctrl( ev1: &AxEvent, ev2: &AxEvent, - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, ) -> bool { !ev1.is_ifetch @@ -467,7 +469,7 @@ pub mod relations { pub fn rmw( ev1: &AxEvent, ev2: &AxEvent, - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, ) -> bool { (po(ev1, ev2) || intra_instruction_ordered(ev1, ev2)) @@ -518,7 +520,7 @@ pub struct ExecutionInfo<'ev, B> { /// but are useful for display purposes pub other_events: Vec>, /// A vector of po-ordered instruction opcodes for each thread - pub thread_opcodes: Vec>, + pub thread_opcodes: Vec>>, /// The final write (or initial value if unwritten) for each register in each thread pub final_writes: HashMap<(Name, ThreadId), &'ev Val>, /// A mapping from SMT symbols to their types @@ -739,7 +741,7 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> { self.smt_events.retain(|ev| { if let Some(trans_id) = ev.translate { let merged = all_translations.entry(trans_id).or_insert_with(|| MergedTranslation { - opcode: ev.opcode, + opcode: ev.opcode.unwrap(), instruction_index: ev.instruction_index, intra_instruction_index: ev.intra_instruction_index, thread_id: ev.thread_id, @@ -748,7 +750,7 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> { // Each translate event we encounter with a specific // translation id should be from the same instruction - assert_eq!(ev.opcode, merged.opcode); + assert_eq!(ev.opcode.unwrap(), merged.opcode); assert_eq!(ev.instruction_index, merged.instruction_index); assert_eq!(ev.thread_id, merged.thread_id); @@ -774,7 +776,7 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> { let s1_name = format!("TRANS_S1_{}", trans_id); let s2_name = format!("TRANS_S2_{}", trans_id); self.smt_events.push(AxEvent { - opcode: merged.opcode, + opcode: Some(merged.opcode), instruction_index: merged.instruction_index, intra_instruction_index: merged.intra_instruction_index, in_program_order: false, @@ -788,7 +790,7 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> { translate: Some(trans_id), }); self.smt_events.push(AxEvent { - opcode: merged.opcode, + opcode: Some(merged.opcode), instruction_index: merged.instruction_index, intra_instruction_index: merged.intra_instruction_index, in_program_order: false, @@ -804,7 +806,7 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> { } else { let name = format!("TRANS_{}", trans_id); self.smt_events.push(AxEvent { - opcode: merged.opcode, + opcode: Some(merged.opcode), instruction_index: merged.instruction_index, intra_instruction_index: merged.intra_instruction_index, in_program_order: false, @@ -933,7 +935,7 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> { if let Some(opcode) = cycle_instr { return Err(MultipleInstructionsInCycle { opcode1: *bv, opcode2: opcode }); } else { - exec.thread_opcodes[tid].push(*bv); + exec.thread_opcodes[tid].push(Some(*bv)); cycle_instr = Some(*bv) } } @@ -985,36 +987,37 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> { } if po != 0 { + if cycle_instr.is_none() { + exec.thread_opcodes[tid].push(None) + } + for ( iio, CycleEvent { tid, name, event, in_program_order, is_ifetch, translate, include_in_smt }, ) in cycle_events.drain(..).enumerate() { - // Events must be associated with an instruction - if let Some(opcode) = cycle_instr { - let evs = if include_in_smt && !(ignore_ifetch && is_ifetch) { - &mut exec.smt_events - } else { - &mut exec.other_events - }; - - // An event is a translate event if it was - // created by the translation function - evs.push(AxEvent { - opcode, - instruction_index: po - 1, - intra_instruction_index: iio, - in_program_order, - thread_id: tid, - name: name.clone(), - mm_name: symtab.intern_owned(name), - base: vec![event], - index_set: None, - extra: vec![], - is_ifetch, - translate, - }) - } + let evs = if include_in_smt && !(ignore_ifetch && is_ifetch) { + &mut exec.smt_events + } else { + &mut exec.other_events + }; + + // An event is a translate event if it was + // created by the translation function + evs.push(AxEvent { + opcode: cycle_instr, + instruction_index: po - 1, + intra_instruction_index: iio, + in_program_order, + thread_id: tid, + name: name.clone(), + mm_name: symtab.intern_owned(name), + base: vec![event], + index_set: None, + extra: vec![], + is_ifetch, + translate, + }) } } } @@ -1051,22 +1054,22 @@ impl<'l> fmt::Display for FinalLocValuesError<'l> { match self { ReadModelError => { write!(f, "Failed to parse smt model") - }, + } LocInterpretError => { write!(f, "Failed to read from smt model") - }, + } BadAddressWidth(addr, width) => { write!(f, "Bad address width, {} has width {}, but should be one of [4, 8]", addr, width) - }, + } BadLastWriteTo(val) => { write!(f, "Bad last_write_to({}), should return Bits", val) - }, + } BadRegisterName(reg, thread_id) => { write!(f, "Could not find register {}:{:?}", thread_id, reg) - }, + } BadAddress(addr) => { write!(f, "Could not find address {}", addr) - }, + } } } } @@ -1088,39 +1091,35 @@ pub fn final_state_from_z3_output<'exec, 'ev, 'litmus, 'model, B: BV>( // later in the code let model_buf: &str = &z3_output[3..]; let event_names: Vec<&'ev str> = exec.smt_events.iter().map(|ev| ev.name.as_ref()).collect(); - let mut model = - Model::::parse(&event_names, model_buf) - .map_err(|_mpe| FinalLocValuesError::ReadModelError)?; - - let mut calc = |loc: &'litmus LitmusLoc| { - match loc { - LitmusLoc::Register { reg, thread_id } => { - exec.final_writes.get(&(*reg, *thread_id)) - .cloned() - .cloned() - .ok_or_else(|| FinalLocValuesError::BadRegisterName(reg, *thread_id)) - }, - LitmusLoc::LastWriteTo { address, bytes } => { - let symbolic_addr = - litmus.symbolic_addrs.get(address) - .ok_or_else(|| FinalLocValuesError::BadAddress(address))?; - let addr_bv = B::from_u64(*symbolic_addr); - - let r = - if *bytes == 4 { - model.interpret("last_write_to_32", &[SexpVal::Bits(addr_bv)]) - .map_err(|_ie| FinalLocValuesError::LocInterpretError) - } else if *bytes == 8 { - model.interpret("last_write_to_64", &[SexpVal::Bits(addr_bv)]) - .map_err(|_ie| FinalLocValuesError::LocInterpretError) - } else { - Err(FinalLocValuesError::BadAddressWidth(address, *bytes)) - }?; + let mut model = Model::::parse(&event_names, model_buf).map_err(|_mpe| FinalLocValuesError::ReadModelError)?; + + let mut calc = |loc: &'litmus LitmusLoc| match loc { + LitmusLoc::Register { reg, thread_id } => exec + .final_writes + .get(&(*reg, *thread_id)) + .cloned() + .cloned() + .ok_or_else(|| FinalLocValuesError::BadRegisterName(reg, *thread_id)), + LitmusLoc::LastWriteTo { address, bytes } => { + let symbolic_addr = + litmus.symbolic_addrs.get(address).ok_or_else(|| FinalLocValuesError::BadAddress(address))?; + let addr_bv = B::from_u64(*symbolic_addr); + + let r = if *bytes == 4 { + model + .interpret("last_write_to_32", &[SexpVal::Bits(addr_bv)]) + .map_err(|_ie| FinalLocValuesError::LocInterpretError) + } else if *bytes == 8 { + model + .interpret("last_write_to_64", &[SexpVal::Bits(addr_bv)]) + .map_err(|_ie| FinalLocValuesError::LocInterpretError) + } else { + Err(FinalLocValuesError::BadAddressWidth(address, *bytes)) + }?; - match r { - SexpVal::Bits(b) => Ok(Val::Bits(b)), - _ => Err(FinalLocValuesError::BadLastWriteTo(address)), - } + match r { + SexpVal::Bits(b) => Ok(Val::Bits(b)), + _ => Err(FinalLocValuesError::BadLastWriteTo(address)), } } }; @@ -1133,4 +1132,4 @@ pub fn final_state_from_z3_output<'exec, 'ev, 'litmus, 'model, B: BV>( } Ok(values) -} \ No newline at end of file +} diff --git a/isla-axiomatic/src/footprint_analysis.rs b/isla-axiomatic/src/footprint_analysis.rs index d60a12b..9a9208b 100644 --- a/isla-axiomatic/src/footprint_analysis.rs +++ b/isla-axiomatic/src/footprint_analysis.rs @@ -206,23 +206,29 @@ impl Footprint { // load-exclusive and `to` is a store-exclusive and there are no // intervening exclusives. #[allow(clippy::needless_range_loop)] -pub fn rmw_dep(from: usize, to: usize, instrs: &[B], footprints: &HashMap) -> bool { +pub fn rmw_dep(from: usize, to: usize, instrs: &[Option], footprints: &HashMap) -> bool { if from > to { return false; } - let from_footprint = footprints.get(&instrs[from]).unwrap(); + let Some(from_opcode) = instrs[from] else { return false }; + + let Some(to_opcode) = instrs[to] else { return false }; + + let from_footprint = footprints.get(&from_opcode).unwrap(); if !(from_footprint.is_exclusive && from_footprint.is_load) { return false; } for i in (from + 1)..to { - if footprints.get(&instrs[i]).unwrap().is_exclusive { + let Some(opcode) = instrs[i] else { continue }; + + if footprints.get(&opcode).unwrap().is_exclusive { return false; } } - let to_footprint = footprints.get(&instrs[to]).unwrap(); + let to_footprint = footprints.get(&to_opcode).unwrap(); to_footprint.is_exclusive && to_footprint.is_store } @@ -232,13 +238,18 @@ pub fn rmw_dep(from: usize, to: usize, instrs: &[B], footprints: &HashMap fn touched_by( from: usize, to: usize, - instrs: &[B], + instrs: &[Option], footprints: &HashMap, ) -> HashSet { - let mut touched = footprints.get(&instrs[from]).unwrap().register_writes_tainted.clone(); + let Some(from_opcode) = instrs[from] else { return HashSet::new() }; + + let mut touched = footprints.get(&from_opcode).unwrap().register_writes_tainted.clone(); let mut new_touched = HashSet::new(); + for i in (from + 1)..to { - let footprint = footprints.get(&instrs[i]).unwrap(); + let Some(opcode) = instrs[i] else { continue }; + + let footprint = footprints.get(&opcode).unwrap(); for rreg in &touched { if footprint.register_reads.contains(rreg) { @@ -273,18 +284,20 @@ fn touched_by( /// /// Panics if either `from` or `to` are out-of-bounds in `instrs`, or /// if an instruction does not have a footprint. -pub fn addr_dep(from: usize, to: usize, instrs: &[B], footprints: &HashMap) -> bool { +pub fn addr_dep(from: usize, to: usize, instrs: &[Option], footprints: &HashMap) -> bool { // `to` must be po-order-later than `from` for the dependency to exist. if from >= to { return false; } + let Some(to_opcode) = instrs[to] else { return false }; + let touched = touched_by(from, to, instrs, footprints); // If any of the registers transitively touched by the first // instruction's register writes can feed into a memory address // used by the last we have an address dependency. - for reg in &footprints.get(&instrs[to]).unwrap().mem_addr_taints.registers { + for reg in &footprints.get(&to_opcode).unwrap().mem_addr_taints.registers { if touched.contains(reg) { return true; } @@ -297,14 +310,16 @@ pub fn addr_dep(from: usize, to: usize, instrs: &[B], footprints: &HashMa /// # Panics /// /// See `addr_dep` -pub fn data_dep(from: usize, to: usize, instrs: &[B], footprints: &HashMap) -> bool { +pub fn data_dep(from: usize, to: usize, instrs: &[Option], footprints: &HashMap) -> bool { if from >= to { return false; } + let Some(to_opcode) = instrs[to] else { return false }; + let touched = touched_by(from, to, instrs, footprints); - for reg in &footprints.get(&instrs[to]).unwrap().write_data_taints.registers { + for reg in &footprints.get(&to_opcode).unwrap().write_data_taints.registers { if touched.contains(reg) { return true; } @@ -318,18 +333,24 @@ pub fn data_dep(from: usize, to: usize, instrs: &[B], footprints: &HashMa /// /// See `addr_dep` #[allow(clippy::needless_range_loop)] -pub fn ctrl_dep(from: usize, to: usize, instrs: &[B], footprints: &HashMap) -> bool { +pub fn ctrl_dep(from: usize, to: usize, instrs: &[Option], footprints: &HashMap) -> bool { + let Some(from_opcode) = instrs[from] else { + return false; + }; + // `to` must be a program-order later load or store - let to_footprint = footprints.get(&instrs[from]).unwrap(); + let to_footprint = footprints.get(&from_opcode).unwrap(); if !(to_footprint.is_load || to_footprint.is_store) || (from >= to) { return false; } - let mut touched = footprints.get(&instrs[from]).unwrap().register_writes_tainted.clone(); + let mut touched = footprints.get(&from_opcode).unwrap().register_writes_tainted.clone(); let mut new_touched = Vec::new(); for i in (from + 1)..to { - let footprint = footprints.get(&instrs[i]).unwrap(); + let Some(opcode) = instrs[i] else { continue }; + + let footprint = footprints.get(&opcode).unwrap(); if footprint.is_branch { for reg in &footprint.branch_addr_taints.registers { @@ -387,17 +408,23 @@ fn advance_deps(footprint: &Footprint, touched: &mut HashSet) { } } -pub fn pick_dep(from: usize, to: usize, instrs: &[B], footprints: &HashMap) -> bool { - let to_footprint = footprints.get(&instrs[to]).unwrap(); +pub fn pick_dep(from: usize, to: usize, instrs: &[Option], footprints: &HashMap) -> bool { + let Some(from_opcode) = instrs[from] else { return false }; + + let Some(to_opcode) = instrs[to] else { return false }; + + let to_footprint = footprints.get(&to_opcode).unwrap(); if !(to_footprint.is_load || to_footprint.is_store) || (from >= to) { return false; } - let mut touched_before_pick = footprints.get(&instrs[from]).unwrap().register_writes_tainted.clone(); + let mut touched_before_pick = footprints.get(&from_opcode).unwrap().register_writes_tainted.clone(); let mut touched_after_pick = HashSet::new(); for i in (from + 1)..to { - let footprint = footprints.get(&instrs[i]).unwrap(); + let Some(opcode) = instrs[i] else { continue }; + + let footprint = footprints.get(&opcode).unwrap(); for (r_to, r_froms) in &footprint.register_pick_deps { for r_from in r_froms { diff --git a/isla-axiomatic/src/graph/graph_events.rs b/isla-axiomatic/src/graph/graph_events.rs index 680f954..1854070 100644 --- a/isla-axiomatic/src/graph/graph_events.rs +++ b/isla-axiomatic/src/graph/graph_events.rs @@ -338,10 +338,14 @@ impl GraphEvent { /// underlying axiomatic event. For display, we use the objdump /// output to find the human-readable assembly instruction pub fn from_axiomatic(ev: &AxEvent, objdump: &Objdump, value: Option) -> Self { - let instr = instruction_from_objdump(&format!("{:x}", ev.opcode), objdump); + let (instr, opcode) = if let Some(opcode) = ev.opcode { + (instruction_from_objdump(&format!("{:x}", opcode), objdump), format!("{:x}", opcode)) + } else { + (None, "none".to_string()) + }; GraphEvent { instr, - opcode: format!("{}", ev.opcode), + opcode, po: ev.instruction_index, iio: ev.intra_instruction_index, thread_id: ev.thread_id, diff --git a/isla-axiomatic/src/litmus.rs b/isla-axiomatic/src/litmus.rs index 2bdd22a..1237e36 100644 --- a/isla-axiomatic/src/litmus.rs +++ b/isla-axiomatic/src/litmus.rs @@ -553,7 +553,10 @@ pub fn parse_constrained(toml: &Value, symbolic_addrs: &HashMap) -> Result, String> { +pub fn parse_locations( + litmus_toml: &Value, + symbolic_addrs: &HashMap, +) -> Result, String> { let location_table = match litmus_toml.get("locations") { Some(value) => { value.as_table().ok_or_else(|| "[locations] must be a table of
= pairs".to_string())? @@ -697,9 +700,13 @@ fn parse_interrupt( type_info: &IRTypeInfo, isa: &ISAConfig, ) -> Result { - let at_str = value.get("at").ok_or_else(|| "Interrupt must have an 'at' field".to_string())?.as_str().ok_or_else(|| "Interrupt 'at' field must be a string")?; + let at_str = value + .get("at") + .ok_or_else(|| "Interrupt must have an 'at' field".to_string())? + .as_str() + .ok_or_else(|| "Interrupt 'at' field must be a string")?; let Some(at) = label_from_objdump(at_str, objdump) else { - return Err("Could not find interrupt 'at' label in threads".to_string()) + return Err("Could not find interrupt 'at' label in threads".to_string()); }; let reset = if let Some(value) = value.get("reset") { @@ -708,10 +715,7 @@ fn parse_interrupt( HashMap::default() }; - Ok(Interrupt { - at, - reset, - }) + Ok(Interrupt { at, reset }) } fn parse_thread_initialization( @@ -741,12 +745,15 @@ fn parse_thread_initialization( let interrupts = if let Some(value) = thread.get("interrupt") { let values = value.as_array().ok_or_else(|| "Thread interrupts must be an array of tables".to_string())?; - values.iter().map(|value| parse_interrupt(value, symbolic_addrs, objdump, symtab, type_info, isa)).collect::>()? + values + .iter() + .map(|value| parse_interrupt(value, symbolic_addrs, objdump, symtab, type_info, isa)) + .collect::>()? } else { Vec::new() }; - Ok(ThreadInit {inits, reset, interrupts}) + Ok(ThreadInit { inits, reset, interrupts }) } fn parse_self_modify_region(toml_region: &Value, objdump: &Objdump) -> Result, String> { diff --git a/isla-axiomatic/src/litmus/exp.rs b/isla-axiomatic/src/litmus/exp.rs index 7683562..275279d 100644 --- a/isla-axiomatic/src/litmus/exp.rs +++ b/isla-axiomatic/src/litmus/exp.rs @@ -33,11 +33,11 @@ use std::sync::Arc; use isla_lib::bitvector::BV; use isla_lib::error::ExecError; -use isla_lib::ir::{Name, Symtab, Reset, Val}; +use isla_lib::ir::{Name, Reset, Symtab, Val}; use isla_lib::memory::Memory; -use isla_lib::{primop, zencode}; use isla_lib::smt::Solver; use isla_lib::source_loc::SourceLoc; +use isla_lib::{primop, zencode}; use super::{label_from_objdump, Objdump}; use crate::page_table::{self, PageAttrs, S1PageAttrs, S2PageAttrs, TranslationTableWalk, VirtualAddress}; @@ -720,26 +720,16 @@ pub fn collect_locs<'litmus>(exp: &'litmus Exp, target: &mut HashSet<&'l EqLoc(loc, exp) => { target.insert(loc); collect_locs(exp, target); - }, - Loc(_) - | Label(_) - | True - | False - | Bin(_) - | Hex(_) - | Bits64(_, _) - | Nat(_) => (), - And(v) => - v.iter().for_each(|e| collect_locs(e, target)), - Or(v) => - v.iter().for_each(|e| collect_locs(e, target)), + } + Loc(_) | Label(_) | True | False | Bin(_) | Hex(_) | Bits64(_, _) | Nat(_) => (), + And(v) => v.iter().for_each(|e| collect_locs(e, target)), + Or(v) => v.iter().for_each(|e| collect_locs(e, target)), Not(e) => collect_locs(e, target), - App(_, args, kwargs) => - args.iter().chain(kwargs.values()).for_each(|e| collect_locs(e, target)), + App(_, args, kwargs) => args.iter().chain(kwargs.values()).for_each(|e| collect_locs(e, target)), Implies(lhs, rhs) => { collect_locs(lhs, target); collect_locs(rhs, target); - }, + } } } @@ -761,15 +751,13 @@ impl<'l, 's, 'ir, A: fmt::Display> fmt::Display for LocDisplay<'l, 's, 'ir, A> { use Loc::*; match self.loc { Register { reg, thread_id } => { - let unmangled= self.symtab.to_str_demangled(*reg); - let reg_name = - zencode::try_decode(unmangled) - .unwrap_or(unmangled.to_string()); + let unmangled = self.symtab.to_str_demangled(*reg); + let reg_name = zencode::try_decode(unmangled).unwrap_or(unmangled.to_string()); write!(f, "{}:{}", thread_id, reg_name) - }, - LastWriteTo { address , .. } => { + } + LastWriteTo { address, .. } => { write!(f, "{}", address) - }, + } } } } @@ -805,42 +793,46 @@ impl<'e, 's, 'ir, A: fmt::Display> fmt::Display for ExpDisplay<'e, 's, 'ir, A> { match self.exp { EqLoc(loc, val) => { write!(f, "{}={}", loc.display(self.symtab), val.display(self.symtab, self.exp.precedence())) - }, + } Loc(l) => { write!(f, "{}", l) - }, + } Label(l) => write!(f, "{}:", l), True => write!(f, "true"), False => write!(f, "false"), Bin(s) => write!(f, "{}", s), Hex(s) => write!(f, "{}", s), - Bits64(b,_) => write!(f, "{:x}", b), + Bits64(b, _) => write!(f, "{:x}", b), Nat(n) => write!(f, "{}", n), And(elems) => { let elems: Vec = - elems.iter().map(|e| format!("{}", e.display(self.symtab, e.precedence()))) - .collect(); + elems.iter().map(|e| format!("{}", e.display(self.symtab, e.precedence()))).collect(); write!(f, "{}", elems.join(" /\\ ")) - }, + } Or(elems) => { let elems: Vec = - elems.iter().map(|e| format!("{}", e.display(self.symtab, e.precedence()))) - .collect(); + elems.iter().map(|e| format!("{}", e.display(self.symtab, e.precedence()))).collect(); write!(f, "{}", elems.join(" \\/ ")) - }, + } Not(e) => { write!(f, "{}", e.display(self.symtab, self.exp.precedence())) - }, + } App(name, args, kwargs) => { - let args: Vec = - args.iter().map(|e| format!("{}", e.display(self.symtab, e.precedence()))) - .chain(kwargs.iter().map(|(kw,e)| format!("{}={}", kw, e.display(self.symtab, e.precedence())))) + let args: Vec = args + .iter() + .map(|e| format!("{}", e.display(self.symtab, e.precedence()))) + .chain(kwargs.iter().map(|(kw, e)| format!("{}={}", kw, e.display(self.symtab, e.precedence())))) .collect(); write!(f, "{}({})", name, args.join(", ")) - }, + } Implies(lhs, rhs) => { - write!(f, "{}-->{},", lhs.display(self.symtab, lhs.precedence()), rhs.display(self.symtab, rhs.precedence())) - }, + write!( + f, + "{}-->{},", + lhs.display(self.symtab, lhs.precedence()), + rhs.display(self.symtab, rhs.precedence()) + ) + } }?; if self.precedence > self.exp.precedence() { @@ -863,15 +855,7 @@ impl Exp { pub fn precedence(&self) -> usize { use Exp::*; match self { - Loc(_) - | EqLoc(_, _) - | Label(_) - | True - | False - | Bin(_) - | Hex(_) - | Bits64(_, _) - | Nat(_) => 0, + Loc(_) | EqLoc(_, _) | Label(_) | True | False | Bin(_) | Hex(_) | Bits64(_, _) | Nat(_) => 0, App(_, _, _) => 1, Not(_) => 2, And(_) => 3, @@ -879,4 +863,4 @@ impl Exp { Implies(_, _) => 5, } } -} \ No newline at end of file +} diff --git a/isla-axiomatic/src/page_table.rs b/isla-axiomatic/src/page_table.rs index a1e6226..2460935 100644 --- a/isla-axiomatic/src/page_table.rs +++ b/isla-axiomatic/src/page_table.rs @@ -560,14 +560,14 @@ impl Desc { Desc::Symbolic(init, mut maybe_bits, old_desc) => { maybe_bits.push(new_bits); Desc::Symbolic( - init, + init, maybe_bits, - Arc::new(move |solver| { - let v = old_desc(solver); - solver.choice(Var(v), bits64(new_bits, 64), SourceLoc::unknown()) - }), + Arc::new(move |solver| { + let v = old_desc(solver); + solver.choice(Var(v), bits64(new_bits, 64), SourceLoc::unknown()) + }), ) - }, + } } } diff --git a/isla-axiomatic/src/run_litmus.rs b/isla-axiomatic/src/run_litmus.rs index e1d2751..b27876a 100644 --- a/isla-axiomatic/src/run_litmus.rs +++ b/isla-axiomatic/src/run_litmus.rs @@ -608,14 +608,10 @@ where } for name in enums { - let members = arch - .shared_state - .type_info - .enums - .get(&name) - .ok_or_else(|| CallbackError::Internal( - format!("Failed to get enumeration '{}'", name) - ))?; + let members = + arch.shared_state.type_info.enums.get(&name).ok_or_else(|| { + CallbackError::Internal(format!("Failed to get enumeration '{}'", name)) + })?; let name = zencode::decode(arch.shared_state.symtab.to_str(name)); write!(&mut fd, "(declare-datatypes ((|{}| 0)) ((", name).map_err(internal_err)?; for member in members.iter() { diff --git a/isla-axiomatic/src/smt_events.rs b/isla-axiomatic/src/smt_events.rs index 2256dc9..a3899e3 100644 --- a/isla-axiomatic/src/smt_events.rs +++ b/isla-axiomatic/src/smt_events.rs @@ -171,15 +171,14 @@ fn read_initial_symbolic( }; let mut expr = { - let bv = - if let Some((region, concrete_addr)) = region_info { - match region.initial_value(concrete_addr, bytes) { - Some(bv) => bv, - None => B::new(0, 8 * bytes), - } - } else { - B::new(0, 8 * bytes) - }; + let bv = if let Some((region, concrete_addr)) = region_info { + match region.initial_value(concrete_addr, bytes) { + Some(bv) => bv, + None => B::new(0, 8 * bytes), + } + } else { + B::new(0, 8 * bytes) + }; let bv = Val::Bits(bv); Eq(Box::new(Literal(smt_bitvec(&sym))), Box::new(Literal(smt_bitvec(&bv)))) }; @@ -207,20 +206,19 @@ fn read_initial_concrete(bv: B, addr1: &Val, memory: &Memory, initi None }; - let mut expr = - if let Some((region, concrete_addr)) = region_info { - if Some(bv) == region.initial_value(concrete_addr, bv.len() / 8) { - True - } else { - False - } + let mut expr = if let Some((region, concrete_addr)) = region_info { + if Some(bv) == region.initial_value(concrete_addr, bv.len() / 8) { + True } else { - if bv.is_zero() { - True - } else { - False - } - }; + False + } + } else { + if bv.is_zero() { + True + } else { + False + } + }; for (addr2, value) in initial_addrs { let addr2 = Val::Bits(B::new(*addr2, 64)); @@ -313,12 +311,17 @@ fn ifetch_initial_opcode(ev: &AxEvent, litmus: &Litmus) -> Result(ev: &AxEvent, litmus: &Litmus) -> Sexp { use Sexp::*; + + let Some(opcode) = ev.opcode else { + return False; + }; + match ev.address() { Some(Val::Bits(addr)) => { - if let Some(opcode) = opcode_from_objdump(*addr, &litmus.objdump) { + if let Some(initial_opcode) = opcode_from_objdump(*addr, &litmus.objdump) { match ev.read_value() { - Some((Val::Symbolic(sym), _)) => Literal(format!("(= v{} {} {})", sym, opcode, ev.opcode)), - Some((Val::Bits(bv), _)) => Literal(format!("(= {} {} {})", bv, opcode, ev.opcode)), + Some((Val::Symbolic(sym), _)) => Literal(format!("(= v{} {} {})", sym, initial_opcode, opcode)), + Some((Val::Bits(bv), _)) => Literal(format!("(= {} {} {})", bv, initial_opcode, opcode)), _ => False, } } else { @@ -338,9 +341,11 @@ fn ifetch_match(ev: &AxEvent) -> Sexp { return False; } + let Some(opcode) = ev.opcode else { return False }; + match ev.read_value() { - Some((Val::Symbolic(sym), _)) => Literal(format!("(= v{} {})", sym, ev.opcode)), - Some((Val::Bits(bv), _)) => Literal(format!("(= {} {})", bv, ev.opcode)), + Some((Val::Symbolic(sym), _)) => Literal(format!("(= v{} {})", sym, opcode)), + Some((Val::Bits(bv), _)) => Literal(format!("(= {} {})", bv, opcode)), _ => False, } } @@ -421,7 +426,7 @@ where fn smt_dep_rel2( rel: DepRel, events: &[AxEvent], - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, ) -> Sexp { use Sexp::*; @@ -441,7 +446,7 @@ fn smt_dep_rel2( fn smt_dep_rel( rel: DepRel, events: &[AxEvent], - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, ) -> Sexp { use Sexp::*; diff --git a/isla-axiomatic/src/smt_relations.rs b/isla-axiomatic/src/smt_relations.rs index 2717212..1321efb 100644 --- a/isla-axiomatic/src/smt_relations.rs +++ b/isla-axiomatic/src/smt_relations.rs @@ -145,7 +145,7 @@ where fn dependency_rel( rel: relations::DepRel, events: &[AxEvent], - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, sexps: &mut SexpArena, ) -> SexpId { @@ -161,7 +161,7 @@ macro_rules! smt_basic_relation { pub fn $r( mode: RelationMode, events: &[AxEvent], - _: &[Vec], + _: &[Vec>], _: &HashMap, symtab: &mut Symtab, sexps: &mut SexpArena, @@ -178,7 +178,7 @@ macro_rules! smt_condition_relation { pub fn $r1( mode: RelationMode, events: &[AxEvent], - _: &[Vec], + _: &[Vec>], _: &HashMap, symtab: &mut Symtab, sexps: &mut SexpArena, @@ -195,7 +195,7 @@ macro_rules! smt_dependency_relation { pub fn $r( mode: RelationMode, events: &[AxEvent], - thread_opcodes: &[Vec], + thread_opcodes: &[Vec>], footprints: &HashMap, symtab: &mut Symtab, sexps: &mut SexpArena, diff --git a/isla-cat/src/smt.rs b/isla-cat/src/smt.rs index d4b0b67..34f9cf8 100644 --- a/isla-cat/src/smt.rs +++ b/isla-cat/src/smt.rs @@ -88,7 +88,7 @@ impl Sexp { Implies(sexp1, sexp2) | Eq(sexp1, sexp2) => { sexp1.modify(f); sexp2.modify(f) - }, + } IfThenElse(sexp1, sexp2, sexp3) => { sexp1.modify(f); sexp2.modify(f); diff --git a/isla-lib/src/executor.rs b/isla-lib/src/executor.rs index d3c6eda..43410db 100644 --- a/isla-lib/src/executor.rs +++ b/isla-lib/src/executor.rs @@ -582,7 +582,17 @@ fn assign<'ir, B: BV>( ) -> Result<(), ExecError> { let id = loc.id(); if local_state.should_probe(shared_state, &id) { - log_from!(tid, log::PROBE, &format!("Assigning {}[{:?}] <- {:?} at {}", loc_string(loc, &shared_state.symtab), id, v, info.location_string(shared_state.symtab.files()))) + log_from!( + tid, + log::PROBE, + &format!( + "Assigning {}[{:?}] <- {:?} at {}", + loc_string(loc, &shared_state.symtab), + id, + v, + info.location_string(shared_state.symtab.files()) + ) + ) } assign_with_accessor(loc, v, local_state, shared_state, solver, &mut Vec::new(), info) @@ -630,14 +640,18 @@ pub fn interrupt_pending<'ir, B: BV>( info: SourceLoc, ) -> Result { for interrupt in &task_state.interrupts { - let Some(Val::Bits(reg_value)) = frame.local_state.regs.get(interrupt.trigger_register, shared_state, solver, info)? else { - return Err(ExecError::BadInterrupt("trigger register does not exist, or does not have a concrete bitvector value")) + let Some(Val::Bits(reg_value)) = + frame.local_state.regs.get(interrupt.trigger_register, shared_state, solver, info)? + else { + return Err(ExecError::BadInterrupt( + "trigger register does not exist, or does not have a concrete bitvector value", + )); }; if *reg_value == interrupt.trigger_value { for (taken_task_id, taken_interrupt_id) in frame.taken_interrupts.iter().cloned() { if task_id == taken_task_id && interrupt.id == taken_interrupt_id { - return Ok(false) + return Ok(false); } } @@ -647,11 +661,19 @@ pub fn interrupt_pending<'ir, B: BV>( for (loc, reset) in &interrupt.reset { let value = reset(&frame.memory, shared_state.typedefs(), solver)?; let mut accessor = Vec::new(); - assign_with_accessor(loc, value.clone(), &mut frame.local_state, shared_state, solver, &mut accessor, info)?; + assign_with_accessor( + loc, + value.clone(), + &mut frame.local_state, + shared_state, + solver, + &mut accessor, + info, + )?; solver.add_event(Event::AssumeReg(loc.id(), accessor, value)); } - return Ok(true) + return Ok(true); } } @@ -1132,7 +1154,18 @@ fn run_loop<'ir, 'task, B: BV>( Instr::Call(loc, _, f, args, info) => { match shared_state.functions.get(f) { None => { - match run_special_primop(loc, *f, args, *info, tid, task_id, frame, task_state, shared_state, solver)? { + match run_special_primop( + loc, + *f, + args, + *info, + tid, + task_id, + frame, + task_state, + shared_state, + solver, + )? { SpecialResult::Continue => (), SpecialResult::Exit => return Ok(Run::Exit), } diff --git a/isla-lib/src/executor/frame.rs b/isla-lib/src/executor/frame.rs index d053eb6..14e9ac0 100644 --- a/isla-lib/src/executor/frame.rs +++ b/isla-lib/src/executor/frame.rs @@ -112,7 +112,7 @@ pub fn unfreeze_frame<'ir, B: BV>(frame: &Frame<'ir, B>) -> LocalFrame<'ir, B> { backtrace: (*frame.backtrace).clone(), function_assumptions: (*frame.function_assumptions).clone(), pc_counts: (*frame.pc_counts).clone(), - taken_interrupts: (*frame.taken_interrupts).clone() + taken_interrupts: (*frame.taken_interrupts).clone(), } } @@ -310,14 +310,11 @@ impl<'ir, B: BV> LocalFrame<'ir, B> { } pub fn set_probes(&mut self, shared_state: &SharedState<'ir, B>) { - let should_probe_here = - if shared_state.probe_functions.is_empty() { - true - } else { - self.backtrace - .iter() - .any(|(n,_)| shared_state.probe_functions.contains(n)) - }; + let should_probe_here = if shared_state.probe_functions.is_empty() { + true + } else { + self.backtrace.iter().any(|(n, _)| shared_state.probe_functions.contains(n)) + }; self.local_state.probes.probe_this_function = should_probe_here } diff --git a/isla-lib/src/ir.rs b/isla-lib/src/ir.rs index 43b8262..66a452d 100644 --- a/isla-lib/src/ir.rs +++ b/isla-lib/src/ir.rs @@ -46,7 +46,7 @@ use serde::{Deserialize, Serialize}; use std::collections::{BTreeMap, HashMap, HashSet}; use std::fmt; use std::hash::Hash; -use std::io::{Write, Error, ErrorKind}; +use std::io::{Error, ErrorKind, Write}; use std::sync::Arc; use crate::bitvector::{b64::B64, BV}; @@ -332,9 +332,9 @@ impl Val { } String(s) => write!(buf, "\"{}\"", s), Enum(EnumMember { enum_id, member }) => { - let members = shared_state.type_info.enums.get(&enum_id.to_name()).ok_or_else(|| + let members = shared_state.type_info.enums.get(&enum_id.to_name()).ok_or_else(|| { Error::new(ErrorKind::Other, format!("Failed to get enumeration '{}'", enum_id.to_name())) - )?; + })?; let name = zencode::decode(symtab.to_str(members[*member])); write!(buf, "|{}|", name) } diff --git a/isla-lib/src/probe.rs b/isla-lib/src/probe.rs index 2f420e3..ff44062 100644 --- a/isla-lib/src/probe.rs +++ b/isla-lib/src/probe.rs @@ -53,8 +53,7 @@ pub fn taint_info(log_type: u32, sym: Sym, shared_state: Option<&SharedSt .map(|(reg, _)| { if let Some(shared_state) = shared_state { let sym = shared_state.symtab.to_str(*reg); - zencode::try_decode(sym) - .unwrap_or(sym.to_string()) + zencode::try_decode(sym).unwrap_or(sym.to_string()) } else { format!("{:?}", reg) } @@ -72,12 +71,13 @@ pub fn args_info(tid: usize, args: &[Val], shared_state: &SharedState< for arg in args { for sym in arg.symbolic_variables() { let Taints { registers, memory } = references.taints(sym, &events); - let registers: Vec = - registers.iter().map(|(reg, _)| { + let registers: Vec = registers + .iter() + .map(|(reg, _)| { let sym = shared_state.symtab.to_str(*reg); - zencode::try_decode(sym) - .unwrap_or(sym.to_string()) - }).collect(); + zencode::try_decode(sym).unwrap_or(sym.to_string()) + }) + .collect(); let memory = if memory { ", MEMORY" } else { "" }; log_from!(tid, log::PROBE, &format!("Symbol {} taints: {:?}{}", sym, registers, memory)) } diff --git a/isla-lib/src/simplify.rs b/isla-lib/src/simplify.rs index 23d6592..f6856b7 100644 --- a/isla-lib/src/simplify.rs +++ b/isla-lib/src/simplify.rs @@ -34,7 +34,7 @@ use std::borrow::{Borrow, BorrowMut, Cow}; use std::cmp::Ordering; use std::collections::{HashMap, HashSet}; -use std::io::{Write, Error, ErrorKind}; +use std::io::{Error, ErrorKind, Write}; use crate::bitvector::{write_bits64, BV}; use crate::ir::{BitsSegment, Loc, Name, SharedState, Symtab, Val, HAVE_EXCEPTION}; @@ -1384,9 +1384,9 @@ fn write_exp( Bits(bv) => write_bits(buf, bv), Bits64(bv) => write_bits64(buf, bv.lower_u64(), bv.len()), Enum(e) => { - let members = shared_state.type_info.enums.get(&e.enum_id.to_name()).ok_or_else(|| + let members = shared_state.type_info.enums.get(&e.enum_id.to_name()).ok_or_else(|| { Error::new(ErrorKind::Other, format!("Failed to get enumeration '{}'", e.enum_id.to_name())) - )?; + })?; let name = zencode::decode(shared_state.symtab.to_str(members[e.member])); write!(buf, "|{}|", name) } @@ -1738,9 +1738,9 @@ pub fn write_events_in_context( } Def::DefineEnum(name, size) => { if !opts.just_smt { - let members = shared_state.type_info.enums.get(name).ok_or_else(|| + let members = shared_state.type_info.enums.get(name).ok_or_else(|| { Error::new(ErrorKind::Other, format!("Failed to get enumeration '{}'", name)) - )?; + })?; let members = members .iter() .map(|constr| zencode::decode(shared_state.symtab.to_str(*constr))) diff --git a/isla-lib/src/smt.rs b/isla-lib/src/smt.rs index 021dd6c..b87e9fb 100644 --- a/isla-lib/src/smt.rs +++ b/isla-lib/src/smt.rs @@ -1911,7 +1911,6 @@ pub unsafe fn finalize_solver() { Z3_finalize_memory() } - pub fn z3_version() -> String { let cs; unsafe { diff --git a/isla-mml/src/accessor.rs b/isla-mml/src/accessor.rs index 1bca300..770d352 100644 --- a/isla-mml/src/accessor.rs +++ b/isla-mml/src/accessor.rs @@ -55,7 +55,7 @@ pub trait ModelEvent<'ev, B> { fn index_set(&self) -> Option; - fn opcode(&self) -> B; + fn opcode(&self) -> Option; } #[derive(Debug)] @@ -177,9 +177,11 @@ macro_rules! access_extension { } impl<'ev, B: BV> View<'ev, B> { - fn new(opcode: B) -> Self { + fn new(opcode: Option) -> Self { let mut view = Self::default(); - view.special.insert("opcode".to_string(), AccessorVal::Bits(opcode)); + if let Some(opcode) = opcode { + view.special.insert("opcode".to_string(), AccessorVal::Bits(opcode)); + } view } @@ -394,7 +396,7 @@ pub fn infer_accessor_type(accessors: &[Accessor], sexps: &mut SexpArena) -> Sex } } -fn event_view<'ev, B: BV>(ev: &'ev Event, opcode: B, shared_state: &SharedState) -> Option> { +fn event_view<'ev, B: BV>(ev: &'ev Event, opcode: Option, shared_state: &SharedState) -> Option> { match ev { Event::ReadMem { address, value, read_kind, .. } => Some( View::new(opcode) diff --git a/isla-mml/src/smt.rs b/isla-mml/src/smt.rs index 3819ba1..579ad67 100644 --- a/isla-mml/src/smt.rs +++ b/isla-mml/src/smt.rs @@ -324,9 +324,9 @@ impl Sexp { } }, Sexp::Enum(e) => { - let members = typedefs.enums.get(&e.enum_id.to_name()).ok_or_else(|| + let members = typedefs.enums.get(&e.enum_id.to_name()).ok_or_else(|| { io::Error::new(io::ErrorKind::Other, format!("Failed to get enumeration '{}'", e.enum_id.to_name())) - )?; + })?; let name = zencode::decode(typedefs.symtab.to_str(members[e.member])); write!(buf, "{}", name) } diff --git a/src/axiomatic.rs b/src/axiomatic.rs index 95a4634..eebfe4d 100644 --- a/src/axiomatic.rs +++ b/src/axiomatic.rs @@ -47,9 +47,9 @@ use isla_axiomatic::graph::{ GraphValueNames, }; -use isla_axiomatic::axiomatic::{FinalLocValuesError, final_state_from_z3_output}; +use isla_axiomatic::axiomatic::{final_state_from_z3_output, FinalLocValuesError}; +use isla_axiomatic::litmus::exp::{collect_locs, Loc as LitmusLoc}; use isla_axiomatic::litmus::Litmus; -use isla_axiomatic::litmus::exp::{Loc as LitmusLoc, collect_locs}; use isla_axiomatic::page_table::{name_initial_walk_bitvectors, VirtualAddress}; use isla_axiomatic::run_litmus; use isla_axiomatic::run_litmus::{LitmusRunOpts, PCLimitMode}; @@ -75,8 +75,7 @@ fn main() { process::exit(code) } -type FinalState = - HashMap, Val>; +type FinalState = HashMap, Val>; #[derive(Debug)] enum AxResult { @@ -719,17 +718,19 @@ fn isla_main() -> i32 { get_z3_model, cache, &|exec, memory, all_addrs, tables, footprints, z3_output| { - let final_state: Option = - if get_z3_model { - final_state_from_z3_output(&litmus, &exec, &final_assertion_locs, z3_output) + let final_state: Option = if get_z3_model { + final_state_from_z3_output(&litmus, &exec, &final_assertion_locs, z3_output) .map(Some) .unwrap_or_else(|e| { - log!(log::VERBOSE, format!("warning: failed to get final state for execution: {}", e)); + log!( + log::VERBOSE, + format!("warning: failed to get final state for execution: {}", e) + ); None }) - } else { - None - }; + } else { + None + }; let mut names = GraphValueNames { s1_ptable_names: HashMap::new(), @@ -838,7 +839,14 @@ fn isla_main() -> i32 { "{}", err.source_loc().message(source_path.as_ref(), symtab.files(), &msg, true, true) ); - print_results(print_like_herd7, &litmus, shared_state, now, &[Error(None, "".to_string())], ref_result); + print_results( + print_like_herd7, + &litmus, + shared_state, + now, + &[Error(None, "".to_string())], + ref_result, + ); continue; } @@ -1046,10 +1054,10 @@ fn print_results_herd7<'ir>( print!("{}={};", r.display(&shared_state.symtab), v.to_string(shared_state)); } println!(); - }, + } None => { println!("???;"); - }, + } } } @@ -1069,7 +1077,10 @@ fn print_results_herd7<'ir>( println!("Witnesses"); println!("Positive: {} Negative: {}", positive, negative); - println!("Condition exists {}", litmus.final_assertion.display(&shared_state.symtab, litmus.final_assertion.precedence())); + println!( + "Condition exists {}", + litmus.final_assertion.display(&shared_state.symtab, litmus.final_assertion.precedence()) + ); println!("Observation {} {} {} {}", litmus.name, condition, positive, negative); if let Some(hash) = &litmus.hash { @@ -1113,15 +1124,14 @@ fn print_results_herd7<'ir>( "\x1b[91m\x1b[1merror\x1b[0m" }; let count = format!("{} of {}", positive, results.len()); - let prefix = - format!( - "{} {} ({}) reference: {} {}ms ", - litmus.name, - got.map(AxResult::short_name).unwrap_or("error"), - count, - reference.short_name(), - start_time.elapsed().as_millis() - ); + let prefix = format!( + "{} {} ({}) reference: {} {}ms ", + litmus.name, + got.map(AxResult::short_name).unwrap_or("error"), + count, + reference.short_name(), + start_time.elapsed().as_millis() + ); eprintln!("{:.<100} {}", prefix, status); } } diff --git a/src/opts.rs b/src/opts.rs index eac000d..92c91e4 100644 --- a/src/opts.rs +++ b/src/opts.rs @@ -47,9 +47,9 @@ use isla_lib::ir::partial_linearize; use isla_lib::ir::serialize::{read_serialized_architecture, DeserializedArchitecture, SerializationError}; use isla_lib::ir::*; use isla_lib::ir_parser; -use isla_lib::smt::z3_version; use isla_lib::log; use isla_lib::primop_util::symbolic_from_typedefs; +use isla_lib::smt::z3_version; use isla_lib::smt_parser; use isla_lib::source_loc::SourceLoc; use isla_lib::value_parser;