goto_program.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Concrete Goto Program
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
#define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
 
#include <util/invariant.h>
#include <util/source_location.h>
 
#include "goto_instruction_code.h"
 
#include <iosfwd>
#include <limits>
#include <list>
#include <set>
#include <string>
 
class code_gotot;
class namespacet;
enum class validation_modet;
 
enum goto_program_instruction_typet
{
  NO_INSTRUCTION_TYPE = 0,
  GOTO = 1,              // branch, possibly guarded
  ASSUME = 2,            // non-failing guarded self loop
  ASSERT = 3,            // assertions
  OTHER = 4,             // anything else
  SKIP = 5,              // just advance the PC
  START_THREAD = 6,      // spawns an asynchronous thread
  END_THREAD = 7,        // end the current thread
  LOCATION = 8,          // semantically like SKIP
  END_FUNCTION = 9,      // exit point of a function
  ATOMIC_BEGIN = 10,     // marks a block without interleavings
  ATOMIC_END = 11,       // end of a block without interleavings
  SET_RETURN_VALUE = 12, // set function return value (no control-flow change)
  ASSIGN = 13,           // assignment lhs:=rhs
  DECL = 14,             // declare a local variable
  DEAD = 15,             // marks the end-of-live of a local variable
  FUNCTION_CALL = 16,    // call a function
  THROW = 17,            // throw an exception
  CATCH = 18,            // push, pop or enter an exception handler
  INCOMPLETE_GOTO = 19   // goto where target is yet to be determined
};
 
std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
 
class goto_programt
{
public:
  goto_programt(const goto_programt &)=delete;
  goto_programt &operator=(const goto_programt &)=delete;
 
  // Move operations need to be explicitly enabled as they are deleted with the
  // copy operations
  // default for move operations isn't available on Windows yet, so define
  //  explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
  //  under "Defaulted and Deleted Functions")
 
  goto_programt(goto_programt &&other):
    instructions(std::move(other.instructions))
  {
  }
 
  goto_programt &operator=(goto_programt &&other)
  {
    instructions=std::move(other.instructions);
    return *this;
  }
 
  class instructiont final
  {
  protected:
    goto_instruction_codet _code;
 
  public:
    const goto_instruction_codet &code() const
    {
      return _code;
    }
 
    goto_instruction_codet &code_nonconst()
    {
      return _code;
    }
 
    const exprt &assign_lhs() const
    {
      PRECONDITION(is_assign());
      return to_code_assign(_code).lhs();
    }
 
    exprt &assign_lhs_nonconst()
    {
      PRECONDITION(is_assign());
      return to_code_assign(_code).lhs();
    }
 
    const exprt &assign_rhs() const
    {
      PRECONDITION(is_assign());
      return to_code_assign(_code).rhs();
    }
 
    exprt &assign_rhs_nonconst()
    {
      PRECONDITION(is_assign());
      return to_code_assign(_code).rhs();
    }
 
    const symbol_exprt &decl_symbol() const
    {
      PRECONDITION(is_decl());
      auto &decl = expr_checked_cast<code_declt>(_code);
      return decl.symbol();
    }
 
    symbol_exprt &decl_symbol()
    {
      PRECONDITION(is_decl());
      auto &decl = expr_checked_cast<code_declt>(_code);
      return decl.symbol();
    }
 
    const symbol_exprt &dead_symbol() const
    {
      PRECONDITION(is_dead());
      return to_code_dead(_code).symbol();
    }
 
    symbol_exprt &dead_symbol()
    {
      PRECONDITION(is_dead());
      return to_code_dead(_code).symbol();
    }
 
    const exprt &return_value() const
    {
      PRECONDITION(is_set_return_value());
      return to_code_return(_code).return_value();
    }
 
    exprt &return_value()
    {
      PRECONDITION(is_set_return_value());
      return to_code_return(_code).return_value();
    }
 
    const exprt &call_function() const
    {
      PRECONDITION(is_function_call());
      return to_code_function_call(_code).function();
    }
 
    exprt &call_function()
    {
      PRECONDITION(is_function_call());
      return to_code_function_call(_code).function();
    }
 
    const exprt &call_lhs() const
    {
      PRECONDITION(is_function_call());
      return to_code_function_call(_code).lhs();
    }
 
