From 4cae2a3946c78c307468198b88876c300321bb84 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 21 Sep 2018 15:32:52 +0100 Subject: [PATCH 1/2] Rename variables in boolbv_equality for readability --- src/solvers/flattening/boolbv_equality.cpp | 32 +++++++++++----------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 2e7ac9aa500..b01713e1b19 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -41,24 +41,24 @@ literalt boolbvt::convert_equality(const equal_exprt &expr) return record_array_equality(expr); } - const bvt &bv0=convert_bv(expr.lhs()); - const bvt &bv1=convert_bv(expr.rhs()); + const bvt &lhs_bv = convert_bv(expr.lhs()); + const bvt &rhs_bv = convert_bv(expr.rhs()); DATA_INVARIANT( - bv0.size() == bv1.size(), - std::string("unexpected size mismatch on equality:\n") + "lhs: " + - expr.lhs().pretty() + '\n' + "lhs size: " + std::to_string(bv0.size()) + - '\n' + "rhs: " + expr.rhs().pretty() + '\n' + - "rhs size: " + std::to_string(bv1.size())); + lhs_bv.size() == rhs_bv.size(), + std::string("unexpected size mismatch on equality:\n") + + "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " + + std::to_string(lhs_bv.size()) + '\n' + "rhs: " + expr.rhs().pretty() + + '\n' + "rhs size: " + std::to_string(rhs_bv.size())); - if(bv0.empty()) + if(lhs_bv.empty()) { // An empty bit-vector comparison. It's not clear // what this is meant to say. return prop.new_variable(); } - return bv_utils.equal(bv0, bv1); + return bv_utils.equal(lhs_bv, rhs_bv); } literalt boolbvt::convert_verilog_case_equality( @@ -75,18 +75,18 @@ literalt boolbvt::convert_verilog_case_equality( "######### lhs: " + expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty()); - const bvt &bv0=convert_bv(expr.lhs()); - const bvt &bv1=convert_bv(expr.rhs()); + const bvt &lhs_bv = convert_bv(expr.lhs()); + const bvt &rhs_bv = convert_bv(expr.rhs()); DATA_INVARIANT( - bv0.size() == bv1.size(), + lhs_bv.size() == rhs_bv.size(), std::string("unexpected size mismatch on verilog_case_equality:\n") + "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " + - std::to_string(bv0.size()) + '\n' + "rhs: " + expr.rhs().pretty() + '\n' + - "rhs size: " + std::to_string(bv1.size())); + std::to_string(lhs_bv.size()) + '\n' + "rhs: " + expr.rhs().pretty() + + '\n' + "rhs size: " + std::to_string(rhs_bv.size())); if(expr.id()==ID_verilog_case_inequality) - return !bv_utils.equal(bv0, bv1); + return !bv_utils.equal(lhs_bv, rhs_bv); else - return bv_utils.equal(bv0, bv1); + return bv_utils.equal(lhs_bv, rhs_bv); } From cbc78dbe63be5dcbe4d277278d37887a84cff483 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 21 Sep 2018 15:41:40 +0100 Subject: [PATCH 2/2] Replace throws with invariants in boolbv_equality --- src/solvers/flattening/boolbv_equality.cpp | 42 +++++++++++----------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index b01713e1b19..f121610b4a9 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -19,13 +19,11 @@ literalt boolbvt::convert_equality(const equal_exprt &expr) { const bool is_base_type_eq = base_type_eq(expr.lhs().type(), expr.rhs().type(), ns); - if(!is_base_type_eq) - { - const std::string error_msg = - std::string("equality without matching types:\n") + "######### lhs: " + - expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty(); - throw bitvector_conversion_exceptiont(error_msg, expr); - } + DATA_INVARIANT_WITH_DIAGNOSTICS( + is_base_type_eq, + "types of expressions on each side of equality should match", + irep_pretty_diagnosticst{expr.lhs()}, + irep_pretty_diagnosticst{expr.rhs()}); // see if it is an unbounded array if(is_unbounded_array(expr.lhs().type())) @@ -44,12 +42,13 @@ literalt boolbvt::convert_equality(const equal_exprt &expr) const bvt &lhs_bv = convert_bv(expr.lhs()); const bvt &rhs_bv = convert_bv(expr.rhs()); - DATA_INVARIANT( + DATA_INVARIANT_WITH_DIAGNOSTICS( lhs_bv.size() == rhs_bv.size(), - std::string("unexpected size mismatch on equality:\n") + - "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " + - std::to_string(lhs_bv.size()) + '\n' + "rhs: " + expr.rhs().pretty() + - '\n' + "rhs size: " + std::to_string(rhs_bv.size())); + "sizes of lhs and rhs bitvectors should match", + irep_pretty_diagnosticst{expr.lhs()}, + "lhs size: " + std::to_string(lhs_bv.size()), + irep_pretty_diagnosticst{expr.rhs()}, + "rhs size: " + std::to_string(rhs_bv.size())); if(lhs_bv.empty()) { @@ -69,21 +68,22 @@ literalt boolbvt::convert_verilog_case_equality( const bool is_base_type_eq = base_type_eq(expr.lhs().type(), expr.rhs().type(), ns); - DATA_INVARIANT( + DATA_INVARIANT_WITH_DIAGNOSTICS( is_base_type_eq, - std::string("verilog_case_equality without matching types:\n") + - "######### lhs: " + expr.lhs().pretty() + '\n' + - "######### rhs: " + expr.rhs().pretty()); + "lhs and rhs types should match in verilog_case_equality", + irep_pretty_diagnosticst{expr.lhs()}, + irep_pretty_diagnosticst{expr.rhs()}); const bvt &lhs_bv = convert_bv(expr.lhs()); const bvt &rhs_bv = convert_bv(expr.rhs()); - DATA_INVARIANT( + DATA_INVARIANT_WITH_DIAGNOSTICS( lhs_bv.size() == rhs_bv.size(), - std::string("unexpected size mismatch on verilog_case_equality:\n") + - "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " + - std::to_string(lhs_bv.size()) + '\n' + "rhs: " + expr.rhs().pretty() + - '\n' + "rhs size: " + std::to_string(rhs_bv.size())); + "bitvector arguments to verilog_case_equality should have the same size", + irep_pretty_diagnosticst{expr.lhs()}, + "lhs size: " + std::to_string(lhs_bv.size()), + irep_pretty_diagnosticst{expr.rhs()}, + "rhs size: " + std::to_string(rhs_bv.size())); if(expr.id()==ID_verilog_case_inequality) return !bv_utils.equal(lhs_bv, rhs_bv);