Add unit test for expr_initializer

Author: Enrico Steffinlongo

unit/util/expr_initializer.cpp

@@ -0,0 +1,275 @@
+// Author: Diffblue Ltd.
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/expr_initializer.h>
+#include <util/namespace.h>
+#include <util/std_code.h>
+#include <util/symbol_table.h>
+
+#include <testing-utils/use_catch.h>
+
+#include "c_types.h"
+
+/// Helper struct to hold useful test components.
+struct expr_initializer_test_environmentt
+{
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  source_locationt loc{};
+
+  static expr_initializer_test_environmentt make()
+  {
+    return {};
+  }
+
+private:
+  expr_initializer_test_environmentt() = default;
+};
+
+/// Helper function to create and populate a c_enum_typet type.
+static c_enum_typet make_c_enum_type(
+  const unsignedbv_typet &underlying_type,
+  unsigned int value_count)
+{
+  c_enum_typet enum_type{underlying_type};
+
+  auto &members = enum_type.members();
+  members.reserve(value_count);
+
+  for(unsigned int i = 0; i < value_count; ++i)
+  {
+    c_enum_typet::c_enum_membert member;
+    member.set_identifier("V" + std::to_string(i));
+    member.set_base_name("V" + std::to_string(i));
+    member.set_value(integer2bvrep(i, underlying_type.get_width()));
+    members.push_back(member);
+  }
+  return enum_type;
+}
+
+/// Create a type symbol, a type_tag and a symbol for the tag and populate with
+/// them the symbol_table in the environment.
+static symbolt create_tag_populate_env(
+  const typet &type,
+  expr_initializer_test_environmentt &env)
+{
+  const type_symbolt symbol{"my_type_symbol", type, ID_C};
+  symbolt tag_symbol = [&]() {
+    if(can_cast_type<c_enum_typet>(type))
+    {
+      const c_enum_tag_typet c_enum_tag_type{symbol.name};
+      return symbolt{"my_type_tag_symbol", c_enum_tag_type, ID_C};
+    }
+    else if(can_cast_type<struct_typet>(type))
+    {
+      const struct_tag_typet struct_tag_type{symbol.name};
+      return symbolt{"my_type_tag_symbol", struct_tag_type, ID_C};
+    }
+    else if(can_cast_type<union_typet>(type))
+    {
+      const union_tag_typet union_tag_type{symbol.name};
+      return symbolt{"my_type_tag_symbol", union_tag_type, ID_C};
+    }
+    UNREACHABLE;
+  }();
+  env.symbol_table.insert(symbol);
+  env.symbol_table.insert(tag_symbol);
+  return tag_symbol;
+}
+
+TEST_CASE("nondet_initializer boolean", "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  typet input = bool_typet{};
+  const auto result = nondet_initializer(input, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  const auto expected = side_effect_expr_nondett{bool_typet{}, test.loc};
+  REQUIRE(result.value() == expected);
+}
+
+TEST_CASE("nondet_initializer signed_bv", "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  typet input = signedbv_typet{8};
+  const auto result = nondet_initializer(input, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  const auto expected = side_effect_expr_nondett{signedbv_typet{8}, test.loc};
+  REQUIRE(result.value() == expected);
+}
+
+TEST_CASE("nondet_initializer c_enum", "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  const unsignedbv_typet enum_underlying_type{8};
+  const auto enum_type = make_c_enum_type(enum_underlying_type, 3);
+  const auto result = nondet_initializer(enum_type, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  const auto expected = side_effect_expr_nondett{enum_type, test.loc};
+  REQUIRE(result.value() == expected);
+
+  // Repeat with the c_enum_tag_typet instead of the c_enum_typet it points to
+  const symbolt symbol = create_tag_populate_env(enum_type, test);
+  const auto tag_result = nondet_initializer(symbol.type, test.loc, test.ns);
+  REQUIRE(tag_result.has_value());
+  const auto expected_tag = side_effect_expr_nondett{symbol.type, test.loc};
+  REQUIRE(tag_result.value() == expected_tag);
+}
+
+TEST_CASE(
+  "nondet_initializer simple array_type",
+  "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  typet inner_type = signedbv_typet{8};
+  const std::size_t elem_count = 3;
+  typet array_type =
+    array_typet{inner_type, from_integer(elem_count, signedbv_typet{8})};
+  const auto result = nondet_initializer(array_type, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  std::vector<exprt> array_values{
+    elem_count, side_effect_expr_nondett{signedbv_typet{8}, test.loc}};
+  const auto expected = array_exprt{
+    array_values,
+    array_typet{
+      signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}};
+  REQUIRE(result.value() == expected);
+}
+
+TEST_CASE(
+  "nondet_initializer on array_type with nondet size",
+  "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  typet inner_type = signedbv_typet{8};
+  typet array_type = array_typet{
+    inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}};
+  const auto result = nondet_initializer(array_type, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  const auto expected = side_effect_expr_nondett{
+    array_typet{
+      inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}},
+    test.loc};
+  REQUIRE(result.value() == expected);
+}
+
+TEST_CASE(
+  "nondet_initializer double array_type",
+  "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  typet inner_type = signedbv_typet{8};
+  const std::size_t elem_count = 3;
+  typet inner_array_type =
+    array_typet{inner_type, from_integer(elem_count, signedbv_typet{8})};
+  typet array_type =
+    array_typet{inner_array_type, from_integer(elem_count, signedbv_typet{8})};
+  const auto result = nondet_initializer(array_type, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  std::vector<exprt> inner_array_values{
+    elem_count, side_effect_expr_nondett{signedbv_typet{8}, test.loc}};
+  const auto inner_expected = array_exprt{
+    inner_array_values,
+    array_typet{
+      signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}};
+  std::vector<exprt> array_values{elem_count, inner_expected};
+  const auto expected = array_exprt{
+    array_values,
+    array_typet{
+      array_typet{
+        signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})},
+      from_integer(elem_count, signedbv_typet{8})}};
+  REQUIRE(result.value() == expected);
+}
+
+TEST_CASE(
+  "nondet_initializer nested struct type",
+  "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  const struct_union_typet::componentst inner_struct_components{
+    {"foo", signedbv_typet{32}}, {"bar", unsignedbv_typet{16}}};
+  const struct_typet inner_struct_type{inner_struct_components};
+  const struct_union_typet::componentst struct_components{
+    {"fizz", bool_typet{}}, {"bar", inner_struct_type}};
+  const struct_typet struct_type{struct_components};
+  const auto result = nondet_initializer(struct_type, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  const exprt::operandst expected_inner_struct_operands{
+    side_effect_expr_nondett{signedbv_typet{32}, test.loc},
+    side_effect_expr_nondett{unsignedbv_typet{16}, test.loc}};
+  const struct_exprt expected_inner_struct_expr{
+    expected_inner_struct_operands, inner_struct_type};
+  const exprt::operandst expected_struct_operands{
+    side_effect_expr_nondett{bool_typet{}, test.loc},
+    expected_inner_struct_expr};
+  const struct_exprt expected_struct_expr{
+    expected_struct_operands, struct_type};
+  REQUIRE(result.value() == expected_struct_expr);
+
+  const symbolt inner_struct_tag_symbol =
+    create_tag_populate_env(inner_struct_type, test);
+  const auto tag_result =
+    nondet_initializer(inner_struct_tag_symbol.type, test.loc, test.ns);
+  REQUIRE(tag_result.has_value());
+  const struct_exprt expected_inner_struct_tag_expr{
+    expected_inner_struct_operands, inner_struct_tag_symbol.type};
+  REQUIRE(tag_result.value() == expected_inner_struct_tag_expr);
+}
+
+TEST_CASE("nondet_initializer union type", "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  const struct_union_typet::componentst inner_struct_components{
+    {"foo", signedbv_typet{32}}, {"bar", unsignedbv_typet{16}}};
+  const struct_typet inner_struct_type{inner_struct_components};
+  const struct_union_typet::componentst union_components{
+    {"foo", signedbv_typet{256}},
+    {"bar", unsignedbv_typet{16}},
+    {"fizz", bool_typet{}},
+    {"array",
+     array_typet{signedbv_typet{8}, from_integer(8, signedbv_typet{8})}},
+    {"struct", inner_struct_type}};
+  const union_typet union_type{union_components};
+  const auto result = nondet_initializer(union_type, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  const union_exprt expected_union{
+    "foo", side_effect_expr_nondett{signedbv_typet{256}, test.loc}, union_type};
+  REQUIRE(result.value() == expected_union);
+
+  const symbolt union_tag_symbol = create_tag_populate_env(union_type, test);
+  const auto tag_result =
+    nondet_initializer(union_tag_symbol.type, test.loc, test.ns);
+  REQUIRE(tag_result.has_value());
+  const union_exprt expected_union_tag{
+    "foo",
+    side_effect_expr_nondett{signedbv_typet{256}, test.loc},
+    union_tag_symbol.type};
+  REQUIRE(tag_result.value() == expected_union_tag);
+}
+
+TEST_CASE(
+  "nondet_initializer union type with nondet sized array (fails)",
+  "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  const struct_union_typet::componentst union_components{
+    {"foo", signedbv_typet{256}},
+    {"array",
+     array_typet{
+       signedbv_typet{8},
+       side_effect_expr_nondett{signedbv_typet{8}, test.loc}}}};
+  const union_typet union_type{union_components};
+  const auto result = nondet_initializer(union_type, test.loc, test.ns);
+  REQUIRE(!result.has_value());
+}
+
+TEST_CASE("nondet_initializer string type", "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  const string_typet string_type{};
+  const auto result = nondet_initializer(string_type, test.loc, test.ns);
+  REQUIRE(result.has_value());
+  const side_effect_expr_nondett expected_string{string_typet{}, test.loc};
+  REQUIRE(result.value() == expected_string);
+}