From 48f5002163eab14ff992b1b728e47fbe2aca3a64 Mon Sep 17 00:00:00 2001 From: Kevin Laeufer Date: Tue, 5 Nov 2024 10:32:41 -0500 Subject: [PATCH] remove btor code (#2332) Removes all the old btor code that is no longer used. --- Cargo.lock | 270 +------ Cargo.toml | 1 - docs/tools/sv2btor.md | 18 - interp/Cargo.toml | 2 - interp/src/flatten/primitives/btor2_prim.rs | 63 -- 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 -------------------- tools/btor2/core/std_add.btor | 7 - tools/btor2/core/std_and.btor | 7 - tools/btor2/core/std_cat.btor | 8 - tools/btor2/core/std_eq.btor | 8 - tools/btor2/core/std_ge.btor | 8 - tools/btor2/core/std_gt.btor | 8 - tools/btor2/core/std_le.btor | 8 - tools/btor2/core/std_lsh.btor | 7 - tools/btor2/core/std_lt.btor | 8 - tools/btor2/core/std_mem_d1.btor | 97 --- tools/btor2/core/std_mem_d2.btor | 104 --- tools/btor2/core/std_mem_d3.btor | 112 --- tools/btor2/core/std_mem_d4.btor | 117 --- tools/btor2/core/std_mux.btor | 9 - tools/btor2/core/std_neq.btor | 8 - tools/btor2/core/std_not.btor | 6 - tools/btor2/core/std_or.btor | 7 - tools/btor2/core/std_pad.btor | 5 - tools/btor2/core/std_reg.btor | 21 - tools/btor2/core/std_rsh.btor | 7 - tools/btor2/core/std_slice.btor | 5 - tools/btor2/core/std_sub.btor | 7 - tools/btor2/core/std_xor.btor | 7 - tools/btor2/sv2btor.py | 166 ----- tools/btor2/sync/std_sync_reg.btor | 108 --- tools/btor2/verible_verilog_syntax.py | 580 --------------- 44 files changed, 2 insertions(+), 4178 deletions(-) delete mode 100644 docs/tools/sv2btor.md delete mode 100644 interp/src/flatten/primitives/btor2_prim.rs delete mode 100644 tools/btor2/btor2i/Cargo.toml delete mode 100644 tools/btor2/btor2i/Makefile delete mode 100644 tools/btor2/btor2i/README.md delete mode 100644 tools/btor2/btor2i/benchmark.toml delete mode 100644 tools/btor2/btor2i/src/bvec.rs delete mode 100644 tools/btor2/btor2i/src/cli.rs delete mode 100644 tools/btor2/btor2i/src/error.rs delete mode 100644 tools/btor2/btor2i/src/interp.rs delete mode 100644 tools/btor2/btor2i/src/lib.rs delete mode 100644 tools/btor2/btor2i/src/main.rs delete mode 100644 tools/btor2/btor2i/src/program.rs delete mode 100644 tools/btor2/btor2i/src/shared_env.rs delete mode 100644 tools/btor2/core/std_add.btor delete mode 100644 tools/btor2/core/std_and.btor delete mode 100644 tools/btor2/core/std_cat.btor delete mode 100644 tools/btor2/core/std_eq.btor delete mode 100644 tools/btor2/core/std_ge.btor delete mode 100644 tools/btor2/core/std_gt.btor delete mode 100644 tools/btor2/core/std_le.btor delete mode 100644 tools/btor2/core/std_lsh.btor delete mode 100644 tools/btor2/core/std_lt.btor delete mode 100644 tools/btor2/core/std_mem_d1.btor delete mode 100644 tools/btor2/core/std_mem_d2.btor delete mode 100644 tools/btor2/core/std_mem_d3.btor delete mode 100644 tools/btor2/core/std_mem_d4.btor delete mode 100644 tools/btor2/core/std_mux.btor delete mode 100644 tools/btor2/core/std_neq.btor delete mode 100644 tools/btor2/core/std_not.btor delete mode 100644 tools/btor2/core/std_or.btor delete mode 100644 tools/btor2/core/std_pad.btor delete mode 100644 tools/btor2/core/std_reg.btor delete mode 100644 tools/btor2/core/std_rsh.btor delete mode 100644 tools/btor2/core/std_slice.btor delete mode 100644 tools/btor2/core/std_sub.btor delete mode 100644 tools/btor2/core/std_xor.btor delete mode 100644 tools/btor2/sv2btor.py delete mode 100644 tools/btor2/sync/std_sync_reg.btor delete mode 100644 tools/btor2/verible_verilog_syntax.py diff --git a/Cargo.lock b/Cargo.lock index 51660edfe7..7b5156844a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -66,54 +66,6 @@ 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" @@ -247,29 +199,6 @@ 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.58", - "which", -] - [[package]] name = "bit-set" version = "0.5.3" @@ -341,38 +270,6 @@ dependencies = [ "syn 2.0.58", ] -[[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" @@ -576,15 +473,6 @@ 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" @@ -665,17 +553,6 @@ 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" @@ -687,46 +564,6 @@ 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 0.10.0", -] - -[[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.58", -] - -[[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" @@ -738,12 +575,6 @@ dependencies = [ "winapi", ] -[[package]] -name = "colorchoice" -version = "1.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" - [[package]] name = "component_cells" version = "0.7.1" @@ -799,15 +630,6 @@ dependencies = [ "tiny-keccak", ] -[[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" @@ -837,7 +659,7 @@ checksum = "b01d6de93b2b6c65e17c634a26653a29d107b3c98c607c765bf38d041531cd8f" dependencies = [ "atty", "cast", - "clap 2.34.0", + "clap", "criterion-plot", "csv", "itertools 0.10.5", @@ -1447,12 +1269,6 @@ 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" @@ -1520,15 +1336,6 @@ 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" @@ -1646,7 +1453,6 @@ dependencies = [ "baa", "bitvec", "bon", - "btor2i", "calyx-frontend", "calyx-ir", "calyx-opt", @@ -1726,28 +1532,12 @@ 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.52.4", -] - [[package]] name = "libm" version = "0.2.8" @@ -1833,12 +1623,6 @@ 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" @@ -1890,16 +1674,6 @@ 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" @@ -2068,12 +1842,6 @@ 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" @@ -2241,16 +2009,6 @@ 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.58", -] - [[package]] name = "proc-macro2" version = "1.0.78" @@ -2518,12 +2276,6 @@ 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" @@ -2657,7 +2409,7 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5318bfeed779c64075ce317c81462ed54dc00021be1c6b34957d798e11a68bdb" dependencies = [ - "nom 4.2.3", + "nom", "serde", ] @@ -2742,12 +2494,6 @@ dependencies = [ "lazy_static", ] -[[package]] -name = "shlex" -version = "1.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" - [[package]] name = "signal-hook" version = "0.3.17" @@ -3537,18 +3283,6 @@ 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 d509d9a1fd..be30dce2d8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -15,7 +15,6 @@ members = [ "fud2", "fud2/fud-core", "tools/data-conversion", - "tools/btor2/btor2i", "tools/calyx-pass-explorer", "tools/cider-data-converter", "tools/component_cells", diff --git a/docs/tools/sv2btor.md b/docs/tools/sv2btor.md deleted file mode 100644 index 4544aaa21c..0000000000 --- a/docs/tools/sv2btor.md +++ /dev/null @@ -1,18 +0,0 @@ -# `sv2btor` - -The `sv2btor` tool is a tool that leverages `yosys` and -`verible` to translate the SystemVerilog files into BTOR2. - -# Usage - -```bash -Usage: sv2btor.py -``` - -# Installation -To run this tool, you need to have `yosys` and `verible-verilog-syntax` installed. You will also need the `anytree` python package. - -- You can install `yosys` by following the instructions [here](https://github.com/YosysHQ/yosys). -- You can install `verible-verilog-syntax` by following the instructions [here](https://github.com/chipsalliance/verible). Note that we only need the standalone `verible-verilog-syntax` executable, the rest of the tools are optional. -- You can install `anytree` by running `pip install anytree`. - diff --git a/interp/Cargo.toml b/interp/Cargo.toml index e54873bfe8..537518f77b 100644 --- a/interp/Cargo.toml +++ b/interp/Cargo.toml @@ -43,8 +43,6 @@ calyx-utils = { path = "../calyx-utils", features = ["serialize"] } calyx-opt = { path = "../calyx-opt" } calyx-frontend = { path = "../calyx-frontend" } -btor2i = { path = "../tools/btor2/btor2i" } - ciborium = "0.2.2" baa = { version = "0.14.0", features = ["bigint", "serde1", "fraction1"] } fst-writer = "0.2.1" diff --git a/interp/src/flatten/primitives/btor2_prim.rs b/interp/src/flatten/primitives/btor2_prim.rs deleted file mode 100644 index fe74d950f5..0000000000 --- a/interp/src/flatten/primitives/btor2_prim.rs +++ /dev/null @@ -1,63 +0,0 @@ -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 baa::{BitVecValue, WidthInt}; -// use std::env; - -use std::cell::RefCell; -use std::collections::HashMap; - -pub struct MyBtor2Add<'a> { - program: RefCell>, - base_port: GlobalPortIdx, - width: WidthInt, // do stuff -} - -impl<'a> MyBtor2Add<'a> { - declare_ports![ LEFT:0, RIGHT:1, OUT:2 ]; - pub fn new(base: GlobalPortIdx, width: WidthInt) -> 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_u64().unwrap_or(0).to_string(), - ), - ( - "right".to_string(), - port_map[right].as_u64().unwrap_or(0).to_string(), - ), - ]); - match self.program.borrow_mut().run(input_map) { - Ok(output_map) => Ok(port_map.insert_val_general( - out, - AssignedValue::cell_value(BitVecValue::from_u64( - output_map["out"], - self.width, - )), - )?), - Err(msg) => { - panic!("{}", msg); - } - } - } - - fn has_stateful(&self) -> bool { - false - } -} diff --git a/interp/src/flatten/primitives/mod.rs b/interp/src/flatten/primitives/mod.rs index 935e2add53..25c5c0706a 100644 --- a/interp/src/flatten/primitives/mod.rs +++ b/interp/src/flatten/primitives/mod.rs @@ -1,4 +1,3 @@ -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 deleted file mode 100644 index f4c33be76c..0000000000 --- a/tools/btor2/btor2i/Cargo.toml +++ /dev/null @@ -1,17 +0,0 @@ -[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 deleted file mode 100644 index 6e2314837e..0000000000 --- a/tools/btor2/btor2i/Makefile +++ /dev/null @@ -1,18 +0,0 @@ -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 deleted file mode 100644 index 91d6ad0c8b..0000000000 --- a/tools/btor2/btor2i/README.md +++ /dev/null @@ -1,33 +0,0 @@ -# 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 deleted file mode 100644 index 51a72d1a07..0000000000 --- a/tools/btor2/btor2i/benchmark.toml +++ /dev/null @@ -1,37 +0,0 @@ -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 deleted file mode 100644 index bd3faedf89..0000000000 --- a/tools/btor2/btor2i/src/bvec.rs +++ /dev/null @@ -1,718 +0,0 @@ -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 deleted file mode 100644 index b6e8bca7e4..0000000000 --- a/tools/btor2/btor2i/src/cli.rs +++ /dev/null @@ -1,22 +0,0 @@ -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 deleted file mode 100644 index 62d562e753..0000000000 --- a/tools/btor2/btor2i/src/error.rs +++ /dev/null @@ -1,33 +0,0 @@ -// 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 deleted file mode 100644 index 12a1e0e44e..0000000000 --- a/tools/btor2/btor2i/src/interp.rs +++ /dev/null @@ -1,544 +0,0 @@ -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 deleted file mode 100644 index 03dac751a9..0000000000 --- a/tools/btor2/btor2i/src/lib.rs +++ /dev/null @@ -1,6 +0,0 @@ -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 deleted file mode 100644 index 7f0b50fab7..0000000000 --- a/tools/btor2/btor2i/src/main.rs +++ /dev/null @@ -1,92 +0,0 @@ -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 deleted file mode 100644 index 53035d8f58..0000000000 --- a/tools/btor2/btor2i/src/program.rs +++ /dev/null @@ -1,124 +0,0 @@ -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_u64(slice: &BitSlice) -> u64 { - let mut ans = 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_u64(output_val)); - } - }); - - Ok(output_map) - } -} diff --git a/tools/btor2/btor2i/src/shared_env.rs b/tools/btor2/btor2i/src/shared_env.rs deleted file mode 100644 index bfa0d3fdf7..0000000000 --- a/tools/btor2/btor2i/src/shared_env.rs +++ /dev/null @@ -1,746 +0,0 @@ -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]); - } -} diff --git a/tools/btor2/core/std_add.btor b/tools/btor2/core/std_add.btor deleted file mode 100644 index c76e54845f..0000000000 --- a/tools/btor2/core/std_add.btor +++ /dev/null @@ -1,7 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_add. -1 sort bitvec 32 -2 input 1 left ; temp.sv:5.35-5.39 -3 input 1 right ; temp.sv:6.35-6.40 -4 add 1 2 3 -5 output 4 out ; temp.sv:7.35-7.38 -; end of yosys output diff --git a/tools/btor2/core/std_and.btor b/tools/btor2/core/std_and.btor deleted file mode 100644 index 7097df75a7..0000000000 --- a/tools/btor2/core/std_and.btor +++ /dev/null @@ -1,7 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_and. -1 sort bitvec 32 -2 input 1 left ; core.sv:97.35-97.39 -3 input 1 right ; core.sv:98.35-98.40 -4 and 1 2 3 -5 output 4 out ; core.sv:99.35-99.38 -; end of yosys output diff --git a/tools/btor2/core/std_cat.btor b/tools/btor2/core/std_cat.btor deleted file mode 100644 index 56847207b9..0000000000 --- a/tools/btor2/core/std_cat.btor +++ /dev/null @@ -1,8 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_cat. -1 sort bitvec 32 -2 input 1 left ; core.sv:63.39-63.43 -3 input 1 right ; core.sv:64.40-64.45 -4 sort bitvec 64 -5 concat 4 2 3 -6 output 5 out ; core.sv:65.34-65.37 -; end of yosys output diff --git a/tools/btor2/core/std_eq.btor b/tools/btor2/core/std_eq.btor deleted file mode 100644 index 1b4e39b479..0000000000 --- a/tools/btor2/core/std_eq.btor +++ /dev/null @@ -1,8 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_eq. -1 sort bitvec 32 -2 input 1 left ; core.sv:157.34-157.38 -3 input 1 right ; core.sv:158.34-158.39 -4 sort bitvec 1 -5 eq 4 2 3 -6 output 5 out ; core.sv:159.18-159.21 -; end of yosys output diff --git a/tools/btor2/core/std_ge.btor b/tools/btor2/core/std_ge.btor deleted file mode 100644 index 9e55d2f14b..0000000000 --- a/tools/btor2/core/std_ge.btor +++ /dev/null @@ -1,8 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_ge. -1 sort bitvec 32 -2 input 1 left ; core.sv:177.34-177.38 -3 input 1 right ; core.sv:178.34-178.39 -4 sort bitvec 1 -5 ugte 4 2 3 -6 output 5 out ; core.sv:179.18-179.21 -; end of yosys output diff --git a/tools/btor2/core/std_gt.btor b/tools/btor2/core/std_gt.btor deleted file mode 100644 index 9fd09e4a4e..0000000000 --- a/tools/btor2/core/std_gt.btor +++ /dev/null @@ -1,8 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_gt. -1 sort bitvec 32 -2 input 1 left ; core.sv:137.34-137.38 -3 input 1 right ; core.sv:138.34-138.39 -4 sort bitvec 1 -5 ugt 4 2 3 -6 output 5 out ; core.sv:139.18-139.21 -; end of yosys output diff --git a/tools/btor2/core/std_le.btor b/tools/btor2/core/std_le.btor deleted file mode 100644 index c0c9369912..0000000000 --- a/tools/btor2/core/std_le.btor +++ /dev/null @@ -1,8 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_le. -1 sort bitvec 32 -2 input 1 left ; core.sv:187.34-187.38 -3 input 1 right ; core.sv:188.34-188.39 -4 sort bitvec 1 -5 ulte 4 2 3 -6 output 5 out ; core.sv:189.18-189.21 -; end of yosys output diff --git a/tools/btor2/core/std_lsh.btor b/tools/btor2/core/std_lsh.btor deleted file mode 100644 index fa84191dca..0000000000 --- a/tools/btor2/core/std_lsh.btor +++ /dev/null @@ -1,7 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_lsh. -1 sort bitvec 32 -2 input 1 left ; core.sv:197.35-197.39 -3 input 1 right ; core.sv:198.35-198.40 -4 sll 1 2 3 -5 output 4 out ; core.sv:199.35-199.38 -; end of yosys output diff --git a/tools/btor2/core/std_lt.btor b/tools/btor2/core/std_lt.btor deleted file mode 100644 index fcc942c6e9..0000000000 --- a/tools/btor2/core/std_lt.btor +++ /dev/null @@ -1,8 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_lt. -1 sort bitvec 32 -2 input 1 left ; core.sv:147.34-147.38 -3 input 1 right ; core.sv:148.34-148.39 -4 sort bitvec 1 -5 ult 4 2 3 -6 output 5 out ; core.sv:149.18-149.21 -; end of yosys output diff --git a/tools/btor2/core/std_mem_d1.btor b/tools/btor2/core/std_mem_d1.btor deleted file mode 100644 index 34918fe27f..0000000000 --- a/tools/btor2/core/std_mem_d1.btor +++ /dev/null @@ -1,97 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module comb_mem_d1. -1 sort bitvec 4 -2 input 1 addr0 ; core.sv:232.38-232.43 -3 sort bitvec 1 -4 input 3 clk ; core.sv:235.38-235.41 -5 input 3 reset ; core.sv:236.38-236.43 -6 sort bitvec 32 -7 input 6 write_data ; core.sv:233.38-233.48 -8 input 3 write_en ; core.sv:234.38-234.46 -9 state 3 -10 output 9 done ; core.sv:238.38-238.42 -11 sort array 1 6 -12 state 11 mem -13 read 6 12 2 -14 output 13 read_data ; core.sv:237.38-237.47 -15 const 3 0 -16 const 3 1 -17 ite 3 8 16 15 -18 ite 3 5 15 17 -19 next 3 9 18 -20 input 1 -21 not 3 5 -22 and 3 21 8 -23 ite 1 22 2 20 -24 input 6 -25 ite 6 22 7 24 -26 ite 3 22 16 15 -27 sort bitvec 2 -28 concat 27 26 26 -29 sort bitvec 3 -30 concat 29 26 28 -31 concat 1 26 30 -32 sort bitvec 5 -33 concat 32 26 31 -34 sort bitvec 6 -35 concat 34 26 33 -36 sort bitvec 7 -37 concat 36 26 35 -38 sort bitvec 8 -39 concat 38 26 37 -40 sort bitvec 9 -41 concat 40 26 39 -42 sort bitvec 10 -43 concat 42 26 41 -44 sort bitvec 11 -45 concat 44 26 43 -46 sort bitvec 12 -47 concat 46 26 45 -48 sort bitvec 13 -49 concat 48 26 47 -50 sort bitvec 14 -51 concat 50 26 49 -52 sort bitvec 15 -53 concat 52 26 51 -54 sort bitvec 16 -55 concat 54 26 53 -56 sort bitvec 17 -57 concat 56 26 55 -58 sort bitvec 18 -59 concat 58 26 57 -60 sort bitvec 19 -61 concat 60 26 59 -62 sort bitvec 20 -63 concat 62 26 61 -64 sort bitvec 21 -65 concat 64 26 63 -66 sort bitvec 22 -67 concat 66 26 65 -68 sort bitvec 23 -69 concat 68 26 67 -70 sort bitvec 24 -71 concat 70 26 69 -72 sort bitvec 25 -73 concat 72 26 71 -74 sort bitvec 26 -75 concat 74 26 73 -76 sort bitvec 27 -77 concat 76 26 75 -78 sort bitvec 28 -79 concat 78 26 77 -80 sort bitvec 29 -81 concat 80 26 79 -82 sort bitvec 30 -83 concat 82 26 81 -84 sort bitvec 31 -85 concat 84 26 83 -86 concat 6 26 85 -87 read 6 12 23 -88 not 6 86 -89 and 6 87 88 -90 and 6 25 86 -91 or 6 90 89 -92 write 11 12 23 91 -93 redor 3 86 -94 ite 11 93 92 12 -95 next 11 12 94 mem ; core.sv:241.21-241.24 -; end of yosys output diff --git a/tools/btor2/core/std_mem_d2.btor b/tools/btor2/core/std_mem_d2.btor deleted file mode 100644 index 9144f1ebf8..0000000000 --- a/tools/btor2/core/std_mem_d2.btor +++ /dev/null @@ -1,104 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module comb_mem_d2. -1 sort bitvec 4 -2 input 1 addr0 ; core.sv:272.41-272.46 -3 input 1 addr1 ; core.sv:273.41-273.46 -4 sort bitvec 1 -5 input 4 clk ; core.sv:276.41-276.44 -6 input 4 reset ; core.sv:277.41-277.46 -7 sort bitvec 32 -8 input 7 write_data ; core.sv:274.41-274.51 -9 input 4 write_en ; core.sv:275.41-275.49 -10 state 4 -11 output 10 done ; core.sv:279.41-279.45 -12 sort bitvec 8 -13 sort array 12 7 -14 state 13 mem -15 uext 12 2 4 -16 sort bitvec 5 -17 const 16 10000 -18 uext 12 17 3 -19 mul 12 15 18 -20 uext 12 3 4 -21 add 12 19 20 -22 read 7 14 21 -23 output 22 read_data ; core.sv:278.41-278.50 -24 const 4 0 -25 const 4 1 -26 ite 4 9 25 24 -27 ite 4 6 24 26 -28 next 4 10 27 -29 input 12 -30 not 4 6 -31 and 4 30 9 -32 ite 12 31 21 29 -33 input 7 -34 ite 7 31 8 33 -35 ite 4 31 25 24 -36 sort bitvec 2 -37 concat 36 35 35 -38 sort bitvec 3 -39 concat 38 35 37 -40 concat 1 35 39 -41 concat 16 35 40 -42 sort bitvec 6 -43 concat 42 35 41 -44 sort bitvec 7 -45 concat 44 35 43 -46 concat 12 35 45 -47 sort bitvec 9 -48 concat 47 35 46 -49 sort bitvec 10 -50 concat 49 35 48 -51 sort bitvec 11 -52 concat 51 35 50 -53 sort bitvec 12 -54 concat 53 35 52 -55 sort bitvec 13 -56 concat 55 35 54 -57 sort bitvec 14 -58 concat 57 35 56 -59 sort bitvec 15 -60 concat 59 35 58 -61 sort bitvec 16 -62 concat 61 35 60 -63 sort bitvec 17 -64 concat 63 35 62 -65 sort bitvec 18 -66 concat 65 35 64 -67 sort bitvec 19 -68 concat 67 35 66 -69 sort bitvec 20 -70 concat 69 35 68 -71 sort bitvec 21 -72 concat 71 35 70 -73 sort bitvec 22 -74 concat 73 35 72 -75 sort bitvec 23 -76 concat 75 35 74 -77 sort bitvec 24 -78 concat 77 35 76 -79 sort bitvec 25 -80 concat 79 35 78 -81 sort bitvec 26 -82 concat 81 35 80 -83 sort bitvec 27 -84 concat 83 35 82 -85 sort bitvec 28 -86 concat 85 35 84 -87 sort bitvec 29 -88 concat 87 35 86 -89 sort bitvec 30 -90 concat 89 35 88 -91 sort bitvec 31 -92 concat 91 35 90 -93 concat 7 35 92 -94 read 7 14 32 -95 not 7 93 -96 and 7 94 95 -97 and 7 34 93 -98 or 7 97 96 -99 write 13 14 32 98 -100 redor 4 93 -101 ite 13 100 99 14 -102 next 13 14 101 mem ; core.sv:283.21-283.24 -; end of yosys output diff --git a/tools/btor2/core/std_mem_d3.btor b/tools/btor2/core/std_mem_d3.btor deleted file mode 100644 index 2d35a0c1a8..0000000000 --- a/tools/btor2/core/std_mem_d3.btor +++ /dev/null @@ -1,112 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module comb_mem_d3. -1 sort bitvec 4 -2 input 1 addr0 ; core.sv:317.41-317.46 -3 input 1 addr1 ; core.sv:318.41-318.46 -4 input 1 addr2 ; core.sv:319.41-319.46 -5 sort bitvec 1 -6 input 5 clk ; core.sv:322.41-322.44 -7 input 5 reset ; core.sv:323.41-323.46 -8 sort bitvec 32 -9 input 8 write_data ; core.sv:320.41-320.51 -10 input 5 write_en ; core.sv:321.41-321.49 -11 state 5 -12 output 11 done ; core.sv:325.41-325.45 -13 sort bitvec 12 -14 sort array 13 8 -15 state 14 mem -16 sort bitvec 9 -17 uext 16 2 5 -18 sort bitvec 5 -19 const 18 10000 -20 uext 16 19 4 -21 mul 16 17 20 -22 sort bitvec 23 -23 const 22 00000000000000000000000 -24 concat 8 23 21 -25 uext 8 3 28 -26 add 8 24 25 -27 uext 8 19 27 -28 mul 8 26 27 -29 slice 13 28 11 0 -30 uext 13 4 8 -31 add 13 29 30 -32 read 8 15 31 -33 output 32 read_data ; core.sv:324.41-324.50 -34 const 5 0 -35 const 5 1 -36 ite 5 10 35 34 -37 ite 5 7 34 36 -38 next 5 11 37 -39 input 13 -40 not 5 7 -41 and 5 40 10 -42 ite 13 41 31 39 -43 input 8 -44 ite 8 41 9 43 -45 ite 5 41 35 34 -46 sort bitvec 2 -47 concat 46 45 45 -48 sort bitvec 3 -49 concat 48 45 47 -50 concat 1 45 49 -51 concat 18 45 50 -52 sort bitvec 6 -53 concat 52 45 51 -54 sort bitvec 7 -55 concat 54 45 53 -56 sort bitvec 8 -57 concat 56 45 55 -58 concat 16 45 57 -59 sort bitvec 10 -60 concat 59 45 58 -61 sort bitvec 11 -62 concat 61 45 60 -63 concat 13 45 62 -64 sort bitvec 13 -65 concat 64 45 63 -66 sort bitvec 14 -67 concat 66 45 65 -68 sort bitvec 15 -69 concat 68 45 67 -70 sort bitvec 16 -71 concat 70 45 69 -72 sort bitvec 17 -73 concat 72 45 71 -74 sort bitvec 18 -75 concat 74 45 73 -76 sort bitvec 19 -77 concat 76 45 75 -78 sort bitvec 20 -79 concat 78 45 77 -80 sort bitvec 21 -81 concat 80 45 79 -82 sort bitvec 22 -83 concat 82 45 81 -84 concat 22 45 83 -85 sort bitvec 24 -86 concat 85 45 84 -87 sort bitvec 25 -88 concat 87 45 86 -89 sort bitvec 26 -90 concat 89 45 88 -91 sort bitvec 27 -92 concat 91 45 90 -93 sort bitvec 28 -94 concat 93 45 92 -95 sort bitvec 29 -96 concat 95 45 94 -97 sort bitvec 30 -98 concat 97 45 96 -99 sort bitvec 31 -100 concat 99 45 98 -101 concat 8 45 100 -102 read 8 15 42 -103 not 8 101 -104 and 8 102 103 -105 and 8 44 101 -106 or 8 105 104 -107 write 14 15 42 106 -108 redor 5 101 -109 ite 14 108 107 15 -110 next 14 15 109 mem ; core.sv:329.21-329.24 -; end of yosys output diff --git a/tools/btor2/core/std_mem_d4.btor b/tools/btor2/core/std_mem_d4.btor deleted file mode 100644 index 16d6bf7d31..0000000000 --- a/tools/btor2/core/std_mem_d4.btor +++ /dev/null @@ -1,117 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module comb_mem_d4. -1 sort bitvec 4 -2 input 1 addr0 ; core.sv:367.41-367.46 -3 input 1 addr1 ; core.sv:368.41-368.46 -4 input 1 addr2 ; core.sv:369.41-369.46 -5 input 1 addr3 ; core.sv:370.41-370.46 -6 sort bitvec 1 -7 input 6 clk ; core.sv:373.41-373.44 -8 input 6 reset ; core.sv:374.41-374.46 -9 sort bitvec 32 -10 input 9 write_data ; core.sv:371.41-371.51 -11 input 6 write_en ; core.sv:372.41-372.49 -12 state 6 -13 output 12 done ; core.sv:376.41-376.45 -14 sort bitvec 16 -15 sort array 14 9 -16 state 15 mem -17 sort bitvec 9 -18 uext 17 2 5 -19 sort bitvec 5 -20 const 19 10000 -21 uext 17 20 4 -22 mul 17 18 21 -23 sort bitvec 23 -24 const 23 00000000000000000000000 -25 concat 9 24 22 -26 uext 9 3 28 -27 add 9 25 26 -28 uext 9 20 27 -29 mul 9 27 28 -30 uext 9 4 28 -31 add 9 29 30 -32 uext 9 20 27 -33 mul 9 31 32 -34 slice 14 33 15 0 -35 uext 14 5 12 -36 add 14 34 35 -37 read 9 16 36 -38 output 37 read_data ; core.sv:375.41-375.50 -39 const 6 0 -40 const 6 1 -41 ite 6 11 40 39 -42 ite 6 8 39 41 -43 next 6 12 42 -44 input 14 -45 not 6 8 -46 and 6 45 11 -47 ite 14 46 36 44 -48 input 9 -49 ite 9 46 10 48 -50 ite 6 46 40 39 -51 sort bitvec 2 -52 concat 51 50 50 -53 sort bitvec 3 -54 concat 53 50 52 -55 concat 1 50 54 -56 concat 19 50 55 -57 sort bitvec 6 -58 concat 57 50 56 -59 sort bitvec 7 -60 concat 59 50 58 -61 sort bitvec 8 -62 concat 61 50 60 -63 concat 17 50 62 -64 sort bitvec 10 -65 concat 64 50 63 -66 sort bitvec 11 -67 concat 66 50 65 -68 sort bitvec 12 -69 concat 68 50 67 -70 sort bitvec 13 -71 concat 70 50 69 -72 sort bitvec 14 -73 concat 72 50 71 -74 sort bitvec 15 -75 concat 74 50 73 -76 concat 14 50 75 -77 sort bitvec 17 -78 concat 77 50 76 -79 sort bitvec 18 -80 concat 79 50 78 -81 sort bitvec 19 -82 concat 81 50 80 -83 sort bitvec 20 -84 concat 83 50 82 -85 sort bitvec 21 -86 concat 85 50 84 -87 sort bitvec 22 -88 concat 87 50 86 -89 concat 23 50 88 -90 sort bitvec 24 -91 concat 90 50 89 -92 sort bitvec 25 -93 concat 92 50 91 -94 sort bitvec 26 -95 concat 94 50 93 -96 sort bitvec 27 -97 concat 96 50 95 -98 sort bitvec 28 -99 concat 98 50 97 -100 sort bitvec 29 -101 concat 100 50 99 -102 sort bitvec 30 -103 concat 102 50 101 -104 sort bitvec 31 -105 concat 104 50 103 -106 concat 9 50 105 -107 read 9 16 47 -108 not 9 106 -109 and 9 107 108 -110 and 9 49 106 -111 or 9 110 109 -112 write 15 16 47 111 -113 redor 6 106 -114 ite 15 113 112 16 -115 next 15 16 114 mem ; core.sv:380.21-380.24 -; end of yosys output diff --git a/tools/btor2/core/std_mux.btor b/tools/btor2/core/std_mux.btor deleted file mode 100644 index 995a6f3946..0000000000 --- a/tools/btor2/core/std_mux.btor +++ /dev/null @@ -1,9 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_mux. -1 sort bitvec 1 -2 input 1 cond ; core.sv:219.35-219.39 -3 sort bitvec 32 -4 input 3 fal ; core.sv:221.35-221.38 -5 input 3 tru ; core.sv:220.35-220.38 -6 ite 3 2 5 4 -7 output 6 out ; core.sv:222.35-222.38 -; end of yosys output diff --git a/tools/btor2/core/std_neq.btor b/tools/btor2/core/std_neq.btor deleted file mode 100644 index a69d287254..0000000000 --- a/tools/btor2/core/std_neq.btor +++ /dev/null @@ -1,8 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_neq. -1 sort bitvec 32 -2 input 1 left ; core.sv:167.34-167.38 -3 input 1 right ; core.sv:168.34-168.39 -4 sort bitvec 1 -5 neq 4 2 3 -6 output 5 out ; core.sv:169.18-169.21 -; end of yosys output diff --git a/tools/btor2/core/std_not.btor b/tools/btor2/core/std_not.btor deleted file mode 100644 index a27bcf1ba0..0000000000 --- a/tools/btor2/core/std_not.btor +++ /dev/null @@ -1,6 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_not. -1 sort bitvec 32 -2 input 1 in ; core.sv:88.35-88.37 -3 not 1 2 -4 output 3 out ; core.sv:89.35-89.38 -; end of yosys output diff --git a/tools/btor2/core/std_or.btor b/tools/btor2/core/std_or.btor deleted file mode 100644 index 1b8787e357..0000000000 --- a/tools/btor2/core/std_or.btor +++ /dev/null @@ -1,7 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_or. -1 sort bitvec 32 -2 input 1 left ; core.sv:107.35-107.39 -3 input 1 right ; core.sv:108.35-108.40 -4 or 1 2 3 -5 output 4 out ; core.sv:109.35-109.38 -; end of yosys output diff --git a/tools/btor2/core/std_pad.btor b/tools/btor2/core/std_pad.btor deleted file mode 100644 index f4a988eeb9..0000000000 --- a/tools/btor2/core/std_pad.btor +++ /dev/null @@ -1,5 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_pad. -1 sort bitvec 32 -2 input 1 in ; core.sv:38.39-38.41 -3 output 2 out ; core.sv:39.39-39.42 -; end of yosys output diff --git a/tools/btor2/core/std_reg.btor b/tools/btor2/core/std_reg.btor deleted file mode 100644 index 98a6b9ebed..0000000000 --- a/tools/btor2/core/std_reg.btor +++ /dev/null @@ -1,21 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_reg. -1 sort bitvec 1 -2 input 1 clk ; temp.sv:7.31-7.34 -3 sort bitvec 32 -4 input 3 in ; temp.sv:5.31-5.33 -5 input 1 reset ; temp.sv:8.31-8.36 -6 input 1 write_en ; temp.sv:6.31-6.39 -7 state 1 -8 output 7 done ; temp.sv:11.31-11.35 -9 state 3 -10 output 9 out ; temp.sv:10.31-10.34 -11 const 1 0 -12 const 1 1 -13 ite 1 6 12 11 -14 ite 1 5 11 13 -15 next 1 7 14 -16 ite 3 6 4 9 ; input if write_en else existing 9 state val -17 const 3 00000000000000000000000000000000 -18 ite 3 5 17 16 ; 32 bit 0 if reset else 16 -19 next 3 9 18 -; end of yosys output diff --git a/tools/btor2/core/std_rsh.btor b/tools/btor2/core/std_rsh.btor deleted file mode 100644 index fd7ac517cb..0000000000 --- a/tools/btor2/core/std_rsh.btor +++ /dev/null @@ -1,7 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_rsh. -1 sort bitvec 32 -2 input 1 left ; core.sv:207.35-207.39 -3 input 1 right ; core.sv:208.35-208.40 -4 srl 1 2 3 -5 output 4 out ; core.sv:209.35-209.38 -; end of yosys output diff --git a/tools/btor2/core/std_slice.btor b/tools/btor2/core/std_slice.btor deleted file mode 100644 index 4fc2197342..0000000000 --- a/tools/btor2/core/std_slice.btor +++ /dev/null @@ -1,5 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_slice. -1 sort bitvec 32 -2 input 1 in ; core.sv:15.39-15.41 -3 output 2 out ; core.sv:16.39-16.42 -; end of yosys output diff --git a/tools/btor2/core/std_sub.btor b/tools/btor2/core/std_sub.btor deleted file mode 100644 index e3c8c5cf8e..0000000000 --- a/tools/btor2/core/std_sub.btor +++ /dev/null @@ -1,7 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_sub. -1 sort bitvec 32 -2 input 1 left ; core.sv:127.35-127.39 -3 input 1 right ; core.sv:128.35-128.40 -4 sub 1 2 3 -5 output 4 out ; core.sv:129.35-129.38 -; end of yosys output diff --git a/tools/btor2/core/std_xor.btor b/tools/btor2/core/std_xor.btor deleted file mode 100644 index a6d9e663b4..0000000000 --- a/tools/btor2/core/std_xor.btor +++ /dev/null @@ -1,7 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_xor. -1 sort bitvec 32 -2 input 1 left ; core.sv:117.35-117.39 -3 input 1 right ; core.sv:118.35-118.40 -4 xor 1 2 3 -5 output 4 out ; core.sv:119.35-119.38 -; end of yosys output diff --git a/tools/btor2/sv2btor.py b/tools/btor2/sv2btor.py deleted file mode 100644 index 8f0636c86a..0000000000 --- a/tools/btor2/sv2btor.py +++ /dev/null @@ -1,166 +0,0 @@ -""" -Generates a .btor file for each module in each .sv file in the current directory -""" -import os -import json -import subprocess -import sys -import anytree -import tempfile -import verible_verilog_syntax - - -# Adapted from verible examples: -# https://github.com/chipsalliance/verible/blob/e76eb275b8e6739e9c9edc9e35032b193e0ce187/verilog/tools/syntax/export_json_examples/print_modules.py -def process_file_data(path: str, data: verible_verilog_syntax.SyntaxData): - """Print information about modules found in SystemVerilog file. - - This function uses verible_verilog_syntax.Node methods to find module - declarations and specific tokens containing following information: - - * module name - * module port names - * module parameter names - * module imports - * module header code - - Args: - path: Path to source file (used only for informational purposes) - data: Parsing results returned by one of VeribleVerilogSyntax' parse_* - methods. - """ - if not data.tree: - return - - modules_info = [] - - # Collect information about each module declaration in the file - for module in data.tree.iter_find_all({"tag": "kModuleDeclaration"}): - module_info = { - "header_text": "", - "name": "", - "ports": [], - "parameters": [], - "imports": [], - } - - # Find module header - header = module.find({"tag": "kModuleHeader"}) - if not header: - continue - module_info["header_text"] = header.text - - # Find module name - name = header.find( - {"tag": ["SymbolIdentifier", "EscapedIdentifier"]}, - iter_=anytree.PreOrderIter, - ) - if not name: - continue - module_info["name"] = name.text - - # Get the list of ports - for port in header.iter_find_all({"tag": ["kPortDeclaration", "kPort"]}): - port_id = port.find({"tag": ["SymbolIdentifier", "EscapedIdentifier"]}) - module_info["ports"].append(port_id.text) - - # Get the list of parameters - for param in header.iter_find_all({"tag": ["kParamDeclaration"]}): - param_id = param.find({"tag": ["SymbolIdentifier", "EscapedIdentifier"]}) - module_info["parameters"].append(param_id.text) - - # Get the list of imports - for pkg in module.iter_find_all({"tag": ["kPackageImportItem"]}): - module_info["imports"].append(pkg.text) - - modules_info.append(module_info) - - return modules_info - - -def gen_btor(yosys_executable, sv_filename, modules_info, out_dir="."): - """ - Generates a .btor file for each module in the given .sv file - """ - # create a temporary file (.ys) for the synthesis script - _, synthesis_script_path = tempfile.mkstemp(suffix=".ys") - - # modify the synthesis script with a different prep -top for each module - for module_info in modules_info: - with open(synthesis_script_path, "w") as f: - f.write(f"read -sv {sv_filename}\n") - f.write(f"prep -top {module_info['name']}\n") - f.write( - f"write_btor -s {os.path.join(out_dir, module_info['name'])}.btor\n" - ) - f.close() - - # print contents of synthesis script - # with open(synthesis_script_path, "r") as f: - # print(f.read()) - - # run yosys - conversion_process = subprocess.Popen( - [yosys_executable, synthesis_script_path], - stdout=subprocess.PIPE, - stderr=subprocess.PIPE, - ) - btor_out, btor_err = conversion_process.communicate() - if btor_err: - print(btor_err.decode("utf-8")) - return 1 - - -def main(): - if len(sys.argv) < 5: - args_desc = [ - "PATH_TO_YOSYS_EXECUTABLE", - "PATH_TO_VERIBLE_VERILOG_SYNTAX", - "OUTPUT_DIR", - "VERILOG_FILE [VERILOG_FILE [...]]", - ] - print(f"Usage: {sys.argv[0]} {' '.join(args_desc)}") - return 1 - - yosys_path = sys.argv[1] - parser_path = sys.argv[2] - output_dir = sys.argv[3] - file_paths = sys.argv[4:] - - # validate - if not os.path.exists(yosys_path): - print(f"Error: {yosys_path} does not exist") - return 1 - if not os.path.exists(parser_path): - print(f"Error: {parser_path} does not exist") - return 1 - if not os.path.exists(output_dir): - os.makedirs(output_dir) - - # if the output directory is not empty, warn the user that it will be overwritten and confirm - if os.listdir(output_dir): - print(f"Warning: {output_dir} is not empty, and will be overwritten") - print("Continue? [y/N]") - if input().lower() != "y": - return 1 - - # clear the output directory - for f in os.listdir(output_dir): - os.remove(os.path.join(output_dir, f)) - - # parse the files - parser = verible_verilog_syntax.VeribleVerilogSyntax(executable=parser_path) - data = parser.parse_files(file_paths) - - for file_path, file_data in data.items(): - modules_info = process_file_data(file_path, file_data) - gen_btor( - yosys_path, - file_path, - modules_info, - output_dir, - ) - - -if __name__ == "__main__": - sys.exit(main()) diff --git a/tools/btor2/sync/std_sync_reg.btor b/tools/btor2/sync/std_sync_reg.btor deleted file mode 100644 index c66be0f4fa..0000000000 --- a/tools/btor2/sync/std_sync_reg.btor +++ /dev/null @@ -1,108 +0,0 @@ -; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_sync_reg. -1 sort bitvec 1 -2 input 1 clk ; sync.sv:22.31-22.34 -3 sort bitvec 32 -4 input 3 in_0 ; sync.sv:16.31-16.35 -5 input 3 in_1 ; sync.sv:17.31-17.35 -6 input 1 read_en_0 ; sync.sv:18.31-18.40 -7 input 1 read_en_1 ; sync.sv:19.31-19.40 -8 input 1 reset ; sync.sv:23.31-23.36 -9 input 1 write_en_0 ; sync.sv:20.31-20.41 -10 input 1 write_en_1 ; sync.sv:21.31-21.41 -11 state 3 -12 output 11 out_0 ; sync.sv:25.31-25.36 -13 state 3 -14 output 13 out_1 ; sync.sv:26.31-26.36 -15 state 3 -16 output 15 peek ; sync.sv:31.31-31.35 -17 state 1 -18 output 17 read_done_0 ; sync.sv:29.31-29.42 -19 state 1 -20 output 19 read_done_1 ; sync.sv:30.31-30.42 -21 state 1 -22 output 21 write_done_0 ; sync.sv:27.31-27.43 -23 state 1 -24 output 23 write_done_1 ; sync.sv:28.31-28.43 -25 state 1 is_full -26 xor 1 6 7 -27 and 1 25 26 -28 and 1 27 6 -29 and 1 6 7 -30 and 1 25 29 -31 state 1 arbiter_r -32 not 1 31 -33 and 1 30 32 -34 or 1 28 33 -35 uext 1 34 0 READ_0 ; sync.sv:40.79-40.85 -36 and 1 27 7 -37 and 1 30 31 -38 or 1 36 37 -39 uext 1 38 0 READ_1 ; sync.sv:40.87-40.93 -40 uext 1 30 0 READ_MULT ; sync.sv:40.23-40.32 -41 uext 1 27 0 READ_ONE_HOT ; sync.sv:40.9-40.21 -42 not 1 25 -43 xor 1 9 10 -44 and 1 42 43 -45 and 1 44 9 -46 and 1 9 10 -47 and 1 42 46 -48 state 1 arbiter_w -49 not 1 48 -50 and 1 47 49 -51 or 1 45 50 -52 uext 1 51 0 WRITE_0 ; sync.sv:40.61-40.68 -53 and 1 44 10 -54 and 1 47 48 -55 or 1 53 54 -56 uext 1 55 0 WRITE_1 ; sync.sv:40.70-40.77 -57 uext 1 47 0 WRITE_MULT ; sync.sv:40.49-40.59 -58 uext 1 44 0 WRITE_ONE_HOT ; sync.sv:40.34-40.47 -59 state 3 state -60 input 3 -61 ite 3 34 59 60 -62 const 3 00000000000000000000000000000000 -63 ite 3 8 62 61 -64 next 3 11 63 -65 input 3 -66 ite 3 38 59 65 -67 ite 3 8 62 66 -68 next 3 13 67 -69 ite 3 55 5 15 -70 ite 3 51 4 69 -71 ite 3 8 62 70 -72 next 3 15 71 -73 const 1 0 -74 const 1 1 -75 ite 1 34 74 73 -76 ite 1 8 73 75 -77 next 1 17 76 -78 ite 1 38 74 73 -79 ite 1 8 73 78 -80 next 1 19 79 -81 ite 1 51 74 73 -82 ite 1 8 73 81 -83 next 1 21 82 -84 ite 1 55 74 73 -85 ite 1 8 73 84 -86 next 1 23 85 -87 or 1 27 30 -88 ite 1 87 73 25 -89 or 1 44 47 -90 ite 1 89 74 88 -91 ite 1 8 73 90 -92 next 1 25 91 -93 ite 1 37 73 31 -94 ite 1 33 74 93 -95 ite 1 8 73 94 -96 next 1 31 95 -97 ite 1 54 73 48 -98 ite 1 50 74 97 -99 ite 1 8 73 98 -100 next 1 48 99 -101 input 3 -102 ite 3 87 101 59 -103 ite 3 55 5 102 -104 ite 3 51 4 103 -105 ite 3 8 62 104 -106 next 3 59 105 -; end of yosys output diff --git a/tools/btor2/verible_verilog_syntax.py b/tools/btor2/verible_verilog_syntax.py deleted file mode 100644 index 06332297b8..0000000000 --- a/tools/btor2/verible_verilog_syntax.py +++ /dev/null @@ -1,580 +0,0 @@ -# Copyright 2017-2020 The Verible Authors. -# -# Licensed under the Apache License, Version 2.0 (the "License"); -# you may not use this file except in compliance with the License. -# You may obtain a copy of the License at -# -# http://www.apache.org/licenses/LICENSE-2.0 -# -# Unless required by applicable law or agreed to in writing, software -# distributed under the License is distributed on an "AS IS" BASIS, -# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -# See the License for the specific language governing permissions and -# limitations under the License. -"""Wrapper for ``verible-verilog-syntax --export_json``""" - -import collections -import json -import re -import subprocess -from typing import Any, Callable, Dict, Iterable, List, Optional, Union - -import anytree -import dataclasses - -_CSI_SEQUENCE = re.compile("\033\\[.*?m") - - -def _colorize(formats: List[str], strings: List[str]) -> str: - result = "" - fi = 0 - for s in strings: - result += f"\033[{formats[fi]}m{s}\033[0m" - fi = (fi + 1) % len(formats) - return result - - -# Type aliases - -CallableFilter = Callable[["Node"], bool] -KeyValueFilter = Dict[str, Union[str, List[str]]] -TreeIterator = Union["_TreeIteratorBase", anytree.iterators.AbstractIter] - - -# Custom tree iterators with an option for reverse children iteration - - -class _TreeIteratorBase: - def __init__( - self, - tree: "Node", - filter_: Optional[CallableFilter] = None, - reverse_children: bool = False, - ): - self.tree = tree - self.reverse_children = reverse_children - self.filter_ = filter_ if filter_ else lambda n: True - - def __iter__(self) -> Iterable["Node"]: - yield from self._iter_tree(self.tree) - - def _iter_children(self, tree: Optional["Node"]) -> Iterable["Node"]: - if not tree or not hasattr(tree, "children"): - return [] - return tree.children if not self.reverse_children else reversed(tree.children) - - def _iter_tree(self, tree: Optional["Node"]) -> Iterable["Node"]: - raise NotImplementedError("Subclass must implement '_iter_tree' method") - - -class PreOrderTreeIterator(_TreeIteratorBase): - def _iter_tree(self, tree: Optional["Node"]) -> Iterable["Node"]: - if self.filter_(tree): - yield tree - for child in self._iter_children(tree): - yield from self._iter_tree(child) - - -class PostOrderTreeIterator(_TreeIteratorBase): - def _iter_tree(self, tree: Optional["Node"]) -> Iterable["Node"]: - for child in self._iter_children(tree): - yield from self._iter_tree(child) - if self.filter_(tree): - yield tree - - -class LevelOrderTreeIterator(_TreeIteratorBase): - def _iter_tree(self, tree: Optional["Node"]) -> Iterable["Node"]: - queue = collections.deque([tree]) - while len(queue) > 0: - n = queue.popleft() - if self.filter_(n): - yield n - queue.extend(self._iter_children(n)) - - -class Node(anytree.NodeMixin): - """Base VeribleVerilogSyntax syntax tree node. - - Attributes: - parent (Optional[Node]): Parent node. - """ - - def __init__(self, parent: Optional["Node"] = None): - self.parent = parent - - @property - def syntax_data(self) -> Optional["SyntaxData"]: - """Parent SyntaxData""" - return self.parent.syntax_data if self.parent else None - - @property - def start(self) -> Optional[int]: - """Byte offset of node's first character in source text""" - raise NotImplementedError("Subclass must implement 'start' property") - - @property - def end(self) -> Optional[int]: - """Byte offset of a character just past the node in source text.""" - raise NotImplementedError("Subclass must implement 'end' property") - - @property - def text(self) -> str: - """Source code fragment spanning all tokens in a node.""" - start = self.start - end = self.end - sd = self.syntax_data - if ( - (start is not None) - and (end is not None) - and sd - and sd.source_code - and end <= len(sd.source_code) - ): - return sd.source_code[start:end].decode("utf-8") - return "" - - def __repr__(self) -> str: - return _CSI_SEQUENCE.sub("", self.to_formatted_string()) - - def to_formatted_string(self) -> str: - """Print node representation formatted for printing in terminal.""" - return super().__repr__() - - -class BranchNode(Node): - """Syntax tree branch node - - Attributes: - tag (str): Node tag. - children (Optional[Node]): Child nodes. - """ - - def __init__( - self, - tag: str, - parent: Optional[Node] = None, - children: Optional[List[Node]] = None, - ): - super().__init__(parent) - self.tag = tag - self.children = children if children is not None else [] - - @property - def start(self) -> Optional[int]: - first_token = self.find( - lambda n: isinstance(n, TokenNode), iter_=PostOrderTreeIterator - ) - return first_token.start if first_token else None - - @property - def end(self) -> Optional[int]: - last_token = self.find( - lambda n: isinstance(n, TokenNode), - iter_=PostOrderTreeIterator, - reverse_children=True, - ) - return last_token.end if last_token else None - - def iter_find_all( - self, - filter_: Union[CallableFilter, KeyValueFilter, None], - max_count: int = 0, - iter_: TreeIterator = LevelOrderTreeIterator, - **kwargs, - ) -> Iterable[Node]: - """Iterate all nodes matching specified filter. - - Args: - filter_: Describes what to search for. Might be: - * Callable taking Node as an argument and returning True for accepted - nodes. - * Dict mapping Node attribute names to searched value or list of - searched values. - max_count: Stop searching after finding that many matching nodes. - iter_: Tree iterator. Decides in what order nodes are visited. - - Yields: - Nodes matching specified filter. - """ - - def as_list(v): - return v if isinstance(v, list) else [v] - - if filter_ and not callable(filter_): - filters = filter_ - - def f(node): - for attr, value in filters.items(): - if not hasattr(node, attr): - return False - if getattr(node, attr) not in as_list(value): - return False - return True - - filter_ = f - - for node in iter_(self, filter_, **kwargs): - yield node - max_count -= 1 - if max_count == 0: - break - - def find( - self, - filter_: Union[CallableFilter, KeyValueFilter, None], - iter_: TreeIterator = LevelOrderTreeIterator, - **kwargs, - ) -> Optional[Node]: - """Find node matching specified filter. - - Args: - filter_: Describes what to search for. Might be: - * Callable taking Node as an argument and returning True for accepted - node. - * Dict mapping Node attribute names to searched value or list of - searched values. - iter_: Tree iterator. Decides in what order nodes are visited. - - Returns: - First Node matching filter. - """ - return next( - self.iter_find_all(filter_, max_count=1, iter_=iter_, **kwargs), None - ) - - def find_all( - self, - filter_: Union[CallableFilter, KeyValueFilter, None], - max_count: int = 0, - iter_: TreeIterator = LevelOrderTreeIterator, - **kwargs, - ) -> List[Node]: - """Find all nodes matching specified filter. - - Args: - filter_: Describes what to search for. Might be: - * Callable taking Node as an argument and returning True for accepted - nodes. - * Dict mapping Node attribute names to searched value or list of - searched values. - max_count: Stop searching after finding that many matching nodes. - iter_: Tree iterator. Decides in what order nodes are visited. - - Returns: - List of nodes matching specified filter. - """ - return list( - self.iter_find_all(filter_, max_count=max_count, iter_=iter_, **kwargs) - ) - - def to_formatted_string(self) -> str: - tag = self.tag if self.tag == repr(self.tag)[1:-1] else repr(self.tag) - return _colorize(["37", "1;97"], ["[", tag, "]"]) - - -class RootNode(BranchNode): - """Syntax tree root node.""" - - def __init__( - self, - tag: str, - syntax_data: Optional["SyntaxData"] = None, - children: Optional[List[Node]] = None, - ): - super().__init__(tag, None, children) - self._syntax_data = syntax_data - - @property - def syntax_data(self) -> Optional["SyntaxData"]: - return self._syntax_data - - -class LeafNode(Node): - """Syntax tree leaf node. - - This specific class is used for null nodes. - """ - - @property - def start(self) -> None: - """Byte offset of token's first character in source text""" - return None - - @property - def end(self) -> None: - """Byte offset of a character just past the token in source text.""" - return None - - def to_formatted_string(self) -> str: - return _colorize(["90"], ["null"]) - - -class TokenNode(LeafNode): - """Tree node with token data - - Represents single token in a syntax tree. - - Attributes: - tag (str): Token tag. - """ - - def __init__(self, tag: str, start: int, end: int, parent: Optional[Node] = None): - super().__init__(parent) - self.tag = tag - self._start = start - self._end = end - - @property - def start(self) -> int: - return self._start - - @property - def end(self) -> int: - return self._end - - def to_formatted_string(self) -> str: - tag = self.tag if self.tag == repr(self.tag)[1:-1] else repr(self.tag) - parts = [ - _colorize(["37", "1;97"], ["[", tag, "]"]), - _colorize(["33", "93"], ["@(", self.start, "-", self.end, ")"]), - ] - text = self.text - if self.tag != text: - parts.append(_colorize(["32", "92"], ["'", repr(text)[1:-1], "'"])) - return " ".join(parts) - - -class Token: - """Token data - - Represents single token in tokens and rawtokens lists. - - Attributes: - tag (str): Token tag. - start (int): Byte offset of token's first character in source text. - end (int): Byte offset of a character just past the token in source text. - syntax_data (Optional["SyntaxData"]): Parent SyntaxData. - """ - - def __init__( - self, tag: str, start: int, end: int, syntax_data: Optional["SyntaxData"] = None - ): - self.tag = tag - self.start = start - self.end = end - self.syntax_data = syntax_data - - @property - def text(self) -> str: - """Token text in source code.""" - sd = self.syntax_data - if sd and sd.source_code and self.end <= len(sd.source_code): - return sd.source_code[self.start : self.end].decode("utf-8") - return "" - - def __repr__(self) -> str: - return _CSI_SEQUENCE.sub("", self.to_formatted_string()) - - def to_formatted_string(self) -> str: - tag = self.tag if self.tag == repr(self.tag)[1:-1] else repr(self.tag) - parts = [ - _colorize(["37", "1;97"], ["[", tag, "]"]), - _colorize(["33", "93"], ["@(", self.start, "-", self.end, ")"]), - _colorize(["32", "92"], ["'", repr(self.text)[1:-1], "'"]), - ] - return " ".join(parts) - - -@dataclasses.dataclass -class Error: - line: int - column: int - phase: str - message: str = "" - - -@dataclasses.dataclass -class SyntaxData: - source_code: Optional[str] = None - tree: Optional[RootNode] = None - tokens: Optional[List[Token]] = None - rawtokens: Optional[List[Token]] = None - errors: Optional[List[Error]] = None - - -class VeribleVerilogSyntax: - """``verible-verilog-syntax`` wrapper. - - This class provides methods for running ``verible-verilog-syntax`` and - transforming its output into Python data structures. - - Args: - executable: path to ``verible-verilog-syntax`` binary. - """ - - def __init__(self, executable: str = "verible-verilog-syntax"): - self.executable = executable - - @staticmethod - def _transform_tree(tree, data: SyntaxData, skip_null: bool) -> RootNode: - def transform(tree): - if tree is None: - return None - if "children" in tree: - children = [ - transform(child) or LeafNode() - for child in tree["children"] - if not (skip_null and child is None) - ] - tag = tree["tag"] - return BranchNode(tag, children=children) - tag = tree["tag"] - start = tree["start"] - end = tree["end"] - return TokenNode(tag, start, end) - - if "children" not in tree: - return None - - children = [ - transform(child) or LeafNode() - for child in tree["children"] - if not (skip_null and child is None) - ] - tag = tree["tag"] - return RootNode(tag, syntax_data=data, children=children) - - @staticmethod - def _transform_tokens(tokens, data: SyntaxData) -> List[Token]: - return [Token(t["tag"], t["start"], t["end"], data) for t in tokens] - - @staticmethod - def _transform_errors(tokens) -> List[Error]: - return [ - Error(t["line"], t["column"], t["phase"], t.get("message", None)) - for t in tokens - ] - - def _parse( - self, paths: List[str], input_: str = None, options: Dict[str, Any] = None - ) -> Dict[str, SyntaxData]: - """Common implementation of parse_* methods""" - options = { - "gen_tree": True, - "skip_null": False, - "gen_tokens": False, - "gen_rawtokens": False, - **(options or {}), - } - - args = ["-export_json"] - if options["gen_tree"]: - args.append("-printtree") - if options["gen_tokens"]: - args.append("-printtokens") - if options["gen_rawtokens"]: - args.append("-printrawtokens") - - proc = subprocess.run( - [self.executable, *args, *paths], - stdout=subprocess.PIPE, - input=input_, - encoding="utf-8", - check=False, - ) - - json_data = json.loads(proc.stdout) - data = {} - for file_path, file_json in json_data.items(): - file_data = SyntaxData() - - if file_path == "-": - file_data.source_code = input_.encode("utf-8") - else: - with open(file_path, "rb") as f: - file_data.source_code = f.read() - - if "tree" in file_json: - file_data.tree = VeribleVerilogSyntax._transform_tree( - file_json["tree"], file_data, options["skip_null"] - ) - - if "tokens" in file_json: - file_data.tokens = VeribleVerilogSyntax._transform_tokens( - file_json["tokens"], file_data - ) - - if "rawtokens" in file_json: - file_data.rawtokens = VeribleVerilogSyntax._transform_tokens( - file_json["rawtokens"], file_data - ) - - if "errors" in file_json: - file_data.errors = VeribleVerilogSyntax._transform_errors( - file_json["errors"] - ) - - data[file_path] = file_data - - return data - - def parse_files( - self, paths: List[str], options: Dict[str, Any] = None - ) -> Dict[str, SyntaxData]: - """Parse multiple SystemVerilog files. - - Args: - paths: list of paths to files to parse. - options: dict with parsing options. - Available options: - gen_tree (boolean): whether to generate syntax tree. - skip_null (boolean): null nodes won't be stored in a tree if True. - gen_tokens (boolean): whether to generate tokens list. - gen_rawtokens (boolean): whether to generate raw token list. - By default only ``gen_tree`` is True. - - Returns: - A dict that maps file names to their parsing results in SyntaxData object. - """ - return self._parse(paths, options=options) - - def parse_file( - self, path: str, options: Dict[str, Any] = None - ) -> Optional[SyntaxData]: - """Parse single SystemVerilog file. - - Args: - path: path to a file to parse. - options: dict with parsing options. - Available options: - gen_tree (boolean): whether to generate syntax tree. - skip_null (boolean): null nodes won't be stored in a tree if True. - gen_tokens (boolean): whether to generate tokens list. - gen_rawtokens (boolean): whether to generate raw token list. - By default only ``gen_tree`` is True. - - Returns: - Parsing results in SyntaxData object. - """ - return self._parse([path], options=options).get(path, None) - - def parse_string( - self, string: str, options: Dict[str, Any] = None - ) -> Optional[SyntaxData]: - """Parse a string with SystemVerilog code. - - Args: - string: SystemVerilog code to parse. - options: dict with parsing options. - Available options: - gen_tree (boolean): whether to generate syntax tree. - skip_null (boolean): null nodes won't be stored in a tree if True. - gen_tokens (boolean): whether to generate tokens list. - gen_rawtokens (boolean): whether to generate raw token list. - By default only ``gen_tree`` is True. - - Returns: - Parsing results in SyntaxData object. - """ - return self._parse(["-"], input_=string, options=options).get("-", None)