From a9ff34d5036f4b633489c9f05653f17564809f1d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Wed, 29 Nov 2023 14:02:20 -0500
Subject: [PATCH] sha sim is working

---
 .github/workflows/test.yml |  3 +++
 examples/sim.rs            | 13 ++++++++++---
 src/sim/exec.rs            | 33 +++++++++++++++++++++++++++++++++
 src/sim/interpreter.rs     | 29 ++++++++++++++---------------
 4 files changed, 60 insertions(+), 18 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 069162f..4e2e181 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -70,6 +70,9 @@ jobs:
       - name: simulate mux
         run: |
           cargo run --release --example sim -- --testbench=inputs/repair/mux_4_1.original.tb.csv inputs/repair/mux_4_1.original.btor
+      - name: simulate sha3 (keccak)
+        run: |
+          cargo run --release --example sim -- --testbench=inputs/repair/keccak.original.tb.csv inputs/repair/keccak.original.btor
 
   semver:
     name: Check Semantic Versioning
diff --git a/examples/sim.rs b/examples/sim.rs
index 327ee7a..ce2f157 100644
--- a/examples/sim.rs
+++ b/examples/sim.rs
@@ -7,6 +7,8 @@ use libpatron::ir::*;
 use libpatron::mc::Simulator;
 use libpatron::sim::interpreter::{InitKind, Interpreter};
 use libpatron::*;
+use num_bigint::BigUint;
+use num_traits::Num;
 use std::collections::HashMap;
 use std::io::BufRead;
 
@@ -157,9 +159,14 @@ fn do_step(
                 // apply input
                 let trimmed = cell.trim();
                 if trimmed.to_ascii_lowercase() != "x" {
-                    let expected = u64::from_str_radix(trimmed, 10).unwrap();
-                    let actual = sim.get(output.1).unwrap().to_u64().unwrap();
-                    assert_eq!(expected, actual, "{}@{step_id}", output.2);
+                    if let Ok(expected) = u64::from_str_radix(trimmed, 10) {
+                        let actual = sim.get(output.1).unwrap().to_u64().unwrap();
+                        assert_eq!(expected, actual, "{}@{step_id}", output.2);
+                    } else {
+                        let expected = BigUint::from_str_radix(trimmed, 10).unwrap();
+                        let actual = sim.get(output.1).unwrap().to_big_uint();
+                        assert_eq!(expected, actual, "{}@{step_id}", output.2);
+                    }
                 }
 
                 // get next output
diff --git a/src/sim/exec.rs b/src/sim/exec.rs
index 2fe1ab3..b5324c9 100644
--- a/src/sim/exec.rs
+++ b/src/sim/exec.rs
@@ -24,6 +24,11 @@ pub(crate) fn assign(dst: &mut [Word], source: &[Word]) {
     }
 }
 
+#[inline]
+pub(crate) fn read_bool(source: &[Word]) -> bool {
+    word_to_bool(source[0])
+}
+
 #[inline]
 pub(crate) fn assign_word(dst: &mut [Word], value: Word) {
     // assign the lsb
@@ -156,6 +161,11 @@ fn bool_to_word(value: bool) -> Word {
     }
 }
 
+#[inline]
+fn word_to_bool(value: Word) -> bool {
+    (value & 1) == 1
+}
+
 #[inline]
 pub(crate) fn split_borrow_1(
     data: &mut [Word],
@@ -229,6 +239,29 @@ pub(crate) fn to_bit_str(values: &[Word], width: WidthInt) -> String {
     out
 }
 
+pub(crate) fn to_big_uint(words: &[Word], width: WidthInt) -> num_bigint::BigUint {
+    let mut words32 = Vec::with_capacity(words.len() * 2);
+    let mask32 = mask(32);
+    let msb_offset = width % Word::BITS;
+    let msb_mask = if msb_offset == 0 {
+        Word::MAX
+    } else {
+        mask(msb_offset)
+    };
+    for (ii, w) in words.iter().enumerate() {
+        let word = if ii + 1 == words.len() {
+            msb_mask & (*w)
+        } else {
+            *w
+        };
+        let lsb = (word & mask32) as u32;
+        let msb = ((word >> 32) & mask32) as u32;
+        words32.push(lsb);
+        words32.push(msb);
+    }
+    num_bigint::BigUint::from_slice(&words32)
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
diff --git a/src/sim/interpreter.rs b/src/sim/interpreter.rs
index ab924cd..bbc5a73 100644
--- a/src/sim/interpreter.rs
+++ b/src/sim/interpreter.rs
@@ -306,6 +306,10 @@ impl<'a> ValueRef<'a> {
     pub fn to_bit_string(&self) -> String {
         exec::to_bit_str(self.words, self.bits)
     }
+
+    pub fn to_big_uint(&self) -> num_bigint::BigUint {
+        exec::to_big_uint(self.words, self.bits)
+    }
 }
 
 #[derive(Debug, Clone)]
@@ -421,23 +425,18 @@ fn exec_instr(instr: &Instr, data: &mut [Word]) {
                 );
             }
         }
-        InstrType::Tertiary(tpe, a_loc, b_loc, c_loc) => {
-            match tpe {
-                TertiaryOp::BVIte => {
-                    // we take advantage of the fact that the condition is always a bool
-                    let cond_value = data[a_loc.range()][0] != 0;
-                    if cond_value {
-                        let (dst, src) =
-                            exec::split_borrow_1(data, instr.dst.range(), b_loc.range());
-                        exec::assign(dst, src);
-                    } else {
-                        let (dst, src) =
-                            exec::split_borrow_1(data, instr.dst.range(), c_loc.range());
-                        exec::assign(dst, src);
-                    }
+        InstrType::Tertiary(tpe, a_loc, b_loc, c_loc) => match tpe {
+            TertiaryOp::BVIte => {
+                let cond_value = exec::read_bool(&data[a_loc.range()]);
+                if cond_value {
+                    let (dst, src) = exec::split_borrow_1(data, instr.dst.range(), b_loc.range());
+                    exec::assign(dst, src);
+                } else {
+                    let (dst, src) = exec::split_borrow_1(data, instr.dst.range(), c_loc.range());
+                    exec::assign(dst, src);
                 }
             }
-        }
+        },
     }
 }