SPLIT

Author: tautschnig

regression/cbmc/array-cell-sensitivity15/test.desc

@@ -3,7 +3,7 @@ access.c
 --program-only
 ^EXIT=0$
 ^SIGNAL=0$
-s!0@1#1\.\.n == \{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] } WITH \[\(.*\)i!0@1#2:=k!0@1#1\]
+s!0@1#2\.\.n == \{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] } WITH \[\(.*\)i!0@1#2:=k!0@1#1\]
 --
 byte_update
 --

regression/cbmc/array-cell-sensitivity8/test.desc

@@ -10,7 +10,7 @@ main::1::array!0@1#2\[\[6\]\] =
 main::1::array!0@1#2\[\[7\]\] =
 main::1::array!0@1#2\[\[8\]\] =
 main::1::array!0@1#2\[\[9\]\] =
-main::1::array!0@1#2 =.*byte_extract_little_endian
+main::1::array!0@1#3 =.*byte_extract_little_endian
 main::1::array!0@1#3\[\[0\]\] =
 main::1::array!0@1#3\[\[1\]\] =
 main::1::array!0@1#3\[\[2\]\] =

regression/cbmc/field-sensitivity9/test.desc

@@ -1,8 +1,8 @@
 CORE
 test.c
 --show-vcc
-main::1::a1!0@1#1 =
-main::1::a2!0@1#1 =
+main::1::a1!0@1#2 =
+main::1::a2!0@1#2 =
 main::1::a1!0@1#2\.\.x =
 main::1::a1!0@1#2\.\.y =
 main::1::a1!0@1#2\.\.z =

src/goto-symex/field_sensitivity.cpp

@@ -9,8 +9,9 @@ Author: Michael Tautschnig
 #include "field_sensitivity.h"
 
 #include <util/arith_tools.h>
+#include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/simplify_expr.h>
-#include <util/std_expr.h>
 
 #include "goto_symex_state.h"
 #include "symex_target.h"
@@ -26,7 +27,7 @@ exprt field_sensitivityt::apply(
   if(!run_apply || write)
     return std::move(ssa_expr);
   else
-    return get_fields(ns, state, ssa_expr);
+    return get_fields(ns, state, ssa_expr, true);
 }
 
 exprt field_sensitivityt::apply(
@@ -72,7 +73,9 @@ exprt field_sensitivityt::apply(
     if(
       is_ssa_expr(member.struct_op()) &&
       (member.struct_op().type().id() == ID_struct ||
-       member.struct_op().type().id() == ID_struct_tag))
+       member.struct_op().type().id() == ID_struct_tag ||
+       member.struct_op().type().id() == ID_union ||
+       member.struct_op().type().id() == ID_union_tag))
     {
       // place the entire member expression, not just the struct operand, in an
       // SSA expression
@@ -88,6 +91,35 @@ exprt field_sensitivityt::apply(
         return std::move(tmp);
     }
   }
