From 1502f02aff75c5cd83642396bafae7f9efce166a Mon Sep 17 00:00:00 2001
From: Ted Kaminski <tedinski@amazon.com>
Date: Wed, 24 Nov 2021 02:08:56 +0000
Subject: [PATCH 1/7] Introduce rmc::proof function attribute

---
 Cargo.lock                                    |  7 ++++
 compiler/cbmc/src/goto_program/location.rs    |  7 ++++
 .../rustc_codegen_rmc/src/codegen/function.rs | 41 ++++++++++++++++++
 .../src/compiler_interface.rs                 | 17 +++++---
 .../rustc_codegen_rmc/src/context/goto_ctx.rs |  3 ++
 .../rustc_codegen_rmc/src/context/metadata.rs | 24 +++++++++++
 compiler/rustc_codegen_rmc/src/context/mod.rs |  1 +
 library/rmc-annotations/Cargo.toml            | 13 ++++++
 library/rmc-annotations/src/lib.rs            | 42 +++++++++++++++++++
 library/rmc/Cargo.toml                        |  1 +
 library/rmc/src/lib.rs                        |  3 ++
 scripts/rmc-rustc                             | 17 +++++++-
 scripts/rmc.py                                |  1 +
 scripts/setup/build_rmc_lib.sh                |  1 +
 14 files changed, 171 insertions(+), 7 deletions(-)
 create mode 100644 compiler/rustc_codegen_rmc/src/context/metadata.rs
 create mode 100644 library/rmc-annotations/Cargo.toml
 create mode 100644 library/rmc-annotations/src/lib.rs

diff --git a/Cargo.lock b/Cargo.lock
index f28d1ff8934c..2511ad198f1a 100644
--- a/Cargo.lock
+++ b/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"
diff --git a/compiler/cbmc/src/goto_program/location.rs b/compiler/cbmc/src/goto_program/location.rs
index e08a0fefd979..37fd9fc1e832 100644
--- a/compiler/cbmc/src/goto_program/location.rs
+++ b/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 {
diff --git a/compiler/rustc_codegen_rmc/src/codegen/function.rs b/compiler/rustc_codegen_rmc/src/codegen/function.rs
index b57751f71dc1..5a8858fc7130 100644
--- a/compiler/rustc_codegen_rmc/src/codegen/function.rs
+++ b/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,
+    }
 }
diff --git a/compiler/rustc_codegen_rmc/src/compiler_interface.rs b/compiler/rustc_codegen_rmc/src/compiler_interface.rs
index 144aa2116a6c..b62870aa4d10 100644
--- a/compiler/rustc_codegen_rmc/src/compiler_interface.rs
+++ b/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(())
diff --git a/compiler/rustc_codegen_rmc/src/context/goto_ctx.rs b/compiler/rustc_codegen_rmc/src/context/goto_ctx.rs
index 717a32e1d069..416c65e1033e 100644
--- a/compiler/rustc_codegen_rmc/src/context/goto_ctx.rs
+++ b/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![],
         }
     }
 }
diff --git a/compiler/rustc_codegen_rmc/src/context/metadata.rs b/compiler/rustc_codegen_rmc/src/context/metadata.rs
new file mode 100644
index 000000000000..8f18b995ce05
--- /dev/null
+++ b/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>,
+}
diff --git a/compiler/rustc_codegen_rmc/src/context/mod.rs b/compiler/rustc_codegen_rmc/src/context/mod.rs
index 019ebae95b8a..8aa6d4d2ca77 100644
--- a/compiler/rustc_codegen_rmc/src/context/mod.rs
+++ b/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;
diff --git a/library/rmc-annotations/Cargo.toml b/library/rmc-annotations/Cargo.toml
new file mode 100644
index 000000000000..78b6fcd4efa7
--- /dev/null
+++ b/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]
diff --git a/library/rmc-annotations/src/lib.rs b/library/rmc-annotations/src/lib.rs
new file mode 100644
index 000000000000..eb081cc0f5d7
--- /dev/null
+++ b/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
+    // )
+}
diff --git a/library/rmc/Cargo.toml b/library/rmc/Cargo.toml
index 32a76e76b345..bf10fac23c34 100644
--- a/library/rmc/Cargo.toml
+++ b/library/rmc/Cargo.toml
@@ -8,3 +8,4 @@ edition = "2018"
 license = "MIT OR Apache-2.0"
 
 [dependencies]
