From 698b78d854608b84f2a9457c994a8c4dea405e7b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 29 Nov 2023 21:06:50 -0500 Subject: [PATCH] add a couple new interpreter ops --- src/ir/analysis.rs | 18 +++++++-- src/ir/mod.rs | 3 +- src/sim/exec.rs | 69 ++++++++++++++++++++++++++------- src/sim/interpreter.rs | 88 ++++++++++++++++++++++++++++-------------- 4 files changed, 130 insertions(+), 48 deletions(-) diff --git a/src/ir/analysis.rs b/src/ir/analysis.rs index 4016efc..e24e0af 100644 --- a/src/ir/analysis.rs +++ b/src/ir/analysis.rs @@ -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 { + internal_count_expr_uses(ctx, sys, false) +} + +pub fn count_expr_uses_without_init(ctx: &Context, sys: &TransitionSystem) -> Vec { + internal_count_expr_uses(ctx, sys, true) +} + +fn internal_count_expr_uses(ctx: &Context, sys: &TransitionSystem, ignore_init: bool) -> Vec { let mut use_count = ExprMetaData::default(); let states: HashMap = HashMap::from_iter(sys.states().map(|s| (s.symbol, s))); let mut todo = Vec::from_iter( @@ -33,10 +41,12 @@ pub fn count_expr_uses(ctx: &Context, sys: &TransitionSystem) -> Vec { 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 { diff --git a/src/ir/mod.rs b/src/ir/mod.rs index c403d36..a1cbfb9 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -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, diff --git a/src/sim/exec.rs b/src/sim/exec.rs index b5324c9..2d4bb41 100644 --- a/src/sim/exec.rs +++ b/src/sim/exec.rs @@ -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]) @@ -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; @@ -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()) { @@ -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 { @@ -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); + } } diff --git a/src/sim/interpreter.rs b/src/sim/interpreter.rs index bbc5a73..b38e35d 100644 --- a/src/sim/interpreter.rs +++ b/src/sim/interpreter.rs @@ -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()); @@ -68,7 +68,7 @@ fn compile( use_counts: &[u32], ) -> (Vec>, usize) { // used to track instruction result allocations - let mut locs: Vec> = Vec::with_capacity(use_counts.len()); + let mut locs: Vec> = Vec::with_capacity(use_counts.len()); let mut instructions = Vec::new(); let mut word_count = 0u32; for (idx, count) in use_counts.iter().enumerate() { @@ -78,8 +78,8 @@ 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)); } @@ -87,15 +87,25 @@ fn compile( (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) } } } @@ -105,7 +115,7 @@ fn compile_expr( sys: &TransitionSystem, expr_ref: ExprRef, dst: Loc, - locs: &[Option], + locs: &[Option<(Loc, WidthInt)>], result_width: WidthInt, ) -> Instr { let expr = ctx.get(expr_ref); @@ -124,21 +134,23 @@ fn compile_expr( } } -fn compile_expr_type(expr: &Expr, locs: &[Option], 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!(), @@ -147,23 +159,23 @@ fn compile_expr_type(expr: &Expr, locs: &[Option], 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!(), @@ -176,17 +188,21 @@ fn compile_expr_type(expr: &Expr, locs: &[Option], 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!(), } } @@ -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, } @@ -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()]; @@ -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!( @@ -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); + } } }