From a87fa5519a7b7d218cacfaacaf959b1ecbfe6466 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sun, 24 Mar 2024 21:50:17 +0100 Subject: [PATCH 01/25] Added an initial version of dynamically compiled and loaded library. --- Cargo.lock | 18 +++++ libraries/sabre-compiling/Cargo.toml | 15 ++++ libraries/sabre-compiling/src/lib.rs | 103 +++++++++++++++++++++++++++ 3 files changed, 136 insertions(+) create mode 100644 libraries/sabre-compiling/Cargo.toml create mode 100644 libraries/sabre-compiling/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index d117582c..1a97cb79 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" @@ -3967,6 +3973,18 @@ dependencies = [ "test-log", ] +[[package]] +name = "sabre-compiling" +version = "0.1.0" +dependencies = [ + "duct", + "indoc", + "libloading 0.8.3", + "log", + "mcrl2", + "sabre", +] + [[package]] name = "same-file" version = "1.0.6" diff --git a/libraries/sabre-compiling/Cargo.toml b/libraries/sabre-compiling/Cargo.toml new file mode 100644 index 00000000..d54a5071 --- /dev/null +++ b/libraries/sabre-compiling/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "sabre-compiling" +version.workspace = true +rust-version.workspace = true +edition.workspace = true + +[dependencies] +duct = "0.13" +indoc = "2.0" +libloading = "0.8" +log.workspace = true +mcrl2.workspace = true +sabre.workspace = true + +[dev-dependencies] diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs new file mode 100644 index 00000000..9bb59763 --- /dev/null +++ b/libraries/sabre-compiling/src/lib.rs @@ -0,0 +1,103 @@ +use std::{env::temp_dir, error::Error, ffi::c_void, fs::{self, File}, io::Write, path::{Path, PathBuf}}; + +use duct::cmd; +use indoc::indoc; +use libloading::{Library, Symbol}; +use log::info; +use mcrl2::data::DataExpression; +use sabre::{RewriteEngine, RewriteSpecification}; + +pub struct SabreCompiling { + library: Library, + //rewrite_func: Symbol u32>, +} + +impl RewriteEngine for SabreCompiling { + fn rewrite(&mut self, term: DataExpression) -> DataExpression { + term + } +} + +impl SabreCompiling { + + pub fn new(spec: &RewriteSpecification) -> Result> { + + // Create the directory structure for a Cargo project + let generated_dir = Path::new("temp"); + let source_dir = PathBuf::from(generated_dir).join("src"); + + if !generated_dir.exists() { + fs::create_dir(&generated_dir)?; + } + + if !source_dir.exists() { + fs::create_dir(&source_dir)?; + } + + // Write the cargo configuration + { + let mut file = File::create(PathBuf::from(generated_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] + + [lib] + crate-type = [\"cdylib\", \"rlib\"] + "})?; + } + + // Ignore the created package. + + + // Write the output source file. + { + let mut file = File::create(source_dir.join("lib.rs"))?; + writeln!(&mut file, indoc! {" + #[no_mangle] + pub unsafe extern \"C\" fn rewrite_term() {{ + println!(\"Hello world!\"); + }} + "})?; + } + + // Compile the dynamic object. + info!("Compiling..."); + cmd("cargo", &["build", "--lib"]) + .dir(generated_dir) + .run()?; + println!("ok."); + + // Load it back in and call the rewriter. + unsafe { + let library = Library::new(PathBuf::from(generated_dir).join("./target/debug/sabre_generated.dll"))?; + let func: Symbol = library.get(b"rewrite_term")?; + + func(); + + Ok(SabreCompiling { + library, + }) + } + + + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_compilation() { + let spec = RewriteSpecification::default(); + + SabreCompiling::new(&spec).unwrap(); + } +} \ No newline at end of file From 5f0c4172241c7f1b0e46dff8ab3e831a82366c95 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux <2884328+mlaveaux@users.noreply.github.com> Date: Sun, 17 Mar 2024 13:03:53 +0000 Subject: [PATCH 02/25] Deal with different shared library names on Linux. --- libraries/sabre-compiling/src/lib.rs | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index 9bb59763..8c49cfa7 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -1,4 +1,4 @@ -use std::{env::temp_dir, error::Error, ffi::c_void, fs::{self, File}, io::Write, path::{Path, PathBuf}}; +use std::{error::Error, fs::{self, File}, io::Write, path::{Path, PathBuf}}; use duct::cmd; use indoc::indoc; @@ -74,9 +74,18 @@ impl SabreCompiling { .run()?; println!("ok."); + // Figure out the path to the library (it is based on platform) + let mut path = PathBuf::from(generated_dir).join("./target/debug/libsabre_generated.so"); + if !path.exists() { + path = PathBuf::from(generated_dir).join("./target/debug/sabre_generated.lib"); + if !path.exists() { + return Err("Could not find the compiled library!".into()); + } + } + // Load it back in and call the rewriter. unsafe { - let library = Library::new(PathBuf::from(generated_dir).join("./target/debug/sabre_generated.dll"))?; + let library = Library::new(&path)?; let func: Symbol = library.get(b"rewrite_term")?; func(); From 6d8607ea48515487962bec5ede43761393717481 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sun, 17 Mar 2024 16:58:57 +0100 Subject: [PATCH 03/25] Made the compiling rewriter use a temp directory. --- Cargo.lock | 9 +++++++++ libraries/sabre-compiling/Cargo.toml | 3 +++ libraries/sabre-compiling/src/lib.rs | 25 +++++++++++++++++-------- 3 files changed, 29 insertions(+), 8 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 1a97cb79..3bd0bfdb 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -3978,11 +3978,14 @@ name = "sabre-compiling" version = "0.1.0" dependencies = [ "duct", + "env_logger", "indoc", "libloading 0.8.3", "log", "mcrl2", "sabre", + "temp-dir", + "test-log", ] [[package]] @@ -4507,6 +4510,12 @@ dependencies = [ "xattr", ] +[[package]] +name = "temp-dir" +version = "0.1.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dd16aa9ffe15fe021c6ee3766772132c6e98dfa395a167e16864f61a9cfb71d6" + [[package]] name = "tempfile" version = "3.10.1" diff --git a/libraries/sabre-compiling/Cargo.toml b/libraries/sabre-compiling/Cargo.toml index d54a5071..aaf6da38 100644 --- a/libraries/sabre-compiling/Cargo.toml +++ b/libraries/sabre-compiling/Cargo.toml @@ -8,8 +8,11 @@ edition.workspace = true duct = "0.13" indoc = "2.0" libloading = "0.8" +temp-dir = "0.1" +env_logger.workspace = true log.workspace = true mcrl2.workspace = true sabre.workspace = true [dev-dependencies] +test-log.workspace = true \ No newline at end of file diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index 8c49cfa7..18599e91 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -1,11 +1,12 @@ -use std::{error::Error, fs::{self, File}, io::Write, path::{Path, PathBuf}}; +use std::{error::Error, fs::{self, File}, io::Write, path::PathBuf}; use duct::cmd; use indoc::indoc; use libloading::{Library, Symbol}; use log::info; use mcrl2::data::DataExpression; -use sabre::{RewriteEngine, RewriteSpecification}; +use sabre::{set_automaton::SetAutomaton, RewriteEngine, RewriteSpecification}; +use temp_dir::TempDir; pub struct SabreCompiling { library: Library, @@ -21,13 +22,17 @@ impl RewriteEngine for SabreCompiling { impl SabreCompiling { pub fn new(spec: &RewriteSpecification) -> Result> { + let apma = SetAutomaton::new(spec, |_| (), true); // Create the directory structure for a Cargo project - let generated_dir = Path::new("temp"); - let source_dir = PathBuf::from(generated_dir).join("src"); + let temp_directory = TempDir::new().unwrap(); + let temp_dir = temp_directory.path(); - if !generated_dir.exists() { - fs::create_dir(&generated_dir)?; + info!("Compiling sabre into directory {}", temp_dir.to_string_lossy()); + let source_dir = PathBuf::from(temp_dir).join("src"); + + if !temp_dir.exists() { + fs::create_dir(&temp_dir)?; } if !source_dir.exists() { @@ -36,7 +41,7 @@ impl SabreCompiling { // Write the cargo configuration { - let mut file = File::create(PathBuf::from(generated_dir).join("Cargo.toml"))?; + let mut file = File::create(PathBuf::from(temp_dir).join("Cargo.toml"))?; writeln!(&mut file, indoc! {" [package] name = \"sabre-generated\" @@ -70,7 +75,7 @@ impl SabreCompiling { // Compile the dynamic object. info!("Compiling..."); cmd("cargo", &["build", "--lib"]) - .dir(generated_dir) + .dir(temp_dir) .run()?; println!("ok."); @@ -103,8 +108,12 @@ impl SabreCompiling { mod tests { use super::*; + use test_log::test; + #[test] fn test_compilation() { + env_logger::init(); + let spec = RewriteSpecification::default(); SabreCompiling::new(&spec).unwrap(); From dd49691ddfaeed059e1854c4eaff814a673acb43 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sun, 17 Mar 2024 17:13:08 +0100 Subject: [PATCH 04/25] Use a system provided temporary file, and added a .gitignore to the local one. --- libraries/sabre-compiling/src/lib.rs | 34 +++++++++++++++++----------- 1 file changed, 21 insertions(+), 13 deletions(-) diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index 18599e91..56812bbe 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -1,4 +1,4 @@ -use std::{error::Error, fs::{self, File}, io::Write, path::PathBuf}; +use std::{error::Error, fs::{self, File}, io::Write, path::{Path, PathBuf}}; use duct::cmd; use indoc::indoc; @@ -21,12 +21,16 @@ impl RewriteEngine for SabreCompiling { impl SabreCompiling { - pub fn new(spec: &RewriteSpecification) -> Result> { + pub fn new(spec: &RewriteSpecification, use_local_tmp: bool) -> Result> { let apma = SetAutomaton::new(spec, |_| (), true); // Create the directory structure for a Cargo project - let temp_directory = TempDir::new().unwrap(); - let temp_dir = temp_directory.path(); + let system_tmp_dir = TempDir::new()?; + let temp_dir = if use_local_tmp { + &Path::new("./tmp") + } else { + system_tmp_dir.path() + }; info!("Compiling sabre into directory {}", temp_dir.to_string_lossy()); let source_dir = PathBuf::from(temp_dir).join("src"); @@ -59,9 +63,12 @@ impl SabreCompiling { } // Ignore the created package. + { + let mut file = File::create(PathBuf::from(temp_dir).join(".gitignore"))?; + writeln!(&mut file, "*.*")?; + } - - // Write the output source file. + // Write the output source file(s). { let mut file = File::create(source_dir.join("lib.rs"))?; writeln!(&mut file, indoc! {" @@ -79,12 +86,15 @@ impl SabreCompiling { .run()?; println!("ok."); - // Figure out the path to the library (it is based on platform) - let mut path = PathBuf::from(generated_dir).join("./target/debug/libsabre_generated.so"); + // Figure out the path to the library (it is based on platform: linux, windows and then macos) + let mut path = PathBuf::from(temp_dir).join("./target/debug/libsabre_generated.so"); if !path.exists() { - path = PathBuf::from(generated_dir).join("./target/debug/sabre_generated.lib"); + path = PathBuf::from(temp_dir).join("./target/debug/sabre_generated.dll"); if !path.exists() { - return Err("Could not find the compiled library!".into()); + path = PathBuf::from(temp_dir).join("./target/debug/libsabre_generated.dylib"); + if !path.exists() { + return Err("Could not find the compiled library!".into()); + } } } @@ -112,10 +122,8 @@ mod tests { #[test] fn test_compilation() { - env_logger::init(); - let spec = RewriteSpecification::default(); - SabreCompiling::new(&spec).unwrap(); + SabreCompiling::new(&spec, true).unwrap(); } } \ No newline at end of file From 8bccf3aa337a30311d3b1a95c988d8aa5f4cf44f Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 27 Mar 2024 15:24:26 +0100 Subject: [PATCH 05/25] Generate a Compilation.toml to store the environment variables. --- .gitignore | 7 ++----- Cargo.lock | 1 + libraries/sabre-compiling/Cargo.toml | 1 + libraries/sabre-compiling/build.rs | 26 ++++++++++++++++++++++++ libraries/sabre-compiling/src/lib.rs | 30 +++++++++++++++++++++++----- 5 files changed, 55 insertions(+), 10 deletions(-) create mode 100644 libraries/sabre-compiling/build.rs diff --git a/.gitignore b/.gitignore index 1933a508..dc27c368 100644 --- a/.gitignore +++ b/.gitignore @@ -2,11 +2,8 @@ # will have compiled files and executables /target/ -# Folder generated by WASM. -**/*/dist/ - -# will have the code coverage report -/coverage/ +# A generated file used by the compiling rewriter. +Compilation.toml # These are backup files generated by rustfmt **/*.rs.bk diff --git a/Cargo.lock b/Cargo.lock index 3bd0bfdb..0afd20f0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -3986,6 +3986,7 @@ dependencies = [ "sabre", "temp-dir", "test-log", + "toml", ] [[package]] diff --git a/libraries/sabre-compiling/Cargo.toml b/libraries/sabre-compiling/Cargo.toml index aaf6da38..f3dd45dc 100644 --- a/libraries/sabre-compiling/Cargo.toml +++ b/libraries/sabre-compiling/Cargo.toml @@ -9,6 +9,7 @@ duct = "0.13" indoc = "2.0" libloading = "0.8" temp-dir = "0.1" +toml = "0.8" env_logger.workspace = true log.workspace = true mcrl2.workspace = true diff --git a/libraries/sabre-compiling/build.rs b/libraries/sabre-compiling/build.rs new file mode 100644 index 00000000..81d3afb1 --- /dev/null +++ b/libraries/sabre-compiling/build.rs @@ -0,0 +1,26 @@ +use std::{env, error::Error, 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> { + // Write compiler related environment variables to a configuration file. + + for (from, to) in env::vars() { + println!("{} to {}", from, to); + } + + let mut file = File::create("./Compilation.toml")?; + writeln!(file, "[env]")?; + write_env(&mut file, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"])?; + + Ok(()) +} \ No newline at end of file diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index 56812bbe..a9496670 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -1,12 +1,13 @@ use std::{error::Error, fs::{self, File}, io::Write, path::{Path, PathBuf}}; -use duct::cmd; +use duct::{cmd, Expression}; use indoc::indoc; use libloading::{Library, Symbol}; use log::info; use mcrl2::data::DataExpression; use sabre::{set_automaton::SetAutomaton, RewriteEngine, RewriteSpecification}; use temp_dir::TempDir; +use toml::{map::Map, Table, Value}; pub struct SabreCompiling { library: Library, @@ -19,11 +20,28 @@ impl RewriteEngine for SabreCompiling { } } +/// 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]) -> Expression +{ + let mut result = builder; + + for var in variables { + let value = compilation_toml.get(*var).unwrap().to_string(); + + info!("Variable {} = {}", var, value); + result = result.env(var, value); + } + + result +} + impl SabreCompiling { pub fn new(spec: &RewriteSpecification, use_local_tmp: bool) -> Result> { let apma = SetAutomaton::new(spec, |_| (), true); + let compilation_toml = fs::read_to_string("./Compilation.toml")?.parse::().unwrap(); + // Create the directory structure for a Cargo project let system_tmp_dir = TempDir::new()?; let temp_dir = if use_local_tmp { @@ -81,10 +99,12 @@ impl SabreCompiling { // Compile the dynamic object. info!("Compiling..."); - cmd("cargo", &["build", "--lib"]) - .dir(temp_dir) - .run()?; - println!("ok."); + let mut expr = cmd("cargo", &["build", "--lib"]) + .dir(temp_dir); + expr = apply_env(expr, &compilation_toml, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"]); + expr.run()?; + + println!("finished."); // Figure out the path to the library (it is based on platform: linux, windows and then macos) let mut path = PathBuf::from(temp_dir).join("./target/debug/libsabre_generated.so"); From 8682559ddb44ba9b5060d76438c833e7a1c31cb4 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 27 Mar 2024 18:48:52 +0100 Subject: [PATCH 06/25] Fixed setting the environment from the Compilation.toml. --- libraries/sabre-compiling/src/lib.rs | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index a9496670..9bba5dde 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -21,18 +21,19 @@ impl RewriteEngine for SabreCompiling { } /// 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]) -> Expression +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 = compilation_toml.get(*var).unwrap().to_string(); + let value = env.get(*var).ok_or("Missing var")?.as_str().ok_or("Not a string")?; - info!("Variable {} = {}", var, value); + info!("Setting environment variable {} = {}", var, value); result = result.env(var, value); } - result + Ok(result) } impl SabreCompiling { @@ -40,7 +41,7 @@ impl SabreCompiling { pub fn new(spec: &RewriteSpecification, use_local_tmp: bool) -> Result> { let apma = SetAutomaton::new(spec, |_| (), true); - let compilation_toml = fs::read_to_string("./Compilation.toml")?.parse::
().unwrap(); + let compilation_toml = include_str!("../Compilation.toml").parse::
()?; // Create the directory structure for a Cargo project let system_tmp_dir = TempDir::new()?; @@ -101,7 +102,7 @@ impl SabreCompiling { info!("Compiling..."); let mut expr = cmd("cargo", &["build", "--lib"]) .dir(temp_dir); - expr = apply_env(expr, &compilation_toml, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"]); + expr = apply_env(expr, &compilation_toml, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"])?; expr.run()?; println!("finished."); From 6142500265a71d952e4cdc303dc61cb3b01c7a64 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 29 Mar 2024 17:47:34 +0100 Subject: [PATCH 07/25] Split the implementation into several modules for readability. --- libraries/sabre-compiling/src/lib.rs | 155 +----------------- libraries/sabre-compiling/src/library.rs | 124 ++++++++++++++ .../sabre-compiling/src/sabre_compiling.rs | 112 +++++++++++++ 3 files changed, 243 insertions(+), 148 deletions(-) create mode 100644 libraries/sabre-compiling/src/library.rs create mode 100644 libraries/sabre-compiling/src/sabre_compiling.rs diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index 9bba5dde..dfe0131a 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -1,150 +1,9 @@ -use std::{error::Error, fs::{self, File}, io::Write, path::{Path, PathBuf}}; +//! +//! +//! +//! -use duct::{cmd, Expression}; -use indoc::indoc; -use libloading::{Library, Symbol}; -use log::info; -use mcrl2::data::DataExpression; -use sabre::{set_automaton::SetAutomaton, RewriteEngine, RewriteSpecification}; -use temp_dir::TempDir; -use toml::{map::Map, Table, Value}; +mod library; +mod sabre_compiling; -pub struct SabreCompiling { - library: Library, - //rewrite_func: Symbol u32>, -} - -impl RewriteEngine for SabreCompiling { - fn rewrite(&mut self, term: DataExpression) -> DataExpression { - term - } -} - -/// 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) -} - -impl SabreCompiling { - - pub fn new(spec: &RewriteSpecification, use_local_tmp: bool) -> Result> { - let apma = SetAutomaton::new(spec, |_| (), true); - - let compilation_toml = include_str!("../Compilation.toml").parse::
()?; - - // Create the directory structure for a Cargo project - let system_tmp_dir = TempDir::new()?; - let temp_dir = if use_local_tmp { - &Path::new("./tmp") - } else { - system_tmp_dir.path() - }; - - info!("Compiling sabre into directory {}", temp_dir.to_string_lossy()); - let source_dir = PathBuf::from(temp_dir).join("src"); - - 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] - - [lib] - crate-type = [\"cdylib\", \"rlib\"] - "})?; - } - - // Ignore the created package. - { - let mut file = File::create(PathBuf::from(temp_dir).join(".gitignore"))?; - writeln!(&mut file, "*.*")?; - } - - // Write the output source file(s). - { - let mut file = File::create(source_dir.join("lib.rs"))?; - writeln!(&mut file, indoc! {" - #[no_mangle] - pub unsafe extern \"C\" fn rewrite_term() {{ - println!(\"Hello world!\"); - }} - "})?; - } - - // Compile the dynamic object. - info!("Compiling..."); - let mut expr = cmd("cargo", &["build", "--lib"]) - .dir(temp_dir); - expr = apply_env(expr, &compilation_toml, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"])?; - expr.run()?; - - println!("finished."); - - // Figure out the path to the library (it is based on platform: linux, windows and then macos) - let mut path = PathBuf::from(temp_dir).join("./target/debug/libsabre_generated.so"); - if !path.exists() { - path = PathBuf::from(temp_dir).join("./target/debug/sabre_generated.dll"); - if !path.exists() { - path = PathBuf::from(temp_dir).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 { - let library = Library::new(&path)?; - let func: Symbol = library.get(b"rewrite_term")?; - - func(); - - Ok(SabreCompiling { - library, - }) - } - - - } -} - -#[cfg(test)] -mod tests { - use super::*; - - use test_log::test; - - #[test] - fn test_compilation() { - let spec = RewriteSpecification::default(); - - SabreCompiling::new(&spec, true).unwrap(); - } -} \ No newline at end of file +pub use sabre_compiling::*; \ No newline at end of file diff --git a/libraries/sabre-compiling/src/library.rs b/libraries/sabre-compiling/src/library.rs new file mode 100644 index 00000000..2fabc201 --- /dev/null +++ b/libraries/sabre-compiling/src/library.rs @@ -0,0 +1,124 @@ +use std::{error::Error, fs::{self, File}, io::Write, path::{Path, PathBuf}}; + +use toml::{map::Map, Table, Value}; +use libloading::Library; + +use duct::{cmd, 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!("../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()?; + + println!("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)?) + } + } +} \ No newline at end of file diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs new file mode 100644 index 00000000..631b92e4 --- /dev/null +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -0,0 +1,112 @@ +use std::{ + cell::RefCell, error::Error, fs::File, io::Write, path::{Path, PathBuf}, rc::Rc +}; + +use indoc::indoc; +use libloading::{Library, Symbol}; +use log::info; +use temp_dir::TempDir; +use toml::Table; + +use mcrl2::{aterm::TermPool, data::DataExpression}; +use sabre::{set_automaton::SetAutomaton, RewriteEngine, RewriteSpecification}; + +use crate::library::RuntimeLibrary; + +pub struct SabreCompilingRewriter { + library: Library, + //rewrite_func: Symbol u32>, +} + +impl RewriteEngine for SabreCompilingRewriter { + fn rewrite(&mut self, term: DataExpression) -> DataExpression { + 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. + pub fn new( + tp: Rc>, + spec: &RewriteSpecification, + use_local_workspace: bool, + use_local_tmp: bool, + ) -> Result> { + let apma = SetAutomaton::new(spec, |_| (), true); + + 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!("../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!( + "sabre-ffi = {{ path = \"{}\" }}", PathBuf::from(path).join("sabre-ffi").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). + { + let mut file = + File::create(PathBuf::from(compilation_crate.source_dir()).join("lib.rs"))?; + writeln!( + &mut file, + indoc! {" + #[no_mangle] + pub unsafe extern \"C\" fn rewrite_term() {{ + println!(\"Hello world!\"); + }} + "} + )?; + } + + let library = compilation_crate.compile()?; + + unsafe { + let func: Symbol = library.get(b"rewrite_term")?; + + func(); + } + + Ok(SabreCompilingRewriter { library }) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + use test_log::test; + + #[test] + fn test_compilation() { + let spec = RewriteSpecification::default(); + let tp = Rc::new(RefCell::new(TermPool::new())); + + SabreCompilingRewriter::new(tp, &spec, true, false).unwrap(); + } +} From 65620b60431497a09f9cbaf9976dbe6d63130906 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 29 Mar 2024 17:47:50 +0100 Subject: [PATCH 08/25] Added a sabre-ffi to contain the FFI related functionality. --- libraries/sabre-compiling/Cargo.toml | 1 + libraries/sabre-compiling/build.rs | 9 +++++++-- libraries/sabre-compiling/sabre-ffi/Cargo.toml | 11 +++++++++++ libraries/sabre-compiling/sabre-ffi/src/atermpp.rs | 6 ++++++ libraries/sabre-compiling/sabre-ffi/src/lib.rs | 6 ++++++ 5 files changed, 31 insertions(+), 2 deletions(-) create mode 100644 libraries/sabre-compiling/sabre-ffi/Cargo.toml create mode 100644 libraries/sabre-compiling/sabre-ffi/src/atermpp.rs create mode 100644 libraries/sabre-compiling/sabre-ffi/src/lib.rs diff --git a/libraries/sabre-compiling/Cargo.toml b/libraries/sabre-compiling/Cargo.toml index f3dd45dc..a4ebc096 100644 --- a/libraries/sabre-compiling/Cargo.toml +++ b/libraries/sabre-compiling/Cargo.toml @@ -10,6 +10,7 @@ indoc = "2.0" libloading = "0.8" temp-dir = "0.1" toml = "0.8" +sabre-ffi = { path = "./sabre-ffi" } env_logger.workspace = true log.workspace = true mcrl2.workspace = true diff --git a/libraries/sabre-compiling/build.rs b/libraries/sabre-compiling/build.rs index 81d3afb1..9487e447 100644 --- a/libraries/sabre-compiling/build.rs +++ b/libraries/sabre-compiling/build.rs @@ -1,3 +1,4 @@ +use std::fs; use std::{env, error::Error, fs::File}; use std::io::Write; @@ -12,13 +13,17 @@ fn write_env(writer: &mut impl Write, variables: &[&'static str]) -> Result<(), } fn main() -> Result<(), Box> { - // Write compiler related environment variables to a configuration file. - for (from, to) in env::vars() { println!("{} to {}", from, to); } let mut file = File::create("./Compilation.toml")?; + // Write the developement location. + writeln!(file, "[sabrec]")?; + writeln!(file, "path = \"{}\"", fs::canonicalize(".")?.to_string_lossy())?; + + // Write compilation related environment variables to the configuration file. + writeln!(file)?; writeln!(file, "[env]")?; write_env(&mut file, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"])?; diff --git a/libraries/sabre-compiling/sabre-ffi/Cargo.toml b/libraries/sabre-compiling/sabre-ffi/Cargo.toml new file mode 100644 index 00000000..7deba5f4 --- /dev/null +++ b/libraries/sabre-compiling/sabre-ffi/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "sabre-ffi" +version.workspace = true +rust-version.workspace = true +edition.workspace = true + +[dependencies] +stabby = "4.0" + +[dev-dependencies] +test-log.workspace = true \ No newline at end of file diff --git a/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs b/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs new file mode 100644 index 00000000..d7bcedce --- /dev/null +++ b/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs @@ -0,0 +1,6 @@ +use stabby::stabby; + +#[stabby] +struct ATermFFI { + +} \ No newline at end of file diff --git a/libraries/sabre-compiling/sabre-ffi/src/lib.rs b/libraries/sabre-compiling/sabre-ffi/src/lib.rs new file mode 100644 index 00000000..7637bdef --- /dev/null +++ b/libraries/sabre-compiling/sabre-ffi/src/lib.rs @@ -0,0 +1,6 @@ +//! +//! This crate provides a Rust to Rust stable ABI to allow the compiling rewriter to be compiled +//! with a different version of rustc. +//! + +mod atermpp; \ No newline at end of file From 2f5a6b6883a7db61e7a4c5157b6a8d3dced41536 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 29 Mar 2024 17:48:18 +0100 Subject: [PATCH 09/25] Added the compiling rewriter as option to mcrl2rewrite. --- Cargo.lock | 52 +++++++++++++++++++++++++++++++++++ Cargo.toml | 2 ++ tools/mcrl2rewrite/Cargo.toml | 1 + tools/mcrl2rewrite/src/lib.rs | 30 +++++++++++++++++++- 4 files changed, 84 insertions(+), 1 deletion(-) diff --git a/Cargo.lock b/Cargo.lock index 0afd20f0..660d288d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2964,6 +2964,7 @@ dependencies = [ "mcrl2", "rec-tests", "sabre", + "sabre-compiling", ] [[package]] @@ -3984,11 +3985,20 @@ dependencies = [ "log", "mcrl2", "sabre", + "sabre-ffi", "temp-dir", "test-log", "toml", ] +[[package]] +name = "sabre-ffi" +version = "0.1.0" +dependencies = [ + "stabby", + "test-log", +] + [[package]] name = "same-file" version = "1.0.6" @@ -4120,6 +4130,12 @@ dependencies = [ "digest", ] +[[package]] +name = "sha2-const-stable" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5f179d4e11094a893b82fff208f74d448a7512f99f5a0acbd5c679b705f83ed9" + [[package]] name = "sharded-slab" version = "0.1.7" @@ -4393,6 +4409,42 @@ dependencies = [ "pin-utils", ] +[[package]] +name = "stabby" +version = "4.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0d703a24a549fc06c1535ad416df7375e781a0613b6ef965218c698e52383edb" +dependencies = [ + "lazy_static", + "rustversion", + "stabby-abi", +] + +[[package]] +name = "stabby-abi" +version = "4.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "94ee77c602ee96c410efd3756dbab4c0f7ccf35a6a3d3dca5c55dcf5cc7ad175" +dependencies = [ + "libc", + "rustversion", + "sha2-const-stable", + "stabby-macros", +] + +[[package]] +name = "stabby-macros" +version = "4.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e3fdde04cf3de956591380cf08c0cba18fd225156c3a0a1092d6fde5d93103a0" +dependencies = [ + "proc-macro-crate 3.1.0", + "proc-macro2", + "quote", + "rand", + "syn 1.0.109", +] + [[package]] name = "stable_deref_trait" version = "1.2.0" diff --git a/Cargo.toml b/Cargo.toml index 4557ad70..b3004e18 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -8,6 +8,7 @@ debug = "line-tables-only" resolver = "2" members = [ "libraries/*", + "libraries/sabre-compiling/sabre-ffi", "libraries/**/benchmarks", "tools/*", "tools/**/benchmarks", @@ -77,4 +78,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/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..2e2de9d8 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. @@ -91,6 +93,19 @@ 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()); } } @@ -136,7 +151,20 @@ 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"); } From e1a68d527eb4068a362ca73eb4f408b46156f0e8 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 2 Apr 2024 16:07:13 +0200 Subject: [PATCH 10/25] Moved the generated Compilation.toml to the target directory. --- libraries/sabre-compiling/build.rs | 15 +++++++++++---- libraries/sabre-compiling/src/library.rs | 2 +- libraries/sabre-compiling/src/sabre_compiling.rs | 2 +- 3 files changed, 13 insertions(+), 6 deletions(-) diff --git a/libraries/sabre-compiling/build.rs b/libraries/sabre-compiling/build.rs index 9487e447..8fbfbb76 100644 --- a/libraries/sabre-compiling/build.rs +++ b/libraries/sabre-compiling/build.rs @@ -1,6 +1,8 @@ use std::fs; use std::{env, error::Error, fs::File}; +use toml::{map::Map, Table, Value}; + use std::io::Write; /// Write every environment variable in the variables array. @@ -17,13 +19,18 @@ fn main() -> Result<(), Box> { println!("{} to {}", from, to); } - let mut file = File::create("./Compilation.toml")?; + let mut file = File::create("../../target/Compilation.toml")?; + // Write the developement location. - writeln!(file, "[sabrec]")?; - writeln!(file, "path = \"{}\"", fs::canonicalize(".")?.to_string_lossy())?; + let mut table = Map::new(); + + let mut sabrec = Table::new(); + sabrec.insert("path".to_string(), Value::String(fs::canonicalize(".")?.to_string_lossy().to_string())); + table.insert("sabrec".to_string(), Value::Table(sabrec)); + + writeln!(file, "{}", table)?; // Write compilation related environment variables to the configuration file. - writeln!(file)?; writeln!(file, "[env]")?; write_env(&mut file, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"])?; diff --git a/libraries/sabre-compiling/src/library.rs b/libraries/sabre-compiling/src/library.rs index 2fabc201..d5d30e18 100644 --- a/libraries/sabre-compiling/src/library.rs +++ b/libraries/sabre-compiling/src/library.rs @@ -93,7 +93,7 @@ impl RuntimeLibrary { /// Compiles the library into pub fn compile(&mut self) -> Result> { - let compilation_toml = include_str!("../Compilation.toml").parse::
()?; + let compilation_toml = include_str!("../../../target/Compilation.toml").parse::
()?; // Compile the dynamic object. info!("Compiling..."); diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index 631b92e4..d0bb0e50 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -47,7 +47,7 @@ impl SabreCompilingRewriter { let mut dependencies = vec![]; if use_local_workspace { - let compilation_toml = include_str!("../Compilation.toml").parse::
()?; + let compilation_toml = include_str!("../../../target/Compilation.toml").parse::
()?; let path = compilation_toml .get("sabrec") .ok_or("Missing [sabre] section)")? From 60097fea2b47f644e6b8e4e44b9fa1e77308dfc8 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 2 Apr 2024 18:20:59 +0200 Subject: [PATCH 11/25] Made it possible to send ATerm objects over FFI. --- .gitignore | 3 -- Cargo.lock | 1 + libraries/mcrl2/src/aterm/term.rs | 2 ++ libraries/sabre-compiling/Cargo.toml | 5 +++- libraries/sabre-compiling/examples/rewrite.rs | 10 +++++++ .../sabre-compiling/sabre-ffi/Cargo.toml | 1 + .../sabre-compiling/sabre-ffi/src/atermpp.rs | 7 +---- .../sabre-compiling/sabre-ffi/src/lib.rs | 4 ++- libraries/sabre-compiling/src/lib.rs | 4 +-- .../sabre-compiling/src/sabre_compiling.rs | 29 +++++++++++-------- 10 files changed, 41 insertions(+), 25 deletions(-) create mode 100644 libraries/sabre-compiling/examples/rewrite.rs diff --git a/.gitignore b/.gitignore index dc27c368..475cc393 100644 --- a/.gitignore +++ b/.gitignore @@ -2,9 +2,6 @@ # will have compiled files and executables /target/ -# A generated file used by the compiling rewriter. -Compilation.toml - # These are backup files generated by rustfmt **/*.rs.bk diff --git a/Cargo.lock b/Cargo.lock index 660d288d..e831bbf5 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -3995,6 +3995,7 @@ dependencies = [ name = "sabre-ffi" version = "0.1.0" dependencies = [ + "mcrl2", "stabby", "test-log", ] diff --git a/libraries/mcrl2/src/aterm/term.rs b/libraries/mcrl2/src/aterm/term.rs index 9097db44..67cf6880 100644 --- a/libraries/mcrl2/src/aterm/term.rs +++ b/libraries/mcrl2/src/aterm/term.rs @@ -26,6 +26,7 @@ use super::global_aterm_pool::GLOBAL_TERM_POOL; /// to acquire the 'static lifetime. This occasionally gives rise to issues /// 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. +#[repr(transparent)] #[derive(Hash, PartialEq, Eq, PartialOrd, Ord)] pub struct ATermRef<'a> { term: *const ffi::_aterm, @@ -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/sabre-compiling/Cargo.toml b/libraries/sabre-compiling/Cargo.toml index a4ebc096..30020841 100644 --- a/libraries/sabre-compiling/Cargo.toml +++ b/libraries/sabre-compiling/Cargo.toml @@ -17,4 +17,7 @@ mcrl2.workspace = true sabre.workspace = true [dev-dependencies] -test-log.workspace = true \ No newline at end of file +test-log.workspace = true + +[build-dependencies] +toml = "0.8" \ No newline at end of file diff --git a/libraries/sabre-compiling/examples/rewrite.rs b/libraries/sabre-compiling/examples/rewrite.rs new file mode 100644 index 00000000..d5727d01 --- /dev/null +++ b/libraries/sabre-compiling/examples/rewrite.rs @@ -0,0 +1,10 @@ +use sabre_ffi::ATerm; + +#[no_mangle] +pub unsafe extern "C" fn rewrite_term(term: ATerm) -> ATerm { + term +} + +fn main() { + +} \ No newline at end of file diff --git a/libraries/sabre-compiling/sabre-ffi/Cargo.toml b/libraries/sabre-compiling/sabre-ffi/Cargo.toml index 7deba5f4..367bb6f3 100644 --- a/libraries/sabre-compiling/sabre-ffi/Cargo.toml +++ b/libraries/sabre-compiling/sabre-ffi/Cargo.toml @@ -6,6 +6,7 @@ edition.workspace = true [dependencies] stabby = "4.0" +mcrl2.workspace = true [dev-dependencies] test-log.workspace = true \ No newline at end of file diff --git a/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs b/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs index d7bcedce..16a8156c 100644 --- a/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs +++ b/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs @@ -1,6 +1 @@ -use stabby::stabby; - -#[stabby] -struct ATermFFI { - -} \ No newline at end of file +pub use mcrl2::aterm::ATerm; \ No newline at end of file diff --git a/libraries/sabre-compiling/sabre-ffi/src/lib.rs b/libraries/sabre-compiling/sabre-ffi/src/lib.rs index 7637bdef..e21f4309 100644 --- a/libraries/sabre-compiling/sabre-ffi/src/lib.rs +++ b/libraries/sabre-compiling/sabre-ffi/src/lib.rs @@ -3,4 +3,6 @@ //! with a different version of rustc. //! -mod atermpp; \ No newline at end of file +mod atermpp; + +pub use atermpp::*; \ No newline at end of file diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index dfe0131a..89ddbd2f 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -1,6 +1,6 @@ //! -//! -//! +//! This module contains an implementation for a compiling variant of the Sabre +//! rewrite engine. //! mod library; diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index d0bb0e50..2e887fbb 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -20,7 +20,14 @@ pub struct SabreCompilingRewriter { impl RewriteEngine for SabreCompilingRewriter { fn rewrite(&mut self, term: DataExpression) -> DataExpression { - term + // TODO: This ought to be stored somewhere for repeated calls. + unsafe { + let func: Symbol = self.library.get(b"rewrite_term").unwrap(); + + func(); + + term + } } } @@ -35,7 +42,6 @@ impl SabreCompilingRewriter { use_local_workspace: bool, use_local_tmp: bool, ) -> Result> { - let apma = SetAutomaton::new(spec, |_| (), true); let system_tmp_dir = TempDir::new()?; let temp_dir = if use_local_tmp { @@ -69,29 +75,28 @@ impl SabreCompilingRewriter { let mut compilation_crate = RuntimeLibrary::new(temp_dir, dependencies)?; + // Generate the automata used for matching + let apma = SetAutomaton::new(spec, |_| (), true); + // Write the output source file(s). { let mut file = File::create(PathBuf::from(compilation_crate.source_dir()).join("lib.rs"))?; + writeln!( &mut file, indoc! {" + use sabre_ffi::ATerm; + #[no_mangle] - pub unsafe extern \"C\" fn rewrite_term() {{ - println!(\"Hello world!\"); + pub unsafe extern \"C\" fn rewrite_term(term: ATerm) -> ATerm {{ + term }} "} )?; } let library = compilation_crate.compile()?; - - unsafe { - let func: Symbol = library.get(b"rewrite_term")?; - - func(); - } - Ok(SabreCompilingRewriter { library }) } } @@ -107,6 +112,6 @@ mod tests { let spec = RewriteSpecification::default(); let tp = Rc::new(RefCell::new(TermPool::new())); - SabreCompilingRewriter::new(tp, &spec, true, false).unwrap(); + SabreCompilingRewriter::new(tp, &spec, true, true).unwrap(); } } From ef139d1889f3c4681828d9edd4e428b87ce28781 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 3 Apr 2024 00:23:13 +0200 Subject: [PATCH 12/25] Enabled debug log level for all tests. --- .github/workflows/nightly.yml | 1 + .github/workflows/test.yml | 1 + .github/workflows/test_address_sanitizer.yml | 1 + .github/workflows/test_thread_sanitizer.yml | 1 + 4 files changed, 4 insertions(+) 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 From 93536b9dcca4e0c9fd8cdd581cef8281938276fc Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 3 Apr 2024 00:23:25 +0200 Subject: [PATCH 13/25] Escape the path inside the toml file that is generated. --- libraries/sabre-compiling/build.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libraries/sabre-compiling/build.rs b/libraries/sabre-compiling/build.rs index 8fbfbb76..e16c65e9 100644 --- a/libraries/sabre-compiling/build.rs +++ b/libraries/sabre-compiling/build.rs @@ -25,7 +25,7 @@ fn main() -> Result<(), Box> { let mut table = Map::new(); let mut sabrec = Table::new(); - sabrec.insert("path".to_string(), Value::String(fs::canonicalize(".")?.to_string_lossy().to_string())); + sabrec.insert("path".to_string(), Value::String(fs::canonicalize(".")?.to_string_lossy().escape_default().to_string())); table.insert("sabrec".to_string(), Value::Table(sabrec)); writeln!(file, "{}", table)?; From 58ce54ab2ac53f6086c6f3598829b16b1fc34efd Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 3 Apr 2024 20:38:08 +0200 Subject: [PATCH 14/25] Replaced this by a logging statement. --- libraries/sabre-compiling/src/library.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/libraries/sabre-compiling/src/library.rs b/libraries/sabre-compiling/src/library.rs index d5d30e18..168a11bd 100644 --- a/libraries/sabre-compiling/src/library.rs +++ b/libraries/sabre-compiling/src/library.rs @@ -48,6 +48,8 @@ impl RuntimeLibrary { fs::create_dir(&source_dir)?; } + + // Write the cargo configuration { let mut file = File::create(PathBuf::from(temp_dir).join("Cargo.toml"))?; @@ -102,7 +104,7 @@ impl RuntimeLibrary { expr = apply_env(expr, &compilation_toml, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"])?; expr.run()?; - println!("finished."); + 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"); From 7a4ea2fb9f8acf26e094a7cdb24cbc7aa6239c89 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 8 Apr 2024 15:25:40 +0200 Subject: [PATCH 15/25] Use raw strings in the toml file to allow for Windows paths. --- libraries/sabre-compiling/build.rs | 13 +-- libraries/sabre-compiling/src/library.rs | 86 +++++++++++++------ .../sabre-compiling/src/sabre_compiling.rs | 4 +- 3 files changed, 64 insertions(+), 39 deletions(-) diff --git a/libraries/sabre-compiling/build.rs b/libraries/sabre-compiling/build.rs index e16c65e9..55f8cf50 100644 --- a/libraries/sabre-compiling/build.rs +++ b/libraries/sabre-compiling/build.rs @@ -8,7 +8,7 @@ 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())?; + writeln!(writer, "{} = '{}'", var, env::var(var).unwrap_or_default())?; } Ok(()) @@ -21,14 +21,9 @@ fn main() -> Result<(), Box> { let mut file = File::create("../../target/Compilation.toml")?; - // Write the developement location. - let mut table = Map::new(); - - let mut sabrec = Table::new(); - sabrec.insert("path".to_string(), Value::String(fs::canonicalize(".")?.to_string_lossy().escape_default().to_string())); - table.insert("sabrec".to_string(), Value::Table(sabrec)); - - writeln!(file, "{}", table)?; + // 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]")?; diff --git a/libraries/sabre-compiling/src/library.rs b/libraries/sabre-compiling/src/library.rs index 168a11bd..1d97544a 100644 --- a/libraries/sabre-compiling/src/library.rs +++ b/libraries/sabre-compiling/src/library.rs @@ -1,20 +1,32 @@ -use std::{error::Error, fs::{self, File}, io::Write, path::{Path, PathBuf}}; +use std::{ + error::Error, + fs::{self, File}, + io::Write, + path::{Path, PathBuf}, +}; -use toml::{map::Map, Table, Value}; use libloading::Library; +use toml::{map::Map, Table, Value}; use duct::{cmd, 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> -{ +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")?; + 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); @@ -31,12 +43,16 @@ pub struct RuntimeLibrary { } 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()); + 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 @@ -48,12 +64,12 @@ impl RuntimeLibrary { 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! {" + writeln!( + &mut file, + indoc! {" [package] name = \"sabre-generated\" edition = \"2021\" @@ -63,18 +79,22 @@ impl RuntimeLibrary { [workspace] [dependencies] - "})?; + "} + )?; for dependency in &dependencies { writeln!(&mut file, "{dependency}")?; } - writeln!(&mut file, indoc! {" + writeln!( + &mut file, + indoc! {" [lib] crate-type = [\"cdylib\", \"rlib\"] - "})?; - } + "} + )?; + } // Ignore the created package. { @@ -84,7 +104,7 @@ impl RuntimeLibrary { Ok(RuntimeLibrary { temp_dir: PathBuf::from(temp_dir), - source_dir + source_dir, }) } @@ -93,25 +113,37 @@ impl RuntimeLibrary { &self.source_dir } - /// Compiles the library into + /// 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"])?; + 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"); + 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"); + 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"); + path = self + .temp_dir + .clone() + .join("./target/debug/libsabre_generated.dylib"); if !path.exists() { return Err("Could not find the compiled library!".into()); } @@ -119,8 +151,6 @@ impl RuntimeLibrary { } // Load it back in and call the rewriter. - unsafe { - Ok(Library::new(&path)?) - } + unsafe { Ok(Library::new(&path)?) } } -} \ No newline at end of file +} diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index 2e887fbb..7e8978f3 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -64,12 +64,12 @@ impl SabreCompilingRewriter { info!("Using local dependency {}", path); dependencies.push(format!( - "sabre-ffi = {{ path = \"{}\" }}", PathBuf::from(path).join("sabre-ffi").to_string_lossy() + "sabre-ffi = {{ path = '{}' }}", PathBuf::from(path).join("sabre-ffi").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(), + "sabre-ffi = { git = 'https://github.com/mlaveaux/mCRL2-rust.git' }".to_string(), ); } From 2feff32fb53bf06d812a4e9108591678ed1df17b Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 16 Apr 2024 13:24:52 +0200 Subject: [PATCH 16/25] Minor cleanup --- Cargo.lock | 16 ++++++++-------- libraries/sabre-compiling/build.rs | 2 -- libraries/sabre-compiling/src/sabre_compiling.rs | 4 ++-- 3 files changed, 10 insertions(+), 12 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e831bbf5..ea967681 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4412,9 +4412,9 @@ dependencies = [ [[package]] name = "stabby" -version = "4.0.3" +version = "4.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0d703a24a549fc06c1535ad416df7375e781a0613b6ef965218c698e52383edb" +checksum = "6ec04c5825384722310b6a1fd83023bee0bfdc838f7aa3069f0a59e10203836b" dependencies = [ "lazy_static", "rustversion", @@ -4423,9 +4423,9 @@ dependencies = [ [[package]] name = "stabby-abi" -version = "4.0.3" +version = "4.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94ee77c602ee96c410efd3756dbab4c0f7ccf35a6a3d3dca5c55dcf5cc7ad175" +checksum = "976322da1deb6cc64a8406fd24378b840b1962acaac1978a993131c3838d81b3" dependencies = [ "libc", "rustversion", @@ -4435,9 +4435,9 @@ dependencies = [ [[package]] name = "stabby-macros" -version = "4.0.3" +version = "4.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e3fdde04cf3de956591380cf08c0cba18fd225156c3a0a1092d6fde5d93103a0" +checksum = "736712a13ab37b1fa6e073831efca751bbcb31033af4d7308bd5d9d605939183" dependencies = [ "proc-macro-crate 3.1.0", "proc-macro2", @@ -4566,9 +4566,9 @@ dependencies = [ [[package]] name = "temp-dir" -version = "0.1.12" +version = "0.1.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dd16aa9ffe15fe021c6ee3766772132c6e98dfa395a167e16864f61a9cfb71d6" +checksum = "1f227968ec00f0e5322f9b8173c7a0cbcff6181a0a5b28e9892491c286277231" [[package]] name = "tempfile" diff --git a/libraries/sabre-compiling/build.rs b/libraries/sabre-compiling/build.rs index 55f8cf50..27c15c38 100644 --- a/libraries/sabre-compiling/build.rs +++ b/libraries/sabre-compiling/build.rs @@ -1,8 +1,6 @@ use std::fs; use std::{env, error::Error, fs::File}; -use toml::{map::Map, Table, Value}; - use std::io::Write; /// Write every environment variable in the variables array. diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index 7e8978f3..d6f26c50 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -37,7 +37,7 @@ impl SabreCompilingRewriter { /// - 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. pub fn new( - tp: Rc>, + _tp: Rc>, spec: &RewriteSpecification, use_local_workspace: bool, use_local_tmp: bool, @@ -76,7 +76,7 @@ impl SabreCompilingRewriter { let mut compilation_crate = RuntimeLibrary::new(temp_dir, dependencies)?; // Generate the automata used for matching - let apma = SetAutomaton::new(spec, |_| (), true); + let _apma = SetAutomaton::new(spec, |_| (), true); // Write the output source file(s). { From dcf834d6c5e3dc78a92cc2eee9c604bf875a00fe Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 16 Apr 2024 17:27:28 +0200 Subject: [PATCH 17/25] Removed the sabre-ffi and moved code generation to its own module. --- Cargo.lock | 52 ------------------- Cargo.toml | 1 - libraries/mcrl2/src/aterm/term.rs | 2 +- libraries/mcrl2/src/data/data_terms.rs | 1 + libraries/sabre-compiling/Cargo.toml | 1 - libraries/sabre-compiling/examples/rewrite.rs | 16 ++++-- .../sabre-compiling/sabre-ffi/Cargo.toml | 12 ----- .../sabre-compiling/sabre-ffi/src/atermpp.rs | 1 - .../sabre-compiling/sabre-ffi/src/lib.rs | 8 --- .../sabre-compiling/src/innermost_codegen.rs | 35 +++++++++++++ libraries/sabre-compiling/src/lib.rs | 4 +- .../sabre-compiling/src/sabre_compiling.rs | 44 ++++++---------- 12 files changed, 69 insertions(+), 108 deletions(-) delete mode 100644 libraries/sabre-compiling/sabre-ffi/Cargo.toml delete mode 100644 libraries/sabre-compiling/sabre-ffi/src/atermpp.rs delete mode 100644 libraries/sabre-compiling/sabre-ffi/src/lib.rs create mode 100644 libraries/sabre-compiling/src/innermost_codegen.rs diff --git a/Cargo.lock b/Cargo.lock index ea967681..6387f8d1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -3985,21 +3985,11 @@ dependencies = [ "log", "mcrl2", "sabre", - "sabre-ffi", "temp-dir", "test-log", "toml", ] -[[package]] -name = "sabre-ffi" -version = "0.1.0" -dependencies = [ - "mcrl2", - "stabby", - "test-log", -] - [[package]] name = "same-file" version = "1.0.6" @@ -4131,12 +4121,6 @@ dependencies = [ "digest", ] -[[package]] -name = "sha2-const-stable" -version = "0.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5f179d4e11094a893b82fff208f74d448a7512f99f5a0acbd5c679b705f83ed9" - [[package]] name = "sharded-slab" version = "0.1.7" @@ -4410,42 +4394,6 @@ dependencies = [ "pin-utils", ] -[[package]] -name = "stabby" -version = "4.0.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ec04c5825384722310b6a1fd83023bee0bfdc838f7aa3069f0a59e10203836b" -dependencies = [ - "lazy_static", - "rustversion", - "stabby-abi", -] - -[[package]] -name = "stabby-abi" -version = "4.0.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "976322da1deb6cc64a8406fd24378b840b1962acaac1978a993131c3838d81b3" -dependencies = [ - "libc", - "rustversion", - "sha2-const-stable", - "stabby-macros", -] - -[[package]] -name = "stabby-macros" -version = "4.0.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "736712a13ab37b1fa6e073831efca751bbcb31033af4d7308bd5d9d605939183" -dependencies = [ - "proc-macro-crate 3.1.0", - "proc-macro2", - "quote", - "rand", - "syn 1.0.109", -] - [[package]] name = "stable_deref_trait" version = "1.2.0" diff --git a/Cargo.toml b/Cargo.toml index b3004e18..d962a43b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -8,7 +8,6 @@ debug = "line-tables-only" resolver = "2" members = [ "libraries/*", - "libraries/sabre-compiling/sabre-ffi", "libraries/**/benchmarks", "tools/*", "tools/**/benchmarks", diff --git a/libraries/mcrl2/src/aterm/term.rs b/libraries/mcrl2/src/aterm/term.rs index 67cf6880..bb8acc8b 100644 --- a/libraries/mcrl2/src/aterm/term.rs +++ b/libraries/mcrl2/src/aterm/term.rs @@ -26,8 +26,8 @@ use super::global_aterm_pool::GLOBAL_TERM_POOL; /// to acquire the 'static lifetime. This occasionally gives rise to issues /// 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. -#[repr(transparent)] #[derive(Hash, PartialEq, Eq, PartialOrd, Ord)] +#[repr(transparent)] pub struct ATermRef<'a> { term: *const ffi::_aterm, marker: PhantomData<&'a ()>, 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 index 30020841..e8b062c4 100644 --- a/libraries/sabre-compiling/Cargo.toml +++ b/libraries/sabre-compiling/Cargo.toml @@ -10,7 +10,6 @@ indoc = "2.0" libloading = "0.8" temp-dir = "0.1" toml = "0.8" -sabre-ffi = { path = "./sabre-ffi" } env_logger.workspace = true log.workspace = true mcrl2.workspace = true diff --git a/libraries/sabre-compiling/examples/rewrite.rs b/libraries/sabre-compiling/examples/rewrite.rs index d5727d01..242a8aff 100644 --- a/libraries/sabre-compiling/examples/rewrite.rs +++ b/libraries/sabre-compiling/examples/rewrite.rs @@ -1,8 +1,18 @@ -use sabre_ffi::ATerm; +use mcrl2::{aterm::{ATerm, TermPool}, data::{DataApplication, DataExpression, DataExpressionRef}}; +/// Generic rewrite function #[no_mangle] -pub unsafe extern "C" fn rewrite_term(term: ATerm) -> ATerm { - term +pub unsafe extern "C" fn rewrite_term(term: DataExpression) -> DataExpression { + let mut arguments: Vec = vec![]; + let mut tp = TermPool::new(); + + for arg in term.data_arguments() { + let t: DataExpressionRef<'_> = arg.into(); + + arguments.push(rewrite_term(t.protect()).into()); + } + + DataApplication::new(&mut tp, &term.data_function_symbol(), &arguments).into() } fn main() { diff --git a/libraries/sabre-compiling/sabre-ffi/Cargo.toml b/libraries/sabre-compiling/sabre-ffi/Cargo.toml deleted file mode 100644 index 367bb6f3..00000000 --- a/libraries/sabre-compiling/sabre-ffi/Cargo.toml +++ /dev/null @@ -1,12 +0,0 @@ -[package] -name = "sabre-ffi" -version.workspace = true -rust-version.workspace = true -edition.workspace = true - -[dependencies] -stabby = "4.0" -mcrl2.workspace = true - -[dev-dependencies] -test-log.workspace = true \ No newline at end of file diff --git a/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs b/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs deleted file mode 100644 index 16a8156c..00000000 --- a/libraries/sabre-compiling/sabre-ffi/src/atermpp.rs +++ /dev/null @@ -1 +0,0 @@ -pub use mcrl2::aterm::ATerm; \ No newline at end of file diff --git a/libraries/sabre-compiling/sabre-ffi/src/lib.rs b/libraries/sabre-compiling/sabre-ffi/src/lib.rs deleted file mode 100644 index e21f4309..00000000 --- a/libraries/sabre-compiling/sabre-ffi/src/lib.rs +++ /dev/null @@ -1,8 +0,0 @@ -//! -//! This crate provides a Rust to Rust stable ABI to allow the compiling rewriter to be compiled -//! with a different version of rustc. -//! - -mod atermpp; - -pub use atermpp::*; \ No newline at end of file diff --git a/libraries/sabre-compiling/src/innermost_codegen.rs b/libraries/sabre-compiling/src/innermost_codegen.rs new file mode 100644 index 00000000..b3a2c234 --- /dev/null +++ b/libraries/sabre-compiling/src/innermost_codegen.rs @@ -0,0 +1,35 @@ +use std::{error::Error, fs::File, io::Write, path::{Path, PathBuf}}; + +use indoc::indoc; + +pub fn generate(source_dir: &Path) -> Result<(), Box> { + + { + let mut file = + File::create(PathBuf::from(source_dir).join("lib.rs"))?; + + writeln!( + &mut file, + indoc! {" + use mcrl2::{{aterm::{{ATerm, TermPool}}, data::{{DataApplication, DataExpression, DataExpressionRef}}}}; + + /// Generic rewrite function + #[no_mangle] + pub unsafe extern \"C\" fn rewrite_term(term: DataExpression) -> DataExpression {{ + let mut arguments: Vec = vec![]; + let mut tp = TermPool::new(); + + for arg in term.data_arguments() {{ + let t: DataExpressionRef<'_> = arg.into(); + + arguments.push(rewrite_term(t.protect()).into()); + }} + + DataApplication::new(&mut tp, &term.data_function_symbol(), &arguments).into() + }} + "} + )?; + } + + Ok(()) +} \ No newline at end of file diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index 89ddbd2f..68225ff3 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -5,5 +5,7 @@ mod library; mod sabre_compiling; +mod innermost_codegen; -pub use sabre_compiling::*; \ No newline at end of file +pub use sabre_compiling::*; +pub use innermost_codegen::*; \ No newline at end of file diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index d6f26c50..4323415b 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -1,8 +1,10 @@ use std::{ - cell::RefCell, error::Error, fs::File, io::Write, path::{Path, PathBuf}, rc::Rc + cell::RefCell, + error::Error, + path::{Path, PathBuf}, + rc::Rc, }; -use indoc::indoc; use libloading::{Library, Symbol}; use log::info; use temp_dir::TempDir; @@ -11,7 +13,7 @@ use toml::Table; use mcrl2::{aterm::TermPool, data::DataExpression}; use sabre::{set_automaton::SetAutomaton, RewriteEngine, RewriteSpecification}; -use crate::library::RuntimeLibrary; +use crate::{generate, library::RuntimeLibrary}; pub struct SabreCompilingRewriter { library: Library, @@ -42,7 +44,6 @@ impl SabreCompilingRewriter { 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") @@ -53,18 +54,20 @@ impl SabreCompilingRewriter { let mut dependencies = vec![]; if use_local_workspace { - let compilation_toml = include_str!("../../../target/Compilation.toml").parse::
()?; + 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")?; + .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!( - "sabre-ffi = {{ path = '{}' }}", PathBuf::from(path).join("sabre-ffi").to_string_lossy() + "mcrl2 = {{ path = '{}' }}", + PathBuf::from(path).join("../mcrl2").to_string_lossy() )); } else { info!("Using git dependency https://github.com/mlaveaux/mCRL2-rust.git"); @@ -79,22 +82,7 @@ impl SabreCompilingRewriter { let _apma = SetAutomaton::new(spec, |_| (), true); // Write the output source file(s). - { - let mut file = - File::create(PathBuf::from(compilation_crate.source_dir()).join("lib.rs"))?; - - writeln!( - &mut file, - indoc! {" - use sabre_ffi::ATerm; - - #[no_mangle] - pub unsafe extern \"C\" fn rewrite_term(term: ATerm) -> ATerm {{ - term - }} - "} - )?; - } + generate(compilation_crate.source_dir())?; let library = compilation_crate.compile()?; Ok(SabreCompilingRewriter { library }) From 5a3c00c45abacbb768169d7b04155151f30c870c Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 21 Jun 2024 12:09:37 +0200 Subject: [PATCH 18/25] Updated to the latest version. --- Cargo.toml | 6 ++++- libraries/sabre-compiling/Cargo.toml | 12 ++++----- libraries/sabre-compiling/build.rs | 14 +++++++--- libraries/sabre-compiling/examples/rewrite.rs | 10 ++++--- .../sabre-compiling/src/innermost_codegen.rs | 16 ++++++----- libraries/sabre-compiling/src/lib.rs | 6 ++--- libraries/sabre-compiling/src/library.rs | 19 +++++++------ .../sabre-compiling/src/sabre_compiling.rs | 26 ++++++++++-------- tools/mcrl2rewrite/src/lib.rs | 27 ++++++++++++------- 9 files changed, 82 insertions(+), 54 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index d962a43b..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" diff --git a/libraries/sabre-compiling/Cargo.toml b/libraries/sabre-compiling/Cargo.toml index e8b062c4..cd107a69 100644 --- a/libraries/sabre-compiling/Cargo.toml +++ b/libraries/sabre-compiling/Cargo.toml @@ -5,11 +5,11 @@ rust-version.workspace = true edition.workspace = true [dependencies] -duct = "0.13" -indoc = "2.0" -libloading = "0.8" -temp-dir = "0.1" -toml = "0.8" +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 @@ -19,4 +19,4 @@ sabre.workspace = true test-log.workspace = true [build-dependencies] -toml = "0.8" \ No newline at end of file +toml.workspace = true \ No newline at end of file diff --git a/libraries/sabre-compiling/build.rs b/libraries/sabre-compiling/build.rs index 27c15c38..f6286e49 100644 --- a/libraries/sabre-compiling/build.rs +++ b/libraries/sabre-compiling/build.rs @@ -1,5 +1,7 @@ +use std::env; +use std::error::Error; use std::fs; -use std::{env, error::Error, fs::File}; +use std::fs::File; use std::io::Write; @@ -19,13 +21,17 @@ fn main() -> Result<(), Box> { let mut file = File::create("../../target/Compilation.toml")?; - // Write the development location. + // Write the development location. writeln!(file, "[sabrec]")?; - writeln!(file, "path = '{}'", fs::canonicalize(".")?.to_string_lossy())?; + 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(()) -} \ No newline at end of file +} diff --git a/libraries/sabre-compiling/examples/rewrite.rs b/libraries/sabre-compiling/examples/rewrite.rs index 242a8aff..adec4c8b 100644 --- a/libraries/sabre-compiling/examples/rewrite.rs +++ b/libraries/sabre-compiling/examples/rewrite.rs @@ -1,4 +1,8 @@ -use mcrl2::{aterm::{ATerm, TermPool}, data::{DataApplication, DataExpression, DataExpressionRef}}; +use mcrl2::aterm::ATerm; +use mcrl2::aterm::TermPool; +use mcrl2::data::DataApplication; +use mcrl2::data::DataExpression; +use mcrl2::data::DataExpressionRef; /// Generic rewrite function #[no_mangle] @@ -15,6 +19,4 @@ pub unsafe extern "C" fn rewrite_term(term: DataExpression) -> DataExpression { DataApplication::new(&mut tp, &term.data_function_symbol(), &arguments).into() } -fn main() { - -} \ No newline at end of file +fn main() {} diff --git a/libraries/sabre-compiling/src/innermost_codegen.rs b/libraries/sabre-compiling/src/innermost_codegen.rs index b3a2c234..3a3ac9ab 100644 --- a/libraries/sabre-compiling/src/innermost_codegen.rs +++ b/libraries/sabre-compiling/src/innermost_codegen.rs @@ -1,16 +1,18 @@ -use std::{error::Error, fs::File, io::Write, path::{Path, PathBuf}}; +use std::error::Error; +use std::fs::File; +use std::io::Write; +use std::path::Path; +use std::path::PathBuf; use indoc::indoc; pub fn generate(source_dir: &Path) -> Result<(), Box> { - { - let mut file = - File::create(PathBuf::from(source_dir).join("lib.rs"))?; - + let mut file = File::create(PathBuf::from(source_dir).join("lib.rs"))?; + writeln!( &mut file, - indoc! {" + indoc! {" use mcrl2::{{aterm::{{ATerm, TermPool}}, data::{{DataApplication, DataExpression, DataExpressionRef}}}}; /// Generic rewrite function @@ -32,4 +34,4 @@ pub fn generate(source_dir: &Path) -> Result<(), Box> { } Ok(()) -} \ No newline at end of file +} diff --git a/libraries/sabre-compiling/src/lib.rs b/libraries/sabre-compiling/src/lib.rs index 68225ff3..66fba464 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -1,11 +1,11 @@ //! //! This module contains an implementation for a compiling variant of the Sabre //! rewrite engine. -//! +//! +mod innermost_codegen; mod library; mod sabre_compiling; -mod innermost_codegen; +pub use innermost_codegen::*; pub use sabre_compiling::*; -pub use innermost_codegen::*; \ No newline at end of file diff --git a/libraries/sabre-compiling/src/library.rs b/libraries/sabre-compiling/src/library.rs index 1d97544a..670a1d82 100644 --- a/libraries/sabre-compiling/src/library.rs +++ b/libraries/sabre-compiling/src/library.rs @@ -1,14 +1,17 @@ -use std::{ - error::Error, - fs::{self, File}, - io::Write, - path::{Path, PathBuf}, -}; +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, Table, Value}; +use toml::map::Map; +use toml::Table; +use toml::Value; -use duct::{cmd, Expression}; +use duct::cmd; +use duct::Expression; use indoc::indoc; use log::info; diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index 4323415b..ed43ccf1 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -1,19 +1,23 @@ -use std::{ - cell::RefCell, - error::Error, - path::{Path, PathBuf}, - rc::Rc, -}; - -use libloading::{Library, Symbol}; +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, data::DataExpression}; -use sabre::{set_automaton::SetAutomaton, RewriteEngine, RewriteSpecification}; +use mcrl2::aterm::TermPool; +use mcrl2::data::DataExpression; +use sabre::set_automaton::SetAutomaton; +use sabre::RewriteEngine; +use sabre::RewriteSpecification; -use crate::{generate, library::RuntimeLibrary}; +use crate::generate; +use crate::library::RuntimeLibrary; pub struct SabreCompilingRewriter { library: Library, diff --git a/tools/mcrl2rewrite/src/lib.rs b/tools/mcrl2rewrite/src/lib.rs index 2e2de9d8..374cca22 100644 --- a/tools/mcrl2rewrite/src/lib.rs +++ b/tools/mcrl2rewrite/src/lib.rs @@ -93,19 +93,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 mut sabre_rewriter = + SabreCompilingRewriter::new(tp.clone(), &rewrite_spec, true, false).unwrap(); + let now = Instant::now(); - for term in &terms { + 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()); + println!( + "Sabre compiling rewrite took {} ms", + now.elapsed().as_millis() + ); } } @@ -151,10 +155,10 @@ 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 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()); @@ -163,8 +167,11 @@ pub fn rewrite_rec( println!("{}", result) } } - println!("Sabre compiling rewrite took {} ms", now.elapsed().as_millis()); - }, + println!( + "Sabre compiling rewrite took {} ms", + now.elapsed().as_millis() + ); + } Rewriter::Jitty => { bail!("Cannot use REC specifications with mCRL2's jitty rewriter"); } From 65d2f13fa149a1474010bf91d24bc982fbb95e49 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 21 Jun 2024 16:21:17 +0200 Subject: [PATCH 19/25] Started to implement the innermost codegen. --- libraries/sabre-compiling/examples/rewrite.rs | 22 ------ .../sabre-compiling/src/innermost_codegen.rs | 77 +++++++++++++++---- .../sabre-compiling/src/sabre_compiling.rs | 12 +-- 3 files changed, 70 insertions(+), 41 deletions(-) delete mode 100644 libraries/sabre-compiling/examples/rewrite.rs diff --git a/libraries/sabre-compiling/examples/rewrite.rs b/libraries/sabre-compiling/examples/rewrite.rs deleted file mode 100644 index adec4c8b..00000000 --- a/libraries/sabre-compiling/examples/rewrite.rs +++ /dev/null @@ -1,22 +0,0 @@ -use mcrl2::aterm::ATerm; -use mcrl2::aterm::TermPool; -use mcrl2::data::DataApplication; -use mcrl2::data::DataExpression; -use mcrl2::data::DataExpressionRef; - -/// Generic rewrite function -#[no_mangle] -pub unsafe extern "C" fn rewrite_term(term: DataExpression) -> DataExpression { - let mut arguments: Vec = vec![]; - let mut tp = TermPool::new(); - - for arg in term.data_arguments() { - let t: DataExpressionRef<'_> = arg.into(); - - arguments.push(rewrite_term(t.protect()).into()); - } - - DataApplication::new(&mut tp, &term.data_function_symbol(), &arguments).into() -} - -fn main() {} diff --git a/libraries/sabre-compiling/src/innermost_codegen.rs b/libraries/sabre-compiling/src/innermost_codegen.rs index 3a3ac9ab..a049682e 100644 --- a/libraries/sabre-compiling/src/innermost_codegen.rs +++ b/libraries/sabre-compiling/src/innermost_codegen.rs @@ -1,3 +1,4 @@ +use std::collections::HashSet; use std::error::Error; use std::fs::File; use std::io::Write; @@ -5,32 +6,80 @@ 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(source_dir: &Path) -> Result<(), Box> { +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::{{aterm::{{ATerm, TermPool}}, data::{{DataApplication, DataExpression, DataExpressionRef}}}}; + indoc! {"use mcrl2::data::DataExpression; + use mcrl2::data::DataExpressionRef; /// Generic rewrite function #[no_mangle] - pub unsafe extern \"C\" fn rewrite_term(term: DataExpression) -> DataExpression {{ - let mut arguments: Vec = vec![]; - let mut tp = TermPool::new(); - - for arg in term.data_arguments() {{ - let t: DataExpressionRef<'_> = arg.into(); - - arguments.push(rewrite_term(t.protect()).into()); - }} - - DataApplication::new(&mut tp, &term.data_function_symbol(), &arguments).into() + 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);", 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\tt")?; + writeln!(&mut file, "\t\t}}")?; + } + } + + // No match + writeln!(&mut file, indoc! { + "_ => {{ + t.protect() + }}"})?; + + 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> {{", 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(()) diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index ed43ccf1..8c60fc3c 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -28,7 +28,7 @@ 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 = self.library.get(b"rewrite_term").unwrap(); + let func: Symbol = self.library.get(b"rewrite").unwrap(); func(); @@ -82,11 +82,9 @@ impl SabreCompilingRewriter { let mut compilation_crate = RuntimeLibrary::new(temp_dir, dependencies)?; - // Generate the automata used for matching - let _apma = SetAutomaton::new(spec, |_| (), true); // Write the output source file(s). - generate(compilation_crate.source_dir())?; + generate(spec, compilation_crate.source_dir())?; let library = compilation_crate.compile()?; Ok(SabreCompilingRewriter { library }) @@ -104,6 +102,10 @@ mod tests { let spec = RewriteSpecification::default(); let tp = Rc::new(RefCell::new(TermPool::new())); - SabreCompilingRewriter::new(tp, &spec, true, true).unwrap(); + let mut rewriter = SabreCompilingRewriter::new(tp, &spec, true, true).unwrap(); + + let t = DataExpression::default(); + + assert_eq!(rewriter.rewrite(t.clone()), t, "The rewritten result does not match the expected result"); } } From 124318963fb5b0763b2fe7e3dd5f5588757a5532 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 21 Jun 2024 16:21:47 +0200 Subject: [PATCH 20/25] Added explicit immutable accessors to the set automaton. --- libraries/sabre/src/innermost_rewriter.rs | 19 ++-- libraries/sabre/src/sabre_rewriter.rs | 23 +++-- .../sabre/src/set_automaton/automaton.rs | 99 ++++++++++++++----- libraries/sabre/src/set_automaton/display.rs | 42 ++++---- .../sabre/src/set_automaton/match_goal.rs | 8 +- 5 files changed, 124 insertions(+), 67 deletions(-) diff --git a/libraries/sabre/src/innermost_rewriter.rs b/libraries/sabre/src/innermost_rewriter.rs index fcb71b1d..204591b2 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,6 +195,9 @@ impl InnermostRewriter { .pop() .expect("The result should be the last element on the stack") .protect(); + }, + Config::Yield(_, _) => { + unreachable!(""); } } @@ -206,6 +209,7 @@ impl InnermostRewriter { match x { Config::Construct(_, _, result) => index == *result, Config::Rewrite(result) => index == *result, + Config::Yield(_, _) => true, Config::Return() => true, } }), @@ -229,19 +233,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 +256,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..d65df381 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 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..508e7510 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(); 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 { From e5b35cea909ce60030c852ae9294e166a295bc09 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 22 Jun 2024 23:54:54 +0200 Subject: [PATCH 21/25] Fixed compilation errors. --- libraries/sabre/src/set_automaton/automaton.rs | 2 +- libraries/sabre/src/utilities/configuration_stack.rs | 2 +- libraries/sabre/src/utilities/innermost_stack.rs | 8 ++++++-- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/libraries/sabre/src/set_automaton/automaton.rs b/libraries/sabre/src/set_automaton/automaton.rs index d65df381..10480710 100644 --- a/libraries/sabre/src/set_automaton/automaton.rs +++ b/libraries/sabre/src/set_automaton/automaton.rs @@ -323,7 +323,7 @@ impl State { } /// Returns the match goals of the state. - pub fn match_goals(&self) -> &Vec { + pub(crate) fn match_goals(&self) -> &Vec { &self.match_goals } 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, } From 27f755693a1ea1a1850f3b1fa582b5582ea3574f Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sun, 23 Jun 2024 15:08:06 +0200 Subject: [PATCH 22/25] Fixed calling the rewrite function. --- libraries/sabre-compiling/src/innermost_codegen.rs | 8 ++++---- libraries/sabre-compiling/src/sabre_compiling.rs | 7 ++----- libraries/sabre/src/innermost_rewriter.rs | 4 ---- libraries/sabre/src/set_automaton/match_goal.rs | 4 ++-- 4 files changed, 8 insertions(+), 15 deletions(-) diff --git a/libraries/sabre-compiling/src/innermost_codegen.rs b/libraries/sabre-compiling/src/innermost_codegen.rs index a049682e..70085d1a 100644 --- a/libraries/sabre-compiling/src/innermost_codegen.rs +++ b/libraries/sabre-compiling/src/innermost_codegen.rs @@ -49,7 +49,7 @@ pub fn generate(spec: &RewriteSpecification, source_dir: &Path) -> Result<(), Bo writeln!(&mut file, "\t\t{symbol} => {{")?; // Continue on the outgoing transition. - for (announcement, annotation) in transition.announcements() { + for (_announcement, _annotation) in transition.announcements() { } @@ -60,9 +60,9 @@ pub fn generate(spec: &RewriteSpecification, source_dir: &Path) -> Result<(), Bo // No match writeln!(&mut file, indoc! { - "_ => {{ - t.protect() - }}"})?; + "\t\t_ => {{ + \t\t t.protect() + \t\t}}"})?; writeln!(&mut file, "\t }}")?; writeln!(&mut file, "}}")?; diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index 8c60fc3c..ef03c65c 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -12,7 +12,6 @@ use toml::Table; use mcrl2::aterm::TermPool; use mcrl2::data::DataExpression; -use sabre::set_automaton::SetAutomaton; use sabre::RewriteEngine; use sabre::RewriteSpecification; @@ -28,11 +27,9 @@ 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 = self.library.get(b"rewrite").unwrap(); + let func: Symbol DataExpression> = self.library.get(b"rewrite").unwrap(); - func(); - - term + func(term) } } } diff --git a/libraries/sabre/src/innermost_rewriter.rs b/libraries/sabre/src/innermost_rewriter.rs index 204591b2..2046e894 100644 --- a/libraries/sabre/src/innermost_rewriter.rs +++ b/libraries/sabre/src/innermost_rewriter.rs @@ -196,9 +196,6 @@ impl InnermostRewriter { .expect("The result should be the last element on the stack") .protect(); }, - Config::Yield(_, _) => { - unreachable!(""); - } } let read_configs = stack.configs.read(); @@ -209,7 +206,6 @@ impl InnermostRewriter { match x { Config::Construct(_, _, result) => index == *result, Config::Rewrite(result) => index == *result, - Config::Yield(_, _) => true, Config::Return() => true, } }), diff --git a/libraries/sabre/src/set_automaton/match_goal.rs b/libraries/sabre/src/set_automaton/match_goal.rs index 508e7510..d1c8d7fb 100644 --- a/libraries/sabre/src/set_automaton/match_goal.rs +++ b/libraries/sabre/src/set_automaton/match_goal.rs @@ -28,9 +28,9 @@ 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 From 24159b06c03584af528f942030147a93651b1c23 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sun, 23 Jun 2024 15:10:08 +0200 Subject: [PATCH 23/25] Changed the test. --- libraries/sabre-compiling/src/sabre_compiling.rs | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index ef03c65c..8054a2c2 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -92,16 +92,24 @@ impl SabreCompilingRewriter { mod tests { use super::*; + use mcrl2::data::DataSpecification; use test_log::test; #[test] fn test_compilation() { - let spec = RewriteSpecification::default(); - let tp = Rc::new(RefCell::new(TermPool::new())); - let mut rewriter = SabreCompilingRewriter::new(tp, &spec, true, true).unwrap(); + 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 t = DataExpression::default(); + let mut rewriter = SabreCompilingRewriter::new(tp, &spec).unwrap(); assert_eq!(rewriter.rewrite(t.clone()), t, "The rewritten result does not match the expected result"); } From 063d0c5df56a1780d12acbb146b450d30f702a13 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Mon, 24 Jun 2024 11:58:14 +0200 Subject: [PATCH 24/25] Fixed compilation errors. --- .../sabre-compiling/src/innermost_codegen.rs | 124 +++++++++++------- libraries/sabre-compiling/src/lib.rs | 2 +- .../sabre-compiling/src/sabre_compiling.rs | 2 +- 3 files changed, 75 insertions(+), 53 deletions(-) diff --git a/libraries/sabre-compiling/src/innermost_codegen.rs b/libraries/sabre-compiling/src/innermost_codegen.rs index 70085d1a..5659f38e 100644 --- a/libraries/sabre-compiling/src/innermost_codegen.rs +++ b/libraries/sabre-compiling/src/innermost_codegen.rs @@ -1,5 +1,6 @@ use std::collections::HashSet; use std::error::Error; +use std::fmt; use std::fs::File; use std::io::Write; use std::path::Path; @@ -11,76 +12,97 @@ 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"))?; + let mut file = File::create(PathBuf::from(source_dir).join("lib.rs"))?; - // Generate the automata used for matching - let apma = SetAutomaton::new(spec, |_| (), true); + // Generate the automata used for matching + let apma = SetAutomaton::new(spec, |_| (), true); - writeln!( - &mut file, - indoc! {"use mcrl2::data::DataExpression; - use mcrl2::data::DataExpressionRef; + 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()) - }} - "} - )?; + /// 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(); + // 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() { + 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);", state.label())?; - writeln!(&mut file, "\t let symbol = arg.data_function_symbol();")?; + 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()); + positions.insert(state.label().clone()); - writeln!(&mut file, "\t match symbol.operation_id() {{")?; + 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} => {{")?; + 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() { + // Continue on the outgoing transition. + for (_announcement, _annotation) in transition.announcements() { - } + } - writeln!(&mut file, "\t\tt")?; - writeln!(&mut file, "\t\t}}")?; - } + 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> {{", position)?; - write!(&mut file, "\t t.copy()")?; + // No match + writeln!(&mut file, indoc! { + "\t\t_ => {{ + \t\t t.protect() + \t\t}}"})?; - for index in &position.indices { - write!(&mut file, ".arg({index})")?; - } + 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()")?; - writeln!(&mut file, ".upgrade(t).into()")?; - writeln!(&mut file, "}}")?; + 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 index 66fba464..918b3e26 100644 --- a/libraries/sabre-compiling/src/lib.rs +++ b/libraries/sabre-compiling/src/lib.rs @@ -1,7 +1,7 @@ //! //! This module contains an implementation for a compiling variant of the Sabre //! rewrite engine. -//! +//! mod innermost_codegen; mod library; diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index 8054a2c2..5479c03a 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -109,7 +109,7 @@ mod tests { let spec = RewriteSpecification::from(spec); let tp = Rc::new(RefCell::new(TermPool::new())); - let mut rewriter = SabreCompilingRewriter::new(tp, &spec).unwrap(); + 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"); } From a9d0f189dc3eaad0f42a0d868e6943ddd856d33e Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Fri, 5 Jul 2024 11:25:39 +0200 Subject: [PATCH 25/25] The term should not be destroyed. --- libraries/sabre-compiling/src/sabre_compiling.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/libraries/sabre-compiling/src/sabre_compiling.rs b/libraries/sabre-compiling/src/sabre_compiling.rs index 5479c03a..fdd39aaf 100644 --- a/libraries/sabre-compiling/src/sabre_compiling.rs +++ b/libraries/sabre-compiling/src/sabre_compiling.rs @@ -27,9 +27,12 @@ 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 func: Symbol DataExpression> = self.library.get(b"rewrite").unwrap(); - func(term) + let result = func(&term); + std::mem::forget(result); + + term } } } @@ -39,6 +42,8 @@ impl SabreCompilingRewriter { /// /// - 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,