From a465e4a0cb04d82b211d5958e2560621dda4b738 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 17 Nov 2023 10:56:47 -0500 Subject: [PATCH] add some array support --- src/btor2/parse.rs | 14 +++++++++----- src/ir/expr.rs | 27 ++++++++++++++++++++++++++ src/ir/serialize.rs | 5 ++--- src/ir/type_check.rs | 16 +++++++++------ src/mc/smt.rs | 19 +++++++++++++++--- src/sim/interpreter.rs | 44 ++++++++++++++++++++++++++++++++++++++++-- 6 files changed, 106 insertions(+), 19 deletions(-) diff --git a/src/btor2/parse.rs b/src/btor2/parse.rs index 426f250..5c29891 100644 --- a/src/btor2/parse.rs +++ b/src/btor2/parse.rs @@ -125,7 +125,7 @@ impl<'a> Parser<'a> { } else { self.require_at_least_n_tokens(line, tokens, 3)?; match op { - "ite" => { + "ite" | "write" => { // ternary ops Some(self.parse_ternary_op(line, tokens)?) } @@ -335,6 +335,7 @@ impl<'a> Parser<'a> { self.check_expr_type(inner, line, tpe)?; self.ctx.not(inner) } + "read" => self.ctx.array_read(a, b), other => panic!("unexpected binary op: {other}"), }; self.check_expr_type(e, line, tpe) @@ -354,6 +355,7 @@ impl<'a> Parser<'a> { todo!("Array ITE") } } + "write" => self.ctx.array_store(a, b, c), other => panic!("unexpected binary op: {other}"), }; self.check_expr_type(res, line, tpe) @@ -574,8 +576,10 @@ impl<'a> Parser<'a> { } "array" => { self.require_at_least_n_tokens(line, tokens, 5)?; - let index_width = self.parse_width_int(line, tokens[3], "array index width")?; - let data_width = self.parse_width_int(line, tokens[4], "array data width")?; + let index_tpe = self.get_tpe_from_id(line, tokens[3])?; + let data_tpe = self.get_tpe_from_id(line, tokens[4])?; + let index_width = index_tpe.get_bit_vector_width().unwrap(); + let data_width = data_tpe.get_bit_vector_width().unwrap(); self.type_map.insert( line_id, Type::Array(ArrayType { @@ -776,11 +780,11 @@ fn str_offset(needle: &str, haystack: &str) -> usize { const UNARY_OPS: [&str; 10] = [ "not", "inc", "dec", "neg", "redand", "redor", "redxor", "slice", "uext", "sext", ]; -const BINARY_OPS: [&str; 40] = [ +const BINARY_OPS: [&str; 41] = [ "iff", "implies", "sgt", "ugt", "sgte", "ugte", "slt", "ult", "slte", "ulte", "and", "nand", "nor", "or", "xnor", "xor", "rol", "ror", "sll", "sra", "srl", "add", "mul", "sdiv", "udiv", "smod", "srem", "urem", "sub", "saddo", "uaddo", "sdivo", "udivo", "smulo", "umulo", "ssubo", - "usubo", "concat", "eq", "neq", + "usubo", "concat", "eq", "neq", "read", ]; const TERNARY_OPS: [&str; 1] = ["ite"]; const OTHER_OPS: [&str; 17] = [ diff --git a/src/ir/expr.rs b/src/ir/expr.rs index 9c2c217..1654e25 100644 --- a/src/ir/expr.rs +++ b/src/ir/expr.rs @@ -136,6 +136,19 @@ pub trait ExprNodeConstruction: let width = e.get_bv_type(self).unwrap() + by; self.add_node(Expr::BVSignExt { e, by, width }) } + + fn array_store(&mut self, array: ExprRef, index: ExprRef, data: ExprRef) -> ExprRef { + self.add_node(Expr::ArrayStore { array, index, data }) + } + + fn array_read(&mut self, array: ExprRef, index: ExprRef) -> ExprRef { + let width = array.get_type(self).get_array_data_width().unwrap(); + self.add_node(Expr::BVArrayRead { + array, + index, + width, + }) + } } pub fn bv_value_fits_width(value: BVLiteralInt, width: WidthInt) -> bool { @@ -440,6 +453,20 @@ impl Type { Type::Array(_) => None, } } + + pub fn get_array_data_width(&self) -> Option { + match &self { + Type::BV(_) => None, + Type::Array(a) => Some(a.data_width), + } + } + + pub fn get_array_index_width(&self) -> Option { + match &self { + Type::BV(_) => None, + Type::Array(a) => Some(a.index_width), + } + } } impl std::fmt::Display for Type { diff --git a/src/ir/serialize.rs b/src/ir/serialize.rs index d9a54d9..a05e8fd 100644 --- a/src/ir/serialize.rs +++ b/src/ir/serialize.rs @@ -4,8 +4,7 @@ use super::{Context, Expr, ExprRef, GetNode}; use crate::ir::{ - count_expr_uses, is_usage_root_signal, SignalInfo, SignalKind, TransitionSystem, Type, - TypeCheck, + count_expr_uses, is_usage_root_signal, SignalKind, TransitionSystem, Type, TypeCheck, }; use std::io::Write; @@ -441,7 +440,7 @@ impl SerializableIrNode for Type { } } -fn inline_expr_for_transition_system(expr: &Expr, use_count: u32) -> bool { +fn inline_expr_for_transition_system(expr: &Expr, _use_count: u32) -> bool { let always_inline = expr.is_symbol() || expr.is_bv_lit(); // TODO: re-enable using the use_count for inlining decisions after we add a way to turn it off always_inline // || use_count <= 1 diff --git a/src/ir/type_check.rs b/src/ir/type_check.rs index 2d7a66a..92be20c 100644 --- a/src/ir/type_check.rs +++ b/src/ir/type_check.rs @@ -36,8 +36,8 @@ impl Type { } fn expect_array(&self, op: &str) -> Result { match self { - Type::BV(_) => Err(TypeCheckError { - msg: format!("{op} only works on arrays, not bit-vectors."), + Type::BV(w) => Err(TypeCheckError { + msg: format!("{op} needs to be an array, not a bv<{w}>."), }), Type::Array(tpe) => Ok(*tpe), } @@ -215,7 +215,9 @@ impl TypeCheck for Expr { index, width, } => { - let array_tpe = array.get_type(ctx).expect_array("array read")?; + let array_tpe = array + .get_type(ctx) + .expect_array("the first argument to the read operation")?; let index_width = index.get_type(ctx).expect_bv("array read index")?; if array_tpe.index_width != index_width { Err(TypeCheckError { @@ -259,11 +261,13 @@ impl TypeCheck for Expr { })) } Expr::ArrayEqual(a, b) => { - expect_same_size_arrays(ctx, "array equals", a, b)?; + expect_same_size_arrays(ctx, "the array equals operation", a, b)?; Ok(Type::BV(1)) } Expr::ArrayStore { array, index, data } => { - let tpe = array.get_type(ctx).expect_array("array store")?; + let tpe = array + .get_type(ctx) + .expect_array("the first argument to the store operation")?; index .get_type(ctx) .expect_bv_of(tpe.index_width, "array store index")?; @@ -273,7 +277,7 @@ impl TypeCheck for Expr { } Expr::ArrayIte { cond, tru, fals } => { cond.get_type(ctx).expect_bv_of(1, "ite condition")?; - expect_same_size_arrays(ctx, "ite branches", tru, fals) + expect_same_size_arrays(ctx, "both ite branches", tru, fals) } } } diff --git a/src/mc/smt.rs b/src/mc/smt.rs index a6ca178..8baf18f 100644 --- a/src/mc/smt.rs +++ b/src/mc/smt.rs @@ -361,7 +361,11 @@ where Expr::BVReduceOr(_) => todo!(), Expr::BVReduceAnd(_) => todo!(), Expr::BVReduceXor(_) => todo!(), - Expr::BVEqual(_, _) => todo!(), + Expr::BVEqual(a_ref, b_ref) => { + let a = convert_expr(smt_ctx, ctx, *a_ref, rename_sym); + let b = convert_expr(smt_ctx, ctx, *b_ref, rename_sym); + smt_ctx.eq(a, b) + } Expr::BVImplies(a_ref, b_ref) => { let a = convert_expr(smt_ctx, ctx, *a_ref, rename_sym); let b = convert_expr(smt_ctx, ctx, *b_ref, rename_sym); @@ -398,7 +402,11 @@ where Expr::BVSignedRem(_, _, _) => todo!(), Expr::BVUnsignedRem(_, _, _) => todo!(), Expr::BVSub(_, _, _) => todo!(), - Expr::BVArrayRead { .. } => todo!(), + Expr::BVArrayRead { array, index, .. } => { + let a = convert_expr(smt_ctx, ctx, *array, rename_sym); + let i = convert_expr(smt_ctx, ctx, *index, rename_sym); + smt_ctx.select(a, i) + } Expr::BVIte { cond, tru, fals } => { let c = convert_expr(smt_ctx, ctx, *cond, rename_sym); let t = convert_expr(smt_ctx, ctx, *tru, rename_sym); @@ -411,7 +419,12 @@ where } Expr::ArrayConstant { .. } => todo!(), Expr::ArrayEqual(_, _) => todo!(), - Expr::ArrayStore { .. } => todo!(), + Expr::ArrayStore { array, index, data } => { + let a = convert_expr(smt_ctx, ctx, *array, rename_sym); + let i = convert_expr(smt_ctx, ctx, *index, rename_sym); + let d = convert_expr(smt_ctx, ctx, *data, rename_sym); + smt_ctx.store(a, i, d) + } Expr::ArrayIte { .. } => todo!(), } } diff --git a/src/sim/interpreter.rs b/src/sim/interpreter.rs index dfae3d7..adffb7a 100644 --- a/src/sim/interpreter.rs +++ b/src/sim/interpreter.rs @@ -3,11 +3,24 @@ // author: Kevin Laeufer use crate::ir::*; -use crate::sim::ValueStore; +use crate::sim::{Value, ValueStore}; + +/// Specifies how to initialize states that do not have +#[derive(Debug, PartialEq, Copy, Clone)] +pub enum InitKind { + Zero, + Random, +} pub trait Simulator { + /// Load the initial state values. + fn init(&mut self, kind: InitKind); + /// Advance the state. fn step(&mut self); + + /// Change the value of an input + fn set_input(&mut self, input_id: usize, value: Value); } /// Interpreter based simulator for a transition system. @@ -15,18 +28,45 @@ pub struct Interpreter<'a> { ctx: &'a Context, sys: &'a TransitionSystem, state: ValueStore, + meta: Vec, +} + +/// Meta data for each expression. +#[derive(Debug, Clone, Copy)] +struct InterpreterMetaData {} + +impl Default for InterpreterMetaData { + fn default() -> Self { + Self {} + } } impl<'a> Interpreter<'a> { pub fn new(ctx: &'a Context, sys: &'a TransitionSystem) -> Self { + let use_counts = count_expr_uses(ctx, sys); let types = sys.states().map(|s| s.symbol.get_type(ctx)); let state = ValueStore::new(types); - Self { ctx, sys, state } + let mut meta = Vec::with_capacity(use_counts.len()); + meta.resize(use_counts.len(), InterpreterMetaData::default()); + Self { + ctx, + sys, + state, + meta, + } } } impl<'a> Simulator for Interpreter<'a> { + fn init(&mut self, kind: InitKind) { + todo!() + } + fn step(&mut self) { todo!() } + + fn set_input(&mut self, input_id: usize, value: Value) { + todo!() + } }