From fa118692a7a4494d27ca5892e514f79c8c2aee32 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 15 Jun 2021 20:38:37 -0400 Subject: [PATCH 1/4] Separate sanity check function --- .../rustc_codegen_llvm/src/gotoc/metadata.rs | 31 +++++++++++++++++++ .../rustc_codegen_llvm/src/gotoc/rvalue.rs | 4 +-- 2 files changed, 32 insertions(+), 3 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index b5f59c7f71a6..49daa19012e3 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -394,6 +394,37 @@ impl<'tcx> GotocCtx<'tcx> { Expr::statement_expression(body, t).with_location(loc) } + + /// RMC-specific function to sanity check expected components of in code + /// generation. If users see these assertions fail, something in our + /// translation to Gotoc has gone wrong, and we want them to file an issue. + pub fn codegen_sanity_check( + &mut self, + expect_true: Expr, + message: &str, + loc: Location, + ) -> Stmt { + let url = "https://github.com/model-checking/rmc/issues/new?template=bug_report.md"; + let assert_msg = format!( + "RMC code generation sanity check: {}. Please report failures:\n{}", + message, url + ); + + Stmt::block( + vec![ + // Assert our expected true expression. + Stmt::assert(expect_true.clone(), &assert_msg, loc.clone()), + // If it fails, assume false to block any further exploration of this path. + Stmt::if_then_else( + expect_true.not(), + Stmt::assume(Expr::bool_false(), loc.clone()), + None, + loc.clone(), + ), + ], + loc, + ) + } } impl<'tcx> LayoutOf for GotocCtx<'tcx> { diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 0eb5620f0e6b..5ddcbb81eae8 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -788,10 +788,8 @@ impl<'tcx> GotocCtx<'tcx> { let temp_var = self.gen_temp_variable(ty, Location::none()).to_expr(); let decl = Stmt::decl(temp_var.clone(), None, Location::none()); let check = Expr::eq(Expr::object_size(temp_var.address_of()), vt_size.clone()); - - // TODO: Add an rmc_sanity_check function https://github.com/model-checking/rmc/issues/200 let assert_msg = format!("Correct CBMC vtable size for {:?}", operand_type.kind()); - let size_assert = Stmt::assert(check, &assert_msg, Location::none()); + let size_assert = self.codegen_sanity_check(check, &assert_msg, Location::none()); Stmt::block(vec![decl, size_assert], Location::none()) } From c09d5665adba18c89376a1ab3457e6d206f4e6b9 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 16 Jun 2021 11:25:43 -0400 Subject: [PATCH 2/4] DSN review comments --- .../src/gotoc/cbmc/goto_program/stmt.rs | 22 +++++++++++++++++++ .../rustc_codegen_llvm/src/gotoc/rvalue.rs | 2 +- 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs index 6d42500d7944..11df389b851a 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs @@ -187,6 +187,28 @@ impl Stmt { Stmt::assert(Expr::bool_false(), msg, loc) } + /// RMC-specific function to sanity check expected components of in code + /// generation. If users see these assertions fail, something in our + /// translation to Gotoc has gone wrong, and we want them to file an issue. + pub fn assert_sanity_check(expect_true: Expr, message: &str, loc: Location) -> Stmt { + let url = "https://github.com/model-checking/rmc/issues/new?template=bug_report.md"; + let assert_msg = format!( + "RMC code generation sanity check: {}. Please report failures:\n{}", + message, url + ); + + Stmt::block( + vec![ + // Assert our expected true expression. + Stmt::assert(expect_true.clone(), &assert_msg, loc.clone()), + // If expect_true is false, assume false to block any further + // exploration of this path. + Stmt::assume(expect_true, loc.clone()), + ], + loc, + ) + } + /// `__CPROVER_assume(cond);` pub fn assume(cond: Expr, loc: Location) -> Self { assert!(cond.typ().is_bool(), "Assume expected bool, got {:?}", cond); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 5ddcbb81eae8..fa20c3d49628 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -789,7 +789,7 @@ impl<'tcx> GotocCtx<'tcx> { let decl = Stmt::decl(temp_var.clone(), None, Location::none()); let check = Expr::eq(Expr::object_size(temp_var.address_of()), vt_size.clone()); let assert_msg = format!("Correct CBMC vtable size for {:?}", operand_type.kind()); - let size_assert = self.codegen_sanity_check(check, &assert_msg, Location::none()); + let size_assert = Stmt::assert_sanity_check(check, &assert_msg, Location::none()); Stmt::block(vec![decl, size_assert], Location::none()) } From a0494dd0a771eca1e4e3a35d45a5a90146a6efa8 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 16 Jun 2021 13:48:35 -0400 Subject: [PATCH 3/4] Delete old --- .../rustc_codegen_llvm/src/gotoc/metadata.rs | 31 ------------------- 1 file changed, 31 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index 49daa19012e3..b5f59c7f71a6 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -394,37 +394,6 @@ impl<'tcx> GotocCtx<'tcx> { Expr::statement_expression(body, t).with_location(loc) } - - /// RMC-specific function to sanity check expected components of in code - /// generation. If users see these assertions fail, something in our - /// translation to Gotoc has gone wrong, and we want them to file an issue. - pub fn codegen_sanity_check( - &mut self, - expect_true: Expr, - message: &str, - loc: Location, - ) -> Stmt { - let url = "https://github.com/model-checking/rmc/issues/new?template=bug_report.md"; - let assert_msg = format!( - "RMC code generation sanity check: {}. Please report failures:\n{}", - message, url - ); - - Stmt::block( - vec![ - // Assert our expected true expression. - Stmt::assert(expect_true.clone(), &assert_msg, loc.clone()), - // If it fails, assume false to block any further exploration of this path. - Stmt::if_then_else( - expect_true.not(), - Stmt::assume(Expr::bool_false(), loc.clone()), - None, - loc.clone(), - ), - ], - loc, - ) - } } impl<'tcx> LayoutOf for GotocCtx<'tcx> { From c4e1f6fe06739c243b9925a5887c514b15541cc2 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 16 Jun 2021 16:51:37 -0400 Subject: [PATCH 4/4] Move out URL --- .../src/gotoc/cbmc/goto_program/stmt.rs | 13 +++++-------- compiler/rustc_codegen_llvm/src/gotoc/cbmc/utils.rs | 4 ++++ compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs | 5 +++-- 3 files changed, 12 insertions(+), 10 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs index 11df389b851a..784073ca4636 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs @@ -187,15 +187,12 @@ impl Stmt { Stmt::assert(Expr::bool_false(), msg, loc) } - /// RMC-specific function to sanity check expected components of in code - /// generation. If users see these assertions fail, something in our + /// A __CPROVER_assert to sanity check expected components of code + /// generation. If users see these assertions fail, something in the /// translation to Gotoc has gone wrong, and we want them to file an issue. - pub fn assert_sanity_check(expect_true: Expr, message: &str, loc: Location) -> Stmt { - let url = "https://github.com/model-checking/rmc/issues/new?template=bug_report.md"; - let assert_msg = format!( - "RMC code generation sanity check: {}. Please report failures:\n{}", - message, url - ); + pub fn assert_sanity_check(expect_true: Expr, message: &str, url: &str, loc: Location) -> Stmt { + let assert_msg = + format!("Code generation sanity check: {}. Please report failures:\n{}", message, url); Stmt::block( vec![ diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/utils.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/utils.rs index 0cce5ba654f0..9c71313533cc 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/utils.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/utils.rs @@ -2,6 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Useful utilities for CBMC +/// RMC bug report URL, for asserts/errors +pub const BUG_REPORT_URL: &str = + "https://github.com/model-checking/rmc/issues/new?template=bug_report.md"; + /// The aggregate name used in CBMC for aggregates of type `n`. pub fn aggr_name(n: &str) -> String { format!("tag-{}", n) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index fa20c3d49628..849377ab5230 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT use super::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type}; -use super::cbmc::utils::aggr_name; +use super::cbmc::utils::{aggr_name, BUG_REPORT_URL}; use super::cbmc::MachineModel; use super::metadata::*; use super::typ::{is_pointer, pointee_type}; @@ -789,7 +789,8 @@ impl<'tcx> GotocCtx<'tcx> { let decl = Stmt::decl(temp_var.clone(), None, Location::none()); let check = Expr::eq(Expr::object_size(temp_var.address_of()), vt_size.clone()); let assert_msg = format!("Correct CBMC vtable size for {:?}", operand_type.kind()); - let size_assert = Stmt::assert_sanity_check(check, &assert_msg, Location::none()); + let size_assert = + Stmt::assert_sanity_check(check, &assert_msg, BUG_REPORT_URL, Location::none()); Stmt::block(vec![decl, size_assert], Location::none()) }