+  else if(
+    !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_zero())
+    {
+      const union_typet &type = to_union_type(ns.follow(be.op().type()));
+      for(const auto &comp : type.components())
+      {
+        if(comp.type() == be.type())
+        {
+          ssa_exprt tmp = to_ssa_expr(be.op());
+          bool was_l2 = !tmp.get_level_2().empty();
+          tmp.remove_level_2();
+          member_exprt member{tmp.get_original_expr(), comp};
+          tmp.type() = be.type();
+          tmp.set_expression(member);
+          if(was_l2)
+            return state.rename(std::move(tmp), ns).get();
+          else
+            return std::move(tmp);
+        }
+      }
+    }
+  }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(expr.id() == ID_index)
   {
@@ -144,7 +176,7 @@ exprt field_sensitivityt::apply(
         {
           // Expand the array and return `{array[0]; array[1]; ...}[index]`
           exprt expanded_array =
-            get_fields(ns, state, to_ssa_expr(index.array()));
+            get_fields(ns, state, to_ssa_expr(index.array()), true);
           return index_exprt{std::move(expanded_array), index.index()};
         }
       }
@@ -157,33 +189,48 @@ exprt field_sensitivityt::apply(
 exprt field_sensitivityt::get_fields(
   const namespacet &ns,
   goto_symex_statet &state,
-  const ssa_exprt &ssa_expr) const
+  const ssa_exprt &ssa_expr,
+  bool disjoined_fields_only) const
 {
-  if(ssa_expr.type().id() == ID_struct || ssa_expr.type().id() == ID_struct_tag)
+  if(
+    ssa_expr.type().id() == ID_struct ||
+    ssa_expr.type().id() == ID_struct_tag ||
+    (!disjoined_fields_only && (ssa_expr.type().id() == ID_union ||
+                                ssa_expr.type().id() == ID_union_tag)))
   {
-    const struct_typet &type = to_struct_type(ns.follow(ssa_expr.type()));
+    const struct_union_typet &type =
+      to_struct_union_type(ns.follow(ssa_expr.type()));
     const struct_union_typet::componentst &components = type.components();
 
-    struct_exprt::operandst fields;
+    exprt::operandst fields;
     fields.reserve(components.size());
 
-    const exprt &struct_op = ssa_expr.get_original_expr();
+    const exprt &compound_op = ssa_expr.get_original_expr();
 
     for(const auto &comp : components)
     {
       ssa_exprt tmp = ssa_expr;
       bool was_l2 = !tmp.get_level_2().empty();
       tmp.remove_level_2();
-      tmp.set_expression(member_exprt{struct_op, comp.get_name(), comp.type()});
+      tmp.set_expression(
+        member_exprt{compound_op, comp.get_name(), comp.type()});
+      exprt field = get_fields(ns, state, tmp, disjoined_fields_only);
       if(was_l2)
       {
-        fields.push_back(state.rename(get_fields(ns, state, tmp), ns).get());
+        fields.emplace_back(state.rename(std::move(field), ns).get());
       }
       else
-        fields.push_back(get_fields(ns, state, tmp));
+        fields.emplace_back(std::move(field));
     }
 
-    return struct_exprt(std::move(fields), ssa_expr.type());
+    if(
+      disjoined_fields_only && (ssa_expr.type().id() == ID_struct ||
+                                ssa_expr.type().id() == ID_struct_tag))
+    {
+      return struct_exprt{std::move(fields), ssa_expr.type()};
+    }
+    else
+      return field_sensitive_ssa_exprt{ssa_expr, std::move(fields)};
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
@@ -210,15 +257,19 @@ exprt field_sensitivityt::get_fields(
       bool was_l2 = !tmp.get_level_2().empty();
       tmp.remove_level_2();
       tmp.set_expression(index);
+      exprt element = get_fields(ns, state, tmp, disjoined_fields_only);
       if(was_l2)
       {
-        elements.push_back(state.rename(get_fields(ns, state, tmp), ns).get());
+        elements.emplace_back(state.rename(std::move(element), ns).get());
       }
       else
-        elements.push_back(get_fields(ns, state, tmp));
+        elements.emplace_back(std::move(element));
     }
 
-    return array_exprt(std::move(elements), type);
+    if(disjoined_fields_only)
+      return array_exprt(std::move(elements), type);
+    else
+      return field_sensitive_ssa_exprt{ssa_expr, std::move(elements)};
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else
@@ -233,15 +284,15 @@ void field_sensitivityt::field_assignments(
   symex_targett &target,
   bool allow_pointer_unsoundness)
 {
-  const exprt lhs_fs = apply(ns, state, lhs, false);
+  PRECONDITION(run_apply);
+  const exprt lhs_fs = get_fields(ns, state, lhs, false);
 
   if(lhs != lhs_fs)
   {
-    bool run_apply_bak = run_apply;
     run_apply = false;
     field_assignments_rec(
       ns, state, lhs_fs, rhs, target, allow_pointer_unsoundness);
-    run_apply = run_apply_bak;
+    run_apply = true;
   }
 }
 
@@ -302,6 +353,43 @@ void field_sensitivityt::field_assignments_rec(
         simplify_opt(member_exprt{ssa_rhs, comp.get_name(), comp.type()}, ns);
       const exprt &member_lhs = *fs_it;
 
+      field_assignments_rec(
+        ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
+      ++fs_it;
+    }
+  }
+  else if(
+    ssa_rhs.type().id() == ID_union || ssa_rhs.type().id() == ID_union_tag)
+  {
+    const union_typet &type = to_union_type(ns.follow(ssa_rhs.type()));
+    const struct_union_typet::componentst &components = type.components();
+
+    PRECONDITION(
+      components.empty() ||
+      (lhs_fs.has_operands() && lhs_fs.operands().size() == components.size()));
+
+    exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
+    for(const auto &comp : components)
+    {
+      const exprt member_rhs = simplify_opt(
+        make_byte_extract(
+          ssa_rhs, from_integer(0, c_index_type()), comp.type()),
+        ns);
+      const exprt &member_lhs = *fs_it;
+
+      if(
+        auto fs_ssa =
+          expr_try_dynamic_cast<field_sensitive_ssa_exprt>(member_lhs))
+      {
+        field_assignments_rec(
+          ns,
+          state,
+          fs_ssa->get_object_ssa(),
+          member_rhs,
+          target,
+          allow_pointer_unsoundness);
+      }
+
       field_assignments_rec(
         ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
       ++fs_it;
@@ -350,7 +438,9 @@ void field_sensitivityt::field_assignments_rec(
   }
 }
 
-bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
+bool field_sensitivityt::is_divisible(
+  const ssa_exprt &expr,
+  bool disjoined_fields_only) const
 {
   if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
     return true;
@@ -366,6 +456,13 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
   }
 #endif
 
+  if(
+    !disjoined_fields_only &&
+    (expr.type().id() == ID_union || expr.type().id() == ID_union_tag))
+  {
+    return true;
+  }
+
   return false;
 }
 

src/goto-symex/field_sensitivity.h

@@ -9,16 +9,51 @@ Author: Michael Tautschnig
 #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 
-#include <cstddef>
-
 #include <util/nodiscard.h>
+#include <util/ssa_expr.h>
 
-class exprt;
-class ssa_exprt;
 class namespacet;
 class goto_symex_statet;
 class symex_targett;
 
+class field_sensitive_ssa_exprt : public exprt
+{
+public:
+  field_sensitive_ssa_exprt(const ssa_exprt &ssa, exprt::operandst &&fields)
+    : exprt(ID_field_sensitive_ssa, ssa.type(), std::move(fields))
+  {
+    add(ID_expression, ssa);
+  }
+
+  const ssa_exprt &get_object_ssa() const
+  {
+    return static_cast<const ssa_exprt &>(find(ID_expression));
+  }
+};
+
+template <>
+inline bool can_cast_expr<field_sensitive_ssa_exprt>(const exprt &base)
+{
+  return base.id() == ID_field_sensitive_ssa;
+}
+
+inline const field_sensitive_ssa_exprt &
+to_field_sensitive_ssa_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_field_sensitive_ssa);
+  const field_sensitive_ssa_exprt &ret =
+    static_cast<const field_sensitive_ssa_exprt &>(expr);
+  return ret;
+}
+
+inline field_sensitive_ssa_exprt &to_field_sensitive_ssa_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_field_sensitive_ssa);
+  field_sensitive_ssa_exprt &ret =
+    static_cast<field_sensitive_ssa_exprt &>(expr);
+  return ret;
+}
+
 /// Control granularity of object accesses
 ///
 /// [Field sensitivity](\ref field_sensitivityt) is a transformation of the
