From dc8a4ce29a5a83c5a4d027e6fbc0938e26a82ae1 Mon Sep 17 00:00:00 2001
From: bjs <benjsimner@gmail.com>
Date: Tue, 5 Sep 2023 11:14:15 +0000
Subject: [PATCH] (isla-axiomatic) add ifetch_initial_opcode function to
 generated smt

Adds ifetch_initial_opcode : Event -> bits(32) to isla-cat,
retrieving the value of the initial write of an IF event's opcode.
---
 isla-axiomatic/src/smt_events.rs | 65 ++++++++++++++++++++++++++++++++
 1 file changed, 65 insertions(+)

diff --git a/isla-axiomatic/src/smt_events.rs b/isla-axiomatic/src/smt_events.rs
index 90b7a88a..4be3d352 100644
--- a/isla-axiomatic/src/smt_events.rs
+++ b/isla-axiomatic/src/smt_events.rs
@@ -29,6 +29,7 @@
 
 use std::collections::{HashMap, HashSet};
 use std::error::Error;
+use std::fmt;
 use std::io::Write;
 
 use isla_lib::bitvector::BV;
@@ -265,6 +266,48 @@ fn read_initial<B: BV>(ev: &AxEvent<B>, memory: &Memory<B>, initial_addrs: &Hash
     }
 }
 
+/// Error when trying to get an opcode from [ifetch_initial_opcode]
+/// Either the event didn't have an address at all to fetch,
+/// or could not find the opcode in the objdump
+#[derive(Debug)]
+enum MissingOpcodeError<B: BV> {
+    MissingObjdump(B),
+    NoAddress,
+}
+
+impl<B: BV> fmt::Display for MissingOpcodeError<B> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            MissingOpcodeError::MissingObjdump(addr) => {
+                write!(f, "opcode missing for address {}", addr)
+            }
+            MissingOpcodeError::NoAddress => {
+                write!(f, "event address missing")
+            }
+        }
+    }
+}
+
+impl<B: BV> Error for MissingOpcodeError<B> {}
+
+/// [ifetch_initial_opcode] gets the original opcode
+/// (i.e. what will become the initial write for that location)
+/// for a given ifetch event `ev`
+/// using the opcodes in the objdump.
+fn ifetch_initial_opcode<B: BV>(ev: &AxEvent<B>, litmus: &Litmus<B>) -> Result<Sexp, MissingOpcodeError<B>> {
+    use Sexp::*;
+    match ev.address() {
+        Some(Val::Bits(addr)) => {
+            if let Some(opcode) = opcode_from_objdump(*addr, &litmus.objdump) {
+                Ok(Literal(format!("{}", opcode)))
+            } else {
+                Err(MissingOpcodeError::MissingObjdump(*addr))
+            }
+        }
+        _ => Err(MissingOpcodeError::NoAddress),
+    }
+}
+
 /// [ifetch_initial] checks if a ifetch is a valid fetch from the
 /// initial state, using the opcodes in the objdump. It also performs
 /// the same check as [ifetch_match], so they do not need to be used
@@ -577,6 +620,28 @@ pub fn smt_of_candidate<B: BV>(
         writeln!(output, ")\n")?
     }
 
+    {
+        // TODO: don't hardcode 32-bit ifetch opcode, or at least pad out to max word size
+        writeln!(output, "(define-fun ifetch_initial_opcode ((ev Event)) (_ BitVec 32)")?;
+        let mut ites: usize = 0;
+        for ev in events {
+            match ev.base() {
+                Some(Event::ReadMem { opts, .. }) if opts.is_ifetch => {
+                    write!(output, "{}", String::from_utf8(vec![b' '; 1 + ites])?)?;
+                    write!(output, "(ite (= ev {}) ", ev.name)?;
+                    ifetch_initial_opcode(ev, litmus)?.write_to(output, false, 0, true)?;
+                    ites += 1
+                }
+                _ => (),
+            }
+        }
+        write!(output, " {}", B::zeros(32))?;
+        for _ in 0..ites {
+            write!(output, ")")?
+        }
+        writeln!(output, ")\n")?
+    }
+
     {
         writeln!(output, "(define-fun addr_of ((ev Event)) (_ BitVec 64)")?;
         let mut ites: usize = 0;