Merge pull request #4063 from tautschnig/byte-op-2

byte_extract lowering: ensure type consistency [blocks: #2068]

Author: tautschnig

regression/cbmc/Pointer_byte_extract3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc/Pointer_byte_extract7/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --big-endian
 ^EXIT=0$

regression/cbmc/equality_through_union1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc/equality_through_union2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc/equality_through_union3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc/gcc_vector1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc/trace_address_arithmetic1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --trace
 ^EXIT=10$

regression/cbmc/union11/union_list.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 union_list.c
 
 ^EXIT=0$

regression/cbmc/union8/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

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

@@ -104,8 +104,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},
@@ -114,8 +114,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),
@@ -193,10 +193,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);
           }
         }
       }