diff --git a/regression/cbmc-shadow-memory/bv-get-max/main.c b/regression/cbmc-shadow-memory/bv-get-max/main.c new file mode 100644 index 00000000000..2585d96e8e7 --- /dev/null +++ b/regression/cbmc-shadow-memory/bv-get-max/main.c @@ -0,0 +1,19 @@ +#include + +int main() +{ + __CPROVER_field_decl_local("uninitialized", (char)0); + __CPROVER_field_decl_global("uninitialized", (char)0); + + int i; + char *a = &i; + + __CPROVER_set_field(a + 1, "uninitialized", 1); + + assert(__CPROVER_get_field(a, "uninitialized") == 0); + assert(__CPROVER_get_field(&i, "uninitialized") == 1); + assert(__CPROVER_get_field(a + 1, "uninitialized") == 1); + // Expecting the remaining bytes to be untouched by the setting of the field. + assert(__CPROVER_get_field(a + 2, "uninitialized") == 0); + assert(__CPROVER_get_field(a + 3, "uninitialized") == 0); +} diff --git a/regression/cbmc-shadow-memory/bv-get-max/test.desc b/regression/cbmc-shadow-memory/bv-get-max/test.desc new file mode 100644 index 00000000000..67cb3bf2767 --- /dev/null +++ b/regression/cbmc-shadow-memory/bv-get-max/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- diff --git a/regression/cbmc-shadow-memory/bv-get-or/main.c b/regression/cbmc-shadow-memory/bv-get-or/main.c new file mode 100644 index 00000000000..2348bae1fbc --- /dev/null +++ b/regression/cbmc-shadow-memory/bv-get-or/main.c @@ -0,0 +1,19 @@ +#include + +int main() +{ + __CPROVER_field_decl_local("uninitialized", (_Bool)0); + __CPROVER_field_decl_global("uninitialized", (_Bool)0); + + int i; + char *a = &i; + + __CPROVER_set_field(a + 1, "uninitialized", 1); + + assert(__CPROVER_get_field(a, "uninitialized") == 0); + assert(__CPROVER_get_field(a + 1, "uninitialized") == 1); + assert(__CPROVER_get_field(&i, "uninitialized") == 1); + // Expecting the remaining bytes to be untouched by the setting of the field. + assert(__CPROVER_get_field(a + 2, "uninitialized") == 0); + assert(__CPROVER_get_field(a + 3, "uninitialized") == 0); +} diff --git a/regression/cbmc-shadow-memory/bv-get-or/test.desc b/regression/cbmc-shadow-memory/bv-get-or/test.desc new file mode 100644 index 00000000000..67cb3bf2767 --- /dev/null +++ b/regression/cbmc-shadow-memory/bv-get-or/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- diff --git a/regression/cbmc-shadow-memory/union-get-max1/main.c b/regression/cbmc-shadow-memory/union-get-max1/main.c index 90ac1b5a70a..c9acb560210 100644 --- a/regression/cbmc-shadow-memory/union-get-max1/main.c +++ b/regression/cbmc-shadow-memory/union-get-max1/main.c @@ -14,11 +14,18 @@ union UNIONNAME char x3[3]; }; +// [Shadow] Memory layout (PP is padding) +// u = [ byte1 byte2 byte3 byte4 byte5 byte6 ] +// u.x1 = [ X1 X1 X1 X1 PP PP ] +// u.x2 = [ Y1 PP Y2 Y2 Y3 Y3 ] +// u.x3 = [ X3[0] X3[1] X3[2] PP PP PP ] + int main() { __CPROVER_field_decl_local("field2", (__CPROVER_bitvector[6])0); union UNIONNAME u; + // u = [0x00 0x00 0x00 0x00 0x00 0x00] assert(__CPROVER_get_field(&u, "field2") == 0); assert(__CPROVER_get_field(&(u.x1), "field2") == 0); @@ -32,6 +39,7 @@ int main() assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 0); __CPROVER_set_field(&(u.x1), "field2", 1); + // u = [0x02 0x01 0x01 0x01 0x00 0x00] assert(__CPROVER_get_field(&u, "field2") == 1); assert(__CPROVER_get_field(&(u.x1), "field2") == 1); assert(__CPROVER_get_field(&(u.x2), "field2") == 1); @@ -44,6 +52,7 @@ int main() assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 1); __CPROVER_set_field(&(u.x2.y1), "field2", 2); + // u = [0x02 0x01 0x01 0x01 0x00 0x00] assert(__CPROVER_get_field(&u, "field2") == 2); assert(__CPROVER_get_field(&(u.x1), "field2") == 2); assert(__CPROVER_get_field(&(u.x2), "field2") == 2); @@ -56,8 +65,9 @@ int main() assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 1); __CPROVER_set_field(&(u.x2.y2), "field2", 3); + // u = [0x02 0x01 0x03 0x03 0x00 0x00] assert(__CPROVER_get_field(&u, "field2") == 3); - assert(__CPROVER_get_field(&(u.x1), "field2") == 2); + assert(__CPROVER_get_field(&(u.x1), "field2") == 3); assert(__CPROVER_get_field(&(u.x2), "field2") == 3); assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 2); assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 3); @@ -68,8 +78,9 @@ int main() assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 3); __CPROVER_set_field(&(u.x2.y3), "field2", 4); + // u = [0x02 0x01 0x03 0x03 0x04 0x04] assert(__CPROVER_get_field(&u, "field2") == 4); - assert(__CPROVER_get_field(&(u.x1), "field2") == 2); + assert(__CPROVER_get_field(&(u.x1), "field2") == 3); assert(__CPROVER_get_field(&(u.x2), "field2") == 4); assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 2); assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 3); @@ -78,4 +89,21 @@ int main() assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 2); assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1); assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 3); + + __CPROVER_set_field(&(u.x3[1]), "field2", 5); + // u = [0x02 0x05 0x03 0x03 0x04 0x04] + assert(__CPROVER_get_field(&u, "field2") == 5); + assert(__CPROVER_get_field(&(u.x1), "field2") == 5); + assert(__CPROVER_get_field(&(u.x2), "field2") == 5); + assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 2); + assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 3); + assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 4); + // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 5); + assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 2); + assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 5); + assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 3); + + // Failing assertion added to get trace and to test what the inner + // representation is. + assert(__CPROVER_get_field(&u, "field2") == 42); } diff --git a/regression/cbmc-shadow-memory/union-get-max1/test.desc b/regression/cbmc-shadow-memory/union-get-max1/test.desc index 49bbf7d5ebc..152c86c42e0 100644 --- a/regression/cbmc-shadow-memory/union-get-max1/test.desc +++ b/regression/cbmc-shadow-memory/union-get-max1/test.desc @@ -1,9 +1,14 @@ CORE main.c - -^EXIT=0$ +--trace +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ +SM__&u!0@1__field2\.x2=\{ \.y1=1, \.\$pad1=1, \.y2=257, \.y3=0 \} \(\{ 00000001, 00000001, 00000001 00000001, 00000000 00000000 \}\)$ +SM__&u!0@1__field2\.x2=\{ \.y1=2, \.\$pad1=1, \.y2=257, \.y3=0 \} \(\{ 00000010, 00000001, 00000001 00000001, 00000000 00000000 \}\)$ +SM__&u!0@1__field2\.x2=\{ \.y1=2, \.\$pad1=1, \.y2=771, \.y3=0 \} \(\{ 00000010, 00000001, 00000011 00000011, 00000000 00000000 \}\)$ +SM__&u!0@1__field2\.x2=\{ \.y1=2, \.\$pad1=1, \.y2=771, \.y3=1028 \} \(\{ 00000010, 00000001, 00000011 00000011, 00000100 00000100 \}\)$ +SM__&u!0@1__field2\.x2=\{ \.y1=2, \.\$pad1=5, \.y2=771, \.y3=1028 \} \(\{ 00000010, 00000101, 00000011 00000011, 00000100 00000100 \}\)$ -- ^warning: ignoring -- diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp index 3d241910652..b2e7e1cbe18 100644 --- a/src/goto-symex/shadow_memory_util.cpp +++ b/src/goto-symex/shadow_memory_util.cpp @@ -15,6 +15,7 @@ Author: Peter Schrammel #include #include #include +#include #include #include #include @@ -22,6 +23,7 @@ Author: Peter Schrammel #include #include +#include // TODO: change DEBUG_SM to DEBUG_SHADOW_MEMORY (it also appears in other files) @@ -428,119 +430,120 @@ exprt compute_or_over_cells( return or_values(values, field_type); } -// TODO: doxygen? -static void -max_element(const exprt &element, const typet &field_type, exprt &max) +/// Create an expression comparing the element at `expr_iterator` with the +/// following elements of the collection (or `nil_exprt`if none) and return a +/// pair `(condition, element)` such that if the condition is `true`, then the +/// element is the max of the collection in the interval denoted by +/// `expr_iterator` and `end`. +/// \param expr_iterator the iterator pointing at the element to compare to. +/// \param end the end of collection iterator. +/// \return A pair (cond, elem) containing the condition and the max element. +std::pair compare_to_collection( + const std::vector::const_iterator &expr_iterator, + const std::vector::const_iterator &end) { - exprt value = typecast_exprt::conditional_cast(element, field_type); - if(max.is_nil()) + // We need at least an element in the collection + INVARIANT(expr_iterator != end, "Cannot compute max of an empty collection"); + const exprt ¤t_expr = *expr_iterator; + + // Iterator for the other elements in the collection in the interval denoted + // by `expr_iterator` and `end`. + std::vector::const_iterator expr_to_compare_to = + std::next(expr_iterator); + if(expr_to_compare_to == end) { - max = value; + return {nil_exprt{}, current_expr}; } - else + + std::vector comparisons; + for(; expr_to_compare_to != end; ++expr_to_compare_to) { - max = if_exprt(binary_predicate_exprt(value, ID_gt, max), value, max); + // Compare the current element with the n-th following it + comparisons.emplace_back( + binary_predicate_exprt(current_expr, ID_gt, *expr_to_compare_to)); } + + return {and_exprt(comparisons), current_expr}; } -// TODO: doxygen? -static void max_over_bytes( - const exprt &value, - const typet &type, - const typet &field_type, - exprt &max) +/// Combine each (condition, value) element in the input collection into a +/// if-then-else expression such as +/// (cond_1 ? val_1 : (cond_2 ? val_2 : ... : val_n)) +/// \param conditions_and_values collection containing codnition-value pairs +/// \return the combined max expression +static exprt combine_condition_and_max_values( + const std::vector> &conditions_and_values) { - const size_t size = to_bitvector_type(type).get_width() / 8; - max_element(value, field_type, max); - for(size_t i = 1; i < size; ++i) + // We need at least one element + INVARIANT( + conditions_and_values.size() > 0, + "Cannot compute max of an empty collection"); + + // We use reverse-iterator, so the last element is the one in the last else + // case. + auto reverse_ite = conditions_and_values.rbegin(); + + // The last element must have `nil_exprt` as condition + INVARIANT( + reverse_ite->first == nil_exprt{}, + "Last element of condition-value list must have nil_exprt condition."); + + exprt res = std::move(reverse_ite->second); + + for(++reverse_ite; reverse_ite != conditions_and_values.rend(); ++reverse_ite) { - max_element( - lshr_exprt(value, from_integer(8 * i, size_type())), field_type, max); + res = if_exprt(reverse_ite->first, reverse_ite->second, res); } + + return res; } -// TODO: doxygen? -static void max_elements( - exprt element, - const typet &field_type, - const namespacet &ns, - const messaget &log, - const bool is_union, - exprt &max) +/// Create an expression encoding the max operation over the collection `values` +/// \param values an `exprt` that encodes the max of `values` +/// \return an `exprt` encoding the max operation over the collection `values` +static exprt create_max_expr(const std::vector &values) { - element = conditional_cast_floatbv_to_unsignedbv(element); - if(element.type().id() == ID_unsignedbv || element.type().id() == ID_signedbv) - { - if(is_union) - { - max_over_bytes(element, element.type(), field_type, max); - } - else - { - max_element(element, field_type, max); - } - } - else + std::vector> rows; + rows.reserve(values.size()); + for(auto byte_it = values.begin(); byte_it != values.end(); ++byte_it) { - exprt value = - compute_max_over_cells(element, field_type, ns, log, is_union); - max_element(value, field_type, max); + // Create a pair condition-element where the condition is the comparison of + // the element with all the ones contained in the rest of the collection. + rows.emplace_back(compare_to_collection(byte_it, values.end())); } + + return combine_condition_and_max_values(rows); } exprt compute_max_over_cells( const exprt &expr, const typet &field_type, - const namespacet &ns, - const messaget &log, - const bool is_union) + const namespacet &ns) { - const typet type = ns.follow(expr.type()); + // Compute the bit-width of the type of `expr`. + std::size_t size = boolbv_widtht{ns}(expr.type()); - if(type.id() == ID_struct || type.id() == ID_union) + // Compute how many bytes are in `expr` + std::size_t byte_count = size / config.ansi_c.char_width; + + // Extract each byte of `expr` by using byte_extract. + std::vector extracted_bytes; + extracted_bytes.reserve(byte_count); + for(std::size_t i = 0; i < byte_count; ++i) { - exprt max = nil_exprt(); - for(const auto &component : to_struct_union_type(type).components()) - { - if(component.get_is_padding()) - { - continue; - } - max_elements( - member_exprt(expr, component), field_type, ns, log, is_union, max); - } - return max; + extracted_bytes.emplace_back(make_byte_extract( + expr, from_integer(i, unsigned_long_int_type()), field_type)); } - else if(type.id() == ID_array) - { - const array_typet &array_type = to_array_type(type); - if(array_type.size().is_constant()) - { - exprt max = nil_exprt(); - const mp_integer size = - numeric_cast_v(to_constant_expr(array_type.size())); - for(mp_integer index = 0; index < size; ++index) - { - max_elements( - index_exprt(expr, from_integer(index, index_type())), - field_type, - ns, - log, - is_union, - max); - } - return max; - } - else - { - log.warning() - << "Shadow memory: cannot compute max over variable-size array " - << format(expr) << messaget::eom; - } - } - // TODO: This is incorrect when accessing non-0 offsets of scalars. - return typecast_exprt::conditional_cast( - conditional_cast_floatbv_to_unsignedbv(expr), field_type); + + // Compute the max of the bytes extracted from `expr`. + exprt max_expr = create_max_expr(extracted_bytes); + + INVARIANT( + max_expr.type() == field_type, + "Aggregated max value type must be the same as shadow memory field's " + "type."); + + return max_expr; } // TODO: doxygen? @@ -819,10 +822,7 @@ std::vector> get_shadow_dereference_candidates( else { // Value is of other (bitvector) type, so aggregate with max - value = typecast_exprt::conditional_cast( - compute_max_over_cells( - shadow_dereference.value, field_type, ns, log, is_union), - lhs_type); + value = compute_max_over_cells(shadow_dereference.value, field_type, ns); } const exprt base_cond = get_matched_base_cond( diff --git a/src/goto-symex/shadow_memory_util.h b/src/goto-symex/shadow_memory_util.h index ddffc43d7d8..c73896e2e7f 100644 --- a/src/goto-symex/shadow_memory_util.h +++ b/src/goto-symex/shadow_memory_util.h @@ -156,12 +156,15 @@ exprt compute_or_over_cells( /// Performs aggregation of the shadow memory field value over multiple cells /// for fields whose type is a signed/unsigned bitvector (where the value is /// arbitrary up until the max represented by the bitvector size). +/// \param expr the expression to extract the max from +/// \param field_type the type of the shadow memory field to return +/// \param ns the namespace to perform type-lookups into +/// \return the aggregated max byte-sized value contained in expr +/// Note that the expr type size must be known at compile time. exprt compute_max_over_cells( const exprt &expr, const typet &field_type, - const namespacet &ns, - const messaget &log, - const bool is_union); + const namespacet &ns); /// Build an if-then-else chain from a vector containing pairs of expressions. /// \param conds_values Contains pairs , where `e1` is going to be diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index d0a7fecf744..2cd605253b2 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -427,19 +427,19 @@ exprt duplicate_per_byte( // We haven't got a constant. So, build the expression using shift-and-or. exprt::operandst values; - typet operation_type = output_type; - if(const auto ptr_type = type_try_dynamic_cast(output_type)) - { - operation_type = unsignedbv_typet{ptr_type->get_width()}; - } - if( - const auto float_type = type_try_dynamic_cast(output_type)) - { - operation_type = unsignedbv_typet{float_type->get_width()}; - } - // Let's cast simplified_init_expr to output_type. - const exprt casted_init_byte_expr = - typecast_exprt::conditional_cast(init_byte_expr, operation_type); + // When doing the replication we extend the init_expr to the output size to + // compute the bitwise or. To avoid that the sign is extended too we change + // the type of the output to an unsigned bitvector with the same size as the + // output type. + typet operation_type = unsignedbv_typet{output_bv->get_width()}; + // To avoid sign-extension during cast we first cast to an unsigned version + // of the same bv type, then we extend it to the output type (adding 0 + // padding). + const exprt casted_init_byte_expr = typecast_exprt::conditional_cast( + typecast_exprt::conditional_cast( + init_byte_expr, unsignedbv_typet{init_type_as_bitvector->get_width()}), + operation_type); + values.push_back(casted_init_byte_expr); for(size_t i = 1; i < size; ++i) { diff --git a/unit/util/expr_initializer.cpp b/unit/util/expr_initializer.cpp index f297892e32a..386691b10a0 100644 --- a/unit/util/expr_initializer.cpp +++ b/unit/util/expr_initializer.cpp @@ -311,10 +311,15 @@ TEST_CASE( const auto result = duplicate_per_byte(init_expr, output_type, test.ns); - const auto casted_init_expr = - typecast_exprt::conditional_cast(init_expr, output_type); - const auto expected = - replicate_expression(casted_init_expr, output_type, replication_count); + const auto operation_type = unsignedbv_typet{output_size}; + const auto casted_init_expr = typecast_exprt::conditional_cast( + typecast_exprt::conditional_cast( + init_expr, unsignedbv_typet{init_expr_size}), + operation_type); + const auto expected = typecast_exprt::conditional_cast( + replicate_expression( + casted_init_expr, operation_type, replication_count), + output_type); REQUIRE(result == expected); }