@@ -128,33 +163,40 @@ class field_sensitivityt
   apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
     const;
   /// \copydoc apply(const namespacet&,goto_symex_statet&,exprt,bool) const
+  NODISCARD
   exprt apply(
     const namespacet &ns,
     goto_symex_statet &state,
     ssa_exprt expr,
     bool write) const;
 
   /// Compute an expression representing the individual components of a
-  /// field-sensitive SSA representation of \p ssa_expr.
+  /// field-sensitive SSA representation of \p ssa_expr. When
+  /// \p disjoined_fields_only is false, the resulting expression must be
+  /// handled with care as it will have multiple operands but empty `id()`.
   /// \param ns: a namespace to resolve type symbols/tag types
   /// \param [in,out] state: symbolic execution state
   /// \param ssa_expr: the expression to evaluate
+  /// \param disjoined_fields_only: whether to expand unions (`false`) or not (`true`)
   /// \return Expanded expression; for example, for a \p ssa_expr of some struct
   ///   type, a `struct_exprt` with each component now being an SSA expression
   ///   is built.
+  NODISCARD
   exprt get_fields(
     const namespacet &ns,
     goto_symex_statet &state,
-    const ssa_exprt &ssa_expr) const;
+    const ssa_exprt &ssa_expr,
+    bool disjoined_fields_only) const;
 
   /// Determine whether \p expr would translate to an atomic SSA expression
   /// (returns false) or a composite object made of several SSA expressions as
   /// components (such as a struct with each member becoming an individual SSA
   /// expression, return true in this case).
   /// \param expr: the expression to evaluate
+  /// \param disjoined_fields_only: whether to expand unions (`false`) or not (`true`)
   /// \return False, if and only if, \p expr would be a single field-sensitive
   /// SSA expression.
-  bool is_divisible(const ssa_exprt &expr) const;
+  bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
 
 private:
   /// whether or not to invoke \ref field_sensitivityt::apply