diff --git a/Cargo.lock b/Cargo.lock index 6b62f901631a..94928b6355e3 100644 --- a/Cargo.lock +++ b/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" diff --git a/compiler/cbmc/src/goto_program/location.rs b/compiler/cbmc/src/goto_program/location.rs index e08a0fefd979..927e2b8cf11d 100644 --- a/compiler/cbmc/src/goto_program/location.rs +++ b/compiler/cbmc/src/goto_program/location.rs @@ -32,6 +32,20 @@ impl Location { } } + pub fn filename(&self) -> Option { + match self { + Location::Loc { file, .. } => Some(file.to_string()), + _ => None, + } + } + + pub fn line(&self) -> Option { + 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 b57751f71dc1..e367838c7179 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.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(¤t_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 { + 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, + } } diff --git a/compiler/rustc_codegen_rmc/src/compiler_interface.rs b/compiler/rustc_codegen_rmc/src/compiler_interface.rs index 5d7931ff0b28..008001a4422c 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; @@ -29,9 +29,10 @@ use tracing::{debug, warn}; // #[derive(RustcEncodable, RustcDecodable)] pub struct GotocCodegenResult { - pub type_map: BTreeMap, - pub symtab: SymbolTable, pub crate_name: rustc_span::Symbol, + pub metadata: RmcMetadata, + pub symtab: SymbolTable, + pub type_map: BTreeMap, pub vtable_restrictions: Option, } @@ -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); diff --git a/compiler/rustc_codegen_rmc/src/context/goto_ctx.rs b/compiler/rustc_codegen_rmc/src/context/goto_ctx.rs index f1beb328be28..71180f0d0976 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 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>, pub type_map: FxHashMap>, + pub proof_harnesses: Vec, } /// 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![], } } } 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..519eacc5b91c --- /dev/null +++ b/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, +} diff --git a/compiler/rustc_codegen_rmc/src/context/mod.rs b/compiler/rustc_codegen_rmc/src/context/mod.rs index eb4ec2f8e741..7bf8c3f51b1c 100644 --- a/compiler/rustc_codegen_rmc/src/context/mod.rs +++ b/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; diff --git a/library/rmc/Cargo.toml b/library/rmc/Cargo.toml index 32a76e76b345..8f3f764140f1 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_macros = { path = "../rmc_macros" } diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs index e1001bb4b329..4c7acf68f766 100644 --- a/library/rmc/src/lib.rs +++ b/library/rmc/src/lib.rs @@ -53,3 +53,6 @@ pub fn nondet() -> 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::*; diff --git a/library/rmc_macros/Cargo.toml b/library/rmc_macros/Cargo.toml new file mode 100644 index 000000000000..bd8f791b8030 --- /dev/null +++ b/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] diff --git a/library/rmc_macros/src/lib.rs b/library/rmc_macros/src/lib.rs new file mode 100644 index 000000000000..f7f9f004bec7 --- /dev/null +++ b/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::().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::().unwrap()); + // no_mangle is a temporary hack to make the function "public" so it gets codegen'd + result.extend("#[no_mangle]".parse::().unwrap()); + result.extend(item); + result + // quote!( + // #[rmctool::proof] + // $item + // ) +} diff --git a/scripts/rmc-rustc b/scripts/rmc-rustc index 8d981fed5dd2..fd2a6168828c 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_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} diff --git a/scripts/rmc.py b/scripts/rmc.py index 4f3032a98845..8fb1bab7709e 100644 --- a/scripts/rmc.py +++ b/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) 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" $@ 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); +}