toolCHAINZ
diff --git a/‎jingle/Cargo.toml‎
Lines changed: 2 additions & 2 deletions b/‎jingle/Cargo.toml‎
Lines changed: 2 additions & 2 deletions
diff --git a/‎jingle/src/context.rs‎
Lines changed: 57 additions & 40 deletions b/‎jingle/src/context.rs‎
Lines changed: 57 additions & 40 deletions
diff --git a/‎jingle/src/error.rs‎
Lines changed: 2 additions & 2 deletions b/‎jingle/src/error.rs‎
Lines changed: 2 additions & 2 deletions
diff --git a/‎jingle/src/modeling/block.rs‎
Lines changed: 20 additions & 7 deletions b/‎jingle/src/modeling/block.rs‎
Lines changed: 20 additions & 7 deletions
diff --git a/‎jingle/src/modeling/instruction.rs‎
Lines changed: 19 additions & 7 deletions b/‎jingle/src/modeling/instruction.rs‎
Lines changed: 19 additions & 7 deletions
diff --git a/‎jingle/src/modeling/machine/cpu/concrete.rs‎
Lines changed: 78 additions & 0 deletions b/‎jingle/src/modeling/machine/cpu/concrete.rs‎
Lines changed: 78 additions & 0 deletions
@@ -1,6 +1,6 @@
 [package]
 name = "jingle"
-version = "0.1.1"
+version = "0.2.1"
 edition = "2021"
 description = "SMT Modeling for Ghidra's PCODE"
 homepage = "https://github.com/toolCHAINZ/jingle"
@@ -19,7 +19,7 @@ name = "jingle"
 required-features = ["bin_features"]
 
 [dependencies]
-jingle_sleigh = { path = "../jingle_sleigh", version = "0.1.1" }
+jingle_sleigh = { path = "../jingle_sleigh", version = "0.2.0" }
 z3 = { git = "https://github.com/prove-rs/z3.rs.git", branch = "master" }
 thiserror = "1.0.58"
 serde = { version = "1.0.197", features = ["derive"] }
 
@@ -1,15 +1,54 @@
 use crate::modeling::State;
-use jingle_sleigh::{RegisterManager, SpaceInfo, SpaceManager, VarNode};
+use jingle_sleigh::{ArchInfoProvider, SpaceInfo, VarNode};
 use std::ops::Deref;
 use std::rc::Rc;
 use z3::Context;
 
+#[derive(Clone, Debug)]
+pub struct CachedArchInfo {
+    registers: Vec<(VarNode, String)>,
+    spaces: Vec<SpaceInfo>,
+    default_code_space: usize,
+}
+
+impl ArchInfoProvider for JingleContext<'_> {
+    fn get_space_info(&self, idx: usize) -> Option<&SpaceInfo> {
+        self.info.spaces.get(idx)
+    }
+
+    fn get_all_space_info(&self) -> impl Iterator<Item = &SpaceInfo> {
+        self.info.spaces.iter()
+    }
+
+    fn get_code_space_idx(&self) -> usize {
+        self.info.default_code_space
+    }
+
+    fn get_register(&self, name: &str) -> Option<&VarNode> {
+        self.info
+            .registers
+            .iter()
+            .find(|(_, reg_name)| reg_name.as_str() == name)
+            .map(|(vn, _)| vn)
+    }
+
+    fn get_register_name(&self, location: &VarNode) -> Option<&str> {
+        self.info
+            .registers
+            .iter()
+            .find(|(vn, _)| vn == location)
+            .map(|(_, name)| name.as_str())
+    }
+
+    fn get_registers(&self) -> impl Iterator<Item = (&VarNode, &str)> {
+        self.info.registers.iter().map(|(a, b)| (a, b.as_str()))
+    }
+}
+
 #[derive(Clone, Debug)]
 pub struct JingleContextInternal<'ctx> {
     pub z3: &'ctx Context,
-    spaces: Vec<SpaceInfo>,
-    default_code_space_index: usize,
-    registers: Vec<(VarNode, String)>,
+    pub info: CachedArchInfo,
 }
 
 #[derive(Clone, Debug)]
