Implement a compiling version of the sabre rewriter

.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

.github/workflows/test.yml

@@ -38,3 +38,4 @@ jobs:
       env:
         RUST_BACKTRACE: full
         RUSTC_WRAPPER: sccache
+        RUST_LOG: debug

.github/workflows/test_address_sanitizer.yml

@@ -55,3 +55,4 @@ jobs:
       env:
         RUST_BACKTRACE: full
         RUSTC_WRAPPER: sccache
+        RUST_LOG: debug

.github/workflows/test_thread_sanitizer.yml

@@ -54,3 +54,4 @@ jobs:
       env:
         RUST_BACKTRACE: full
         RUSTC_WRAPPER: sccache
+        RUST_LOG: debug

.gitignore

@@ -2,12 +2,6 @@
 # will have compiled files and executables
 /target/
 
-# Folder generated by WASM.
-**/*/dist/
-
-# will have the code coverage report
-/coverage/
-
 # These are backup files generated by rustfmt
 **/*.rs.bk
 

Cargo.toml

@@ -31,11 +31,14 @@ cc = "1.0"
 clap = { version = "4.5", features = ["derive"] }
 cxx = "1.0"
 cxx-build = { version = "1.0", features = ["parallel"] }
+duct = "0.13"
 env_logger = "0.11"
 fxhash = "0.2"
 html-escape = "0.2"
+indoc = "2.0"
 itertools = "0.13"
 jemallocator = "0.5"
+libloading = "0.8"
 log = "0.4"
 once_cell = "1.19"
 pest = "2.7"
@@ -48,9 +51,11 @@ rustc-hash = "2.0.0"
 smallvec = "1.13"
 streaming-iterator = "0.1"
 syn = { version = "2.0", features = ["full", "extra-traits"] }
+temp-dir = "0.1"
 test-case = "3.3"
 test-log = "0.2"
 thiserror = "1.0"
+toml = "0.8"
 trybuild = "1.0"
 
 # Used for GUI tools
@@ -61,7 +66,6 @@ tokio = { version = "1.37", features = ["rt", "macros"] }
 winapi = "0.3"
 
 # Only used for xtask
-duct = "0.13"
 fs_extra = "1.3"
 glob = "0.3"
 human-sort = "0.2"
@@ -77,4 +81,5 @@ mcrl2-macros = { path = "libraries/mcrl2-macros" }
 mcrl2-sys = { path = "libraries/mcrl2-sys" }
 rec-tests = { path = "libraries/rec-tests" }
 sabre = { path = "libraries/sabre" }
+sabre-compiling = { path = "libraries/sabre-compiling" }
 utilities = { path = "libraries/utilities" }

libraries/mcrl2/src/aterm/term.rs

@@ -27,6 +27,7 @@ use super::global_aterm_pool::GLOBAL_TERM_POOL;
 /// where we look at the argument of a term and want to return it's name, but
 /// this is not allowed since the temporary returned by the argument is dropped.
 #[derive(Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[repr(transparent)]
 pub struct ATermRef<'a> {
     term: *const ffi::_aterm,
     marker: PhantomData<&'a ()>,
