Update Isla for exceptions

- Support data dependencies into system register writes

- Allow multiple axiomatic model variants to be defined on a single line

configs/armv9p4.toml

@@ -8,7 +8,7 @@ translation_function = "AArch64_TranslateAddress"
 # bit to set to inject an interrupt.
 interrupt_status_bit = "ISR_EL1.I"
 
-in_program_order = ["sail_barrier", "sail_cache_op", "sail_take_exception", "sail_return_exception", "sail_tlbi"]
+in_program_order = ["sail_barrier", "sail_cache_op", "sail_take_exception", "sail_return_exception", "sail_tlbi", "sail_system_register_write"]
 
 # litmus variables have type uint32_t by default
 default_sizeof = 4
@@ -233,8 +233,9 @@ ignore = [
 # These registers are set during symbolic execution by the special builtin "reset_registers"
 [registers.reset]
 # Bit 1 being unset allows unaligned accesses
+# Bit 9 being set allows DAIF bits to be set at EL0
 # Bit 26 being set allows cache-maintenance ops in EL0
-"SCTLR_EL1" = "{ bits = 0x0000000004000000 }"
+"SCTLR_EL1" = "{ bits = 0x0000000004000200 }"
 "CNTCR" = "{ bits = 0x00000000 }"
 # Set above, but ENABLE might be reset to UNKNOWN
 "CNTHP_CTL_EL2" = "{ bits = 0x0000000000000000 }"

isla-axiomatic/src/axiomatic.rs

@@ -1033,7 +1033,7 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> {
 
 #[derive(Debug)]
 pub enum FinalLocValuesError<'l> {
-    ReadModelError,
+    ReadModelError(String),
     LocInterpretError,
     BadAddressWidth(&'l String, u32),
     BadLastWriteTo(&'l String),
@@ -1052,8 +1052,8 @@ impl<'l> fmt::Display for FinalLocValuesError<'l> {
         use FinalLocValuesError::*;
         write!(f, "Failed to get final register state: ")?;
         match self {
-            ReadModelError => {
-                write!(f, "Failed to parse smt model")
+            ReadModelError(s) => {
+                write!(f, "Failed to parse smt model: {}", s)
             }
             LocInterpretError => {
                 write!(f, "Failed to read from smt model")
@@ -1090,8 +1090,9 @@ pub fn final_state_from_z3_output<'exec, 'ev, 'litmus, 'model, B: BV>(
     // that allows us to lookup the values z3 produced
     // 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::<B>::parse(&event_names, model_buf).map_err(|_mpe| FinalLocValuesError::ReadModelError)?;
+    let mut event_names: Vec<&'ev str> = exec.smt_events.iter().map(|ev| ev.name.as_ref()).collect();
+    event_names.push("IW");
+    let mut model = Model::<B>::parse(&event_names, model_buf).map_err(|mpe| FinalLocValuesError::ReadModelError(format!("{}", mpe)))?;
 
     let mut calc = |loc: &'litmus LitmusLoc<String>| match loc {
         LitmusLoc::Register { reg, thread_id } => exec

isla-axiomatic/src/footprint_analysis.rs

@@ -91,6 +91,8 @@ pub struct Footprint {
     pub is_branch: bool,
     /// An exclusive is any event with an exclusive read or write kind.
     pub is_exclusive: bool,
+    /// An event that writes to a system register
+    pub is_system_register_write: bool,
 }
 
 pub struct Footprintkey {
@@ -122,6 +124,7 @@ impl Footprint {
             is_load: false,
             is_branch: false,
             is_exclusive: false,
+            is_system_register_write: false,
         }
     }
 
@@ -197,6 +200,7 @@ impl Footprint {
         write!(buf, "\n  Is load: {}", self.is_load)?;
         write!(buf, "\n  Is exclusive: {}", self.is_exclusive)?;
         write!(buf, "\n  Is branch: {}", self.is_branch)?;
+        write!(buf, "\n  Is system register write: {}", self.is_system_register_write)?;
         writeln!(buf)?;
         Ok(())
     }
@@ -319,11 +323,22 @@ pub fn data_dep<B: BV>(from: usize, to: usize, instrs: &[Option<B>], footprints:
 
     let touched = touched_by(from, to, instrs, footprints);
 
-    for reg in &footprints.get(&to_opcode).unwrap().write_data_taints.registers {
+    let to_footprint = footprints.get(&to_opcode).unwrap();
+
+    for reg in &to_footprint.write_data_taints.registers {
         if touched.contains(reg) {
             return true;
         }
     }
+
+    if to_footprint.is_system_register_write {
+        for reg in &to_footprint.register_reads {
+            if touched.contains(reg) {
+                return true
+            }
+        }
+    }
+
     false
 }
 
@@ -565,6 +580,7 @@ where
                             || ev.is_branch()
                             || ev.is_smt()
                             || ev.is_fork()
+                            || ev.is_abstract()
                     })
                     .collect();
                 isla_lib::simplify::remove_unused(&mut events);
@@ -656,6 +672,8 @@ where
                             evrefs.collect_taints(*v, events, &mut footprint.branch_addr_taints)
                         }
                     }
+                    Event::Abstract { name, .. } if arch.shared_state.symtab.to_str(*name) == "zsail_system_register_write" =>
+                        footprint.is_system_register_write = true,
                     _ => (),
                 }
             }

isla-axiomatic/src/litmus.rs

@@ -1154,6 +1154,7 @@ impl<B: BV> Litmus<B> {
             ("_", ""),
             ("+", "plus"),
             (".", "dot"),
+            ("=", "equals"),
             ("0", "zero"),
             ("1", "one"),
             ("2", "two"),

isla-axiomatic/src/litmus/exp_parser.lalrpop

@@ -95,7 +95,7 @@ AtomicExp: Exp<String> = {
     <address:Id> => {
         let bytes = *sizeof.get(&address).unwrap_or(&8);
         Exp::Loc(address)
-    },      
+    },
     <f:Id> "(" ")" => Exp::App(f, Vec::new(), HashMap::new()),
     <f:Id> "(" <arg1:Arg> <mut argn:("," <Arg>)*> ")" => {
         let mut all_args = vec![arg1];

isla-axiomatic/src/sexp.rs

@@ -503,6 +503,16 @@ impl<'s> Sexp<'s> {
         }
     }
 
+    pub fn is_as_const(&self) -> bool {
+        match self {
+            Sexp::List(xs) if xs.len() == 2 => match &xs[0] {
+                Sexp::List(ys) if ys.len() == 3 && ys[0].is_atom("as") && ys[1].is_atom("const") => true,
+                _ => false
+            }
+            _ => false
+        }
+    }
+
     pub fn is_lambda(&self) -> bool {
         match self {
             Sexp::List(xs) if xs.len() == 3 && xs[0].is_atom("lambda") => true,
@@ -731,7 +741,7 @@ impl<'s> Sexp<'s> {
                     && (xs[1].is_atom("false") || xs[1].is_atom("true"))
                     && matches!(
                     &xs[0],
-                    Sexp::List(ys) if ys.len() == 3 && ys[0].is_atom("as") && ys[1].is_atom("const") && ys[2].is_atom("Array")) =>
+                    Sexp::List(ys) if ys.len() == 3 && ys[0].is_atom("as") && ys[1].is_atom("const")) =>
             {
                 Ok(SexpVal::Relation(SexpRelation::EmptyRelation(xs[1].is_atom("true"))))
             }

isla-axiomatic/src/smt_events.rs

@@ -40,6 +40,7 @@ use isla_lib::memory::Memory;
 use isla_lib::smt::{Event, Sym};
 
 use isla_cat::smt::Sexp;
+use isla_mml::accessor::ModelEvent;
 
 use crate::axiomatic::relations::*;
 use crate::axiomatic::{AxEvent, ExecutionInfo};
@@ -373,12 +374,20 @@ fn translate_read_invalid<B: BV>(ev: &AxEvent<B>) -> Sexp {
     }
 }
 
-fn dep_rel_target<B: BV>(ev: &AxEvent<B>) -> Sexp {
+fn dep_rel_target<B: BV>(ev: &AxEvent<B>, shared_state: &SharedState<B>) -> Sexp {
     if is_read(ev) || is_write(ev) {
-        Sexp::True
-    } else {
-        translate_read_invalid(ev)
+        return Sexp::True
     }
+
+    if let [base_event] = ev.base_events() {
+        match base_event {
+            Event::Abstract { name, .. } if shared_state.symtab.to_str(*name) == "zsail_system_register_write" =>
+                return Sexp::True,
+            _ => (),
+        }
+    }
+
+    translate_read_invalid(ev)
 }
 
 fn smt_empty() -> Sexp {
@@ -428,14 +437,15 @@ fn smt_dep_rel2<B: BV>(
     events: &[AxEvent<B>],
     thread_opcodes: &[Vec<Option<B>>],
     footprints: &HashMap<B, Footprint>,
+    shared_state: &SharedState<B>,
 ) -> Sexp {
     use Sexp::*;
     let mut deps = Vec::new();
     for (ev1, ev2) in Pairs::from_slice(events).filter(|(ev1, ev2)| rel(ev1, ev2, thread_opcodes, footprints)) {
         deps.push(And(vec![
             Eq(Box::new(Var(1)), Box::new(Literal(ev1.name.to_string()))),
             Eq(Box::new(Var(2)), Box::new(Literal(ev2.name.to_string()))),
-            dep_rel_target(ev2),
+            dep_rel_target(ev2, shared_state),
         ]))
     }
     let mut sexp = Or(deps);
@@ -571,7 +581,7 @@ pub fn smt_of_candidate<B: BV>(
     memory: &Memory<B>,
     initial_physical_addrs: &HashMap<u64, u64>,
     final_assertion: &Exp<u64>,
-    _shared_state: &SharedState<B>,
+    shared_state: &SharedState<B>,
     isa_config: &ISAConfig<B>,
 ) -> Result<(), Box<dyn Error>> {
     let events = &exec.smt_events;
@@ -915,8 +925,8 @@ pub fn smt_of_candidate<B: BV>(
     smt_condition_rel(disjoint, events, overlap_location).write_rel(output, "overlap-loc")?;
     smt_condition_rel(po, events, same_location).write_rel(output, "po-loc")?;
     smt_condition_rel(univ, events, read_write_pair).write_rel(output, "rw-pair")?;
-    smt_dep_rel2(addr, events, &exec.thread_opcodes, footprints).write_rel(output, "addr")?;
-    smt_dep_rel2(data, events, &exec.thread_opcodes, footprints).write_rel(output, "data")?;
+    smt_dep_rel2(addr, events, &exec.thread_opcodes, footprints, shared_state).write_rel(output, "addr")?;
+    smt_dep_rel2(data, events, &exec.thread_opcodes, footprints, shared_state).write_rel(output, "data")?;
     smt_dep_rel(ctrl, events, &exec.thread_opcodes, footprints).write_rel(output, "ctrl")?;
     smt_dep_rel(rmw, events, &exec.thread_opcodes, footprints).write_rel(output, "rmw")?;
     smt_basic_rel(|ev1, ev2| same_va_page(ev1, ev2, &translations), events)

isla-mml/src/memory_model.rs

@@ -545,7 +545,7 @@ pub enum Def {
     Let(Name, Vec<(Name, TyAnnot)>, TyAnnot, ExpId),
     Relation(u32, Name),
     Show(Vec<Name>),
-    Variant(Name),
+    Variants(Vec<Name>),
 }
 
 pub struct MemoryModel {
@@ -687,7 +687,7 @@ impl MemoryModel {
                 | Def::Declare(_, _, _)
                 | Def::Enum(_, _)
                 | Def::Index(_) => (),
-                Def::Variant(_) => (),
+                Def::Variants(_) => (),
             }
         }
         Ok(collection)
@@ -696,8 +696,10 @@ impl MemoryModel {
     pub fn variants(&self) -> Vec<&Name> {
         let mut names = vec![];
         for def in &self.defs {
-            if let Def::Variant(name) = &def.node {
-                names.push(name);
+            if let Def::Variants(new_names) = &def.node {
+                for name in new_names {
+                    names.push(name);
+                }
             }
         }
         names

isla-mml/src/parser.lalrpop

@@ -391,8 +391,8 @@ Def: Spanned<Def> = {
             Ok(Spanned { node: Def::Relation(n, id), file, span: (start, end) })
         }
     },
-    <start:@L> "variant" <id:VariantId> <end:@R> =>? {
-            Ok(Spanned { node: Def::Variant(id), file, span: (start, end) })
+    <start:@L> "variant" <ids:VariantId+> <end:@R> =>? {
+            Ok(Spanned { node: Def::Variants(ids), file, span: (start, end) })
     },
     <start:@L> "show" <ids:CommaNonEmpty<TopLevelId>> <end:@R> =>
         Spanned { node: Def::Show(ids), file, span: (start, end) },

isla-mml/src/smt.rs

@@ -1132,8 +1132,8 @@ pub fn compile_def(
             Ok(())
         }
 
-        // `variant blah` gets compiled to a set of Bool consts elsewhere
-        Def::Variant(_) => Ok(()),
+        // `variant x y z` gets compiled to a set of Bool consts elsewhere
+        Def::Variants(_) => Ok(()),
 
         Def::Relation(_, _) | Def::Show(_) => Ok(()),
 

isla-sail/sail_plugin_isla.ml

@@ -364,6 +364,7 @@ let isla_initialize () =
   Initial_check.opt_magic_hash := true;
 
   Specialize.add_initial_calls (IdSet.singleton (mk_id "isla_footprint"));
+  Specialize.add_initial_calls (IdSet.singleton (mk_id "isla_footprint_no_init"));
   Specialize.add_initial_calls (IdSet.singleton (mk_id "isla_footprint_bare"));
   Specialize.add_initial_calls (IdSet.singleton (mk_id "isla_client"));
   List.iter (fun id ->

src/axiomatic.rs

@@ -381,7 +381,7 @@ fn isla_main() -> i32 {
         panic!("cannot generate graph with --no-z3-model");
     }
 
-    let get_z3_model = matches.opt_present("no-z3-model");
+    let get_z3_model = !matches.opt_present("no-z3-model");
 
     let isla_litmus_path = matches.opt_str("isla-litmus");
     let litmus_translator_path = matches.opt_str("litmus-translator");