From fc44d994c2dab1a0f59cc0bceb174c64fb5f1803 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 22 Feb 2018 10:33:32 +0000 Subject: [PATCH 1/7] Use invariant instead if printing error message to cout --- src/solvers/flattening/boolbv_equality.cpp | 26 ++++++++++++---------- 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 95a379a5a95..76fa73697b1 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -19,12 +20,12 @@ Author: Daniel Kroening, kroening@kroening.com literalt boolbvt::convert_equality(const equal_exprt &expr) { - if(!base_type_eq(expr.lhs().type(), expr.rhs().type(), ns)) - { - std::cout << "######### lhs: " << expr.lhs().pretty() << '\n'; - std::cout << "######### rhs: " << expr.rhs().pretty() << '\n'; - throw "equality without matching types"; - } + const bool is_base_type_eq = + base_type_eq(expr.lhs().type(), expr.rhs().type(), ns); + DATA_INVARIANT( + is_base_type_eq, + std::string("equality without matching types:\n") + "######### lhs: " + + expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty()); // see if it is an unbounded array if(is_unbounded_array(expr.lhs().type())) @@ -68,12 +69,13 @@ literalt boolbvt::convert_verilog_case_equality( // This is 4-valued comparison, i.e., z===z, x===x etc. // The result is always Boolean. - if(!base_type_eq(expr.lhs().type(), expr.rhs().type(), ns)) - { - std::cout << "######### lhs: " << expr.lhs().pretty() << '\n'; - std::cout << "######### rhs: " << expr.rhs().pretty() << '\n'; - throw "verilog_case_equality without matching types"; - } + const bool is_base_type_eq = + base_type_eq(expr.lhs().type(), expr.rhs().type(), ns); + DATA_INVARIANT( + is_base_type_eq, + std::string("verilog_case_equality without matching types:\n") + + "######### lhs: " + expr.lhs().pretty() + '\n' + + "######### rhs: " + expr.rhs().pretty()); const bvt &bv0=convert_bv(expr.lhs()); const bvt &bv1=convert_bv(expr.rhs()); From f7afe1f5f4bbd86332d96fa9d8a65896f3597250 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 22 Feb 2018 10:34:07 +0000 Subject: [PATCH 2/7] Replace assert by invariant --- src/solvers/sat/cnf.cpp | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/solvers/sat/cnf.cpp b/src/solvers/sat/cnf.cpp index bed97954bac..7250131a384 100644 --- a/src/solvers/sat/cnf.cpp +++ b/src/solvers/sat/cnf.cpp @@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "cnf.h" #include -#include -#include #include +#include + // #define VERBOSE /// Tseitin encoding of conjunction of two literals @@ -426,10 +426,12 @@ bool cnft::process_clause(const bvt &bv, bvt &dest) for(const auto l : bv) { // we never use index 0 - assert(l.var_no()!=0); + INVARIANT(l.var_no() != 0, "variable 0 must not be used"); // we never use 'unused_var_no' - assert(l.var_no()!=literalt::unused_var_no()); + INVARIANT( + l.var_no() != literalt::unused_var_no(), + "variable 'unused_var_no' must not be used"); if(l.is_true()) return true; // clause satisfied @@ -437,11 +439,10 @@ bool cnft::process_clause(const bvt &bv, bvt &dest) if(l.is_false()) continue; // will remove later - if(l.var_no()>=_no_variables) - std::cout << "l.var_no()=" << l.var_no() - << " _no_variables=" << _no_variables << '\n'; - - assert(l.var_no()<_no_variables); + INVARIANT( + l.var_no() < _no_variables, + "unknown variable " + std::to_string(l.var_no()) + + " (no_variables = " + std::to_string(_no_variables) + " )"); } // now copy From 25292117da2a14be6f4a1629df1712708bb1d613 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 22 Feb 2018 10:56:10 +0000 Subject: [PATCH 3/7] Clang-format --- src/solvers/sat/pbs_dimacs_cnf.cpp | 195 ++++++++++++++--------------- 1 file changed, 97 insertions(+), 98 deletions(-) diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp index b439577c270..561ff98e16e 100644 --- a/src/solvers/sat/pbs_dimacs_cnf.cpp +++ b/src/solvers/sat/pbs_dimacs_cnf.cpp @@ -15,12 +15,14 @@ Author: Alex Groce void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out) { - double d_sum=0; + double d_sum = 0; // std::cout << "enter: No Lit.=" << no_variables () << "\n"; - for(std::map::const_iterator it=pb_constraintmap.begin(); - it!=pb_constraintmap.end(); ++it) + for(std::map::const_iterator it = + pb_constraintmap.begin(); + it != pb_constraintmap.end(); + ++it) d_sum += ((*it).second); if(!optimize) @@ -45,7 +47,7 @@ void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out) for(const auto &lit_entry : pb_constraintmap) { - int dimacs_lit=lit_entry.first.dimacs(); + int dimacs_lit = lit_entry.first.dimacs(); out << "v" << dimacs_lit << " c" << lit_entry.second << "\n"; } @@ -61,7 +63,7 @@ bool pbs_dimacs_cnft::pbs_solve() if(!pbs_path.empty()) { command += pbs_path; - if(command.substr(command.length(), 1)!="/") + if(command.substr(command.length(), 1) != "/") command += "/"; } @@ -69,20 +71,20 @@ bool pbs_dimacs_cnft::pbs_solve() // std::cout << "PBS COMMAND IS: " << command << "\n"; /* - if (!(getenv("PBS_PATH")==NULL)) - { + if (!(getenv("PBS_PATH")==NULL)) + { command=getenv("PBS_PATH"); - } - else - { + } + else + { error ("Unable to read PBS_PATH environment variable.\n"); return false; - } + } */ command += " -f temp.cnf"; - #if 1 +#if 1 if(optimize) { if(binary_search) @@ -99,19 +101,19 @@ bool pbs_dimacs_cnft::pbs_solve() { command += " -S 1000 -D 1 -a"; } - #else +#else command += " -z"; - #endif +#endif command += " -a > temp.out"; - int res=system(command.c_str()); - CHECK_RETURN(0==res); + int res = system(command.c_str()); + CHECK_RETURN(0 == res); std::ifstream file("temp.out"); std::string line; int v; - bool satisfied=false; + bool satisfied = false; if(file.fail()) { @@ -119,60 +121,60 @@ bool pbs_dimacs_cnft::pbs_solve() return false; } - opt_sum=-1; + opt_sum = -1; - while(file && !file.eof ()) + while(file && !file.eof()) + { + std::getline(file, line); + if( + strstr(line.c_str(), "Variable Assignments Satisfying CNF Formula:") != + nullptr) { - std::getline(file, line); - if(strstr(line.c_str(), - "Variable Assignments Satisfying CNF Formula:")!=nullptr) + // print ("Reading assignments...\n"); + // std::cout << "No literals: " << no_variables() << "\n"; + satisfied = true; + assigned.clear(); + for(size_t i = 0; (file && (i < no_variables())); ++i) + { + file >> v; + if(v > 0) { - // print ("Reading assignments...\n"); - // std::cout << "No literals: " << no_variables() << "\n"; - satisfied=true; - assigned.clear(); - for(size_t i=0; (file && (i < no_variables())); ++i) - { - file >> v; - if(v > 0) - { - // std::cout << v << " "; - assigned.insert(v); - } - } - // std::cout << "\n"; - // print ("Finished reading assignments.\n"); - } - else if(strstr(line.c_str(), "SAT... SUM")!=nullptr) - { - // print (line); - sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); - } - else if(strstr(line.c_str(), "SAT - All implied")!=nullptr) - { - // print (line); - sscanf( - line.c_str(), - "%*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %d", - &opt_sum); - } - else if(strstr(line.c_str(), "SAT... Solution")!=nullptr) - { - // print(line); - sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); - } - else if(strstr(line.c_str(), "Optimal Soln")!=nullptr) - { - // print(line); - if(strstr(line.c_str(), "time out")!=nullptr) - { - status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT." - << eom; - return satisfied; - } - sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); + // std::cout << v << " "; + assigned.insert(v); } + } + // std::cout << "\n"; + // print ("Finished reading assignments.\n"); + } + else if(strstr(line.c_str(), "SAT... SUM") != nullptr) + { + // print (line); + sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); + } + else if(strstr(line.c_str(), "SAT - All implied") != nullptr) + { + // print (line); + sscanf( + line.c_str(), + "%*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %d", + &opt_sum); } + else if(strstr(line.c_str(), "SAT... Solution") != nullptr) + { + // print(line); + sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); + } + else if(strstr(line.c_str(), "Optimal Soln") != nullptr) + { + // print(line); + if(strstr(line.c_str(), "time out") != nullptr) + { + status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT." << eom; + return satisfied; + } + sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); + } + } return satisfied; } @@ -191,21 +193,18 @@ propt::resultt pbs_dimacs_cnft::prop_solve() pbfile.close(); // We start counting at 1, thus there is one variable fewer. - messaget::status() << - (no_variables()-1) << " variables, " << - clauses.size() << " clauses" << eom; + messaget::status() << (no_variables() - 1) << " variables, " << clauses.size() + << " clauses" << eom; - bool result=pbs_solve(); + bool result = pbs_solve(); if(!result) { - messaget::status() << - "PBS checker: system is UNSATISFIABLE" << eom; + messaget::status() << "PBS checker: system is UNSATISFIABLE" << eom; } else { - messaget::status() << - "PBS checker: system is SATISFIABLE"; + messaget::status() << "PBS checker: system is SATISFIABLE"; if(optimize) messaget::status() << " (distance " << opt_sum << ")"; messaget::status() << eom; @@ -219,40 +218,40 @@ propt::resultt pbs_dimacs_cnft::prop_solve() tvt pbs_dimacs_cnft::l_get(literalt a) const { - int dimacs_lit=a.dimacs(); + int dimacs_lit = a.dimacs(); // std::cout << a << " / " << dimacs_lit << "="; - bool neg=(dimacs_lit < 0); + bool neg = (dimacs_lit < 0); if(neg) - dimacs_lit=-dimacs_lit; + dimacs_lit = -dimacs_lit; - std::set::const_iterator f=assigned.find(dimacs_lit); + std::set::const_iterator f = assigned.find(dimacs_lit); if(!neg) + { + if(f == assigned.end()) { - if(f==assigned.end()) - { - // std::cout << "FALSE" << "\n"; - return tvt(false); - } - else - { - // std::cout << "TRUE" << "\n"; - return tvt(true); - } + // std::cout << "FALSE" << "\n"; + return tvt(false); } + else + { + // std::cout << "TRUE" << "\n"; + return tvt(true); + } + } else + { + if(f != assigned.end()) { - if(f!=assigned.end()) - { - // std::cout << "FALSE" << "\n"; - return tvt(false); - } - else - { - // std::cout << "TRUE" << "\n"; - return tvt(true); - } + // std::cout << "FALSE" << "\n"; + return tvt(false); } + else + { + // std::cout << "TRUE" << "\n"; + return tvt(true); + } + } } From 7018ab44a7285d556a80d5d6e7ac5d6cdaa76aee Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 22 Feb 2018 11:02:19 +0000 Subject: [PATCH 4/7] Clean up commented out code --- src/solvers/sat/pbs_dimacs_cnf.cpp | 80 ++++++++++++++++++++++-------- 1 file changed, 59 insertions(+), 21 deletions(-) diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp index 561ff98e16e..b9120400445 100644 --- a/src/solvers/sat/pbs_dimacs_cnf.cpp +++ b/src/solvers/sat/pbs_dimacs_cnf.cpp @@ -11,13 +11,18 @@ Author: Alex Groce #include #include #include + +#ifdef DEBUG #include +#endif void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out) { double d_sum = 0; - // std::cout << "enter: No Lit.=" << no_variables () << "\n"; +#ifdef DEBUG + std::cout << "enter: No Lit.=" << no_variables() << "\n"; +#endif for(std::map::const_iterator it = pb_constraintmap.begin(); @@ -51,12 +56,16 @@ void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out) out << "v" << dimacs_lit << " c" << lit_entry.second << "\n"; } - // std::cout << "exit: No Lit.=" << no_variables () << "\n"; +#ifdef DEBUG + std::cout << "exit: No Lit.=" << no_variables() << "\n"; +#endif } bool pbs_dimacs_cnft::pbs_solve() { - // std::cout << "solve: No Lit.=" << no_variables () << "\n"; +#ifdef DEBUG + std::cout << "solve: No Lit.=" << no_variables() << "\n"; +#endif std::string command; @@ -69,8 +78,10 @@ bool pbs_dimacs_cnft::pbs_solve() command += "pbs"; - // std::cout << "PBS COMMAND IS: " << command << "\n"; - /* +#ifdef DEBUG + std::cout << "PBS COMMAND IS: " << command << "\n"; +#endif +#if 0 if (!(getenv("PBS_PATH")==NULL)) { command=getenv("PBS_PATH"); @@ -80,7 +91,7 @@ bool pbs_dimacs_cnft::pbs_solve() error ("Unable to read PBS_PATH environment variable.\n"); return false; } - */ +#endif command += " -f temp.cnf"; @@ -93,7 +104,10 @@ bool pbs_dimacs_cnft::pbs_solve() } else { - // std::cout << "NO BINARY SEARCH" << "\n"; +#ifdef DEBUG + std::cout << "NO BINARY SEARCH" + << "\n"; +#endif command += " -S 1000 -D 1 -I -a"; } } @@ -130,8 +144,10 @@ bool pbs_dimacs_cnft::pbs_solve() strstr(line.c_str(), "Variable Assignments Satisfying CNF Formula:") != nullptr) { - // print ("Reading assignments...\n"); - // std::cout << "No literals: " << no_variables() << "\n"; +#ifdef DEBUG + std::cout << "Reading assignments...\n"; + std::cout << "No literals: " << no_variables() << "\n"; +#endif satisfied = true; assigned.clear(); for(size_t i = 0; (file && (i < no_variables())); ++i) @@ -139,21 +155,29 @@ bool pbs_dimacs_cnft::pbs_solve() file >> v; if(v > 0) { - // std::cout << v << " "; +#ifdef DEBUG + std::cout << v << " "; +#endif assigned.insert(v); } } - // std::cout << "\n"; - // print ("Finished reading assignments.\n"); +#ifdef DEBUG + std::cout << "\n"; + std::cout << "Finished reading assignments.\n"; +#endif } else if(strstr(line.c_str(), "SAT... SUM") != nullptr) { - // print (line); +#ifdef DEBUG + std::cout << line; +#endif sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); } else if(strstr(line.c_str(), "SAT - All implied") != nullptr) { - // print (line); +#ifdef DEBUG + std::cout << line; +#endif sscanf( line.c_str(), "%*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %d", @@ -161,12 +185,16 @@ bool pbs_dimacs_cnft::pbs_solve() } else if(strstr(line.c_str(), "SAT... Solution") != nullptr) { - // print(line); +#ifdef DEBUG + std::cout << line; +#endif sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum); } else if(strstr(line.c_str(), "Optimal Soln") != nullptr) { - // print(line); +#ifdef DEBUG + std::cout << line; +#endif if(strstr(line.c_str(), "time out") != nullptr) { status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT." << eom; @@ -220,7 +248,9 @@ tvt pbs_dimacs_cnft::l_get(literalt a) const { int dimacs_lit = a.dimacs(); - // std::cout << a << " / " << dimacs_lit << "="; +#ifdef DEBUG + std::cout << a << " / " << dimacs_lit << "="; +#endif bool neg = (dimacs_lit < 0); if(neg) @@ -232,12 +262,16 @@ tvt pbs_dimacs_cnft::l_get(literalt a) const { if(f == assigned.end()) { - // std::cout << "FALSE" << "\n"; +#ifdef DEBUG + std::cout << "FALSE\n"; +#endif return tvt(false); } else { - // std::cout << "TRUE" << "\n"; +#ifdef DEBUG + std::cout << "TRUE\n"; +#endif return tvt(true); } } @@ -245,12 +279,16 @@ tvt pbs_dimacs_cnft::l_get(literalt a) const { if(f != assigned.end()) { - // std::cout << "FALSE" << "\n"; +#ifdef DEBUG + std::cout << "FALSE\n"; +#endif return tvt(false); } else { - // std::cout << "TRUE" << "\n"; +#ifdef DEBUG + std::cout << "TRUE\n"; +#endif return tvt(true); } } From aaf94771fb8379e79722347d8a22d05532d5d78e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 6 Mar 2018 16:19:45 +0000 Subject: [PATCH 5/7] Use ranged for and const --- src/solvers/sat/pbs_dimacs_cnf.cpp | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp index b9120400445..84d3893eaeb 100644 --- a/src/solvers/sat/pbs_dimacs_cnf.cpp +++ b/src/solvers/sat/pbs_dimacs_cnf.cpp @@ -24,11 +24,8 @@ void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out) std::cout << "enter: No Lit.=" << no_variables() << "\n"; #endif - for(std::map::const_iterator it = - pb_constraintmap.begin(); - it != pb_constraintmap.end(); - ++it) - d_sum += ((*it).second); + for(const auto &lit_entry : pb_constraintmap) + d_sum += lit_entry.second; if(!optimize) { @@ -52,7 +49,7 @@ void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out) for(const auto &lit_entry : pb_constraintmap) { - int dimacs_lit = lit_entry.first.dimacs(); + const int dimacs_lit = lit_entry.first.dimacs(); out << "v" << dimacs_lit << " c" << lit_entry.second << "\n"; } @@ -121,7 +118,7 @@ bool pbs_dimacs_cnft::pbs_solve() command += " -a > temp.out"; - int res = system(command.c_str()); + const int res = system(command.c_str()); CHECK_RETURN(0 == res); std::ifstream file("temp.out"); @@ -224,7 +221,7 @@ propt::resultt pbs_dimacs_cnft::prop_solve() messaget::status() << (no_variables() - 1) << " variables, " << clauses.size() << " clauses" << eom; - bool result = pbs_solve(); + const bool result = pbs_solve(); if(!result) { @@ -252,7 +249,7 @@ tvt pbs_dimacs_cnft::l_get(literalt a) const std::cout << a << " / " << dimacs_lit << "="; #endif - bool neg = (dimacs_lit < 0); + const bool neg = (dimacs_lit < 0); if(neg) dimacs_lit = -dimacs_lit; From fe40b19079462b0c7031801b75ffa6115e5be509 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 22 Feb 2018 11:38:50 +0000 Subject: [PATCH 6/7] Use invariant instead of printing error message to cerr --- src/solvers/flattening/boolbv_add_sub.cpp | 18 ++++-------- src/solvers/flattening/boolbv_case.cpp | 30 +++++++------------- src/solvers/flattening/boolbv_cond.cpp | 16 ++++------- src/solvers/flattening/boolbv_equality.cpp | 30 ++++++++------------ src/solvers/flattening/boolbv_floatbv_op.cpp | 9 ++---- 5 files changed, 37 insertions(+), 66 deletions(-) diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp index 0486874d6d2..fc4e66935d9 100644 --- a/src/solvers/flattening/boolbv_add_sub.cpp +++ b/src/solvers/flattening/boolbv_add_sub.cpp @@ -8,8 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include - +#include #include #include "../floatbv/float_utils.h" @@ -38,12 +37,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr) throw "operator "+expr.id_string()+" takes at least one operand"; const exprt &op0=expr.op0(); - - if(op0.type()!=type) - { - std::cerr << expr.pretty() << '\n'; - throw "add/sub with mixed types"; - } + DATA_INVARIANT( + op0.type() == type, "add/sub with mixed types:\n" + expr.pretty()); bvt bv=convert_bv(op0); @@ -69,11 +64,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr) it=operands.begin()+1; it!=operands.end(); it++) { - if(it->type()!=type) - { - std::cerr << expr.pretty() << '\n'; - throw "add/sub with mixed types"; - } + DATA_INVARIANT( + it->type() == type, "add/sub with mixed types:\n" + expr.pretty()); const bvt &op=convert_bv(*it); diff --git a/src/solvers/flattening/boolbv_case.cpp b/src/solvers/flattening/boolbv_case.cpp index 6434f216178..7e1d2280a32 100644 --- a/src/solvers/flattening/boolbv_case.cpp +++ b/src/solvers/flattening/boolbv_case.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include +#include bvt boolbvt::convert_case(const exprt &expr) { @@ -49,15 +49,11 @@ bvt boolbvt::convert_case(const exprt &expr) break; case COMPARE: - if(compare_bv.size()!=op.size()) - { - std::cerr << "compare operand: " << compare_bv.size() - << "\noperand: " << op.size() << '\n' - << it->pretty() - << '\n'; - - throw "size of compare operand does not match"; - } + DATA_INVARIANT( + compare_bv.size() == op.size(), + std::string("size of compare operand does not match:\n") + + "compare operand: " + std::to_string(compare_bv.size()) + + "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty()); compare_literal=bv_utils.equal(compare_bv, op); compare_literal=prop.land(!previous_compare, compare_literal); @@ -68,15 +64,11 @@ bvt boolbvt::convert_case(const exprt &expr) break; case VALUE: - if(bv.size()!=op.size()) - { - std::cerr << "result size: " << bv.size() - << "\noperand: " << op.size() << '\n' - << it->pretty() - << '\n'; - - throw "size of value operand does not match"; - } + DATA_INVARIANT( + bv.size() == op.size(), + std::string("size of value operand does not match:\n") + + "result size: " + std::to_string(bv.size()) + + "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty()); { literalt value_literal=bv_utils.equal(bv, op); diff --git a/src/solvers/flattening/boolbv_cond.cpp b/src/solvers/flattening/boolbv_cond.cpp index 514c1e817f3..e6bb129b0d4 100644 --- a/src/solvers/flattening/boolbv_cond.cpp +++ b/src/solvers/flattening/boolbv_cond.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include +#include bvt boolbvt::convert_cond(const exprt &expr) { @@ -51,15 +51,11 @@ bvt boolbvt::convert_cond(const exprt &expr) { const bvt &op=convert_bv(*it); - if(bv.size()!=op.size()) - { - std::cerr << "result size: " << bv.size() - << "\noperand: " << op.size() << '\n' - << it->pretty() - << '\n'; - - throw "size of value operand does not match"; - } + DATA_INVARIANT( + bv.size() == op.size(), + std::string("size of value operand does not match:\n") + + "result size: " + std::to_string(bv.size()) + + "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty()); literalt value_literal=bv_utils.equal(bv, op); diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 76fa73697b1..11dda842f17 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include - #include #include #include @@ -44,14 +42,12 @@ literalt boolbvt::convert_equality(const equal_exprt &expr) const bvt &bv0=convert_bv(expr.lhs()); const bvt &bv1=convert_bv(expr.rhs()); - if(bv0.size()!=bv1.size()) - { - std::cerr << "lhs: " << expr.lhs().pretty() << '\n'; - std::cerr << "lhs size: " << bv0.size() << '\n'; - std::cerr << "rhs: " << expr.rhs().pretty() << '\n'; - std::cerr << "rhs size: " << bv1.size() << '\n'; - throw "unexpected size mismatch on equality"; - } + 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())); if(bv0.empty()) { @@ -80,14 +76,12 @@ literalt boolbvt::convert_verilog_case_equality( const bvt &bv0=convert_bv(expr.lhs()); const bvt &bv1=convert_bv(expr.rhs()); - if(bv0.size()!=bv1.size()) - { - std::cerr << "lhs: " << expr.lhs().pretty() << '\n'; - std::cerr << "lhs size: " << bv0.size() << '\n'; - std::cerr << "rhs: " << expr.rhs().pretty() << '\n'; - std::cerr << "rhs size: " << bv1.size() << '\n'; - throw "unexpected size mismatch on verilog_case_equality"; - } + DATA_INVARIANT( + bv0.size() == bv1.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())); if(expr.id()==ID_verilog_case_inequality) return !bv_utils.equal(bv0, bv1); diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp index d6609691df2..6f5b762c17d 100644 --- a/src/solvers/flattening/boolbv_floatbv_op.cpp +++ b/src/solvers/flattening/boolbv_floatbv_op.cpp @@ -88,12 +88,9 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr) bvt bv2=convert_bv(op2); const typet &type=ns.follow(expr.type()); - - if(op0.type()!=type || op1.type()!=type) - { - std::cerr << expr.pretty() << '\n'; - throw "float op with mixed types"; - } + DATA_INVARIANT( + op0.type() == type && op1.type() == type, + "float op with mixed types:\n" + expr.pretty()); float_utilst float_utils(prop); From 26ef31cdbeb6875e1ab376670d4ce263f614712e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 6 Mar 2018 17:54:08 +0000 Subject: [PATCH 7/7] Use invariant instead of abort() --- src/cpp/cpp_typecheck_expr.cpp | 27 ++++++++++++-------- src/goto-symex/goto_symex_state.cpp | 9 +++---- src/solvers/refinement/refine_arithmetic.cpp | 2 -- src/util/cmdline.cpp | 11 +++----- 4 files changed, 22 insertions(+), 27 deletions(-) diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 185b6c8b858..a6502391c3e 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -11,7 +11,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck.h" -#include +#ifdef DEBUG +#include +#endif #include #include @@ -20,6 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include #include #include @@ -69,25 +72,27 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr) typecheck_expr_explicit_constructor_call(expr); else if(expr.is_nil()) { - #if 0 +#ifdef DEBUG + std::cerr << "E: " << expr.pretty() << '\n'; std::cerr << "cpp_typecheckt::typecheck_expr_main got nil\n"; - #endif - abort(); +#endif + UNREACHABLE; } else if(expr.id()==ID_code) { - #if 0 +#ifdef DEBUG + std::cerr << "E: " << expr.pretty() << '\n'; std::cerr << "cpp_typecheckt::typecheck_expr_main got code\n"; - #endif - abort(); +#endif + UNREACHABLE; } else if(expr.id()==ID_symbol) { - #if 0 - std::cout << "E: " << expr.pretty() << '\n'; + // ignore here +#ifdef DEBUG + std::cerr << "E: " << expr.pretty() << '\n'; std::cerr << "cpp_typecheckt::typecheck_expr_main got symbol\n"; - abort(); - #endif +#endif } else if(expr.id()=="__is_base_of") { diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index f1c1e325e46..23f7fea3f0b 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -50,12 +50,9 @@ void goto_symex_statet::level0t::operator()( return; const symbolt *s; - - if(ns.lookup(obj_identifier, s)) - { - std::cerr << "level0: failed to find " << obj_identifier << '\n'; - abort(); - } + const bool found_l0 = !ns.lookup(obj_identifier, s); + DATA_INVARIANT( + found_l0, "level0: failed to find " + id2string(obj_identifier)); // don't rename shared variables or functions if(s->type.id()==ID_code || diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index 2d8d0254599..86641b8ffa4 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -226,8 +226,6 @@ void bv_refinementt::check_SAT(approximationt &a) << "==" << integer2binary(result.pack(), spec.width()) << eom; #endif - // if(a.over_state==1) { debug() << "DISAGREEMENT!\n"; exit(1); } - if(a.over_state -#include -#include +#include cmdlinet::cmdlinet() { @@ -124,11 +122,8 @@ bool cmdlinet::parse(int argc, const char **argv, const char *optstring) { optiont option; - if(optstring[0]==':') - { - std::cerr << "cmdlinet::parse: Invalid option string\n"; - abort(); - } + DATA_INVARIANT( + optstring[0] != ':', "cmdlinet::parse: Invalid option string\n"); if(optstring[0]=='(') {