From 8e38537982962993da5c28835229105935a14fb3 Mon Sep 17 00:00:00 2001
From: Mark <mark.denhoed@cs.ox.ac.uk>
Date: Thu, 28 Nov 2024 10:36:54 +0000
Subject: [PATCH] Remove explicit dependence on p-code operation memory
 location from SMT encoding

---
 jingle/src/modeling/bmc/machine/cpu/relations.rs |  7 +++----
 jingle/src/modeling/bmc/machine/cpu/symbolic.rs  | 13 +++++++++++--
 jingle/src/modeling/bmc/machine/mod.rs           |  6 ++----
 3 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/jingle/src/modeling/bmc/machine/cpu/relations.rs b/jingle/src/modeling/bmc/machine/cpu/relations.rs
index 9330e57..73a0511 100644
--- a/jingle/src/modeling/bmc/machine/cpu/relations.rs
+++ b/jingle/src/modeling/bmc/machine/cpu/relations.rs
@@ -2,7 +2,7 @@ use crate::modeling::bmc::machine::cpu::concrete::ConcretePcodeAddress;
 use crate::modeling::bmc::machine::cpu::symbolic::SymbolicPcodeAddress;
 use crate::modeling::bmc::machine::memory::MemoryState;
 use crate::JingleError;
-use jingle_sleigh::PcodeOperation;
+use jingle_sleigh::{PcodeOperation, VarNode};
 use z3::ast::{Ast, BV};
 use z3::Context;
 
@@ -11,17 +11,16 @@ impl<'ctx> SymbolicPcodeAddress<'ctx> {
         &self,
         memory: &MemoryState<'ctx>,
         op: &PcodeOperation,
-        location: ConcretePcodeAddress,
         z3: &'ctx Context,
     ) -> Result<Self, JingleError> {
         match op {
             PcodeOperation::Branch { input } | PcodeOperation::Call { input } => {
-                Ok(ConcretePcodeAddress::resolve_from_varnode(input, location).symbolize(z3))
+                Ok(self.interpret_branch_dest_varnode(input))
             }
             PcodeOperation::CBranch { input0, input1 } => {
                 let fallthrough = self.increment_pcode();
                 let dest =
-                    ConcretePcodeAddress::resolve_from_varnode(input0, location).symbolize(z3);
+                    self.interpret_branch_dest_varnode(input0);
                 let take_branch =
                     memory
                         .read(input1)?
diff --git a/jingle/src/modeling/bmc/machine/cpu/symbolic.rs b/jingle/src/modeling/bmc/machine/cpu/symbolic.rs
index 8858d56..ece8a0f 100644
--- a/jingle/src/modeling/bmc/machine/cpu/symbolic.rs
+++ b/jingle/src/modeling/bmc/machine/cpu/symbolic.rs
@@ -2,6 +2,7 @@ use crate::modeling::bmc::machine::cpu::concrete::{
     ConcretePcodeAddress, PcodeMachineAddress, PcodeOffset,
 };
 use crate::JingleError;
+use jingle_sleigh::VarNode;
 use std::ops::Add;
 use z3::ast::{Ast, BV};
 use z3::Context;
@@ -58,9 +59,17 @@ impl<'ctx> SymbolicPcodeAddress<'ctx> {
                 pcode: p as PcodeOffset,
             })
     }
-
+    pub fn interpret_branch_dest_varnode(&self, vn: &VarNode) -> Self {
+        match vn.is_const() {
+            true => self.add_pcode_offset(vn.offset),
+            false => ConcretePcodeAddress::from(vn.offset).symbolize(self.machine.get_ctx()),
+        }
+    }
     pub fn increment_pcode(&self) -> SymbolicPcodeAddress<'ctx> {
-        let pcode = self.extract_pcode().add(1u64);
+        self.add_pcode_offset(1)
+    }
+    fn add_pcode_offset(&self, offset: u64) -> SymbolicPcodeAddress<'ctx> {
+        let pcode = self.extract_pcode() + offset;
         let machine = self.extract_machine().clone();
         SymbolicPcodeAddress { machine, pcode }
     }
diff --git a/jingle/src/modeling/bmc/machine/mod.rs b/jingle/src/modeling/bmc/machine/mod.rs
index 46de393..6ad0320 100644
--- a/jingle/src/modeling/bmc/machine/mod.rs
+++ b/jingle/src/modeling/bmc/machine/mod.rs
@@ -38,20 +38,18 @@ impl<'ctx> MachineState<'ctx> {
     fn apply_control_flow(
         &self,
         op: &PcodeOperation,
-        location: ConcretePcodeAddress,
     ) -> Result<SymbolicPcodeAddress<'ctx>, JingleError> {
-        self.pc.apply_op(&self.memory, op, location, self.jingle.z3)
+        self.pc.apply_op(&self.memory, op, self.jingle.z3)
     }
 
     pub fn apply(
         &self,
         op: &PcodeOperation,
-        location: ConcretePcodeAddress,
     ) -> Result<Self, JingleError> {
         Ok(Self {
             jingle: self.jingle.clone(),
             memory: self.memory.apply(op)?,
-            pc: self.apply_control_flow(op, location)?,
+            pc: self.apply_control_flow(op)?,
         })
     }
 }