Unit test of byte operator lowering

Author: tautschnig

unit/Makefile

@@ -31,6 +31,7 @@ SRC += analyses/ai/ai.cpp \
        path_strategies.cpp \
        pointer-analysis/value_set.cpp \
        solvers/floatbv/float_utils.cpp \
+       solvers/lowering/byte_operators.cpp \
        solvers/miniBDD/miniBDD.cpp \
        solvers/refinement/array_pool/array_pool.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \

unit/solvers/lowering/byte_operators.cpp

@@ -0,0 +1,259 @@
+/*******************************************************************\
+
+ Module: Unit tests for byte_extract/byte_update lowering
+
+ Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <solvers/lowering/expr_lowering.h>
+
+#include <util/arith_tools.h>
+#include <util/byte_operators.h>
+#include <util/c_types.h>
+#include <util/expr_util.h>
+#include <util/namespace.h>
+#include <util/simplify_expr.h>
+#include <util/std_types.h>
+#include <util/symbol_table.h>
+
+SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
+{
+  // this test does require a proper architecture to be set so that byte extract
+  // uses adequate endianness
+  cmdlinet cmdline;
+  config.set(cmdline);
+
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  GIVEN("A byte_extract over a POD")
+  {
+    const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32));
+    const byte_extract_exprt be1(
+      ID_byte_extract_little_endian,
+      deadbeef,
+      from_integer(1, index_type()),
+      signedbv_typet(8));
+
+    THEN("byte_extract lowering yields the expected value")
+    {
+      const exprt lower_be1 = lower_byte_extract(be1, ns);
+      const exprt lower_be1_s = simplify_expr(lower_be1, ns);
+
+      REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian));
+      REQUIRE(lower_be1.type() == be1.type());
+      REQUIRE(lower_be1_s == from_integer(0xbe, signedbv_typet(8)));
+
+      byte_extract_exprt be2 = be1;
+      be2.id(ID_byte_extract_big_endian);
+      const exprt lower_be2 = lower_byte_extract(be2, ns);
+      const exprt lower_be2_s = simplify_expr(lower_be2, ns);
+
+      REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian));
+      REQUIRE(lower_be2.type() == be2.type());
+      REQUIRE(lower_be2_s == from_integer(0xad, signedbv_typet(8)));
+    }
+  }
+
+  GIVEN("A collection of types")
+  {
+    unsignedbv_typet u8(8);
+    unsignedbv_typet u32(32);
+    unsignedbv_typet u64(64);
+
+    exprt size = from_integer(8, size_type());
+
+    std::vector<typet> types = {
+      struct_typet({ {"comp1", u32}, {"comp2", u64} }),
+      struct_typet({ {"comp1", u32}, {"compX", c_bit_field_typet(u8, 4)}, {"pad", c_bit_field_typet(u8, 4)}, {"comp2", u8} }),
+      union_typet({ {"compA", u32}, {"compB", u64} }),
+      c_enum_typet(unsignedbv_typet(16)),
+      array_typet(u8, size),
+      array_typet(u64, size),
+      unsignedbv_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)
+    };
+
+    simplify_exprt simp(ns);
+
+    THEN("byte_extract lowering yields the expected value")
+    {
+      for(const auto &t1 : types)
+      {
+        std::ostringstream oss;
+        for(int i = 0; i < 64; ++i)
+          oss << integer2binary(i, 8);
+        const exprt s = simp.bits2expr(oss.str(), t1, true);
+        REQUIRE(s.is_not_nil());
+
+        for(const auto &t2 : types)
+        {
+          oss.str("");
+          for(int i = 2; i < 66; ++i)
+            oss << integer2binary(i, 8);
+          const exprt r = simp.bits2expr(oss.str(), 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);
+
+          REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian));
+          REQUIRE(lower_be1.type() == be1.type());
+          REQUIRE(lower_be1 == r);
+          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);
+
+          REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian));
+          REQUIRE(lower_be2.type() == be2.type());
+          REQUIRE(lower_be2 == r);
+          REQUIRE(lower_be2_s == r);
+        }
+      }
+    }
+  }
+}
+
+SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
+{
+  // this test does require a proper architecture to be set so that byte extract
+  // uses adequate endianness
+  cmdlinet cmdline;
+  config.set(cmdline);
+
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  GIVEN("A byte_update of a POD")
+  {
+    const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32));
+    const byte_update_exprt bu1(
+      ID_byte_update_little_endian,
+      deadbeef,
+      from_integer(1, index_type()),
+      from_integer(0x42, unsignedbv_typet(8)));
+
+    THEN("byte_update lowering yields the expected value")
+    {
+      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_extract_little_endian));
+      REQUIRE(!has_subexpr(lower_bu1, ID_byte_update_little_endian));
+      REQUIRE(lower_bu1.type() == bu1.type());
+      REQUIRE(lower_bu1_s == from_integer(0xdead42ef, unsignedbv_typet(32)));
+
+#if 0
+      // this is currently broken, #2058 will fix it
+      byte_update_exprt bu2 = bu1;
+      bu2.id(ID_byte_update_big_endian);
+      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_extract_big_endian));
+      REQUIRE(!has_subexpr(lower_bu2, ID_byte_update_big_endian));
+      REQUIRE(lower_bu2.type() == bu2.type());
+      REQUIRE(lower_bu2_s == from_integer(0xde42beef, unsignedbv_typet(32)));
+#endif
+    }
+  }
+
+  GIVEN("A collection of types")
+  {
+    unsignedbv_typet u8(8);
+    unsignedbv_typet u32(32);
+    unsignedbv_typet u64(64);
+
+    exprt size = from_integer(8, size_type());
+
+    std::vector<typet> types = {
+      struct_typet({ {"comp1", u32}, {"comp2", u64} }),
+      struct_typet({ {"comp1", u32}, {"compX", c_bit_field_typet(u8, 4)}, {"pad", c_bit_field_typet(u8, 4)}, {"comp2", u8} }),
+      union_typet({ {"compA", u32}, {"compB", u64} }),
+      c_enum_typet(unsignedbv_typet(16)),
+      array_typet(u8, size),
+      array_typet(u64, size),
+      unsignedbv_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)
+    };
+
+    simplify_exprt simp(ns);
+
+    THEN("byte_update lowering yields the expected value")
+    {
+      for(const auto &t1 : types)
+      {
+        std::ostringstream oss;
+        for(int i = 0; i < 64; ++i)
+          oss << integer2binary(i, 8);
+        const exprt s = simp.bits2expr(oss.str(), t1, true);
+        REQUIRE(s.is_not_nil());
+
+        for(const auto &t2 : types)
+        {
+          oss.str("");
+          for(int i = 65; i < 128; ++i)
+            oss << integer2binary(i, 8);
+          const exprt u = simp.bits2expr(oss.str(), t2, true);
+          REQUIRE(u.is_not_nil());
+
+          const byte_update_exprt bu1(
+            ID_byte_update_little_endian,
+            s,
+            from_integer(2, index_type()),
+            u);
+
+          const exprt lower_bu1 = lower_byte_extract(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());
+          REQUIRE(lower_bu1 == u);
+          REQUIRE(lower_bu1_s == u);
+
+          const byte_extract_exprt bu2(
+            ID_byte_update_big_endian,
+            s,
+            from_integer(2, index_type()),
+            u);
+
+          const exprt lower_bu2 = lower_byte_extract(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());
+          REQUIRE(lower_bu2 == u);
+          REQUIRE(lower_bu2_s == u);
+        }
+      }
+    }
+  }
+}