Fixes to the byte_operator lowering unit test

Let's only test byte extracts within bounds for now (there is ample work to be
done to get those right), but make sure there is possible combination for each
pair of types. Endianness needs to be taken into account when constructing the
expected value. Disable any non-POD tests as they all need more work.

Author: tautschnig

unit/solvers/lowering/byte_operators.cpp

@@ -65,96 +65,104 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
   GIVEN("A collection of types")
   {
     unsignedbv_typet u8(8);
+    signedbv_typet s8(8);
+    unsignedbv_typet u16(16);
+    signedbv_typet s16(16);
     unsignedbv_typet u32(32);
+    signedbv_typet s32(32);
     unsignedbv_typet u64(64);
+    signedbv_typet s64(64);
 
     constant_exprt size = from_integer(8, size_type());
 
     std::vector<typet> types = {
-      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},
                     {"compX", c_bit_field_typet(u8, 4)},
                     {"pad", c_bit_field_typet(u8, 4)},
                     {"comp2", u8}}),
 #endif
-      union_typet({{"compA", u32}, {"compB", u64}}),
-      c_enum_typet(unsignedbv_typet(16)),
-      array_typet(u8, size),
-      array_typet(u64, size),
+      // union_typet({{"compA", u32}, {"compB", u64}}),
+      // c_enum_typet(u16),
+      // c_enum_typet(unsignedbv_typet(128)),
+      // array_typet(u8, size),
+      // array_typet(s32, size),
+      // array_typet(u64, size),
       unsignedbv_typet(24),
+      unsignedbv_typet(128),
+      signedbv_typet(24),
       signedbv_typet(128),
-      ieee_float_spect::single_precision().to_type(),
-      pointer_typet(u64, 64),
-      vector_typet(u8, size),
-      vector_typet(u64, size),
-      complex_typet(u32)
+      // ieee_float_spect::single_precision().to_type(),
+      // pointer_typet(u64, 64),
+      // vector_typet(u8, size),
+      // vector_typet(u64, size),
+      // complex_typet(s16),
+      // complex_typet(u64)
     };
 
     simplify_exprt simp(ns);
 
     THEN("byte_extract lowering yields the expected value")
     {
-      for(const auto &t1 : types)
+      for(const auto endianness :
+          {ID_byte_extract_little_endian, ID_byte_extract_big_endian})
       {
-        std::ostringstream oss;
-        for(int i = 0; i < 64; ++i)
-          oss << integer2binary(i, 8);
-
-        const auto type_bits = pointer_offset_bits(t1, ns);
-        REQUIRE(type_bits);
-        const auto type_bits_int = numeric_cast_v<std::size_t>(*type_bits);
-        REQUIRE(type_bits_int <= oss.str().size());
-        const exprt s =
-          simp.bits2expr(oss.str().substr(0, type_bits_int), t1, true);
-        REQUIRE(s.is_not_nil());
-
-        for(const auto &t2 : types)
+        for(const auto &t1 : types)
         {
-          oss.str("");
-          for(int i = 2; i < 66; ++i)
+          std::ostringstream oss;
+          for(int i = 0; i < 64; ++i)
             oss << integer2binary(i, 8);
 
-          const auto type_bits_2 = pointer_offset_bits(t2, ns);
-          REQUIRE(type_bits_2);
-          const auto type_bits_2_int =
-            numeric_cast_v<std::size_t>(*type_bits_2);
-          REQUIRE(type_bits_2_int <= oss.str().size());
-          const exprt r =
-            simp.bits2expr(oss.str().substr(0, type_bits_2_int), t2, true);
-          REQUIRE(r.is_not_nil());
-
-          const byte_extract_exprt be1(
-            ID_byte_extract_little_endian,
-            s,
-            from_integer(2, index_type()),
-            t2);
-
-          const exprt lower_be1 = lower_byte_extract(be1, ns);
-          const exprt lower_be1_s = simplify_expr(lower_be1, ns);
-
-          // TODO: does not currently hold
-          // REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian));
-          REQUIRE(lower_be1.type() == be1.type());
-          // TODO: does not currently hold
-          // REQUIRE(lower_be1 == r);
-          // TODO: does not currently hold
-          // REQUIRE(lower_be1_s == r);
-
-          const byte_extract_exprt be2(
-            ID_byte_extract_big_endian, s, from_integer(2, index_type()), t2);
-
-          const exprt lower_be2 = lower_byte_extract(be2, ns);
-          const exprt lower_be2_s = simplify_expr(lower_be2, ns);
-
-          // TODO: does not currently hold
-          REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian));
-          REQUIRE(lower_be2.type() == be2.type());
-          // TODO: does not currently hold
-          // REQUIRE(lower_be2 == r);
-          // TODO: does not currently hold
-          // REQUIRE(lower_be2_s == r);
+          const auto type_bits = pointer_offset_bits(t1, ns);
+          REQUIRE(type_bits);
+          const auto type_bits_int = numeric_cast_v<std::size_t>(*type_bits);
+          REQUIRE(type_bits_int <= oss.str().size());
+          const exprt s = simp.bits2expr(
+            oss.str().substr(0, type_bits_int),
+            t1,
+            endianness == ID_byte_extract_little_endian);
+          REQUIRE(s.is_not_nil());
+
+          for(const auto &t2 : types)
+          {
+            oss.str("");
+            for(int i = 2; i < 64; ++i)
+              oss << integer2binary(i, 8);
+
+            const auto type_bits_2 = pointer_offset_bits(t2, ns);
+            REQUIRE(type_bits_2);
+
+            // for now only extract within bounds
+            if(*type_bits_2 + 16 > *type_bits)
+              continue;
+
+            const auto type_bits_2_int =
+              numeric_cast_v<std::size_t>(*type_bits_2);
+            REQUIRE(type_bits_2_int <= oss.str().size());
+            const exprt r = simp.bits2expr(
+              oss.str().substr(0, type_bits_2_int),
+              t2,
+              endianness == ID_byte_extract_little_endian);
+            REQUIRE(r.is_not_nil());
+
+            const byte_extract_exprt be(
+              endianness, s, from_integer(2, index_type()), t2);
+
+            const exprt lower_be = lower_byte_extract(be, ns);
+            const exprt lower_be_s = simplify_expr(lower_be, ns);
+
+            // TODO: does not currently hold
+            // 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);
+          }
         }
       }
     }
