Introduce rmc::proof function attribute (#668)

* Introduce rmc::proof function attribute

* add no_mangle as temporary measure to force function codegen

Author: tedinski

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]