From 2dc7beea3792276f7acf21693412483bdc65d2a4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 15:34:27 +0000 Subject: [PATCH 1/6] Replacing throws by invariants in boolbv convert --- src/solvers/flattening/boolbv.cpp | 79 ++++++++----------------------- 1 file changed, 20 insertions(+), 59 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index adc20b6144f..6d597ec1c5e 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -433,13 +433,7 @@ bvt boolbvt::convert_function_application( literalt boolbvt::convert_rest(const exprt &expr) { - if(expr.type().id()!=ID_bool) - { - error() << "boolbvt::convert_rest got non-boolean operand: " - << expr.pretty() << eom; - throw 0; - } - + PRECONDITION(expr.type().id() == ID_bool); const exprt::operandst &operands=expr.operands(); if(expr.id()==ID_typecast) @@ -451,9 +445,7 @@ literalt boolbvt::convert_rest(const exprt &expr) return convert_verilog_case_equality(to_binary_relation_expr(expr)); else if(expr.id()==ID_notequal) { - if(expr.operands().size()!=2) - throw "notequal expects two operands"; - + DATA_INVARIANT(expr.operands().size() == 2, "notequal expects two operands"); return !convert_equality(equal_exprt(expr.op0(), expr.op1())); } else if(expr.id()==ID_ieee_float_equal || @@ -480,57 +472,37 @@ literalt boolbvt::convert_rest(const exprt &expr) else if(expr.id()==ID_index) { bvt bv=convert_index(to_index_expr(expr)); - - if(bv.size()!=1) - throw "convert_index returned non-bool bitvector"; - + CHECK_RETURN(bv.size() == 1); return bv[0]; } else if(expr.id()==ID_member) { bvt bv=convert_member(to_member_expr(expr)); - - if(bv.size()!=1) - throw "convert_member returned non-bool bitvector"; - + CHECK_RETURN(bv.size() == 1); return bv[0]; } else if(expr.id()==ID_case) { bvt bv=convert_case(expr); - - if(bv.size()!=1) - throw "convert_case returned non-bool bitvector"; - + CHECK_RETURN(bv.size() == 1); return bv[0]; } else if(expr.id()==ID_cond) { bvt bv=convert_cond(expr); - - if(bv.size()!=1) - throw "convert_cond returned non-bool bitvector"; - + CHECK_RETURN(bv.size() == 1); return bv[0]; } else if(expr.id()==ID_sign) { - if(expr.operands().size()!=1) - throw "sign expects one operand"; - + DATA_INVARIANT(expr.operands().size() == 1, "sign expects one operand"); const bvt &bv=convert_bv(operands[0]); - - if(bv.empty()) - throw "sign operator takes one non-empty operand"; - - if(operands[0].type().id()==ID_signedbv) + CHECK_RETURN(!bv.empty()); + const irep_idt type_id = operands[0].type().id(); + if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv) return bv[bv.size()-1]; - else if(operands[0].type().id()==ID_unsignedbv) + if(type_id == ID_unsignedbv) return const_literal(false); - else if(operands[0].type().id()==ID_fixedbv) - return bv[bv.size()-1]; - else if(operands[0].type().id()==ID_floatbv) - return bv[bv.size()-1]; } else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and || expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand || @@ -542,9 +514,7 @@ literalt boolbvt::convert_rest(const exprt &expr) return convert_overflow(expr); else if(expr.id()==ID_isnan) { - if(expr.operands().size()!=1) - throw "isnan expects one operand"; - + DATA_INVARIANT(expr.operands().size() == 1, "isnan expects one operand"); const bvt &bv=convert_bv(operands[0]); if(expr.op0().type().id()==ID_floatbv) @@ -552,16 +522,13 @@ literalt boolbvt::convert_rest(const exprt &expr) float_utilst float_utils(prop, to_floatbv_type(expr.op0().type())); return float_utils.is_NaN(bv); } - else if(expr.op0().type().id()==ID_fixedbv) + else if(expr.op0().type().id() == ID_fixedbv) return const_literal(false); } else if(expr.id()==ID_isfinite) { - if(expr.operands().size()!=1) - throw "isfinite expects one operand"; - + DATA_INVARIANT(expr.operands().size() == 1, "isfinite expects one operand"); const bvt &bv=convert_bv(operands[0]); - if(expr.op0().type().id()==ID_floatbv) { float_utilst float_utils(prop, to_floatbv_type(expr.op0().type())); @@ -569,37 +536,31 @@ literalt boolbvt::convert_rest(const exprt &expr) !float_utils.is_infinity(bv), !float_utils.is_NaN(bv)); } - else if(expr.op0().type().id()==ID_fixedbv) + else if(expr.op0().type().id() == ID_fixedbv) return const_literal(true); } else if(expr.id()==ID_isinf) { - if(expr.operands().size()!=1) - throw "isinf expects one operand"; - + DATA_INVARIANT(expr.operands().size() == 1, "isinf expects one operand"); const bvt &bv=convert_bv(operands[0]); - if(expr.op0().type().id()==ID_floatbv) { float_utilst float_utils(prop, to_floatbv_type(expr.op0().type())); return float_utils.is_infinity(bv); } - else if(expr.op0().type().id()==ID_fixedbv) + else if(expr.op0().type().id() == ID_fixedbv) return const_literal(false); } else if(expr.id()==ID_isnormal) { - if(expr.operands().size()!=1) - throw "isnormal expects one operand"; - - const bvt &bv=convert_bv(operands[0]); - + DATA_INVARIANT(expr.operands().size() == 1, "isnormal expects one operand"); if(expr.op0().type().id()==ID_floatbv) { + const bvt &bv = convert_bv(operands[0]); float_utilst float_utils(prop, to_floatbv_type(expr.op0().type())); return float_utils.is_normal(bv); } - else if(expr.op0().type().id()==ID_fixedbv) + else if(expr.op0().type().id() == ID_fixedbv) return const_literal(true); } From 52d0fe4dfa5093928d9603a2b7534cf81eb36454 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 15:39:03 +0000 Subject: [PATCH 2/6] Make build_offset_map return an offset_mapt --- src/solvers/flattening/boolbv.cpp | 19 +++++++++---------- src/solvers/flattening/boolbv.h | 2 +- src/solvers/flattening/boolbv_typecast.cpp | 6 ++---- 3 files changed, 12 insertions(+), 15 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 6d597ec1c5e..f6438834896 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -660,17 +660,16 @@ void boolbvt::print_assignment(std::ostream &out) const out << pair.first << "=" << pair.second.get_value(prop) << '\n'; } -void boolbvt::build_offset_map(const struct_typet &src, offset_mapt &dest) +boolbvt::offset_mapt boolbvt::build_offset_map(const struct_typet &src) { - const struct_typet::componentst &components= - src.components(); - - dest.resize(components.size()); - std::size_t offset=0; - for(std::size_t i=0; i offset_mapt; - void build_offset_map(const struct_typet &src, offset_mapt &dest); + offset_mapt build_offset_map(const struct_typet &src); // strings numbering string_numbering; diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index 838c8df84ac..724b59b6a78 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -530,10 +530,8 @@ bool boolbvt::type_conversion( op_struct.components(); // build offset maps - offset_mapt op_offsets, dest_offsets; - - build_offset_map(op_struct, op_offsets); - build_offset_map(dest_struct, dest_offsets); + const offset_mapt op_offsets = build_offset_map(op_struct); + const offset_mapt dest_offsets = build_offset_map(dest_struct); // build name map typedef std::map op_mapt; From b837b8abb182085fab19ec2f90c8e58e9a27fd79 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 15:41:29 +0000 Subject: [PATCH 3/6] Remove useless throws in boolbvt::convert_index These invariant should already be ensured by the type. --- src/solvers/flattening/boolbv_index.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index ba5b70e52b8..ca66fb2c697 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -17,12 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com bvt boolbvt::convert_index(const index_exprt &expr) { - if(expr.id()!=ID_index) - throw "expected index expression"; - - if(expr.operands().size()!=2) - throw "index takes two operands"; - const exprt &array=expr.array(); const exprt &index=expr.index(); From adc2d5d13eca95bac400e35cf53d5219feab5386 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Feb 2018 06:37:40 +0000 Subject: [PATCH 4/6] Make convert_abs take an abs_exprt parameter --- src/solvers/flattening/boolbv.cpp | 2 +- src/solvers/flattening/boolbv.h | 2 +- src/solvers/flattening/boolbv_abs.cpp | 17 +++++------------ 3 files changed, 7 insertions(+), 14 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index f6438834896..219e372afcf 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -253,7 +253,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr) return convert_bitvector(expr.op0()); } else if(expr.id()==ID_abs) - return convert_abs(expr); + return convert_abs(to_abs_expr(expr)); else if(expr.id() == ID_bswap) return convert_bswap(to_bswap_expr(expr)); else if(expr.id()==ID_byte_extract_little_endian || diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 17c487594aa..429a5aa4b37 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -163,7 +163,7 @@ class boolbvt:public arrayst virtual bvt convert_shift(const binary_exprt &expr); virtual bvt convert_bitwise(const exprt &expr); virtual bvt convert_unary_minus(const unary_exprt &expr); - virtual bvt convert_abs(const exprt &expr); + virtual bvt convert_abs(const abs_exprt &expr); virtual bvt convert_concatenation(const exprt &expr); virtual bvt convert_replication(const replication_exprt &expr); virtual bvt convert_bv_literals(const exprt &expr); diff --git a/src/solvers/flattening/boolbv_abs.cpp b/src/solvers/flattening/boolbv_abs.cpp index 1caabde0fa4..e43451f282e 100644 --- a/src/solvers/flattening/boolbv_abs.cpp +++ b/src/solvers/flattening/boolbv_abs.cpp @@ -14,26 +14,19 @@ Author: Daniel Kroening, kroening@kroening.com #include -bvt boolbvt::convert_abs(const exprt &expr) +bvt boolbvt::convert_abs(const abs_exprt &expr) { - std::size_t width=boolbv_width(expr.type()); + const std::size_t width = boolbv_width(expr.type()); if(width==0) return conversion_failed(expr); - const exprt::operandst &operands=expr.operands(); + const bvt &op_bv=convert_bv(expr.op()); - if(operands.size()!=1) - throw "abs takes one operand"; - - const exprt &op0=expr.op0(); - - const bvt &op_bv=convert_bv(op0); - - if(op0.type()!=expr.type()) + if(expr.op().type()!=expr.type()) return conversion_failed(expr); - bvtypet bvtype=get_bvtype(expr.type()); + const bvtypet bvtype = get_bvtype(expr.type()); if(bvtype==bvtypet::IS_FIXED || bvtype==bvtypet::IS_SIGNED || From 1b43ee98060c6f826e95fc698cdb1ae476339a18 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Feb 2018 06:39:22 +0000 Subject: [PATCH 5/6] Refactoring in boolbvt::convert_bitwise --- src/solvers/flattening/boolbv_bitwise.cpp | 21 ++++++--------------- 1 file changed, 6 insertions(+), 15 deletions(-) diff --git a/src/solvers/flattening/boolbv_bitwise.cpp b/src/solvers/flattening/boolbv_bitwise.cpp index 9eda6eafcd9..33d4a1c2021 100644 --- a/src/solvers/flattening/boolbv_bitwise.cpp +++ b/src/solvers/flattening/boolbv_bitwise.cpp @@ -11,23 +11,16 @@ Author: Daniel Kroening, kroening@kroening.com bvt boolbvt::convert_bitwise(const exprt &expr) { - std::size_t width=boolbv_width(expr.type()); - + const std::size_t width = boolbv_width(expr.type()); if(width==0) return conversion_failed(expr); if(expr.id()==ID_bitnot) { - if(expr.operands().size()!=1) - throw "bitnot takes one operand"; - + DATA_INVARIANT(expr.operands().size() == 1, "bitnot takes one operand"); const exprt &op0=expr.op0(); - const bvt &op_bv=convert_bv(op0); - - if(op_bv.size()!=width) - throw "convert_bitwise: unexpected operand width"; - + CHECK_RETURN(op_bv.size() == width); return bv_utils.inverted(op_bv); } else if(expr.id()==ID_bitand || expr.id()==ID_bitor || @@ -41,9 +34,7 @@ bvt boolbvt::convert_bitwise(const exprt &expr) forall_operands(it, expr) { const bvt &op=convert_bv(*it); - - if(op.size()!=width) - throw "convert_bitwise: unexpected operand width"; + CHECK_RETURN(op.size() == width); if(it==expr.operands().begin()) bv=op; @@ -64,7 +55,7 @@ bvt boolbvt::convert_bitwise(const exprt &expr) else if(expr.id()==ID_bitxnor) bv[i]=prop.lequal(bv[i], op[i]); else - throw "unexpected operand"; + UNIMPLEMENTED; } } } @@ -72,5 +63,5 @@ bvt boolbvt::convert_bitwise(const exprt &expr) return bv; } - throw "unexpected bitwise operand"; + UNIMPLEMENTED; } From d35c2acc40d7e05721bf546af7e59fd3782f4fd6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Feb 2018 06:40:04 +0000 Subject: [PATCH 6/6] Refactoring in boolbvt::convert_byte_extract --- .../flattening/boolbv_byte_extract.cpp | 35 +++++-------------- 1 file changed, 9 insertions(+), 26 deletions(-) diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index b489a9b1924..86fd36231f9 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -23,16 +23,15 @@ Author: Daniel Kroening, kroening@kroening.com bvt map_bv(const bv_endianness_mapt &map, const bvt &src) { - assert(map.number_of_bits()==src.size()); - + PRECONDITION(map.number_of_bits() == src.size()); bvt result; - result.resize(src.size(), const_literal(false)); + result.reserve(src.size()); for(std::size_t i=0; i