    exprt &call_lhs()
    {
      PRECONDITION(is_function_call());
      return to_code_function_call(_code).lhs();
    }
 
    const exprt::operandst &call_arguments() const
    {
      PRECONDITION(is_function_call());
      return to_code_function_call(_code).arguments();
    }
 
    exprt::operandst &call_arguments()
    {
      PRECONDITION(is_function_call());
      return to_code_function_call(_code).arguments();
    }
 
    const goto_instruction_codet &get_other() const
    {
      PRECONDITION(is_other());
      return _code;
    }
 
    void set_other(goto_instruction_codet &c)
    {
      PRECONDITION(is_other());
      _code = std::move(c);
    }
 
  protected:
    source_locationt _source_location;
 
  public:
    const source_locationt &source_location() const
    {
      return _source_location;
    }
 
    source_locationt &source_location_nonconst()
    {
      return _source_location;
    }
 
    goto_program_instruction_typet type() const
    {
      return _type;
    }
 
  protected:
    // Use type() to access. To prevent malformed instructions, no non-const
    // access method is provided.
    goto_program_instruction_typet _type;
 
    exprt guard;
 
  public:
    bool has_condition() const
    {
      return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
    }
 
    const exprt &condition() const
    {
      PRECONDITION(has_condition());
      return guard;
    }
 
    exprt &condition_nonconst()
    {
      PRECONDITION(has_condition());
      return guard;
    }
 
    // The below will eventually become a single target only.
    typedef std::list<instructiont>::iterator targett;
    typedef std::list<instructiont>::const_iterator const_targett;
    typedef std::list<targett> targetst;
    typedef std::list<const_targett> const_targetst;
 
    struct target_less_than // NOLINT(readability/identifiers)
    {
      static inline bool
      order_const_target(const const_targett i1, const const_targett i2)
      {
        const instructiont &_i1 = *i1;
        const instructiont &_i2 = *i2;
        return &_i1 < &_i2;
      }
 
      inline bool
      operator()(const const_targett &i1, const const_targett &i2) const
      {
        return order_const_target(i1, i2);
      }
 
      inline bool operator()(const targett &i1, const targett &i2) const
      {
        return &(*i1) < &(*i2);
      }
    };
 
    targetst targets;
 
    const_targett get_target() const
    {
      PRECONDITION(targets.size() == 1);
      return targets.front();
    }
 
    targett get_target()
    {
      PRECONDITION(targets.size()==1);
      return targets.front();
    }
 
    void set_target(targett t)
    {
      targets.clear();
      targets.push_back(t);
    }
 
    bool has_target() const
    {
      return !targets.empty();
    }
 
    typedef std::list<irep_idt> labelst;
    labelst labels;
 
    // will go away
    std::set<targett, target_less_than> incoming_edges;
 
    bool is_target() const
    { return target_number!=nil_target; }
 
    void clear(goto_program_instruction_typet __type)
    {
      _type = __type;
      targets.clear();
      guard=true_exprt();
      _code.make_nil();
    }
 
    void turn_into_skip()
    {
      clear(SKIP);
    }
 
    void turn_into_assume()
    {
      PRECONDITION(_type == GOTO || _type == ASSERT);
      _type = ASSUME;
      targets.clear();
      _code.make_nil();
    }
 
    void complete_goto(targett _target)
    {
      PRECONDITION(_type == INCOMPLETE_GOTO);
      _code.make_nil();
      targets.push_back(_target);
      _type = GOTO;
    }
 
    // clang-format off
    bool is_goto            () const { return _type == GOTO;             }
    bool is_set_return_value() const { return _type == SET_RETURN_VALUE; }
    bool is_assign          () const { return _type == ASSIGN;           }
    bool is_function_call   () const { return _type == FUNCTION_CALL;    }
    bool is_throw           () const { return _type == THROW;            }
    bool is_catch           () const { return _type == CATCH;            }
    bool is_skip            () const { return _type == SKIP;             }
    bool is_location        () const { return _type == LOCATION;         }
    bool is_other           () const { return _type == OTHER;            }
    bool is_decl            () const { return _type == DECL;             }
    bool is_dead            () const { return _type == DEAD;             }
    bool is_assume          () const { return _type == ASSUME;           }
    bool is_assert          () const { return _type == ASSERT;           }
    bool is_atomic_begin    () const { return _type == ATOMIC_BEGIN;     }
    bool is_atomic_end      () const { return _type == ATOMIC_END;       }
    bool is_start_thread    () const { return _type == START_THREAD;     }
    bool is_end_thread      () const { return _type == END_THREAD;       }
    bool is_end_function    () const { return _type == END_FUNCTION;     }
    bool is_incomplete_goto () const { return _type == INCOMPLETE_GOTO;  }
    // clang-format on
 
