byte_extract lowering: ensure type consistency

Make sure we construct concatenations that are type consistent.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -343,8 +343,10 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     return simplify_expr(typecast_exprt(op.front(), src.type()), ns);
   else // width_bytes>=2
   {
-    concatenation_exprt concatenation(std::move(op), src.type());
-    return simplify_expr(concatenation, ns);
+    concatenation_exprt concatenation(
+      std::move(op), bitvector_typet(subtype.id(), width_bytes * 8));
+    return simplify_expr(
+      typecast_exprt(std::move(concatenation), src.type()), ns);
   }
 }
 

unit/solvers/lowering/byte_operators.cpp

@@ -76,8 +76,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     constant_exprt size = from_integer(8, size_type());
 
     std::vector<typet> types = {
-    // struct_typet({{"comp1", u16}, {"comp2", u16}}),
-    // struct_typet({{"comp1", u32}, {"comp2", u64}}),
+      struct_typet({{"comp1", u16}, {"comp2", u16}}),
+      struct_typet({{"comp1", u32}, {"comp2", u64}}),
 #if 0
       // not currently handled: components not byte aligned
       struct_typet({{"comp1", u32},
@@ -86,8 +86,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
                     {"comp2", u8}}),
 #endif
       // union_typet({{"compA", u32}, {"compB", u64}}),
-      // c_enum_typet(u16),
-      // c_enum_typet(unsignedbv_typet(128)),
+      c_enum_typet(u16),
+      c_enum_typet(unsignedbv_typet(128)),
       // array_typet(u8, size),
       // array_typet(s32, size),
       // array_typet(u64, size),
@@ -166,10 +166,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
             // REQUIRE(!has_subexpr(lower_be, ID_byte_extract_little_endian));
             // REQUIRE(!has_subexpr(lower_be, ID_byte_extract_big_endian));
             REQUIRE(lower_be.type() == be.type());
-            // TODO: does not currently hold
-            // REQUIRE(lower_be == r);
-            // TODO: does not currently hold
-            // REQUIRE(lower_be_s == r);
+            REQUIRE(lower_be == r);
+            REQUIRE(lower_be_s == r);
           }
         }
       }