Restore cross checking code, part 1 (#1575)

Restore the old cross checking code and update the transpiler so it passes CI.

Author: ahomescu

README.md

@@ -26,6 +26,8 @@ required to lift unsafe Rust into safe Rust types.
 However, we are building a [refactoring tool](c2rust-refactor) that reduces the tedium of doing so.
 This work is still in the early stages; please get in touch if you're interested!
 
+You can also [cross-check](cross-checks) the translated code against the original ([tutorial](docs/cross-check-tutorial.md)).
+
 Here's the big picture:
 
 ![C2Rust overview](docs/c2rust-overview.png "C2Rust overview")

c2rust-transpile/src/build_files/Cargo.toml.hbs

@@ -40,4 +40,18 @@ name = "{{name}}"
 {{/if}}
 {{/each}}
 
+{{#if cross_checks~}}
+[dependencies.c2rust-xcheck-plugin]
+version = "*"
+
+[dependencies.c2rust-xcheck-derive]
+version = "*"
+
+[dependencies.c2rust-xcheck-runtime]
+version = "*"
+features = ["libc-hash", "fixed-length-array-hash"]
+
+[dependencies.c2rust-xcheck-backend-{{cross_check_backend}}]
+version = "*"
+{{~/if}}
 {{~/if}}

c2rust-transpile/src/build_files/lib.rs.hbs

@@ -9,6 +9,16 @@
 extern crate {{this.ident}};
 {{~/each}}
 
+{{#if cross_checks~}}
+#![plugin(c2rust_xcheck_plugin({{plugin_args}}))]
+#[macro_use] extern crate c2rust_xcheck_derive;
+#[macro_use] extern crate c2rust_xcheck_runtime;
+extern crate c2rust_xcheck_backend_{{cross_check_backend}};
+
+#[global_allocator]
+static C2RUST_ALLOC: ::std::alloc::System = ::std::alloc::System;
+{{~/if}}
+
 {{#each modules~}}
 {{~#if this.path~}}
 #[path = "{{this.path}}"]

c2rust-transpile/src/build_files/mod.rs

@@ -250,13 +250,24 @@ fn emit_lib_rs(
     pragmas: PragmaSet,
     crates: &CrateSet,
 ) -> Option<PathBuf> {
+    let plugin_args = tcfg
+        .cross_check_configs
+        .iter()
+        .map(|ccc| format!("config_file = \"{}\"", ccc))
+        .collect::<Vec<String>>()
+        .join(", ");
+
     let modules = convert_module_list(tcfg, build_dir, modules, ModuleSubset::Libraries);
     let crates = convert_dependencies_list(crates.clone(), tcfg.c2rust_dir.as_deref());
     let file_name = get_lib_rs_file_name(tcfg);
+    let rs_xcheck_backend = tcfg.cross_check_backend.replace("-", "_");
     let json = json!({
         "lib_rs_file": file_name,
         "reorganize_definitions": tcfg.reorganize_definitions,
         "translate_valist": tcfg.translate_valist,
+        "cross_checks": tcfg.cross_checks,
+        "cross_check_backend": rs_xcheck_backend,
+        "plugin_args": plugin_args,
         "modules": modules,
         "pragmas": pragmas,
         "crates": crates,
@@ -311,6 +322,8 @@ fn emit_cargo_toml<'lcmd>(
             "is_library": ccfg.link_cmd.r#type.is_library(),
             "lib_rs_file": get_lib_rs_file_name(tcfg),
             "binaries": binaries,
+            "cross_checks": tcfg.cross_checks,
+            "cross_check_backend": tcfg.cross_check_backend,
             "dependencies": dependencies,
         });
         json.as_object_mut().unwrap().extend(

c2rust-transpile/src/lib.rs

@@ -79,6 +79,9 @@ pub struct TranspilerConfig {
     pub fail_on_multiple: bool,
     pub filter: Option<Regex>,
     pub debug_relooper_labels: bool,
+    pub cross_checks: bool,
+    pub cross_check_backend: String,
+    pub cross_check_configs: Vec<String>,
     pub prefix_function_names: Option<String>,
     pub translate_asm: bool,
     pub use_c_loop_info: bool,

c2rust-transpile/src/translator/main_function.rs

@@ -299,7 +299,8 @@ impl<'c> Translation<'c> {
             };
 
             let block = mk().block(stmts);
-            Ok(mk().pub_().fn_item(decl, block))
+            let main_attributes = self.mk_cross_check(mk(), vec!["none"]);
+            Ok(main_attributes.pub_().fn_item(decl, block))
         } else {
             Err(TranslationError::generic(
                 "Cannot translate non-function main entry point",

c2rust-transpile/src/translator/mod.rs

@@ -1228,6 +1228,20 @@ fn arrange_header(t: &Translation, is_binary: bool) -> (Vec<syn::Attribute>, Vec
             out_attrs.push(attr);
         }
 
+        if t.tcfg.cross_checks {
+            let xcheck_plugin_args = t
+                .tcfg
+                .cross_check_configs
+                .iter()
+                .map(|config_file| mk().meta_namevalue("config_file", mk().str_lit(config_file)))
+                .collect::<Vec<_>>();
+            let xcheck_plugin_item = mk().meta_list("c2rust_xcheck_plugin", xcheck_plugin_args);
+            let plugin_args = vec![xcheck_plugin_item];
+            let plugin_item = mk().meta_list("plugin", plugin_args);
+            let attr = mk().attribute(AttrStyle::Inner(Default::default()), plugin_item);
+            out_attrs.push(attr);
+        }
+
         if t.tcfg.emit_no_std {
             let meta = mk().meta_path("no_std");
             let attr = mk().attribute(AttrStyle::Inner(Default::default()), meta);
@@ -1247,6 +1261,24 @@ fn arrange_header(t: &Translation, is_binary: bool) -> (Vec<syn::Attribute>, Vec
                 }
             }
 
+            if t.tcfg.cross_checks {
+                out_items.push(
+                    mk().single_attr("macro_use")
+                        .extern_crate_item("c2rust_xcheck_derive", None),
+                );
+                out_items.push(
+                    mk().single_attr("macro_use")
+                        .extern_crate_item("c2rust_xcheck_runtime", None),
+                );
+                // When cross-checking, always use the system allocator
+                let sys_alloc_path = vec!["", "std", "alloc", "System"];
+                out_items.push(mk().single_attr("global_allocator").static_item(
+                    "C2RUST_ALLOC",
+                    mk().path_ty(sys_alloc_path.clone()),
+                    mk().path_expr(sys_alloc_path),
+                ));
+            }
+
             // TODO: switch to `#[expect(unused_imports, reason = ...)]` once
             // we upgrade to a newer nightly (Rust 1.81) that supports it.
             out_items.push(
@@ -1432,6 +1464,10 @@ impl<'c> Translation<'c> {
                 "unused_assignments",
             ],
         )];
+        if self.tcfg.cross_checks {
+            features.append(&mut vec!["plugin"]);
+            pragmas.push(("cross_check", vec!["yes"]));
+        }
 
         if self.features.borrow().contains("register_tool") {
             pragmas.push(("register_tool", vec!["c2rust"]));
@@ -1465,6 +1501,14 @@ impl<'c> Translation<'c> {
         ))
     }
 
+    fn mk_cross_check(&self, mk: Builder, args: Vec<&str>) -> Builder {
+        if self.tcfg.cross_checks {
+            mk.call_attr("cross_check", args)
+        } else {
+            mk
+        }
+    }
+
     fn static_initializer_is_unsafe(&self, expr_id: Option<CExprId>, qty: CQualTypeId) -> bool {
         // SIMD types are always unsafe in statics
         match self.ast_context.resolve_type(qty.ctype).kind {
@@ -1660,7 +1704,11 @@ impl<'c> Translation<'c> {
         let fn_decl = mk().fn_decl(fn_name.clone(), vec![], None, fn_ty.clone());
         let fn_bare_decl = (vec![], None, fn_ty);
         let fn_block = mk().block(sectioned_static_initializers);
-        let fn_item = mk().unsafe_().extern_("C").fn_item(fn_decl, fn_block);
+        let fn_attributes = self.mk_cross_check(mk(), vec!["none"]);
+        let fn_item = fn_attributes
+            .unsafe_()
+            .extern_("C")
+            .fn_item(fn_decl, fn_block);
 
         let static_attributes = mk()
             .single_attr("used")
@@ -2418,7 +2466,10 @@ impl<'c> Translation<'c> {
 
                 // Only add linkage attributes if the function is `extern`
                 let mut mk_ = if is_main {
-                    mk()
+                    // Cross-check this function as if it was called `main`
+                    // FIXME: pass in a vector of NestedMetaItem elements,
+                    // but strings have to do for now
+                    self.mk_cross_check(mk(), vec!["entry(djb2=\"main\")", "exit(djb2=\"main\")"])
                 } else if (is_global && !is_inline) || is_extern_inline {
                     mk_linkage(false, new_name, name).extern_("C").pub_()
                 } else if self.cur_file.get().is_some() {

c2rust-transpile/tests/snapshots.rs

@@ -22,6 +22,9 @@ fn config() -> TranspilerConfig {
         fail_on_multiple: false,
         filter: None,
         debug_relooper_labels: false,
+        cross_checks: false,
+        cross_check_backend: Default::default(),
+        cross_check_configs: Default::default(),
         prefix_function_names: None,
         translate_asm: true,
         use_c_loop_info: true,

c2rust/src/bin/c2rust-transpile.rs

@@ -170,6 +170,15 @@ struct Args {
     /// Fail when the control-flow graph generates branching constructs
     #[clap(long)]
     fail_on_multiple: bool,
+
+    #[clap(long, short = 'x')]
+    cross_checks: bool,
+
+    #[clap(long, short = 'X', multiple = true)]
+    cross_check_config: Vec<String>,
+
+    #[clap(long, value_enum, default_value_t)]
+    cross_check_backend: CrossCheckBackend,
 }
 
 // TODO Eventually move this code into `c2rust-transpile`
@@ -200,6 +209,30 @@ impl From<TranslateMacros> for c2rust_transpile::TranslateMacros {
     }
 }
 
+#[derive(Default, Debug, ValueEnum, Clone)]
+pub enum CrossCheckBackend {
+    DynamicDlsym,
+
+    #[default]
+    ZstdLogging,
+
+    LibclevrbufSys,
+
+    LibfakechecksSys,
+}
+
+impl From<CrossCheckBackend> for String {
+    fn from(x: CrossCheckBackend) -> String {
+        let s = match x {
+            CrossCheckBackend::DynamicDlsym => "dynamic-dlsym",
+            CrossCheckBackend::ZstdLogging => "zstd-logging",
+            CrossCheckBackend::LibclevrbufSys => "libclevrbuf-sys",
+            CrossCheckBackend::LibfakechecksSys => "libfakechecks-sys",
+        };
+        s.to_string()
+    }
+}
+
 #[derive(Debug, PartialEq, Eq, ValueEnum, Clone)]
 #[clap(rename_all = "snake_case")]
 enum InvalidCodes {
@@ -228,6 +261,9 @@ fn main() {
         fail_on_multiple: args.fail_on_multiple,
         filter: args.filter,
         debug_relooper_labels: args.debug_labels,
+        cross_checks: args.cross_checks,
+        cross_check_backend: args.cross_check_backend.into(),
+        cross_check_configs: args.cross_check_config,
         prefix_function_names: args.prefix_function_names,
 
         // We used to guard asm translation with a command-line

cross-checks/README.md

@@ -0,0 +1,11 @@
+This is the top-level directory for all cross-checking components, and contains the following:
+
+ * A clang plugin that automatically inserts cross-check instrumentation into C code.
+ 
+ * An equivalent rustc compiler plugin for Rust.
+ 
+ * The `libfakechecks` cross-checking backend library that prints out all cross-checks to standard output.
+ This library is supported by both the C and Rust compiler plugins.
+ 
+ * Our experimental fork of the `ReMon` MVEE modified for C/Rust side-by-side checking,
+ along with the `mvee-configs` directory that contains some MVEE configuration examples.