Introduce rmc::proof function attribute

Cargo.lock

@@ -3341,6 +3341,13 @@ dependencies = [
 [[package]]
 name = "rmc"
 version = "0.1.0"
+dependencies = [
+ "rmc-annotations",
+]
+
+[[package]]
+name = "rmc-annotations"
+version = "0.1.0"
 
 [[package]]
 name = "rust-demangler"

compiler/cbmc/src/goto_program/location.rs

@@ -32,6 +32,13 @@ impl Location {
         }
     }
 
+    pub fn filename(&self) -> Option<String> {
+        match self {
+            Location::Loc { file, .. } => Some(file.to_string()),
+            _ => None,
+        }
+    }
+
     /// Convert a location to a short string suitable for (e.g.) logging.
     /// Goal is to return just "file:line" as clearly as possible.
     pub fn short_string(&self) -> String {

compiler/rustc_codegen_rmc/src/codegen/function.rs

@@ -3,8 +3,10 @@
 
 //! This file contains functions related to codegenning MIR functions into gotoc
 
+use crate::context::metadata::HarnessMetadata;
 use crate::GotocCtx;
 use cbmc::goto_program::{Expr, Stmt, Symbol};
+use rustc_ast::ast;
 use rustc_middle::mir::{HasLocalDecls, Local};
 use rustc_middle::ty::{self, Instance, TyS};
 use tracing::{debug, warn};
@@ -98,6 +100,8 @@ impl<'tcx> GotocCtx<'tcx> {
             let stmts = self.current_fn_mut().extract_block();
             let body = Stmt::block(stmts, loc);
             self.symbol_table.update_fn_declaration_with_definition(&name, body);
+
+            self.codegen_rmctool_attributes();
         }
         self.reset_current_fn();
     }
@@ -199,4 +203,41 @@ impl<'tcx> GotocCtx<'tcx> {
         });
         self.reset_current_fn();
     }
+
+    /// This updates the goto context with any information that should be accumulated from a function's
+    /// attributes.
+    ///
+    /// Currently, this is only proof harness annotations.
+    /// i.e. `#[rmc::proof]` (which rmc-annotations translates to `#[rmctool::proof]` for us to handle here)
+    fn codegen_rmctool_attributes(&mut self) {
+        let instance = self.current_fn().instance();
+
+        for attr in self.tcx.get_attrs(instance.def_id()) {
+            if matches_rmctool_attr(attr, "proof") {
+                let current_fn = self.current_fn();
+                let pretty_name = current_fn.readable_name().to_owned();
+                let mangled_name = current_fn.name();
+                let loc = self.codegen_span(&current_fn.mir().span);
+
+                let harness = HarnessMetadata {
+                    pretty_name,
+                    mangled_name,
+                    original_file: loc.filename().unwrap(),
+                };
+
+                self.proof_harnesses.push(harness);
+            }
+        }
+    }
+}
+
+fn matches_rmctool_attr(attr: &ast::Attribute, name: &str) -> bool {
+    match &attr.kind {
+        ast::AttrKind::Normal(ast::AttrItem { path: ast::Path { segments, .. }, .. }, _) => {
+            segments.len() == 2
+                && segments[0].ident.as_str() == "rmctool"
+                && segments[1].ident.as_str() == name
+        }
+        _ => false,
+    }
 }

compiler/rustc_codegen_rmc/src/compiler_interface.rs

@@ -3,8 +3,8 @@
 
 //! This file contains the code necessary to interface with the compiler backend
 
+use crate::context::metadata::RmcMetadata;
 use crate::GotocCtx;
-
 use bitflags::_core::any::Any;
 use cbmc::goto_program::symtab_transformer;
 use cbmc::goto_program::SymbolTable;
@@ -27,9 +27,10 @@ use tracing::{debug, warn};
 
 // #[derive(RustcEncodable, RustcDecodable)]
 pub struct GotocCodegenResult {
-    pub type_map: BTreeMap<String, String>,
-    pub symtab: SymbolTable,
     pub crate_name: rustc_span::Symbol,
+    pub metadata: RmcMetadata,
+    pub symtab: SymbolTable,
+    pub type_map: BTreeMap<String, String>,
 }
 
 #[derive(Clone)]
