From fbcc49d5c78f2c51aafbf3e654fcc08081c4934c Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 26 Jun 2024 19:11:51 +0100 Subject: [PATCH] Add support for interrupts in tests --- configs/armv9p4.toml | 2 + isla-axiomatic/src/litmus.rs | 67 ++++++++++++++++++++++++++++---- isla-axiomatic/src/run_litmus.rs | 16 +++++++- isla-lib/src/error.rs | 2 + isla-lib/src/executor.rs | 48 ++++++++++++++++++++++- isla-lib/src/executor/frame.rs | 5 +++ isla-lib/src/executor/task.rs | 21 +++++++++- isla-lib/src/ir.rs | 8 ++++ isla-sail/sail_plugin_isla.ml | 7 ++-- 9 files changed, 160 insertions(+), 16 deletions(-) diff --git a/configs/armv9p4.toml b/configs/armv9p4.toml index bfcf23f..103c6e5 100644 --- a/configs/armv9p4.toml +++ b/configs/armv9p4.toml @@ -183,6 +183,7 @@ ignore = [ "EDESR" = "{ bits = 0x00000000 }" "EDECR" = "{ bits = 0x00000000 }" +"CPACR_EL1" = "{ bits = 0x0000000000000000 }" # Avoid some extra complication "FEAT_TME_IMPLEMENTED" = false @@ -214,6 +215,7 @@ ignore = [ # (it's set to UNKNOWN on reset) "MDCR_EL2" = "{ bits = 0x00000000 }" +"PSTATE.nRW" = "0b0" # A map from register names that may appear in litmus files to Sail # register names diff --git a/isla-axiomatic/src/litmus.rs b/isla-axiomatic/src/litmus.rs index 0a776a7..2bdd22a 100644 --- a/isla-axiomatic/src/litmus.rs +++ b/isla-axiomatic/src/litmus.rs @@ -683,7 +683,36 @@ pub fn parse_reset_registers( } } -type ThreadInit = (Vec<(Name, u64)>, HashMap, exp::Exp>); +struct ThreadInit { + inits: Vec<(Name, u64)>, + reset: HashMap, exp::Exp>, + interrupts: Vec, +} + +fn parse_interrupt( + value: &Value, + symbolic_addrs: &HashMap, + objdump: &Objdump, + symtab: &Symtab, + 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 Some(at) = label_from_objdump(at_str, objdump) else { + return Err("Could not find interrupt 'at' label in threads".to_string()) + }; + + let reset = if let Some(value) = value.get("reset") { + parse_reset_registers(value, symbolic_addrs, symtab, type_info, isa)? + } else { + HashMap::default() + }; + + Ok(Interrupt { + at, + reset, + }) +} fn parse_thread_initialization( thread: &Value, @@ -693,7 +722,7 @@ fn parse_thread_initialization( type_info: &IRTypeInfo, isa: &ISAConfig, ) -> Result { - let init = if let Some(value) = thread.get("init") { + let inits = if let Some(value) = thread.get("init") { let table = value.as_table().ok_or_else(|| "Thread init must be a list of register name/value pairs".to_string())?; table @@ -710,7 +739,14 @@ fn parse_thread_initialization( HashMap::new() }; - Ok((init, reset)) + 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::>()? + } else { + Vec::new() + }; + + Ok(ThreadInit {inits, reset, interrupts}) } fn parse_self_modify_region(toml_region: &Value, objdump: &Objdump) -> Result, String> { @@ -796,12 +832,19 @@ where error.map_location(|pos| PageSetupLocation::new(source, pos)).to_string() } +#[derive(Clone)] +pub struct Interrupt { + pub at: u64, + pub reset: HashMap, exp::Exp>, +} + #[derive(Clone)] pub struct AssembledThread { pub name: ThreadName, pub address: u64, pub inits: Vec<(Name, u64)>, pub reset: HashMap, exp::Exp>, + pub interrupts: Vec, pub code: Vec, pub source: String, } @@ -849,6 +892,13 @@ impl Thread { Thread::IR(t) => &t.inits, } } + + pub fn interrupts(&self) -> &[Interrupt] { + match self { + Thread::Assembled(t) => &t.interrupts, + Thread::IR(_) => &[], + } + } } #[derive(Debug, Clone)] @@ -1002,20 +1052,21 @@ impl Litmus { let threads: Vec = thread_bodies .drain(..) .zip(inits.drain(..)) - .map(|((name, body), (inits, reset))| match body { + .map(|((name, body), init)| match body { ThreadBody::Code(source) => { let (address, code) = assembled.remove(&name).ok_or(format!("Thread {} was not found in assembled threads", name))?; Ok(Thread::Assembled(AssembledThread { name, address, - inits, - reset, + inits: init.inits, + reset: init.reset, + interrupts: init.interrupts, code, source: source.to_string(), })) } - ThreadBody::Call(call) => Ok(Thread::IR(IRThread { name, inits, reset, call })), + ThreadBody::Call(call) => Ok(Thread::IR(IRThread { name, inits: init.inits, reset: init.reset, call })), }) .collect::>()?; @@ -1110,4 +1161,4 @@ impl Litmus { name } -} \ No newline at end of file +} diff --git a/isla-axiomatic/src/run_litmus.rs b/isla-axiomatic/src/run_litmus.rs index 2da6246..e1d2751 100644 --- a/isla-axiomatic/src/run_litmus.rs +++ b/isla-axiomatic/src/run_litmus.rs @@ -43,7 +43,7 @@ use std::time::Instant; use isla_lib::bitvector::BV; use isla_lib::error::{ExecError, IslaError}; use isla_lib::executor; -use isla_lib::executor::{LocalFrame, TaskId, TaskState, TraceError}; +use isla_lib::executor::{LocalFrame, TaskId, TaskInterrupt, TaskState, TraceError}; use isla_lib::ir::*; use isla_lib::memory::Memory; use isla_lib::simplify; @@ -276,8 +276,20 @@ where .iter() .map(|(loc, exp)| (loc.clone(), reset_eval(exp, all_addrs, &litmus.objdump))) .collect(); - let task_state = + + let mut task_state = TaskState::new().with_reset_registers(reset).with_zero_announce_exit(isa_config.zero_announce_exit); + + for (n, interrupt) in thread.interrupts().iter().enumerate() { + let reset = interrupt + .reset + .iter() + .map(|(loc, exp)| (loc.clone(), reset_eval(exp, all_addrs, &litmus.objdump))) + .collect(); + log!(log::LITMUS, &format!("Adding interrupt at {:x}", interrupt.at)); + task_state.add_interrupt(TaskInterrupt::new(n as u8, isa_config.pc, B::from_u64(interrupt.at), reset)); + } + if let Some(limit) = opts.pc_limit { task_state.with_pc_limit(isa_config.pc, limit) } else { diff --git a/isla-lib/src/error.rs b/isla-lib/src/error.rs index 1d64f58..18bcb77 100644 --- a/isla-lib/src/error.rs +++ b/isla-lib/src/error.rs @@ -85,6 +85,7 @@ pub enum ExecError { Stopped(String), PCLimitReached(u64), InconsistentRegisterReset, + BadInterrupt(&'static str), } impl IslaError for ExecError { @@ -128,6 +129,7 @@ impl fmt::Display for ExecError { Stopped(func) => write!(f, "Execution stopped at {}", func), PCLimitReached(pc_value) => write!(f, "Executed instruction at {} more than specified limit", pc_value), InconsistentRegisterReset => write!(f, "Inconsistent register reset constraints"), + BadInterrupt(msg) => write!(f, "Bad task interrupt: {}", msg), } } } diff --git a/isla-lib/src/executor.rs b/isla-lib/src/executor.rs index a5fae17..d3c6eda 100644 --- a/isla-lib/src/executor.rs +++ b/isla-lib/src/executor.rs @@ -61,7 +61,7 @@ mod task; pub use frame::{freeze_frame, unfreeze_frame, Backtrace, Frame, LocalFrame, LocalState}; use frame::{pop_call_stack, push_call_stack}; -pub use task::{StopAction, StopConditions, Task, TaskId, TaskState}; +pub use task::{StopAction, StopConditions, Task, TaskId, TaskInterrupt, TaskState}; /// Gets a value from a variable `Bindings` map. Note that this function is set up to handle the /// following case: @@ -620,6 +620,45 @@ fn smt_exp_to_value(exp: smtlib::Exp, solver: &mut Solver) -> Res Ok(v) } +pub fn interrupt_pending<'ir, B: BV>( + tid: usize, + task_id: TaskId, + frame: &mut LocalFrame<'ir, B>, + task_state: &TaskState, + shared_state: &SharedState<'ir, B>, + solver: &mut Solver, + 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")) + }; + + 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) + } + } + + frame.taken_interrupts.push((task_id, interrupt.id)); + + log_from!(tid, log::VERBOSE, "Injecting pending interrupt"); + 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)?; + solver.add_event(Event::AssumeReg(loc.id(), accessor, value)); + } + + return Ok(true) + } + } + + // No interrupts were pending + Ok(false) +} + pub fn reset_registers<'ir, B: BV>( _tid: usize, frame: &mut LocalFrame<'ir, B>, @@ -773,6 +812,7 @@ fn run_special_primop<'ir, B: BV>( args: &[Exp], info: SourceLoc, tid: usize, + task_id: TaskId, frame: &mut LocalFrame<'ir, B>, task_state: &TaskState, shared_state: &SharedState<'ir, B>, @@ -809,6 +849,10 @@ fn run_special_primop<'ir, B: BV>( frame.regs_mut().synchronize(); assign(tid, loc, Val::Unit, &mut frame.local_state, shared_state, solver, info)?; frame.pc += 1 + } else if f == INTERRUPT_PENDING { + let pending = interrupt_pending(tid, task_id, frame, task_state, shared_state, solver, info)?; + assign(tid, loc, Val::Bool(pending), &mut frame.local_state, shared_state, solver, info)?; + frame.pc += 1 } else if f == ITE_PHI { let mut true_value = None; let mut symbolics = Vec::new(); @@ -1088,7 +1132,7 @@ 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, 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 b03f141..d053eb6 100644 --- a/isla-lib/src/executor/frame.rs +++ b/isla-lib/src/executor/frame.rs @@ -95,6 +95,7 @@ pub struct Frame<'ir, B> { pub(super) backtrace: Arc, pub(super) function_assumptions: Arc>, Val)>>>, pub(super) pc_counts: Arc>, + pub(super) taken_interrupts: Arc>, } pub fn unfreeze_frame<'ir, B: BV>(frame: &Frame<'ir, B>) -> LocalFrame<'ir, B> { @@ -111,6 +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() } } @@ -130,6 +132,7 @@ pub struct LocalFrame<'ir, B> { pub(super) backtrace: Backtrace, pub(super) function_assumptions: HashMap>, Val)>>, pub(super) pc_counts: HashMap, + pub(super) taken_interrupts: Vec<(TaskId, u8)>, } pub fn freeze_frame<'ir, B: BV>(frame: &LocalFrame<'ir, B>) -> Frame<'ir, B> { @@ -146,6 +149,7 @@ pub fn freeze_frame<'ir, B: BV>(frame: &LocalFrame<'ir, B>) -> Frame<'ir, B> { backtrace: Arc::new(frame.backtrace.clone()), function_assumptions: Arc::new(frame.function_assumptions.clone()), pc_counts: Arc::new(frame.pc_counts.clone()), + taken_interrupts: Arc::new(frame.taken_interrupts.clone()), } } @@ -264,6 +268,7 @@ impl<'ir, B: BV> LocalFrame<'ir, B> { backtrace: Vec::new(), function_assumptions: HashMap::new(), pc_counts: HashMap::new(), + taken_interrupts: Vec::new(), } } diff --git a/isla-lib/src/executor/task.rs b/isla-lib/src/executor/task.rs index 73c08d7..0832185 100644 --- a/isla-lib/src/executor/task.rs +++ b/isla-lib/src/executor/task.rs @@ -59,6 +59,19 @@ impl TaskId { } } +pub struct TaskInterrupt { + pub(super) id: u8, + pub(super) trigger_register: Name, + pub(super) trigger_value: B, + pub(super) reset: HashMap, Reset>, +} + +impl TaskInterrupt { + pub fn new(id: u8, trigger_register: Name, trigger_value: B, reset: HashMap, Reset>) -> Self { + TaskInterrupt { id, trigger_register, trigger_value, reset } + } +} + pub struct TaskState { pub(super) reset_registers: HashMap, Reset>, // We might want to avoid loops in the assembly by requiring that @@ -68,11 +81,12 @@ pub struct TaskState { pub(super) pc_limit: Option<(Name, usize)>, // Exit if we ever announce an instruction with all bits set to zero pub(super) zero_announce_exit: bool, + pub(super) interrupts: Vec>, } impl TaskState { pub fn new() -> Self { - TaskState { reset_registers: HashMap::new(), pc_limit: None, zero_announce_exit: true } + TaskState { reset_registers: HashMap::new(), pc_limit: None, zero_announce_exit: true, interrupts: Vec::new() } } pub fn with_reset_registers(self, reset_registers: HashMap, Reset>) -> Self { @@ -86,6 +100,11 @@ impl TaskState { pub fn with_zero_announce_exit(self, b: bool) -> Self { TaskState { zero_announce_exit: b, ..self } } + + pub fn add_interrupt(&mut self, interrupt: TaskInterrupt) -> &mut Self { + self.interrupts.push(interrupt); + self + } } impl Default for TaskState { diff --git a/isla-lib/src/ir.rs b/isla-lib/src/ir.rs index 851d323..43b8262 100644 --- a/isla-lib/src/ir.rs +++ b/isla-lib/src/ir.rs @@ -757,6 +757,11 @@ pub const INSTR_ANNOUNCE: Name = Name { id: 22 }; /// [REGISTER_INIT] is a name used in backtraces when evaluating a register initialiser pub const REGISTER_INIT: Name = Name { id: 23 }; +/// [INTERRUPT_PENDING] is a special function that checks if the task +/// has any pending interrupts (which are usually specified in the +/// test file). +pub const INTERRUPT_PENDING: Name = Name { id: 24 }; + static GENSYM: &str = "zzUGENSYMzU"; impl<'ir> Symtab<'ir> { @@ -870,6 +875,7 @@ impl<'ir> Symtab<'ir> { symtab.intern_constant(WRITE_REGISTER_FROM_VECTOR, "zwrite_register_from_vector"); symtab.intern_constant(INSTR_ANNOUNCE, "zplatform_instr_announce"); symtab.intern_constant(REGISTER_INIT, "zzUregister_initzU"); + symtab.intern_constant(INTERRUPT_PENDING, "interrupt_pending"); symtab } @@ -1157,6 +1163,8 @@ fn insert_instr_primops( Instr::Call(loc.clone(), false, REG_DEREF, args.clone(), *info) } else if name == "reset_registers" { Instr::Call(loc.clone(), false, RESET_REGISTERS, args.clone(), *info) + } else if name == "interrupt_pending" { + Instr::Call(loc.clone(), false, INTERRUPT_PENDING, args.clone(), *info) } else if name == "read_register_from_vector" { Instr::Call(loc.clone(), false, READ_REGISTER_FROM_VECTOR, args.clone(), *info) } else if name == "write_register_from_vector" { diff --git a/isla-sail/sail_plugin_isla.ml b/isla-sail/sail_plugin_isla.ml index 36182e4..d4cb6fa 100644 --- a/isla-sail/sail_plugin_isla.ml +++ b/isla-sail/sail_plugin_isla.ml @@ -52,6 +52,7 @@ open Libsail open Ast open Ast_util +open Interactive.State open Jib open Jib_util @@ -290,7 +291,7 @@ let remove_casts cdefs = let cdefs = List.map (fun cdef -> cdef_concatmap_instr remove_instr_casts cdef) cdefs in let vals = List.map (fun (fid, (ctyp_from, ctyp_to)) -> - CDEF_aux (CDEF_val (mk_id fid, Some fid, [ctyp_from], ctyp_to), mk_def_annot Parse_ast.Unknown) + CDEF_aux (CDEF_val (mk_id fid, Some fid, [ctyp_from], ctyp_to), mk_def_annot Parse_ast.Unknown ()) ) (StringMap.bindings !conversions) in vals @ cdefs @@ -331,13 +332,13 @@ let fix_cons cdefs = let cdef = cdef_map_instr (collect_cons_ctyps list_ctyps) cdef in let vals = List.map (fun ctyp -> - CDEF_aux (CDEF_val (cons_name ctyp, Some "cons", [ctyp; CT_list ctyp], CT_list ctyp), mk_def_annot Parse_ast.Unknown) + CDEF_aux (CDEF_val (cons_name ctyp, Some "cons", [ctyp; CT_list ctyp], CT_list ctyp), mk_def_annot Parse_ast.Unknown ()) ) (CTSet.elements (CTSet.diff !list_ctyps !all_list_ctyps)) in vals @ [cdef] ) cdefs |> List.concat -let isla_target _ _ out_file ast effect_info env = +let isla_target out_file { ast; effect_info; env; _ } = let out_file = match out_file with Some out_file -> out_file ^ ".ir" | None -> "out.ir" in let props = Property.find_properties ast in Bindings.bindings props |> List.map fst |> IdSet.of_list |> Specialize.add_initial_calls;