    instructiont():
      instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
    {
    }
 
    explicit instructiont(goto_program_instruction_typet __type)
      : _code(static_cast<const goto_instruction_codet &>(get_nil_irep())),
        _source_location(source_locationt::nil()),
        _type(__type),
        guard(true_exprt())
    {
    }
 
    instructiont(
      goto_instruction_codet __code,
      source_locationt __source_location,
      goto_program_instruction_typet __type,
      exprt _guard,
      targetst _targets)
      : _code(std::move(__code)),
        _source_location(std::move(__source_location)),
        _type(__type),
        guard(std::move(_guard)),
        targets(std::move(_targets))
    {
    }
 
    void swap(instructiont &instruction)
    {
      using std::swap;
      swap(instruction._code, _code);
      swap(instruction._source_location, _source_location);
      swap(instruction._type, _type);
      swap(instruction.guard, guard);
      swap(instruction.targets, targets);
      swap(instruction.labels, labels);
    }
 
    static const unsigned nil_target=
      std::numeric_limits<unsigned>::max();
 
    unsigned location_number = 0;
 
    unsigned loop_number = 0;
 
    unsigned target_number = nil_target;
 
    bool is_backwards_goto() const
    {
      if(!is_goto())
        return false;
 
      for(const auto &t : targets)
        if(t->location_number<=location_number)
          return true;
 
      return false;
    }
 
    std::string to_string() const
    {
      std::ostringstream instruction_id_builder;
      instruction_id_builder << _type;
      return instruction_id_builder.str();
    }
 
    bool equals(const instructiont &other) const;
 
    void validate(const namespacet &ns, const validation_modet vm) const;
 
    void transform(std::function<std::optional<exprt>(exprt)>);
 
    void apply(std::function<void(const exprt &)>) const;
 
    std::ostream &output(std::ostream &) const;
  };
 
  // Never try to change this to vector-we mutate the list while iterating
  typedef std::list<instructiont> instructionst;
 
  typedef instructionst::iterator targett;
  typedef instructionst::const_iterator const_targett;
  typedef std::list<targett> targetst;
  typedef std::list<const_targett> const_targetst;
  // NOLINTNEXTLINE(readability/identifiers)
  typedef instructiont::target_less_than target_less_than;
 
  instructionst instructions;
 
  targett const_cast_target(const_targett t)
  {
    return instructions.erase(t, t);
  }
 
  const_targett const_cast_target(const_targett t) const
  {
    return t;
  }
 
  template <typename Target>
  std::list<Target> get_successors(Target target) const;
 
  void compute_incoming_edges();
 
  void insert_before_swap(targett target)
  {
    PRECONDITION(target!=instructions.end());
    const auto next=std::next(target);
    instructions.insert(next, instructiont())->swap(*target);
  }
 
  void insert_before_swap(targett target, instructiont &instruction)
  {
    insert_before_swap(target);
    target->swap(instruction);
  }
 
  void insert_before_swap(
    targett target,
    goto_programt &p)
  {
    PRECONDITION(target!=instructions.end());
    if(p.instructions.empty())
      return;
    insert_before_swap(target, p.instructions.front());
    auto next=std::next(target);
    p.instructions.erase(p.instructions.begin());
    instructions.splice(next, p.instructions);
  }
 
  targett insert_before(const_targett target)
  {
    return instructions.insert(target, instructiont());
  }
 
  targett insert_before(const_targett target, const instructiont &i)
  {
    return instructions.insert(target, i);
  }
 
  targett insert_after(const_targett target)
  {
    return instructions.insert(std::next(target), instructiont());
  }
 
  targett insert_after(const_targett target, const instructiont &i)
  {
    return instructions.insert(std::next(target), i);
  }
 
  void destructive_append(goto_programt &p)
  {
    instructions.splice(instructions.end(),
                        p.instructions);
  }
 
  void destructive_insert(
    const_targett target,
    goto_programt &p)
  {
    instructions.splice(target, p.instructions);
  }
 
