Introduce rmc::proof function attribute (rust-lang#668)

* Introduce rmc::proof function attribute

* add no_mangle as temporary measure to force function codegen

Cargo.lock

@@ -3342,6 +3342,9 @@ dependencies = [
 [[package]]
 name = "rmc"
 version = "0.1.0"
+dependencies = [
+ "rmc_macros",
+]
 
 [[package]]
 name = "rmc-link-restrictions"
@@ -3353,6 +3356,10 @@ dependencies = [
  "serde_json",
 ]
 
+[[package]]
+name = "rmc_macros"
+version = "0.1.0"
+
 [[package]]
 name = "rmc_restrictions"
 version = "0.1.0"

compiler/cbmc/src/goto_program/location.rs

@@ -32,6 +32,20 @@ impl Location {
         }
     }
 
+    pub fn filename(&self) -> Option<String> {
+        match self {
+            Location::Loc { file, .. } => Some(file.to_string()),
+            _ => None,
+        }
+    }
+
+    pub fn line(&self) -> Option<u64> {
+        match self {
+            Location::Loc { line, .. } => Some(*line),
+            _ => 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.handle_rmctool_attributes();
         }
         self.reset_current_fn();
     }
@@ -199,4 +203,49 @@ 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_macros translates to `#[rmctool::proof]` for us to handle here)
+    fn handle_rmctool_attributes(&mut self) {
+        let instance = self.current_fn().instance();
+
+        for attr in self.tcx.get_attrs(instance.def_id()) {
+            match rmctool_attr_name(attr).as_deref() {
+                Some("proof") => self.handle_rmctool_proof(),
+                _ => {}
+            }
+        }
+    }
+
+    /// Update `self` (the goto context) to add the current function as a listed proof harness
+    fn handle_rmctool_proof(&mut self) {
+        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(),
+            original_line: loc.line().unwrap().to_string(),
+        };
+
+        self.proof_harnesses.push(harness);
+    }
+}
+
+/// If the attribute is named `rmctool::name`, this extracts `name`
+fn rmctool_attr_name(attr: &ast::Attribute) -> Option<String> {
+    match &attr.kind {
+        ast::AttrKind::Normal(ast::AttrItem { path: ast::Path { segments, .. }, .. }, _)
+            if segments.len() == 2 && segments[0].ident.as_str() == "rmctool" =>
+        {
+            Some(segments[1].ident.as_str().to_string())
+        }
+        _ => None,
+    }
 }

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;
@@ -29,9 +29,10 @@ use tracing::{debug, warn};
 
 // #[derive(RustcEncodable, RustcDecodable)]
 pub struct GotocCodegenResult {
-    pub type_map: BTreeMap<InternedString, InternedString>,
-    pub symtab: SymbolTable,
     pub crate_name: rustc_span::Symbol,
+    pub metadata: RmcMetadata,
+    pub symtab: SymbolTable,
+    pub type_map: BTreeMap<InternedString, InternedString>,
     pub vtable_restrictions: Option<VtableCtxResults>,
 }
 
@@ -128,7 +129,7 @@ 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,
         );
@@ -144,11 +145,14 @@ impl CodegenBackend for GotocCodegenBackend {
             None
         };
 
+        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,
-            vtable_restrictions: vtable_restrictions,
+            metadata,
+            symtab,
+            type_map,
+            vtable_restrictions,
         })
     }
 
@@ -176,7 +180,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);
             // If they exist, write out vtable virtual call function pointer restrictions
             if let Some(restrictions) = result.vtable_restrictions {
                 write_file(&base_filename, "restrictions.json", &restrictions);

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 super::vtable_ctx::VtableCtx;
 use crate::overrides::{fn_hooks, GotocHooks};
 use crate::utils::full_crate_name;
@@ -53,6 +54,7 @@ pub struct GotocCtx<'tcx> {
     pub vtable_ctx: VtableCtx,
     pub current_fn: Option<CurrentFnCtx<'tcx>>,
     pub type_map: FxHashMap<InternedString, Ty<'tcx>>,
+    pub proof_harnesses: Vec<HarnessMetadata>,
 }
 
 /// Constructor
@@ -72,6 +74,7 @@ impl<'tcx> GotocCtx<'tcx> {
             vtable_ctx: VtableCtx::new(emit_vtable_restrictions),
             current_fn: None,
             type_map: FxHashMap::default(),
+            proof_harnesses: vec![],
         }
     }
 }

compiler/rustc_codegen_rmc/src/context/metadata.rs

@@ -0,0 +1,26 @@
+// 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 line in that file where the proof harness begins
+    pub original_line: 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,6 +8,7 @@
 
 mod current_fn;
 mod goto_ctx;
+pub mod metadata;
 mod vtable_ctx;
 
 pub use goto_ctx::GotocCtx;

library/rmc/Cargo.toml

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

library/rmc/src/lib.rs

@@ -53,3 +53,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_macros::*;

library/rmc_macros/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_macros"
+version = "0.1.0"
+edition = "2018"
+license = "MIT OR Apache-2.0"
+
+[lib]
+proc-macro = true
+
+[dependencies]

library/rmc_macros/src/lib.rs

@@ -0,0 +1,51 @@
+// 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(all(not(rmc), not(test)))]
+#[proc_macro_attribute]
+pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    // Not-RMC, Not-Test means this code shouldn't exist, return nothing.
+    TokenStream::new()
+}
+
+#[cfg(all(not(rmc), test))]
+#[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());
+    // no_mangle is a temporary hack to make the function "public" so it gets codegen'd
+    result.extend("#[no_mangle]".parse::<TokenStream>().unwrap());
+    result.extend(item);
+    result
+    // quote!(
+    //     #[rmctool::proof]
+    //     $item
+    // )
+}

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_MACRO_LIB_PATH
+    local MACRO_LIB_CANDIDATE=(${RMC_LIB_PATH}/deps/librmc_macros-*)
+    if [[ ${#MACRO_LIB_CANDIDATE[@]} -ne 1 ]]
+    then
+        echo "ERROR: Could not find RMC library."
+        echo "Looked for: \"${RMC_LIB_PATH}/deps/librmc_macros-*\""
+        echo "Was RMC library successfully built first?"
+        exit 1
+    fi
+    RMC_MACRO_LIB_PATH="${MACRO_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 librmc_macros=${RMC_MACRO_LIB_PATH} \
+            "
     if [ "${1:-''}" == "--rmc-flags" ]
     then
         echo ${RMC_FLAGS}

scripts/rmc.py

@@ -227,6 +227,7 @@ def compile_single_rust_file(
     if not extra_args.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(extra_args.mangler, symbol_table_passes,
                                               extra_args.restrict_vtable)

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" $@
 

src/test/cargo-rmc/simple-proof-annotation/Cargo.toml

@@ -0,0 +1,9 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "simple-proof-annotation"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

src/test/cargo-rmc/simple-proof-annotation/main.expected

@@ -0,0 +1 @@
+line 5 assertion failed: 1 == 2: FAILURE

src/test/cargo-rmc/simple-proof-annotation/src/main.rs

@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    assert!(1 == 2);
+}
+
+// NOTE: Currently the below is not detected or run by this test!
+
+// The expected file presently looks for "1 == 2" above.
+// But eventually this test may start to fail as we might stop regarding 'main'
+// as a valid proof harness, since it isn't annotated as such.
+// This test should be updated if we go that route.
+
+#[rmc::proof]
+fn harness() {
+    assert!(3 == 4);
+}