@@ -208,13 +216,19 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
   GIVEN("A collection of types")
   {
     unsignedbv_typet u8(8);
+    signedbv_typet s8(8);
+    unsignedbv_typet u16(16);
+    signedbv_typet s16(16);
     unsignedbv_typet u32(32);
+    signedbv_typet s32(32);
     unsignedbv_typet u64(64);
+    signedbv_typet s64(64);
 
     constant_exprt size = from_integer(8, size_type());
 
     std::vector<typet> types = {
     // TODO: only arrays and scalars
+    // struct_typet({{"comp1", u16}, {"comp2", u16}}),
     // struct_typet({{"comp1", u32}, {"comp2", u64}}),
 #if 0
       // not currently handled: components not byte aligned
@@ -225,83 +239,88 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
 #endif
       // TODO: only arrays and scalars
       // union_typet({{"compA", u32}, {"compB", u64}}),
-      // c_enum_typet(unsignedbv_typet(16)),
-      array_typet(u8, size),
-      array_typet(u64, size),
+      // c_enum_typet(u16),
+      // c_enum_typet(unsignedbv_typet(128)),
+      // array_typet(u8, size),
+      // array_typet(s32, size),
+      // array_typet(u64, size),
       unsignedbv_typet(24),
+      unsignedbv_typet(128),
+      signedbv_typet(24),
       signedbv_typet(128),
-      ieee_float_spect::single_precision().to_type(),
-      pointer_typet(u64, 64),
+      // ieee_float_spect::single_precision().to_type(),
+      // pointer_typet(u64, 64),
       // TODO: only arrays and scalars
       // vector_typet(u8, size),
       // vector_typet(u64, size),
-      // complex_typet(u32)
+      // complex_typet(s16),
+      // complex_typet(u64)
     };
 
     simplify_exprt simp(ns);
 
     THEN("byte_update lowering yields the expected value")
     {
-      for(const auto &t1 : types)
+      for(const auto endianness :
+          {ID_byte_update_little_endian, ID_byte_update_big_endian})
       {
-        std::ostringstream oss;
-        for(int i = 0; i < 64; ++i)
-          oss << integer2binary(i, 8);
-
-        const auto type_bits = pointer_offset_bits(t1, ns);
-        REQUIRE(type_bits);
-        const auto type_bits_int = numeric_cast_v<std::size_t>(*type_bits);
-        REQUIRE(type_bits_int <= oss.str().size());
-        const exprt s =
-          simp.bits2expr(oss.str().substr(0, type_bits_int), t1, true);
-        REQUIRE(s.is_not_nil());
-
-        for(const auto &t2 : types)
+        for(const auto &t1 : types)
         {
-          oss.str("");
-          for(int i = 64; i < 128; ++i)
+          std::ostringstream oss;
+          for(int i = 0; i < 64; ++i)
             oss << integer2binary(i, 8);
 
-          const auto type_bits_2 = pointer_offset_bits(t2, ns);
-          REQUIRE(type_bits_2);
-          const auto type_bits_2_int =
-            numeric_cast_v<std::size_t>(*type_bits_2);
-          REQUIRE(type_bits_2_int <= oss.str().size());
-          const exprt u =
-            simp.bits2expr(oss.str().substr(0, type_bits_2_int), t2, true);
-          REQUIRE(u.is_not_nil());
-
-          // TODO: currently required
-          if(type_bits < type_bits_2)
-            continue;
-
-          const byte_update_exprt bu1(
-            ID_byte_update_little_endian, s, from_integer(2, index_type()), u);
-
-          const exprt lower_bu1 = lower_byte_operators(bu1, ns);
-          const exprt lower_bu1_s = simplify_expr(lower_bu1, ns);
-
-          REQUIRE(!has_subexpr(lower_bu1, ID_byte_update_little_endian));
-          REQUIRE(!has_subexpr(lower_bu1, ID_byte_extract_little_endian));
-          REQUIRE(lower_bu1.type() == bu1.type());
-          // TODO: does not currently hold
-          // REQUIRE(lower_bu1 == u);
-          // TODO: does not currently hold
-          // REQUIRE(lower_bu1_s == u);
-
-          const byte_update_exprt bu2(
-            ID_byte_update_big_endian, s, from_integer(2, index_type()), u);
-
-          const exprt lower_bu2 = lower_byte_operators(bu2, ns);
-          const exprt lower_bu2_s = simplify_expr(lower_bu2, ns);
-
-          REQUIRE(!has_subexpr(lower_bu2, ID_byte_update_big_endian));
-          REQUIRE(!has_subexpr(lower_bu2, ID_byte_extract_big_endian));
-          REQUIRE(lower_bu2.type() == bu2.type());
-          // TODO: does not currently hold
-          // REQUIRE(lower_bu2 == u);
-          // TODO: does not currently hold
-          // REQUIRE(lower_bu2_s == u);
+          const auto type_bits = pointer_offset_bits(t1, ns);
+          REQUIRE(type_bits);
+          const auto type_bits_int = numeric_cast_v<std::size_t>(*type_bits);
+          REQUIRE(type_bits_int <= oss.str().size());
+          std::string s_string = oss.str().substr(0, type_bits_int);
+          const exprt s = simp.bits2expr(
+            s_string, t1, endianness == ID_byte_update_little_endian);
+          REQUIRE(s.is_not_nil());
+
+          for(const auto &t2 : types)
+          {
+            oss.str("");
+            for(int i = 64; i < 128; ++i)
+              oss << integer2binary(i, 8);
+
+            const auto type_bits_2 = pointer_offset_bits(t2, ns);
+            REQUIRE(type_bits_2);
+
+            // for now only update within bounds
+            if(*type_bits_2 + 16 > *type_bits)
+              continue;
+
+            const auto type_bits_2_int =
+              numeric_cast_v<std::size_t>(*type_bits_2);
+            REQUIRE(type_bits_2_int <= oss.str().size());
+            std::string u_string = oss.str().substr(0, type_bits_2_int);
+            const exprt u = simp.bits2expr(
+              u_string, t2, endianness == ID_byte_update_little_endian);
+            REQUIRE(u.is_not_nil());
+
+            const exprt r = simp.bits2expr(
+              s_string.replace(16, u_string.size(), u_string),
+              t1,
+              endianness == ID_byte_update_little_endian);
+            REQUIRE(r.is_not_nil());
+
+            const byte_update_exprt bu(
+              endianness, s, from_integer(2, index_type()), u);
+
+            const exprt lower_bu = lower_byte_operators(bu, ns);
+            const exprt lower_bu_s = simplify_expr(lower_bu, ns);
+
+            REQUIRE(!has_subexpr(lower_bu, endianness));
+            REQUIRE(!has_subexpr(lower_bu, ID_byte_extract_big_endian));
+            REQUIRE(!has_subexpr(lower_bu, ID_byte_extract_little_endian));
+            REQUIRE(lower_bu.type() == bu.type());
+            // TODO: does not currently hold
+            // REQUIRE(lower_bu == r);
+            // TODO: does not currently hold
+            // REQUIRE(lower_bu_s == r);
+          }
         }
       }
     }