Make the simplifier preserve syntactically equal types

base_type_eq guarantees semantic equality, but the resulting expression should
always have exactly the same type.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -1657,6 +1657,9 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     if(base_type_eq(expr.type(), expr.op().op2().type(), ns))
     {
       exprt tmp=expr.op().op2();
+      // types are known to be semantically equivalent (via base_type_eq), make
+      // sure they are syntactically the same
+      tmp.type() = expr.type();
       expr.swap(tmp);
 
       return false;
@@ -1687,6 +1690,9 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     if(base_type_eq(expr.type(), expr.op().type(), ns))
     {
       exprt tmp = expr.op();
+      // types are known to be semantically equivalent (via base_type_eq), make
+      // sure they are syntactically the same
+      tmp.type() = expr.type();
       expr.swap(tmp);
 
       return false;

src/util/simplify_expr_int.cpp

@@ -955,8 +955,13 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
   // { x } = x
   if(expr.operands().size()==1)
   {
-    exprt tmp;
-    tmp.swap(expr.op0());
+    exprt tmp = expr.op0();
+    if(expr.type() != tmp.type())
+    {
+      tmp.make_typecast(expr.type());
+      simplify_node(tmp);
+    }
+
     expr.swap(tmp);
     result=false;
   }

src/util/simplify_expr_struct.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include "arith_tools.h"
 #include "base_type.h"
 #include "byte_operators.h"
+#include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "std_expr.h"
@@ -134,8 +135,14 @@ bool simplify_exprt::simplify_member(exprt &expr)
       if(struct_type.has_component(component_name))
       {
         std::size_t number=struct_type.component_number(component_name);
-        exprt tmp;
-        tmp.swap(op.operands()[number]);
+        exprt tmp = op.operands()[number];
+        if(tmp.type() != expr.type())
+        {
+          DATA_INVARIANT(
+            base_type_eq(tmp.type(), expr.type(), ns),
+            "member expression type must match component type");
+          tmp.type() = expr.type();
+        }
         expr.swap(tmp);
         return false;
       }