From 848e633b6770d96f7761a08c862b829cc2515384 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 11 Apr 2019 22:47:05 +0000 Subject: [PATCH] Use bv_typet to fix type consistency in byte-operator lowering Previously we fixed the extracted bytes to be unsigned bitvectors, but we should not actually impose (un)signedness as we do not actually interpret the bytes as numeric values. This fixes byte operators over floating-point values, and makes various SMT-solver tests pass as the SMT back-end is more strict about typing and therefore was more frequently affected by this bug. To make all this work it was also necessary to extend and fix the simplifier's handling of bv_typet expressions, and also cover one more case of type casts in the bitvector back-end. The tests Array_operations1/test.desc Float-equality1/test_no_equality.desc memory_allocation1/test.desc union12/test.desc union6/test.desc union7/test.desc continue to fail on Windows and thus cannot yet be enabled. --- regression/cbmc/Bitfields3/paths.desc | 3 + regression/cbmc/Bitfields3/test.desc | 2 +- regression/cbmc/Malloc23/test.desc | 2 +- .../cbmc/Pointer_Arithmetic11/test.desc | 2 +- .../cbmc/Pointer_byte_extract2/test.desc | 2 +- .../cbmc/Pointer_byte_extract9/test.desc | 2 +- .../cbmc/Quantifiers-assignment/test.desc | 2 +- regression/cbmc/byte_update3/test.desc | 2 +- regression/cbmc/byte_update5/test.desc | 2 +- regression/cbmc/memory_allocation2/test.desc | 2 +- src/solvers/flattening/boolbv_typecast.cpp | 7 + src/solvers/lowering/byte_operators.cpp | 128 +++++++++--------- src/solvers/smt2/smt2_conv.cpp | 5 +- src/util/simplify_expr.cpp | 50 ++++++- src/util/simplify_expr_int.cpp | 16 ++- unit/solvers/lowering/byte_operators.cpp | 7 +- 16 files changed, 143 insertions(+), 91 deletions(-) diff --git a/regression/cbmc/Bitfields3/paths.desc b/regression/cbmc/Bitfields3/paths.desc index c6d543290f7..00d29f0d4fb 100644 --- a/regression/cbmc/Bitfields3/paths.desc +++ b/regression/cbmc/Bitfields3/paths.desc @@ -6,3 +6,6 @@ main.c ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring +-- +This test is marked broken-smt-backend for performance reasons only: it passes, +but takes 5 seconds to do so. diff --git a/regression/cbmc/Bitfields3/test.desc b/regression/cbmc/Bitfields3/test.desc index 35db6e71ddb..96c9b4bcd7b 100644 --- a/regression/cbmc/Bitfields3/test.desc +++ b/regression/cbmc/Bitfields3/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc index 47408244d66..a190cab817e 100644 --- a/regression/cbmc/Malloc23/test.desc +++ b/regression/cbmc/Malloc23/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/Pointer_Arithmetic11/test.desc b/regression/cbmc/Pointer_Arithmetic11/test.desc index b0acb9b5913..f5e039ba3ed 100644 --- a/regression/cbmc/Pointer_Arithmetic11/test.desc +++ b/regression/cbmc/Pointer_Arithmetic11/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --pointer-check --little-endian ^EXIT=0$ diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc index e6619de477a..eb98d4f78ba 100644 --- a/regression/cbmc/Pointer_byte_extract2/test.desc +++ b/regression/cbmc/Pointer_byte_extract2/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --little-endian ^EXIT=10$ diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc index 61e6035ff74..0570ab7aba7 100644 --- a/regression/cbmc/Pointer_byte_extract9/test.desc +++ b/regression/cbmc/Pointer_byte_extract9/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=10$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index 998d3865da2..a584f718857 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^\*\* Results:$ diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc index 9d95b7efe83..9845e70d84b 100644 --- a/regression/cbmc/byte_update3/test.desc +++ b/regression/cbmc/byte_update3/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc index 9d95b7efe83..9845e70d84b 100644 --- a/regression/cbmc/byte_update5/test.desc +++ b/regression/cbmc/byte_update5/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --little-endian ^EXIT=0$ diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index a821e1b3264..ff8497a9af5 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --bounds-check ^EXIT=10$ diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index cfbe1221019..97cedc85b38 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -415,6 +415,13 @@ bool boolbvt::type_conversion( } break; + case bvtypet::IS_BV: + INVARIANT( + src_width == dest_width, + "source bitvector with shall equal the destination bitvector width"); + dest=src; + return false; + default: if(src_type.id()==ID_bool) { diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 9dac8ffe747..d46b046d9d1 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -274,8 +274,11 @@ static exprt bv_to_expr( target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag || target_type.id() == ID_string) { + std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width(); + exprt bv_expr = + typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width}); return simplify_expr( - typecast_exprt::conditional_cast(bitvector_expr, target_type), ns); + typecast_exprt::conditional_cast(bv_expr, target_type), ns); } if(target_type.id() == ID_struct) @@ -371,7 +374,7 @@ static array_exprt unpack_array_vector( // insert offset_bytes-many nil bytes into the output array byte_operands.resize( numeric_cast_v(*offset_bytes - (*offset_bytes % el_bytes)), - from_integer(0, unsignedbv_typet(8))); + from_integer(0, bv_typet{8})); } } @@ -409,7 +412,7 @@ static array_exprt unpack_array_vector( const std::size_t size = byte_operands.size(); return array_exprt( std::move(byte_operands), - array_typet(unsignedbv_typet(8), from_integer(size, size_type()))); + array_typet{bv_typet{8}, from_integer(size, size_type())}); } /// Extract bytes from a sequence of bitvector-typed elements. @@ -432,7 +435,7 @@ static void process_bit_fields( const namespacet &ns) { const concatenation_exprt concatenation{std::move(bit_fields), - unsignedbv_typet{total_bits}}; + bv_typet{total_bits}}; exprt sub = unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns, true); @@ -530,7 +533,7 @@ static array_exprt unpack_struct( const std::size_t bits_int = numeric_cast_v(*component_bits); bit_fields->first.insert( little_endian ? bit_fields->first.begin() : bit_fields->first.end(), - typecast_exprt::conditional_cast(member, unsignedbv_typet{bits_int})); + typecast_exprt::conditional_cast(member, bv_typet{bits_int})); bit_fields->second += bits_int; member_offset_bits += *component_bits; @@ -565,9 +568,8 @@ static array_exprt unpack_struct( ns); const std::size_t size = byte_operands.size(); - return array_exprt{ - std::move(byte_operands), - array_typet{unsignedbv_typet{8}, from_integer(size, size_type())}}; + return array_exprt{std::move(byte_operands), + array_typet{bv_typet{8}, from_integer(size, size_type())}}; } /// Rewrite a complex_exprt into its individual bytes. @@ -607,9 +609,8 @@ unpack_complex(const exprt &src, bool little_endian, const namespacet &ns) std::make_move_iterator(sub_imag.operands().end())); const std::size_t size = byte_operands.size(); - return array_exprt{ - std::move(byte_operands), - array_typet{unsignedbv_typet(8), from_integer(size, size_type())}}; + return array_exprt{std::move(byte_operands), + array_typet{bv_typet{8}, from_integer(size, size_type())}}; } /// Rewrite an object into its individual bytes. @@ -713,8 +714,7 @@ static exprt unpack_rec( else if(src.type().id() == ID_pointer) { return unpack_rec( - typecast_exprt( - src, unsignedbv_typet(to_pointer_type(src.type()).get_width())), + typecast_exprt{src, bv_typet{to_pointer_type(src.type()).get_width()}}, little_endian, offset_bytes, max_bytes, @@ -759,10 +759,11 @@ static exprt unpack_rec( for(mp_integer i=0; i(bits)}), + from_integer(i + 7, index_type()), from_integer(i, index_type()), - unsignedbv_typet(8)); + bv_typet{8}); // endianness_mapt should be the point of reference for mapping out // endianness, but we need to work on elements here instead of @@ -776,11 +777,11 @@ static exprt unpack_rec( const std::size_t size = byte_operands.size(); return array_exprt( std::move(byte_operands), - array_typet(unsignedbv_typet(8), from_integer(size, size_type()))); + array_typet{bv_typet{8}, from_integer(size, size_type())}); } return array_exprt( - {}, array_typet(unsignedbv_typet(8), from_integer(0, size_type()))); + {}, array_typet{bv_typet{8}, from_integer(0, size_type())}); } /// Rewrite a byte extraction of a complex-typed result to byte extraction of @@ -1258,7 +1259,7 @@ static exprt lower_byte_update_array_vector_non_const( byte_extract_exprt{extract_opcode, value_as_byte_array, from_integer(0, src.offset().type()), - array_typet{unsignedbv_typet{8}, initial_bytes}}}, + array_typet{bv_typet{8}, initial_bytes}}}, ns)}; // We will update one array/vector element at a time - compute the number of @@ -1298,7 +1299,7 @@ static exprt lower_byte_update_array_vector_non_const( byte_extract_exprt{extract_opcode, value_as_byte_array, std::move(offset_expr), - array_typet{unsignedbv_typet{8}, subtype_size}}}, + array_typet{bv_typet{8}, subtype_size}}}, ns); result.add_to_operands(std::move(where), std::move(element)); @@ -1318,11 +1319,11 @@ static exprt lower_byte_update_array_vector_non_const( src.id(), index_exprt{src.op(), where}, from_integer(0, src.offset().type()), - byte_extract_exprt{extract_opcode, - value_as_byte_array, - from_integer(offset, src.offset().type()), - array_typet{unsignedbv_typet{8}, - from_integer(tail_size, size_type())}}}, + byte_extract_exprt{ + extract_opcode, + value_as_byte_array, + from_integer(offset, src.offset().type()), + array_typet{bv_typet{8}, from_integer(tail_size, size_type())}}}, ns); result.add_to_operands(std::move(where), std::move(element)); @@ -1414,9 +1415,9 @@ static exprt lower_byte_update_array_vector( src.id(), index_exprt{src.op(), from_integer(i, index_type())}, from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()), - array_exprt{std::move(update_values), - array_typet{unsignedbv_typet{8}, - from_integer(update_size, size_type())}}}; + array_exprt{ + std::move(update_values), + array_typet{bv_typet{8}, from_integer(update_size, size_type())}}}; elements.push_back(lower_byte_operators(bu, ns)); } @@ -1493,21 +1494,18 @@ static exprt lower_byte_update_struct( extract_opcode, src.op(), from_integer(0, src.offset().type()), - array_typet{unsignedbv_typet{8}, src_size_opt.value()}}; + array_typet{bv_typet{8}, src_size_opt.value()}}; byte_update_exprt bu = src; bu.op() = lower_byte_extract(byte_extract_expr, ns); return lower_byte_extract( - byte_extract_exprt{extract_opcode, - lower_byte_update_byte_array_vector( - bu, - unsignedbv_typet{8}, - value_as_byte_array, - non_const_update_bound, - ns), - from_integer(0, src.offset().type()), - src.type()}, + byte_extract_exprt{ + extract_opcode, + lower_byte_update_byte_array_vector( + bu, bv_typet{8}, value_as_byte_array, non_const_update_bound, ns), + from_integer(0, src.offset().type()), + src.type()}, ns); } @@ -1544,11 +1542,10 @@ static exprt lower_byte_update_struct( const bool little_endian = src.id() == ID_byte_update_little_endian; if(shift != 0) { - member = - concatenation_exprt{typecast_exprt::conditional_cast( - member, unsignedbv_typet{element_bits_int}), - from_integer(0, unsignedbv_typet{shift}), - unsignedbv_typet{shift + element_bits_int}}; + member = concatenation_exprt{ + typecast_exprt::conditional_cast(member, bv_typet{element_bits_int}), + from_integer(0, bv_typet{shift}), + bv_typet{shift + element_bits_int}}; if(!little_endian) member.op0().swap(member.op1()); } @@ -1557,9 +1554,9 @@ static exprt lower_byte_update_struct( src.id(), std::move(member), offset, - array_exprt{std::move(update_values), - array_typet{unsignedbv_typet{8}, - from_integer(update_size, size_type())}}}; + array_exprt{ + std::move(update_values), + array_typet{bv_typet{8}, from_integer(update_size, size_type())}}}; if(shift == 0) elements.push_back(lower_byte_operators(bu, ns)); @@ -1569,7 +1566,7 @@ static exprt lower_byte_update_struct( extractbits_exprt{lower_byte_operators(bu, ns), element_bits_int - 1 + (little_endian ? shift : 0), (little_endian ? shift : 0), - unsignedbv_typet{element_bits_int}}, + bv_typet{element_bits_int}}, comp.type())); } @@ -1701,12 +1698,12 @@ static exprt lower_byte_update( // build mask exprt mask; if(is_little_endian) - mask = - from_integer(power(2, update_size * 8) - 1, unsignedbv_typet{width}); + mask = from_integer(power(2, update_size * 8) - 1, bv_typet{width}); else + { mask = from_integer( - power(2, width) - power(2, width - update_size * 8), - unsignedbv_typet{width}); + power(2, width) - power(2, width - update_size * 8), bv_typet{width}); + } const typet &offset_type = src.offset().type(); mult_exprt offset_times_eight{src.offset(), from_integer(8, offset_type)}; @@ -1722,13 +1719,13 @@ static exprt lower_byte_update( // original_bits &= ~mask exprt val_before = - typecast_exprt::conditional_cast(src.op(), unsignedbv_typet{type_bits}); + typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits}); if(width > type_bits) { - val_before = concatenation_exprt{ - from_integer(0, unsignedbv_typet{width - type_bits}), - val_before, - unsignedbv_typet{width}}; + val_before = + concatenation_exprt{from_integer(0, bv_typet{width - type_bits}), + val_before, + bv_typet{width}}; if(!is_little_endian) val_before.op0().swap(val_before.op1()); @@ -1737,17 +1734,17 @@ static exprt lower_byte_update( // concatenate and zero-extend the value concatenation_exprt value{exprt::operandst{value_as_byte_array.operands()}, - unsignedbv_typet{update_size * 8}}; + bv_typet{update_size * 8}}; if(is_little_endian) std::reverse(value.operands().begin(), value.operands().end()); exprt zero_extended; if(width > update_size * 8) { - zero_extended = concatenation_exprt{ - from_integer(0, unsignedbv_typet{width - update_size * 8}), - value, - unsignedbv_typet{width}}; + zero_extended = + concatenation_exprt{from_integer(0, bv_typet{width - update_size * 8}), + value, + bv_typet{width}}; if(!is_little_endian) zero_extended.op0().swap(zero_extended.op1()); @@ -1769,10 +1766,8 @@ static exprt lower_byte_update( { return simplify_expr( typecast_exprt::conditional_cast( - extractbits_exprt{bitor_expr, - width - 1, - width - type_bits, - unsignedbv_typet{type_bits}}, + extractbits_exprt{ + bitor_expr, width - 1, width - type_bits, bv_typet{type_bits}}, src.type()), ns); } @@ -1840,8 +1835,7 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns) extract_opcode, src.value(), from_integer(0, src.offset().type()), - array_typet{unsignedbv_typet{8}, - from_integer(max_update_bytes, size_type())}}; + array_typet{bv_typet{8}, from_integer(max_update_bytes, size_type())}}; const array_exprt value_as_byte_array = to_array_expr(lower_byte_extract(byte_extract_expr, ns)); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 7780c45ed56..410f623ea2e 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2243,8 +2243,9 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) // this just passes through convert_expr(src); } - else if(src_type.id()==ID_unsignedbv || - src_type.id()==ID_signedbv) + else if( + src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv || + src_type.id() == ID_bv) { // integer to pointer diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 40f417c1c81..80520b58e74 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -754,6 +754,12 @@ bool simplify_exprt::simplify_typecast(exprt &expr) expr=f.to_expr(); return false; } + else if(expr_type_id == ID_bv) + { + fixedbvt f{to_constant_expr(expr.op0())}; + expr = from_integer(f.get_value(), expr_type); + return false; + } } else if(op_type_id==ID_floatbv) { @@ -784,16 +790,47 @@ bool simplify_exprt::simplify_typecast(exprt &expr) expr=fixedbv.to_expr(); return false; } + else if(expr_type_id == ID_bv) + { + expr = from_integer(f.pack(), expr_type); + return false; + } } else if(op_type_id==ID_bv) { - if(expr_type_id==ID_unsignedbv || - expr_type_id==ID_signedbv || - expr_type_id==ID_floatbv) + if( + expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv || + expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag || + expr_type_id == ID_c_bit_field) { const auto width = to_bv_type(op_type).get_width(); const auto int_value = bvrep2integer(value, width, false); - expr=from_integer(int_value, expr_type); + if(expr_type_id != ID_c_enum_tag) + expr = from_integer(int_value, expr_type); + else + { + c_enum_tag_typet tag_type = to_c_enum_tag_type(expr_type); + expr = from_integer(int_value, ns.follow_tag(tag_type)); + expr.type() = tag_type; + } + return false; + } + else if(expr_type_id == ID_floatbv) + { + const auto width = to_bv_type(op_type).get_width(); + const auto int_value = bvrep2integer(value, width, false); + ieee_floatt ieee_float{to_floatbv_type(expr_type)}; + ieee_float.unpack(int_value); + expr = ieee_float.to_expr(); + return false; + } + else if(expr_type_id == ID_fixedbv) + { + const auto width = to_bv_type(op_type).get_width(); + const auto int_value = bvrep2integer(value, width, false); + fixedbvt fixedbv{fixedbv_spect{to_fixedbv_type(expr_type)}}; + fixedbv.set_value(int_value); + expr = fixedbv.to_expr(); return false; } } @@ -1573,7 +1610,8 @@ optionalt simplify_exprt::bits2expr( if( type.id() == ID_unsignedbv || type.id() == ID_signedbv || type.id() == ID_floatbv || type.id() == ID_fixedbv || - type.id() == ID_c_bit_field || type.id() == ID_pointer) + type.id() == ID_c_bit_field || type.id() == ID_pointer || + type.id() == ID_bv) { endianness_mapt map(type, little_endian, ns); @@ -1769,7 +1807,7 @@ optionalt simplify_exprt::expr2bits( if( type.id() == ID_unsignedbv || type.id() == ID_signedbv || type.id() == ID_floatbv || type.id() == ID_fixedbv || - type.id() == ID_c_bit_field) + type.id() == ID_c_bit_field || type.id() == ID_bv) { const auto width = to_bitvector_type(type).get_width(); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 8efef95340b..fbf24059f2f 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -951,7 +951,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr) bool simplify_exprt::simplify_shifts(exprt &expr) { - if(!is_number(expr.type())) + if(!is_bitvector_type(expr.type())) return true; if(expr.operands().size()!=2) @@ -972,11 +972,21 @@ bool simplify_exprt::simplify_shifts(exprt &expr) auto value = numeric_cast(expr.op0()); + if( + !value.has_value() && expr.op0().type().id() == ID_bv && + expr.op0().id() == ID_constant) + { + const std::size_t width = to_bitvector_type(expr.op0().type()).get_width(); + value = + bvrep2integer(to_constant_expr(expr.op0()).get_value(), width, false); + } + if(!value.has_value()) return true; - if(expr.op0().type().id()==ID_unsignedbv || - expr.op0().type().id()==ID_signedbv) + if( + expr.op0().type().id() == ID_unsignedbv || + expr.op0().type().id() == ID_signedbv || expr.op0().type().id() == ID_bv) { const std::size_t width = to_bitvector_type(expr.op0().type()).get_width(); diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index 6290c725bed..0cdeb1849cd 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -150,14 +150,13 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") unsignedbv_typet(128), signedbv_typet(24), signedbv_typet(128), - // ieee_float_spect::single_precision().to_type(), + ieee_float_spect::single_precision().to_type(), // generates the correct value, but remains wrapped in a typecast // pointer_typet(u64, 64), vector_typet(u8, size), vector_typet(u64, size), complex_typet(s16), - complex_typet(u64) - }; + complex_typet(u64)}; simplify_exprt simp(ns); @@ -301,7 +300,7 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]") unsignedbv_typet(128), signedbv_typet(24), signedbv_typet(128), - // ieee_float_spect::single_precision().to_type(), + ieee_float_spect::single_precision().to_type(), // generates the correct value, but remains wrapped in a typecast // pointer_typet(u64, 64), vector_typet(u8, size),