From 4b8ac7c4d6f197458646e89456d2261205d42781 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 25 Nov 2021 15:39:07 +0000 Subject: [PATCH 1/2] Simplify away type cast The array size may include a type cast, possibly of a constant. Therefore, the size would be found to be constant via simplification, but other ways of computing the size may fail to derive a constant. --- src/goto-programs/builtin_functions.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index aa300c66654..699b1dc14eb 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -699,7 +700,7 @@ void goto_convertt::do_havoc_slice( t->source_location_nonconst().set_comment( "assertion havoc_slice " + from_expr(ns, identifier, ok_expr)); - const array_typet array_type(char_type(), arguments[1]); + const array_typet array_type(char_type(), simplify_expr(arguments[1], ns)); const symbolt &nondet_contents = new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode); From eeb137205fba870a6050cc1de426c34c93d299d3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 25 Nov 2021 15:40:39 +0000 Subject: [PATCH 2/2] Byte updates using bit fields require extension to full bytes A byte update with an update value that has a size that's not a multiple of bytes must not overwrite bits that are not in the update value. We previously generated extractbits expressions that would go out of bounds, which tripped up the SMT solvers. No longer generating these out-of-bounds expressions makes the SMT solvers happy on the Promotion3 test, which exercised this feature. --- regression/cbmc/Promotion3/test.desc | 2 +- .../cbmc/havoc_slice/test_struct_b_slice.desc | 2 +- src/solvers/lowering/byte_operators.cpp | 43 ++++++++++++++++++- 3 files changed, 43 insertions(+), 4 deletions(-) diff --git a/regression/cbmc/Promotion3/test.desc b/regression/cbmc/Promotion3/test.desc index 39d9265e8a7..9efefbc7362 100644 --- a/regression/cbmc/Promotion3/test.desc +++ b/regression/cbmc/Promotion3/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/havoc_slice/test_struct_b_slice.desc b/regression/cbmc/havoc_slice/test_struct_b_slice.desc index c99c590cd59..c4cd5bcdf2c 100644 --- a/regression/cbmc/havoc_slice/test_struct_b_slice.desc +++ b/regression/cbmc/havoc_slice/test_struct_b_slice.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE test_struct_b_slice.c ^EXIT=10$ diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 70aee6d3c04..cfcfb91277a 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -2278,12 +2278,51 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns) // place. // 4) Construct a new object. optionalt non_const_update_bound; - auto update_size_expr_opt = size_of_expr(src.value().type(), ns); + // update value, may require extension to full bytes + exprt update_value = src.value(); + auto update_size_expr_opt = size_of_expr(update_value.type(), ns); CHECK_RETURN(update_size_expr_opt.has_value()); simplify(update_size_expr_opt.value(), ns); if(!update_size_expr_opt.value().is_constant()) non_const_update_bound = *update_size_expr_opt; + else + { + auto update_bits = pointer_offset_bits(update_value.type(), ns); + // If the following invariant fails, then the type was only found to be + // constant via simplification. Such instances should be fixed at the place + // introducing these constant-but-not-constant_exprt type sizes. + DATA_INVARIANT( + update_bits.has_value(), "constant size-of should imply fixed bit width"); + const size_t update_bits_int = numeric_cast_v(*update_bits); + + if(update_bits_int % 8 != 0) + { + DATA_INVARIANT( + can_cast_type(update_value.type()), + "non-byte aligned type expected to be a bitvector type"); + size_t n_extra_bits = 8 - update_bits_int % 8; + + endianness_mapt endianness_map( + src.op().type(), src.id() == ID_byte_update_little_endian, ns); + const auto bounds = map_bounds( + endianness_map, update_bits_int, update_bits_int + n_extra_bits - 1); + extractbits_exprt extra_bits{ + src.op(), bounds.ub, bounds.lb, bv_typet{n_extra_bits}}; + + update_value = + concatenation_exprt{typecast_exprt::conditional_cast( + update_value, bv_typet{update_bits_int}), + extra_bits, + bitvector_typet{update_value.type().id(), + update_bits_int + n_extra_bits}}; + } + else + { + update_size_expr_opt = + from_integer(update_bits_int / 8, update_size_expr_opt->type()); + } + } const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian @@ -2291,7 +2330,7 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns) const byte_extract_exprt byte_extract_expr{ extract_opcode, - src.value(), + update_value, from_integer(0, src.offset().type()), array_typet{bv_typet{8}, *update_size_expr_opt}};