+rmc-annotations = { path = "../rmc-annotations" }
diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs
index 631f1a372967..784ce560fbf7 100644
--- a/library/rmc/src/lib.rs
+++ b/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::*;
diff --git a/scripts/rmc-rustc b/scripts/rmc-rustc
index 8d981fed5dd2..db5345f5ebb0 100755
--- a/scripts/rmc-rustc
+++ b/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}
diff --git a/scripts/rmc.py b/scripts/rmc.py
index 964caf7ca7a3..3c1461f8106b 100644
--- a/scripts/rmc.py
+++ b/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)
 
diff --git a/scripts/setup/build_rmc_lib.sh b/scripts/setup/build_rmc_lib.sh
index 1ef3d8cddd4c..4f801e68e48c 100755
--- a/scripts/setup/build_rmc_lib.sh
+++ b/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" $@
 

From ee317eaeef40606c6bef37af3ebc0d4c28c3ad04 Mon Sep 17 00:00:00 2001
From: Ted Kaminski <tedinski@amazon.com>
Date: Wed, 1 Dec 2021 01:34:50 +0000
Subject: [PATCH 2/7] rename crate to 'rmc_macros'

---
 Cargo.lock                                         | 10 +++++-----
 compiler/rustc_codegen_rmc/src/codegen/function.rs |  2 +-
 library/rmc/Cargo.toml                             |  2 +-
 library/rmc/src/lib.rs                             |  2 +-
 library/{rmc-annotations => rmc_macros}/Cargo.toml |  2 +-
 library/{rmc-annotations => rmc_macros}/src/lib.rs |  0
 scripts/rmc-rustc                                  | 12 ++++++------
 7 files changed, 15 insertions(+), 15 deletions(-)
 rename library/{rmc-annotations => rmc_macros}/Cargo.toml (90%)
 rename library/{rmc-annotations => rmc_macros}/src/lib.rs (100%)

diff --git a/Cargo.lock b/Cargo.lock
index cb9a043bc148..25ee54321fa4 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -3342,13 +3342,9 @@ dependencies = [
 name = "rmc"
 version = "0.1.0"
 dependencies = [
- "rmc-annotations",
+ "rmc_macros",
 ]
 
-[[package]]
-name = "rmc-annotations"
-version = "0.1.0"
-
 [[package]]
 name = "rmc-link-restrictions"
 version = "0.1.0"
@@ -3359,6 +3355,10 @@ dependencies = [
  "serde_json",
 ]
 
+[[package]]
+name = "rmc_macros"
+version = "0.1.0"
+
 [[package]]
 name = "rmc_restrictions"
 version = "0.1.0"
diff --git a/compiler/rustc_codegen_rmc/src/codegen/function.rs b/compiler/rustc_codegen_rmc/src/codegen/function.rs
index 5a8858fc7130..3d0d0b9d799c 100644
--- a/compiler/rustc_codegen_rmc/src/codegen/function.rs
+++ b/compiler/rustc_codegen_rmc/src/codegen/function.rs
@@ -208,7 +208,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// attributes.
     ///
     /// Currently, this is only proof harness annotations.
-    /// i.e. `#[rmc::proof]` (which rmc-annotations translates to `#[rmctool::proof]` for us to handle here)
+    /// i.e. `#[rmc::proof]` (which rmc_macros translates to `#[rmctool::proof]` for us to handle here)
     fn codegen_rmctool_attributes(&mut self) {
         let instance = self.current_fn().instance();
 
diff --git a/library/rmc/Cargo.toml b/library/rmc/Cargo.toml
index bf10fac23c34..8f3f764140f1 100644
--- a/library/rmc/Cargo.toml
+++ b/library/rmc/Cargo.toml
@@ -8,4 +8,4 @@ edition = "2018"
 license = "MIT OR Apache-2.0"
 
 [dependencies]
-rmc-annotations = { path = "../rmc-annotations" }
+rmc_macros = { path = "../rmc_macros" }
diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs
index 784ce560fbf7..73fc51542484 100644
--- a/library/rmc/src/lib.rs
+++ b/library/rmc/src/lib.rs
@@ -53,4 +53,4 @@ pub fn nondet<T>() -> T {
 pub fn expect_fail(_cond: bool, _message: &str) {}
 
 /// RMC proc macros must be in a separate crate
-pub use rmc_annotations::*;
+pub use rmc_macros::*;
diff --git a/library/rmc-annotations/Cargo.toml b/library/rmc_macros/Cargo.toml
similarity index 90%
rename from library/rmc-annotations/Cargo.toml
rename to library/rmc_macros/Cargo.toml
index 78b6fcd4efa7..bd8f791b8030 100644
--- a/library/rmc-annotations/Cargo.toml
+++ b/library/rmc_macros/Cargo.toml
@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [package]
-name = "rmc-annotations"
+name = "rmc_macros"
 version = "0.1.0"
 edition = "2018"
 license = "MIT OR Apache-2.0"
diff --git a/library/rmc-annotations/src/lib.rs b/library/rmc_macros/src/lib.rs
similarity index 100%
rename from library/rmc-annotations/src/lib.rs
rename to library/rmc_macros/src/lib.rs
diff --git a/scripts/rmc-rustc b/scripts/rmc-rustc
index db5345f5ebb0..fd2a6168828c 100755
--- a/scripts/rmc-rustc
+++ b/scripts/rmc-rustc
@@ -45,16 +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 ]]
+    # 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_annotations-*\""
+        echo "Looked for: \"${RMC_LIB_PATH}/deps/librmc_macros-*\""
         echo "Was RMC library successfully built first?"
         exit 1
     fi
-    RMC_ANNO_LIB_PATH="${ANNO_LIB_CANDIDATE[0]}"
+    RMC_MACRO_LIB_PATH="${MACRO_LIB_CANDIDATE[0]}"
 }
 
 set_rmc_path