@@ -125,17 +126,20 @@ impl CodegenBackend for GotocCodegenBackend {
         }
 
         // perform post-processing symbol table passes
-        let symbol_table = symtab_transformer::do_passes(
+        let symtab = symtab_transformer::do_passes(
             c.symbol_table,
             &tcx.sess.opts.debugging_opts.symbol_table_passes,
         );
 
         let type_map = BTreeMap::from_iter(c.type_map.into_iter().map(|(k, v)| (k, v.to_string())));
 
+        let metadata = RmcMetadata { proof_harnesses: c.proof_harnesses };
+
         Box::new(GotocCodegenResult {
-            type_map,
-            symtab: symbol_table,
             crate_name: tcx.crate_name(LOCAL_CRATE) as rustc_span::Symbol,
+            metadata,
+            symtab,
+            type_map,
         })
     }
 
@@ -163,6 +167,7 @@ impl CodegenBackend for GotocCodegenBackend {
             let base_filename = outputs.path(OutputType::Object);
             write_file(&base_filename, "symtab.json", &result.symtab);
             write_file(&base_filename, "type_map.json", &result.type_map);
+            write_file(&base_filename, "rmc-metadata.json", &result.metadata);
         }
 
         Ok(())

compiler/rustc_codegen_rmc/src/context/goto_ctx.rs

@@ -14,6 +14,7 @@
 //! Any MIR specific functionality (e.g. codegen etc) should live in specialized files that use
 //! this structure as input.
 use super::current_fn::CurrentFnCtx;
+use super::metadata::HarnessMetadata;
 use crate::overrides::{fn_hooks, GotocHooks};
 use crate::utils::full_crate_name;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type};
@@ -50,6 +51,7 @@ pub struct GotocCtx<'tcx> {
     pub alloc_map: FxHashMap<&'tcx Allocation, String>,
     pub current_fn: Option<CurrentFnCtx<'tcx>>,
     pub type_map: FxHashMap<String, Ty<'tcx>>,
+    pub proof_harnesses: Vec<HarnessMetadata>,
 }
 
 /// Constructor
@@ -67,6 +69,7 @@ impl<'tcx> GotocCtx<'tcx> {
             alloc_map: FxHashMap::default(),
             current_fn: None,
             type_map: FxHashMap::default(),
+            proof_harnesses: vec![],
         }
     }
 }

compiler/rustc_codegen_rmc/src/context/metadata.rs

@@ -0,0 +1,24 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module should be factored out into its own separate crate eventually,
+//! but leaving it here for now...
+
+use serde::Serialize;
+
+/// We emit this structure for each annotated proof harness we find
+#[derive(Serialize)]
+pub struct HarnessMetadata {
+    /// The name the user gave to the function
+    pub pretty_name: String,
+    /// The name of the function in the CBMC symbol table
+    pub mangled_name: String,
+    /// The (currently full-) path to the file this proof harness was declared within
+    pub original_file: String,
+}
+
+/// The structure of `.rmc-metadata.json` files, which are emitted for each crate
+#[derive(Serialize)]
+pub struct RmcMetadata {
+    pub proof_harnesses: Vec<HarnessMetadata>,
+}

compiler/rustc_codegen_rmc/src/context/mod.rs

@@ -8,5 +8,6 @@
 
 mod current_fn;
 mod goto_ctx;
+pub mod metadata;
 
 pub use goto_ctx::GotocCtx;

library/rmc-annotations/Cargo.toml

@@ -0,0 +1,13 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "rmc-annotations"
+version = "0.1.0"
+edition = "2018"
+license = "MIT OR Apache-2.0"
+
+[lib]
+proc-macro = true
+
+[dependencies]

library/rmc-annotations/src/lib.rs

