From 3e8fb6019a910e8806c360eece3ab9e9b50d6e5c Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Tue, 4 May 2021 19:32:47 +0200 Subject: [PATCH] Avoid strict type comparison in statement assignment (#110) * Workaround for issue #95 * Print types in assert statement Co-authored-by: Nathan Chong --- .../src/gotoc/cbmc/goto_program/stmt.rs | 23 ++++++++++++++++++- 1 file changed, 22 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 52cdb24543958..98974e4e1698d 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,27 @@ 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( + &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]); + } stmt!(Assign { lhs, rhs }, loc) }