Add support for indexing register array

isla-axiomatic/src/litmus/format.rs

@@ -102,6 +102,7 @@ fn loc_latex(loc: &Loc<Name>, 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),
     }
 }
 

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

isla-lib/src/ir.rs

@@ -155,20 +155,21 @@ pub enum Loc<A> {
     Id(A),
     Field(Box<Loc<A>>, A),
     Addr(Box<Loc<A>>),
+    Index(Box<Loc<A>>, u32),
 }
 
 impl<A: Clone> Loc<A> {
     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<String> {
             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<Name>, 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),
     }
 }
 

isla-lib/src/ir/linearize.rs

@@ -181,6 +181,7 @@ fn unssa_loc(loc: &BlockLoc, symtab: &mut Symtab, names: &mut HashMap<SSAName, N
         BlockLoc::Id(id) => 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),
     }
 }
 

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<BlockLoc>, SSAName, SSAName),
     Addr(Box<BlockLoc>),
+    // Index is not assignable and don't need SSA Name, so the ssa number is always -1.
+    Index(Box<BlockLoc>, 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<Name>> 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))),
         }
     }
 }

isla-lib/src/simplify.rs

@@ -1364,6 +1364,10 @@ impl WriteVar for Loc<String> {
                             l = loc
                         }
                         Loc::Addr(loc) => l = loc,
+                        Loc::Index(loc, idx) => {
+                            write!(buf, "(_ index |{}|) ", idx)?;
+                            l = loc
+                        }
                     }
                 }
                 write!(buf, "))")

isla-lib/src/smt_parser.lalrpop

@@ -51,13 +51,15 @@ Comma<T>: Vec<T> = {
 
 Ident: String = <id:r"[A-Za-z_][A-Za-z0-9_'#]*"> => zencode::encode(id);
 
+Num: u32 = <n:r"[0-9]+"> =>? Ok(u32::from_str(n).map_err(|e| e.to_string())?);
+
 Loc: Loc<String> = {
     <id:Ident> => Loc::Id(id),
     <loc:Loc> "." <id:Ident> => Loc::Field(Box::new(loc), id),
+    // locate var by indexing array var
+    <loc:Loc> "[" <idx:Num> "]" => Loc::Index(Box::new(loc), idx),
 }
 
-Num: u32 = <n:r"[0-9]+"> =>? Ok(u32::from_str(n).map_err(|e| e.to_string())?);
-
 pub Exp: Exp<Loc<String>> = {
     "=" <exp:Exp1> <mut exps:Exp1+> => {
         exps.drain(..).fold(None, |acc, r| match acc {