From 344566b5c34d541b6e14e3f44108a5d0987dd206 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Sep 2022 09:18:12 +0000 Subject: [PATCH 1/2] SMT2 back-end: do not flatten flattened arrays convert_expr may flatten an array anyway, in which case flatten_array would generate select statements over bitvectors instead of arrays (as flatten_array itself invokes convert_expr to supposedly construct the array expression). Also, make sure the same flattening logic applies to 1-element structs. --- regression/cbmc/array-function-parameters/test.desc | 2 +- src/solvers/smt2/smt2_conv.cpp | 13 +++++++++++-- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/regression/cbmc/array-function-parameters/test.desc b/regression/cbmc/array-function-parameters/test.desc index c9ede9f1fe2..769bc7e70a5 100644 --- a/regression/cbmc/array-function-parameters/test.desc +++ b/regression/cbmc/array-function-parameters/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE test.c --function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check ^EXIT=10$ diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index d7806a971b3..2b35b6a356a 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3137,7 +3137,16 @@ void smt2_convt::convert_struct(const struct_exprt &expr) else { if(components.size()==1) - convert_expr(expr.op0()); + { + const exprt &op = expr.op0(); + // may need to flatten array-theory arrays in there + if(op.type().id() == ID_array && use_array_theory(op)) + flatten_array(op); + else if(op.type().id() == ID_bool) + flatten2bv(op); + else + convert_expr(op); + } else { // SMT-LIB 2 concat is binary only @@ -3148,7 +3157,7 @@ void smt2_convt::convert_struct(const struct_exprt &expr) exprt op=expr.operands()[i-1]; // may need to flatten array-theory arrays in there - if(op.type().id() == ID_array) + if(op.type().id() == ID_array && use_array_theory(op)) flatten_array(op); else if(op.type().id() == ID_bool) flatten2bv(op); From e5d94c871616c6ce6099a6c991eb64c93ea20a61 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 21 Sep 2022 12:41:49 +0000 Subject: [PATCH 2/2] Byte update lowering: make array update tails conditional When updating an array/vector at a non-constant byte offset the update value may affect multiple array/vector elements. The last such element needs to be updated with however many bytes have not yet been used from the update value. With a non-constant byte offset the size of remaining bytes may be zero. Therefore, make the tail update use symbolic offsets rather than constants. When fixing this, it also became apparent that we must not use byte extracts of non-constant extraction size to build update elements. Instead, the update offset should be non-constant, and will actually need to be negative on such occasions. --- regression/cbmc/Array_operations2/test.desc | 2 +- src/solvers/lowering/byte_operators.cpp | 114 ++++++++------------ 2 files changed, 48 insertions(+), 68 deletions(-) diff --git a/regression/cbmc/Array_operations2/test.desc b/regression/cbmc/Array_operations2/test.desc index deed98df48c..712e870ea1c 100644 --- a/regression/cbmc/Array_operations2/test.desc +++ b/regression/cbmc/Array_operations2/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE broken-cprover-smt-backend main.c ^\[main.assertion.12\] line 34 assertion arr\[1\].c\[2\] == 0: FAILURE$ diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index f374b813c51..6f4deea7674 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -1621,19 +1621,14 @@ static exprt lower_byte_update_array_vector_unbounded( plus_exprt{last_index, from_integer(1, last_index.type())}}}; // The actual value of a partial update at the end. - exprt last_update_value = lower_byte_operators( + exprt last_update_value = lower_byte_update( byte_update_exprt{ src.id(), index_exprt{src.op(), last_index}, - from_integer(0, src.offset().type()), - byte_extract_exprt{ - extract_opcode, - value_as_byte_array, - mult_exprt{ - typecast_exprt::conditional_cast(last_index, subtype_size.type()), - subtype_size}, - src.get_bits_per_byte(), - array_typet{bv_typet{src.get_bits_per_byte()}, tail_size}}, + unary_minus_exprt{mult_exprt{ + typecast_exprt::conditional_cast(last_index, subtype_size.type()), + subtype_size}}, + value_as_byte_array, src.get_bits_per_byte()}, ns); @@ -1675,10 +1670,6 @@ static exprt lower_byte_update_array_vector_non_const( const optionalt &non_const_update_bound, const namespacet &ns) { - const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian - ? ID_byte_extract_little_endian - : ID_byte_extract_big_endian; - // do all arithmetic below using index/offset types - the array theory // back-end is really picky about indices having the same type auto subtype_size_opt = size_of_expr(subtype, ns); @@ -1699,6 +1690,8 @@ static exprt lower_byte_update_array_vector_non_const( // compute the number of bytes (from the update value) that are going to be // consumed for updating the first element + const exprt update_size = + from_integer(value_as_byte_array.operands().size(), subtype_size.type()); exprt initial_bytes = minus_exprt{subtype_size, update_offset}; exprt update_bound; if(non_const_update_bound.has_value()) @@ -1711,8 +1704,7 @@ static exprt lower_byte_update_array_vector_non_const( DATA_INVARIANT( value_as_byte_array.id() == ID_array, "value should be an array expression if the update bound is constant"); - update_bound = - from_integer(value_as_byte_array.operands().size(), initial_bytes.type()); + update_bound = update_size; } initial_bytes = if_exprt{binary_predicate_exprt{initial_bytes, ID_lt, update_bound}, @@ -1720,19 +1712,15 @@ static exprt lower_byte_update_array_vector_non_const( update_bound}; simplify(initial_bytes, ns); - // encode the first update: update the original element at first_index with - // initial_bytes-many bytes extracted from value_as_byte_array - exprt first_update_value = lower_byte_operators( + // encode the first update: update the original element at first_index (the + // actual update will only be initial_bytes-many bytes from + // value_as_byte_array) + exprt first_update_value = lower_byte_update( byte_update_exprt{ src.id(), index_exprt{src.op(), first_index}, update_offset, - byte_extract_exprt{ - extract_opcode, - value_as_byte_array, - from_integer(0, src.offset().type()), - src.get_bits_per_byte(), - array_typet{bv_typet{src.get_bits_per_byte()}, initial_bytes}}, + value_as_byte_array, src.get_bits_per_byte()}, ns); @@ -1768,63 +1756,45 @@ static exprt lower_byte_update_array_vector_non_const( with_exprt result{src.op(), first_index, first_update_value}; - std::size_t i = 1; - for(; offset + step_size <= value_as_byte_array.operands().size(); - offset += step_size, ++i) - { + auto lower_byte_update_array_vector_non_const_one_element = + [&src, + &first_index, + &initial_bytes, + &subtype_size, + &value_as_byte_array, + &ns, + &result](std::size_t i) -> void { exprt where = simplify_expr( plus_exprt{first_index, from_integer(i, first_index.type())}, ns); - exprt offset_expr = simplify_expr( - plus_exprt{ + exprt neg_offset_expr = simplify_expr( + unary_minus_exprt{plus_exprt{ initial_bytes, - mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}}, + mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}}}, ns); - exprt element = lower_byte_operators( + exprt element = lower_byte_update( byte_update_exprt{ src.id(), index_exprt{src.op(), where}, - from_integer(0, src.offset().type()), - byte_extract_exprt{ - extract_opcode, - value_as_byte_array, - std::move(offset_expr), - src.get_bits_per_byte(), - array_typet{bv_typet{src.get_bits_per_byte()}, subtype_size}}, + neg_offset_expr, + value_as_byte_array, src.get_bits_per_byte()}, ns); result.add_to_operands(std::move(where), std::move(element)); + }; + + std::size_t i = 1; + for(; offset + step_size <= value_as_byte_array.operands().size(); + offset += step_size, ++i) + { + lower_byte_update_array_vector_non_const_one_element(i); } // do the tail if(offset < value_as_byte_array.operands().size()) - { - const std::size_t tail_size = - value_as_byte_array.operands().size() - offset; - - exprt where = simplify_expr( - plus_exprt{first_index, from_integer(i, first_index.type())}, ns); - - exprt element = lower_byte_operators( - byte_update_exprt{ - 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()), - src.get_bits_per_byte(), - array_typet{ - bv_typet{src.get_bits_per_byte()}, - from_integer(tail_size, size_type())}}, - src.get_bits_per_byte()}, - ns); - - result.add_to_operands(std::move(where), std::move(element)); - } + lower_byte_update_array_vector_non_const_one_element(i); return simplify_expr(std::move(result), ns); } @@ -2333,9 +2303,14 @@ static exprt lower_byte_update( if_exprt mask_shifted{ offset_ge_zero, shl_exprt{mask, offset_in_bits}, - lshr_exprt{mask, offset_in_bits}}; + lshr_exprt{mask, unary_minus_exprt{offset_in_bits}}}; if(!is_little_endian) + { mask_shifted.true_case().swap(mask_shifted.false_case()); + to_shift_expr(mask_shifted.true_case()) + .distance() + .swap(to_shift_expr(mask_shifted.false_case()).distance()); + } // original_bits &= ~mask bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}}; @@ -2365,9 +2340,14 @@ static exprt lower_byte_update( if_exprt value_shifted{ offset_ge_zero, shl_exprt{zero_extended, offset_in_bits}, - lshr_exprt{zero_extended, offset_in_bits}}; + lshr_exprt{zero_extended, unary_minus_exprt{offset_in_bits}}}; if(!is_little_endian) + { value_shifted.true_case().swap(value_shifted.false_case()); + to_shift_expr(value_shifted.true_case()) + .distance() + .swap(to_shift_expr(value_shifted.false_case()).distance()); + } // original_bits |= newvalue bitor_exprt bitor_expr{bitand_expr, value_shifted};