Add support for running the regalloc2 checker. (#4043)

With these fixes, all this PR has to do is instantiate and run the
checker on the `regalloc2::Output`. This is off by default, and is
enabled by setting the `regalloc_checker` Cranelift option.

This restores the old functionality provided by e.g. the
`backtracking_checked` regalloc algorithm setting rather than
`backtracking` when we were still on regalloc.rs.

cranelift/codegen/Cargo.toml

@@ -23,7 +23,7 @@ serde = { version = "1.0.94", features = ["derive"], optional = true }
 bincode = { version = "1.2.1", optional = true }
 gimli = { version = "0.26.0", default-features = false, features = ["write"], optional = true }
 smallvec = { version = "1.6.1" }
-regalloc2 = { version = "0.1.1", features = ["checker"] }
+regalloc2 = { version = "0.1.2", features = ["checker"] }
 souper-ir = { version = "2.1.0", optional = true }
 # It is a goal of the cranelift-codegen crate to have minimal external dependencies.
 # Please don't add any unless they are essential to the task of creating binary

cranelift/codegen/meta/src/shared/settings.rs

@@ -3,6 +3,21 @@ use crate::cdsl::settings::{SettingGroup, SettingGroupBuilder};
 pub(crate) fn define() -> SettingGroup {
     let mut settings = SettingGroupBuilder::new("shared");
 
+    settings.add_bool(
+        "regalloc_checker",
+        "Enable the symbolic checker for register allocation.",
+        r#"
+            This performs a verification that the register allocator preserves
+            equivalent dataflow with respect to the original (pre-regalloc)
+            program. This analysis is somewhat expensive. However, if it succeeds,
+            it provides independent evidence (by a carefully-reviewed, from-first-principles
+            analysis) that no regalloc bugs were triggered for the particular compilations
+            performed. This is a valuable assurance to have as regalloc bugs can be
+            very dangerous and difficult to debug.
+        "#,
+        false,
+    );
+
     settings.add_enum(
         "opt_level",
         "Optimization level for generated code.",

cranelift/codegen/src/machinst/compile.rs

@@ -47,5 +47,23 @@ pub fn compile<B: LowerBackend + TargetIsa>(
             .expect("register allocation")
     };
 
+    // Run the regalloc checker, if requested.
+    if b.flags().regalloc_checker() {
+        let _tt = timing::regalloc_checker();
+        let mut checker = regalloc2::checker::Checker::new(&vcode, machine_env);
+        checker.prepare(&regalloc_result);
+        checker
+            .run()
+            .map_err(|err| {
+                log::error!(
+                    "Register allocation checker errors:\n{:?}\nfor vcode:\n{:?}",
+                    err,
+                    vcode
+                );
+                err
+            })
+            .expect("register allocation checker");
+    }
+
     Ok((vcode, regalloc_result))
 }

cranelift/codegen/src/settings.rs

@@ -515,6 +515,7 @@ tls_model = "none"
 libcall_call_conv = "isa_default"
 baldrdash_prologue_words = 0
 probestack_size_log2 = 12
+regalloc_checker = false
 enable_verifier = true
 is_pic = false
 use_colocated_libcalls = false

cranelift/codegen/src/timing.rs

@@ -65,6 +65,7 @@ define_passes! {
     vcode_emit_finish: "VCode emission finalization",
 
     regalloc: "Register allocation",
+    regalloc_checker: "Register allocation symbolic verification",
     binemit: "Binary machine code emission",
     layout_renumber: "Layout full renumbering",