@@ -73,7 +73,7 @@ else
             -L ${RMC_LIB_PATH} \
             --extern rmc \
             -L ${RMC_LIB_PATH}/deps \
-            --extern rmc_annotations=${RMC_ANNO_LIB_PATH} \
+            --extern librmc_macros=${RMC_MACRO_LIB_PATH} \
             "
     if [ "${1:-''}" == "--rmc-flags" ]
     then

From e4de6831d84b22bc97c85a5564bf41fbaf4bc228 Mon Sep 17 00:00:00 2001
From: Ted Kaminski <tedinski@amazon.com>
Date: Wed, 1 Dec 2021 23:51:03 +0000
Subject: [PATCH 3/7] add no_mangle as temporary measure to force function
 codegen

---
 library/rmc_macros/src/lib.rs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/library/rmc_macros/src/lib.rs b/library/rmc_macros/src/lib.rs
index eb081cc0f5d7..76be06df5c5e 100644
--- a/library/rmc_macros/src/lib.rs
+++ b/library/rmc_macros/src/lib.rs
@@ -33,6 +33,8 @@ 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!(

From 37d6aa2774a71e3a25665b8789b6c39c2ad5ef36 Mon Sep 17 00:00:00 2001
From: Ted Kaminski <tedinski@amazon.com>
Date: Wed, 1 Dec 2021 23:51:56 +0000
Subject: [PATCH 4/7] rmc::proof with 3 cases, not 2: normal build, test build,
 rmc build

---
 library/rmc_macros/src/lib.rs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/library/rmc_macros/src/lib.rs b/library/rmc_macros/src/lib.rs
index 76be06df5c5e..f7f9f004bec7 100644
--- a/library/rmc_macros/src/lib.rs
+++ b/library/rmc_macros/src/lib.rs
@@ -11,7 +11,14 @@
 // proc_macro::quote is nightly-only, so we'll cobble things together instead
 use proc_macro::TokenStream;
 
-#[cfg(not(rmc))]
+#[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,

From 76081aa6c32d7c27aef3656eb104682a4e1c085e Mon Sep 17 00:00:00 2001
From: Ted Kaminski <tedinski@amazon.com>
Date: Thu, 2 Dec 2021 22:59:46 +0000
Subject: [PATCH 5/7] refactor the attribute 'parsing' code a bit

---
 .../rustc_codegen_rmc/src/codegen/function.rs | 46 ++++++++++---------
 1 file changed, 25 insertions(+), 21 deletions(-)

diff --git a/compiler/rustc_codegen_rmc/src/codegen/function.rs b/compiler/rustc_codegen_rmc/src/codegen/function.rs
index 3d0d0b9d799c..e46aed0743fb 100644
--- a/compiler/rustc_codegen_rmc/src/codegen/function.rs
+++ b/compiler/rustc_codegen_rmc/src/codegen/function.rs
@@ -101,7 +101,7 @@ impl<'tcx> GotocCtx<'tcx> {
             let body = Stmt::block(stmts, loc);
             self.symbol_table.update_fn_declaration_with_definition(&name, body);
 
-            self.codegen_rmctool_attributes();
+            self.handle_rmctool_attributes();
         }
         self.reset_current_fn();
     }
@@ -209,35 +209,39 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// Currently, this is only proof harness annotations.
     /// i.e. `#[rmc::proof]` (which rmc_macros translates to `#[rmctool::proof]` for us to handle here)
