WIP: Field sensitivity for unions

Field-sensitive tracking of unions permits propagating constants even
when those do not affect the full width of the union (implying that some
bits remain non-constant).

Author: tautschnig

regression/cbmc/union18/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+union u_type
+{
+  int i;
+  char ch;
+};
+
+int main()
+{
+  union u_type u;
+
+  u.ch = 2;
+  assert(u.ch == 2);
+}

regression/cbmc/union18/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This should be fully solved by constant propagation when union field-sensitivity
+is in place.

src/goto-symex/field_sensitivity.cpp

@@ -9,6 +9,8 @@ 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>
 
@@ -17,6 +19,27 @@ Author: Michael Tautschnig
 
 #define ENABLE_ARRAY_FIELD_SENSITIVITY
 
+/// Produce a `struct_exprt` or an `array_exprt` when multiple fields are
+/// provided; else just return the original expression.
+static exprt fields_to_expr(std::vector<exprt> &&operands, const ssa_exprt &original_ssa_expr)
+{
+  const typet &type = original_ssa_expr.type();
+  if(type.id() == ID_struct || type.id() == ID_struct_tag)
+  {
+    return struct_exprt{std::move(operands), type};
+  }
+  else if(type.id() == ID_array)
+  {
+    return array_exprt{std::move(operands), type};
+  }
+  else
+  {
+    DATA_INVARIANT(operands.size() == 1, "only arrays or structs yield multiple fields");
+    DATA_INVARIANT(operands.front() == original_ssa_expr, "expression should be unmodified");
+    return std::move(operands.front());
+  }
+}
+
 exprt field_sensitivityt::apply(
   const namespacet &ns,
   goto_symex_statet &state,
@@ -26,7 +49,7 @@ exprt field_sensitivityt::apply(
   if(!run_apply || write)
     return std::move(ssa_expr);
   else
-    return get_fields(ns, state, ssa_expr);
+    return fields_to_expr(get_fields(ns, state, ssa_expr), ssa_expr);
 }
 
 exprt field_sensitivityt::apply(
@@ -72,7 +95,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 +113,35 @@ exprt field_sensitivityt::apply(
         return std::move(tmp);
     }
   }
+  else if(
+    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) &&
+      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)
   {
@@ -143,8 +197,9 @@ exprt field_sensitivityt::apply(
         else if(!write)
         {
           // Expand the array and return `{array[0]; array[1]; ...}[index]`
+          const ssa_exprt &array = to_ssa_expr(index.array());
           exprt expanded_array =
-            get_fields(ns, state, to_ssa_expr(index.array()));
+            fields_to_expr(get_fields(ns, state, array), array);
           return index_exprt{std::move(expanded_array), index.index()};
         }
       }
@@ -154,36 +209,39 @@ exprt field_sensitivityt::apply(
   return expr;
 }
 
-exprt field_sensitivityt::get_fields(
+exprt::operandst field_sensitivityt::get_fields(
   const namespacet &ns,
   goto_symex_statet &state,
   const ssa_exprt &ssa_expr) 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 ||
+    (do_union &&
+    (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 = fields_to_expr(get_fields(ns, state, tmp), tmp);
       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());
+    return fields;
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
@@ -210,19 +268,20 @@ exprt field_sensitivityt::get_fields(
       bool was_l2 = !tmp.get_level_2().empty();
       tmp.remove_level_2();
       tmp.set_expression(index);
+      exprt element = fields_to_expr(get_fields(ns, state, tmp), tmp);
       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);
+    return elements;
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else
-    return ssa_expr;
+    return {ssa_expr};
 }
 
 void field_sensitivityt::field_assignments(
@@ -233,9 +292,13 @@ void field_sensitivityt::field_assignments(
   symex_targett &target,
   bool allow_pointer_unsoundness)
 {
-  const exprt lhs_fs = apply(ns, state, lhs, false);
+  assert(run_apply);
+  bool do_union_bak = do_union;
+  do_union = true;
+  const exprt::operandst lhs_fs = get_fields(ns, state, lhs);
+  do_union = do_union_bak;
 
-  if(lhs != lhs_fs)
+  if(lhs_fs.empty() || lhs != lhs_fs.front())
   {
     bool run_apply_bak = run_apply;
     run_apply = false;
@@ -258,16 +321,16 @@ void field_sensitivityt::field_assignments(
 void field_sensitivityt::field_assignments_rec(
   const namespacet &ns,
   goto_symex_statet &state,
-  const exprt &lhs_fs,
+  const exprt::operandst &lhs_fs,
   const exprt &ssa_rhs,
   symex_targett &target,
   bool allow_pointer_unsoundness)
 {
-  if(is_ssa_expr(lhs_fs))
+  if(lhs_fs.size() == 1 && is_ssa_expr(lhs_fs.front()))
   {
     const ssa_exprt ssa_lhs = state
                                 .assignment(
-                                  to_ssa_expr(lhs_fs),
+                                  to_ssa_expr(lhs_fs.front()),
                                   ssa_rhs,
                                   ns,
                                   true,
@@ -293,15 +356,39 @@ void field_sensitivityt::field_assignments_rec(
 
     PRECONDITION(
       components.empty() ||
-      (lhs_fs.has_operands() && lhs_fs.operands().size() == components.size()));
+      lhs_fs.size() == components.size());
 
-    exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
+    exprt::operandst::const_iterator fs_it = lhs_fs.begin();
     for(const auto &comp : components)
     {
       const exprt member_rhs =
         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.size() == components.size());
+
+    exprt::operandst::const_iterator fs_it = lhs_fs.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;
+
       field_assignments_rec(
         ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
       ++fs_it;
@@ -312,12 +399,12 @@ void field_sensitivityt::field_assignments_rec(
   {
     const std::size_t array_size =
       numeric_cast_v<std::size_t>(to_constant_expr(type->size()));
-    PRECONDITION(lhs_fs.operands().size() == array_size);
+    PRECONDITION(lhs_fs.size() == array_size);
 
     if(array_size > max_field_sensitivity_array_size)
       return;
 
-    exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
+    exprt::operandst::const_iterator fs_it = lhs_fs.begin();
     for(std::size_t i = 0; i < array_size; ++i)
     {
       const exprt index_rhs = simplify_opt(
@@ -330,24 +417,20 @@ void field_sensitivityt::field_assignments_rec(
     }
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
-  else if(lhs_fs.has_operands())
+  else
   {
     PRECONDITION(
       ssa_rhs.has_operands() &&
-      lhs_fs.operands().size() == ssa_rhs.operands().size());
+      lhs_fs.size() == ssa_rhs.operands().size());
 
-    exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
+    exprt::operandst::const_iterator fs_it = lhs_fs.begin();
     for(const exprt &op : ssa_rhs.operands())
     {
       field_assignments_rec(
         ns, state, *fs_it, op, target, allow_pointer_unsoundness);
       ++fs_it;
     }
   }
-  else
-  {
-    UNREACHABLE;
-  }
 }
 
 bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
@@ -366,6 +449,9 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
   }
 #endif
 
+  if(expr.type().id() == ID_union || expr.type().id() == ID_union_tag)
+    return true;
+
   return false;
 }
 

src/goto-symex/field_sensitivity.h

@@ -134,15 +134,15 @@ class field_sensitivityt
     ssa_exprt expr,
     bool write) const;
 
-  /// Compute an expression representing the individual components of a
-  /// field-sensitive SSA representation of \p ssa_expr.
+  /// Compute a sequence holding the individual components of a field-sensitive
+  /// SSA representation of \p ssa_expr.
   /// \param ns: a namespace to resolve type symbols/tag types
   /// \param [in,out] state: symbolic execution state
   /// \param ssa_expr: the expression to evaluate
-  /// \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.
-  exprt get_fields(
+  /// \return Expanded fields or vector containing just \p ssa_expr. For
+  ///   example, for a \p ssa_expr of some struct type, all operands (as SSA
+  ///   expressions)  of what could then be turned into a `struct_exprt`.
+  exprt::operandst get_fields(
     const namespacet &ns,
     goto_symex_statet &state,
     const ssa_exprt &ssa_expr) const;
@@ -159,6 +159,8 @@ class field_sensitivityt
 private:
   /// whether or not to invoke \ref field_sensitivityt::apply
   bool run_apply = true;
+  /// whether or not to expand unions in \ref field_sensitivityt::get_fields
+  bool do_union = false;
 
   const std::size_t max_field_sensitivity_array_size;
 

src/goto-symex/goto_symex_state.cpp

@@ -836,6 +836,7 @@ ssa_exprt goto_symex_statet::declare(ssa_exprt ssa, const namespacet &ns)
   }
 
   // L2 renaming
+  // fix get_fields to obtain union support
   const exprt fields = field_sensitivity.get_fields(ns, *this, ssa);
   fields.visit_pre([this](const exprt &e) {
     if(auto l1_symbol = expr_try_dynamic_cast<symbol_exprt>(e))

src/goto-symex/symex_dead.cpp

@@ -48,7 +48,9 @@ static void remove_l1_object_rec(
     // identifier is still live.
     state.drop_l1_name(l1_identifier);
   }
-  else if(l1_expr.id() == ID_array || l1_expr.id() == ID_struct)
+  else if(
+    l1_expr.id() == ID_array || l1_expr.id() == ID_struct ||
+    l1_expr.id() == ID_union)
   {
     for(const auto &op : l1_expr.operands())
       remove_l1_object_rec(state, op, ns);