From 3dcaff73becaa59cdd47c176d6cb4802c9d4a034 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 21 Sep 2018 15:49:02 +0100 Subject: [PATCH 1/7] Use src/index instead of operand position in boolbv_extractbit --- src/solvers/flattening/boolbv_extractbit.cpp | 22 ++++++++------------ 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp index a2da9cc3352..43119ac6f66 100644 --- a/src/solvers/flattening/boolbv_extractbit.cpp +++ b/src/solvers/flattening/boolbv_extractbit.cpp @@ -17,19 +17,14 @@ Author: Daniel Kroening, kroening@kroening.com literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) { - const exprt::operandst &operands=expr.operands(); - - if(operands.size()!=2) - throw "extractbit takes two operands"; - - const bvt &bv0=convert_bv(operands[0]); + const bvt &bv0 = convert_bv(expr.src()); // constant? - if(operands[1].is_constant()) + if(expr.index().is_constant()) { mp_integer o; - if(to_integer(operands[1], o)) + if(to_integer(expr.index(), o)) throw "extractbit failed to convert constant index"; if(o<0 || o>=bv0.size()) @@ -38,16 +33,17 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) return bv0[integer2size_t(o)]; } - if(operands[0].type().id()==ID_verilog_signedbv || - operands[0].type().id()==ID_verilog_unsignedbv) + if( + expr.src().type().id() == ID_verilog_signedbv || + expr.src().type().id() == ID_verilog_unsignedbv) { // TODO assert(false); } else { - std::size_t width_op0=boolbv_width(operands[0].type()); - std::size_t width_op1=boolbv_width(operands[1].type()); + std::size_t width_op0 = boolbv_width(expr.src().type()); + std::size_t width_op1 = boolbv_width(expr.index().type()); if(width_op0==0 || width_op1==0) return SUB::convert_rest(expr); @@ -56,7 +52,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) unsignedbv_typet index_type(index_width); equal_exprt equality; - equality.lhs()=operands[1]; // index operand + equality.lhs() = expr.index(); if(index_type!=equality.lhs().type()) equality.lhs().make_typecast(index_type); From 10cab6a0ce2368d3d8121d776cd1155adc673468 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 24 Sep 2018 11:04:19 +0100 Subject: [PATCH 2/7] Rename some local variables in boolbv_extractbit Using semantic names for operators instead of their position and expanding single letter abbreviations should help with legibility. --- src/solvers/flattening/boolbv_extractbit.cpp | 35 ++++++++++---------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp index 43119ac6f66..09f800ae703 100644 --- a/src/solvers/flattening/boolbv_extractbit.cpp +++ b/src/solvers/flattening/boolbv_extractbit.cpp @@ -17,20 +17,20 @@ Author: Daniel Kroening, kroening@kroening.com literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) { - const bvt &bv0 = convert_bv(expr.src()); + const bvt &src_bv = convert_bv(expr.src()); // constant? if(expr.index().is_constant()) { - mp_integer o; + mp_integer index_as_integer; - if(to_integer(expr.index(), o)) + if(to_integer(expr.index(), index_as_integer)) throw "extractbit failed to convert constant index"; - if(o<0 || o>=bv0.size()) + if(index_as_integer < 0 || index_as_integer >= src_bv.size()) return prop.new_variable(); // out of range! else - return bv0[integer2size_t(o)]; + return src_bv[integer2size_t(index_as_integer)]; } if( @@ -42,13 +42,14 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) } else { - std::size_t width_op0 = boolbv_width(expr.src().type()); - std::size_t width_op1 = boolbv_width(expr.index().type()); + std::size_t src_bv_width = boolbv_width(expr.src().type()); + std::size_t index_bv_width = boolbv_width(expr.index().type()); - if(width_op0==0 || width_op1==0) + if(src_bv_width == 0 || index_bv_width == 0) return SUB::convert_rest(expr); - std::size_t index_width = std::max(address_bits(width_op0), width_op1); + std::size_t index_width = + std::max(address_bits(src_bv_width), index_bv_width); unsignedbv_typet index_type(index_width); equal_exprt equality; @@ -60,29 +61,29 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) if(prop.has_set_to()) { // free variable - literalt l=prop.new_variable(); + literalt literal = prop.new_variable(); // add implications - for(std::size_t i=0; i Date: Mon, 24 Sep 2018 11:34:12 +0100 Subject: [PATCH 3/7] Replace throw and assert in boolbv_extractbit The throw was on checking if a constant expression with extractbit was a valid integer expression. The assert was signaling that we didn't support a type of expression so has been replaced with a throw of the appropriate exception type --- src/solvers/flattening/boolbv_extractbit.cpp | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp index 09f800ae703..ce4637340fe 100644 --- a/src/solvers/flattening/boolbv_extractbit.cpp +++ b/src/solvers/flattening/boolbv_extractbit.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -22,10 +23,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) // constant? if(expr.index().is_constant()) { - mp_integer index_as_integer; - - if(to_integer(expr.index(), index_as_integer)) - throw "extractbit failed to convert constant index"; + mp_integer index_as_integer = numeric_cast_v(expr.index()); if(index_as_integer < 0 || index_as_integer >= src_bv.size()) return prop.new_variable(); // out of range! @@ -37,8 +35,9 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) expr.src().type().id() == ID_verilog_signedbv || expr.src().type().id() == ID_verilog_unsignedbv) { - // TODO - assert(false); + throw unsupported_operation_exceptiont( + "extractbit expression not implemented for verilog integers in " + "flattening solver"); } else { From 550f37c94f864e862afa61159c501e014c06087c Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 24 Sep 2018 13:23:39 +0100 Subject: [PATCH 4/7] Rename variables in boolbv_extractbits for easier readability --- src/solvers/flattening/boolbv_extractbits.cpp | 42 ++++++++++--------- 1 file changed, 22 insertions(+), 20 deletions(-) diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index 4f549139feb..61d511d0135 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) { - std::size_t width=boolbv_width(expr.type()); + const std::size_t bv_width = boolbv_width(expr.type()); - if(width==0) + if(bv_width == 0) return conversion_failed(expr); if(expr.operands().size()!=3) @@ -24,23 +24,24 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) throw 0; } - mp_integer o1, o2; - const bvt &bv0=convert_bv(expr.op0()); + mp_integer upper_as_int, lower_as_int; + auto const &src_bv = convert_bv(expr.src()); // We only do constants for now. // Should implement a shift here. - if(to_integer(expr.op1(), o1) || - to_integer(expr.op2(), o2)) + if( + to_integer(expr.op1(), upper_as_int) || + to_integer(expr.op2(), lower_as_int)) return conversion_failed(expr); - if(o1<0 || o1>=bv0.size()) + if(upper_as_int < 0 || upper_as_int >= src_bv.size()) { error().source_location=expr.find_source_location(); error() << "extractbits: second operand out of range: " << expr.pretty() << eom; } - if(o2<0 || o2>=bv0.size()) + if(lower_as_int < 0 || lower_as_int >= src_bv.size()) { error().source_location=expr.find_source_location(); error() << "extractbits: third operand out of range: " @@ -48,26 +49,27 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) throw 0; } - if(o2>o1) - std::swap(o1, o2); + if(lower_as_int > upper_as_int) + std::swap(upper_as_int, lower_as_int); - // now o2<=o1 + // now lower_as_int <= upper_as_int - if((o1-o2+1)!=width) + if((upper_as_int - lower_as_int + 1) != bv_width) { error().source_location=expr.find_source_location(); - error() << "extractbits: wrong width (expected " << (o1-o2+1) - << " but got " << width << "): " << expr.pretty() << eom; + error() << "extractbits: wrong width (expected " + << (upper_as_int - lower_as_int + 1) << " but got " << bv_width + << "): " << expr.pretty() << eom; throw 0; } - std::size_t offset=integer2unsigned(o2); + const std::size_t offset = integer2unsigned(lower_as_int); - bvt bv; - bv.resize(width); + bvt result_bv; + result_bv.resize(bv_width); - for(std::size_t i=0; i Date: Mon, 24 Sep 2018 13:59:52 +0100 Subject: [PATCH 5/7] Replace to_integer with numeric_cast in extractbits_expr This allows us to be a bit more explicit in the code with `has_value` rather than using an "anonymous" boolean result. --- src/solvers/flattening/boolbv_extractbits.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index 61d511d0135..5c9dbe1bc9b 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -24,16 +24,19 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) throw 0; } - mp_integer upper_as_int, lower_as_int; auto const &src_bv = convert_bv(expr.src()); + auto const maybe_upper_as_int = numeric_cast(expr.upper()); + auto const maybe_lower_as_int = numeric_cast(expr.lower()); + // We only do constants for now. // Should implement a shift here. - if( - to_integer(expr.op1(), upper_as_int) || - to_integer(expr.op2(), lower_as_int)) + if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value()) return conversion_failed(expr); + auto upper_as_int = maybe_upper_as_int.value(); + auto lower_as_int = maybe_lower_as_int.value(); + if(upper_as_int < 0 || upper_as_int >= src_bv.size()) { error().source_location=expr.find_source_location(); From af0eb45300f8208a604927063e7420624d3a5392 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 24 Sep 2018 14:46:04 +0100 Subject: [PATCH 6/7] Replace throws with invariants in boolbv_extractbits Also removes one throw that guards against violation of extractbits_expr invariants --- src/solvers/flattening/boolbv_extractbits.cpp | 46 +++++++------------ 1 file changed, 17 insertions(+), 29 deletions(-) diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index 5c9dbe1bc9b..a0fdce4dbaa 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -17,13 +17,6 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) if(bv_width == 0) return conversion_failed(expr); - if(expr.operands().size()!=3) - { - error().source_location=expr.find_source_location(); - error() << "extractbits takes three operands" << eom; - throw 0; - } - auto const &src_bv = convert_bv(expr.src()); auto const maybe_upper_as_int = numeric_cast(expr.upper()); @@ -37,34 +30,29 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) auto upper_as_int = maybe_upper_as_int.value(); auto lower_as_int = maybe_lower_as_int.value(); - if(upper_as_int < 0 || upper_as_int >= src_bv.size()) - { - error().source_location=expr.find_source_location(); - error() << "extractbits: second operand out of range: " - << expr.pretty() << eom; - } - - if(lower_as_int < 0 || lower_as_int >= src_bv.size()) - { - error().source_location=expr.find_source_location(); - error() << "extractbits: third operand out of range: " - << expr.pretty() << eom; - throw 0; - } + DATA_INVARIANT_WITH_DIAGNOSTICS( + upper_as_int >= 0 && upper_as_int < src_bv.size(), + "upper end of extracted bits must be within the bitvector", + expr.find_source_location(), + irep_pretty_diagnosticst{expr}); + + DATA_INVARIANT_WITH_DIAGNOSTICS( + lower_as_int >= 0 && lower_as_int < src_bv.size(), + "lower end of extracted bits must be within the bitvector", + expr.find_source_location(), + irep_pretty_diagnosticst{expr}); if(lower_as_int > upper_as_int) std::swap(upper_as_int, lower_as_int); // now lower_as_int <= upper_as_int - if((upper_as_int - lower_as_int + 1) != bv_width) - { - error().source_location=expr.find_source_location(); - error() << "extractbits: wrong width (expected " - << (upper_as_int - lower_as_int + 1) << " but got " << bv_width - << "): " << expr.pretty() << eom; - throw 0; - } + DATA_INVARIANT_WITH_DIAGNOSTICS( + (upper_as_int - lower_as_int + 1) == bv_width, + "the difference between upper and lower end of the range must have the " + "same width as the resulting bitvector type", + expr.find_source_location(), + irep_pretty_diagnosticst{expr}); const std::size_t offset = integer2unsigned(lower_as_int); From 9423a5ce38cb27ce92ef604f218f2c5a0438f269 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Wed, 26 Sep 2018 12:54:42 +0100 Subject: [PATCH 7/7] Use bvt constructor instead of manual loop for initialisation --- src/solvers/flattening/boolbv_extractbits.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index a0fdce4dbaa..0ad828bbca4 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -56,11 +56,7 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) const std::size_t offset = integer2unsigned(lower_as_int); - bvt result_bv; - result_bv.resize(bv_width); - - for(std::size_t i = 0; i < bv_width; i++) - result_bv[i] = src_bv[offset + i]; + bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width); return result_bv; }