Skip to content

Commit

Permalink
sha sim is working
Browse files Browse the repository at this point in the history
  • Loading branch information
ekiwi committed Nov 29, 2023
1 parent fb2cf89 commit a9ff34d
Show file tree
Hide file tree
Showing 4 changed files with 60 additions and 18 deletions.
3 changes: 3 additions & 0 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
13 changes: 10 additions & 3 deletions examples/sim.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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
Expand Down
33 changes: 33 additions & 0 deletions src/sim/exec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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],
Expand Down Expand Up @@ -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::*;
Expand Down
29 changes: 14 additions & 15 deletions src/sim/interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -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);
}
}
}
},
}
}

Expand Down

0 comments on commit a9ff34d

Please sign in to comment.