/*******************************************************************\

Module: Unit tests for value_sett

Author: Diffblue Ltd.

\*******************************************************************/

/// \file
/// Unit tests for value_sett

#include <util/arith_tools.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/symbol_table.h>

#include <pointer-analysis/value_set.h>
#include <testing-utils/use_catch.h>

#include <climits>

static bool object_descriptor_matches(
  const exprt &descriptor_expr, const exprt &target)
{
  if(descriptor_expr.id() != ID_object_descriptor)
    return false;
  const auto &descriptor = to_object_descriptor_expr(descriptor_expr);

  if(
    target.type().id() == ID_pointer &&
    target == null_pointer_exprt(to_pointer_type(target.type())))
  {
    return descriptor.object().id() == "NULL-object" &&
           descriptor.object().type() ==
             to_pointer_type(target.type()).base_type();
  }
  else
  {
    return descriptor.object() == target;
  }
}

SCENARIO(
  "value_sett", "[core][pointer-analysis][value_set]")
{
  symbol_tablet symbol_table;
  namespacet ns(symbol_table);
  value_sett value_set;

  GIVEN("A value-set containing some structure-typed objects")
  {
    // Create struct A { A *x; A *y }

    struct_typet struct_A(
      {{"x", pointer_typet(struct_tag_typet("A"), sizeof(void *) * CHAR_BIT)},
       {"y", pointer_typet(struct_tag_typet("A"), sizeof(void *) * CHAR_BIT)}});
    struct_A.set_tag("A");

    auto &A_x = struct_A.components()[0];
    auto &A_y = struct_A.components()[1];

    A_x.set_base_name("x");
    A_x.set_pretty_name("x");

    A_y.set_base_name("y");
    A_y.set_pretty_name("y");

    type_symbolt A_symbol{"A", struct_A, irep_idt{}};
    A_symbol.base_name = "A";
    A_symbol.pretty_name = "A";

    symbol_table.add(A_symbol);

    // Create global symbols struct A a1, a2, a3;

    symbolt a1_symbol{"a1", struct_tag_typet(A_symbol.name), irep_idt{}};
    a1_symbol.base_name = "a1";
    a1_symbol.pretty_name = "a1";
    a1_symbol.is_static_lifetime = true;
    symbol_table.add(a1_symbol);

    symbolt a2_symbol{"a2", struct_tag_typet(A_symbol.name), irep_idt{}};
    a2_symbol.base_name = "a2";
    a2_symbol.pretty_name = "a2";
    a2_symbol.is_static_lifetime = true;
    symbol_table.add(a2_symbol);

    symbolt a3_symbol{"a3", struct_tag_typet(A_symbol.name), irep_idt{}};
    a3_symbol.base_name = "a3";
    a3_symbol.pretty_name = "a3";
    a3_symbol.is_static_lifetime = true;
    symbol_table.add(a3_symbol);

    // Assign a1.x = &a2; a1.y = &a3:

    member_exprt a1_x(a1_symbol.symbol_expr(), A_x);
    member_exprt a1_y(a1_symbol.symbol_expr(), A_y);

    code_assignt assign_x(a1_x, address_of_exprt(a2_symbol.symbol_expr()));
    code_assignt assign_y(a1_y, address_of_exprt(a3_symbol.symbol_expr()));

    value_set.apply_code(assign_x, ns);
    value_set.apply_code(assign_y, ns);

    null_pointer_exprt null_A_ptr(to_pointer_type(a1_x.type()));

    WHEN("We query what a1.x points to")
    {
      const std::vector<exprt> a1_x_result = value_set.get_value_set(a1_x, ns);

      THEN("It should point to 'a2'")
      {
        REQUIRE(a1_x_result.size() == 1);
        const exprt &result = *a1_x_result.begin();
        REQUIRE(object_descriptor_matches(result, a2_symbol.symbol_expr()));
      }
    }

    WHEN("We query what a1.y points to")
    {
      const std::vector<exprt> a1_y_result = value_set.get_value_set(a1_y, ns);

      THEN("It should point to 'a3'")
      {
        REQUIRE(a1_y_result.size() == 1);
        const exprt &result = *a1_y_result.begin();
        REQUIRE(object_descriptor_matches(result, a3_symbol.symbol_expr()));
      }
    }

    WHEN("We query what (a1 WITH x = NULL).x points to")
    {
      with_exprt a1_with(
        a1_symbol.symbol_expr(), exprt{ID_member_name}, null_A_ptr);
      a1_with.where().set(ID_component_name, A_x.get_name());

      member_exprt member_of_with(a1_with, A_x);

      const std::vector<exprt> matching_with_result =
        value_set.get_value_set(member_of_with, ns);

      THEN("It should be NULL")
      {
        REQUIRE(matching_with_result.size() == 1);
        const exprt &result = *matching_with_result.begin();
        REQUIRE(object_descriptor_matches(result, null_A_ptr));
      }
    }

    WHEN("We query what (a1 WITH x = NULL).y points to")
    {
      with_exprt a1_with(
        a1_symbol.symbol_expr(), exprt{ID_member_name}, null_A_ptr);
      a1_with.where().set(ID_component_name, A_x.get_name());

      member_exprt member_of_with(a1_with, A_y);

      const std::vector<exprt> non_matching_with_result =
        value_set.get_value_set(member_of_with, ns);

      THEN("It should point to 'a3'")
      {
        REQUIRE(non_matching_with_result.size() == 1);
        const exprt &result = *non_matching_with_result.begin();
        REQUIRE(object_descriptor_matches(result, a3_symbol.symbol_expr()));
      }
    }

    WHEN("We query what (a1 WITH x = NULL) points to")
    {
      with_exprt a1_with(
        a1_symbol.symbol_expr(), exprt{ID_member_name}, null_A_ptr);
      a1_with.where().set(ID_component_name, A_x.get_name());

      const std::vector<exprt> maybe_matching_with_result =
        value_set.get_value_set(a1_with, ns);

      THEN("It may point to NULL")
      {
        bool found = false;
        for(const exprt &e : maybe_matching_with_result)
        {
          if(object_descriptor_matches(e, a1_with.new_value()))
            found = true;
        }

        REQUIRE(found);
      }

      THEN("It may point to 'a2'")
      {
        // This happens because no entry for the whole struct is recorded, so
        // value_sett tries looking up the struct's first component.

        bool found = false;
        for(const exprt &e : maybe_matching_with_result)
        {
          if(object_descriptor_matches(e, a2_symbol.symbol_expr()))
            found = true;
        }

        REQUIRE(found);
      }
    }

    WHEN("We query what '{ .x = &a2, .y = &a3 }.x' points to")
    {
      struct_exprt struct_constant(
        {address_of_exprt(a2_symbol.symbol_expr()),
         address_of_exprt(a3_symbol.symbol_expr())},
        struct_tag_typet(A_symbol.name));

      member_exprt member_of_constant(struct_constant, A_x);

      auto member_of_constant_result = value_set.get_value_set(
        member_of_constant, ns);

      THEN("It should point to 'a2'")
      {
        REQUIRE(member_of_constant_result.size() == 1);
        const exprt &result = *member_of_constant_result.begin();
        REQUIRE(object_descriptor_matches(result, a2_symbol.symbol_expr()));
      }
    }
  }

  GIVEN("Some global integer symbols")
  {
    // Make some global integers i1, i2, i3:
    signedbv_typet int32_type(32);
    pointer_typet int32_ptr(int32_type, sizeof(void *) * CHAR_BIT);

    symbolt i1{"i1", int32_type, irep_idt{}};
    i1.base_name = "i1";
    i1.pretty_name = "i1";
    i1.is_static_lifetime = true;
    symbol_table.add(i1);

    symbolt i2{"i2", int32_type, irep_idt{}};
    i2.base_name = "i2";
    i2.pretty_name = "i2";
    i2.is_static_lifetime = true;
    symbol_table.add(i2);

    symbolt i3{"i3", int32_type, irep_idt{}};
    i3.base_name = "i3";
    i3.pretty_name = "i3";
    i3.is_static_lifetime = true;
    symbol_table.add(i3);

    WHEN("We query { &i1, &i2 }[i3]")
    {
      array_exprt arr(
        {address_of_exprt(i1.symbol_expr()),
         address_of_exprt(i2.symbol_expr())},
        array_typet(int32_ptr, from_integer(2, int32_type)));

      index_exprt index_of_arr(arr, i3.symbol_expr());

      const std::vector<exprt> index_of_arr_result =
        value_set.get_value_set(index_of_arr, ns);

      THEN("We should get either &i1 or &i2, but not unknown")
      {
        REQUIRE(index_of_arr_result.size() == 2);

        bool found_i1 = false, found_i2 = false;
        for(const exprt &result : index_of_arr_result)
        {
          if(object_descriptor_matches(result, i1.symbol_expr()))
            found_i1 = true;
          else if(object_descriptor_matches(result, i2.symbol_expr()))
            found_i2 = true;
        }

        REQUIRE(found_i1);
        REQUIRE(found_i2);
      }
    }

    WHEN("We query (ARRAY_OF(&i1))[i3]")
    {
      array_of_exprt arr(
        address_of_exprt(i1.symbol_expr()),
        array_typet(int32_ptr, from_integer(2, int32_type)));

      index_exprt index_of_arr(arr, i3.symbol_expr());

      std::vector<exprt> index_of_arr_result =
        value_set.get_value_set(index_of_arr, ns);

      THEN("We should get &i1")
      {
        REQUIRE(index_of_arr_result.size() == 1);
        REQUIRE(
          object_descriptor_matches(
            *index_of_arr_result.begin(), i1.symbol_expr()));
      }
    }
  }
}