diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml index 24ae5490..476da313 100644 --- a/.github/workflows/nightly.yml +++ b/.github/workflows/nightly.yml @@ -38,6 +38,7 @@ jobs: env: RUST_BACKTRACE: full RUSTC_WRAPPER: sccache + RUST_LOG: debug RUST_MIN_STACK: 104857600 - name: Build Release diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 7fa11490..5c2eb77c 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -38,3 +38,4 @@ jobs: env: RUST_BACKTRACE: full RUSTC_WRAPPER: sccache + RUST_LOG: debug diff --git a/.github/workflows/test_address_sanitizer.yml b/.github/workflows/test_address_sanitizer.yml index 5f40007f..7bf202dc 100644 --- a/.github/workflows/test_address_sanitizer.yml +++ b/.github/workflows/test_address_sanitizer.yml @@ -55,3 +55,4 @@ jobs: env: RUST_BACKTRACE: full RUSTC_WRAPPER: sccache + RUST_LOG: debug diff --git a/.github/workflows/test_thread_sanitizer.yml b/.github/workflows/test_thread_sanitizer.yml index c6ffdb81..9ec3f1aa 100644 --- a/.github/workflows/test_thread_sanitizer.yml +++ b/.github/workflows/test_thread_sanitizer.yml @@ -54,3 +54,4 @@ jobs: env: RUST_BACKTRACE: full RUSTC_WRAPPER: sccache + RUST_LOG: debug diff --git a/.gitignore b/.gitignore index 1933a508..475cc393 100644 --- a/.gitignore +++ b/.gitignore @@ -2,12 +2,6 @@ # will have compiled files and executables /target/ -# Folder generated by WASM. -**/*/dist/ - -# will have the code coverage report -/coverage/ - # These are backup files generated by rustfmt **/*.rs.bk diff --git a/Cargo.lock b/Cargo.lock index d117582c..6387f8d1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2488,6 +2488,12 @@ dependencies = [ "hashbrown", ] +[[package]] +name = "indoc" +version = "2.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" + [[package]] name = "input" version = "0.8.3" @@ -2958,6 +2964,7 @@ dependencies = [ "mcrl2", "rec-tests", "sabre", + "sabre-compiling", ] [[package]] @@ -3967,6 +3974,22 @@ dependencies = [ "test-log", ] +[[package]] +name = "sabre-compiling" +version = "0.1.0" +dependencies = [ + "duct", + "env_logger", + "indoc", + "libloading 0.8.3", + "log", + "mcrl2", + "sabre", + "temp-dir", + "test-log", + "toml", +] + [[package]] name = "same-file" version = "1.0.6" @@ -4489,6 +4512,12 @@ dependencies = [ "xattr", ] +[[package]] +name = "temp-dir" +version = "0.1.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1f227968ec00f0e5322f9b8173c7a0cbcff6181a0a5b28e9892491c286277231" + [[package]] name = "tempfile" version = "3.10.1" diff --git a/Cargo.toml b/Cargo.toml index 4557ad70..e8c83cec 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -31,11 +31,14 @@ cc = "1.0" clap = { version = "4.5", features = ["derive"] } cxx = "1.0" cxx-build = { version = "1.0", features = ["parallel"] } +duct = "0.13" env_logger = "0.11" fxhash = "0.2" html-escape = "0.2" +indoc = "2.0" itertools = "0.13" jemallocator = "0.5" +libloading = "0.8" log = "0.4" once_cell = "1.19" pest = "2.7" @@ -48,9 +51,11 @@ rustc-hash = "2.0.0" smallvec = "1.13" streaming-iterator = "0.1" syn = { version = "2.0", features = ["full", "extra-traits"] } +temp-dir = "0.1" test-case = "3.3" test-log = "0.2" thiserror = "1.0" +toml = "0.8" trybuild = "1.0" # Used for GUI tools @@ -61,7 +66,6 @@ tokio = { version = "1.37", features = ["rt", "macros"] } winapi = "0.3" # Only used for xtask -duct = "0.13" fs_extra = "1.3" glob = "0.3" human-sort = "0.2" @@ -77,4 +81,5 @@ mcrl2-macros = { path = "libraries/mcrl2-macros" } mcrl2-sys = { path = "libraries/mcrl2-sys" } rec-tests = { path = "libraries/rec-tests" } sabre = { path = "libraries/sabre" } +sabre-compiling = { path = "libraries/sabre-compiling" } utilities = { path = "libraries/utilities" } \ No newline at end of file diff --git a/libraries/mcrl2/src/aterm/term.rs b/libraries/mcrl2/src/aterm/term.rs index 9097db44..bb8acc8b 100644 --- a/libraries/mcrl2/src/aterm/term.rs +++ b/libraries/mcrl2/src/aterm/term.rs @@ -27,6 +27,7 @@ use super::global_aterm_pool::GLOBAL_TERM_POOL; /// where we look at the argument of a term and want to return it's name, but /// this is not allowed since the temporary returned by the argument is dropped. #[derive(Hash, PartialEq, Eq, PartialOrd, Ord)] +#[repr(transparent)] pub struct ATermRef<'a> { term: *const ffi::_aterm, marker: PhantomData<&'a ()>, @@ -201,6 +202,7 @@ impl<'a> fmt::Debug for ATermRef<'a> { /// The protected version of [ATermRef], mostly derived from it. #[derive(Default)] +#[repr(C)] pub struct ATerm { pub(crate) term: ATermRef<'static>, pub(crate) root: usize, diff --git a/libraries/mcrl2/src/data/data_terms.rs b/libraries/mcrl2/src/data/data_terms.rs index 40075366..924422c9 100644 --- a/libraries/mcrl2/src/data/data_terms.rs +++ b/libraries/mcrl2/src/data/data_terms.rs @@ -82,6 +82,7 @@ mod inner { /// - bag enumeration /// #[mcrl2_term(is_data_expression)] + #[repr(transparent)] pub struct DataExpression { term: ATerm, } diff --git a/libraries/sabre-compiling/Cargo.toml b/libraries/sabre-compiling/Cargo.toml new file mode 100644 index 00000000..cd107a69 --- /dev/null +++ b/libraries/sabre-compiling/Cargo.toml @@ -0,0 +1,22 @@ +[package] +name = "sabre-compiling" +version.workspace = true +rust-version.workspace = true +edition.workspace = true + +[dependencies] +duct.workspace = true +indoc.workspace = true +libloading.workspace = true +temp-dir.workspace = true +toml.workspace = true +env_logger.workspace = true +log.workspace = true +mcrl2.workspace = true +sabre.workspace = true + +[dev-dependencies] +test-log.workspace = true + +[build-dependencies] +toml.workspace = true \ No newline at end of file diff --git a/libraries/sabre-compiling/build.rs b/libraries/sabre-compiling/build.rs new file mode 100644 index 00000000..f6286e49 --- /dev/null +++ b/libraries/sabre-compiling/build.rs @@ -0,0 +1,37 @@ +use std::env; +use std::error::Error; +use std::fs; +use std::fs::File; + +use std::io::Write; + +/// Write every environment variable in the variables array. +fn write_env(writer: &mut impl Write, variables: &[&'static str]) -> Result<(), Box> { + for var in variables { + writeln!(writer, "{} = '{}'", var, env::var(var).unwrap_or_default())?; + } + + Ok(()) +} + +fn main() -> Result<(), Box> { + for (from, to) in env::vars() { + println!("{} to {}", from, to); + } + + let mut file = File::create("../../target/Compilation.toml")?; + + // Write the development location. + writeln!(file, "[sabrec]")?; + writeln!( + file, + "path = '{}'", + fs::canonicalize(".")?.to_string_lossy() + )?; + + // Write compilation related environment variables to the configuration file. + writeln!(file, "[env]")?; + write_env(&mut file, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"])?; + + Ok(()) +} diff --git a/libraries/sabre-compiling/src/innermost_codegen.rs b/libraries/sabre-compiling/src/innermost_codegen.rs new file mode 100644 index 00000000..5659f38e --- /dev/null +++ b/libraries/sabre-compiling/src/innermost_codegen.rs @@ -0,0 +1,108 @@ +use std::collections::HashSet; +use std::error::Error; +use std::fmt; +use std::fs::File; +use std::io::Write; +use std::path::Path; +use std::path::PathBuf; + +use indoc::indoc; +use sabre::set_automaton::SetAutomaton; +use sabre::utilities::ExplicitPosition; +use sabre::RewriteSpecification; + +pub fn generate(spec: &RewriteSpecification, source_dir: &Path) -> Result<(), Box> { + let mut file = File::create(PathBuf::from(source_dir).join("lib.rs"))?; + + // Generate the automata used for matching + let apma = SetAutomaton::new(spec, |_| (), true); + + writeln!( + &mut file, + indoc! {"use mcrl2::data::DataExpression; + use mcrl2::data::DataExpressionRef; + + /// Generic rewrite function + #[no_mangle] + pub unsafe extern \"C\" fn rewrite(term: &DataExpression) -> DataExpression {{ + rewrite_0(&term.copy()) + }} + "} + )?; + + // Introduce a match function for every state of the set automaton. + let mut positions: HashSet = HashSet::new(); + + for (index, state) in apma.states().iter().enumerate() { + + writeln!(&mut file, "fn rewrite_{}(t: &DataExpressionRef<'_>) -> DataExpression {{", index)?; + writeln!(&mut file, "\t let arg = get_position_{}(t);", UnderscoreFormatter(state.label()))?; + writeln!(&mut file, "\t let symbol = arg.data_function_symbol();")?; + + positions.insert(state.label().clone()); + + writeln!(&mut file, "\t match symbol.operation_id() {{")?; + + for ((from, symbol), transition) in apma.transitions() { + // TODO: Only take outgoing directly. + if *from == index { + writeln!(&mut file, "\t\t{symbol} => {{")?; + + // Continue on the outgoing transition. + for (_announcement, _annotation) in transition.announcements() { + + } + + writeln!(&mut file, "\t\t\tt.protect()")?; + writeln!(&mut file, "\t\t}}")?; + } + } + + // No match + writeln!(&mut file, indoc! { + "\t\t_ => {{ + \t\t t.protect() + \t\t}}"})?; + + writeln!(&mut file, "\t }}")?; + writeln!(&mut file, "}}")?; + } + + // Introduce getters for all the positions that must be read from terms. + for position in &positions { + writeln!(&mut file, "fn get_position_{}<'a>(t: &'a DataExpressionRef<'_>) -> DataExpressionRef<'a> {{", UnderscoreFormatter(position))?; + write!(&mut file, "\t t.copy()")?; + + for index in &position.indices { + write!(&mut file, ".arg({index})")?; + } + + writeln!(&mut file, ".upgrade(t).into()")?; + writeln!(&mut file, "}}")?; + } + + Ok(()) +} + +struct UnderscoreFormatter<'a>(&'a ExplicitPosition); + +impl fmt::Display for UnderscoreFormatter<'_> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + + if self.0.indices.is_empty() { + write!(f, "epsilon")?; + } else { + let mut first = true; + for p in &self.0.indices { + if first { + write!(f, "{}", p)?; + first = false; + } else { + write!(f, "_{}", p)?; + } + } + } + + Ok(()) + } +} \ No newline at end of file diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs new file mode 100644 index 00000000..918b3e26 --- /dev/null +++ b/libraries/sabre-compiling/src/lib.rs @@ -0,0 +1,11 @@ +//! +//! This module contains an implementation for a compiling variant of the Sabre +//! rewrite engine. +//! + +mod innermost_codegen; +mod library; +mod sabre_compiling; + +pub use innermost_codegen::*; +pub use sabre_compiling::*; diff --git a/libraries/sabre-compiling/src/library.rs b/libraries/sabre-compiling/src/library.rs new file mode 100644 index 00000000..670a1d82 --- /dev/null +++ b/libraries/sabre-compiling/src/library.rs @@ -0,0 +1,159 @@ +use std::error::Error; +use std::fs::File; +use std::fs::{self}; +use std::io::Write; +use std::path::Path; +use std::path::PathBuf; + +use libloading::Library; +use toml::map::Map; +use toml::Table; +use toml::Value; + +use duct::cmd; +use duct::Expression; +use indoc::indoc; +use log::info; + +/// Apply the value from compilation_toml for every given variable as an environment variable. +fn apply_env( + builder: Expression, + compilation_toml: &Map, + variables: &[&'static str], +) -> Result> { + let mut result = builder; + let env = compilation_toml.get("env").ok_or("Missing [env] table")?; + + for var in variables { + let value = env + .get(*var) + .ok_or("Missing var")? + .as_str() + .ok_or("Not a string")?; + + info!("Setting environment variable {} = {}", var, value); + result = result.env(var, value); + } + + Ok(result) +} + +/// A library that can be used to generate a crate on-the-fly and load it back +/// in after compiling at runtime. +pub struct RuntimeLibrary { + source_dir: PathBuf, + temp_dir: PathBuf, +} + +impl RuntimeLibrary { + /// Creates a new library that can be compiled at runtime. + /// - depe + pub fn new( + temp_dir: &Path, + dependencies: Vec, + ) -> Result> { + info!( + "Creating library in directory {}", + temp_dir.to_string_lossy() + ); + let source_dir = PathBuf::from(temp_dir).join("src"); + + // Create the directory structure for a Cargo project + if !temp_dir.exists() { + fs::create_dir(&temp_dir)?; + } + + if !source_dir.exists() { + fs::create_dir(&source_dir)?; + } + + // Write the cargo configuration + { + let mut file = File::create(PathBuf::from(temp_dir).join("Cargo.toml"))?; + writeln!( + &mut file, + indoc! {" + [package] + name = \"sabre-generated\" + edition = \"2021\" + rust-version = \"1.70.0\" + version = \"0.1.0\" + + [workspace] + + [dependencies] + "} + )?; + + for dependency in &dependencies { + writeln!(&mut file, "{dependency}")?; + } + + writeln!( + &mut file, + indoc! {" + + [lib] + crate-type = [\"cdylib\", \"rlib\"] + "} + )?; + } + + // Ignore the created package. + { + let mut file = File::create(PathBuf::from(temp_dir).join(".gitignore"))?; + writeln!(&mut file, "*.*")?; + } + + Ok(RuntimeLibrary { + temp_dir: PathBuf::from(temp_dir), + source_dir, + }) + } + + /// Returns the directory in which the source files can be placed. + pub fn source_dir(&self) -> &PathBuf { + &self.source_dir + } + + /// Compiles the library into + pub fn compile(&mut self) -> Result> { + let compilation_toml = include_str!("../../../target/Compilation.toml").parse::()?; + + // Compile the dynamic object. + info!("Compiling..."); + let mut expr = cmd("cargo", &["build", "--lib"]).dir(self.temp_dir.as_path()); + expr = apply_env( + expr, + &compilation_toml, + &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"], + )?; + expr.run()?; + + info!("finished."); + + // Figure out the path to the library (it is based on platform: linux, windows and then macos) + let mut path = self + .temp_dir + .clone() + .join("./target/debug/libsabre_generated.so"); + if !path.exists() { + path = self + .temp_dir + .clone() + .join("./target/debug/sabre_generated.dll"); + if !path.exists() { + path = self + .temp_dir + .clone() + .join("./target/debug/libsabre_generated.dylib"); + if !path.exists() { + return Err("Could not find the compiled library!".into()); + } + } + } + + // Load it back in and call the rewriter. + unsafe { Ok(Library::new(&path)?) } + } +} diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs new file mode 100644 index 00000000..fdd39aaf --- /dev/null +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -0,0 +1,121 @@ +use std::cell::RefCell; +use std::error::Error; +use std::path::Path; +use std::path::PathBuf; +use std::rc::Rc; + +use libloading::Library; +use libloading::Symbol; +use log::info; +use temp_dir::TempDir; +use toml::Table; + +use mcrl2::aterm::TermPool; +use mcrl2::data::DataExpression; +use sabre::RewriteEngine; +use sabre::RewriteSpecification; + +use crate::generate; +use crate::library::RuntimeLibrary; + +pub struct SabreCompilingRewriter { + library: Library, + //rewrite_func: Symbol u32>, +} + +impl RewriteEngine for SabreCompilingRewriter { + fn rewrite(&mut self, term: DataExpression) -> DataExpression { + // TODO: This ought to be stored somewhere for repeated calls. + unsafe { + let func: Symbol DataExpression> = self.library.get(b"rewrite").unwrap(); + + let result = func(&term); + std::mem::forget(result); + + term + } + } +} + +impl SabreCompilingRewriter { + /// Creates a new compiling rewriter for the given specifications. + /// + /// - use_local_workspace: Use the developement version of the toolset instead of referring to the github one. + /// - use_local_tmp: Use a relative 'tmp' directory instead of using the system directory. Mostly used for debugging purposes. + /// + /// - [`RewriteEngine`] + pub fn new( + _tp: Rc>, + spec: &RewriteSpecification, + use_local_workspace: bool, + use_local_tmp: bool, + ) -> Result> { + let system_tmp_dir = TempDir::new()?; + let temp_dir = if use_local_tmp { + &Path::new("./tmp") + } else { + system_tmp_dir.path() + }; + + let mut dependencies = vec![]; + + if use_local_workspace { + let compilation_toml = + include_str!("../../../target/Compilation.toml").parse::
()?; + let path = compilation_toml + .get("sabrec") + .ok_or("Missing [sabre] section)")? + .get("path") + .ok_or("Missing path entry")? + .as_str() + .ok_or("Not a string")?; + + info!("Using local dependency {}", path); + dependencies.push(format!( + "mcrl2 = {{ path = '{}' }}", + PathBuf::from(path).join("../mcrl2").to_string_lossy() + )); + } else { + info!("Using git dependency https://github.com/mlaveaux/mCRL2-rust.git"); + dependencies.push( + "sabre-ffi = { git = 'https://github.com/mlaveaux/mCRL2-rust.git' }".to_string(), + ); + } + + let mut compilation_crate = RuntimeLibrary::new(temp_dir, dependencies)?; + + + // Write the output source file(s). + generate(spec, compilation_crate.source_dir())?; + + let library = compilation_crate.compile()?; + Ok(SabreCompilingRewriter { library }) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + use mcrl2::data::DataSpecification; + use test_log::test; + + #[test] + fn test_compilation() { + + let spec = DataSpecification::new(" + map f: Bool # Bool -> Bool; + + eqn f(true, false) = false; + ").unwrap(); + + let t = spec.parse("f(true, false)").unwrap(); + + let spec = RewriteSpecification::from(spec); + let tp = Rc::new(RefCell::new(TermPool::new())); + + let mut rewriter = SabreCompilingRewriter::new(tp, &spec, true, true).unwrap(); + + assert_eq!(rewriter.rewrite(t.clone()), t, "The rewritten result does not match the expected result"); + } +} diff --git a/libraries/sabre/src/innermost_rewriter.rs b/libraries/sabre/src/innermost_rewriter.rs index fcb71b1d..2046e894 100644 --- a/libraries/sabre/src/innermost_rewriter.rs +++ b/libraries/sabre/src/innermost_rewriter.rs @@ -165,7 +165,7 @@ impl InnermostRewriter { "rewrite {} => {} using rule {}", term, annotation.rhs_stack.evaluate(tp, &term), - announcement.rule + announcement.rule() ); // Reacquire the write access and add the matching RHSStack. @@ -195,7 +195,7 @@ impl InnermostRewriter { .pop() .expect("The result should be the last element on the stack") .protect(); - } + }, } let read_configs = stack.configs.read(); @@ -229,19 +229,18 @@ impl InnermostRewriter { // Start at the initial state let mut state_index = 0; loop { - let state = &automaton.states[state_index]; + let state = &automaton.states()[state_index]; // Get the symbol at the position state.label stats.symbol_comparisons += 1; - let pos: DataExpressionRef<'_> = t.get_position(&state.label).into(); + let pos: DataExpressionRef<'_> = t.get_position(&state.label()).into(); let symbol = pos.data_function_symbol(); // Get the transition for the label and check if there is a pattern match if let Some(transition) = automaton - .transitions - .get(&(state_index, symbol.operation_id())) + .transition(state_index, symbol.operation_id()) { - for (announcement, annotation) in &transition.announcements { + for (announcement, annotation) in transition.announcements() { if check_equivalence_classes(t, &annotation.equivalence_classes) && InnermostRewriter::check_conditions( tp, stack, builder, stats, automaton, annotation, t, @@ -253,12 +252,12 @@ impl InnermostRewriter { } // If there is no pattern match we check if the transition has a destination state - if transition.destinations.is_empty() { + if transition.destinations().is_empty() { // If there is no destination state there is no pattern match return None; } else { // Continue matching in the next state - state_index = transition.destinations.first().unwrap().1; + state_index = transition.destinations().first().unwrap().1; } } else { return None; diff --git a/libraries/sabre/src/sabre_rewriter.rs b/libraries/sabre/src/sabre_rewriter.rs index 4755772b..e1ea0371 100644 --- a/libraries/sabre/src/sabre_rewriter.rs +++ b/libraries/sabre/src/sabre_rewriter.rs @@ -108,7 +108,7 @@ impl SabreRewriter { None => { // Observe a symbol according to the state label of the set automaton. let pos: DataExpressionRef = leaf_term - .get_position(&automaton.states[leaf.state].label) + .get_position(&automaton.states()[leaf.state].label()) .into(); let function_symbol = pos.data_function_symbol(); @@ -116,18 +116,17 @@ impl SabreRewriter { // Get the transition belonging to the observed symbol if let Some(tr) = automaton - .transitions - .get(&(leaf.state, function_symbol.operation_id())) + .transition(leaf.state, function_symbol.operation_id()) { // Loop over the match announcements of the transition - for (announcement, annotation) in &tr.announcements { + for (announcement, annotation) in tr.announcements() { if annotation.conditions.is_empty() && annotation.equivalence_classes.is_empty() { if annotation.is_duplicating { trace!( "Delaying duplicating rule {}", - announcement.rule + announcement.rule() ); // We do not want to apply duplicating rules straight away @@ -155,7 +154,7 @@ impl SabreRewriter { // We delay the condition checks trace!( "Delaying condition check for rule {}", - announcement.rule + announcement.rule() ); cs.side_branch_stack.push(SideInfo { corresponding_configuration: leaf_index, @@ -167,7 +166,7 @@ impl SabreRewriter { } } - if tr.destinations.is_empty() { + if tr.destinations().is_empty() { // If there is no destination we are done matching and go back to the previous // configuration on the stack with information on the side stack. // Note, it could be that we stay at the same configuration and apply a rewrite @@ -179,7 +178,7 @@ impl SabreRewriter { } } else { // Grow the bud; if there is more than one destination a SideBranch object will be placed on the side stack - let tr_slice = tr.destinations.as_slice(); + let tr_slice = tr.destinations().as_slice(); cs.grow(leaf_index, tr_slice); } } else { @@ -266,16 +265,16 @@ impl SabreRewriter { // Computes the new subterm of the configuration let new_subterm = annotation .semi_compressed_rhs - .evaluate(&leaf_subterm.get_position(&announcement.position), tp) + .evaluate(&leaf_subterm.get_position(&announcement.position()), tp) .into(); debug!( "rewrote {} to {} using rule {}", - &leaf_subterm, &new_subterm, announcement.rule + &leaf_subterm, &new_subterm, announcement.rule() ); // The match announcement tells us how far we need to prune back. - let prune_point = leaf_index - announcement.symbols_seen; + let prune_point = leaf_index - announcement.symbols_seen(); cs.prune(tp, automaton, prune_point, new_subterm); } @@ -289,7 +288,7 @@ impl SabreRewriter { stats: &mut RewritingStatistics, ) -> bool { for c in &annotation.conditions { - let subterm = subterm.get_position(&announcement.position); + let subterm = subterm.get_position(&announcement.position()); let rhs: DataExpression = c.semi_compressed_rhs.evaluate(&subterm, tp).into(); let lhs: DataExpression = c.semi_compressed_lhs.evaluate(&subterm, tp).into(); diff --git a/libraries/sabre/src/set_automaton/automaton.rs b/libraries/sabre/src/set_automaton/automaton.rs index a559ecba..10480710 100644 --- a/libraries/sabre/src/set_automaton/automaton.rs +++ b/libraries/sabre/src/set_automaton/automaton.rs @@ -38,34 +38,30 @@ use super::MatchGoal; // of Computing – ICTAC 2021. ICTAC 2021. Lecture Notes in Computer Science(), // vol 12819. Springer, Cham. https://doi.org/10.1007/978-3-030-85315-0_5 pub struct SetAutomaton { - pub(crate) states: Vec, - pub(crate) transitions: HashMap<(usize, usize), Transition>, + states: Vec, + + /// Stores the from, symbol, to in a hash table. + transitions: HashMap<(usize, usize), Transition>, } #[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] -pub(crate) struct MatchAnnouncement { - pub rule: Rule, - pub position: ExplicitPosition, - pub symbols_seen: usize, +pub struct MatchAnnouncement { + rule: Rule, + pub (crate) position: ExplicitPosition, + symbols_seen: usize, } #[derive(Clone)] pub struct Transition { - pub(crate) symbol: DataFunctionSymbol, - pub(crate) announcements: SmallVec<[(MatchAnnouncement, T); 1]>, - pub(crate) destinations: SmallVec<[(ExplicitPosition, usize); 1]>, -} - -#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] -pub(crate) struct MatchObligation { - pub pattern: DataExpression, - pub position: ExplicitPosition, + symbol: DataFunctionSymbol, + announcements: SmallVec<[(MatchAnnouncement, T); 1]>, + destinations: SmallVec<[(ExplicitPosition, usize); 1]>, } #[derive(Debug)] -enum GoalsOrInitial { - InitialState, - Goals(Vec), +pub struct State { + label: ExplicitPosition, + match_goals: Vec, } impl SetAutomaton { @@ -248,6 +244,21 @@ impl SetAutomaton { self.transitions.len() } + /// Returns a reference to the given state. + pub fn states(&self) -> &Vec { + &self.states + } + + /// Returns an iterator over all the transitions in the automaton + pub fn transitions(&self) -> impl Iterator)> { + self.transitions.iter() + } + + /// Returns the transition with the given state and symbol (if it exists) + pub fn transition(&self, state: usize, symbol: usize) -> Option<&Transition> { + self.transitions.get(&(state, symbol)) + } + /// Provides a formatter for the .dot file format pub fn to_dot_graph(&self, show_backtransitions: bool, show_final: bool) -> DotFormatter { DotFormatter { @@ -258,6 +269,40 @@ impl SetAutomaton { } } +impl Transition { + pub fn symbol(&self) -> &DataFunctionSymbol { + &self.symbol + } + + pub fn announcements(&self) -> &SmallVec<[(MatchAnnouncement, T); 1]> { + &self.announcements + } + + pub fn destinations(&self) -> &SmallVec<[(ExplicitPosition, usize); 1]> { + &self.destinations + } +} + +impl MatchAnnouncement { + pub fn rule(&self) -> &Rule { + &self.rule + } + + pub fn position(&self) -> &ExplicitPosition { + &self.position + } + + pub fn symbols_seen(&self) -> usize { + self.symbols_seen + } +} + +#[derive(Debug)] +enum GoalsOrInitial { + InitialState, + Goals(Vec), +} + #[derive(Debug)] pub struct Derivative { pub(crate) completed: Vec, @@ -265,13 +310,23 @@ pub struct Derivative { pub(crate) reduced: Vec, } -#[derive(Debug)] -pub(crate) struct State { - pub(crate) label: ExplicitPosition, - pub(crate) match_goals: Vec, +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub(crate) struct MatchObligation { + pub pattern: DataExpression, + pub position: ExplicitPosition, } impl State { + /// Returns the label of the state. + pub fn label(&self) -> &ExplicitPosition { + &self.label + } + + /// Returns the match goals of the state. + pub(crate) fn match_goals(&self) -> &Vec { + &self.match_goals + } + /// Derive transitions from a state given a head symbol. The resulting transition is returned as a tuple /// The tuple consists of a vector of outputs and a set of destinations (which are sets of match goals). /// We don't use the struct Transition as it requires that the destination is a full state, with name. diff --git a/libraries/sabre/src/set_automaton/display.rs b/libraries/sabre/src/set_automaton/display.rs index ddf2d4ba..ac321a6b 100644 --- a/libraries/sabre/src/set_automaton/display.rs +++ b/libraries/sabre/src/set_automaton/display.rs @@ -20,9 +20,9 @@ impl fmt::Display for Transition { write!( f, "Transition {{ {}, announce: [{}], dest: [{}] }}", - self.symbol, - self.announcements.iter().map(|(x, _)| { x }).format(", "), - self.destinations.iter().format_with(", ", |element, f| { + self.symbol(), + self.announcements().iter().map(|(x, _)| { x }).format(", "), + self.destinations().iter().format_with(", ", |element, f| { f(&format_args!("{} -> {}", element.0, element.1)) }) ) @@ -32,7 +32,7 @@ impl fmt::Display for Transition { /// Implement display for a match announcement impl fmt::Display for MatchAnnouncement { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!(f, "({})@{}", self.rule, self.position) + write!(f, "({})@{}", self.rule(), self.position()) } } @@ -45,9 +45,9 @@ impl fmt::Display for MatchObligation { /// Implement display for a state with a term pool impl fmt::Display for State { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - writeln!(f, "Label: {}, ", self.label)?; + writeln!(f, "Label: {}, ", self.label())?; writeln!(f, "Match goals: [")?; - for m in &self.match_goals { + for m in self.match_goals() { writeln!(f, "\t {}", m)?; } write!(f, "]") @@ -58,11 +58,11 @@ impl fmt::Display for SetAutomaton { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { writeln!(f, "States: {{")?; - for (state_index, s) in self.states.iter().enumerate() { - writeln!(f, "State {} {{\n{}", state_index, s)?; + for (state_index, s) in self.states().iter().enumerate() { + writeln!(f, "State {} {{\n{:?}", state_index, s)?; writeln!(f, "Transitions: {{")?; - for ((from, _), tr) in self.transitions.iter() { + for ((from, _), tr) in self.transitions() { if state_index == *from { writeln!(f, "\t {}", tr)?; } @@ -89,8 +89,8 @@ impl<'a, M> fmt::Display for DotFormatter<'a, M> { writeln!(f, " final[label=\"💩\"];")?; } - for (i, s) in self.automaton.states.iter().enumerate() { - let match_goals = s.match_goals.iter().format_with("\\n", |goal, f| { + for (i, s) in self.automaton.states().iter().enumerate() { + let match_goals = s.match_goals().iter().format_with("\\n", |goal, f| { f(&format_args!( "{}", html_escape::encode_safe(&format!("{}", goal)) @@ -100,44 +100,44 @@ impl<'a, M> fmt::Display for DotFormatter<'a, M> { writeln!( f, " s{}[shape=record label=\"{{{{s{} | {}}} | {}}}\"]", - i, i, s.label, match_goals + i, i, s.label(), match_goals )?; } - for ((i, _), tr) in &self.automaton.transitions { + for ((i, _), tr) in self.automaton.transitions() { let announcements = - tr.announcements + tr.announcements() .iter() .format_with(", ", |(announcement, _), f| { f(&format_args!( "{}@{}", - announcement.rule.rhs, announcement.position + announcement.rule().rhs, announcement.position )) }); - if tr.destinations.is_empty() { + if tr.destinations().is_empty() { if self.show_final { writeln!( f, " s{} -> final [label=\"{} \\[{}\\]\"]", - i, tr.symbol, announcements + i, tr.symbol(), announcements )?; } } else { - writeln!(f, " \"s{}{}\" [shape=point]", i, tr.symbol,).unwrap(); + writeln!(f, " \"s{}{}\" [shape=point]", i, tr.symbol(),).unwrap(); writeln!( f, " s{} -> \"s{}{}\" [label=\"{} \\[{}\\]\"]", - i, i, tr.symbol, tr.symbol, announcements + i, i, tr.symbol(), tr.symbol(), announcements )?; - for (pos, des) in &tr.destinations { + for (pos, des) in tr.destinations() { if self.show_backtransitions || *des != 0 { // Hide backpointers to the initial state. writeln!( f, " \"s{}{}\" -> s{} [label = \"{}\"]", - i, tr.symbol, des, pos + i, tr.symbol(), des, pos )?; } } diff --git a/libraries/sabre/src/set_automaton/match_goal.rs b/libraries/sabre/src/set_automaton/match_goal.rs index ef034ebf..d1c8d7fb 100644 --- a/libraries/sabre/src/set_automaton/match_goal.rs +++ b/libraries/sabre/src/set_automaton/match_goal.rs @@ -28,17 +28,17 @@ impl MatchGoal { } // Initialise the prefix with the first match goal, can only shrink afterwards - let first_match_pos = &goals.first().unwrap().announcement.position; + let first_match_pos = goals.first().unwrap().announcement.position(); let mut gcp_length = first_match_pos.len(); - let prefix = &first_match_pos.clone(); + let prefix = first_match_pos.clone(); for g in goals { // Compare up to gcp_length or the length of the announcement position - let compare_length = min(gcp_length, g.announcement.position.len()); + let compare_length = min(gcp_length, g.announcement.position().len()); // gcp_length shrinks if they are not the same up to compare_length gcp_length = MatchGoal::common_prefix_length( &prefix.indices[0..compare_length], - &g.announcement.position.indices[0..compare_length], + &g.announcement.position().indices[0..compare_length], ); for mo in &g.obligations { @@ -63,7 +63,7 @@ impl MatchGoal { for goal in &mut goals { // update match announcement goal.announcement.position = ExplicitPosition { - indices: SmallVec::from_slice(&goal.announcement.position.indices[len..]), + indices: SmallVec::from_slice(&goal.announcement.position().indices[len..]), }; for mo_index in 0..goal.obligations.len() { let shortened = ExplicitPosition { diff --git a/libraries/sabre/src/utilities/configuration_stack.rs b/libraries/sabre/src/utilities/configuration_stack.rs index 3502ef3f..2afa76c5 100644 --- a/libraries/sabre/src/utilities/configuration_stack.rs +++ b/libraries/sabre/src/utilities/configuration_stack.rs @@ -235,7 +235,7 @@ impl<'a> ConfigurationStack<'a> { tp, write_terms[depth].deref(), new_subterm.into(), - &automaton.states[self.stack[depth].state].label.indices, + &automaton.states()[self.stack[depth].state].label().indices, ) .deref(), ); diff --git a/libraries/sabre/src/utilities/innermost_stack.rs b/libraries/sabre/src/utilities/innermost_stack.rs index 1d981e00..749b26d6 100644 --- a/libraries/sabre/src/utilities/innermost_stack.rs +++ b/libraries/sabre/src/utilities/innermost_stack.rs @@ -199,11 +199,15 @@ impl fmt::Display for Config { } } -/// A stack for the right-hand side. +/// A stack for the right-hand side, consisting of a small innermost stack and +/// the positions that must be added to stack, and are read from the left-hand +/// side term. pub struct RHSStack { - /// The innermost rewrite stack for the right hand side and the positions that must be added to the stack. + /// The innermost rewrite stack for the right hand side. innermost_stack: Protected>, +/// The variables of the left-hand side that must be placed at certain places in the stack. variables: Vec<(ExplicitPosition, usize)>, +/// The number of elements that must be reserved on the innermost stack. stack_size: usize, } diff --git a/tools/mcrl2rewrite/Cargo.toml b/tools/mcrl2rewrite/Cargo.toml index bf90c3b5..3f107f8b 100644 --- a/tools/mcrl2rewrite/Cargo.toml +++ b/tools/mcrl2rewrite/Cargo.toml @@ -15,6 +15,7 @@ env_logger.workspace = true log.workspace = true mcrl2.workspace = true rec-tests.workspace = true +sabre-compiling.workspace = true sabre.workspace = true [target.'cfg(not(target_env = "msvc"))'.dependencies] diff --git a/tools/mcrl2rewrite/src/lib.rs b/tools/mcrl2rewrite/src/lib.rs index 98305bbe..374cca22 100644 --- a/tools/mcrl2rewrite/src/lib.rs +++ b/tools/mcrl2rewrite/src/lib.rs @@ -21,12 +21,14 @@ use sabre::InnermostRewriter; use sabre::RewriteEngine; use sabre::RewriteSpecification; use sabre::SabreRewriter; +use sabre_compiling::SabreCompilingRewriter; #[derive(ValueEnum, Debug, Clone)] pub enum Rewriter { Jitty, Innermost, Sabre, + SabreCompiling, } /// Rewrites the given expressions with the given data specification and optionally prints the result. @@ -92,6 +94,23 @@ pub fn rewrite_data_spec( } println!("Sabre rewrite took {} ms", now.elapsed().as_millis()); } + Rewriter::SabreCompiling => { + let rewrite_spec = RewriteSpecification::from(data_spec.clone()); + let mut sabre_rewriter = + SabreCompilingRewriter::new(tp.clone(), &rewrite_spec, true, false).unwrap(); + + let now = Instant::now(); + for term in &terms { + let result = sabre_rewriter.rewrite(term.clone()); + if output { + println!("{}", result) + } + } + println!( + "Sabre compiling rewrite took {} ms", + now.elapsed().as_millis() + ); + } } Ok(()) @@ -137,6 +156,22 @@ pub fn rewrite_rec( } println!("Sabre rewrite took {} ms", now.elapsed().as_millis()); } + Rewriter::SabreCompiling => { + let mut sa = SabreCompilingRewriter::new(tp.clone(), &spec, true, false).unwrap(); + + let now = Instant::now(); + for term in &syntax_terms { + let term = to_untyped_data_expression(&mut tp.borrow_mut(), term, &AHashSet::new()); + let result = sa.rewrite(term); + if output { + println!("{}", result) + } + } + println!( + "Sabre compiling rewrite took {} ms", + now.elapsed().as_millis() + ); + } Rewriter::Jitty => { bail!("Cannot use REC specifications with mCRL2's jitty rewriter"); }