local_safe_pointers.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Local safe pointer analysis
 
Author: Diffblue Ltd
 
\*******************************************************************/
 
 
#include "local_safe_pointers.h"
 
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/format_expr.h>
#include <util/symbol_table.h>
 
struct goto_null_checkt
{
  bool checked_when_taken;
 
  exprt checked_expr;
};
 
static optionalt<goto_null_checkt> get_null_checked_expr(const exprt &expr)
{
  exprt normalized_expr = expr;
  // If true, then a null check is made when test `expr` passes; if false,
  // one is made when it fails.
  bool checked_when_taken = true;
 
  // Reduce some roundabout ways of saying "x != null", e.g. "!(x == null)".
  while(normalized_expr.id() == ID_not)
  {
    normalized_expr = to_not_expr(normalized_expr).op();
    checked_when_taken = !checked_when_taken;
  }
 
  if(normalized_expr.id() == ID_equal)
  {
    normalized_expr.id(ID_notequal);
    checked_when_taken = !checked_when_taken;
  }
 
  if(normalized_expr.id() == ID_notequal)
  {
    const exprt &op0 = skip_typecast(to_notequal_expr(normalized_expr).op0());
    const exprt &op1 = skip_typecast(to_notequal_expr(normalized_expr).op1());
 
    if(op0.type().id() == ID_pointer &&
       op0 == null_pointer_exprt(to_pointer_type(op0.type())))
    {
      return { { checked_when_taken, op1 } };
    }
 
    if(op1.type().id() == ID_pointer &&
       op1 == null_pointer_exprt(to_pointer_type(op1.type())))
    {
      return { { checked_when_taken, op0 } };
    }
  }
 
  return {};
}
 
void local_safe_pointerst::operator()(const goto_programt &goto_program)
{
  std::set<exprt, type_comparet> checked_expressions(type_comparet{});
 
  for(const auto &instruction : goto_program.instructions)
  {
    // Handle control-flow convergence pessimistically:
    if(instruction.incoming_edges.size() > 1)
      checked_expressions.clear();
    // Retrieve working set for forward GOTOs:
    else if(instruction.is_target())
    {
      auto findit = non_null_expressions.find(instruction.location_number);
      if(findit != non_null_expressions.end())
        checked_expressions = findit->second;
      else
      {
        checked_expressions = std::set<exprt, type_comparet>(type_comparet{});
      }
    }
 
    // Save the working set at this program point:
    if(!checked_expressions.empty())
    {
      non_null_expressions.emplace(
        instruction.location_number, checked_expressions);
    }
 
    switch(instruction.type())
    {
    // Instruction types that definitely don't write anything, and therefore
    // can't store a null pointer:
    case DECL:
    case DEAD:
    case ASSERT:
    case SKIP:
    case LOCATION:
    case SET_RETURN_VALUE:
    case THROW:
    case CATCH:
    case END_FUNCTION:
    case ATOMIC_BEGIN:
    case ATOMIC_END:
      break;
 
    // Possible checks:
    case ASSUME:
      if(auto assume_check = get_null_checked_expr(instruction.condition()))
      {
        if(assume_check->checked_when_taken)
          checked_expressions.insert(assume_check->checked_expr);
      }
 
      break;
 
    case GOTO:
      if(!instruction.is_backwards_goto())
      {
        // Copy current state to GOTO target:
 
        auto target_emplace_result =
          non_null_expressions.emplace(
            instruction.get_target()->location_number, checked_expressions);
 
        // If the target already has a state entry then it is a control-flow
        // merge point and everything will be assumed maybe-null in any case.
        if(target_emplace_result.second)
        {
          if(
            auto conditional_check =
              get_null_checked_expr(instruction.condition()))
          {
            // Add the GOTO condition to either the target or current state,
            // as appropriate:
            if(conditional_check->checked_when_taken)
            {
              target_emplace_result.first->second.insert(
                conditional_check->checked_expr);
            }
            else
              checked_expressions.insert(conditional_check->checked_expr);
          }
        }
      }
 
      break;
 
    case ASSIGN:
    case START_THREAD:
    case END_THREAD:
    case FUNCTION_CALL:
    case OTHER:
    case INCOMPLETE_GOTO:
    case NO_INSTRUCTION_TYPE:
      // Pessimistically assume all other instructions might overwrite any
      // pointer with a possibly-null value.
      checked_expressions.clear();
      break;
    }
  }
}
 
void local_safe_pointerst::output(
  std::ostream &out,
  const goto_programt &goto_program,
  const namespacet &ns)
{
  for(const auto &instruction : goto_program.instructions)
  {
    out << "**** " << instruction.location_number << " "
        << instruction.source_location() << "\n";
 
    out << "Non-null expressions: ";
 
    auto findit = non_null_expressions.find(instruction.location_number);
    if(findit == non_null_expressions.end())
      out << "{}";
    else
    {
      out << "{";
      bool first = true;
      for(const exprt &expr : findit->second)
      {
        if(!first)
          out << ", ";
        first = true;
        format_rec(out, expr);
      }
      out << "}";
    }
 
    out << '\n';
    instruction.output(out);
    out << '\n';
  }
}
 
void local_safe_pointerst::output_safe_dereferences(
  std::ostream &out,
  const goto_programt &goto_program,
  const namespacet &ns)
{
  for(const auto &instruction : goto_program.instructions)
  {
    out << "**** " << instruction.location_number << " "
        << instruction.source_location() << "\n";
 
    out << "Safe (known-not-null) dereferences: ";
 
    auto findit = non_null_expressions.find(instruction.location_number);
    if(findit == non_null_expressions.end())
      out << "{}";
    else
    {
      out << "{";
      bool first = true;
      instruction.apply([&first, &out](const exprt &e) {
        for(auto subexpr_it = e.depth_begin(), subexpr_end = e.depth_end();
            subexpr_it != subexpr_end;
            ++subexpr_it)
        {
          if(subexpr_it->id() == ID_dereference)
          {
            if(!first)
              out << ", ";
            first = true;
            format_rec(out, to_dereference_expr(*subexpr_it).pointer());
          }
        }
      });
      out << "}";
    }
 
    out << '\n';
    instruction.output(out);
    out << '\n';
  }
}
 
bool local_safe_pointerst::is_non_null_at_program_point(
  const exprt &expr, goto_programt::const_targett program_point)
{
  auto findit = non_null_expressions.find(program_point->location_number);
  if(findit == non_null_expressions.end())
    return false;
 
  return findit->second.count(skip_typecast(expr)) != 0;
}