write_stack.cpp

Go to the documentation of this file.

/*******************************************************************\
 
 Module: Variable Sensitivity Domain
 
 Author: DiffBlue Limited.
 
\*******************************************************************/
 
 
#include "write_stack.h"
 
#include <unordered_set>
 
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
 
#include "abstract_environment.h"
 
write_stackt::write_stackt() : stack(), top_stack(true)
{
}
 
write_stackt::write_stackt(
  const exprt &expr,
  const abstract_environmentt &environment,
  const namespacet &ns)
{
  top_stack = false;
  if(expr.type().id() == ID_array)
  {
    // We are assigning an array to a pointer, which is equivalent to assigning
    // the first element of that array
    // &(expr)[0]
    construct_stack_to_pointer(
      address_of_exprt(index_exprt(expr, from_integer(0, signed_size_type()))),
      environment,
      ns);
  }
  else
  {
    construct_stack_to_pointer(expr, environment, ns);
  }
}
 
void write_stackt::construct_stack_to_pointer(
  const exprt &expr,
  const abstract_environmentt &environment,
  const namespacet &ns)
{
  PRECONDITION(expr.type().id() == ID_pointer);
 
  if(expr.id() == ID_address_of)
  {
    // resovle reminder, can either be a symbol, member or index of
    // otherwise unsupported
    construct_stack_to_lvalue(
      to_address_of_expr(expr).object(), environment, ns);
  }
  else if(expr.id() == ID_plus || expr.id() == ID_minus)
  {
    exprt base;
    exprt offset;
    const integral_resultt &which_side =
      get_which_side_integral(expr, base, offset);
    INVARIANT(
      which_side != integral_resultt::NEITHER_INTEGRAL,
      "An offset must be an integral amount");
 
    if(expr.id() == ID_minus)
    {
      // can't get a valid pointer by subtracting from a constant number
      if(which_side == integral_resultt::LHS_INTEGRAL)
      {
        top_stack = true;
        return;
      }
      offset = unary_minus_exprt(offset);
    }
 
    abstract_object_pointert offset_value = environment.eval(offset, ns);
 
    add_to_stack(
      std::make_shared<offset_entryt>(offset_value), environment, ns);
 
    // Build the pointer part
    construct_stack_to_pointer(base, environment, ns);
 
    if(!top_stack)
    {
      // check the symbol at the bottom of the stack
      const auto access = stack.front()->get_access_expr();
      INVARIANT(
        !access.second && access.first.id() == ID_symbol,
        "The base should be an addressable location (i.e. symbol)");
 
      if(access.first.type().id() != ID_array)
      {
        top_stack = true;
      }
    }
  }
  else
  {
    // unknown expression type - play it safe and set to top
    top_stack = true;
  }
}
 
void write_stackt::construct_stack_to_lvalue(
  const exprt &expr,
  const abstract_environmentt &environment,
  const namespacet &ns)
{
  if(!top_stack)
  {
    if(expr.id() == ID_member)
    {
      add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
      construct_stack_to_lvalue(
        to_member_expr(expr).struct_op(), environment, ns);
    }
    else if(expr.id() == ID_symbol || expr.id() == ID_dynamic_object)
    {
      add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
    }
    else if(expr.id() == ID_index)
    {
      construct_stack_to_array_index(to_index_expr(expr), environment, ns);
    }
    else
    {
      top_stack = true;
    }
  }
}
 
void write_stackt::construct_stack_to_array_index(
  const index_exprt &index_expr,
  const abstract_environmentt &environment,
  const namespacet &ns)
{
  abstract_object_pointert offset_value =
    environment.eval(index_expr.index(), ns);
 
  add_to_stack(std::make_shared<offset_entryt>(offset_value), environment, ns);
  construct_stack_to_lvalue(index_expr.array(), environment, ns);
}
 
exprt write_stackt::to_expression() const
{
  // A top stack is useless and its expression should not be evaluated
  PRECONDITION(!is_top_value());
  PRECONDITION(!stack.empty());
  exprt access_expr = stack.front()->get_access_expr().first;
  for(auto it = std::next(stack.begin()); it != stack.end(); ++it)
  {
    const auto access = (*it)->get_access_expr();
    if(access.second)
      access_expr = index_exprt{access_expr, access.first};
    else
      access_expr = access.first;
  }
  address_of_exprt top_expr(access_expr);
  return std::move(top_expr);
}
 
size_t write_stackt::depth() const
{
  return stack.size();
}
 
exprt write_stackt::target_expression(size_t depth) const
{
  PRECONDITION(!is_top_value());
  return stack[depth]->get_access_expr().first;
}
 
exprt write_stackt::offset_expression() const
{
  PRECONDITION(!is_top_value());
  auto const access = stack.back()->get_access_expr();
 
  if(access.second)
    return access.first;
 
  if(access.first.id() == ID_member || access.first.id() == ID_symbol)
    return access.first;
 
  if(access.first.id() == ID_index)
    return to_index_expr(access.first).index();
 
  return from_integer(0, unsigned_long_int_type());
}
 
bool write_stackt::is_top_value() const
{
  return top_stack;
}
 
void write_stackt::add_to_stack(
  std::shared_ptr<write_stack_entryt> entry_pointer,
  const abstract_environmentt environment,
  const namespacet &ns)
{
  if(
    stack.empty() ||
    !stack.front()->try_squash_in(entry_pointer, environment, ns))
  {
    stack.insert(stack.begin(), entry_pointer);
  }
}
 
write_stackt::integral_resultt write_stackt::get_which_side_integral(
  const exprt &expr,
  exprt &out_base_expr,
  exprt &out_integral_expr)
{
  PRECONDITION(expr.operands().size() == 2);
  const auto binary_e = to_binary_expr(expr);
  static const std::unordered_set<irep_idt, irep_id_hash> integral_types = {
    ID_signedbv, ID_unsignedbv, ID_integer};
  if(integral_types.find(binary_e.lhs().type().id()) != integral_types.cend())
  {
    out_integral_expr = binary_e.lhs();
    out_base_expr = binary_e.rhs();
    return integral_resultt::LHS_INTEGRAL;
  }
  else if(
    integral_types.find(binary_e.rhs().type().id()) != integral_types.cend())
  {
    out_integral_expr = binary_e.rhs();
    out_base_expr = binary_e.lhs();
    return integral_resultt::RHS_INTEGRAL;
  }
  else
  {
    out_integral_expr.make_nil();
    out_base_expr.make_nil();
    return integral_resultt::NEITHER_INTEGRAL;
  }
}