Skip to content

Commit

Permalink
add a couple new interpreter ops
Browse files Browse the repository at this point in the history
  • Loading branch information
@ekiwi
ekiwi committed Nov 30, 2023
1 parent ddd4375 commit 698b78d
Show file tree
Hide file tree
Showing 4 changed files with 130 additions and 48 deletions.
18 changes: 14 additions & 4 deletions src/ir/analysis.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,14 @@ pub fn find_expr_with_multiple_uses(ctx: &Context, sys: &TransitionSystem) -> Ve
}

pub fn count_expr_uses(ctx: &Context, sys: &TransitionSystem) -> Vec<u32> {
internal_count_expr_uses(ctx, sys, false)
}

pub fn count_expr_uses_without_init(ctx: &Context, sys: &TransitionSystem) -> Vec<u32> {
internal_count_expr_uses(ctx, sys, true)
}

fn internal_count_expr_uses(ctx: &Context, sys: &TransitionSystem, ignore_init: bool) -> Vec<u32> {
let mut use_count = ExprMetaData::default();
let states: HashMap<ExprRef, &State> = HashMap::from_iter(sys.states().map(|s| (s.symbol, s)));
let mut todo = Vec::from_iter(
Expand All @@ -33,10 +41,12 @@ pub fn count_expr_uses(ctx: &Context, sys: &TransitionSystem) -> Vec<u32> {
if let Some(state) = states.get(&expr) {
// for states, we also want to mark the initial and the next expression as used
if let Some(init) = state.init {
let count = use_count.get_mut(init);
if *count == 0 {
*count = 1;
todo.push(init);
if !ignore_init {
let count = use_count.get_mut(init);
if *count == 0 {
*count = 1;
todo.push(init);
}
}
}
if let Some(next) = state.next {
Expand Down
3 changes: 2 additions & 1 deletion src/ir/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@ mod transition_system;
mod type_check;

pub use analysis::{
count_expr_uses, find_expr_with_multiple_uses, is_usage_root_signal, ForEachChild,
count_expr_uses, count_expr_uses_without_init, find_expr_with_multiple_uses,
is_usage_root_signal, ForEachChild,
};
pub use expr::{
bv_value_fits_width, AddNode, ArrayType, BVLiteralInt, Context, Expr, ExprNodeConstruction,
Expand Down
69 changes: 56 additions & 13 deletions src/sim/exec.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,20 @@ pub(crate) fn assign(dst: &mut [Word], source: &[Word]) {
}
}

fn assign_with_mask(dst: &mut [Word], source: &[Word], source_width: WidthInt) {
let offset = source_width % Word::BITS;
for (ii, (d, l)) in dst.iter_mut().zip(source.iter()).enumerate() {
let is_msb = ii + 1 == source.len();
if is_msb && offset > 0 {
// the msb of the lsb might need to be masked
let m = mask(offset);
*d = (*l) & m;
} else {
*d = *l;
}
}
}

#[inline]
pub(crate) fn read_bool(source: &[Word]) -> bool {
word_to_bool(source[0])
Expand All @@ -50,6 +64,14 @@ pub(crate) fn mask(bits: WidthInt) -> Word {
}
}

#[inline]
pub(crate) fn zero_extend(dst: &mut [Word], source: &[Word], source_width: WidthInt) {
// copy source to dst
assign_with_mask(dst, source, source_width);
// zero out remaining words
clear(&mut dst[source.len()..]);
}

#[inline]
pub(crate) fn slice(dst: &mut [Word], source: &[Word], hi: WidthInt, lo: WidthInt) {
let lo_offset = lo % Word::BITS;
Expand All @@ -76,21 +98,10 @@ pub(crate) fn slice(dst: &mut [Word], source: &[Word], hi: WidthInt, lo: WidthIn

#[inline]
pub(crate) fn concat(dst: &mut [Word], msb: &[Word], lsb: &[Word], lsb_width: WidthInt) {
let lsb_offset = lsb_width % Word::BITS;

// copy lsb to dst
for (ii, (d, l)) in dst.iter_mut().zip(lsb.iter()).enumerate() {
let is_msb = ii + 1 == lsb.len();
if is_msb && lsb_offset > 0 {
// the msb of the lsb might need to be masked
let m = mask(lsb_offset);
*d = (*l) & m;
} else {
*d = *l;
}
}
//
assign_with_mask(dst, lsb, lsb_width);

let lsb_offset = lsb_width % Word::BITS;
if lsb_offset == 0 {
// copy msb to dst
for (d, m) in dst.iter_mut().skip(lsb.len()).zip(msb.iter()) {
Expand Down Expand Up @@ -152,6 +163,17 @@ pub(crate) fn cmp_equal(a: &[Word], b: &[Word]) -> Word {
bool_to_word(bool_res)
}

#[inline]
pub(crate) fn cmp_greater(a: &[Word], b: &[Word]) -> Word {
todo!()
}

#[inline]
pub(crate) fn cmp_greater_equal(a: &[Word], b: &[Word]) -> Word {
// TODO: there is probably a more efficient way of implementing this
cmp_equal(a, b) | cmp_greater(a, b)
}

#[inline]
fn bool_to_word(value: bool) -> Word {
if value {
Expand Down Expand Up @@ -457,4 +479,25 @@ mod tests {
do_test_slice(&in2, 3 + (Word::BITS * 2) + 11, 3, &mut rng);
do_test_slice(&in2, 875, 875 - (Word::BITS * 2) - 15, &mut rng);
}

fn do_test_zero_ext(src: &str, by: WidthInt, rng: &mut impl Rng) {
let (mut src_vec, src_width) = from_bit_str(src);
randomize_dont_care_bits(&mut src_vec, src_width, rng);
let res_width = src_width + by;
let mut res_vec = vec![0 as Word; res_width.div_ceil(Word::BITS) as usize];
zero_extend(&mut res_vec, &src_vec, src_width);
let expected: String = format!("{}{}", "0".repeat(by as usize), src);
assert_eq!(to_bit_str(&res_vec, res_width), expected);
}

#[test]
fn test_zero_ext() {
let mut rng = rand_xoshiro::Xoshiro256PlusPlus::seed_from_u64(1);
do_test_zero_ext("0", 1, &mut rng);
do_test_zero_ext("1", 1, &mut rng);
do_test_zero_ext("0", 16, &mut rng);
do_test_zero_ext("1", 16, &mut rng);
do_test_zero_ext("0", 13 + Word::BITS, &mut rng);
do_test_zero_ext("1", 13 + Word::BITS, &mut rng);
}
}
88 changes: 58 additions & 30 deletions src/sim/interpreter.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ pub struct Interpreter<'a> {

impl<'a> Interpreter<'a> {
pub fn new(ctx: &'a Context, sys: &TransitionSystem) -> Self {
let use_counts = count_expr_uses(ctx, sys);
let use_counts = count_expr_uses_without_init(ctx, sys);
let (meta, data_len) = compile(ctx, sys, &use_counts);
let data = vec![0; data_len];
let mut states = Vec::with_capacity(sys.states().len());
Expand All @@ -68,7 +68,7 @@ fn compile(
use_counts: &[u32],
) -> (Vec<Option<Instr>>, usize) {
// used to track instruction result allocations
let mut locs: Vec<Option<Loc>> = Vec::with_capacity(use_counts.len());
let mut locs: Vec<Option<(Loc, WidthInt)>> = Vec::with_capacity(use_counts.len());
let mut instructions = Vec::new();
let mut word_count = 0u32;
for (idx, count) in use_counts.iter().enumerate() {
Expand All @@ -78,24 +78,34 @@ fn compile(
instructions.push(None); // TODO: we would like to store the instructions compacted
} else {
let tpe = expr.get_type(ctx);
let (loc, width) = allocate_result_space(tpe, &mut word_count);
locs.push(Some(loc));
let (loc, width, index_width) = allocate_result_space(tpe, &mut word_count);
locs.push(Some((loc, index_width)));
let instr = compile_expr(ctx, sys, expr, loc, &locs, width);
instructions.push(Some(instr));
}
}
(instructions, word_count as usize)
}

fn allocate_result_space(tpe: Type, word_count: &mut u32) -> (Loc, WidthInt) {
match tpe.get_bit_vector_width() {
None => todo!("array support"),
Some(width) => {
fn allocate_result_space(tpe: Type, word_count: &mut u32) -> (Loc, WidthInt, WidthInt) {
match tpe {
Type::BV(width) => {
let words = width.div_ceil(Word::BITS as WidthInt) as u16;
let offset = *word_count;
*word_count += words as u32;
let loc = Loc { offset, words };
(loc, width)
(loc, width, 0)
}
Type::Array(ArrayType {
index_width,
data_width,
}) => {
let words = data_width.div_ceil(Word::BITS as WidthInt) as u16;
let offset = *word_count;
let entries = 1u32 << index_width;
*word_count += words as u32 * entries;
let loc = Loc { offset, words };
(loc, data_width, index_width)
}
}
}
Expand All @@ -105,7 +115,7 @@ fn compile_expr(
sys: &TransitionSystem,
expr_ref: ExprRef,
dst: Loc,
locs: &[Option<Loc>],
locs: &[Option<(Loc, WidthInt)>],
result_width: WidthInt,
) -> Instr {
let expr = ctx.get(expr_ref);
Expand All @@ -124,21 +134,23 @@ fn compile_expr(
}
}

fn compile_expr_type(expr: &Expr, locs: &[Option<Loc>], ctx: &Context) -> InstrType {
fn compile_expr_type(expr: &Expr, locs: &[Option<(Loc, WidthInt)>], ctx: &Context) -> InstrType {
match expr {
Expr::BVSymbol { .. } => InstrType::Nullary(NullaryOp::BVSymbol),
Expr::BVLiteral { value, .. } => InstrType::Nullary(NullaryOp::BVLiteral(*value)),
Expr::BVZeroExt { .. } => todo!("compile zext"),
Expr::BVZeroExt { e, by, width } => {
InstrType::Unary(UnaryOp::ZeroExt(*width - *by), locs[e.index()].unwrap().0)
}
Expr::BVSignExt { .. } => todo!("compile sext"),
Expr::BVSlice { e, hi, lo } => {
InstrType::Unary(UnaryOp::Slice(*hi, *lo), locs[e.index()].unwrap())
InstrType::Unary(UnaryOp::Slice(*hi, *lo), locs[e.index()].unwrap().0)
}
Expr::BVNot(e, _) => InstrType::Unary(UnaryOp::Not, locs[e.index()].unwrap()),
Expr::BVNot(e, _) => InstrType::Unary(UnaryOp::Not, locs[e.index()].unwrap().0),
Expr::BVNegate(_, _) => todo!(),
Expr::BVEqual(a, b) => InstrType::Binary(
BinaryOp::BVEqual,
locs[a.index()].unwrap(),
locs[b.index()].unwrap(),
locs[a.index()].unwrap().0,
locs[b.index()].unwrap().0,
),
Expr::BVImplies(_, _) => todo!(),
Expr::BVGreater(_, _) => todo!(),
Expand All @@ -147,23 +159,23 @@ fn compile_expr_type(expr: &Expr, locs: &[Option<Loc>], ctx: &Context) -> InstrT
Expr::BVGreaterEqualSigned(_, _) => todo!(),
Expr::BVConcat(a, b, _) => InstrType::Binary(
BinaryOp::Concat(b.get_bv_type(ctx).unwrap()), // LSB width
locs[a.index()].unwrap(),
locs[b.index()].unwrap(),
locs[a.index()].unwrap().0,
locs[b.index()].unwrap().0,
),
Expr::BVAnd(a, b, _) => InstrType::Binary(
BinaryOp::And,
locs[a.index()].unwrap(),
locs[b.index()].unwrap(),
locs[a.index()].unwrap().0,
locs[b.index()].unwrap().0,
),
Expr::BVOr(a, b, _) => InstrType::Binary(
BinaryOp::Or,
locs[a.index()].unwrap(),
locs[b.index()].unwrap(),
locs[a.index()].unwrap().0,
locs[b.index()].unwrap().0,
),
Expr::BVXor(a, b, _) => InstrType::Binary(
BinaryOp::Xor,
locs[a.index()].unwrap(),
locs[b.index()].unwrap(),
locs[a.index()].unwrap().0,
locs[b.index()].unwrap().0,
),
Expr::BVShiftLeft(_, _, _) => todo!(),
Expr::BVArithmeticShiftRight(_, _, _) => todo!(),
Expand All @@ -176,17 +188,21 @@ fn compile_expr_type(expr: &Expr, locs: &[Option<Loc>], ctx: &Context) -> InstrT
Expr::BVSignedRem(_, _, _) => todo!(),
Expr::BVUnsignedRem(_, _, _) => todo!(),
Expr::BVSub(_, _, _) => todo!(),
Expr::BVArrayRead { .. } => todo!(),
Expr::BVArrayRead { array, index, .. } => {
let (array_loc, index_width) = locs[array.index()].unwrap();
assert!(index_width <= Word::BITS, "array too large!");
InstrType::ArrayRead(array_loc, index_width, locs[index.index()].unwrap().0)
}
Expr::BVIte { cond, tru, fals } => InstrType::Tertiary(
TertiaryOp::BVIte,
locs[cond.index()].unwrap(),
locs[tru.index()].unwrap(),
locs[fals.index()].unwrap(),
locs[cond.index()].unwrap().0,
locs[tru.index()].unwrap().0,
locs[fals.index()].unwrap().0,
),
Expr::ArraySymbol { .. } => todo!(),
Expr::ArraySymbol { .. } => InstrType::Nullary(NullaryOp::ArraySymbol),
Expr::ArrayConstant { .. } => todo!(),
Expr::ArrayEqual(_, _) => todo!(),
Expr::ArrayStore { .. } => todo!(),
Expr::ArrayStore { .. } => panic!("Array stores should have been preprocessed!"),
Expr::ArrayIte { .. } => todo!(),
}
}
Expand Down Expand Up @@ -327,17 +343,20 @@ enum InstrType {
Unary(UnaryOp, Loc),
Binary(BinaryOp, Loc, Loc),
Tertiary(TertiaryOp, Loc, Loc, Loc),
ArrayRead(Loc, WidthInt, Loc), // array loc + array index width + index loc
}

#[derive(Debug, Clone)]
enum NullaryOp {
BVSymbol,
ArraySymbol,
BVLiteral(BVLiteralInt),
}

#[derive(Debug, Clone)]
enum UnaryOp {
Slice(WidthInt, WidthInt),
ZeroExt(WidthInt),
Not,
}

Expand Down Expand Up @@ -376,6 +395,7 @@ fn exec_instr(instr: &Instr, data: &mut [Word]) {
InstrType::Nullary(tpe) => {
match tpe {
NullaryOp::BVSymbol => {}
NullaryOp::ArraySymbol => {}
NullaryOp::BVLiteral(value) => {
// TODO: optimize by only calculating once!
let dst = &mut data[instr.dst.range()];
Expand All @@ -394,6 +414,7 @@ fn exec_instr(instr: &Instr, data: &mut [Word]) {
match tpe {
UnaryOp::Slice(hi, lo) => exec::slice(dst, a, *hi, *lo),
UnaryOp::Not => exec::not(dst, a),
UnaryOp::ZeroExt(source_width) => exec::zero_extend(dst, a, *source_width),
}
if instr.do_trace {
println!(
Expand Down Expand Up @@ -437,6 +458,13 @@ fn exec_instr(instr: &Instr, data: &mut [Word]) {
}
}
},
InstrType::ArrayRead(array, index_width, index) => {
let index_value = data[index.range()][0] & exec::mask(*index_width);
let src_start = array.offset as usize + array.words as usize * index_value as usize;
let src_range = src_start..(src_start + array.words as usize);
let (dst, src) = exec::split_borrow_1(data, instr.dst.range(), src_range);
exec::assign(dst, src);
}
}
}

Expand Down

0 comments on commit 698b78d

Please sign in to comment.