@@ -0,0 +1,42 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// #![feature(register_tool)]
+// #![register_tool(rmctool)]
+// Frustratingly, it's not enough for our crate to enable these features, because we need all
+// downstream crates to enable these features as well.
+// So we have to enable this on the commandline (see rmc-rustc) with:
+//   RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rmctool)"
+
+// proc_macro::quote is nightly-only, so we'll cobble things together instead
+use proc_macro::TokenStream;
+
+#[cfg(not(rmc))]
+#[proc_macro_attribute]
+pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    // Leave the code intact, so it can be easily be edited in an IDE,
+    // but outside RMC, this code is likely never called.
+    let mut result = TokenStream::new();
+
+    result.extend("#[allow(dead_code)]".parse::<TokenStream>().unwrap());
+    result.extend(item);
+    result
+    // quote!(
+    //     #[allow(dead_code)]
+    //     $item
+    // )
+}
+
+#[cfg(rmc)]
+#[proc_macro_attribute]
+pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    let mut result = TokenStream::new();
+
+    result.extend("#[rmctool::proof]".parse::<TokenStream>().unwrap());
+    result.extend(item);
+    result
+    // quote!(
+    //     #[rmctool::proof]
+    //     $item
+    // )
+}

library/rmc/Cargo.toml

@@ -8,3 +8,4 @@ edition = "2018"
 license = "MIT OR Apache-2.0"
 
 [dependencies]
+rmc-annotations = { path = "../rmc-annotations" }

library/rmc/src/lib.rs

@@ -51,3 +51,6 @@ pub fn nondet<T>() -> T {
 #[inline(never)]
 #[rustc_diagnostic_item = "RmcExpectFail"]
 pub fn expect_fail(_cond: bool, _message: &str) {}
+
+/// RMC proc macros must be in a separate crate
+pub use rmc_annotations::*;

scripts/rmc-rustc

@@ -45,6 +45,16 @@ set_rmc_lib_path() {
         fi
         RMC_LIB_PATH=$(dirname ${RMC_LIB_CANDIDATES[0]})
     fi
+    # Having set RMC_LIB_PATH, find RMC_ANNO_LIB_PATH
+    local ANNO_LIB_CANDIDATE=(${RMC_LIB_PATH}/deps/librmc_annotations-*)
+    if [[ ${#ANNO_LIB_CANDIDATE[@]} -ne 1 ]]
+    then
+        echo "ERROR: Could not find RMC library."
+        echo "Looked for: \"${RMC_LIB_PATH}/deps/librmc_annotations-*\""
+        echo "Was RMC library successfully built first?"
+        exit 1
+    fi
+    RMC_ANNO_LIB_PATH="${ANNO_LIB_CANDIDATE[0]}"
 }
 
 set_rmc_path
@@ -58,8 +68,13 @@ else
             -Z trim-diagnostic-paths=no \
             -Z human_readable_cgu_names \
             --cfg=rmc \
+            -Zcrate-attr=feature(register_tool) \
+            -Zcrate-attr=register_tool(rmctool) \
             -L ${RMC_LIB_PATH} \
-            --extern rmc"
+            --extern rmc \
+            -L ${RMC_LIB_PATH}/deps \
+            --extern rmc_annotations=${RMC_ANNO_LIB_PATH} \
+            "
     if [ "${1:-''}" == "--rmc-flags" ]
     then
         echo ${RMC_FLAGS}

scripts/rmc.py

@@ -224,6 +224,7 @@ def compile_single_rust_file(
     if not keep_temps:
         atexit.register(delete_file, output_filename)
         atexit.register(delete_file, base + ".type_map.json")
+        atexit.register(delete_file, base + ".rmc-metadata.json")
 
     build_cmd = [RMC_RUSTC_EXE] + rustc_flags(mangler, symbol_table_passes)
 

scripts/setup/build_rmc_lib.sh

@@ -10,6 +10,7 @@ SCRIPTS_DIR="$(dirname $SCRIPT_DIR)"
 REPO_DIR="$(dirname $SCRIPTS_DIR)"
 
 export RUSTC=$(${SCRIPTS_DIR}/rmc-rustc --rmc-path)
+export RUSTFLAGS="--cfg rmc"
 cargo clean --manifest-path "${REPO_DIR}/library/rmc/Cargo.toml" $@
 cargo build --manifest-path "${REPO_DIR}/library/rmc/Cargo.toml" $@