Unit test of byte operator lowering

Author: tautschnig

unit/Makefile

@@ -30,6 +30,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,111 @@
+/*******************************************************************\
+
+ 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)));
+    }
+  }
+
+  std::vector<typet> types = {
+    struct_typet().components() = { {"comp1", typet()}, {"comp2", typet()} },
+    struct_typet().components() = { {"comp1", typet()}, {"compX", c_bit_field_typet(subtype, width)}, {"comp2", typet()} },
+    union_typet().components() = { {"compA", typet()}, {"compB", typet()} },
+    c_enum_typet(unsignedbv_typet(16)),
+    array_typet(unsignedbv_typet(8), size),
+    array_typet(unsignedbv_typet(64), size),
+    unsignedbv_typet(24),
+    signedbv_typet(128),
+    floatbv_typet(),
+    pointer_typet(subtype, width),
+    vector_typet(unsignedbv_typet(8), size),
+    vector_typet(unsignedbv_typet(64), size),
+    complex_typet(subtype)
+  }
+}
+
+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
+    }
+  }
+}