Merge pull request #8724 from tautschnig/simplify-with-single-member

Simplify WITH expression over structs with a single component

Author: tautschnig

regression/cbmc/havoc_slice/functional_slice_bytes.desc

@@ -1,10 +1,12 @@
 CORE
 functional.c
 -DN=4 -DSLICE_BYTES --program-only
+WITH \[.*i!0@1#2:=\{ \.coeffs=byte_extract
 ^EXIT=0$
 ^SIGNAL=0$
 --
 byte_update
+WITH \[.*i!0@1#2:=\{ \{ \.coeffs=\{
 --
 We want these tests not to produce any byte_update expressions, but instead want
 updates at specific array indices.

src/util/simplify_expr.cpp

@@ -1470,14 +1470,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_with(const with_exprt &expr)
     expr.old().type().id() == ID_struct ||
     expr.old().type().id() == ID_struct_tag)
   {
+    const struct_typet &old_type_followed =
+      expr.old().type().id() == ID_struct_tag
+        ? ns.follow_tag(to_struct_tag_type(expr.old().type()))
+        : to_struct_type(expr.old().type());
+    const irep_idt &component_name = expr.where().get(ID_component_name);
+
     if(expr.old().id() == ID_struct || expr.old().is_constant())
     {
-      const irep_idt &component_name = expr.where().get(ID_component_name);
-
-      const struct_typet &old_type_followed =
-        expr.old().type().id() == ID_struct_tag
-          ? ns.follow_tag(to_struct_tag_type(expr.old().type()))
-          : to_struct_type(expr.old().type());
       if(!old_type_followed.has_component(component_name))
         return unchanged(expr);
 
@@ -1490,6 +1490,12 @@ simplify_exprt::resultt<> simplify_exprt::simplify_with(const with_exprt &expr)
       result.operands()[number] = expr.new_value();
       return result;
     }
+    else if(
+      old_type_followed.components().size() == 1 &&
+      old_type_followed.has_component(component_name))
+    {
+      return struct_exprt{{expr.new_value()}, expr.type()};
+    }
   }
   else if(
     expr.old().type().id() == ID_array || expr.old().type().id() == ID_vector)