From 17b0db5b32ec13a3f91b03149d1f3ce9058f7097 Mon Sep 17 00:00:00 2001 From: Yiqun Liu Date: Mon, 22 Jul 2024 12:37:35 +0200 Subject: [PATCH 1/2] Add support for indexing register array, for example pmpaddr_n and pmpcfg_n. --- isla-axiomatic/src/litmus/format.rs | 1 + isla-lib/src/executor.rs | 43 +++++++++++++++++++++++++++++ isla-lib/src/ir.rs | 8 ++++-- isla-lib/src/ir/linearize.rs | 1 + isla-lib/src/ir/ssa.rs | 8 +++++- isla-lib/src/simplify.rs | 4 +++ isla-lib/src/smt_parser.lalrpop | 6 ++-- 7 files changed, 66 insertions(+), 5 deletions(-) diff --git a/isla-axiomatic/src/litmus/format.rs b/isla-axiomatic/src/litmus/format.rs index 3e510e7..d628009 100644 --- a/isla-axiomatic/src/litmus/format.rs +++ b/isla-axiomatic/src/litmus/format.rs @@ -102,6 +102,7 @@ fn loc_latex(loc: &Loc, symtab: &Symtab) -> String { Loc::Id(id) => zencode::decode(symtab.to_str(*id)), Loc::Field(loc, field) => format!("{}.{}", loc_latex(loc, symtab), zencode::decode(symtab.to_str(*field))), Loc::Addr(loc) => format!("(*{})", loc_latex(loc, symtab)), + Loc::Index(loc, index) => format!("{}[{}]", loc_latex(loc, symtab), *index), } } diff --git a/isla-lib/src/executor.rs b/isla-lib/src/executor.rs index 986240b..23cd56b 100644 --- a/isla-lib/src/executor.rs +++ b/isla-lib/src/executor.rs @@ -161,6 +161,18 @@ fn get_loc_and_initialize<'ir, B: BV>( panic!("Struct expression did not evaluate to a struct") } } + Loc::Index(loc, index) => { + if let Val::Vector(vs) = + get_loc_and_initialize(loc, local_state, shared_state, solver, accessor, info, for_write)? + { + match vs.get(*index as usize) { + Some(index_value) => index_value.clone(), + None => panic!("Out of range {:?}", *index), + } + } else { + panic!("Index expression did not evalue to an array") + } + } _ => panic!("Cannot get_loc_and_initialize"), }) } @@ -567,6 +579,37 @@ fn assign_with_accessor<'ir, B: BV>( panic!("Cannot get address of non-reference {:?}", loc) } } + + Loc::Index(loc, index) => { + if let Val::Vector(index_values) = + get_loc_and_initialize(loc, local_state, shared_state, solver, &mut accessor.clone(), info, true)? + { + // As a sanity test, check that the index is in the range. + match index_values.get(*index as usize) { + Some(_) => { + let mut index_values = index_values.clone(); + index_values[*index as usize] = v; + assign_with_accessor( + loc, + Val::Vector(index_values), + local_state, + shared_state, + solver, + accessor, + info, + )?; + } + None => panic!("Out of range"), + } + } else { + panic!( + "Cannot assign Index to non-index {:?}.{:?} ({:?})", + loc, + index, + get_loc_and_initialize(loc, local_state, shared_state, solver, &mut accessor.clone(), info, true) + ) + } + } }; Ok(()) } diff --git a/isla-lib/src/ir.rs b/isla-lib/src/ir.rs index 52cf568..c0d339b 100644 --- a/isla-lib/src/ir.rs +++ b/isla-lib/src/ir.rs @@ -155,20 +155,21 @@ pub enum Loc { Id(A), Field(Box>, A), Addr(Box>), + Index(Box>, u32), } impl Loc { pub fn id(&self) -> A { match self { Loc::Id(id) => id.clone(), - Loc::Field(loc, _) | Loc::Addr(loc) => loc.id(), + Loc::Field(loc, _) | Loc::Addr(loc) | Loc::Index(loc, _) => loc.id(), } } pub fn id_mut(&mut self) -> &mut A { match self { Loc::Id(id) => id, - Loc::Field(loc, _) | Loc::Addr(loc) => loc.id_mut(), + Loc::Field(loc, _) | Loc::Addr(loc) | Loc::Index(loc, _) => loc.id_mut(), } } } @@ -179,6 +180,7 @@ impl fmt::Display for Loc { Loc::Id(a) => write!(f, "{}", zencode::decode(a)), Loc::Field(loc, a) => write!(f, "{}.{}", loc, a), Loc::Addr(a) => write!(f, "{}*", a), + Loc::Index(loc, a) => write!(f, "{}[{}]", loc, a), } } } @@ -922,6 +924,7 @@ impl<'ir> Symtab<'ir> { Id(v) => Id(self.get(v)?), Field(loc, field) => Field(Box::new(self.get_loc(loc)?), self.get(field)?), Addr(loc) => Addr(Box::new(self.get_loc(loc)?)), + Index(loc, idx) => Index(Box::new(self.get_loc(loc)?), *idx), }) } @@ -942,6 +945,7 @@ pub fn loc_string(loc: &Loc, symtab: &Symtab) -> String { Loc::Id(a) => zencode::decode(symtab.to_str(*a)), Loc::Field(loc, a) => format!("{}.{}", loc_string(loc, symtab), zencode::decode(symtab.to_str(*a))), Loc::Addr(a) => format!("{}*", loc_string(a, symtab)), + Loc::Index(loc, a) => format!("{}[{}]", loc_string(loc, symtab), a), } } diff --git a/isla-lib/src/ir/linearize.rs b/isla-lib/src/ir/linearize.rs index c84a843..9a76b82 100644 --- a/isla-lib/src/ir/linearize.rs +++ b/isla-lib/src/ir/linearize.rs @@ -181,6 +181,7 @@ fn unssa_loc(loc: &BlockLoc, symtab: &mut Symtab, names: &mut HashMap Id(id.unssa(symtab, names)), BlockLoc::Field(loc, _, field) => Field(Box::new(unssa_loc(loc, symtab, names)), field.unssa_orig(symtab)), BlockLoc::Addr(loc) => Addr(Box::new(unssa_loc(loc, symtab, names))), + BlockLoc::Index(loc, index) => Index(Box::new(unssa_loc(loc, symtab, names)), index.unssa_orig(symtab).id), } } diff --git a/isla-lib/src/ir/ssa.rs b/isla-lib/src/ir/ssa.rs index 6f620e3..ab919e3 100644 --- a/isla-lib/src/ir/ssa.rs +++ b/isla-lib/src/ir/ssa.rs @@ -157,13 +157,15 @@ pub enum BlockLoc { // Field locations contain the previous name so that we can update one field at a time Field(Box, SSAName, SSAName), Addr(Box), + // Index is not assignable and don't need SSA Name, so the ssa number is always -1. + Index(Box, SSAName), } impl BlockLoc { fn id(&self) -> SSAName { match self { BlockLoc::Id(id) => *id, - BlockLoc::Field(loc, _, _) | BlockLoc::Addr(loc) => loc.id(), + BlockLoc::Field(loc, _, _) | BlockLoc::Addr(loc) | BlockLoc::Index(loc, _) => loc.id(), } } @@ -172,6 +174,7 @@ impl BlockLoc { BlockLoc::Id(id) => (*id, None), BlockLoc::Field(loc, base_id, _) => (loc.id(), Some(*base_id)), BlockLoc::Addr(loc) => (loc.id(), None), + BlockLoc::Index(loc, index) => (loc.id(), Some(*index)), } } @@ -183,6 +186,8 @@ impl BlockLoc { vars.push(Variable::Usage(id)) } BlockLoc::Addr(loc) => loc.collect_variables(vars), + // idx is not var. + BlockLoc::Index(loc, _) => loc.collect_variables(vars), } } @@ -203,6 +208,7 @@ impl From<&Loc> for BlockLoc { BlockLoc::Field(Box::new(Self::from(loc.as_ref())), base_name, SSAName::new(*field)) } Loc::Addr(loc) => BlockLoc::Addr(Box::new(Self::from(loc.as_ref()))), + Loc::Index(loc, index) => BlockLoc::Index(Box::new(Self::from(loc.as_ref())), SSAName::new(Name::from_u32(*index))), } } } diff --git a/isla-lib/src/simplify.rs b/isla-lib/src/simplify.rs index 208861f..387a9c6 100644 --- a/isla-lib/src/simplify.rs +++ b/isla-lib/src/simplify.rs @@ -1364,6 +1364,10 @@ impl WriteVar for Loc { l = loc } Loc::Addr(loc) => l = loc, + Loc::Index(loc, idx) => { + write!(buf, "(_ index |{}|) ", idx)?; + l = loc + } } } write!(buf, "))") diff --git a/isla-lib/src/smt_parser.lalrpop b/isla-lib/src/smt_parser.lalrpop index 4fd3ff7..abed301 100644 --- a/isla-lib/src/smt_parser.lalrpop +++ b/isla-lib/src/smt_parser.lalrpop @@ -51,13 +51,15 @@ Comma: Vec = { Ident: String = => zencode::encode(id); +Num: u32 = =>? Ok(u32::from_str(n).map_err(|e| e.to_string())?); + Loc: Loc = { => Loc::Id(id), "." => Loc::Field(Box::new(loc), id), + // locate var by indexing array var + "[" "]" => Loc::Index(Box::new(loc), idx), } -Num: u32 = =>? Ok(u32::from_str(n).map_err(|e| e.to_string())?); - pub Exp: Exp> = { "=" => { exps.drain(..).fold(None, |acc, r| match acc { From fd2910430078c35602cda65ed2c210703f893654 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 22 Jul 2024 13:30:20 +0100 Subject: [PATCH 2/2] Add test for vector register constraints --- test/property/vector_register_reset.unsat.opts | 1 + test/property/vector_register_reset.unsat.sail | 10 ++++++++++ 2 files changed, 11 insertions(+) create mode 100644 test/property/vector_register_reset.unsat.opts create mode 100644 test/property/vector_register_reset.unsat.sail diff --git a/test/property/vector_register_reset.unsat.opts b/test/property/vector_register_reset.unsat.opts new file mode 100644 index 0000000..c0e8073 --- /dev/null +++ b/test/property/vector_register_reset.unsat.opts @@ -0,0 +1 @@ +--reset-constraint '(= R[3] true)' diff --git a/test/property/vector_register_reset.unsat.sail b/test/property/vector_register_reset.unsat.sail new file mode 100644 index 0000000..e3a57b9 --- /dev/null +++ b/test/property/vector_register_reset.unsat.sail @@ -0,0 +1,10 @@ +default Order dec +$include +$include + +register R: vector(16, bool) + +function prop() -> bool = { + isla_reset_registers(); + R[3] +}