remove_skip.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Program Transformation
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#include "remove_skip.h"
#include "goto_model.h"
 
#include <util/std_code.h>

bool is_skip(
  const goto_programt &body,
  goto_programt::const_targett it,
  bool ignore_labels)
{
  if(!ignore_labels && !it->labels.empty())
    return false;
 
  if(it->is_skip())
    return !it->code().get_bool(ID_explicit);
 
  if(it->is_goto())
  {
    if(it->condition() == false)
      return true;
 
    goto_programt::const_targett next_it = it;
    next_it++;
 
    if(next_it == body.instructions.end())
      return false;
 
    // A branch to the next instruction is a skip
    // We also require the guard to be 'true'
    return it->condition() == true && it->get_target() == next_it;
  }
 
  if(it->is_other())
  {
    if(it->get_other().is_nil())
      return true;
 
    const irep_idt &statement = it->get_other().get_statement();
 
    if(statement==ID_skip)
      return true;
    else if(statement==ID_expression)
    {
      const code_expressiont &code_expression = to_code_expression(it->code());
      const exprt &expr=code_expression.expression();
      if(expr.id()==ID_typecast &&
         expr.type().id()==ID_empty &&
         to_typecast_expr(expr).op().is_constant())
      {
        // something like (void)0
        return true;
      }
    }
 
    return false;
  }
 
  return false;
}

void remove_skip(
  goto_programt &goto_program,
  goto_programt::targett begin,
  goto_programt::targett end)
{
  // This needs to be a fixed-point, as
  // removing a skip can turn a goto into a skip.
  std::size_t old_size;
 
  do
  {
    old_size=goto_program.instructions.size();
 
    // maps deleted instructions to their replacement
    typedef std::map<
      goto_programt::targett,
      goto_programt::targett,
      goto_programt::target_less_than>
      new_targetst;
    new_targetst new_targets;
 
    // remove skip statements
 
    for(goto_programt::instructionst::iterator it = begin; it != end;)
    {
      goto_programt::targett old_target=it;
 
      // for collecting labels
      std::list<irep_idt> labels;
 
      while(is_skip(goto_program, it, true))
      {
        // don't remove the last skip statement,
        // it could be a target
        if(
          it == std::prev(end) ||
          (std::next(it)->is_end_function() &&
           (!labels.empty() || !it->labels.empty())))
        {
          break;
        }
 
        // save labels
        labels.splice(labels.end(), it->labels);
        it++;
      }
 
      goto_programt::targett new_target=it;
 
      // save labels
      it->labels.splice(it->labels.begin(), labels);
 
      if(new_target!=old_target)
      {
        for(; old_target!=new_target; ++old_target)
          new_targets[old_target]=new_target; // remember the old targets
      }
      else
        it++;
    }
 
    // adjust gotos across the full goto program body
    for(auto &ins : goto_program.instructions)
    {
      if(ins.is_goto() || ins.is_start_thread() || ins.is_catch())
      {
        for(auto &target : ins.targets)
        {
          new_targetst::const_iterator result = new_targets.find(target);
 
          if(result!=new_targets.end())
            target = result->second;
        }
      }
    }
 
    while(new_targets.find(begin) != new_targets.end())
      ++begin;
 
    // now delete the skips -- we do so after adjusting the
    // gotos to avoid dangling targets
    for(const auto &new_target : new_targets)
      goto_program.instructions.erase(new_target.first);
 
    // remove the last skip statement unless it's a target
    goto_program.compute_target_numbers();
 
    if(begin != end)
    {
      goto_programt::targett last = std::prev(end);
      if(begin == last)
        ++begin;
 
      if(is_skip(goto_program, last) && !last->is_target())
        goto_program.instructions.erase(last);
    }
  }
  while(goto_program.instructions.size()<old_size);
}

void remove_skip(goto_programt &goto_program)
{
  remove_skip(
    goto_program,
    goto_program.instructions.begin(),
    goto_program.instructions.end());
 
  goto_program.update();
}

void remove_skip(goto_functionst &goto_functions)
{
  for(auto &gf_entry : goto_functions.function_map)
  {
    remove_skip(
      gf_entry.second.body,
      gf_entry.second.body.instructions.begin(),
      gf_entry.second.body.instructions.end());
  }
 
  // we may remove targets
  goto_functions.update();
}
 
void remove_skip(goto_modelt &goto_model)
{
  remove_skip(goto_model.goto_functions);
}