diff --git a/.gitignore b/.gitignore index 3b1ae089..679459d0 100644 --- a/.gitignore +++ b/.gitignore @@ -31,7 +31,9 @@ run_dir/ # Archived catalog-generation logic (kept locally, not checked in) scripts/_catalog_gen.py -scripts/__pycache__/ + +# Python +__pycache__ # Include images of waveforms in Brave New World bug readme !tests/fpga-debugging/axis-async-fifo-c4/*.png diff --git a/Cargo.toml b/Cargo.toml index fbc34bba..759ab37c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [workspace] resolver = "3" -members = ["bi", "interp", "protocols", "cli", "graph-interp"] +members = ["bi", "functional-models", "interp", "protocols", "cli", "graph-interp"] [workspace.package] @@ -13,6 +13,7 @@ license = "MIT" [workspace.dependencies] protocols = { path = "protocols" } +functional = { path = "functional-models" } baa = { version = "0.19.3", features = ["rand1"] } patronus = { git="https://github.com/Nikil-Shyamsunder/patronus#" } rand = "0.10" diff --git a/functional-models/Cargo.toml b/functional-models/Cargo.toml new file mode 100644 index 00000000..6460853c --- /dev/null +++ b/functional-models/Cargo.toml @@ -0,0 +1,18 @@ +[package] +name = "functional" +version = "0.1.0" +description = "load functional models generated by our python library" +edition.workspace = true +rust-version.workspace = true +repository.workspace = true +license.workspace = true + +[dependencies] +protocols.workspace = true +clap-verbosity-flag = "3.0.4" +clap.workspace = true +baa.workspace = true +patronus.workspace = true +rustc-hash.workspace = true +serde = { version = "1.0.229", features = ["derive"] } +serde_json = "1.0.151" diff --git a/functional-models/README.md b/functional-models/README.md new file mode 100644 index 00000000..d3317f10 --- /dev/null +++ b/functional-models/README.md @@ -0,0 +1,4 @@ +# Functional Models + +Define your functional model in `main.py`, export to JSON and +then load it using the rust library. diff --git a/functional-models/fun.py b/functional-models/fun.py new file mode 100644 index 00000000..1cb7409e --- /dev/null +++ b/functional-models/fun.py @@ -0,0 +1,134 @@ +import json +from dataclasses import dataclass, field +from typing import Optional, Tuple + +from pypatronus import ( + TransitionSystem, + State, + BitVec, + ExprRef, + BitVecVal, + If, + Interpreter, +) + + +@dataclass +class Method: + name: str + inputs: list[ExprRef] = field(default_factory=list) + outputs: list[Tuple[str, ExprRef]] = field(default_factory=list) + nexts: Optional[list[ExprRef]] = None + # indicates whether the method can be executed based on the current model state + guard: Optional[ExprRef] = None + + +@dataclass +class FunctionalModel: + name: str + methods: list[Method] = field(default_factory=list) + states: list[ExprRef] = field(default_factory=list) + + +class Sim: + def __init__(self, model: FunctionalModel): + self.sys = _build_sys(model) + self.model = model + self.sim = Interpreter(self.sys) + for idx, m in enumerate(model.methods): + # note: python lambdas capture the context instead of the value of idx be default which is why + # we need the nested lambdas! + setattr( + self, + m.name, + ( + lambda ii: ( + lambda *args, **kwargs: self._exec_method(ii, *args, **kwargs) + ) + )(idx), + ) + + def _exec_method(self, idx: int, *args, **kwargs): + assert len(kwargs) == 0, "TODO: support keyword args" + method = self.model.methods[idx] + inputs = list(args) + assert len(inputs) == len(method.inputs), ( + f"Wrong number of inputs {len(inputs)} != {len(method.inputs)}" + ) + + assert False, f"TODO: exec {method.name} {inputs}" + + +def verify_model(m: FunctionalModel): + for method in m.methods: + allowed_symbols = set(m.states) | set(method.inputs) + + for out_name, out_expr in method.outputs: + unallowed = out_expr.symbols() - allowed_symbols + assert len(unallowed) == 0, ( + f"Output {out_name}={out_expr} uses symbols that are neither inputs nor state: {unallowed}" + ) + + if method.nexts is not None: + assert len(method.nexts) == len(m.states), ( + f"[{method.name}] {len(method.nexts)} next state assignments, but model has {len(m.states)} states." + ) + for state, next in zip(m.states, method.nexts): + assert state.sort() == next.sort(), ( + f"[{method.name}] {state} : {state.sort()} = {next} : {next.sort()}" + ) + unallowed = next.symbols() - allowed_symbols + assert len(unallowed) == 0, ( + f"[{method.name}] State update {state}={next} uses symbols that are neither inputs nor state: {unallowed}" + ) + + # check guard + if method.guard is not None: + allowed_symbols = set(m.states) + unallowed = method.guard.symbols() - allowed_symbols + assert len(unallowed) == 0, ( + f"Guard {method.guard} uses symbols that are not state: {unallowed}" + ) + + +def _build_sys(m: FunctionalModel) -> TransitionSystem: + verify_model(m) + sys = TransitionSystem(name=m.name) + next_states = list(m.states) + for t in m.methods: + commit_signal = BitVec(f"{t.name}_commit", 1) + sys.add_input(commit_signal) + guard_signal = BitVecVal(1, 1) if t.guard is None else t.guard + sys.add_output(f"{t.name}_guard", guard_signal) + input_map = {} + for inp in t.inputs: + renamed = BitVec(f"{t.name}_in_{inp.name()}", inp.width()) + input_map[inp] = renamed + sys.add_input(renamed) + for out_name, out_expr in t.outputs: + out_expr = out_expr.replace(input_map) + sys.add_output(f"{t.name}_out_{out_name}", out_expr) + if t.nexts is not None: + for idx, next in enumerate(t.nexts): + expr = next.replace(input_map) + next_states[idx] = If(commit_signal, expr, next_states[idx]) + assert len(next_states) == len(m.states) + sys.states = [ + State(sym.name(), next=next) for (sym, next) in zip(m.states, next_states) + ] + return sys + + +def serialize(m: FunctionalModel, filename): + sys = _build_sys(m) + + info = { + "name": m.name, + "methods": [t.name for t in m.methods], + "states": [s.name() for s in m.states], + } + + print(sys) + + with open(filename, "w") as f: + json.dump({"info": info, "sys": sys.to_btor2_str()}, f) diff --git a/functional-models/main.py b/functional-models/main.py new file mode 100644 index 00000000..891390e0 --- /dev/null +++ b/functional-models/main.py @@ -0,0 +1,125 @@ +# Copyright 2026 Cornell University +# released under MIT License +# author: Kevin Laeufer + +from pypatronus import BitVec, SignExt, ZeroExt, Slice, Update, If, Array, BitVecVal +from fun import FunctionalModel, Method, serialize, Sim + + +def picorv32_pcpi_mul(): + """ + https://github.com/ekiwi/paso/blob/ad2bf83f420ca704ff0e76e7a583791a0e80a545/benchmarks/src/benchmarks/picorv32/PicoRV32Spec.scala#L8 + """ + m = FunctionalModel(name="picorv32_pcpi_mul") + rs1, rs2 = BitVec("rs1_data", 32), BitVec("rs2_data", 32) + m.methods = [ + Method("pcpi_mul", [rs1, rs2], [("rd_data", rs1 * rs2)]), + Method( + "pcpi_mulh", + [rs1, rs2], + [("rd_data", Slice(63, 32, SignExt(32, rs1) * SignExt(32, rs2)))], + ), + Method( + "pcpi_mulhu", + [rs1, rs2], + [("rd_data", Slice(63, 32, ZeroExt(32, rs1) * ZeroExt(32, rs2)))], + ), + Method( + "pcpi_mulhsu", + [rs1, rs2], + [("rd_data", Slice(63, 32, SignExt(32, rs1) * ZeroExt(32, rs2)))], + ), + Method("pcpi_mul_reset"), + Method("idle"), + ] + return m + + +def fifo(data_width: int, num_elements: int, push_pop: bool = False): + """https://github.com/ekiwi/paso/blob/ad2bf83f420ca704ff0e76e7a583791a0e80a545/benchmarks/src/benchmarks/fifo/FifoSpec.scala""" + counter_width = 12 + assert num_elements < ((1 << (counter_width - 1)) - 1) + mem = Array("mem", counter_width, data_width) + count = BitVec("count", counter_width) + read = BitVec("read", counter_width) + m = FunctionalModel(name="fifo", states=[mem, count, read]) + num_elements_bv = BitVecVal(num_elements, counter_width) + full = count.equals(num_elements_bv) + zero = BitVecVal(0, counter_width) + empty = count.equals(zero) + input = BitVec("input", data_width) + + non_wrap = count + read + write_adr = If(non_wrap < num_elements_bv, non_wrap, non_wrap - num_elements_bv) + read_plus_one = read + BitVecVal(1, counter_width) + read_incr = If( + read_plus_one.equals(num_elements_bv), + zero, + read_plus_one, + ) + + m.methods = [ + Method( + "push", + [input], + [], + [ + Update(mem, write_adr, input), # mem + count + BitVecVal(1, counter_width), # count + read, # read + ], + ~full, + ), + Method( + "pop", + [], + [("output", mem[read])], + [ + mem, # mem + count - BitVecVal(1, counter_width), # count + read_incr, # read + ], + ~empty, + ), + Method("reset", nexts=[mem, zero, zero]), + Method("idle"), + ] + if push_pop: + m.methods.append( + Method( + "push_pop", + [input], + [("output", mem[read])], + [ + Update(mem, write_adr, input), # mem + count, # count + read_incr, # read + ], + ), + ) + return m + + +def test_fifo(m: FunctionalModel, num_elements: int, push_pop: bool = False): + sim = Sim(m) + # sim.push(123) + # assert sim.pop() == 123 + pass # TODO: implement simulator for testing + + +def main(): + serialize(picorv32_pcpi_mul(), "picorv32_pcpi_mul.json") + params = [ + {"data_width": 32, "num_elements": 8}, + {"data_width": 32, "num_elements": 16}, + {"data_width": 32, "num_elements": 128}, + ] + for p in params: + file_name = "fifo_" + "_".join(f"{k}={v}" for k, v in p.items()) + ".json" + m = fifo(**p) + test_fifo(m, num_elements=p["num_elements"]) + serialize(m, file_name) + + +if __name__ == "__main__": + main() diff --git a/functional-models/pyproject.toml b/functional-models/pyproject.toml new file mode 100644 index 00000000..daf1593b --- /dev/null +++ b/functional-models/pyproject.toml @@ -0,0 +1,9 @@ +[project] +name = "functional-models" +version = "0.1.0" +description = "Add your description here" +readme = "README.md" +requires-python = ">=3.12" +dependencies = [ + "pypatronus==0.39.6", +] diff --git a/functional-models/src/lib.rs b/functional-models/src/lib.rs new file mode 100644 index 00000000..8d7d755e --- /dev/null +++ b/functional-models/src/lib.rs @@ -0,0 +1,312 @@ +// Copyright 2026 Cornell University +// released under MIT License +// author: Kevin Laeufer + +use baa::{BitVecOps, BitVecValue, WidthInt}; +use patronus::expr::{Context, ExprRef, TypeCheck}; +use patronus::sim::{InitKind, Simulator}; +use patronus::system::{Output, TransitionSystem}; +use protocols::Value; +use rustc_hash::FxHashMap; +use serde::{Deserialize, Serialize}; +use std::ops::Index; +use std::path::Path; + +#[derive(Debug)] +pub struct FunctionalModel { + sys: TransitionSystem, + method_names: FxHashMap, + methods: Vec, +} + +#[derive(Debug, Copy, Clone, Eq, PartialEq)] +pub struct MethodId(u32); + +impl From for usize { + fn from(value: MethodId) -> Self { + value.0 as usize + } +} + +#[derive(Debug, Copy, Clone, Eq, PartialEq)] +pub struct ParameterId { + method: MethodId, + index: u16, + is_input: bool, + width: WidthInt, +} + +impl ParameterId { + pub fn width(&self) -> WidthInt { + self.width + } +} + +impl ParameterId { + pub fn is_input(&self) -> bool { + self.is_input + } +} + +#[derive(Debug)] +pub struct Method { + id: MethodId, + name: String, + guard: ExprRef, + commit: ExprRef, + inputs: Vec<(String, WidthInt, ExprRef)>, + outputs: Vec<(String, WidthInt, ExprRef)>, +} + +impl Method { + pub fn parameter_id(&self, name: &str) -> Option { + if let Some(idx) = self.inputs.iter().position(|(n, _, _)| n == name) { + Some(ParameterId { + method: self.id, + is_input: true, + index: idx as u16, + width: self.inputs[idx].1, + }) + } else { + self.outputs + .iter() + .position(|(n, _, _)| n == name) + .map(|idx| ParameterId { + method: self.id, + is_input: false, + index: idx as u16, + width: self.outputs[idx].1, + }) + } + } + + pub fn name(&self) -> &str { + &self.name + } +} + +impl FunctionalModel { + pub fn load(ctx: &mut Context, reader: &mut impl std::io::BufRead) -> std::io::Result { + let m: FunctionalModelJson = serde_json::from_reader(reader)?; + let sys = patronus::btor2::parse_str(ctx, &m.sys, Some(&m.info.name)).unwrap(); + + let methods: Vec<_> = m + .info + .methods + .into_iter() + .enumerate() + .map(|(idx, name)| { + let id = MethodId(idx as u32); + let guard = sys + .lookup_output(ctx, &format!("{name}_guard")) + .expect("Failed to find guard output."); + let commit = sys + .lookup_input(ctx, &format!("{name}_commit")) + .expect("Failed to find commit input."); + let input_prefix = format!("{name}_in_"); + let inputs = sys + .inputs + .iter() + .filter_map(|i| { + ctx.get_symbol_name(*i) + .and_then(|name| name.strip_prefix(&input_prefix)) + .map(|name| (name.to_string(), i.get_bv_type(ctx).unwrap(), *i)) + }) + .collect(); + let output_prefix = format!("{name}_out_"); + let outputs = sys + .outputs + .iter() + .filter_map(|o| { + ctx[o.name].strip_prefix(&output_prefix).map(|name| { + (name.to_string(), o.expr.get_bv_type(ctx).unwrap(), o.expr) + }) + }) + .collect(); + Method { + id, + name, + guard, + commit, + inputs, + outputs, + } + }) + .collect(); + let method_names = methods + .iter() + .enumerate() + .map(|(idx, m)| (m.name.to_string(), MethodId(idx as u32))) + .collect(); + Ok(Self { + sys, + methods, + method_names, + }) + } + + pub fn name(&self) -> &str { + &self.sys.name + } + + pub fn sys(&self) -> &TransitionSystem { + &self.sys + } + + pub fn method_id(&self, name: &str) -> Option { + self.method_names.get(name).cloned() + } + + pub fn method(&self, name: &str) -> Option<&Method> { + self.method_id(name).map(|id| &self[id]) + } +} + +impl Index for FunctionalModel { + type Output = Method; + + fn index(&self, index: MethodId) -> &Self::Output { + &self.methods[index.0 as usize] + } +} + +pub struct FunctionalModelSimulator { + model: FunctionalModel, + sim: patronus::sim::Interpreter, + tru: BitVecValue, + fals: BitVecValue, + init_snapshot: u32, +} + +impl FunctionalModelSimulator { + pub fn from_file(filename: impl AsRef) -> std::io::Result { + let file = std::fs::File::open(filename)?; + let mut reader = std::io::BufReader::new(file); + Self::load(&mut reader) + } + + pub fn load(reader: &mut impl std::io::BufRead) -> std::io::Result { + let mut ctx = Context::default(); + let model = FunctionalModel::load(&mut ctx, reader)?; + Ok(Self::new(&ctx, model)) + } + + pub fn new(ctx: &Context, model: FunctionalModel) -> Self { + let mut sim = patronus::sim::Interpreter::new(ctx, &model.sys); + sim.init(InitKind::Zero); + let init_snapshot = sim.take_snapshot(); + let tru = BitVecValue::from_bool(true); + let fals = BitVecValue::from_bool(false); + Self { + sim, + model, + tru, + fals, + init_snapshot, + } + } + + pub fn name(&self) -> &str { + self.model.name() + } + + pub fn model(&self) -> &FunctionalModel { + &self.model + } + + pub fn guard(&self, method: MethodId) -> bool { + let e = self.model[method].guard; + let bv: BitVecValue = self.sim.get(e).try_into().unwrap(); + bv.is_bit_set(0) + } + + pub fn commit(&mut self, method: MethodId) { + let e = self.model[method].commit; + debug_assert!(self.guard(method), "method is not available!"); + self.sim.set(e, &self.tru); + self.sim.step(); + self.sim.set(e, &self.fals); + } + + pub fn set_input(&mut self, param: ParameterId, value: &Value) { + assert!(param.is_input()); + let (width, e) = self.param_id_to_width_and_e(param); + if let Ok(bv) = BitVecValue::try_from(value.clone()) { + debug_assert_eq!(width, bv.width()); + self.sim.set(e, &bv); + } else { + todo!("Deal with non-scalar values.") + } + } + + /// get the value of an input or output parameter + pub fn get(&self, param: ParameterId) -> Value { + let (width, e) = self.param_id_to_width_and_e(param); + if let Ok(bv) = BitVecValue::try_from(self.sim.get(e)) { + debug_assert_eq!(width, bv.width()); + bv.into() + } else { + todo!() + } + } + + fn param_id_to_width_and_e(&self, param: ParameterId) -> (WidthInt, ExprRef) { + let (_, width, e) = if param.is_input() { + &self.model[param.method].inputs[param.index as usize] + } else { + &self.model[param.method].outputs[param.index as usize] + }; + (*width, *e) + } + + pub fn reset(&mut self) { + self.sim.restore_snapshot(self.init_snapshot); + } +} + +#[derive(Debug)] +pub struct Transaction { + pub name: String, + pub commit: Vec, + pub inputs: Vec, + pub outputs: Vec, +} + +#[derive(Debug, Deserialize, Serialize)] +struct FunctionalModelJson { + info: FunctionalModelInfoJson, + sys: String, +} + +#[derive(Debug, Deserialize, Serialize)] +struct FunctionalModelInfoJson { + name: String, + methods: Vec, + states: Vec, +} + +#[cfg(test)] +pub mod tests { + use super::*; + + const MUL_JSON: &[u8] = r##"{"info": {"name": "picorv32_pcpi_mul", "methods": ["pcpi_mul", "pcpi_mulh", "pcpi_mulhu", "pcpi_mulhsu"], "states": []}, "sys": "; btor2 description of `picorv32_pcpi_mul` generated by patronus 0.39.4\n1 sort bitvec 1\n2 input 1 pcpi_mul_commit\n3 sort bitvec 32\n4 input 3 pcpi_mul_in_rs1_data\n5 input 3 pcpi_mul_in_rs2_data\n6 input 1 pcpi_mulh_commit\n7 input 3 pcpi_mulh_in_rs1_data\n8 input 3 pcpi_mulh_in_rs2_data\n9 input 1 pcpi_mulhu_commit\n10 input 3 pcpi_mulhu_in_rs1_data\n11 input 3 pcpi_mulhu_in_rs2_data\n12 input 1 pcpi_mulhsu_commit\n13 input 3 pcpi_mulhsu_in_rs1_data\n14 input 3 pcpi_mulhsu_in_rs2_data\n15 one 1\n16 output 15 pcpi_mul_guard\n17 mul 3 4 5\n18 output 17 pcpi_mul_out_rd_data\n19 output 15 pcpi_mulh_guard\n20 sort bitvec 64\n21 sext 20 7 32\n22 sext 20 8 32\n23 mul 20 21 22\n24 slice 3 23 63 32\n25 output 24 pcpi_mulh_out_rd_data\n26 output 15 pcpi_mulhu_guard\n27 uext 20 10 32\n28 uext 20 11 32\n29 mul 20 27 28\n30 slice 3 29 63 32\n31 output 30 pcpi_mulhu_out_rd_data\n32 output 15 pcpi_mulhsu_guard\n33 sext 20 13 32\n34 uext 20 14 32\n35 mul 20 33 34\n36 slice 3 35 63 32\n37 output 36 pcpi_mulhsu_out_rd_data\n"}"##.as_bytes(); + + #[test] + fn test_load_mul_json() { + let mut ctx = Context::default(); + let m = FunctionalModel::load(&mut ctx, &mut std::io::Cursor::new(MUL_JSON)).unwrap(); + assert_eq!(m.name(), "picorv32_pcpi_mul"); + for name in ["pcpi_mul", "pcpi_mulh", "pcpi_mulhu", "pcpi_mulhsu"] { + let method = m.method(name).unwrap(); + assert_eq!(method.inputs[0].0, "rs1_data"); + assert_eq!(method.inputs[1].0, "rs2_data"); + assert_eq!(method.outputs[0].0, "rd_data"); + assert_eq!(method.guard, ctx.get_true()); + } + } + + #[test] + fn test_sim() { + let _sim = FunctionalModelSimulator::load(&mut std::io::Cursor::new(MUL_JSON)).unwrap(); + } +} diff --git a/interp/Cargo.toml b/interp/Cargo.toml index 60e499db..5fb51a47 100644 --- a/interp/Cargo.toml +++ b/interp/Cargo.toml @@ -13,3 +13,7 @@ clap.workspace = true clap-verbosity-flag = "3.0.4" env_logger = "0.11.8" anyhow.workspace = true +functional.workspace = true +patronus.workspace = true +rand.workspace = true +baa.workspace = true diff --git a/interp/src/main.rs b/interp/src/main.rs index ca1a1b6c..48ea9409 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -2,14 +2,21 @@ // released under MIT License // author: Ernest Ng +use baa::BitVecValue; use clap::{ColorChoice, Parser}; use clap_verbosity_flag::log::LevelFilter; use clap_verbosity_flag::{Verbosity, WarnLevel}; +use functional::{FunctionalModel, FunctionalModelSimulator, MethodId, ParameterId}; use protocols::ascii_waveform::print_ascii_waveform; use protocols::frontend::diagnostic::DiagnosticHandler; -use protocols::frontend::require_single_module; -use protocols::scheduler::Scheduler; -use protocols::{PatronusSim, frontend, transaction_frontend}; +use protocols::frontend::symbol::SymbolTable; +use protocols::frontend::{Module, require_single_module}; +use protocols::scheduler::{Invocation, Scheduler}; +use protocols::transactions::Traces; +use protocols::{PatronusSim, Value, frontend, transaction_frontend}; +use rand::SeedableRng; +use rand::prelude::StdRng; +use rand::seq::IndexedRandom; /// Args for the interpreter CLI #[derive(Parser, Debug)] @@ -29,7 +36,7 @@ struct Cli { /// Path to a Transactions (.tx) file #[arg(short, long, value_name = "TRANSACTIONS_FILE")] - transactions: String, + transactions: Option, /// Name of the top-level module (if one exists) #[arg(short, long, value_name = "MODULE_NAME")] @@ -39,6 +46,15 @@ struct Cli { #[arg(short, long, value_name = "WAVEFORM_FILE")] fst: Option, + /// Functional model JSON file. (optional) + #[arg(long)] + functional_model: Option, + + /// Number of transactions to randomly generate from the functional model. + /// These will be appended to any transactions loaded from the transaction file. + #[arg(long, default_value_t = 0)] + num_random_transactions: u32, + /// Users can specify `-v` or `--verbose` to toggle logging #[command(flatten)] verbosity: Verbosity, @@ -149,23 +165,14 @@ fn main() -> anyhow::Result<()> { let module = require_single_module(modules, &cli.protocol)?; // Create a separate `DiagnosticHandler` when parsing the transactions file - let mut transactions_handler = DiagnosticHandler::new( + let transactions_handler = DiagnosticHandler::new( color_choice, cli.no_error_locations, emit_warnings, cli.display_hex, ); - let traces = match transaction_frontend( - cli.transactions, - &st, - &module.protos, - &mut transactions_handler, - ) { - Ok(result) => result, - Err(error) => { - exit_after_setup_error(error, !transactions_handler.error_string().is_empty()) - } - }; + let mut trace_rng = StdRng::seed_from_u64(0); + let traces = load_traces(&cli, transactions_handler, &st, &module, &mut trace_rng); let mut any_failed = false; for (trace_index, todos) in traces.into_iter().enumerate() { @@ -216,3 +223,177 @@ fn main() -> anyhow::Result<()> { } Ok(()) } + +fn load_traces( + cli: &Cli, + mut transactions_handler: DiagnosticHandler, + st: &SymbolTable, + module: &Module, + rng: &mut impl rand::Rng, +) -> Traces { + let mut traces = if let Some(t) = cli.transactions.as_deref() { + match transaction_frontend(t, st, &module.protos, &mut transactions_handler) { + Ok(result) => result, + Err(error) => { + exit_after_setup_error(error, !transactions_handler.error_string().is_empty()) + } + } + } else { + vec![] + }; + + if let Some(fun) = cli.functional_model.as_deref() { + let mut sim = + FunctionalModelSimulator::from_file(fun).expect("failed to load functional model"); + let map = FunMap::new(st, sim.model(), module); + // 1) verify existing traces + for trace in &traces { + verify_trace(&mut sim, &map, trace, cli.display_hex); + } + + // 2) generate a new trace + let trace = sample_functional_model(&mut sim, &map, cli.num_random_transactions, rng); + if !trace.is_empty() { + traces.push(trace); + } + } else { + assert_eq!( + cli.num_random_transactions, 0, + "cannot generate random transactions without a functional model" + ); + } + + traces +} + +fn sample_functional_model( + sim: &mut FunctionalModelSimulator, + map: &FunMap, + num: u32, + rng: &mut impl rand::Rng, +) -> Vec { + sim.reset(); + let mut out = Vec::with_capacity(num as usize); + for _ in 0..num { + // pick method + let available: Vec<_> = map.methods().iter().filter(|m| sim.guard(**m)).collect(); + assert!(!available.is_empty()); + if let Some(&&method) = available.choose(rng) { + // generate and apply inputs + for &p in map.params(method) { + if p.is_input() { + let value: Value = BitVecValue::random(rng, p.width()).into(); + sim.set_input(p, &value) + } + } + // read all values + let args: Vec = map.params(method).iter().map(|&p| sim.get(p)).collect(); + // commit + sim.commit(method); + out.push((sim.model()[method].name().to_string(), args)); + } else { + panic!( + "Cannot generate invocation #{}, because none of the methods have active guards.", + out.len() + 1 + ); + } + } + out +} + +fn verify_trace( + sim: &mut FunctionalModelSimulator, + map: &FunMap, + trace: &[Invocation], + display_hex: bool, +) { + sim.reset(); + for (name, args) in trace { + if let Some(method) = sim.model().method_id(name) { + assert!(sim.guard(method), "Transaction {name} cannot be executed"); + let params = map.params(method); + debug_assert_eq!(params.len(), args.len()); + for (p, a) in params.iter().zip(args.iter()) { + if p.is_input() { + sim.set_input(*p, a); + } + } + for (p, a) in params.iter().zip(args.iter()) { + if !p.is_input() { + let actual = sim.get(*p); + assert_eq!( + &actual, + a, + "Transaction {name} is supposed to produce {}, but the functional model indicates that is should produce {}", + a.to_string(display_hex), + actual.to_string(display_hex) + ); + } + } + sim.commit(method); + } else { + panic!( + "Unknown transaction {name}. Not part of the functional model {}", + sim.name() + ); + } + } +} + +struct FunMap { + params: Vec>, + methods: Vec, +} + +impl FunMap { + fn new(st: &SymbolTable, model: &FunctionalModel, module: &Module) -> Self { + let mut params = vec![]; + let mut methods = vec![]; + for proto in &module.protos { + if let Some(method_id) = model.method_id(&proto.name) { + methods.push(method_id); + let idx: usize = method_id.into(); + if idx >= params.len() { + params.resize(idx + 1, vec![]); + } + let method = &model[method_id]; + params[idx] = proto + .args + .iter() + .map(|arg| { + let sym = &st[arg.symbol()]; + if let Some(p) = method.parameter_id(sym.name()) { + p + } else { + panic!( + "Method {} is missing parameter `{}`", + proto.name, + sym.name() + ); + } + }) + .collect(); + } else { + panic!( + "Functional model {} is missing a method for protocol `{}` from {}.", + model.name(), + proto.name, + module.name + ); + } + } + + Self { params, methods } + } + + /// The parameters of a given method in the same order as the args of the corresponding protocol. + fn params(&self, method: MethodId) -> &[ParameterId] { + &self.params[usize::from(method)] + } + + /// The methods in the functional model in the same order as the corresponding protocol in the + /// module. + fn methods(&self) -> &[MethodId] { + &self.methods + } +} diff --git a/protocols/src/value.rs b/protocols/src/value.rs index 3d496fe2..2f3f1aa9 100644 --- a/protocols/src/value.rs +++ b/protocols/src/value.rs @@ -9,10 +9,30 @@ use baa::{BitVecOps, BitVecValue}; /// A concrete value of any type. -#[derive(Debug, Clone)] +#[derive(Debug, Clone, Eq, PartialEq)] pub struct Value(ValueKind); -#[derive(Debug, Clone)] +impl Value { + pub fn to_string(&self, display_hex: bool) -> String { + match &self.0 { + ValueKind::Scalar(v) => bv_to_string(v, display_hex), + ValueKind::Seq(v) => { + let entries: Vec<_> = v.iter().map(|e| bv_to_string(e, display_hex)).collect(); + format!("[{}]", entries.join(", ")) + } + } + } +} + +fn bv_to_string(value: &BitVecValue, display_hex: bool) -> String { + if display_hex { + format!("0x{}", value.to_hex_str()) + } else { + value.to_dec_str() + } +} + +#[derive(Debug, Clone, Eq, PartialEq)] enum ValueKind { Scalar(BitVecValue), Seq(Vec), @@ -116,11 +136,7 @@ impl SymBitVecValue { pub fn to_string(&self, display_hex: bool) -> String { if self.known.is_all_ones() { - if display_hex { - format!("0x{}", self.value.to_hex_str()) - } else { - self.value.to_dec_str() - } + bv_to_string(&self.value, display_hex) } else if self.known.is_zero() { // TODO: do we actually want to keep this behavior? "X".to_string() diff --git a/pyproject.toml b/pyproject.toml index 83fd56f5..c7b57668 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -11,3 +11,8 @@ dev = [ "ruff>=0.15.1", "ty>=0.0.17", ] + +[tool.uv.workspace] +members = [ + "functional-models", +] diff --git a/uv.lock b/uv.lock index f1f647a9..d34c42b9 100644 --- a/uv.lock +++ b/uv.lock @@ -2,6 +2,23 @@ version = 1 revision = 3 requires-python = ">=3.12" +[manifest] +members = [ + "functional-models", + "protocols", +] + +[[package]] +name = "functional-models" +version = "0.1.0" +source = { virtual = "functional-models" } +dependencies = [ + { name = "pypatronus" }, +] + +[package.metadata] +requires-dist = [{ name = "pypatronus", specifier = "==0.39.6" }] + [[package]] name = "protocols" version = "0.1.0" @@ -21,6 +38,30 @@ dev = [ { name = "ty", specifier = ">=0.0.17" }, ] +[[package]] +name = "pypatronus" +version = "0.39.6" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/cd/85/e410a6b325d785c3d972afaca878133014897982b1530d68dbbf6ee4d73c/pypatronus-0.39.6.tar.gz", hash = "sha256:e6e12b2424d615b991dc7af64fe5a8fd30cf9df561532a0bf269095eadd94ace", size = 166087, upload-time = "2026-09-28T20:33:53.254Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/9f/0a/29baaaee767a80ed8982aaaee2addf7cf6afe118f4a7e283a81e64d697bd/pypatronus-0.39.6-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:49d80ce4aa5940e0d0f9c393af95decadba685984b834e988c81feafe22a4585", size = 1369317, upload-time = "2026-09-28T20:33:48.129Z" }, + { url = "https://files.pythonhosted.org/packages/44/3e/2afdedbe5b7a2392dbdb4282d8aa1e68cac588eefee6a2b3bc113e7a87ea/pypatronus-0.39.6-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:f427e8941f1ccdd0b0cdb2769e7c03f0d4697907f18bff9da106f91d0d5465a8", size = 1315216, upload-time = "2026-09-28T20:33:40.127Z" }, + { url = "https://files.pythonhosted.org/packages/ac/5a/6534999bd1b5fce10d1a00d94294c46160beb93e8ac49875f35d797baf9b/pypatronus-0.39.6-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:59c37c4d10441c45890aafe86d0f788064bcece288bc4327d926ca8a8363f944", size = 11461735, upload-time = "2026-09-28T20:33:02.393Z" }, + { url = "https://files.pythonhosted.org/packages/a9/9a/065a980897c626297415c4e661e9a8ef7cc1a79dea80b68551932536c2cd/pypatronus-0.39.6-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:57bfdd3708f1381d9b1344ee505c7d56b0763f4d5b542a1c5237fd3073c517b4", size = 12893120, upload-time = "2026-09-28T20:33:19.827Z" }, + { url = "https://files.pythonhosted.org/packages/26/c2/d9fe790d27c8697c18455d7b5d32a47021d94a10359d21405e7096152c5b/pypatronus-0.39.6-cp313-cp313-macosx_10_12_x86_64.whl", hash = "sha256:e523531200d65d6d739fc7793340e12623f10b591178c8342331ca80a870e150", size = 1368247, upload-time = "2026-09-28T20:33:49.713Z" }, + { url = "https://files.pythonhosted.org/packages/ee/bd/05c2bfa7da1e5ca8cb1c9d0de1ab15d1e0ffc45681f3b0e6b71644dc8a85/pypatronus-0.39.6-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:7a288550ced1c6ab6c605866447439228132e70ae1a6de18896467c6c82dad92", size = 1314683, upload-time = "2026-09-28T20:33:41.803Z" }, + { url = "https://files.pythonhosted.org/packages/b8/d4/63992b9ce8b61a4a1cc07dd09897bcf2bee28b9773aaed201875a7855fd2/pypatronus-0.39.6-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:bf41eae6a93aeb0a2833e545fa4c7bdb9c7238e3ac76351a2472676e714b1725", size = 11461964, upload-time = "2026-09-28T20:33:04.647Z" }, + { url = "https://files.pythonhosted.org/packages/53/c0/95a2a9f1af211fbdb3c513137c8d36ca73ebe4c923ef45c352bae02070cc/pypatronus-0.39.6-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d68fc25825396671ce9e78bb957097c2ac7775aac51989a2eb36824aa1ca68cb", size = 12879933, upload-time = "2026-09-28T20:33:22.277Z" }, + { url = "https://files.pythonhosted.org/packages/60/9b/9b08580ecbdcab0ad1fa09a56803d5d498ac0a16a94c4cf9056f5c5ce90e/pypatronus-0.39.6-cp314-cp314-macosx_10_12_x86_64.whl", hash = "sha256:3b66b2a7219a69a82608477fed2db9a008be0a56da12799ec0136c8930ee22d9", size = 1369875, upload-time = "2026-09-28T20:33:51.932Z" }, + { url = "https://files.pythonhosted.org/packages/d8/44/1f99e3b2719d4f8ab89b9161b5d8abc7b30180cef02174cb27c58df60aad/pypatronus-0.39.6-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:4a71b25176b43c0da296001e36c8844d0e16a393fefe14933095f8559778e521", size = 1315648, upload-time = "2026-09-28T20:33:43.259Z" }, + { url = "https://files.pythonhosted.org/packages/6c/48/99c56ca7822e49f9b8f30564534386abd1901d5abff687b6a62c72938a29/pypatronus-0.39.6-cp314-cp314-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:7da76e07d964cb89ce5a31d1e588ca9d5c479b3d3c466d0dd9b8be2e2220680f", size = 11470857, upload-time = "2026-09-28T20:33:07.36Z" }, + { url = "https://files.pythonhosted.org/packages/0d/bb/e93ee9569de4c760b98947cce80bfdbd63434d0a0326c89d2aa30a4c9c7d/pypatronus-0.39.6-cp314-cp314-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e20c3db284e858429dd242f064f226229a1bd8e83a0d995dcda43a6ce551ba68", size = 12898658, upload-time = "2026-09-28T20:33:24.741Z" }, + { url = "https://files.pythonhosted.org/packages/19/4d/b530a6480c8517af372807f90c0392cfbf05eb44bb98fa6da290e845a6cd/pypatronus-0.39.6-cp314-cp314t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:991cfdb0a835ba949b9838476ba4113566e62d7e2fca2fc414c1f33cd7c6168d", size = 11448543, upload-time = "2026-09-28T20:33:09.915Z" }, + { url = "https://files.pythonhosted.org/packages/46/99/30b72c81569dff0df6119ffdc12c9648d22332c0e82559301be954955d6a/pypatronus-0.39.6-cp314-cp314t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:aeb6a1aa38f1d8de5157633cb2484c6789121852219fb113b0c33ca00b6e244d", size = 12878008, upload-time = "2026-09-28T20:33:27.455Z" }, + { url = "https://files.pythonhosted.org/packages/9f/77/81fa121d8c10ca6dce74bac9ff0ab751d42e78c165e4503ee410775a6562/pypatronus-0.39.6-cp315-cp315-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fa95bb311e5d2f9cc224bb958aa7475d89b268420e447d88c015aad58d8ecd3e", size = 12897710, upload-time = "2026-09-28T20:33:30.023Z" }, + { url = "https://files.pythonhosted.org/packages/59/73/dd8bc9350163762dbbf4b52287c15023dc6ff80a097f877dbe4e6c19dd73/pypatronus-0.39.6-cp315-cp315t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d64dddd65ee6ee86a12c7c729aeed0a39a9333088c2e4baddcd09004a0faf600", size = 12884091, upload-time = "2026-09-28T20:33:32.571Z" }, +] + [[package]] name = "ruff" version = "0.15.1"