diff --git a/regression/cbmc/field-sensitivity17/main.c b/regression/cbmc/field-sensitivity17/main.c new file mode 100644 index 00000000000..d4fe8fffc28 --- /dev/null +++ b/regression/cbmc/field-sensitivity17/main.c @@ -0,0 +1,9 @@ +union U +{ + unsigned char buf[2]; +} s; + +int main() +{ + __CPROVER_assert(s.buf[0] == 0, ""); +} diff --git a/regression/cbmc/field-sensitivity17/test.desc b/regression/cbmc/field-sensitivity17/test.desc new file mode 100644 index 00000000000..3ed4abdf906 --- /dev/null +++ b/regression/cbmc/field-sensitivity17/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--max-field-sensitivity-array-size 1 +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The test is a minimized version of code generated using Kani. It should pass +irrespective of whether field sensitivity is applied to the array or not. (The +original example was unexpectedly failing with an array size of 65, but passed +with an array size of 64 or less.) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 46427c0fd50..0a5a56b6213 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -31,6 +31,97 @@ exprt field_sensitivityt::apply( return get_fields(ns, state, ssa_expr, true); } +exprt field_sensitivityt::apply_byte_extract( + const namespacet &ns, + goto_symex_statet &state, + const byte_extract_exprt &be, + bool write) const +{ + if( + (be.op().type().id() != ID_union && be.op().type().id() != ID_union_tag) || + !is_ssa_expr(be.op()) || !be.offset().is_constant()) + { + return be; + } + + const union_typet &type = be.op().type().id() == ID_union_tag + ? ns.follow_tag(to_union_tag_type(be.op().type())) + : to_union_type(be.op().type()); + for(const auto &comp : type.components()) + { + ssa_exprt tmp = to_ssa_expr(be.op()); + bool was_l2 = !tmp.get_level_2().empty(); + tmp.remove_level_2(); + const member_exprt member{tmp.get_original_expr(), comp}; + auto recursive_member = + get_subexpression_at_offset(member, be.offset(), be.type(), ns); + if(!recursive_member.has_value()) + continue; + + // We need to inspect the access path as the resulting expression may + // involve index expressions. When array field sensitivity is disabled + // or the size of the array that is indexed into is larger than + // max_field_sensitivity_array_size then only the expression up to (but + // excluding) said index expression can be turned into an ssa_exprt. + exprt full_exprt = *recursive_member; + exprt *for_ssa = &full_exprt; + exprt *parent = for_ssa; + while(parent->id() == ID_typecast) + parent = &to_typecast_expr(*parent).op(); + while(parent->id() == ID_member || parent->id() == ID_index) + { + if(parent->id() == ID_member) + { + parent = &to_member_expr(*parent).compound(); + } + else + { + parent = &to_index_expr(*parent).array(); +#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY + if( + !to_array_type(parent->type()).size().is_constant() || + numeric_cast_v( + to_constant_expr(to_array_type(parent->type()).size())) > + max_field_sensitivity_array_size) + { + for_ssa = parent; + } +#else + for_ssa = parent; +#endif // ENABLE_ARRAY_FIELD_SENSITIVITY + } + } + + if(for_ssa->id() == ID_index || for_ssa->id() == ID_member) + { + tmp.type() = for_ssa->type(); + tmp.set_expression(*for_ssa); + if(was_l2) + { + *for_ssa = + apply(ns, state, state.rename(std::move(tmp), ns).get(), write); + } + else + *for_ssa = apply(ns, state, std::move(tmp), write); + + return full_exprt; + } + else if(for_ssa->id() == ID_typecast) + { + if(was_l2) + { + *for_ssa = apply(ns, state, state.rename(*for_ssa, ns).get(), write); + } + else + *for_ssa = apply(ns, state, std::move(*for_ssa), write); + + return full_exprt; + } + } + + return be; +} + exprt field_sensitivityt::apply( const namespacet &ns, goto_symex_statet &state, @@ -93,55 +184,7 @@ exprt field_sensitivityt::apply( !write && (expr.id() == ID_byte_extract_little_endian || expr.id() == ID_byte_extract_big_endian)) { - const byte_extract_exprt &be = to_byte_extract_expr(expr); - if( - (be.op().type().id() == ID_union || - be.op().type().id() == ID_union_tag) && - is_ssa_expr(be.op()) && be.offset().is_constant()) - { - const union_typet &type = - be.op().type().id() == ID_union_tag - ? ns.follow_tag(to_union_tag_type(be.op().type())) - : to_union_type(be.op().type()); - for(const auto &comp : type.components()) - { - ssa_exprt tmp = to_ssa_expr(be.op()); - bool was_l2 = !tmp.get_level_2().empty(); - tmp.remove_level_2(); - const member_exprt member{tmp.get_original_expr(), comp}; - auto recursive_member = - get_subexpression_at_offset(member, be.offset(), be.type(), ns); - if( - recursive_member.has_value() && - (recursive_member->id() == ID_member || - recursive_member->id() == ID_index)) - { - tmp.type() = be.type(); - tmp.set_expression(*recursive_member); - if(was_l2) - { - return apply( - ns, state, state.rename(std::move(tmp), ns).get(), write); - } - else - return apply(ns, state, std::move(tmp), write); - } - else if( - recursive_member.has_value() && recursive_member->id() == ID_typecast) - { - if(was_l2) - { - return apply( - ns, - state, - state.rename(std::move(*recursive_member), ns).get(), - write); - } - else - return apply(ns, state, std::move(*recursive_member), write); - } - } - } + return apply_byte_extract(ns, state, to_byte_extract_expr(expr), write); } #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY else if(expr.id() == ID_index) diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h index 7ab159638a2..12606321ce0 100644 --- a/src/goto-symex/field_sensitivity.h +++ b/src/goto-symex/field_sensitivity.h @@ -11,6 +11,7 @@ Author: Michael Tautschnig #include +class byte_extract_exprt; class namespacet; class goto_symex_statet; class symex_targett; @@ -221,6 +222,13 @@ class field_sensitivityt exprt e, const value_sett &value_set, const namespacet &ns) const; + + /// \copydoc apply(const namespacet&,goto_symex_statet&,exprt,bool) const + [[nodiscard]] exprt apply_byte_extract( + const namespacet &ns, + goto_symex_statet &state, + const byte_extract_exprt &expr, + bool write) const; }; #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H