-    fn codegen_rmctool_attributes(&mut self) {
+    fn handle_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);
+            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() };
+
+        self.proof_harnesses.push(harness);
+    }
 }
 
-fn matches_rmctool_attr(attr: &ast::Attribute, name: &str) -> bool {
+/// 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, .. }, .. }, _) => {
-            segments.len() == 2
-                && segments[0].ident.as_str() == "rmctool"
-                && segments[1].ident.as_str() == name
+        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())
         }
-        _ => false,
+        _ => None,
     }
 }

From 00788d2045d9d709e28b3289e0b6db8da1611ea7 Mon Sep 17 00:00:00 2001
From: Ted Kaminski <tedinski@amazon.com>
Date: Thu, 2 Dec 2021 23:12:53 +0000
Subject: [PATCH 6/7] Add original_line to proof harness metadata

---
 compiler/cbmc/src/goto_program/location.rs         | 7 +++++++
 compiler/rustc_codegen_rmc/src/codegen/function.rs | 8 ++++++--
 compiler/rustc_codegen_rmc/src/context/metadata.rs | 2 ++
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/compiler/cbmc/src/goto_program/location.rs b/compiler/cbmc/src/goto_program/location.rs
index 37fd9fc1e832..927e2b8cf11d 100644
--- a/compiler/cbmc/src/goto_program/location.rs
+++ b/compiler/cbmc/src/goto_program/location.rs
@@ -39,6 +39,13 @@ impl Location {
         }
     }
 
+    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 {
diff --git a/compiler/rustc_codegen_rmc/src/codegen/function.rs b/compiler/rustc_codegen_rmc/src/codegen/function.rs
index e46aed0743fb..e367838c7179 100644
--- a/compiler/rustc_codegen_rmc/src/codegen/function.rs
+++ b/compiler/rustc_codegen_rmc/src/codegen/function.rs
@@ -227,8 +227,12 @@ impl<'tcx> GotocCtx<'tcx> {
         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() };
+        let harness = HarnessMetadata {
+            pretty_name,
+            mangled_name,
+            original_file: loc.filename().unwrap(),
+            original_line: loc.line().unwrap().to_string(),
+        };
 
         self.proof_harnesses.push(harness);
     }
diff --git a/compiler/rustc_codegen_rmc/src/context/metadata.rs b/compiler/rustc_codegen_rmc/src/context/metadata.rs
index 8f18b995ce05..519eacc5b91c 100644
--- a/compiler/rustc_codegen_rmc/src/context/metadata.rs
+++ b/compiler/rustc_codegen_rmc/src/context/metadata.rs
@@ -15,6 +15,8 @@ pub struct HarnessMetadata {
     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

From 2377945c8e2b68c057165824a7a38a0c3f86129b Mon Sep 17 00:00:00 2001
From: Ted Kaminski <tedinski@amazon.com>
Date: Wed, 8 Dec 2021 19:08:36 +0000
Subject: [PATCH 7/7] introduce a 'exercise test' for proof annotations

---
 .../simple-proof-annotation/Cargo.toml         |  9 +++++++++
 .../simple-proof-annotation/main.expected      |  1 +
 .../simple-proof-annotation/src/main.rs        | 18 ++++++++++++++++++
 3 files changed, 28 insertions(+)
 create mode 100644 src/test/cargo-rmc/simple-proof-annotation/Cargo.toml
 create mode 100644 src/test/cargo-rmc/simple-proof-annotation/main.expected
 create mode 100644 src/test/cargo-rmc/simple-proof-annotation/src/main.rs

diff --git a/src/test/cargo-rmc/simple-proof-annotation/Cargo.toml b/src/test/cargo-rmc/simple-proof-annotation/Cargo.toml
new file mode 100644
index 000000000000..ac7b90d22ec0
--- /dev/null
+++ b/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]
diff --git a/src/test/cargo-rmc/simple-proof-annotation/main.expected b/src/test/cargo-rmc/simple-proof-annotation/main.expected
new file mode 100644
index 000000000000..67f4229c0556
--- /dev/null
+++ b/src/test/cargo-rmc/simple-proof-annotation/main.expected
@@ -0,0 +1 @@
+line 5 assertion failed: 1 == 2: FAILURE
diff --git a/src/test/cargo-rmc/simple-proof-annotation/src/main.rs b/src/test/cargo-rmc/simple-proof-annotation/src/main.rs
new file mode 100644
index 000000000000..80f143260d55
--- /dev/null
+++ b/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);
+}