loop_utils.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Helper functions for k-induction and loop invariants
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#include "loop_utils.h"
 
#include <analyses/local_may_alias.h>
 
#include <goto-programs/pointer_arithmetic.h>
 
#include <util/pointer_expr.h>
#include <util/std_expr.h>
 
goto_programt::targett get_loop_exit(const loopt &loop)
{
  PRECONDITION(!loop.empty());
 
  // find the last instruction in the loop
  std::map<unsigned, goto_programt::targett> loop_map;
 
  for(loopt::const_iterator l_it=loop.begin();
      l_it!=loop.end();
      l_it++)
    loop_map[(*l_it)->location_number]=*l_it;
 
  // get the one with the highest number
  goto_programt::targett last=(--loop_map.end())->second;
 
  return ++last;
}
 
void get_assigns_lhs(
  const local_may_aliast &local_may_alias,
  goto_programt::const_targett t,
  const exprt &lhs,
  assignst &assigns)
{
  get_assigns_lhs(
    local_may_alias, t, lhs, assigns, [](const exprt &e) { return true; });
}
 
void get_assigns_lhs(
  const local_may_aliast &local_may_alias,
  goto_programt::const_targett t,
  const exprt &lhs,
  assignst &assigns,
  std::function<bool(const exprt &)> predicate)
{
  if(
    (lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index) &&
    predicate(lhs))
  {
    assigns.insert(lhs);
  }
  else if(lhs.id() == ID_dereference)
  {
    const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
    for(const auto &mod : local_may_alias.get(t, ptr.pointer))
    {
      const typecast_exprt typed_mod{mod, ptr.pointer.type()};
      if(mod.id() == ID_unknown)
      {
        continue;
      }
      exprt to_insert;
      if(ptr.offset.is_nil())
        to_insert = dereference_exprt{typed_mod};
      else
        to_insert = dereference_exprt{plus_exprt{typed_mod, ptr.offset}};
      if(predicate(to_insert))
        assigns.insert(std::move(to_insert));
    }
  }
  else if(lhs.id() == ID_if)
  {
    const if_exprt &if_expr = to_if_expr(lhs);
 
    get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns);
    get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns);
  }
}
 
void get_assigns(
  const local_may_aliast &local_may_alias,
  const loopt &loop,
  assignst &assigns)
{
  get_assigns(
    local_may_alias, loop, assigns, [](const exprt &e) { return true; });
}
 
void get_assigns(
  const local_may_aliast &local_may_alias,
  const loopt &loop,
  assignst &assigns,
  std::function<bool(const exprt &)> predicate)
{
  for(loopt::const_iterator i_it = loop.begin(); i_it != loop.end(); i_it++)
  {
    const goto_programt::instructiont &instruction = **i_it;
 
    if(instruction.is_assign())
    {
      const exprt &lhs = instruction.assign_lhs();
      get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
    }
    else if(instruction.is_function_call())
    {
      const exprt &lhs = instruction.call_lhs();
      get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
    }
  }
}