Merge pull request #7472 from tautschnig/bugfixes/fs-recursive

Field sensitivity: fully expand nested objects

Author: tautschnig

Diff for: regression/cbmc/field-sensitivity15/main.c

@@ -0,0 +1,55 @@
+#include <assert.h>
+
+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 for: 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 for: regression/cbmc/field-sensitivity16/main.c

@@ -0,0 +1,67 @@
+#include <assert.h>
+
+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 for: 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 for: 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 for: 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);
-    }
   }
 }