From 231bda58e347355a104bd1b50890f08b83010126 Mon Sep 17 00:00:00 2001 From: Omkar Bhalerao Date: Wed, 20 Mar 2024 13:22:18 -0400 Subject: [PATCH] Add infrastructure for integrating BTOR2 interpreter into Calyx (#1972) Add interface for BTOR2 interpreter into Calyx, add test primitive using the interface, confirm that executing the primitive using cider2 results in desired output. --- .gitignore | 3 + .vscode/settings.json | 4 +- Cargo.lock | 270 ++++++- Cargo.toml | 1 + Dockerfile | 3 + interp/Cargo.toml | 2 + interp/src/flatten/primitives/btor2_prim.rs | 64 ++ interp/src/flatten/primitives/builder.rs | 4 +- interp/src/flatten/primitives/mod.rs | 1 + tools/btor2/btor2i/Cargo.toml | 17 + tools/btor2/btor2i/Makefile | 18 + tools/btor2/btor2i/README.md | 33 + tools/btor2/btor2i/benchmark.toml | 37 + tools/btor2/btor2i/src/bvec.rs | 718 +++++++++++++++++++ tools/btor2/btor2i/src/cli.rs | 22 + tools/btor2/btor2i/src/error.rs | 33 + tools/btor2/btor2i/src/interp.rs | 544 ++++++++++++++ tools/btor2/btor2i/src/lib.rs | 6 + tools/btor2/btor2i/src/main.rs | 92 +++ tools/btor2/btor2i/src/program.rs | 124 ++++ tools/btor2/btor2i/src/shared_env.rs | 746 ++++++++++++++++++++ 21 files changed, 2737 insertions(+), 5 deletions(-) create mode 100644 interp/src/flatten/primitives/btor2_prim.rs create mode 100644 tools/btor2/btor2i/Cargo.toml create mode 100644 tools/btor2/btor2i/Makefile create mode 100644 tools/btor2/btor2i/README.md create mode 100644 tools/btor2/btor2i/benchmark.toml create mode 100644 tools/btor2/btor2i/src/bvec.rs create mode 100644 tools/btor2/btor2i/src/cli.rs create mode 100644 tools/btor2/btor2i/src/error.rs create mode 100644 tools/btor2/btor2i/src/interp.rs create mode 100644 tools/btor2/btor2i/src/lib.rs create mode 100644 tools/btor2/btor2i/src/main.rs create mode 100644 tools/btor2/btor2i/src/program.rs create mode 100644 tools/btor2/btor2i/src/shared_env.rs diff --git a/.gitignore b/.gitignore index 50e88d317c..332526c53f 100644 --- a/.gitignore +++ b/.gitignore @@ -50,3 +50,6 @@ results.xml !cider-dap/calyxDebug/package.json !cider-dap/calyxDebug/tsconfig.json + +# btor2i ignore +tools/btor2/btor2i/build/ \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json index f86c86fa69..500304fecf 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -3,6 +3,6 @@ // the whole project. For all other things use your own local settings. "[rust]": { "editor.defaultFormatter": "rust-lang.rust-analyzer", - "editor.formatOnSave": true, - }, + "editor.formatOnSave": true + } } diff --git a/Cargo.lock b/Cargo.lock index f769fbf6f6..6eeefe23e0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -65,6 +65,54 @@ dependencies = [ "libc", ] +[[package]] +name = "anstream" +version = "0.6.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e2e1ebcb11de5c03c67de28a7df593d32191b44939c482e97702baaaa6ab6a5" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2faccea4cc4ab4a667ce676a30e8ec13922a692c99bb8f5b11f1502c72e04220" + +[[package]] +name = "anstyle-parse" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c75ac65da39e5fe5ab759307499ddad880d724eed2f6ce5b5e8a26f4f387928c" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e28923312444cdd728e4738b3f9c9cac739500909bb3d3c94b43551b16517648" +dependencies = [ + "windows-sys 0.52.0", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7" +dependencies = [ + "anstyle", + "windows-sys 0.52.0", +] + [[package]] name = "anyhow" version = "1.0.80" @@ -183,6 +231,29 @@ version = "0.21.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9d297deb1925b89f2ccc13d7635fa0714f12c87adce1c75356b39ca9b7178567" +[[package]] +name = "bindgen" +version = "0.68.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "726e4313eb6ec35d2730258ad4e15b547ee75d6afaa1361a922e78e59b7d8078" +dependencies = [ + "bitflags 2.4.2", + "cexpr", + "clang-sys", + "lazy_static", + "lazycell", + "log", + "peeking_take_while", + "prettyplease", + "proc-macro2", + "quote", + "regex", + "rustc-hash", + "shlex", + "syn 2.0.52", + "which", +] + [[package]] name = "bit-set" version = "0.5.3" @@ -231,6 +302,38 @@ dependencies = [ "generic-array", ] +[[package]] +name = "btor2i" +version = "0.1.0" +dependencies = [ + "bitvec", + "btor2tools", + "clap 4.4.18", + "num-bigint", + "num-integer", + "num-traits", + "tempfile", + "thiserror", +] + +[[package]] +name = "btor2tools" +version = "1.1.0" +source = "git+https://github.com/obhalerao/btor2tools.rs#a01b2ebc85ee4489860069b196b2ab886d06f43a" +dependencies = [ + "btor2tools-sys", + "thiserror", +] + +[[package]] +name = "btor2tools-sys" +version = "1.1.0" +source = "git+https://github.com/obhalerao/btor2tools-sys#e5d1c44220cb5a02b30b538c5ade70102109904a" +dependencies = [ + "bindgen", + "copy_dir", +] + [[package]] name = "bumpalo" version = "3.15.3" @@ -413,6 +516,15 @@ version = "1.0.88" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "02f341c093d19155a6e41631ce5971aac4e9a868262212153124c15fa22d1cdc" +[[package]] +name = "cexpr" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766" +dependencies = [ + "nom 7.1.3", +] + [[package]] name = "cfg-if" version = "1.0.0" @@ -449,6 +561,17 @@ dependencies = [ "thiserror", ] +[[package]] +name = "clang-sys" +version = "1.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67523a3b4be3ce1989d607a828d036249522dd9c1c8de7f4dd2dae43a37369d1" +dependencies = [ + "glob", + "libc", + "libloading", +] + [[package]] name = "clap" version = "2.34.0" @@ -460,6 +583,46 @@ dependencies = [ "unicode-width", ] +[[package]] +name = "clap" +version = "4.4.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e578d6ec4194633722ccf9544794b71b1385c3c027efe0c55db226fc880865c" +dependencies = [ + "clap_builder", + "clap_derive", +] + +[[package]] +name = "clap_builder" +version = "4.4.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4df4df40ec50c46000231c914968278b1eb05098cf8f1b3a518a95030e71d1c7" +dependencies = [ + "anstream", + "anstyle", + "clap_lex", + "strsim", +] + +[[package]] +name = "clap_derive" +version = "4.4.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf9804afaaf59a91e75b022a30fb7229a7901f60c755489cc61c9b423b836442" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn 2.0.52", +] + +[[package]] +name = "clap_lex" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "702fc72eb24e5a1e48ce58027a675bc24edd52096d5397d4aea7c6dd9eca0bd1" + [[package]] name = "clipboard-win" version = "4.5.0" @@ -471,6 +634,12 @@ dependencies = [ "winapi", ] +[[package]] +name = "colorchoice" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" + [[package]] name = "console" version = "0.15.8" @@ -493,6 +662,15 @@ dependencies = [ "wasm-bindgen", ] +[[package]] +name = "copy_dir" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "543d1dd138ef086e2ff05e3a48cf9da045da2033d16f8538fd76b86cd49b2ca3" +dependencies = [ + "walkdir", +] + [[package]] name = "core-foundation-sys" version = "0.8.6" @@ -522,7 +700,7 @@ checksum = "b01d6de93b2b6c65e17c634a26653a29d107b3c98c607c765bf38d041531cd8f" dependencies = [ "atty", "cast", - "clap", + "clap 2.34.0", "criterion-plot", "csv", "itertools 0.10.5", @@ -1038,6 +1216,12 @@ version = "0.28.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4271d37baee1b8c7e4b708028c57d816cf9d2434acb33a549475f78c181f6253" +[[package]] +name = "glob" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" + [[package]] name = "half" version = "1.8.3" @@ -1095,6 +1279,15 @@ version = "0.4.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70" +[[package]] +name = "home" +version = "0.5.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e3d1354bf6b7235cb4a0576c2619fd4ed18183f689b12b006a0ee7329eeff9a5" +dependencies = [ + "windows-sys 0.52.0", +] + [[package]] name = "httparse" version = "1.8.0" @@ -1215,6 +1408,7 @@ dependencies = [ "argh", "base64 0.13.1", "bitvec", + "btor2i", "calyx-frontend", "calyx-ir", "calyx-opt", @@ -1291,12 +1485,28 @@ version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" +[[package]] +name = "lazycell" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55" + [[package]] name = "libc" version = "0.2.153" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd" +[[package]] +name = "libloading" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c2a198fb6b0eada2a8df47933734e6d35d350665a33a3593d7164fa52c75c19" +dependencies = [ + "cfg-if", + "windows-targets 0.48.5", +] + [[package]] name = "libm" version = "0.2.8" @@ -1373,6 +1583,12 @@ version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "523dc4f511e55ab87b694dc30d0f820d60906ef06413f93d4d7a1385599cc149" +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + [[package]] name = "miniz_oxide" version = "0.7.2" @@ -1423,6 +1639,16 @@ dependencies = [ "version_check 0.1.5", ] +[[package]] +name = "nom" +version = "7.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" +dependencies = [ + "memchr", + "minimal-lexical", +] + [[package]] name = "nu-ansi-term" version = "0.46.0" @@ -1583,6 +1809,12 @@ dependencies = [ "camino", ] +[[package]] +name = "peeking_take_while" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "19b17cddbe7ec3f8bc800887bab5e717348c95ea2ca0b1bf0837fb964dc67099" + [[package]] name = "percent-encoding" version = "2.3.1" @@ -1750,6 +1982,16 @@ dependencies = [ "unicode-segmentation", ] +[[package]] +name = "prettyplease" +version = "0.2.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a41cf62165e97c7f814d2221421dbb9afcbcdb0a88068e5ea206e19951c2cbb5" +dependencies = [ + "proc-macro2", + "syn 2.0.52", +] + [[package]] name = "proc-macro2" version = "1.0.78" @@ -1943,6 +2185,12 @@ version = "0.1.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" +[[package]] +name = "rustc-hash" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" + [[package]] name = "rustix" version = "0.38.31" @@ -2076,7 +2324,7 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5318bfeed779c64075ce317c81462ed54dc00021be1c6b34957d798e11a68bdb" dependencies = [ - "nom", + "nom 4.2.3", "serde", ] @@ -2161,6 +2409,12 @@ dependencies = [ "lazy_static", ] +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + [[package]] name = "similar" version = "2.4.0" @@ -2852,6 +3106,18 @@ dependencies = [ "wasm-bindgen", ] +[[package]] +name = "which" +version = "4.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87ba24419a2078cd2b0f2ede2691b6c66d8e47836da3b6db8265ebad47afbfc7" +dependencies = [ + "either", + "home", + "once_cell", + "rustix", +] + [[package]] name = "winapi" version = "0.3.9" diff --git a/Cargo.toml b/Cargo.toml index 211819e6db..c705fda544 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,6 +14,7 @@ members = [ "cider-dap", "fud2", "fud2/fud-core", + "tools/btor2/btor2i" ] exclude = ["site"] diff --git a/Dockerfile b/Dockerfile index 3ad51b7015..9c22815330 100644 --- a/Dockerfile +++ b/Dockerfile @@ -20,6 +20,9 @@ RUN python3 -m pip install numpy flit prettytable wheel hypothesis pytest simple # Current cocotb-bus has a bug that is fixed in more up to date repo RUN python3 -m pip install git+https://github.com/cocotb/cocotb-bus.git cocotbext-axi +# Install clang +RUN apt-get install -y clang + # Install Verilator WORKDIR /home ## TODO(rachit): Don't hardcode the version here diff --git a/interp/Cargo.toml b/interp/Cargo.toml index dbe272b62f..2a1224f7f2 100644 --- a/interp/Cargo.toml +++ b/interp/Cargo.toml @@ -48,6 +48,8 @@ calyx-utils = { path = "../calyx-utils", features = ["serialize"] } calyx-opt = { path = "../calyx-opt" } calyx-frontend = { path = "../calyx-frontend" } +btor2i = { path = "../tools/btor2/btor2i" } + [dev-dependencies] proptest = "1.0.0" diff --git a/interp/src/flatten/primitives/btor2_prim.rs b/interp/src/flatten/primitives/btor2_prim.rs new file mode 100644 index 0000000000..a5a0ee5231 --- /dev/null +++ b/interp/src/flatten/primitives/btor2_prim.rs @@ -0,0 +1,64 @@ +use btor2i::program::Btor2Program; + +use crate::flatten::flat_ir::prelude::{AssignedValue, GlobalPortIdx}; +use crate::flatten::primitives::prim_trait::{Primitive, UpdateResult}; +use crate::flatten::primitives::{declare_ports, ports}; +use crate::flatten::structures::environment::PortMap; + +use crate::values::Value; + +// use std::env; + +use std::cell::RefCell; +use std::collections::HashMap; + +pub struct MyBtor2Add<'a> { + program: RefCell>, + base_port: GlobalPortIdx, + width: usize, // do stuff +} + +impl<'a> MyBtor2Add<'a> { + declare_ports![ LEFT:0, RIGHT:1, OUT:2 ]; + pub fn new(base: GlobalPortIdx, width: usize) -> Self { + Self { + program: RefCell::new(Btor2Program::new( + "../tools/btor2/core/std_add.btor", + )), + base_port: base, + width, + } + } +} + +impl<'a> Primitive for MyBtor2Add<'a> { + fn exec_comb(&self, port_map: &mut PortMap) -> UpdateResult { + ports![&self.base_port; left: Self::LEFT, right: Self::RIGHT, out: Self::OUT]; + let input_map = HashMap::from([ + ( + "left".to_string(), + port_map[left].as_usize().unwrap_or(0).to_string(), + ), + ( + "right".to_string(), + port_map[right].as_usize().unwrap_or(0).to_string(), + ), + ]); + match self.program.borrow_mut().run(input_map) { + Ok(output_map) => Ok(port_map.insert_val( + out, + AssignedValue::cell_value(Value::from( + output_map["out"], + self.width, + )), + )?), + Err(msg) => { + panic!("{}", msg); + } + } + } + + fn has_stateful(&self) -> bool { + false + } +} diff --git a/interp/src/flatten/primitives/builder.rs b/interp/src/flatten/primitives/builder.rs index f484db3b82..bb8ae418fc 100644 --- a/interp/src/flatten/primitives/builder.rs +++ b/interp/src/flatten/primitives/builder.rs @@ -199,6 +199,8 @@ pub fn build_primitive( ), )), }, - CellPrototype::Unknown(_, _) => todo!(), + CellPrototype::Unknown(_, _) => { + todo!() + } } } diff --git a/interp/src/flatten/primitives/mod.rs b/interp/src/flatten/primitives/mod.rs index da89eeb012..167a017ba3 100644 --- a/interp/src/flatten/primitives/mod.rs +++ b/interp/src/flatten/primitives/mod.rs @@ -1,3 +1,4 @@ +pub mod btor2_prim; mod builder; pub mod combinational; pub(crate) mod macros; diff --git a/tools/btor2/btor2i/Cargo.toml b/tools/btor2/btor2i/Cargo.toml new file mode 100644 index 0000000000..f4c33be76c --- /dev/null +++ b/tools/btor2/btor2i/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "btor2i" +version = "0.1.0" +authors = ["Justin Ngai ", "Sanjit Basker ","Omkar Bhalerao "] +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +clap = { version = "4.4.7", features = ["derive"] } +num-bigint = "0.4.4" +num-traits = "0.2.17" +bitvec = "1.0.1" +tempfile = "3.8.1" +thiserror = "1.0.50" +num-integer = "0.1.45" +btor2tools = { git = "https://github.com/obhalerao/btor2tools.rs" } \ No newline at end of file diff --git a/tools/btor2/btor2i/Makefile b/tools/btor2/btor2i/Makefile new file mode 100644 index 0000000000..6e2314837e --- /dev/null +++ b/tools/btor2/btor2i/Makefile @@ -0,0 +1,18 @@ +TESTS := ./test/*.btor2 + +.PHONY: install +install: + RUSTFLAGS="-C target-cpu=native" cargo install --path . + +.PHONY: test +test: + turnt $(TESTS) + +.PHONY: benchmarks +benchmarks: + python3 brench-pipeless/brench.py benchmark.toml + +# This is primarily used for running examples and debuging a bril program +.PHONY: example +example: + bril2json < ../benchmarks/sqrt.bril | cargo run diff --git a/tools/btor2/btor2i/README.md b/tools/btor2/btor2i/README.md new file mode 100644 index 0000000000..91d6ad0c8b --- /dev/null +++ b/tools/btor2/btor2i/README.md @@ -0,0 +1,33 @@ +# btor2i + +`btor2i` is a faster interpreter for BTOR2 written in rust. + +It is available as both a command-line interface and a rust library. + +## Command-line interface + +Using `cargo`; run `cargo install --path .` and make sure `$HOME/.cargo/bin` is +on your path. + +Run `btor2i --help` for all of the supported flags. + +## Rust interface [WIP] + +`btor2i` can also be used in your rust code which may be advantageous. Add `btor2i` + to your `Cargo.toml` with: + +```toml +[dependencies.btor2i] +version = "0.1.0" +path = "../btor2i" +``` + +Check out `cargo doc --open` for exposed functions. + +## Contributing + +Issues and PRs are welcome. For pull requests, make sure to run the [Turnt](https://github.com/cucapra/turnt) +test harness with `make test` and `make benchmark`. The `make test` output is in +[TAP](https://testanything.org/) format and can be prettified with TAP consumers, +like [Faucet](https://github.com/ljharb/faucet). There is also `.github/workflows/rust.yaml` +which will format your code and check that it is conforming with clippy. diff --git a/tools/btor2/btor2i/benchmark.toml b/tools/btor2/btor2i/benchmark.toml new file mode 100644 index 0000000000..51a72d1a07 --- /dev/null +++ b/tools/btor2/btor2i/benchmark.toml @@ -0,0 +1,37 @@ +extract = 'Time elapsed: (\d+) µs' +timeout = 60 +benchmarks = 'test/core/combo/*.btor2' + +[runs.baseline] +pipeline = [ + "cargo run -r -- -p -f {file_path} {args}", +] +[runs.10] +pipeline = [ + "cargo run -r -- -p -n 10 -f {file_path} {args}", +] + +[runs.100] +pipeline = [ + "cargo run -r -- -p -n 100 -f {file_path} {args}", +] + +[runs.1000] +pipeline = [ + "cargo run -r -- -p -n 1000 -f {file_path} {args}", +] + +[runs.10000] +pipeline = [ + "cargo run -r -- -p -n 10000 -f {file_path} {args}", +] + +[runs.100000] +pipeline = [ + "cargo run -r -- -p -n 100000 -f {file_path} {args}", +] + +[runs.1000000] +pipeline = [ + "cargo run -r -- -p -n 1000000 -f {file_path} {args}", +] diff --git a/tools/btor2/btor2i/src/bvec.rs b/tools/btor2/btor2i/src/bvec.rs new file mode 100644 index 0000000000..bd3faedf89 --- /dev/null +++ b/tools/btor2/btor2i/src/bvec.rs @@ -0,0 +1,718 @@ +use std::{convert::From, fmt::Display, ops::Neg, ops::Rem}; + +use bitvec::prelude::*; +use num_bigint::{BigInt, BigUint}; +use num_integer::Integer; +use num_traits::{One, Zero}; + +#[derive(Debug, Clone)] +pub struct BitVector { + bits: BitVec, +} + +impl BitVector { + /// the value 0, of width `len` + pub fn zeros(len: usize) -> Self { + BitVector { + bits: BitVec::repeat(false, len), + } + } + + /// the value 1, of width `len` + pub fn one(len: usize) -> Self { + let mut bits = BitVec::repeat(false, len); + bits.set(0, true); + BitVector { bits } + } + + /// the value -1, of width `len` + pub fn ones(len: usize) -> Self { + BitVector { + bits: BitVec::repeat(true, len), + } + } + + pub fn from_bool(b: bool) -> Self { + let mut bits: BitVec = BitVec::new(); + bits.push(b); + BitVector { bits } + } + + pub fn width(&self) -> usize { + self.bits.len() + } + + /// sign-extend `bv` by `w` bits + pub fn sign_extend(bv: &BitVector, w: usize) -> Self { + let mut other_vec = BitVec::new(); + for bit in bv.bits.iter() { + other_vec.push(*bit); + } + for _ in bv.bits.len()..bv.bits.len() + w { + other_vec.push(*bv.bits.last().as_deref().unwrap()); + } + BitVector { bits: other_vec } + } + + /// zero-extend `bv` by `w` + pub fn zero_extend(bv: &BitVector, w: usize) -> Self { + let mut other_vec = BitVec::new(); + for bit in bv.bits.iter() { + other_vec.push(*bit); + } + for _ in 0..w { + other_vec.push(false); + } + BitVector { bits: other_vec } + } + + /// keep bits `l` thru `u` (inclusive, 0-indexed) of `bv` + pub fn slice(bv: &BitVector, l: usize, u: usize) -> Self { + let mut other_vec = BitVec::new(); + for i in (l)..(u + 1) { + other_vec.push(bv.bits[i]); + } + + BitVector { bits: other_vec } + } + + /// bitwise not + pub fn not(bv: &BitVector) -> Self { + let bits = bv.bits.clone(); + BitVector { bits: !bits } + } + + /// increment + pub fn inc(bv: &BitVector) -> Self { + let mut missing: usize = 0; + while missing < bv.bits.len() && bv.bits[missing] { + missing += 1 + } + if missing == bv.bits.len() { + BitVector::zeros(bv.bits.len()) + } else { + let mut ans = bv.clone(); + ans.bits.set(missing, true); + for i in 0..missing { + ans.bits.set(i, false); + } + ans + } + } + + pub fn inc2(bv: &BitVector) -> Self { + match bv.bits.first_zero() { + Some(missing) => { + let mut ans = bv.clone(); + ans.bits.set(missing, true); + for i in 0..missing { + ans.bits.set(i, false); + } + ans + } + None => BitVector::zeros(bv.bits.len()), + } + } + + /// decrement + pub fn dec(bv: &BitVector) -> Self { + let mut present: usize = 0; + while present < bv.bits.len() && !bv.bits[present] { + present += 1 + } + if present == bv.bits.len() { + BitVector::ones(bv.bits.len()) + } else { + let mut ans = bv.clone(); + ans.bits.set(present, false); + for i in 0..present { + ans.bits.set(i, true); + } + ans + } + } + + pub fn dec2(bv: &BitVector) -> Self { + match bv.bits.first_one() { + Some(present) => { + let mut ans = bv.clone(); + ans.bits.set(present, false); + for i in 0..present { + ans.bits.set(i, true); + } + ans + } + None => BitVector::ones(bv.bits.len()), + } + } + + /// two's complement negation + pub fn neg(bv: &BitVector) -> Self { + BitVector::inc(&BitVector::not(bv)) + } + + pub fn redand(bv: &BitVector) -> bool { + bv.bits.all() + } + + pub fn redor(bv: &BitVector) -> bool { + bv.bits.any() + } + + pub fn redxor(bv: &BitVector) -> bool { + bv.bits.count_ones() % 2 == 1 + } + + pub fn iff(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.bits.any() == bv2.bits.any() + } + + pub fn implies(bv1: &BitVector, bv2: &BitVector) -> bool { + bv2.bits.any() | (!bv1.bits.any()) + } + + pub fn equals(bv1: &BitVector, bv2: &BitVector) -> bool { + if bv1.bits.count_ones() != bv2.bits.count_ones() { + return false; + } + for i in bv1.bits.iter_ones() { + if !(bv2.bits[i]) { + return false; + } + } + bv1.bits.len() == bv2.bits.len() + } + + pub fn neq(bv1: &BitVector, bv2: &BitVector) -> bool { + !BitVector::equals(bv1, bv2) + } + + pub fn to_usize(&self) -> usize { + let mut ans: usize = 0; + for i in 0..self.bits.len() { + if self.bits[i] { + ans += 1 << i; + } + } + ans + } + + // perhaps a better implementation of this would be + // to construct the vector of bytes and pass that to from_[signed]_bytes + fn to_bigint(&self) -> BigInt { + if self.bits.is_empty() { + Zero::zero() + } else if self.bits[self.bits.len() - 1] { + if self.bits.count_ones() == 1 { + // handle min int separately + let inc = BitVector::inc(self); + return inc.to_bigint().checked_sub(&One::one()).unwrap(); + } else { + // negations are fast because big int is sign-magnitude + let neg = BitVector::neg(self); + return neg.to_bigint().neg(); + } + } else { + let mut ans: BigInt = Zero::zero(); + for i in 0..self.bits.len() { + ans.set_bit(i.try_into().unwrap(), self.bits[i]) + } + return ans; + } + } + + fn to_biguint(&self) -> BigUint { + let mut ans: BigUint = Zero::zero(); + for i in 0..self.bits.len() { + ans.set_bit(i.try_into().unwrap(), self.bits[i]) + } + ans + } + + pub fn from_bigint(b: BigInt, width: usize) -> Self { + let mut bits = BitVec::new(); + for i in 0..width { + bits.push(b.bit(i.try_into().unwrap())); + } + + BitVector { bits } + } + + fn from_biguint(b: BigUint, width: usize) -> Self { + let mut bits = BitVec::new(); + for i in 0..width { + bits.push(b.bit(i.try_into().unwrap())); + } + + BitVector { bits } + } + + pub fn sgt(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.to_bigint() > bv2.to_bigint() + } + + pub fn ugt(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.to_biguint() > bv2.to_biguint() + } + + pub fn sgte(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.to_bigint() >= bv2.to_bigint() + } + + pub fn ugte(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.to_biguint() >= bv2.to_biguint() + } + + pub fn slt(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.to_bigint() < bv2.to_bigint() + } + + pub fn ult(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.to_biguint() < bv2.to_biguint() + } + + pub fn slte(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.to_bigint() <= bv2.to_bigint() + } + + pub fn ulte(bv1: &BitVector, bv2: &BitVector) -> bool { + bv1.to_biguint() <= bv2.to_biguint() + } + + pub fn and(bv1: &BitVector, bv2: &BitVector) -> Self { + let mut bits = bv1.bits.clone(); + bits &= bv2.bits.as_bitslice(); + BitVector { bits } + } + + pub fn nand(bv1: &BitVector, bv2: &BitVector) -> Self { + let mut bits = bv1.bits.clone(); + bits &= bv2.bits.as_bitslice(); + BitVector { bits: !bits } + } + + pub fn nor(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::not(&BitVector::or(bv1, bv2)) + } + + pub fn or(bv1: &BitVector, bv2: &BitVector) -> Self { + let mut bits = bv1.bits.clone(); + bits |= bv2.bits.as_bitslice(); + BitVector { bits } + } + + pub fn xnor(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::not(&BitVector::xor(bv1, bv2)) + } + + pub fn xor(bv1: &BitVector, bv2: &BitVector) -> Self { + let mut bits = bv1.bits.clone(); + bits ^= bv2.bits.as_bitslice(); + BitVector { bits } + } + + /// rotate index 1 towards index 0 + pub fn rol(bv1: &BitVector, bv2: &BitVector) -> Self { + let len = bv1.bits.len(); + let rotate_amount = bv2.to_usize(); + let mut bits = bitvec![0; len]; + for i in 0..len { + bits.set(i, bv1.bits[(i + rotate_amount) % len]); + } + BitVector { bits } + } + + /// rotate index 1 away from index 0 + pub fn ror(bv1: &BitVector, bv2: &BitVector) -> Self { + let len = bv1.bits.len(); + let rotate_amount = bv2.to_usize(); + let mut bits = bitvec![0; len]; + for i in 0..len { + bits.set((i + rotate_amount) % len, bv1.bits[i]); + } + BitVector { bits } + } + + pub fn sll(bv1: &BitVector, bv2: &BitVector) -> Self { + let len = bv1.bits.len(); + let shift_amount = bv2.to_usize(); + let mut bits = bitvec![0; len]; + for i in shift_amount..len { + bits.set(i, bv1.bits[i - shift_amount]); + } + BitVector { bits } + } + + pub fn sra(bv1: &BitVector, bv2: &BitVector) -> Self { + let len = bv1.bits.len(); + let shift_amount = bv2.to_usize(); + let b = *bv1.bits.last().unwrap(); + let mut bits = BitVec::repeat(b, len); + for i in 0..(len - shift_amount) { + bits.set(i, bv1.bits[i + shift_amount]); + } + BitVector { bits } + } + + pub fn srl(bv1: &BitVector, bv2: &BitVector) -> Self { + let len = bv1.bits.len(); + let shift_amount = bv2.to_usize(); + let mut bits = BitVec::repeat(false, len); + for i in 0..(len - shift_amount) { + bits.set(i, bv1.bits[i + shift_amount]); + } + BitVector { bits } + } + + pub fn add(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::from_biguint( + bv1.to_biguint() + (bv2.to_biguint()), + bv1.bits.len(), + ) + } + + pub fn mul(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::from_biguint( + bv1.to_biguint() * (bv2.to_biguint()), + bv1.bits.len(), + ) + } + + pub fn sub(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::from_bigint( + bv1.to_bigint() - (&bv2.to_bigint()), + bv1.bits.len(), + ) + } + + pub fn udiv(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::from_biguint( + bv1.to_biguint() / bv2.to_biguint(), + bv1.bits.len(), + ) + } + + pub fn urem(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::from_biguint( + bv1.to_biguint().rem(&bv2.to_biguint()), + bv1.bits.len(), + ) + } + + pub fn sdiv(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::from_bigint( + bv1.to_bigint() + .checked_div(&bv2.to_bigint()) + .unwrap_or(BitVector::ones(bv1.bits.len()).to_bigint()), + bv1.bits.len(), + ) + } + + pub fn smod(bv1: &BitVector, bv2: &BitVector) -> Self { + BitVector::from_bigint( + bv1.to_bigint().mod_floor(&bv2.to_bigint()), + bv1.bits.len(), + ) + } + + pub fn srem(bv1: &BitVector, bv2: &BitVector) -> Self { + let bv1i = bv1.to_bigint(); + let bv2i = bv2.to_bigint(); + let ans = bv1i.mod_floor(&bv2i); + if bv1i.sign() != bv2i.sign() && !bv1i.is_zero() && !bv2i.is_zero() { + BitVector::from_bigint(ans - bv2i, bv1.bits.len()) + } else { + BitVector::from_bigint(ans, bv1.bits.len()) + } + } + + pub fn saddo(_bv1: &BitVector, _bv2: &BitVector) -> bool { + todo!() + } + + pub fn uaddo(_bv1: &BitVector, _bv2: &BitVector) -> bool { + todo!() + } + + pub fn sdivo(_bv1: &BitVector, _bv2: &BitVector) -> bool { + todo!() + } + + pub fn smulo(_bv1: &BitVector, _bv2: &BitVector) -> bool { + todo!() + } + + pub fn umulo(_bv1: &BitVector, _bv2: &BitVector) -> bool { + todo!() + } + + pub fn ssubo(_bv1: &BitVector, _bv2: &BitVector) -> bool { + todo!() + } + + pub fn usubo(_bv1: &BitVector, _bv2: &BitVector) -> bool { + todo!() + } + + pub fn concat(bv1: &BitVector, bv2: &BitVector) -> Self { + let mut bits = BitVec::new(); + bits.reserve(bv1.bits.len() + bv2.bits.len()); + for i in 0..bv1.bits.len() { + bits.push(bv1.bits[i]); + } + for i in 0..bv2.bits.len() { + bits.push(bv2.bits[i]); + } + BitVector { bits } + } + + pub fn ite(cond: &BitVector, bv1: &BitVector, bv2: &BitVector) -> Self { + assert!(cond.bits.len() == 1); + if cond.bits[0] { + bv1.clone() + } else { + bv2.clone() + } + } + + pub fn from_int(val: usize, len: usize) -> Self { + let mut bits = BitVec::new(); + for i in 0..len { + bits.push((val >> i) & 1 == 1); + } + BitVector { bits } + } +} + +impl From for BitVector { + fn from(i: usize) -> Self { + let bitvec = BitVec::from_element(i); + BitVector { bits: bitvec } + } +} + +impl From> for BitVector { + fn from(v: Vec) -> Self { + let mut bits = BitVec::new(); + for bit in v.iter() { + bits.push(*bit); + } + BitVector { bits } + } +} + +impl Display for BitVector { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let chunked_bits = self + .bits + .iter() + .map(|bit| if *bit { '1' } else { '0' }) + .collect::>() + .chunks_mut(4) + .rev() + .map(|chunk| { + chunk.reverse(); + chunk.iter().collect::() + }) + .collect::>() + .join(" "); + write!( + f, + "BitVector(length: {}; bits: {})", + self.bits.len(), + chunked_bits + ) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn naive_test_eq(bv1: &BitVector, bv2: &BitVector) -> bool { + for i in bv1.bits.iter_ones() { + if !(bv2.bits[i]) { + return false; + } + } + for i in bv2.bits.iter_ones() { + if !(bv1.bits[i]) { + return false; + } + } + bv1.bits.len() == bv2.bits.len() + } + + #[test] + /// checks internal representation (no actual logic) + fn test_helpers() { + let bv = BitVector::from(vec![true, false, true, true]); + let bv_7 = BitVector::ones(4); + let bv_7_2 = BitVector::from(vec![true, true, true, true]); + assert!(bv.bits[0]); + assert!(!bv.bits[1]); + assert!(bv.bits[2]); + assert!(bv.bits[3]); + assert!(!naive_test_eq(&bv, &bv_7)); + assert!(naive_test_eq(&bv_7, &bv_7_2)); + println!( + "{}", + BitVector::from(vec![ + true, false, true, true, false, true, true, false, false, + false, false + ]) + ); + } + + #[test] + fn test_slices() { + let bv_3 = BitVector::from(vec![true, true, false]); + let bv_5 = BitVector::from(vec![true, false, true]); + + let bv_3_longer = + BitVector::from(vec![true, true, false, false, false]); + + assert!(naive_test_eq( + &BitVector::sign_extend(&bv_3, 2), + &bv_3_longer, + )); + assert!(naive_test_eq( + &BitVector::zero_extend(&bv_3, 2), + &bv_3_longer, + )); + + assert!(naive_test_eq( + &BitVector::sign_extend(&bv_5, 2), + &BitVector::from(vec![true, false, true, true, true]), + )); + assert!(naive_test_eq( + &BitVector::zero_extend(&bv_5, 3), + &BitVector::from(vec![true, false, true, false, false, false]), + )); + + assert!(naive_test_eq( + &BitVector::slice(&bv_5, 0, 0), + &BitVector::from(vec![true]), + )); + assert!(naive_test_eq(&BitVector::slice(&bv_5, 0, 2), &bv_5)); + assert!(naive_test_eq( + &BitVector::slice(&bv_3_longer, 1, 4), + &BitVector::from(vec![true, false, false, false]), + )); + } + + #[test] + fn test_unary() { + let bv_0 = BitVector::from(vec![false, false]); + let bv_1 = BitVector::from(vec![true, false]); + let bv_2 = BitVector::from(vec![false, true]); + let bv_3 = BitVector::from(vec![true, true]); + + assert!(naive_test_eq(&BitVector::inc(&bv_0), &bv_1)); + assert!(naive_test_eq(&BitVector::inc(&bv_1), &bv_2)); + assert!(naive_test_eq(&BitVector::inc(&bv_2), &bv_3)); + assert!(naive_test_eq(&BitVector::inc(&bv_3), &bv_0)); + + assert!(naive_test_eq(&BitVector::dec(&bv_1), &bv_0)); + assert!(naive_test_eq(&BitVector::dec(&bv_2), &bv_1)); + assert!(naive_test_eq(&BitVector::dec(&bv_3), &bv_2)); + assert!(naive_test_eq(&BitVector::dec(&bv_0), &bv_3)); + + assert!(naive_test_eq(&BitVector::not(&bv_0), &bv_3)); + assert!(naive_test_eq(&BitVector::not(&bv_1), &bv_2)); + + // pairs add to 4 + assert!(naive_test_eq(&BitVector::neg(&bv_0), &bv_0)); + assert!(naive_test_eq(&BitVector::neg(&bv_1), &bv_3)); + assert!(naive_test_eq(&BitVector::neg(&bv_2), &bv_2)); + assert!(naive_test_eq(&BitVector::neg(&bv_3), &bv_1)); + + assert!(BitVector::redand(&bv_3)); + assert!(!BitVector::redand(&bv_1)); + assert!(!BitVector::redand(&bv_2)); + assert!(!BitVector::redand(&bv_0)); + + assert!(!BitVector::redor(&bv_0)); + assert!(BitVector::redor(&bv_1)); + assert!(BitVector::redor(&bv_2)); + assert!(BitVector::redor(&bv_3)); + + assert!(!BitVector::redxor(&bv_0)); + assert!(BitVector::redxor(&bv_1)); + assert!(BitVector::redxor(&bv_2)); + assert!(!BitVector::redxor(&bv_3)); + + assert!(naive_test_eq( + &BitVector::neg(&BitVector::neg(&BitVector::neg(&BitVector::neg( + &bv_3 + )))), + &bv_3, + )); + assert!(naive_test_eq( + &BitVector::not(&BitVector::not(&BitVector::not(&BitVector::not( + &bv_2 + )))), + &bv_2, + )); + assert!(naive_test_eq( + &BitVector::inc(&BitVector::dec(&BitVector::dec(&BitVector::inc( + &bv_2 + )))), + &bv_2, + )); + } + + #[test] + fn test_unsigned_arithmetic_small() { + let max = 128; + let size = 7; + + let mut unsigned_numbers: Vec = Vec::new(); + unsigned_numbers.push(BitVector::zeros(size)); + for _i in 1..max { + unsigned_numbers + .push(BitVector::inc(unsigned_numbers.last().unwrap())); + } + + for i in 0..max { + for j in 0..max { + let sum = + BitVector::add(&unsigned_numbers[i], &unsigned_numbers[j]); + // let diff = BitVector::sub(&unsigned_numbers[i], &unsigned_numbers[j]); + let prod = + BitVector::mul(&unsigned_numbers[i], &unsigned_numbers[j]); + + // implementation-specific, behavior should be undefined in second case + let _sub_index = if i >= j { i - j } else { i + max - j }; + + assert!(naive_test_eq(&sum, &unsigned_numbers[(i + j) % max])); + // assert!(naive_test_eq(&diff, &unsigned_numbers[sub_index % max])); + assert!(naive_test_eq(&prod, &unsigned_numbers[(i * j) % max])); + if i < j { + assert!(BitVector::ult( + &unsigned_numbers[i], + &unsigned_numbers[j] + )); + } + if i <= j { + assert!(BitVector::ulte( + &unsigned_numbers[i], + &unsigned_numbers[j] + )); + } + if i > j { + assert!(BitVector::ugt( + &unsigned_numbers[i], + &unsigned_numbers[j] + )); + } + if i >= j { + assert!(BitVector::ugte( + &unsigned_numbers[i], + &unsigned_numbers[j] + )); + } + } + } + } +} diff --git a/tools/btor2/btor2i/src/cli.rs b/tools/btor2/btor2i/src/cli.rs new file mode 100644 index 0000000000..b6e8bca7e4 --- /dev/null +++ b/tools/btor2/btor2i/src/cli.rs @@ -0,0 +1,22 @@ +use clap::Parser; + +#[derive(Parser)] +#[command(about, version, author)] // keeps the cli synced with Cargo.toml +#[command(allow_hyphen_values(true))] +pub struct CLI { + /// The BTOR2 file to run. stdin is assumed if file is not provided + #[arg(short, long, action)] + pub file: Option, + + /// Profile mode + #[arg(short, long, default_value = "false")] + pub profile: bool, + + /// The number of times to repeat the simulation (used for profiling) + #[arg(short, long, default_value = "1")] + pub num_repeat: usize, + + /// Inputs for the main function + #[arg(action)] + pub inputs: Vec, +} diff --git a/tools/btor2/btor2i/src/error.rs b/tools/btor2/btor2i/src/error.rs new file mode 100644 index 0000000000..62d562e753 --- /dev/null +++ b/tools/btor2/btor2i/src/error.rs @@ -0,0 +1,33 @@ +// use std::fmt::Display; +use thiserror::Error; + +// Having the #[error(...)] for all variants derives the Display trait as well +#[derive(Error, Debug)] +pub enum InterpError { + #[error("Expected `{0}` function arguments, found `{1}`")] + BadNumFuncArgs(usize, usize), // (expected, actual) + + #[error("Expected `{0}` instruction arguments, found `{1}`")] + BadNumArgs(usize, usize), // (expected, actual) + + #[error("{0} is not a valid argment name")] + BadFuncArgName(String), // (expected, actual) + + #[error("Expected int args, found `{0}`")] + BadFuncArgType(String), // (actual) + + #[error("Expected {0} with width {1}, found `{2}`")] + BadFuncArgWidth(String, usize, usize), // (name, expected, actual) + + #[error("Not currently supported: `{0}`")] + Unsupported(String), // (feature) +} + +impl InterpError { + // #[must_use] + // pub fn add_pos(self, pos: Option) -> PositionalInterpError { + // // TODO: Support PositionalInterpError in the future + // } +} + +pub type InterpResult = Result; diff --git a/tools/btor2/btor2i/src/interp.rs b/tools/btor2/btor2i/src/interp.rs new file mode 100644 index 0000000000..12a1e0e44e --- /dev/null +++ b/tools/btor2/btor2i/src/interp.rs @@ -0,0 +1,544 @@ +use crate::bvec::BitVector; +use crate::error; +use crate::error::InterpError; +use crate::shared_env::SharedEnvironment; +use btor2tools::Btor2Line; +use btor2tools::Btor2SortContent; +use btor2tools::Btor2SortTag; +use num_bigint::BigInt; +use num_traits::Num; +use std::collections::HashMap; +use std::fmt; +use std::slice::Iter; +use std::vec; + +// TODO: eventually remove pub and make a seperate pub function as a main entry point to the interpreter, for now this is main.rs +#[derive(Debug)] +pub struct Environment { + // Maps sid/nid to value + // TODO: valid programs should not have the same identifier in both sets, but we don't currently check that + // TODO: perhaps could opportunistically free mappings if we know they won't be used again + // TODO: consider indirect mapping of output string -> id in env + env: Vec, + args: HashMap, + output: HashMap, +} + +impl Environment { + pub fn new(size: usize) -> Self { + Self { + // Allocate a larger stack size so the interpreter needs to allocate less often + env: vec![Value::default(); size], + args: HashMap::new(), + output: HashMap::new(), + } + } + + pub fn get(&self, idx: usize) -> &Value { + // A BTOR2 program is well formed when, dynamically, every variable is defined before its use. + // If this is violated, this will return Value::Uninitialized and the whole interpreter will come crashing down. + self.env.get(idx).unwrap() + } + + pub fn set(&mut self, idx: usize, val: Value) { + self.env[idx] = val; + } + + pub fn get_output(&self) -> &HashMap { + &self.output + } +} + +impl fmt::Display for Environment { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + // iterate over self.args in order and print them + + writeln!(f, "Arguments:")?; + let mut sorted_args = self.args.iter().collect::>(); + sorted_args.sort_by(|(name1, _), (name2, _)| name1.cmp(name2)); + sorted_args.iter().try_for_each(|(name, val)| { + writeln!(f, "{}: {}", name, val)?; + Ok(()) + })?; + + write!(f, "\nEnvironment:\n")?; + + // don't print uninitialized values + self.env.iter().enumerate().try_for_each(|(idx, val)| { + writeln!(f, "{}: {}", idx, val)?; + Ok(()) + })?; + + write!(f, "\nOutput:\n")?; + self.output.iter().try_for_each(|(name, val)| { + writeln!(f, "{}: {}", name, val)?; + Ok(()) + })?; + + Ok(()) + } +} + +// TODO: eventually remove pub and make a seperate pub function as a main entry point to the interpreter, for now this is main.rs +#[derive(Debug, Default, Clone)] +pub enum Value { + BitVector(BitVector), + // TODO: Add support for + // TODO: Add support for + #[default] + Uninitialized, +} + +impl fmt::Display for Value { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Value::BitVector(bv) => write!(f, "{}", bv.to_usize()), + Value::Uninitialized => write!(f, "_"), + } + } +} + +pub fn interpret( + mut prog_iterator: Iter, + env: &mut SharedEnvironment, +) -> Result<(), InterpError> { + prog_iterator.try_for_each(|line| { + match line.tag() { + // core + btor2tools::Btor2Tag::Sort => Ok(()), // skip - sort information is handled by the parser + btor2tools::Btor2Tag::Const => eval_const_op(env, line, 2), + btor2tools::Btor2Tag::Constd => eval_const_op(env, line, 10), + btor2tools::Btor2Tag::Consth => eval_const_op(env, line, 16), + btor2tools::Btor2Tag::Input => Ok(()), // handled in parse_inputs + btor2tools::Btor2Tag::Output => Ok(()), // handled in extract_output + btor2tools::Btor2Tag::One => { + eval_literals_op(env, line, SharedEnvironment::one) + } + btor2tools::Btor2Tag::Ones => { + eval_literals_op(env, line, SharedEnvironment::ones) + } + btor2tools::Btor2Tag::Zero => { + eval_literals_op(env, line, SharedEnvironment::zero) + } + + // indexed + btor2tools::Btor2Tag::Sext => { + eval_unary_op(env, line, SharedEnvironment::sext) + } + btor2tools::Btor2Tag::Uext => { + eval_unary_op(env, line, SharedEnvironment::uext) + } + btor2tools::Btor2Tag::Slice => eval_slice_op(env, line), + + // unary + btor2tools::Btor2Tag::Not => { + eval_unary_op(env, line, SharedEnvironment::not) + } + btor2tools::Btor2Tag::Inc => { + eval_unary_op(env, line, SharedEnvironment::inc) + } + btor2tools::Btor2Tag::Dec => { + eval_unary_op(env, line, SharedEnvironment::dec) + } + btor2tools::Btor2Tag::Neg => { + eval_unary_op(env, line, SharedEnvironment::neg) + } + btor2tools::Btor2Tag::Redand => { + eval_unary_op(env, line, SharedEnvironment::redand) + } + btor2tools::Btor2Tag::Redor => { + eval_unary_op(env, line, SharedEnvironment::redor) + } + btor2tools::Btor2Tag::Redxor => { + eval_unary_op(env, line, SharedEnvironment::redxor) + } + + // binary - boolean + btor2tools::Btor2Tag::Iff => { + eval_binary_op(env, line, SharedEnvironment::iff) + } + btor2tools::Btor2Tag::Implies => { + eval_binary_op(env, line, SharedEnvironment::implies) + } + btor2tools::Btor2Tag::Eq => { + eval_binary_op(env, line, SharedEnvironment::eq) + } + btor2tools::Btor2Tag::Neq => { + eval_binary_op(env, line, SharedEnvironment::neq) + } + + // binary - (un)signed inequality + btor2tools::Btor2Tag::Sgt => { + eval_binary_op(env, line, SharedEnvironment::sgt) + } + btor2tools::Btor2Tag::Sgte => { + eval_binary_op(env, line, SharedEnvironment::sgte) + } + btor2tools::Btor2Tag::Slt => { + eval_binary_op(env, line, SharedEnvironment::slt) + } + btor2tools::Btor2Tag::Slte => { + eval_binary_op(env, line, SharedEnvironment::slte) + } + btor2tools::Btor2Tag::Ugt => { + eval_binary_op(env, line, SharedEnvironment::ugt) + } + btor2tools::Btor2Tag::Ugte => { + eval_binary_op(env, line, SharedEnvironment::ugte) + } + btor2tools::Btor2Tag::Ult => { + eval_binary_op(env, line, SharedEnvironment::ult) + } + btor2tools::Btor2Tag::Ulte => { + eval_binary_op(env, line, SharedEnvironment::ulte) + } + + // binary - bit-wise + btor2tools::Btor2Tag::And => { + eval_binary_op(env, line, SharedEnvironment::and) + } + btor2tools::Btor2Tag::Nand => { + eval_binary_op(env, line, SharedEnvironment::nand) + } + btor2tools::Btor2Tag::Nor => { + eval_binary_op(env, line, SharedEnvironment::nor) + } + btor2tools::Btor2Tag::Or => { + eval_binary_op(env, line, SharedEnvironment::or) + } + btor2tools::Btor2Tag::Xnor => { + eval_binary_op(env, line, SharedEnvironment::xnor) + } + btor2tools::Btor2Tag::Xor => { + eval_binary_op(env, line, SharedEnvironment::xor) + } + + // binary - rotate, shift + btor2tools::Btor2Tag::Rol => { + eval_binary_op(env, line, SharedEnvironment::rol) + } + btor2tools::Btor2Tag::Ror => { + eval_binary_op(env, line, SharedEnvironment::ror) + } + btor2tools::Btor2Tag::Sll => { + eval_binary_op(env, line, SharedEnvironment::sll) + } + btor2tools::Btor2Tag::Sra => { + eval_binary_op(env, line, SharedEnvironment::sra) + } + btor2tools::Btor2Tag::Srl => { + eval_binary_op(env, line, SharedEnvironment::srl) + } + + // binary - arithmetic + btor2tools::Btor2Tag::Add => { + eval_binary_op(env, line, SharedEnvironment::add) + } + btor2tools::Btor2Tag::Mul => { + eval_binary_op(env, line, SharedEnvironment::mul) + } + btor2tools::Btor2Tag::Sdiv => { + eval_binary_op(env, line, SharedEnvironment::sdiv) + } + btor2tools::Btor2Tag::Udiv => { + eval_binary_op(env, line, SharedEnvironment::udiv) + } + btor2tools::Btor2Tag::Smod => { + eval_binary_op(env, line, SharedEnvironment::smod) + } + btor2tools::Btor2Tag::Srem => { + eval_binary_op(env, line, SharedEnvironment::srem) + } + btor2tools::Btor2Tag::Urem => { + eval_binary_op(env, line, SharedEnvironment::urem) + } + btor2tools::Btor2Tag::Sub => { + eval_binary_op(env, line, SharedEnvironment::sub) + } + + // binary - overflow + btor2tools::Btor2Tag::Saddo => { + eval_binary_op(env, line, SharedEnvironment::saddo) + } + btor2tools::Btor2Tag::Uaddo => { + eval_binary_op(env, line, SharedEnvironment::uaddo) + } + btor2tools::Btor2Tag::Sdivo => { + eval_binary_op(env, line, SharedEnvironment::sdivo) + } + // btor2tools::Btor2Tag::Udivo => Ok(()), Unsigned division never overflows :D + btor2tools::Btor2Tag::Smulo => { + eval_binary_op(env, line, SharedEnvironment::smulo) + } + btor2tools::Btor2Tag::Umulo => { + eval_binary_op(env, line, SharedEnvironment::umulo) + } + btor2tools::Btor2Tag::Ssubo => { + eval_binary_op(env, line, SharedEnvironment::ssubo) + } + btor2tools::Btor2Tag::Usubo => { + eval_binary_op(env, line, SharedEnvironment::usubo) + } + + // binary - concat + btor2tools::Btor2Tag::Concat => { + eval_binary_op(env, line, SharedEnvironment::concat) + } + + // ternary - conditional + btor2tools::Btor2Tag::Ite => { + eval_ternary_op(env, line, SharedEnvironment::ite) + } + + // Unsupported: arrays, state, assertions + btor2tools::Btor2Tag::Bad + | btor2tools::Btor2Tag::Constraint + | btor2tools::Btor2Tag::Fair + | btor2tools::Btor2Tag::Init + | btor2tools::Btor2Tag::Justice + | btor2tools::Btor2Tag::Next + | btor2tools::Btor2Tag::State + | btor2tools::Btor2Tag::Read + | btor2tools::Btor2Tag::Write => Err( + error::InterpError::Unsupported(format!("{:?}", line.tag())), + ), + } + }) +} + +/// Handles the `const`, `constd`, and `consth` statements. +fn eval_const_op( + env: &mut SharedEnvironment, + line: &btor2tools::Btor2Line, + radix: u32, +) -> Result<(), error::InterpError> { + match line.constant() { + Some(cstr) => match cstr.to_str() { + Ok(str) => { + let nstring = str.to_string(); + let intval = BigInt::from_str_radix(&nstring, radix).unwrap(); + + match line.sort().tag() { + Btor2SortTag::Bitvec => { + if let Btor2SortContent::Bitvec { width } = + line.sort().content() + { + let bool_vec = (0..width) + .map(|i| intval.bit(i as u64)) + .collect::>(); + + env.const_(line.id().try_into().unwrap(), bool_vec); + } + Ok(()) + } + Btor2SortTag::Array => { + Err(error::InterpError::Unsupported(format!( + "{:?}", + line.sort().tag() + ))) + } + } + } + Err(_e) => Err(error::InterpError::BadFuncArgType( + "Bad value in constant".to_string(), + )), + }, + None => Err(error::InterpError::BadFuncArgType( + "No value in constant".to_string(), + )), + } +} + +/// Handle the `one`, `ones` and `zero` statements. +fn eval_literals_op( + env: &mut SharedEnvironment, + line: &btor2tools::Btor2Line, + literal_init: fn(&mut SharedEnvironment, i1: usize), +) -> Result<(), error::InterpError> { + match line.sort().tag() { + Btor2SortTag::Bitvec => { + literal_init(env, line.id().try_into().unwrap()); + Ok(()) + } + Btor2SortTag::Array => Err(error::InterpError::Unsupported(format!( + "{:?}", + line.sort().tag() + ))), + } +} + +/// Handles the `slice` statements. +fn eval_slice_op( + env: &mut SharedEnvironment, + line: &btor2tools::Btor2Line, +) -> Result<(), error::InterpError> { + let sort = line.sort(); + match sort.tag() { + Btor2SortTag::Bitvec => { + assert_eq!(line.args().len(), 3); + let arg1_line = line.args()[0] as usize; + let u = line.args()[1] as usize; + let l = line.args()[2] as usize; + if let Btor2SortContent::Bitvec { width } = line.sort().content() { + if (u - l) + 1 != width as usize { + return Err(error::InterpError::Unsupported(format!( + "Slicing of {:?} is not supported", + arg1_line + ))); + } + env.slice(u, l, arg1_line, line.id().try_into().unwrap()); + Ok(()) + } else { + Err(error::InterpError::Unsupported(format!( + "Slicing of {:?} is not supported", + arg1_line + ))) + } + } + Btor2SortTag::Array => Err(error::InterpError::Unsupported(format!( + "{:?}", + line.sort().tag() + ))), + } +} + +/// Handle all the unary operators. +fn eval_unary_op( + env: &mut SharedEnvironment, + line: &btor2tools::Btor2Line, + unary_fn: fn(&mut SharedEnvironment, usize, usize), +) -> Result<(), error::InterpError> { + let sort = line.sort(); + match sort.tag() { + Btor2SortTag::Bitvec => { + assert_eq!(line.args().len(), 1); + let arg1_line = line.args()[0] as usize; + unary_fn(env, arg1_line, line.id().try_into().unwrap()); + Ok(()) + } + Btor2SortTag::Array => Err(error::InterpError::Unsupported(format!( + "{:?}", + line.sort().tag() + ))), + } +} + +/// Handles all the binary operators. +fn eval_binary_op( + env: &mut SharedEnvironment, + line: &btor2tools::Btor2Line, + binary_fn: fn(&mut SharedEnvironment, usize, usize, usize), +) -> Result<(), error::InterpError> { + let sort = line.sort(); + match sort.tag() { + Btor2SortTag::Bitvec => { + assert_eq!(line.args().len(), 2); + let arg1_line = line.args()[0] as usize; + let arg2_line = line.args()[1] as usize; + + binary_fn(env, arg1_line, arg2_line, line.id().try_into().unwrap()); + Ok(()) + } + Btor2SortTag::Array => Err(error::InterpError::Unsupported(format!( + "{:?}", + line.sort().tag() + ))), + } +} + +fn eval_ternary_op( + env: &mut SharedEnvironment, + line: &btor2tools::Btor2Line, + ternary_fn: fn(&mut SharedEnvironment, usize, usize, usize, usize), +) -> Result<(), error::InterpError> { + assert_eq!(line.args().len(), 3); + let arg1_line = line.args()[0] as usize; + let arg2_line = line.args()[1] as usize; + let arg3_line = line.args()[2] as usize; + ternary_fn( + env, + arg1_line, + arg2_line, + arg3_line, + line.id().try_into().unwrap(), + ); + Ok(()) +} + +// TODO: eventually remove pub and make a seperate pub function as a main entry point to the interpreter, for now this is main.rs +pub fn parse_inputs( + env: &mut SharedEnvironment, + lines: &[Btor2Line], + inputs: &[String], +) -> Result<(), InterpError> { + // create input name to line no. and sort map + let mut input_map = HashMap::new(); + lines.iter().for_each(|line| { + if let btor2tools::Btor2Tag::Input = line.tag() { + let input_name = + line.symbol().unwrap().to_string_lossy().into_owned(); + if let Btor2SortContent::Bitvec { width } = line.sort().content() { + input_map.insert( + input_name, + ( + usize::try_from(line.id()).unwrap(), + usize::try_from(width).unwrap(), + ), + ); + } + } + }); + + if input_map.is_empty() && inputs.is_empty() { + Ok(()) + } else if inputs.len() != input_map.len() { + Err(InterpError::BadNumFuncArgs(input_map.len(), inputs.len())) + } else { + inputs.iter().try_for_each(|input| { + // arg in the form "x=1", extract variable name and value + let mut split = input.split('='); + let arg_name = split.next().unwrap(); + let arg_val = split.next().unwrap(); + + if !input_map.contains_key(arg_name) { + return Err(InterpError::BadFuncArgName(arg_name.to_string())); + } + + let (idx, width) = input_map.get(arg_name).unwrap(); + + // input must begins with 0b + if arg_val.starts_with("0b") { + let arg_as_bin = arg_val + .trim_start_matches("0b") + .chars() + .map(|c| c == '1') + .collect::>(); + + if arg_as_bin.len() > *width { + return Err(InterpError::BadFuncArgWidth( + arg_name.to_string(), + *width, + arg_as_bin.len(), + )); + } + + // pad with 0s if necessary + let arg_as_bin = if arg_as_bin.len() < *width { + let mut arg_as_bin = arg_as_bin; + arg_as_bin.resize(*width, false); + arg_as_bin + } else { + arg_as_bin + }; + + env.set_vec(*idx, arg_as_bin); + + Ok(()) + } else { + Err(InterpError::BadFuncArgType( + "Input must be in binary format".to_string(), + )) + } + }) + } +} diff --git a/tools/btor2/btor2i/src/lib.rs b/tools/btor2/btor2i/src/lib.rs new file mode 100644 index 0000000000..03dac751a9 --- /dev/null +++ b/tools/btor2/btor2i/src/lib.rs @@ -0,0 +1,6 @@ +pub mod bvec; +pub mod cli; +pub mod error; +pub mod interp; +pub mod program; +pub mod shared_env; diff --git a/tools/btor2/btor2i/src/main.rs b/tools/btor2/btor2i/src/main.rs new file mode 100644 index 0000000000..7f0b50fab7 --- /dev/null +++ b/tools/btor2/btor2i/src/main.rs @@ -0,0 +1,92 @@ +pub mod bvec; +pub mod cli; +pub mod error; +pub mod interp; +pub mod shared_env; + +use btor2tools::Btor2Parser; +use clap::Parser; +use error::InterpResult; +use std::io; +use std::path::Path; +use std::time::Instant; +use tempfile::NamedTempFile; + +fn main() -> InterpResult<()> { + let start = Instant::now(); + let args = cli::CLI::parse(); + + let btor2_file = match args.file { + None => { + // If no file is provided, we assume stdin + let mut tmp = NamedTempFile::new().unwrap(); + io::copy(&mut io::stdin(), &mut tmp).unwrap(); + tmp.path().to_path_buf() + } + Some(input_file_path) => { + Path::new(input_file_path.as_str()).to_path_buf() + } + }; + + // Parse and store the btor2 file as Vec + let mut parser = Btor2Parser::new(); + let btor2_lines = + parser.read_lines(&btor2_file).unwrap().collect::>(); + + // take the btor2lines and convert them into normal lines + + for _ in 0..args.num_repeat { + // Collect node sorts + let node_sorts = btor2_lines + .iter() + .map(|line| match line.tag() { + btor2tools::Btor2Tag::Sort | btor2tools::Btor2Tag::Output => 0, + _ => match line.sort().content() { + btor2tools::Btor2SortContent::Bitvec { width } => { + usize::try_from(width).unwrap() + } + btor2tools::Btor2SortContent::Array { .. } => 0, // TODO: handle arrays + }, + }) + .collect::>(); + + // Init environment + // let mut env = interp::Environment::new(btor2_lines.len() + 1); + let mut s_env = shared_env::SharedEnvironment::new(node_sorts); + + // Parse inputs + match interp::parse_inputs(&mut s_env, &btor2_lines, &args.inputs) { + Ok(()) => {} + Err(e) => { + eprintln!("{}", e); + std::process::exit(1); + } + }; + + // Main interpreter loop + interp::interpret(btor2_lines.iter(), &mut s_env)?; + + // Print result of execution + if !args.profile { + println!("{}", s_env); + + // Extract outputs + btor2_lines.iter().for_each(|line| { + if let btor2tools::Btor2Tag::Output = line.tag() { + let output_name = + line.symbol().unwrap().to_string_lossy().into_owned(); + let src_node_idx = line.args()[0] as usize; + let output_val = s_env.get(src_node_idx); + + println!("{}: {}", output_name, output_val); + } + }); + } + } + + // print to stderr the time it took to run + let duration = start.elapsed(); + eprintln!("Time elapsed: {} µs", duration.as_micros()); + + Ok(()) +} diff --git a/tools/btor2/btor2i/src/program.rs b/tools/btor2/btor2i/src/program.rs new file mode 100644 index 0000000000..6ece1cc1ab --- /dev/null +++ b/tools/btor2/btor2i/src/program.rs @@ -0,0 +1,124 @@ +use crate::interp; +use crate::shared_env; + +use btor2tools::Btor2Line; +use btor2tools::Btor2Parser; +use std::collections::HashMap; +use std::path::Path; + +use bitvec::prelude::*; + +pub type BitString = BitVec; + +fn slice_to_usize(slice: &BitSlice) -> usize { + let mut ans: usize = 0; + for i in 0..slice.len() { + if slice[i] { + ans += 1 << i; + } + } + ans +} + +// crappy thing that makes it work: no longer store lines, instead pass in reference to file path +pub struct Btor2Program<'a> { + parser: Btor2Parser, + path: &'a Path, + // lines: Option>>, +} + +// impl Default for Btor2Program { +// fn default() -> Self { +// Self::new() +// } +// } + +impl<'a> Btor2Program<'a> { + pub fn new(path: &'a str) -> Self { + Btor2Program { + parser: Btor2Parser::new(), + path: Path::new(path), + } + } + + // pub fn load(&mut self, input_file: &str) -> Result<(), &str> { + // // Parse and store the btor2 file as Vec + // let input_path = Path::new(input_file); + // let btor2_lines_opt = self.parser.read_lines(input_path); + // match btor2_lines_opt { + // Err(e) => { + // eprintln!("{}", e); + // Err("Input file not found.") + // } + // Ok(btor2_lines) => { + // // self.lines = Option::Some(btor2_lines.collect::>()); + // Ok(()) + // } + // } + // } + + pub fn run( + &mut self, + inputs: HashMap, + ) -> Result, &str> { + let btor2_lines: &Vec> = &self + .parser + .read_lines(self.path) + .as_ref() + .unwrap() + .collect::>(); + let mut inputs_vec = Vec::new(); + for (name, val) in &inputs { + inputs_vec.push(format!("{}={} ", name, val)); + } + + let node_sorts = btor2_lines + .iter() + .map(|line| match line.tag() { + btor2tools::Btor2Tag::Sort | btor2tools::Btor2Tag::Output => 0, + _ => match line.sort().content() { + btor2tools::Btor2SortContent::Bitvec { width } => { + usize::try_from(width).unwrap() + } + btor2tools::Btor2SortContent::Array { .. } => 0, // TODO: handle arrays + }, + }) + .collect::>(); + + let mut s_env = shared_env::SharedEnvironment::new(node_sorts); + + // Parse inputs + match interp::parse_inputs(&mut s_env, btor2_lines, &inputs_vec) { + Ok(()) => {} + Err(e) => { + eprintln!("{}", e); + return Err("Inputs invalid."); + } + }; + + // Main interpreter loop + let result = interp::interpret(btor2_lines.iter(), &mut s_env); + match result { + Ok(()) => {} + Err(e) => { + eprintln!("{}", e); + return Err("Runtime error in BTOR2 program."); + } + } + + let mut output_map = HashMap::new(); + + btor2_lines.iter().for_each(|line| { + if let btor2tools::Btor2Tag::Output = line.tag() { + let output_name = + line.symbol().unwrap().to_string_lossy().into_owned(); + let src_node_idx = line.args()[0] as usize; + let output_val = s_env.get(src_node_idx); + + output_map.insert(output_name, slice_to_usize(output_val)); + } + }); + + Ok(output_map) + } +} diff --git a/tools/btor2/btor2i/src/shared_env.rs b/tools/btor2/btor2i/src/shared_env.rs new file mode 100644 index 0000000000..bfa0d3fdf7 --- /dev/null +++ b/tools/btor2/btor2i/src/shared_env.rs @@ -0,0 +1,746 @@ +use num_integer::Integer; +use num_traits::{One, Zero}; +use std::cmp::Ordering; +use std::fmt; +use std::ops::Rem; + +use bitvec::prelude::*; +use num_bigint::{BigInt, BigUint}; +use std::iter::once; + +#[derive(Debug)] +pub struct SharedEnvironment { + shared_bits: BitVec, // RI: integers are little-endian + offsets: Vec, // offsets[i] = start of node i +} + +impl fmt::Display for SharedEnvironment { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "\nEnvironment:\n")?; + + for i in 0..self.offsets.len() - 1 { + if self.offsets[i] == self.offsets[i + 1] { + writeln!(f, "{} : _", i)?; + } else if self.offsets[i + 1] - self.offsets[i] + > (usize::BITS).try_into().unwrap() + { + writeln!(f, "{} : too large to display", i)?; + } else { + writeln!( + f, + "{} : {}", + i, + SharedEnvironment::slice_to_usize( + &self.shared_bits[self.offsets[i]..self.offsets[i + 1]] + ) + )?; + } + } + + Ok(()) + } +} + +impl SharedEnvironment { + pub fn new(node_sorts: Vec) -> Self { + let offsets = once(&0usize) + .chain(once(&0usize)) + .chain(node_sorts.iter()) + .scan(0usize, |state, &x| { + *state += x; + Some(*state) + }) + .collect::>(); + let shared_bits = BitVec::repeat(false, *offsets.last().unwrap()); + SharedEnvironment { + shared_bits, + offsets, + } + } + + /// Sets the bitslice corresponding to the node at with node_id `idx` + pub fn set(&mut self, idx: usize, value: &BitSlice) { + self.shared_bits[self.offsets[idx]..self.offsets[idx + 1]] + .copy_from_bitslice(value); + } + + /// Sets the bitslice corresponding to the node at with node_id `idx`, used for inputs + pub fn set_vec(&mut self, idx: usize, value: Vec) { + for i in self.offsets[idx]..self.offsets[idx + 1] { + self.shared_bits.set(i, value[i - self.offsets[idx]]); + } + } + + /// Returns the bitslice corresponding to the node at with node_id `idx` + pub fn get(&mut self, idx: usize) -> &BitSlice { + &self.shared_bits[self.offsets[idx]..self.offsets[idx + 1]] + } + + pub fn sext(&mut self, i1: usize, i2: usize) { + let old_start = self.offsets[i1]; + let old_end = self.offsets[i1 + 1]; + let new_start = self.offsets[i2]; + let new_end = self.offsets[i2 + 1]; + let first_bit = self.shared_bits[old_start]; + self.shared_bits.copy_within(old_start..old_end, new_start); + self.shared_bits[new_start + (old_end - old_start)..new_end] + .fill(first_bit); + } + + pub fn uext(&mut self, i1: usize, i2: usize) { + let old_start = self.offsets[i1]; + let old_end = self.offsets[i1 + 1]; + let new_start = self.offsets[i2]; + let new_end = self.offsets[i2 + 1]; + self.shared_bits.copy_within(old_start..old_end, new_start); + self.shared_bits[new_start + (old_end - old_start)..new_end] + .fill(false); + } + + pub fn slice(&mut self, u: usize, l: usize, i1: usize, i2: usize) { + let old_start = self.offsets[i1]; + let new_start = self.offsets[i2]; + self.shared_bits + .copy_within(old_start + l..old_start + u + 1, new_start); + } + + pub fn not(&mut self, i1: usize, i2: usize) { + let old_start = self.offsets[i1]; + let old_end = self.offsets[i1 + 1]; + let new_start = self.offsets[i2]; + let new_end = self.offsets[i2 + 1]; + let mut rhs = BitVec::repeat(true, old_end - old_start); + rhs ^= &self.shared_bits[old_start..old_end]; + self.shared_bits[new_start..new_end] + .copy_from_bitslice(rhs.as_bitslice()); + } + + pub fn and(&mut self, i1: usize, i2: usize, i3: usize) { + let mut rhs = BitVec::from_bitslice( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + rhs &= &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .copy_from_bitslice(rhs.as_bitslice()); + } + + pub fn nand(&mut self, i1: usize, i2: usize, i3: usize) { + let mut rhs = BitVec::from_bitslice( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + rhs &= &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + rhs = !rhs; + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .copy_from_bitslice(rhs.as_bitslice()); + } + + pub fn nor(&mut self, i1: usize, i2: usize, i3: usize) { + let mut rhs = BitVec::from_bitslice( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + rhs |= &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + rhs = !rhs; + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .copy_from_bitslice(rhs.as_bitslice()); + } + + pub fn or(&mut self, i1: usize, i2: usize, i3: usize) { + let mut rhs = BitVec::from_bitslice( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + rhs |= &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .copy_from_bitslice(rhs.as_bitslice()); + } + + pub fn xnor(&mut self, i1: usize, i2: usize, i3: usize) { + let mut rhs = BitVec::from_bitslice( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + rhs ^= &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + rhs = !rhs; + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .copy_from_bitslice(rhs.as_bitslice()); + } + + pub fn xor(&mut self, i1: usize, i2: usize, i3: usize) { + let mut rhs = BitVec::from_bitslice( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + rhs ^= &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .copy_from_bitslice(rhs.as_bitslice()); + } + + pub fn concat(&mut self, i1: usize, i2: usize, i3: usize) { + let start1 = self.offsets[i1]; + let end1 = self.offsets[i1 + 1]; + let start2 = self.offsets[i2]; + let end2 = self.offsets[i2 + 1]; + let start3 = self.offsets[i3]; + self.shared_bits.copy_within(start1..end1, start3); + self.shared_bits + .copy_within(start2..end2, start3 + end1 - start1); + } + + fn slice_to_bigint(slice: &BitSlice) -> BigInt { + if slice.is_empty() { + Zero::zero() + } else if slice[slice.len() - 1] { + let z: BigInt = Zero::zero(); + let o: BigInt = One::one(); + let mut ans = z - o; + for i in 0..slice.len() { + ans.set_bit(i.try_into().unwrap(), slice[i]) + } + ans + } else { + let mut ans: BigInt = Zero::zero(); + for i in 0..slice.len() { + ans.set_bit(i.try_into().unwrap(), slice[i]) + } + ans + } + } + + fn slice_to_biguint(slice: &BitSlice) -> BigUint { + let mut ans: BigUint = Zero::zero(); + for i in 0..slice.len() { + ans.set_bit(i.try_into().unwrap(), slice[i]) + } + ans + } + + fn slice_to_usize(slice: &BitSlice) -> usize { + let mut ans: usize = 0; + for i in 0..slice.len() { + if slice[i] { + ans += 1 << i; + } + } + ans + } + + pub fn inc(&mut self, i1: usize, i2: usize) { + self.shared_bits.copy_within( + self.offsets[i1]..self.offsets[i1 + 1], + self.offsets[i2], + ); + let dest = + self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]].as_mut(); + match dest.first_zero() { + Some(i) => { + dest[i..i + 1].fill(true); + dest[..i].fill(false); + } + None => { + dest.fill(false); + } + } + } + + pub fn dec(&mut self, i1: usize, i2: usize) { + self.shared_bits.copy_within( + self.offsets[i1]..self.offsets[i1 + 1], + self.offsets[i2], + ); + let dest = + self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]].as_mut(); + match dest.first_one() { + Some(i) => { + dest[i..i + 1].fill(false); + dest[..i].fill(true); + } + None => { + dest.fill(true); + } + } + } + + pub fn neg(&mut self, i1: usize, i2: usize) { + let bitwise_neg = !BitVec::from_bitslice( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let dest = + self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]].as_mut(); + dest.copy_from_bitslice(&bitwise_neg); + + match dest.first_zero() { + Some(i) => { + dest[i..i + 1].fill(true); + dest[..i].fill(false); + } + None => { + dest.fill(false); + } + } + } + + pub fn redand(&mut self, i1: usize, i2: usize) { + let ans = + self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]].all(); + self.shared_bits[self.offsets[i2]..self.offsets[i2] + 1].fill(ans); + } + + pub fn redor(&mut self, i1: usize, i2: usize) { + let ans = + self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]].any(); + self.shared_bits[self.offsets[i2]..self.offsets[i2] + 1].fill(ans); + } + + pub fn redxor(&mut self, i1: usize, i2: usize) { + let ans = self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]] + .count_ones() + % 2 + == 1; + self.shared_bits[self.offsets[i2]..self.offsets[i2] + 1].fill(ans); + } + + pub fn iff(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = self.shared_bits[self.offsets[i1]] + == self.shared_bits[self.offsets[i2]]; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn implies(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = !self.shared_bits[self.offsets[i1]] + || self.shared_bits[self.offsets[i2]]; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn eq(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]] + == self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn neq(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]] + != self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + fn compare_signed(&self, i1: usize, i2: usize) -> Ordering { + let a = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + a.cmp(&b) + } + + fn compare_unsigned(&self, i1: usize, i2: usize) -> Ordering { + let a = &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]]; + let b = &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]]; + a.cmp(b) + } + + pub fn sgt(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = match self.compare_signed(i1, i2) { + Ordering::Less => false, + Ordering::Equal => false, + Ordering::Greater => true, + }; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn ugt(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = match self.compare_unsigned(i1, i2) { + Ordering::Less => false, + Ordering::Equal => false, + Ordering::Greater => true, + }; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn sgte(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = match self.compare_signed(i1, i2) { + Ordering::Less => false, + Ordering::Equal => true, + Ordering::Greater => true, + }; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn ugte(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = match self.compare_unsigned(i1, i2) { + Ordering::Less => false, + Ordering::Equal => true, + Ordering::Greater => true, + }; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn slt(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = match self.compare_signed(i1, i2) { + Ordering::Greater => false, + Ordering::Equal => false, + Ordering::Less => true, + }; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn ult(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = match self.compare_unsigned(i1, i2) { + Ordering::Greater => false, + Ordering::Equal => false, + Ordering::Less => true, + }; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn slte(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = match self.compare_signed(i1, i2) { + Ordering::Greater => false, + Ordering::Equal => true, + Ordering::Less => true, + }; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn ulte(&mut self, i1: usize, i2: usize, i3: usize) { + let ans = match self.compare_unsigned(i1, i2) { + Ordering::Greater => false, + Ordering::Equal => true, + Ordering::Less => true, + }; + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(ans); + } + + pub fn add(&mut self, i1: usize, i2: usize, i3: usize) { + let a = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + let c = a + b; + for i in self.offsets[i3]..self.offsets[i3 + 1] { + self.shared_bits[i..i + 1] + .fill(c.bit((i - self.offsets[i3]).try_into().unwrap())); + } + } + + pub fn mul(&mut self, i1: usize, i2: usize, i3: usize) { + let a = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + let c = a * b; + for i in self.offsets[i3]..self.offsets[i3 + 1] { + self.shared_bits[i..i + 1] + .fill(c.bit((i - self.offsets[i3]).try_into().unwrap())); + } + } + + pub fn sdiv(&mut self, i1: usize, i2: usize, i3: usize) { + let a = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + let c = a / b; + for i in self.offsets[i3]..self.offsets[i3 + 1] { + self.shared_bits[i..i + 1] + .fill(c.bit((i - self.offsets[i3]).try_into().unwrap())); + } + } + + pub fn udiv(&mut self, i1: usize, i2: usize, i3: usize) { + let a = Self::slice_to_biguint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_biguint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + let c = a / b; + for i in self.offsets[i3]..self.offsets[i3 + 1] { + self.shared_bits[i..i + 1] + .fill(c.bit((i - self.offsets[i3]).try_into().unwrap())); + } + } + + pub fn smod(&mut self, i1: usize, i2: usize, i3: usize) { + let a = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + let c = a.mod_floor(&b); + for i in self.offsets[i3]..self.offsets[i3 + 1] { + self.shared_bits[i..i + 1] + .fill(c.bit((i - self.offsets[i3]).try_into().unwrap())); + } + } + + pub fn srem(&mut self, i1: usize, i2: usize, i3: usize) { + let a = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + let mut c = a.mod_floor(&b); + if a.sign() != b.sign() && !a.is_zero() && !b.is_zero() { + c -= b; + } + for i in self.offsets[i3]..self.offsets[i3 + 1] { + self.shared_bits[i..i + 1] + .fill(c.bit((i - self.offsets[i3]).try_into().unwrap())); + } + } + + pub fn urem(&mut self, i1: usize, i2: usize, i3: usize) { + let a = Self::slice_to_biguint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_biguint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + let c = a.rem(b); + for i in self.offsets[i3]..self.offsets[i3 + 1] { + self.shared_bits[i..i + 1] + .fill(c.bit((i - self.offsets[i3]).try_into().unwrap())); + } + } + + pub fn sub(&mut self, i1: usize, i2: usize, i3: usize) { + let a = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]], + ); + let b = Self::slice_to_bigint( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + let c = a - b; + for i in self.offsets[i3]..self.offsets[i3 + 1] { + self.shared_bits[i..i + 1] + .fill(c.bit((i - self.offsets[i3]).try_into().unwrap())); + } + } + + pub fn saddo(&mut self, _i1: usize, _i2: usize, _i3: usize) { + todo!() + } + + pub fn uaddo(&mut self, _i1: usize, _i2: usize, _i3: usize) { + todo!() + } + + pub fn sdivo(&mut self, _i1: usize, _i2: usize, _i3: usize) { + todo!() + } + + pub fn udivo(&mut self, _i1: usize, _i2: usize, i3: usize) { + self.shared_bits[self.offsets[i3]..self.offsets[i3] + 1].fill(false); + } + + pub fn smulo(&mut self, _i1: usize, _i2: usize, _i3: usize) { + todo!() + } + + pub fn umulo(&mut self, _i1: usize, _i2: usize, _i3: usize) { + todo!() + } + + pub fn ssubo(&mut self, _i1: usize, _i2: usize, _i3: usize) { + todo!() + } + + pub fn usubo(&mut self, _i1: usize, _i2: usize, _i3: usize) { + todo!() + } + + pub fn ite(&mut self, i1: usize, i2: usize, i3: usize, i4: usize) { + if self.shared_bits[self.offsets[i1]] { + self.shared_bits.copy_within( + self.offsets[i2]..self.offsets[i2 + 1], + self.offsets[i4], + ); + } else { + self.shared_bits.copy_within( + self.offsets[i3]..self.offsets[i3 + 1], + self.offsets[i4], + ); + } + } + + pub fn rol(&mut self, i1: usize, i2: usize, i3: usize) { + let shift_amount = Self::slice_to_usize( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + self.shared_bits.copy_within( + self.offsets[i1]..self.offsets[i1 + 1], + self.offsets[i3], + ); + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .rotate_right(shift_amount); + } + + pub fn ror(&mut self, i1: usize, i2: usize, i3: usize) { + let shift_amount = Self::slice_to_usize( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + self.shared_bits.copy_within( + self.offsets[i1]..self.offsets[i1 + 1], + self.offsets[i3], + ); + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .rotate_left(shift_amount); + } + + pub fn sll(&mut self, i1: usize, i2: usize, i3: usize) { + let shift_amount = Self::slice_to_usize( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + self.shared_bits.copy_within( + self.offsets[i1]..self.offsets[i1 + 1], + self.offsets[i3], + ); + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .shift_right(shift_amount); + } + + pub fn sra(&mut self, i1: usize, i2: usize, i3: usize) { + let shift_amount = Self::slice_to_usize( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + self.shared_bits.copy_within( + self.offsets[i1]..self.offsets[i1 + 1], + self.offsets[i3], + ); + let last_bit = self.shared_bits[self.offsets[i1 + 1] - 1]; + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .shift_left(shift_amount); + self.shared_bits + [self.offsets[i3 + 1] - shift_amount..self.offsets[i3 + 1]] + .fill(last_bit); + } + + pub fn srl(&mut self, i1: usize, i2: usize, i3: usize) { + let shift_amount = Self::slice_to_usize( + &self.shared_bits[self.offsets[i2]..self.offsets[i2 + 1]], + ); + self.shared_bits.copy_within( + self.offsets[i1]..self.offsets[i1 + 1], + self.offsets[i3], + ); + self.shared_bits[self.offsets[i3]..self.offsets[i3 + 1]] + .shift_left(shift_amount); + } + + pub fn one(&mut self, i1: usize) { + self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]].fill(false); + self.shared_bits[self.offsets[i1]..self.offsets[i1] + 1].fill(true); // little endian + } + + pub fn ones(&mut self, i1: usize) { + self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]].fill(true); + } + + pub fn zero(&mut self, i1: usize) { + self.shared_bits[self.offsets[i1]..self.offsets[i1 + 1]].fill(false); + } + + pub fn const_(&mut self, i1: usize, value: Vec) { + for i in self.offsets[i1]..self.offsets[i1 + 1] { + self.shared_bits[i..i + 1].fill(value[i - self.offsets[i1]]); + } + } +} + +#[cfg(test)] +mod tests { + + use super::*; + + #[test] + fn test_get_set() { + let node_widths = vec![2, 8, 6]; + let mut s_env = SharedEnvironment::new(node_widths); + assert!(s_env.get(1) == bits![0, 0]); + assert!(s_env.get(2) == bits![0, 0, 0, 0, 0, 0, 0, 0]); + assert!(s_env.get(3) == bits![0, 0, 0, 0, 0, 0]); + + s_env.set(1, bits![0, 1]); + s_env.set(2, bits![0, 1, 0, 1, 1, 1, 1, 1]); + s_env.set(3, bits![0, 1, 0, 0, 0, 0]); + + assert!(s_env.get(1) == bits![0, 1]); + assert!(s_env.get(2) == bits![0, 1, 0, 1, 1, 1, 1, 1]); + assert!(s_env.get(3) == bits![0, 1, 0, 0, 0, 0]); + } + + #[test] + fn test_shift_left() { + let node_widths = vec![2, 8, 6, 8, 8, 8, 8, 8]; + let mut s_env = SharedEnvironment::new(node_widths); + assert!(s_env.get(1) == bits![0, 0]); + assert!(s_env.get(2) == bits![0, 0, 0, 0, 0, 0, 0, 0]); + assert!(s_env.get(3) == bits![0, 0, 0, 0, 0, 0]); + s_env.set_vec(1, vec![false, true]); + s_env + .set_vec(2, vec![false, true, false, true, true, true, true, true]); + s_env.set_vec(3, vec![false, true, false, false, false, false]); + + s_env.sll(2, 1, 4); + s_env.srl(2, 1, 5); + s_env.rol(2, 1, 6); + s_env.ror(2, 1, 7); + s_env.sra(2, 1, 8); + assert!(s_env.get(4) == bits![0, 0, 0, 1, 0, 1, 1, 1]); + assert!(s_env.get(5) == bits![0, 1, 1, 1, 1, 1, 0, 0]); + assert!(s_env.get(6) == bits![1, 1, 0, 1, 0, 1, 1, 1]); + assert!(s_env.get(7) == bits![0, 1, 1, 1, 1, 1, 0, 1]); + assert!(s_env.get(8) == bits![0, 1, 1, 1, 1, 1, 1, 1]); + } + + #[test] + fn test_add_mul() { + let node_widths = vec![8, 8, 8, 8, 8]; + let mut s_env = SharedEnvironment::new(node_widths); + s_env.set(1, bits![1, 1, 0, 0, 0, 0, 0, 0]); + s_env.set(2, bits![1, 1, 1, 0, 0, 0, 0, 0]); + s_env.set(3, bits![1, 1, 1, 1, 1, 0, 0, 0]); + s_env.add(1, 3, 4); + s_env.mul(1, 2, 5); + assert!(s_env.get(4) == bits![0, 1, 0, 0, 0, 1, 0, 0]); + assert!(s_env.get(5) == bits![1, 0, 1, 0, 1, 0, 0, 0]); + } + + #[test] + fn test_bitwise() { + let node_widths = vec![4, 4, 4, 4, 4, 4, 4, 4]; + let mut s_env = SharedEnvironment::new(node_widths); + s_env.set(1, bits![0, 1, 0, 1]); + s_env.set(2, bits![0, 0, 1, 1]); + s_env.and(1, 2, 3); + s_env.nand(1, 2, 4); + s_env.or(1, 2, 5); + s_env.nor(1, 2, 6); + s_env.xor(1, 2, 7); + s_env.xnor(1, 2, 8); + assert!(s_env.get(3) == bits![0, 0, 0, 1]); + assert!(s_env.get(4) == bits![1, 1, 1, 0]); + assert!(s_env.get(5) == bits![0, 1, 1, 1]); + assert!(s_env.get(6) == bits![1, 0, 0, 0]); + assert!(s_env.get(7) == bits![0, 1, 1, 0]); + assert!(s_env.get(8) == bits![1, 0, 0, 1]); + } + + #[test] + fn test_comparisons() { + let node_widths = vec![4, 4, 1, 1]; + let mut s_env = SharedEnvironment::new(node_widths); + s_env.set(1, bits![0, 1, 0, 1]); + s_env.set(2, bits![0, 0, 1, 0]); + s_env.sgt(1, 2, 3); + s_env.ugt(1, 2, 4); + assert!(s_env.get(3) == bits![0]); + assert!(s_env.get(4) == bits![1]); + } +}