Merge with upstream

.gitignore

@@ -23,4 +23,6 @@ vendor
 examples/build
 examples/.cache
 *.coredump
+*.smt2
+cranelift/isle/veri/veri_engine/test_output
 crates/explorer/node_modules

Cargo.toml

@@ -139,6 +139,8 @@ members = [
   "cranelift",
   "cranelift/isle/fuzz",
   "cranelift/isle/islec",
+  "cranelift/isle/veri/veri_engine",
+  "cranelift/isle/veri/veri_ir",
   "cranelift/serde",
   "crates/bench-api",
   "crates/c-api/artifact",
@@ -227,7 +229,7 @@ wasmtime-jit-icache-coherence = { path = "crates/jit-icache-coherence", version
 wasmtime-wit-bindgen = { path = "crates/wit-bindgen", version = "=26.0.0" }
 test-programs-artifacts = { path = 'crates/test-programs/artifacts' }
 
-pulley-interpreter = { path = 'pulley', version = "=0.2.0" }
+pulley-interpreter = { path = 'pulley', version = "=26.0.0" }
 pulley-interpreter-fuzz = { path = 'pulley/fuzz' }
 
 cranelift-codegen = { path = "cranelift/codegen", version = "0.113.0", default-features = false, features = ["std", "unwind"] }
@@ -246,7 +248,7 @@ cranelift-bitset = { path = "cranelift/bitset", version = "0.113.0" }
 cranelift-control = { path = "cranelift/control", version = "0.113.0" }
 cranelift = { path = "cranelift/umbrella", version = "0.113.0" }
 
-winch-codegen = { path = "winch/codegen", version = "=0.24.0" }
+winch-codegen = { path = "winch/codegen", version = "=26.0.0" }
 
 wasi-preview1-component-adapter = { path = "crates/wasi-preview1-component-adapter" }
 byte-array-literals = { path = "crates/wasi-preview1-component-adapter/byte-array-literals" }

ci/run-tests.sh

@@ -12,6 +12,8 @@
 #
 # - wasm-spec-interpreter: brings in OCaml which is a pain to configure for all
 #   targets, tested as part of the wastime-fuzzing CI job.
+#
+# - veri_engine: requires an SMT solver (z3)
 
 cargo test \
       --workspace \
@@ -21,6 +23,7 @@ cargo test \
       --exclude wasmtime-fuzzing \
       --exclude wasm-spec-interpreter \
       --exclude wasmtime-winch \
+      --exclude veri_engine \
       $@
 
 # NOTE(dhil): Several WasmFX features are conflicting, so we do not
@@ -32,4 +35,5 @@ cargo test \
 #       --exclude wasmtime-wasi-nn \
 #       --exclude wasmtime-fuzzing \
 #       --exclude wasm-spec-interpreter \
+#       --exclude veri_engine \
 #       $@

cranelift/codegen/meta/src/error.rs

@@ -18,6 +18,8 @@ impl Error {
     }
 }
 
+impl std::error::Error for Error {}
+
 impl fmt::Display for Error {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         write!(f, "{}", self.inner)

cranelift/codegen/meta/src/isle.rs

@@ -11,13 +11,47 @@ pub struct IsleCompilations {
     pub items: Vec<IsleCompilation>,
 }
 
+impl IsleCompilations {
+    pub fn lookup(&self, name: &str) -> Option<&IsleCompilation> {
+        for compilation in &self.items {
+            if compilation.name == name {
+                return Some(compilation);
+            }
+        }
+        None
+    }
+}
+
 #[derive(Clone, Debug)]
 pub struct IsleCompilation {
+    pub name: String,
     pub output: std::path::PathBuf,
     pub inputs: Vec<std::path::PathBuf>,
     pub untracked_inputs: Vec<std::path::PathBuf>,
 }
 
+impl IsleCompilation {
+    pub fn inputs(&self) -> Vec<std::path::PathBuf> {
+        self.inputs
+            .iter()
+            .chain(self.untracked_inputs.iter())
+            .cloned()
+            .collect()
+    }
+}
+
+pub fn shared_isle_lower_paths(codegen_crate_dir: &std::path::Path) -> Vec<std::path::PathBuf> {
+    let inst_specs_isle = codegen_crate_dir.join("src").join("inst_specs.isle");
+    let prelude_isle = codegen_crate_dir.join("src").join("prelude.isle");
+    let prelude_lower_isle = codegen_crate_dir.join("src").join("prelude_lower.isle");
+    // The shared instruction selector logic.
+    vec![
+        inst_specs_isle.clone(),
+        prelude_isle.clone(),
+        prelude_lower_isle.clone(),
+    ]
+}
+
 /// Construct the list of compilations (transformations from ISLE
 /// source to generated Rust source) that exist in the repository.
 pub fn get_isle_compilations(
@@ -61,6 +95,7 @@ pub fn get_isle_compilations(
         items: vec![
             // The mid-end optimization rules.
             IsleCompilation {
+                name: "opt".to_string(),
                 output: gen_dir.join("isle_opt.rs"),
                 inputs: vec![
                     prelude_isle.clone(),
@@ -81,6 +116,7 @@ pub fn get_isle_compilations(
             },
             // The x86-64 instruction selector.
             IsleCompilation {
+                name: "x64".to_string(),
                 output: gen_dir.join("isle_x64.rs"),
                 inputs: vec![
                     prelude_isle.clone(),
@@ -92,6 +128,7 @@ pub fn get_isle_compilations(
             },
             // The aarch64 instruction selector.
             IsleCompilation {
+                name: "aarch64".to_string(),
                 output: gen_dir.join("isle_aarch64.rs"),
                 inputs: vec![
                     prelude_isle.clone(),
@@ -105,6 +142,7 @@ pub fn get_isle_compilations(
             },
             // The s390x instruction selector.
             IsleCompilation {
+                name: "s390x".to_string(),
                 output: gen_dir.join("isle_s390x.rs"),
                 inputs: vec![
                     prelude_isle.clone(),
@@ -116,6 +154,7 @@ pub fn get_isle_compilations(
             },
             // The risc-v instruction selector.
             IsleCompilation {
+                name: "riscv64".to_string(),
                 output: gen_dir.join("isle_riscv64.rs"),
                 inputs: vec![
                     prelude_isle.clone(),
@@ -128,6 +167,7 @@ pub fn get_isle_compilations(
             },
             // The Pulley instruction selector.
             IsleCompilation {
+                name: "pulley".to_string(),
                 output: gen_dir.join("isle_pulley_shared.rs"),
                 inputs: vec![
                     prelude_isle.clone(),