From a2f83f9a5f8302d200b6fd37c0fc57700270852b Mon Sep 17 00:00:00 2001 From: Nathan Chong Date: Thu, 22 Apr 2021 20:43:15 +0000 Subject: [PATCH 1/2] Workaround for issue #95 --- .../src/gotoc/cbmc/goto_program/stmt.rs | 17 ++++++++++++++++- 1 file changed, 16 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 52cdb2454395..40c43a8a7853 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 @@ -3,6 +3,7 @@ use self::StmtBody::*; use super::{BuiltinFn, Expr, Location}; use std::fmt::Debug; +use tracing::debug; /////////////////////////////////////////////////////////////////////////////////////////////// /// Datatypes @@ -150,7 +151,21 @@ macro_rules! stmt { impl Stmt { /// `lhs = rhs;` pub fn assign(lhs: Expr, rhs: Expr, loc: Location) -> Self { - assert_eq!(lhs.typ(), rhs.typ()); + //Temporarily work around https://github.com/model-checking/rmc/issues/95 + //by disabling the assert and soundly assigning nondet + //assert_eq!(lhs.typ(), rhs.typ()); + if lhs.typ() != rhs.typ() { + debug!( + "WARNING: assign statement with unequal types lhs {:?} rhs {:?}", + lhs.typ(), + rhs.typ() + ); + let assert_stmt = + Stmt::assert_false("Reached assignment statement with unequal types", loc.clone()); + let nondet_value = lhs.typ().nondet(); + let nondet_assign_stmt = stmt!(Assign { lhs, rhs: nondet_value }, loc.clone()); + return Stmt::block(vec![assert_stmt, nondet_assign_stmt]); + } stmt!(Assign { lhs, rhs }, loc) } From 05f984021878ec9d53016292ee6bd73c066c91a7 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 4 May 2021 15:29:48 +0000 Subject: [PATCH 2/2] Print types in assert statement --- .../src/gotoc/cbmc/goto_program/stmt.rs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 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 40c43a8a7853..98974e4e1698 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 @@ -160,8 +160,14 @@ impl Stmt { lhs.typ(), rhs.typ() ); - let assert_stmt = - Stmt::assert_false("Reached assignment statement with unequal types", loc.clone()); + let assert_stmt = Stmt::assert_false( + &format!( + "Reached assignment statement with unequal types {:?} {:?}", + lhs.typ(), + rhs.typ() + ), + loc.clone(), + ); let nondet_value = lhs.typ().nondet(); let nondet_assign_stmt = stmt!(Assign { lhs, rhs: nondet_value }, loc.clone()); return Stmt::block(vec![assert_stmt, nondet_assign_stmt]);