  targett add(instructiont &&instruction)
  {
    instructions.push_back(std::move(instruction));
    return --instructions.end();
  }
 
  targett add_instruction()
  {
    return add(instructiont());
  }
 
  targett add_instruction(goto_program_instruction_typet type)
  {
    return add(instructiont(type));
  }
 
  std::ostream &output(std::ostream &out) const;
 
  void compute_target_numbers();
 
  void compute_location_numbers(unsigned &nr)
  {
    for(auto &i : instructions)
    {
      INVARIANT(
        nr != std::numeric_limits<unsigned>::max(),
        "Too many location numbers assigned");
      i.location_number=nr++;
    }
  }
 
  void compute_location_numbers()
  {
    unsigned nr=0;
    compute_location_numbers(nr);
  }
 
  void compute_loop_numbers();
 
  void update();
 
  static irep_idt
  loop_id(const irep_idt &function_id, const instructiont &instruction)
  {
    return id2string(function_id) + "." +
           std::to_string(instruction.loop_number);
  }
 
  bool empty() const
  {
    return instructions.empty();
  }
 
  goto_programt()
  {
  }
 
  ~goto_programt()
  {
  }
 
  void swap(goto_programt &program)
  {
    program.instructions.swap(instructions);
  }
 
  void clear()
  {
    instructions.clear();
  }
 
  targett get_end_function()
  {
    PRECONDITION(!instructions.empty());
    const auto end_function=std::prev(instructions.end());
    DATA_INVARIANT(end_function->is_end_function(),
                   "goto program ends on END_FUNCTION");
    return end_function;
  }
 
  const_targett get_end_function() const
  {
    PRECONDITION(!instructions.empty());
    const auto end_function=std::prev(instructions.end());
    DATA_INVARIANT(end_function->is_end_function(),
                   "goto program ends on END_FUNCTION");
    return end_function;
  }
 
  void copy_from(const goto_programt &src);
 
  bool has_assertion() const;
 
  typedef std::set<irep_idt> decl_identifierst;
  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
 
  bool equals(const goto_programt &other) const;
 
  void validate(const namespacet &ns, const validation_modet vm) const
  {
    for(const instructiont &ins : instructions)
    {
      ins.validate(ns, vm);
    }
  }
 
  static instructiont make_set_return_value(
    exprt return_value,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      code_returnt(std::move(return_value)),
      l,
      SET_RETURN_VALUE,
      nil_exprt(),
      {});
  }
 
  static instructiont make_set_return_value(
    const code_returnt &code,
    const source_locationt &l = source_locationt::nil()) = delete;
 
  static instructiont
  make_skip(const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      SKIP,
      nil_exprt(),
      {});
  }
 
  static instructiont make_location(const source_locationt &l)
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      LOCATION,
      nil_exprt(),
      {});
  }
 
  static instructiont
  make_throw(const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      THROW,
      nil_exprt(),
      {});
  }
 
  static instructiont
  make_catch(const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      CATCH,
      nil_exprt(),
      {});
  }
 
  static instructiont make_assertion(
    const exprt &g,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      ASSERT,
      exprt(g),
      {});
  }
 
  static instructiont make_assumption(
    const exprt &g,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      ASSUME,
      g,
      {});
  }
 
  static instructiont make_other(
    const goto_instruction_codet &_code,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(_code, l, OTHER, nil_exprt(), {});
  }
 
  static instructiont make_decl(
    const symbol_exprt &symbol,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
  }
 
  static instructiont make_dead(
    const symbol_exprt &symbol,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
  }
 
  static instructiont
  make_atomic_begin(const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      ATOMIC_BEGIN,
      nil_exprt(),
      {});
  }
 
  static instructiont
  make_atomic_end(const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      ATOMIC_END,
      nil_exprt(),
      {});
  }
 
  static instructiont
  make_end_function(const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      END_FUNCTION,
      nil_exprt(),
      {});
  }
 
  static instructiont make_incomplete_goto(
    const exprt &_cond,
    const source_locationt &l = source_locationt::nil())
  {
    PRECONDITION(_cond.is_boolean());
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      INCOMPLETE_GOTO,
      _cond,
      {});
  }
 
  static instructiont
  make_incomplete_goto(const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      INCOMPLETE_GOTO,
      true_exprt(),
      {});
  }
 
  static instructiont make_incomplete_goto(
    const code_gotot &,
    const source_locationt & = source_locationt::nil());
 
  static instructiont make_goto(
    targett _target,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      GOTO,
      true_exprt(),
      {_target});
  }
 
  static instructiont make_goto(
    targett _target,
    const exprt &g,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      static_cast<const goto_instruction_codet &>(get_nil_irep()),
      l,
      GOTO,
      g,
      {_target});
  }
 
  static instructiont make_assignment(
    const code_assignt &_code,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(_code, l, ASSIGN, nil_exprt(), {});
  }
 
  static instructiont make_assignment(
    exprt lhs,
    exprt rhs,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
  }
 
  static instructiont make_decl(
    const code_declt &_code,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(_code, l, DECL, nil_exprt(), {});
  }
 
  static instructiont make_function_call(
    const code_function_callt &_code,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
  }
 
  static instructiont make_function_call(
    exprt lhs,
    exprt function,
    code_function_callt::argumentst arguments,
    const source_locationt &l = source_locationt::nil())
  {
    return instructiont(
      code_function_callt(lhs, std::move(function), std::move(arguments)),
      l,
      FUNCTION_CALL,
      nil_exprt(),
      {});
  }
};
 
