From ad8086f64864482d2c27d1aae4930b2f105b110a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 6 Jan 2023 22:12:35 +0000 Subject: [PATCH] Field sensitivity: fully expand nested objects When applying field sensitivity to an expression we must expand all levels. In the included test we previously constructed a member symbol (`var_11..value`) as right-hand side that still was of struct type. Instead, we must create a struct expression composed of all its members (here: `{ var_11..value.._0 }`). Also, we must not keep nested expandable members in the propagation map for phi nodes don't merge on them. Fixes: #7462 --- regression/cbmc/field-sensitivity15/main.c | 55 +++++++++++++++ regression/cbmc/field-sensitivity15/test.desc | 9 +++ regression/cbmc/field-sensitivity16/main.c | 67 +++++++++++++++++++ regression/cbmc/field-sensitivity16/test.desc | 9 +++ src/goto-symex/field_sensitivity.cpp | 48 ++++++++----- src/goto-symex/symex_assign.cpp | 8 --- 6 files changed, 173 insertions(+), 23 deletions(-) create mode 100644 regression/cbmc/field-sensitivity15/main.c create mode 100644 regression/cbmc/field-sensitivity15/test.desc create mode 100644 regression/cbmc/field-sensitivity16/main.c create mode 100644 regression/cbmc/field-sensitivity16/test.desc diff --git a/regression/cbmc/field-sensitivity15/main.c b/regression/cbmc/field-sensitivity15/main.c new file mode 100644 index 00000000000..bbe22ad46ca --- /dev/null +++ b/regression/cbmc/field-sensitivity15/main.c @@ -0,0 +1,55 @@ +#include + +struct _12817932758143517076 +{ + unsigned char _0; +}; + +struct _14237415465709481864_union__Err +{ + unsigned char cap; +}; + +union _14237415465709481864_union +{ + struct _12817932758143517076 value; + struct _14237415465709481864_union__Err Err; +}; + +void main(void) +{ + unsigned int x; // nondet + + // the following is crucial (else pn trivially simplifies to 0) + unsigned int var_7 = x; + unsigned int pn = x - var_7; + + unsigned char raw; + unsigned char mask; + if(pn == 0) + { + raw = 1; + mask = 0; + } + else + assert(0); + + union _14237415465709481864_union var_11; + if(mask != 0) + { + var_11.Err.cap = 0; + } + else + { + var_11.value._0 = 1; + goto bb5; + } + + // required to make this test fail (before the fix) + int tmp = 1; + +bb5:; + struct _12817932758143517076 truncated_packet_number = var_11.value; + unsigned char r = truncated_packet_number._0; + assert(raw == r); +} diff --git a/regression/cbmc/field-sensitivity15/test.desc b/regression/cbmc/field-sensitivity15/test.desc new file mode 100644 index 00000000000..bba818d84cd --- /dev/null +++ b/regression/cbmc/field-sensitivity15/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The test is a minimized version of code generated from s2n-quic using Kani. diff --git a/regression/cbmc/field-sensitivity16/main.c b/regression/cbmc/field-sensitivity16/main.c new file mode 100644 index 00000000000..bfec1b50970 --- /dev/null +++ b/regression/cbmc/field-sensitivity16/main.c @@ -0,0 +1,67 @@ +#include + +struct _17626587426415757163 +{ + unsigned long int cap; +}; + +struct _14237415465709481864_union__Err +{ + struct _17626587426415757163 _0; +}; + +struct _12817932758143517076_union__U8 +{ + unsigned char _0; +}; + +union _12817932758143517076_union_ +{ + struct _12817932758143517076_union__U8 U8; +}; + +struct _2123760316064833246_ +{ + union _12817932758143517076_union_ cases; +}; + +union _14237415465709481864_union +{ + struct _2123760316064833246_ Ok; + struct _14237415465709481864_union__Err Err; +}; + +void main(void) +{ + unsigned int x; // nondet + + // the following is crucial (else pn trivially simplifies to 0) + unsigned int var_7 = x; + unsigned int pn = x - var_7; + + unsigned char mask; + if(pn == 0) + mask = 0; + else + assert(0); + + union _14237415465709481864_union var_11; + if(mask != 0) + { + assert(0); + var_11.Err._0.cap = 0; + } + else + { + var_11.Ok.cases.U8._0 = 1; + goto bb5; + } + + // keep this + int tmp = 1; +bb5:; + + struct _2123760316064833246_ truncated_packet_number = var_11.Ok; + assert(1 == var_11.Ok.cases.U8._0); + assert(1 == truncated_packet_number.cases.U8._0); +} diff --git a/regression/cbmc/field-sensitivity16/test.desc b/regression/cbmc/field-sensitivity16/test.desc new file mode 100644 index 00000000000..6dc9d7fb7ce --- /dev/null +++ b/regression/cbmc/field-sensitivity16/test.desc @@ -0,0 +1,9 @@ +CORE broken-z3-smt-backend +main.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The test is a minimized version of code generated from s2n-quic using Kani. diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 0cb2a879a8b..a430fe4c596 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -84,9 +84,9 @@ exprt field_sensitivityt::apply( member.struct_op() = tmp.get_original_expr(); tmp.set_expression(member); if(was_l2) - return state.rename(std::move(tmp), ns).get(); + return apply(ns, state, state.rename(std::move(tmp), ns).get(), write); else - return std::move(tmp); + return apply(ns, state, std::move(tmp), write); } } else if( @@ -116,9 +116,12 @@ exprt field_sensitivityt::apply( tmp.type() = be.type(); tmp.set_expression(*recursive_member); if(was_l2) - return state.rename(std::move(tmp), ns).get(); + { + return apply( + ns, state, state.rename(std::move(tmp), ns).get(), write); + } else - return std::move(tmp); + return apply(ns, state, std::move(tmp), write); } } } @@ -171,9 +174,12 @@ exprt field_sensitivityt::apply( index.index() = l2_index.get(); tmp.set_expression(index); if(was_l2) - return state.rename(std::move(tmp), ns).get(); + { + return apply( + ns, state, state.rename(std::move(tmp), ns).get(), write); + } else - return std::move(tmp); + return apply(ns, state, std::move(tmp), write); } else if(!write) { @@ -293,6 +299,14 @@ void field_sensitivityt::field_assignments( { field_assignments_rec( ns, state, lhs_fs, rhs, target, allow_pointer_unsoundness); + // Erase the composite symbol from our working state. Note that we need to + // have it in the propagation table and the value set while doing the field + // assignments, thus we cannot skip putting it in there above. + if(is_divisible(lhs, true)) + { + state.propagation.erase_if_exists(lhs.get_identifier()); + state.value_set.erase_symbol(lhs, ns); + } } } @@ -316,15 +330,11 @@ void field_sensitivityt::field_assignments_rec( { if(is_ssa_expr(lhs_fs)) { - const ssa_exprt ssa_lhs = state - .assignment( - to_ssa_expr(lhs_fs), - ssa_rhs, - ns, - true, - true, - allow_pointer_unsoundness) - .get(); + const ssa_exprt &l1_lhs = to_ssa_expr(lhs_fs); + const ssa_exprt ssa_lhs = + state + .assignment(l1_lhs, ssa_rhs, ns, true, true, allow_pointer_unsoundness) + .get(); // do the assignment target.assignment( @@ -335,6 +345,14 @@ void field_sensitivityt::field_assignments_rec( ssa_rhs, state.source, symex_targett::assignment_typet::STATE); + // Erase the composite symbol from our working state. Note that we need to + // have it in the propagation table and the value set while doing the field + // assignments, thus we cannot skip putting it in there above. + if(is_divisible(l1_lhs, true)) + { + state.propagation.erase_if_exists(l1_lhs.get_identifier()); + state.value_set.erase_symbol(l1_lhs, ns); + } } else if( ssa_rhs.type().id() == ID_struct || ssa_rhs.type().id() == ID_struct_tag) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 8da10ae2c22..9786b33e41b 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -215,14 +215,6 @@ void symex_assignt::assign_non_struct_symbol( assignment.rhs, target, symex_config.allow_pointer_unsoundness); - // Erase the composite symbol from our working state. Note that we need to - // have it in the propagation table and the value set while doing the field - // assignments, thus we cannot skip putting it in there above. - if(state.field_sensitivity.is_divisible(l1_lhs, true)) - { - state.propagation.erase_if_exists(l1_lhs.get_identifier()); - state.value_set.erase_symbol(l1_lhs, ns); - } } }