Add support for interrupts in tests

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

isla-axiomatic/src/litmus.rs

@@ -683,7 +683,36 @@ pub fn parse_reset_registers<B: BV>(
     }
 }
 
-type ThreadInit = (Vec<(Name, u64)>, HashMap<Loc<Name>, exp::Exp<String>>);
+struct ThreadInit {
+    inits: Vec<(Name, u64)>,
+    reset: HashMap<Loc<Name>, exp::Exp<String>>,
+    interrupts: Vec<Interrupt>,
+}
+
+fn parse_interrupt<B: BV>(
+    value: &Value,
+    symbolic_addrs: &HashMap<String, u64>,
+    objdump: &Objdump,
+    symtab: &Symtab,
+    type_info: &IRTypeInfo,
+    isa: &ISAConfig<B>,
+) -> Result<Interrupt, 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())
+    };
+
+    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<B: BV>(
     thread: &Value,
@@ -693,7 +722,7 @@ fn parse_thread_initialization<B: BV>(
     type_info: &IRTypeInfo,
     isa: &ISAConfig<B>,
 ) -> Result<ThreadInit, String> {
-    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<B: BV>(
         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::<Result<_, _>>()?
+    } else {
+        Vec::new()
+    };
+
+    Ok(ThreadInit {inits, reset, interrupts})
 }
 
 fn parse_self_modify_region<B: BV>(toml_region: &Value, objdump: &Objdump) -> Result<Region<B>, 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<Loc<Name>, exp::Exp<String>>,
+}
+
 #[derive(Clone)]
 pub struct AssembledThread {
     pub name: ThreadName,
     pub address: u64,
     pub inits: Vec<(Name, u64)>,
     pub reset: HashMap<Loc<Name>, exp::Exp<String>>,
+    pub interrupts: Vec<Interrupt>,
     pub code: Vec<u8>,
     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<B: BV> Litmus<B> {
         let threads: Vec<Thread> = 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::<Result<_, String>>()?;
 
@@ -1110,4 +1161,4 @@ impl<B: BV> Litmus<B> {
 
         name
     }
-}
+}

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 {

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),
         }
     }
 }

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<B: BV>(exp: smtlib::Exp<Sym>, solver: &mut Solver<B>) -> Res
     Ok(v)
 }
 
+pub fn interrupt_pending<'ir, B: BV>(
+    tid: usize,
+    task_id: TaskId,
+    frame: &mut LocalFrame<'ir, B>,
+    task_state: &TaskState<B>,
+    shared_state: &SharedState<'ir, B>,
+    solver: &mut Solver<B>,
+    info: SourceLoc,
+) -> Result<bool, ExecError> {
+    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<Name>],
     info: SourceLoc,
     tid: usize,
+    task_id: TaskId,
     frame: &mut LocalFrame<'ir, B>,
     task_state: &TaskState<B>,
     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),
                         }

isla-lib/src/executor/frame.rs

@@ -95,6 +95,7 @@ pub struct Frame<'ir, B> {
     pub(super) backtrace: Arc<Backtrace>,
     pub(super) function_assumptions: Arc<HashMap<Name, Vec<(Vec<Val<B>>, Val<B>)>>>,
     pub(super) pc_counts: Arc<HashMap<B, usize>>,
+    pub(super) taken_interrupts: Arc<Vec<(TaskId, u8)>>,
 }
 
 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<Name, Vec<(Vec<Val<B>>, Val<B>)>>,
     pub(super) pc_counts: HashMap<B, usize>,
+    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(),
         }
     }
 

isla-lib/src/executor/task.rs

@@ -59,6 +59,19 @@ impl TaskId {
     }
 }
 
+pub struct TaskInterrupt<B> {
+    pub(super) id: u8,
+    pub(super) trigger_register: Name,
+    pub(super) trigger_value: B,
+    pub(super) reset: HashMap<Loc<Name>, Reset<B>>,
+}
+
+impl<B> TaskInterrupt<B> {
+    pub fn new(id: u8, trigger_register: Name, trigger_value: B, reset: HashMap<Loc<Name>, Reset<B>>) -> Self {
+        TaskInterrupt { id, trigger_register, trigger_value, reset }
+    }
+}
+
 pub struct TaskState<B> {
     pub(super) reset_registers: HashMap<Loc<Name>, Reset<B>>,
     // We might want to avoid loops in the assembly by requiring that
@@ -68,11 +81,12 @@ pub struct TaskState<B> {
     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<TaskInterrupt<B>>,
 }
 
 impl<B> TaskState<B> {
     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<Loc<Name>, Reset<B>>) -> Self {
@@ -86,6 +100,11 @@ impl<B> TaskState<B> {
     pub fn with_zero_announce_exit(self, b: bool) -> Self {
         TaskState { zero_announce_exit: b, ..self }
     }
+
+    pub fn add_interrupt(&mut self, interrupt: TaskInterrupt<B>) -> &mut Self {
+        self.interrupts.push(interrupt);
+        self
+    }
 }
 
 impl<B> Default for TaskState<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<B: BV>(
                     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" {