template <typename Target>
std::list<Target> goto_programt::get_successors(
  Target target) const
{
  if(target==instructions.end())
    return std::list<Target>();
 
  const auto next=std::next(target);
 
  const instructiont &i=*target;
 
  if(i.is_goto())
  {
    std::list<Target> successors(i.targets.begin(), i.targets.end());
 
    if(!i.condition().is_true() && next != instructions.end())
      successors.push_back(next);
 
    return successors;
  }
 
  if(i.is_start_thread())
  {
    std::list<Target> successors(i.targets.begin(), i.targets.end());
 
    if(next!=instructions.end())
      successors.push_back(next);
 
    return successors;
  }
 
  if(i.is_end_thread())
  {
    // no successors
    return std::list<Target>();
  }
 
  if(i.is_throw())
  {
    // the successors are non-obvious
    return std::list<Target>();
  }
 
  if(i.is_assume())
  {
    return !i.condition().is_false() && next != instructions.end()
             ? std::list<Target>{next}
             : std::list<Target>();
  }
 
  if(next!=instructions.end())
  {
    return std::list<Target>{next};
  }
 
  return std::list<Target>();
}
 
// NOLINTNEXTLINE(readability/identifiers)
struct const_target_hash
{
  std::size_t operator()(
    const goto_programt::const_targett t) const
  {
    using hash_typet = decltype(&(*t));
    return std::hash<hash_typet>{}(&(*t));
  }
};
 
struct pointee_address_equalt
{
  template <class A, class B>
  bool operator()(const A &a, const B &b) const
  {
    return &(*a) == &(*b);
  }
};
 
template <typename GotoFunctionT, typename PredicateT, typename HandlerT>
void for_each_instruction_if(
  GotoFunctionT &&goto_function,
  PredicateT predicate,
  HandlerT handler)
{
  auto &&instructions = goto_function.body.instructions;
  for(auto it = instructions.begin(); it != instructions.end(); ++it)
  {
    if(predicate(it))
    {
      handler(it);
    }
  }
}
 
template <typename GotoFunctionT, typename HandlerT>
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
{
  using iterator_t = decltype(goto_function.body.instructions.begin());
  for_each_instruction_if(
    goto_function, [](const iterator_t &) { return true; }, handler);
}
 
#define forall_goto_program_instructions(it, program) \
  for(goto_programt::instructionst::const_iterator \
      it=(program).instructions.begin(); \
      it!=(program).instructions.end(); it++)
 
#define Forall_goto_program_instructions(it, program) \
  for(goto_programt::instructionst::iterator \
      it=(program).instructions.begin(); \
      it!=(program).instructions.end(); it++)
 
std::list<exprt> objects_read(const goto_programt::instructiont &);
std::list<exprt> objects_written(const goto_programt::instructiont &);
 
std::list<exprt> expressions_read(const goto_programt::instructiont &);
std::list<exprt> expressions_written(const goto_programt::instructiont &);
 
std::string as_string(
  const namespacet &ns,
  const irep_idt &function,
  const goto_programt::instructiont &);
 
#endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H