@@ -23,49 +62,27 @@ impl<'ctx> Deref for JingleContext<'ctx> {
     }
 }
 impl<'ctx> JingleContext<'ctx> {
-    pub fn new<S: RegisterManager>(z3: &'ctx Context, r: &S) -> Self {
-        let spaces = r.get_all_space_info().to_vec();
-        let default_code_space_index = r.get_code_space_idx();
+    pub fn new<S: ArchInfoProvider>(z3: &'ctx Context, r: &S) -> Self {
         Self(Rc::new(JingleContextInternal {
             z3,
-            spaces,
-            default_code_space_index,
-            registers: r.get_registers(),
+            info: CachedArchInfo {
+                spaces: r.get_all_space_info().cloned().collect(),
+                registers: r
+                    .get_registers()
+                    .map(|(a, b)| (a.clone(), b.to_string()))
+                    .collect(),
+                default_code_space: r.get_code_space_idx(),
+            },
         }))
     }
     pub fn fresh_state(&self) -> State<'ctx> {
         State::new(self)
     }
-}
-
-impl SpaceManager for JingleContext<'_> {
-    fn get_space_info(&self, idx: usize) -> Option<&SpaceInfo> {
-        self.spaces.get(idx)
-    }
-
-    fn get_all_space_info(&self) -> &[SpaceInfo] {
-        self.spaces.as_slice()
-    }
-
-    fn get_code_space_idx(&self) -> usize {
-        self.default_code_space_index
-    }
-}
-
-impl RegisterManager for JingleContext<'_> {
-    fn get_register(&self, name: &str) -> Option<VarNode> {
-        self.registers
-            .iter()
-            .find_map(|i| i.1.eq(name).then_some(i.0.clone()))
-    }
 
-    fn get_register_name(&self, location: &VarNode) -> Option<&str> {
-        self.registers
-            .iter()
-            .find_map(|i| i.0.eq(location).then_some(i.1.as_str()))
-    }
-
-    fn get_registers(&self) -> Vec<(VarNode, String)> {
-        self.registers.clone()
+    pub fn with_fresh_z3_context(&self, z3: &'ctx Context) -> Self {
+        Self(Rc::new(JingleContextInternal {
+            z3,
+            info: self.info.clone(),
+        }))
     }
 }
@@ -7,8 +7,8 @@ pub enum JingleError {
     Sleigh(#[from] JingleSleighError),
     #[error("Given address disassembles cleanly but does not terminate within the given bound")]
     DisassemblyLengthBound,
-    #[error("This block exhibits unhandled intra-instruction control-flow")]
-    IntraInstructionControlFlow,
+    #[error("Attempted to construct an illegally-sized branch target")]
+    InvalidBranchTargetSize,
     #[error("A z3 array selection operation returned something other than a bitvector")]
     UnexpectedArraySort,
     #[error("Something referenced a space that isn't declared")]
 
@@ -6,9 +6,9 @@ use crate::modeling::{ModelingContext, TranslationContext};
 use crate::varnode::ResolvedVarnode;
 use crate::JingleContext;
 use crate::JingleError::EmptyBlock;
-use jingle_sleigh::Instruction;
 use jingle_sleigh::PcodeOperation;
-use jingle_sleigh::{SpaceInfo, SpaceManager};
+use jingle_sleigh::SpaceInfo;
+use jingle_sleigh::{ArchInfoProvider, Instruction, VarNode};
 use std::collections::HashSet;
 use std::fmt::{Display, Formatter};
 
@@ -122,16 +122,29 @@ impl<'ctx> ModeledBlock<'ctx> {
     }
 }
 
-impl SpaceManager for ModeledBlock<'_> {
+impl ArchInfoProvider for ModeledBlock<'_> {
     fn get_space_info(&self, idx: usize) -> Option<&SpaceInfo> {
-        self.state.get_space_info(idx)
+        self.jingle.get_space_info(idx)
     }
 
-    fn get_all_space_info(&self) -> &[SpaceInfo] {
-        self.state.get_all_space_info()
+    fn get_all_space_info(&self) -> impl Iterator<Item = &SpaceInfo> {
+        self.jingle.get_all_space_info()
     }
+
     fn get_code_space_idx(&self) -> usize {
-        self.state.get_code_space_idx()
+        self.jingle.get_code_space_idx()
+    }
+
+    fn get_register(&self, name: &str) -> Option<&VarNode> {
+        self.jingle.get_register(name)
+    }
+
+    fn get_register_name(&self, location: &VarNode) -> Option<&str> {
+        self.jingle.get_register_name(location)
+    }
+
+    fn get_registers(&self) -> impl Iterator<Item = (&VarNode, &str)> {
+        self.jingle.get_registers()
     }
 }
 
 
@@ -1,6 +1,6 @@
 use crate::modeling::{ModelingContext, TranslationContext};
-use jingle_sleigh::Instruction;
 use jingle_sleigh::PcodeOperation;
+use jingle_sleigh::{Instruction, VarNode};
 
 use std::collections::HashSet;
 
@@ -9,7 +9,7 @@ use crate::modeling::state::State;
 
 use crate::varnode::ResolvedVarnode;
 use crate::{JingleContext, JingleError};
-use jingle_sleigh::{SpaceInfo, SpaceManager};
+use jingle_sleigh::{ArchInfoProvider, SpaceInfo};
 
 /// A `jingle` model of an individual SLEIGH instruction
 #[derive(Debug, Clone)]
@@ -51,17 +51,29 @@ impl<'ctx> ModeledInstruction<'ctx> {
     }
 }
 