@@ -201,6 +202,7 @@ impl<'a> fmt::Debug for ATermRef<'a> {
 
 /// The protected version of [ATermRef], mostly derived from it.
 #[derive(Default)]
+#[repr(C)]
 pub struct ATerm {
     pub(crate) term: ATermRef<'static>,
     pub(crate) root: usize,

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,
     }

libraries/sabre-compiling/Cargo.toml

@@ -0,0 +1,22 @@
+[package]
+name = "sabre-compiling"
+version.workspace = true
+rust-version.workspace = true
+edition.workspace = true
+
+[dependencies]
+duct.workspace = true
+indoc.workspace = true
+libloading.workspace = true
+temp-dir.workspace = true
+toml.workspace = true
+env_logger.workspace = true
+log.workspace = true
+mcrl2.workspace = true
+sabre.workspace = true
+
+[dev-dependencies]
+test-log.workspace = true
+
+[build-dependencies]
+toml.workspace = true

libraries/sabre-compiling/build.rs

@@ -0,0 +1,37 @@
+use std::env;
+use std::error::Error;
+use std::fs;
+use std::fs::File;
+
+use std::io::Write;
+
+/// Write every environment variable in the variables array.
+fn write_env(writer: &mut impl Write, variables: &[&'static str]) -> Result<(), Box<dyn Error>> {
+    for var in variables {
+        writeln!(writer, "{} = '{}'", var, env::var(var).unwrap_or_default())?;
+    }
+
+    Ok(())
+}
+
+fn main() -> Result<(), Box<dyn Error>> {
+    for (from, to) in env::vars() {
+        println!("{} to {}", from, to);
+    }
+
+    let mut file = File::create("../../target/Compilation.toml")?;
+
+    // Write the development location.
+    writeln!(file, "[sabrec]")?;
+    writeln!(
+        file,
+        "path = '{}'",
+        fs::canonicalize(".")?.to_string_lossy()
+    )?;
+
+    // Write compilation related environment variables to the configuration file.
+    writeln!(file, "[env]")?;
+    write_env(&mut file, &["RUSTFLAGS", "CFLAGS", "CXXFLAGS"])?;
+
+    Ok(())
+}

libraries/sabre-compiling/src/innermost_codegen.rs

@@ -0,0 +1,108 @@
+use std::collections::HashSet;
+use std::error::Error;
+use std::fmt;
+use std::fs::File;
+use std::io::Write;
+use std::path::Path;
+use std::path::PathBuf;
+
+use indoc::indoc;
+use sabre::set_automaton::SetAutomaton;
+use sabre::utilities::ExplicitPosition;
+use sabre::RewriteSpecification;
+
+pub fn generate(spec: &RewriteSpecification, source_dir: &Path) -> Result<(), Box<dyn Error>> {
+    let mut file = File::create(PathBuf::from(source_dir).join("lib.rs"))?;
+
+    // Generate the automata used for matching
+    let apma = SetAutomaton::new(spec, |_| (), true);
+
+    writeln!(
+        &mut file,
+        indoc! {"use mcrl2::data::DataExpression;
+        use mcrl2::data::DataExpressionRef;
+
+        /// Generic rewrite function
+        #[no_mangle]
+        pub unsafe extern \"C\" fn rewrite(term: &DataExpression) -> DataExpression {{
+            rewrite_0(&term.copy())
+        }}
+        "}
+    )?;
+
+    // Introduce a match function for every state of the set automaton.
+    let mut positions: HashSet<ExplicitPosition> = HashSet::new();
+
+    for (index, state) in apma.states().iter().enumerate() {
+
+        writeln!(&mut file, "fn rewrite_{}(t: &DataExpressionRef<'_>) -> DataExpression {{", index)?;
+        writeln!(&mut file, "\t let arg = get_position_{}(t);", UnderscoreFormatter(state.label()))?;
+        writeln!(&mut file, "\t let symbol = arg.data_function_symbol();")?;
+
+        positions.insert(state.label().clone());
+
+        writeln!(&mut file, "\t match symbol.operation_id() {{")?;
+
+        for ((from, symbol), transition) in apma.transitions() {
+            // TODO: Only take outgoing directly.
+            if *from == index {
+                writeln!(&mut file, "\t\t{symbol} => {{")?;
+
+                // Continue on the outgoing transition.
+                for (_announcement, _annotation) in transition.announcements() {
+
+                }                    
+
+                writeln!(&mut file, "\t\t\tt.protect()")?;
+                writeln!(&mut file, "\t\t}}")?;
+            }
+        }
+
+        // No match
+        writeln!(&mut file, indoc! {
+        "\t\t_ => {{
+            \t\t   t.protect()
+            \t\t}}"})?;
+
+        writeln!(&mut file, "\t }}")?;
+        writeln!(&mut file, "}}")?;
+    }
+
+    // Introduce getters for all the positions that must be read from terms.
+    for position in &positions {
+        writeln!(&mut file, "fn get_position_{}<'a>(t: &'a DataExpressionRef<'_>) -> DataExpressionRef<'a> {{", UnderscoreFormatter(position))?;
+        write!(&mut file, "\t t.copy()")?;
+
+        for index in &position.indices {
+            write!(&mut file, ".arg({index})")?;
+        }
+
+        writeln!(&mut file, ".upgrade(t).into()")?;
+        writeln!(&mut file, "}}")?;
+    }
+
+    Ok(())
+}
+
+struct UnderscoreFormatter<'a>(&'a ExplicitPosition);
+
+impl fmt::Display for UnderscoreFormatter<'_> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+
+        if self.0.indices.is_empty() {
+            write!(f, "epsilon")?;
+        } else {
+            let mut first = true;
+            for p in &self.0.indices {
+                if first {
+                    write!(f, "{}", p)?;
+                    first = false;
+                } else {
+                    write!(f, "_{}", p)?;
+                }
+            }
+        }
+
+        Ok(())
+    }
+}

libraries/sabre-compiling/src/lib.rs

@@ -0,0 +1,11 @@
+//!
+//! This module contains an implementation for a compiling variant of the Sabre
+//! rewrite engine.
+//! 
+
+mod innermost_codegen;
+mod library;
+mod sabre_compiling;
+
+pub use innermost_codegen::*;
+pub use sabre_compiling::*;