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,126 @@
+/*******************************************************************\
+
+ 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]")
+{
+  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)));
+    }
+  }
+
+  unsignedbv_typet u8(8);
+  unsignedbv_typet u32(32);
+  unsignedbv_typet u64(64);
+
+  exprt size = from_integer(8, u32);
+
+  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);
+  for(const auto &t1 : types)
+  {
+    exprt s = simp.bits2expr(t1);
+    for(const auto &t2 : types)
+    {
+    }
+  }
+}
+
+SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
+{
+  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
+    }
+  }
+}