-impl SpaceManager for ModeledInstruction<'_> {
+impl ArchInfoProvider for ModeledInstruction<'_> {
     fn get_space_info(&self, idx: usize) -> Option<&SpaceInfo> {
-        self.state.get_space_info(idx)
+        self.jingle.get_space_info(idx)
     }
 
-    fn get_all_space_info(&self) -> &[SpaceInfo] {
-        self.state.get_all_space_info()
+    fn get_all_space_info(&self) -> impl Iterator<Item = &SpaceInfo> {
+        self.jingle.get_all_space_info()
     }
 
     fn get_code_space_idx(&self) -> usize {
-        self.state.get_code_space_idx()
+        self.jingle.get_code_space_idx()
+    }
+
+    fn get_register(&self, name: &str) -> Option<&VarNode> {
+        self.jingle.get_register(name)
+    }
+
+    fn get_register_name(&self, location: &VarNode) -> Option<&str> {
+        self.jingle.get_register_name(location)
+    }
+
+    fn get_registers(&self) -> impl Iterator<Item = (&VarNode, &str)> {
+        self.jingle.get_registers()
     }
 }
 
 
@@ -0,0 +1,78 @@
+use crate::modeling::machine::cpu::symbolic::SymbolicPcodeAddress;
+use jingle_sleigh::VarNode;
+use std::fmt::{Display, Formatter, LowerHex};
+use z3::ast::BV;
+use z3::Context;
+
+pub type PcodeMachineAddress = u64;
+pub type PcodeOffset = u8;
+#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
+pub struct ConcretePcodeAddress {
+    pub(crate) machine: PcodeMachineAddress,
+    pub(crate) pcode: PcodeOffset,
+}
+
+impl Display for ConcretePcodeAddress {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}:{}", self.machine, self.pcode)
+    }
+}
+
+impl LowerHex for ConcretePcodeAddress {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:x}:{:x}", self.machine, self.pcode)
+    }
+}
+
+impl ConcretePcodeAddress {
+    pub fn next_pcode(&self) -> Self {
+        self.add_pcode_offset(1)
+    }
+
+    pub fn machine(&self) -> PcodeMachineAddress {
+        self.machine
+    }
+
+    pub fn pcode(&self) -> PcodeOffset {
+        self.pcode
+    }
+
+    pub(crate) fn add_pcode_offset(&self, off: PcodeOffset) -> Self {
+        Self {
+            machine: self.machine,
+            pcode: self.pcode.wrapping_add(off),
+        }
+    }
+    pub fn symbolize<'ctx>(&self, z3: &'ctx Context) -> SymbolicPcodeAddress<'ctx> {
+        SymbolicPcodeAddress {
+            machine: BV::from_u64(
+                z3,
+                self.machine,
+                size_of::<PcodeMachineAddress>() as u32 * 8,
+            ),
+            pcode: BV::from_u64(z3, self.pcode as u64, size_of::<PcodeOffset>() as u32 * 8),
+        }
+    }
+
+    pub fn resolve_from_varnode(vn: &VarNode, loc: ConcretePcodeAddress) -> Self {
+        if vn.is_const() {
+            // relative jump
+            loc.add_pcode_offset(vn.offset as u8)
+        } else {
+            // absolute jump
+            ConcretePcodeAddress {
+                machine: vn.offset,
+                pcode: 0,
+            }
+        }
+    }
+}
+
+impl From<PcodeMachineAddress> for ConcretePcodeAddress {
+    fn from(value: PcodeMachineAddress) -> Self {
+        Self {
+            machine: value,
+            pcode: 0,
+        }
+    }
+}