stack_depth.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Stack depth checks
 
Author: Daniel Kroening, Michael Tautschnig
 
Date: November 2011
 
\*******************************************************************/
 
 
#include "stack_depth.h"
 
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/c_types.h>
 
#include <goto-programs/goto_model.h>
 
#include <ansi-c/goto-conversion/goto_convert_functions.h>
#include <linking/static_lifetime_init.h>
 
static symbol_exprt add_stack_depth_symbol(
  goto_modelt &goto_model,
  message_handlert &message_handler)
{
  const irep_idt identifier="$stack_depth";
  typet type = size_type();
 
  symbolt new_symbol{identifier, type, ID_C};
  new_symbol.base_name=identifier;
  new_symbol.pretty_name=identifier;
  new_symbol.is_static_lifetime=true;
  new_symbol.value=from_integer(0, type);
  new_symbol.is_thread_local=true;
  new_symbol.is_lvalue=true;
 
  bool failed = goto_model.symbol_table.add(new_symbol);
  CHECK_RETURN(!failed);
 
  if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
    recreate_initialize_function(goto_model, message_handler);
 
  return new_symbol.symbol_expr();
}
 
static void stack_depth(
  goto_programt &goto_program,
  const symbol_exprt &symbol,
  const std::size_t i_depth,
  const exprt &max_depth)
{
  PRECONDITION(!goto_program.instructions.empty());
 
  goto_programt::targett first=goto_program.instructions.begin();
 
  binary_relation_exprt guard(symbol, ID_le, max_depth);
  source_locationt annotated_location = first->source_location();
  annotated_location.set_comment(
    "Stack depth exceeds " + std::to_string(i_depth));
  annotated_location.set_property_class("stack-depth");
  goto_program.insert_before(
    first, goto_programt::make_assertion(guard, annotated_location));
 
  goto_program.insert_before(
    first,
    goto_programt::make_assignment(
      code_assignt(symbol, plus_exprt(symbol, from_integer(1, symbol.type()))),
      first->source_location()));
 
  goto_programt::targett last=--goto_program.instructions.end();
  DATA_INVARIANT(last->is_end_function(), "must be end of function");
 
  goto_programt::instructiont minus_ins = goto_programt::make_assignment(
    code_assignt(symbol, minus_exprt(symbol, from_integer(1, symbol.type()))),
    last->source_location());
 
  goto_program.insert_before_swap(last, minus_ins);
}
 
void stack_depth(
  goto_modelt &goto_model,
  const std::size_t depth,
  message_handlert &message_handler)
{
  const symbol_exprt sym = add_stack_depth_symbol(goto_model, message_handler);
 
  const exprt depth_expr(from_integer(depth, sym.type()));
 
  for(auto &gf_entry : goto_model.goto_functions.function_map)
  {
    if(
      gf_entry.second.body_available() &&
      gf_entry.first != INITIALIZE_FUNCTION &&
      gf_entry.first != goto_functionst::entry_point())
    {
      stack_depth(gf_entry.second.body, sym, depth, depth_expr);
    }
  }
 
  // update counters etc.
  goto_model.goto_functions.update();
}