diff --git a/src/goto-symex/expr_skeleton.cpp b/src/goto-symex/expr_skeleton.cpp index 537ae2a0861..db1f9cc5e4a 100644 --- a/src/goto-symex/expr_skeleton.cpp +++ b/src/goto-symex/expr_skeleton.cpp @@ -11,9 +11,15 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include "expr_skeleton.h" +#include +#include +#include +#include +#include #include -expr_skeletont::expr_skeletont() : skeleton(nil_exprt{}) +expr_skeletont::expr_skeletont(typet missing_type) + : skeleton(nil_exprt{}), type_of_missing_part(std::move(missing_type)) { } @@ -21,13 +27,15 @@ expr_skeletont expr_skeletont::remove_op0(exprt e) { PRECONDITION(e.id() != ID_symbol); PRECONDITION(e.operands().size() >= 1); + typet missing = std::move(e.op0().type()); e.op0().make_nil(); - return expr_skeletont{std::move(e)}; + return expr_skeletont{std::move(e), std::move(missing)}; } exprt expr_skeletont::apply(exprt expr) const { PRECONDITION(skeleton.id() != ID_symbol); + PRECONDITION(expr.type() == type_of_missing_part); exprt result = skeleton; exprt *p = &result; @@ -50,13 +58,18 @@ exprt expr_skeletont::apply(exprt expr) const expr_skeletont expr_skeletont::compose(expr_skeletont other) const { - return expr_skeletont(apply(other.skeleton)); + typet missing_type = other.type_of_missing_part; + return expr_skeletont{apply(std::move(other.skeleton)), + std::move(missing_type)}; } /// In the expression corresponding to a skeleton returns a pointer to the /// deepest subexpression before we encounter nil. +/// Returns nullptr if \p e is nil static exprt *deepest_not_nil(exprt &e) { + if(e.is_nil()) + return nullptr; exprt *ptr = &e; while(!ptr->op0().is_nil()) ptr = &ptr->op0(); @@ -67,10 +80,14 @@ optionalt expr_skeletont::clear_innermost_index_expr(expr_skeletont skeleton) { exprt *to_update = deepest_not_nil(skeleton.skeleton); + if(to_update == nullptr) + return {}; if(index_exprt *index_expr = expr_try_dynamic_cast(*to_update)) { + typet new_missing_type = index_expr->type(); index_expr->make_nil(); - return expr_skeletont{std::move(skeleton)}; + return expr_skeletont{std::move(skeleton.skeleton), + std::move(new_missing_type)}; } return {}; } @@ -79,10 +96,14 @@ optionalt expr_skeletont::clear_innermost_member_expr(expr_skeletont skeleton) { exprt *to_update = deepest_not_nil(skeleton.skeleton); + if(to_update == nullptr) + return {}; if(member_exprt *member = expr_try_dynamic_cast(*to_update)) { + typet new_missing_type = member->type(); member->make_nil(); - return expr_skeletont{std::move(skeleton)}; + return expr_skeletont{std::move(skeleton.skeleton), + std::move(new_missing_type)}; } return {}; } @@ -91,12 +112,96 @@ optionalt expr_skeletont::clear_innermost_byte_extract_expr(expr_skeletont skeleton) { exprt *to_update = deepest_not_nil(skeleton.skeleton); + if(to_update == nullptr) + return {}; if( to_update->id() != ID_byte_extract_big_endian && to_update->id() != ID_byte_extract_little_endian) { return {}; } + typet new_missing_type = to_update->type(); to_update->make_nil(); - return expr_skeletont{std::move(skeleton.skeleton)}; + return expr_skeletont{std::move(skeleton.skeleton), + std::move(new_missing_type)}; +} + +expr_skeletont expr_skeletont::revert_byte_extract_aux( + expr_skeletont skeleton, + exprt offset, + const typet &type, + const namespacet &ns, + exprt offset_already_removed) +{ + offset = simplify_expr(std::move(offset), ns); + const exprt offset_reached = + simplify_expr(equal_exprt{offset_already_removed, offset}, ns); + if(offset_reached.is_true() && type == skeleton.type_of_missing_part) + return expr_skeletont{std::move(skeleton)}; + const exprt offset_exceeded = simplify_expr( + binary_relation_exprt{offset_already_removed, ID_gt, offset}, ns); + exprt *deepest = deepest_not_nil(skeleton.skeleton); + if(deepest == nullptr || offset_exceeded.is_true()) + { + // In case of empty skeleton or if the offset has been exceeded, compose + // with `byte_extract(☐, offset_already_removed - offset)` + const minus_exprt offset_diff{std::move(offset_already_removed), offset}; + const auto simplified = simplify_expr(offset_diff, ns); + return skeleton.compose(expr_skeletont{ + byte_extract_exprt{byte_extract_id(), nil_exprt{}, simplified, type}, + skeleton.type_of_missing_part}); + } + const auto offset_resulting_from_deepest_operation = [&]() -> exprt { + if(auto byte_extract = expr_try_dynamic_cast(*deepest)) + return byte_extract->offset(); + if(auto index_expr = expr_try_dynamic_cast(*deepest)) + { + auto element_size_in_bits = pointer_offset_bits(index_expr->type(), ns); + CHECK_RETURN(element_size_in_bits); + mult_exprt offset_in_bits{ + index_expr->index(), + from_integer(*element_size_in_bits, index_expr->index().type())}; + return div_exprt{offset_in_bits, from_integer(8, offset_in_bits.type())}; + } + auto member_expr = expr_try_dynamic_cast(*deepest); + INVARIANT( + member_expr, + "Skeleton should only be composed of byte_extract, index and member " + "exprts"); + auto struct_type = + type_try_dynamic_cast(skeleton.type_of_missing_part); + INVARIANT( + struct_type, + "In member_exprt skeleton the missing part should have struct type"); + auto member_offset = + member_offset_expr(*struct_type, member_expr->get_component_name(), ns); + CHECK_RETURN(member_offset); + return *member_offset; + }(); + + typet new_missing_type = deepest->type(); + deepest->make_nil(); + skeleton.type_of_missing_part = new_missing_type; + return revert_byte_extract_aux( + skeleton, + offset, + type, + ns, + plus_exprt{std::move(offset_already_removed), + offset_resulting_from_deepest_operation}); +} + +expr_skeletont expr_skeletont::revert_byte_extract( + expr_skeletont skeleton, + exprt offset, + const typet &type, + const namespacet &ns) +{ + exprt init_already_removed = from_integer(0, offset.type()); + return revert_byte_extract_aux( + std::move(skeleton), + std::move(offset), + type, + ns, + std::move(init_already_removed)); } diff --git a/src/goto-symex/expr_skeleton.h b/src/goto-symex/expr_skeleton.h index deaa5b203c4..0177265b577 100644 --- a/src/goto-symex/expr_skeleton.h +++ b/src/goto-symex/expr_skeleton.h @@ -13,6 +13,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #define CPROVER_GOTO_SYMEX_EXPR_SKELETON_H #include +#include /// Expression in which some part is missing and can be substituted for another /// expression. @@ -27,7 +28,7 @@ class expr_skeletont final public: /// Empty skeleton. Applying it to an expression would give the same /// expression unchanged - expr_skeletont(); + explicit expr_skeletont(typet missing_type); /// Replace the missing part of the current skeleton by another skeleton, /// ending in a bigger skeleton corresponding to the two combined. @@ -61,16 +62,43 @@ class expr_skeletont final static optionalt clear_innermost_byte_extract_expr(expr_skeletont skeleton); + /// Attempt to return a skeleton `s` such that for all expression \c x, + /// `s.apply(byte_extract(x, offset, type))` would be semantically equivalent + /// to `skeleton.apply(x)`. + /// If offset + type size exceeds the size (in bytes) of the skeleton then + /// an empty optional is returned. + /// This is done by removing operations of the skeleton (starting by the + /// deepest ones), until the accumulated offset match or exceed \p offset. + /// If it does not exactly match then one of the operation will be replaced + /// by a byte_extract. + static expr_skeletont revert_byte_extract( + expr_skeletont skeleton, + exprt offset, + const typet &type, + const namespacet &ns); + private: /// In \c skeleton, nil_exprt is used to mark the sub expression to be /// substituted. The nil_exprt always appears recursively following the first /// operands because the only way to get a skeleton is by removing the first /// operand. exprt skeleton; + typet type_of_missing_part; - explicit expr_skeletont(exprt e) : skeleton(std::move(e)) + expr_skeletont(exprt e, typet missing) + : skeleton(std::move(e)), type_of_missing_part(std::move(missing)) { } + + /// Auxiliary function for revert_byte_extract. + /// It is recursive and has an extra argument for keeping track of the offset + /// that has been removed by the recursive calls. + static expr_skeletont revert_byte_extract_aux( + expr_skeletont skeleton, + exprt offset, + const typet &type, + const namespacet &ns, + exprt offset_already_removed); }; #endif // CPROVER_GOTO_SYMEX_EXPR_SKELETON_H diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 7a4818fc812..2832501c554 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -82,6 +82,6 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code) exprt::operandst lhs_if_then_else_conditions; symex_assignt{state, assignment_type, ns, symex_config, target}.assign_rec( - lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions); + lhs, expr_skeletont{lhs.type()}, rhs, lhs_if_then_else_conditions); } } diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 8cc62d897e0..4370bcb1ba5 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include // We can either use with_exprt or update_exprt when building expressions that // modify components of an array or a struct. Set USE_UPDATE to use @@ -181,7 +182,7 @@ static assignmentt rewrite_with_to_field_symbols( lhs_mod.type().id() == ID_struct_tag)) { exprt field_sensitive_lhs; - expr_skeletont lhs_skeleton; + expr_skeletont lhs_skeleton{lhs_mod.type()}; const with_exprt &with_expr = to_with_expr(ssa_rhs); if(lhs_mod.type().id() == ID_array) @@ -230,89 +231,86 @@ static assignmentt rewrite_with_to_field_symbols( /// \param [in, out] state: symbolic execution state to perform renaming /// \param assignment: assignment to transform /// \param ns: namespace -/// \param do_simplify: set to true if, and only if, simplification is enabled /// \return updated assignment template static assignmentt shift_indexed_access_to_lhs( goto_symext::statet &state, assignmentt assignment, - const namespacet &ns, - bool do_simplify) + const namespacet &ns) { + if(!can_cast_expr(assignment.rhs)) + return assignment; exprt &ssa_rhs = assignment.rhs; - ssa_exprt &lhs_mod = assignment.lhs; - if( - ssa_rhs.id() == ID_byte_update_little_endian || - ssa_rhs.id() == ID_byte_update_big_endian) + const byte_update_exprt &byte_update = to_byte_update_expr(ssa_rhs); + exprt byte_extract = simplify_exprt{ns} + .simplify_byte_extract(byte_extract_exprt{ + byte_update.id() == ID_byte_update_big_endian + ? ID_byte_extract_big_endian + : ID_byte_extract_little_endian, + assignment.lhs, + byte_update.offset(), + byte_update.value().type()}) + .expr; + + expr_skeletont new_skeleton = expr_skeletont::revert_byte_extract( + assignment.original_lhs_skeleton, + byte_update.offset(), + byte_update.value().type(), + ns); + if(byte_extract.id() == ID_symbol) { - const byte_update_exprt &byte_update = to_byte_update_expr(ssa_rhs); - exprt byte_extract = byte_extract_exprt( - byte_update.id() == ID_byte_update_big_endian - ? ID_byte_extract_big_endian - : ID_byte_extract_little_endian, - lhs_mod, - byte_update.offset(), - byte_update.value().type()); - if(do_simplify) - simplify(byte_extract, ns); - - if(byte_extract.id() == ID_symbol) - { - return assignmentt{to_ssa_expr(byte_extract), - std::move(assignment.original_lhs_skeleton), - byte_update.value()}; - } - else if(byte_extract.id() == ID_index || byte_extract.id() == ID_member) - { - ssa_rhs = byte_update.value(); + return assignmentt{ + to_ssa_expr(byte_extract), std::move(new_skeleton), byte_update.value()}; + } + else if(byte_extract.id() == ID_index || byte_extract.id() == ID_member) + { + ssa_rhs = byte_update.value(); - while(byte_extract.id() == ID_index || byte_extract.id() == ID_member) + while(byte_extract.id() == ID_index || byte_extract.id() == ID_member) + { + if(byte_extract.id() == ID_index) { - if(byte_extract.id() == ID_index) - { - index_exprt &idx = to_index_expr(byte_extract); - ssa_rhs = [&]() -> exprt { - if(use_update) - { - update_exprt new_rhs{idx.array(), exprt{}, ssa_rhs}; - new_rhs.designator().push_back(index_designatort{idx.index()}); - return std::move(new_rhs); - } - else - return with_exprt{idx.array(), idx.index(), ssa_rhs}; - }(); - byte_extract = idx.array(); - } - else - { - member_exprt &member = to_member_expr(byte_extract); - const irep_idt &component_name = member.get_component_name(); - ssa_rhs = [&]() -> exprt { - if(use_update) - { - update_exprt new_rhs{member.compound(), exprt{}, ssa_rhs}; - new_rhs.designator().push_back( - member_designatort{component_name}); - return std::move(new_rhs); - } - else - { - with_exprt new_rhs( - member.compound(), exprt(ID_member_name), ssa_rhs); - new_rhs.where().set(ID_component_name, component_name); - return std::move(new_rhs); - } - }(); - byte_extract = member.compound(); - } + index_exprt &idx = to_index_expr(byte_extract); + ssa_rhs = [&]() -> exprt { + if(use_update) + { + update_exprt new_rhs{idx.array(), exprt{}, ssa_rhs}; + new_rhs.designator().push_back(index_designatort{idx.index()}); + return std::move(new_rhs); + } + else + return with_exprt{idx.array(), idx.index(), ssa_rhs}; + }(); + byte_extract = idx.array(); + } + else + { + member_exprt &member = to_member_expr(byte_extract); + const irep_idt &component_name = member.get_component_name(); + ssa_rhs = [&]() -> exprt { + if(use_update) + { + update_exprt new_rhs{member.compound(), exprt{}, ssa_rhs}; + new_rhs.designator().push_back(member_designatort{component_name}); + return std::move(new_rhs); + } + else + { + with_exprt new_rhs( + member.compound(), exprt(ID_member_name), ssa_rhs); + new_rhs.where().set(ID_component_name, component_name); + return std::move(new_rhs); + } + }(); + byte_extract = member.compound(); } - - // We may have shifted the previous lhs into the rhs; as the lhs is only - // L1-renamed, we need to rename again. - return assignmentt{to_ssa_expr(byte_extract), - std::move(assignment.original_lhs_skeleton), - state.rename(std::move(ssa_rhs), ns).get()}; } + + // We may have shifted the previous lhs into the rhs; as the lhs is only + // L1-renamed, we need to rename again. + return assignmentt{to_ssa_expr(byte_extract), + std::move(new_skeleton), + state.rename(std::move(ssa_rhs), ns).get()}; } return assignment; } @@ -346,7 +344,10 @@ void symex_assignt::assign_from_struct( lhs_field.id() == ID_symbol, "member of symbol should be susceptible to field-sensitivity"); - assign_symbol(to_ssa_expr(lhs_field), full_lhs, comp_rhs.second, guard); + assign_symbol( + to_ssa_expr(lhs_field), + expr_skeletont{lhs_field.type()}, + comp_rhs.second, guard); } } @@ -371,11 +372,14 @@ void symex_assignt::assign_non_struct_symbol( // introduced by assign_struct_member, are transformed into member // expressions on the LHS. If we add an option to disable field-sensitivity // in the future these should be omitted. - assignmentt assignment = rewrite_with_to_field_symbols( - state, - shift_indexed_access_to_lhs( - state, {lhs, full_lhs, std::move(l2_rhs)}, ns, symex_config.simplify_opt), - ns); + assignmentt assignment = {lhs, full_lhs, std::move(l2_rhs)}; + if(symex_config.simplify_opt) + { + assignment = shift_indexed_access_to_lhs( + state, std::move(assignment), ns); + } + assignment = rewrite_with_to_field_symbols( + state, std::move(assignment), ns); if(symex_config.simplify_opt) assignment.rhs = simplify_expr(std::move(assignment.rhs), ns); diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 7c4d63c854f..0788f6a8269 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -185,11 +185,13 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr) do_simplify(let_value); exprt::operandst value_assignment_guard; + const ssa_exprt l1_symbol = + to_ssa_expr(state.rename(let_expr.symbol(), ns).get()); symex_assignt{ state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target} .assign_symbol( - to_ssa_expr(state.rename(let_expr.symbol(), ns).get()), - expr_skeletont{}, + l1_symbol, + expr_skeletont{l1_symbol.type()}, let_value, value_assignment_guard); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 55ee9b67759..5334eb9339f 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -142,7 +142,7 @@ void goto_symext::parameter_assignments( exprt::operandst lhs_conditions; symex_assignt{state, assignment_type, ns, symex_config, target} - .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions); + .assign_rec(lhs, expr_skeletont{lhs.type()}, rhs, lhs_conditions); } if(it1!=arguments.end()) diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index b69c84a2854..f99861c703d 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -90,7 +90,8 @@ void goto_symext::symex_start_thread(statet &state) state.record_events.push(false); symex_assignt{ state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target} - .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions); + .assign_symbol( + lhs_l1, expr_skeletont{lhs_l1.type()}, rhs, lhs_conditions); state.record_events.pop(); } @@ -123,6 +124,6 @@ void goto_symext::symex_start_thread(statet &state) exprt::operandst lhs_conditions; symex_assignt{ state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target} - .assign_symbol(lhs, expr_skeletont{}, rhs, lhs_conditions); + .assign_symbol(lhs, expr_skeletont{lhs.type()}, rhs, lhs_conditions); } } diff --git a/src/util/byte_operators.h b/src/util/byte_operators.h index e28e42a52f3..dfc94044dd1 100644 --- a/src/util/byte_operators.h +++ b/src/util/byte_operators.h @@ -136,4 +136,11 @@ inline byte_update_exprt &to_byte_update_expr(exprt &expr) return static_cast(expr); } +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_byte_update_little_endian || + base.id() == ID_byte_update_big_endian; +} + #endif // CPROVER_UTIL_BYTE_OPERATORS_H diff --git a/unit/goto-symex/expr_skeleton.cpp b/unit/goto-symex/expr_skeleton.cpp index 5f406d3c13f..66bbb5e1d83 100644 --- a/unit/goto-symex/expr_skeleton.cpp +++ b/unit/goto-symex/expr_skeleton.cpp @@ -10,16 +10,21 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include +#include #include +#include #include +#include +#include #include +#include SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]") { const symbol_exprt foo{"foo", typet{}}; GIVEN("Skeletons `☐`, `☐[index]` and `☐.field1`") { - const expr_skeletont empty_skeleton; + const expr_skeletont empty_skeleton{foo.type()}; const signedbv_typet int_type{32}; const expr_skeletont index_skeleton = expr_skeletont::remove_op0(index_exprt{ @@ -61,3 +66,102 @@ SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]") } } } + +SCENARIO( + "revert byte extract", + "[core][goto-symex][symex-assign][expr-skeleton]") +{ + config.ansi_c.pointer_width = config.ansi_c.int_width = 32; + config.ansi_c.endianness = configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN; + const signedbv_typet int_type{32}; + const struct_typet my_struct{{struct_typet::componentt{"field1", int_type}, + struct_typet::componentt{"field2", int_type}}}; + const array_typet struct_array_type{my_struct, from_integer(10, size_type())}; + const symbol_exprt foo{"foo", struct_array_type}; + const symbol_exprt bar{"bar", my_struct}; + const symbol_exprt baz{"baz", int_type}; + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + GIVEN("Skeleton `☐[2].field2`") + { + const expr_skeletont skeleton = [&] { + const exprt skeleton_with_foo = member_exprt{ + index_exprt{foo, from_integer(2, size_type())}, "field2", int_type}; + return expr_skeletont::remove_op0(skeleton_with_foo) + .compose(expr_skeletont::remove_op0(skeleton_with_foo.op0())); + }(); + THEN( + "Reverting byte_extract with offset = 16, type = my_struct gives " + "skeleton `☐.field2` because `☐[2]` is equivalent to an offset of 16") + { + expr_skeletont s = expr_skeletont::revert_byte_extract( + skeleton, from_integer(16, size_type()), my_struct, ns); + REQUIRE(s.apply(bar) == member_exprt{bar, "field2", int_type}); + } + THEN( + "Reverting byte_extract with offset = 9, type = my_struct gives a " + "skeleton s `byte_extract(☐, 7).field2`") + { + expr_skeletont s = expr_skeletont::revert_byte_extract( + skeleton, from_integer(9, size_type()), my_struct, ns); + auto query = make_query(s.apply(bar)).as(); + REQUIRE(query.get().get_component_name() == "field2"); + REQUIRE( + query[0].as().get().offset() == + from_integer(7, size_type())); + } + THEN( + "Reverting byte_extract with offset = 20, type = int gives " + "skeleton `☐` because `☐[2].field2` is equivalent to an offset of 20") + { + expr_skeletont s = expr_skeletont::revert_byte_extract( + skeleton, from_integer(20, size_type()), int_type, ns); + REQUIRE(s.apply(baz) == baz); + } + THEN( + "Reverting byte_extract with offset = 18, type = int gives " + "skeleton `byte_extract(☐, 2)`") + { + expr_skeletont s = expr_skeletont::revert_byte_extract( + skeleton, from_integer(18, size_type()), int_type, ns); + auto query = make_query(s.apply(baz)).as(); + REQUIRE(query.get().offset() == from_integer(2, size_type())); + } + THEN( + "Reverting byte_extract with offset = 16, type = int gives " + "skeleton `byte_extract(☐, 4)`") + { + expr_skeletont s = expr_skeletont::revert_byte_extract( + skeleton, from_integer(16, size_type()), int_type, ns); + auto query = make_query(s.apply(baz)).as(); + REQUIRE(query.get().offset() == from_integer(4, size_type())); + } + } + GIVEN("Skeleton `☐[2].field1`") + { + const expr_skeletont skeleton = [&] { + const exprt skeleton_with_foo = member_exprt{ + index_exprt{foo, from_integer(2, size_type())}, "field1", int_type}; + return expr_skeletont::remove_op0(skeleton_with_foo) + .compose(expr_skeletont::remove_op0(skeleton_with_foo.op0())); + }(); + THEN( + "Reverting byte_extract with offset = 16, type = struct_type gives " + "skeleton `☐.field1` because `☐[2]` is equivalent to an offset of 16") + { + expr_skeletont s = expr_skeletont::revert_byte_extract( + skeleton, from_integer(16, size_type()), my_struct, ns); + auto query = make_query(s.apply(bar)).as(); + REQUIRE(query.get().get_component_name() == "field1"); + } + THEN( + "Reverting byte_extract with offset = 16, type = int gives " + "skeleton `☐` because `☐[2].field1` is also equivalent to an offset " + "of 16") + { + expr_skeletont s = expr_skeletont::revert_byte_extract( + skeleton, from_integer(16, size_type()), int_type, ns); + REQUIRE(s.apply(baz) == baz); + } + } +} diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp index e4ad23da4b5..1a3c034d738 100644 --- a/unit/goto-symex/symex_assign.cpp +++ b/unit/goto-symex/symex_assign.cpp @@ -16,8 +16,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include #include +#include +#include #include +#include #include +#include #include #include @@ -83,7 +87,7 @@ SCENARIO( ns, symex_config, target_equation} - .assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard); + .assign_symbol(ssa_foo, expr_skeletont{ssa_foo.type()}, rhs1, guard); THEN("An equation is added to the target") { REQUIRE(target_equation.SSA_steps.size() == 1); @@ -137,7 +141,8 @@ SCENARIO( ns, symex_config, target_equation}; - symex_assign.assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard); + symex_assign.assign_symbol( + ssa_foo, expr_skeletont{ssa_foo.type()}, rhs1, guard); THEN("An equation with an empty guard is added to the target") { REQUIRE(target_equation.SSA_steps.size() == 1); @@ -153,7 +158,8 @@ SCENARIO( WHEN("foo is assigned a second time") { const exprt rhs2 = from_integer(1841, int_type); - symex_assign.assign_symbol(ssa_foo, expr_skeletont{}, rhs2, guard); + symex_assign.assign_symbol( + ssa_foo, expr_skeletont{ssa_foo.type()}, rhs2, guard); THEN("A second equation is added to the target") { REQUIRE(target_equation.SSA_steps.size() == 2); @@ -250,4 +256,244 @@ SCENARIO( } } } + GIVEN("A RHS expression byte_update(foo, 0, 84523) where foo is an int") + { + config.ansi_c.endianness = configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN; + config.ansi_c.pointer_width = config.ansi_c.int_width = 32; + exprt::operandst guard; + symex_target_equationt target_equation{null_message_handler}; + const constant_exprt offset = from_integer(0, index_type()); + const constant_exprt value = from_integer(84523, int_type); + const exprt rhs = + byte_update_exprt{ID_byte_update_little_endian, foo, offset, value}; + + WHEN("Symbol `foo` is assigned the byte_update expression") + { + symex_config.simplify_opt = true; + symex_assignt{state, + symex_targett::assignment_typet::STATE, + ns, + symex_config, + target_equation} + .assign_symbol(ssa_foo, expr_skeletont{ssa_foo.type()}, rhs, guard); + THEN("An equation is added to the target") + { + REQUIRE(target_equation.SSA_steps.size() == 1); + SSA_stept step = target_equation.SSA_steps.back(); + THEN("LHS is 'foo!0#1'") + { + REQUIRE(step.ssa_lhs.get_identifier() == "foo!0#1"); + } + THEN("Original LHS is 'foo'") + { + REQUIRE( + make_query(step.original_full_lhs) + .as() + .get() + .get_identifier() == "foo"); + } + THEN("RHS is '84523") + { + REQUIRE(step.ssa_rhs == value); + } + } + } + } + // TODO: Should have one of each: + // - byte_update which simplifies to symbol + // - byte_update which simplifies to index + // - byte_update which simplifies to index with use_update + // - byte_update which simplifies to member + // - byte_update which simplifies to member with use_update + /// - byte_update of if_expr + // + config.ansi_c.endianness = configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN; + config.ansi_c.pointer_width = config.ansi_c.int_width = 32; + GIVEN( + "A RHS expression byte_update(array, 0, 84523) and a skeleton " + "`☐[0]` which corresponds to an original assignment array[0] = 84523") + { + exprt::operandst guard; + symex_target_equationt target_equation{null_message_handler}; + const constant_exprt offset = from_integer(0, index_type()); + const constant_exprt value = from_integer(84523, int_type); + const array_typet array_type{int_type, from_integer(2, int_type)}; + const symbol_exprt array{"array", array_type}; + add_to_symbol_table(symbol_table, array); + const byte_update_exprt rhs{ + ID_byte_update_little_endian, array, offset, value}; + const index_exprt original_lhs{array, from_integer(0, index_type())}; + const expr_skeletont skeleton = expr_skeletont::remove_op0(original_lhs); + const ssa_exprt ssa_array{array}; + + WHEN("Symbol `array` is assigned the byte_update expression") + { + symex_config.simplify_opt = true; + symex_assignt{state, + symex_targett::assignment_typet::STATE, + ns, + symex_config, + target_equation} + .assign_symbol(ssa_array, skeleton, rhs, guard); + THEN("An equation is added to the target") + { + REQUIRE(target_equation.SSA_steps.size() == 1); + SSA_stept step = target_equation.SSA_steps.back(); + THEN("LHS is 'array!0#1'") + { + REQUIRE(step.ssa_lhs.get_identifier() == "array!0#1"); + } + THEN("Original LHS is 'array[0]'") + { + REQUIRE(step.original_full_lhs == original_lhs); + } + THEN("RHS is 'with(array!0#0, 0, 84523)") + { + auto with_expr = make_query(step.ssa_rhs).as().get(); + REQUIRE( + make_query(with_expr.old()) + .as() + .get() + .get_identifier() == "array!0#0"); + REQUIRE(with_expr.where() == offset); + REQUIRE(with_expr.new_value() == value); + } + } + } + } + GIVEN( + "A RHS expression byte_update(array2d, 0, 53721) and a skeleton " + "`☐[0][0]` which corresponds to an original assignment " + "array2d[0][0] = 84523") + { + exprt::operandst guard; + symex_target_equationt target_equation{null_message_handler}; + const constant_exprt offset = from_integer(0, index_type()); + const constant_exprt value = from_integer(53721, int_type); + const array_typet array_type{int_type, from_integer(2, int_type)}; + const array_typet array2d_type{array_type, from_integer(2, int_type)}; + const symbol_exprt array2d{"array2d", array2d_type}; + add_to_symbol_table(symbol_table, array2d); + const ssa_exprt ssa_array{array2d}; + const byte_update_exprt rhs{ + ID_byte_update_little_endian, array2d, offset, value}; + const index_exprt original_lhs{ + index_exprt{array2d, from_integer(0, index_type())}, + from_integer(0, index_type())}; + const expr_skeletont skeleton = + expr_skeletont::remove_op0(original_lhs) + .compose(expr_skeletont::remove_op0(original_lhs.array())); + + WHEN("Symbol `array` is assigned the byte_update expression") + { + symex_config.simplify_opt = true; + symex_assignt{state, + symex_targett::assignment_typet::STATE, + ns, + symex_config, + target_equation} + .assign_symbol(ssa_array, skeleton, rhs, guard); + THEN("An equation is added to the target") + { + REQUIRE(target_equation.SSA_steps.size() == 1); + SSA_stept step = target_equation.SSA_steps.back(); + THEN("LHS is 'array!0#1'") + { + REQUIRE(step.ssa_lhs.get_identifier() == "array2d!0#1"); + } + THEN("Original LHS is 'array[0][0]'") + { + REQUIRE(step.original_full_lhs == original_lhs); + } + THEN("RHS is 'with(array!0#0, 0, with(array2d!0#0[0], 0, 84523)") + { + auto with_expr = make_query(step.ssa_rhs).as().get(); + REQUIRE( + make_query(with_expr.old()) + .as() + .get() + .get_identifier() == "array2d!0#0"); + REQUIRE(with_expr.where() == offset); + REQUIRE( + make_query(with_expr.new_value()) + .as()[0] + .as()[0] + .as() + .get() + .get_identifier() == "array2d!0#0"); + } + } + } + } + GIVEN( + "A RHS byte_update({array[0], array[1]}, 0, 53721), " + "a LHS array and a " + "skeleton `☐[0]` which corresponds to an original assignment " + "{array[0], array[1]}[0] = 84523") + { + exprt::operandst guard; + symex_target_equationt target_equation{null_message_handler}; + const constant_exprt offset = from_integer(0, index_type()); + const constant_exprt value = from_integer(53721, int_type); + const array_typet array_type{int_type, from_integer(2, int_type)}; + const symbol_exprt array{"array", array_type}; + add_to_symbol_table(symbol_table, array); + const array_exprt lhs{ + exprt::operandst{index_exprt{array, from_integer(0, index_type())}, + index_exprt{array, from_integer(1, index_type())}}, + array_type}; + const ssa_exprt ssa_lhs{array}; + const byte_update_exprt rhs{ + ID_byte_update_little_endian, lhs, offset, value}; + const index_exprt original_lhs{ + lhs, from_integer(0, index_type()), int_type}; + const expr_skeletont skeleton = expr_skeletont::remove_op0(original_lhs); + + WHEN("`array` is assigned the byte_update expression") + { + symex_config.simplify_opt = true; + symex_assignt{state, + symex_targett::assignment_typet::STATE, + ns, + symex_config, + target_equation} + .assign_symbol(ssa_lhs, skeleton, rhs, guard); + THEN("An equation is added to the target") + { + REQUIRE(target_equation.SSA_steps.size() == 1); + SSA_stept step = target_equation.SSA_steps.back(); + THEN("LHS is 'array!0#1'") + { + REQUIRE(step.ssa_lhs.get_identifier() == "array!0#1"); + } + THEN("Original LHS is 'array[0][0]'") + { + REQUIRE( + make_query(step.original_full_lhs) + .as()[0] + .as()[0] + .as() + .get() + .get_identifier() == "array"); + } + THEN("RHS is 'with(array!0#0, 0, with(array!0#0[0], 0, 84523)") + { + auto with_expr = make_query(step.ssa_rhs).as().get(); + REQUIRE( + make_query(with_expr.old()) + .as() + .get() + .get_identifier() == "array!0#0"); + REQUIRE(with_expr.where() == offset); + REQUIRE( + make_query(with_expr.new_value()) + .as()[0] + .as()[0] + .as() + .get() + .get_identifier() == "array!0#0"); + } + } + } + } } diff --git a/unit/testing-utils/expr_query.h b/unit/testing-utils/expr_query.h index 684a6a53e75..41ce00bf410 100644 --- a/unit/testing-utils/expr_query.h +++ b/unit/testing-utils/expr_query.h @@ -54,7 +54,7 @@ class expr_queryt T value; }; -expr_queryt make_query(exprt e) +inline expr_queryt make_query(exprt e) { return expr_queryt(std::move(e)); }