goto_program.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_PROGRAM_H
#define CPROVER_GOTO_PROGRAM_H

 
#include <cassert>
#include <ostream>
#include <set>
#include <vector>
#include <irep2/irep2_utils.h>
#include <util/irep/location.h>
#include <util/symtab/namespace.h>
#include <util/irep/std_code.h>
 
#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++)
 
typedef enum
{
  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
  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
  RETURN = 12,        // return from a function
  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,         // catch an exception
  // 19 and 20 were THROW_DECL / THROW_DECL_END, removed in favour of
  // function-level exception-specification metadata. The numeric values are
  // left as a gap so the remaining kinds keep their GOTO-binary encoding (and
  // the in-repo v1 binary fixtures keep loading). A pre-removal binary that
  // actually contains 19/20 -- only produced from C++ exception-spec code by an
  // older ESBMC -- has no handler and fails loudly at the symex_step default,
  // like any other unsupported instruction in a cross-version binary.
  LOOP_INVARIANT = 21 // loop invariant
} goto_program_instruction_typet;
 
std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);

class goto_programt
{
public:
  inline goto_programt(const goto_programt &src)
  {
    // CBMC didn't permit copy-construction, instead requiring calling
    // copy_from instead. While explicit is better than implicit though,
    // the only implication of allowing this is the occasional performance
    // loss, which is best identified by a profiler.
    copy_from(src);
    update();
  }

  inline goto_programt &operator=(const goto_programt &src)
  {
    // DO NOT COPY ME! I HAVE POINTERS IN ME!
    instructions.clear();
    copy_from(src);
    update();
    return *this;
  }
 
  bool hide;

  class instructiont
  {
  public:
    expr2tc code;

    irep_idt function;

    locationt location;

    goto_program_instruction_typet type;

    expr2tc guard;

    struct loop_contract_datat
    {
      std::list<expr2tc> invariants;
      std::list<expr2tc> assigns_targets; // for frame rule enforcement
    };
    std::unique_ptr<loop_contract_datat> loop_contract_data;
 
    loop_contract_datat &loop_contract_payload()
    {
      if (!loop_contract_data)
        loop_contract_data = std::make_unique<loop_contract_datat>();
      return *loop_contract_data;
    }

    typedef std::list<class instructiont>::iterator targett;
    typedef std::list<class instructiont>::const_iterator const_targett;
    typedef std::list<targett> targetst;
    typedef std::list<const_targett> const_targetst;
 
    targetst targets;

    targett get_target() const
    {
      assert(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;
 
    // for k-induction
    bool inductive_step_instruction;
 
    bool inductive_assertion;
 
    // Set by optimize_guarded_gotos when "IF !cond GOTO skip; GOTO target" is
    // folded into "IF cond GOTO target". The guard is then the positive source
    // condition, so GOTO-taken means the branch body (original target) IS
    // reached.
    bool flipped_guard;
 
    // Set on the nondet assignments the standalone --loop-invariant-check
    // schema emits in place of a loop. Every claim symex reaches after one of
    // them is checked against the invariant's over-approximation, so a
    // violation there means the invariant is too weak to carry the claim, not
    // that the program can reach the state (issue #7480). A boolean rather
    // than a test on location.comment(): the combined --loop-invariant pass
    // emits "loop invariant havoc (verification branch)", whose downstream
    // claims are *not* abstracted, and that comment is user-visible text
    // rather than an interface.
    bool loop_invariant_havoc;
 
    // Set by convert_switch: decimal strings of all case constants whose
    // target is this GOTO, used by witness waypoint matching.  Contains more
    // than one entry when multiple case labels fall through to the same body.
    std::vector<std::string> switch_case_ids;

    inline bool is_target() const
    {
      return target_number != unsigned(-1);
    }

    inline void clear(goto_program_instruction_typet _type)
    {
      type = _type;
      targets.clear();
      guard = gen_true_expr();
      code = expr2tc();
      loop_contract_data.reset();
      inductive_step_instruction = false;
      inductive_assertion = false;
      flipped_guard = false;
      loop_invariant_havoc = false;
    }
 
    inline void make_goto()
    {
      clear(GOTO);
    }
 
    inline void make_location(const locationt &l)
    {
      clear(LOCATION);
      location = l;
    }
 
    inline void make_return()
    {
      clear(RETURN);
    }
 
    inline void make_function_call(const expr2tc &_code)
    {
      clear(FUNCTION_CALL);
      code = _code;
    }
 
    inline void make_skip()
    {
      clear(SKIP);
    }
 
    inline void make_throw()
    {
      clear(THROW);
    }
 
    inline void make_catch()
    {
      clear(CATCH);
    }
 
    inline void make_assertion(const expr2tc &g)
    {
      clear(ASSERT);
      guard = g;
    }
 
    inline void make_assumption(const expr2tc &g)
    {
      clear(ASSUME);
      guard = g;
    }
 
    inline void make_assignment()
    {
      clear(ASSIGN);
    }
 
    inline void make_other()
    {
      clear(OTHER);
    }
 
    inline void make_decl()
    {
      clear(DECL);
    }
 
    inline void make_dead()
    {
      clear(DEAD);
    }
 
    inline void make_atomic_begin()
    {
      clear(ATOMIC_BEGIN);
    }
 
    inline void make_atomic_end()
    {
      clear(ATOMIC_END);
    }
 
    inline void make_goto(targett _target)
    {
      make_goto();
      targets.push_back(_target);
    }
 
    inline void make_goto(targett _target, const expr2tc &g)
    {
      make_goto(_target);
      guard = g;
    }
 
    inline bool is_goto() const
    {
      return type == GOTO;
    }
 
    inline bool is_return() const
    {
      return type == RETURN;
    }
 
    inline bool is_assign() const
    {
      return type == ASSIGN;
    }
 
    inline bool is_function_call() const
    {
      return type == FUNCTION_CALL;
    }
 
    inline bool is_throw() const
    {
      return type == THROW;
    }
 
    inline bool is_catch() const
    {
      return type == CATCH;
    }
 
    inline bool is_skip() const
    {
      return type == SKIP;
    }
 
    inline bool is_location() const
    {
      return type == LOCATION;
    }
 
    inline bool is_other() const
    {
      return type == OTHER;
    }
 
    inline bool is_decl() const
    {
      return type == DECL;
    }
 
    inline bool is_assume() const
    {
      return type == ASSUME;
    }
 
    inline bool is_assert() const
    {
      return type == ASSERT;
    }
 
    inline bool is_loop_invariant() const
    {
      return type == LOOP_INVARIANT;
    }
 
    inline bool is_atomic_begin() const
    {
      return type == ATOMIC_BEGIN;
    }
 
    inline bool is_atomic_end() const
    {
      return type == ATOMIC_END;
    }
 
    inline bool is_end_function() const
    {
      return type == END_FUNCTION;
    }
 
    inline instructiont()
      : location(static_cast<const locationt &>(get_nil_irep())),
        type(NO_INSTRUCTION_TYPE),
        inductive_step_instruction(false),
        inductive_assertion(false),
        flipped_guard(false),
        loop_invariant_havoc(false),
        location_number(0),
        loop_number(unsigned(0)),
        pragma_unroll_count(0),
        target_number(unsigned(-1))
    {
      guard = gen_true_expr();
    }
 
    inline instructiont(goto_program_instruction_typet _type)
      : location(static_cast<const locationt &>(get_nil_irep())),
        type(_type),
        inductive_step_instruction(false),
        inductive_assertion(false),
        flipped_guard(false),
        loop_invariant_havoc(false),
        location_number(0),
        loop_number(unsigned(0)),
        pragma_unroll_count(0),
        target_number(unsigned(-1))
    {
      guard = gen_true_expr();
    }
 
    instructiont(const instructiont &other)
      : code(other.code),
        function(other.function),
        location(other.location),
        type(other.type),
        guard(other.guard),
        // Deep-copy the loop-contract payload. Without this, copying a
        // LOOP_INVARIANT instruction silently drops its invariants and
        // assigns-clause targets.
        loop_contract_data(
          other.loop_contract_data
            ? std::make_unique<loop_contract_datat>(*other.loop_contract_data)
            : nullptr),
        targets(other.targets),
        labels(other.labels),
        inductive_step_instruction(other.inductive_step_instruction),
        inductive_assertion(other.inductive_assertion),
        flipped_guard(other.flipped_guard),
        loop_invariant_havoc(other.loop_invariant_havoc),
        switch_case_ids(other.switch_case_ids),
        location_number(other.location_number),
        loop_number(other.loop_number),
        pragma_unroll_count(other.pragma_unroll_count),
        target_number(other.target_number),
        scope_id(other.scope_id),
        parent_scope_id(other.parent_scope_id)
    {
    }
 
    instructiont &operator=(const instructiont &other)
    {
      instructiont(other).swap(*this);
      return *this;
    }
 
    instructiont(instructiont &&other)
      : code(std::move(other.code)),
        function(std::move(other.function)),
        location(std::move(other.location)),
        type(other.type),
        guard(std::move(other.guard)),
        // Move the loop-contract payload — same reasoning as the copy
        // ctor; without this, move-constructing a LOOP_INVARIANT
        // instruction loses its invariants.
        loop_contract_data(std::move(other.loop_contract_data)),
        targets(std::move(other.targets)),
        labels(std::move(other.labels)),
        inductive_step_instruction(other.inductive_step_instruction),
        inductive_assertion(other.inductive_assertion),
        flipped_guard(other.flipped_guard),
        loop_invariant_havoc(other.loop_invariant_havoc),
        switch_case_ids(std::move(other.switch_case_ids)),
        location_number(other.location_number),
        loop_number(other.loop_number),
        pragma_unroll_count(other.pragma_unroll_count),
        target_number(other.target_number),
        scope_id(other.scope_id),
        parent_scope_id(other.parent_scope_id)
    {
    }
 
    instructiont &operator=(instructiont &&other)
    {
      swap(other);
      return *this;
    }

    void swap(instructiont &instruction)
    {
      if (this == &instruction)
        return;
 
      instruction.code.swap(code);
      instruction.location.swap(location);
      std::swap(instruction.type, type);
      instruction.guard.swap(guard);
      instruction.targets.swap(targets);
      // Swap the labels too — copy-assign goes through
      // `instructiont(other).swap(*this)`, so without swapping
      // labels here the assignment preserves the LHS's labels
      // instead of taking the RHS's.
      instruction.labels.swap(labels);
      loop_contract_data.swap(instruction.loop_contract_data);
      instruction.function.swap(function);
      std::swap(
        inductive_step_instruction, instruction.inductive_step_instruction);
      std::swap(inductive_assertion, instruction.inductive_assertion);
      std::swap(flipped_guard, instruction.flipped_guard);
      std::swap(loop_invariant_havoc, instruction.loop_invariant_havoc);
      instruction.switch_case_ids.swap(switch_case_ids);
      // Swap location_number too — same copy-assign-through-swap
      // reasoning as for labels.
      std::swap(instruction.location_number, location_number);
      std::swap(instruction.loop_number, loop_number);
      std::swap(instruction.pragma_unroll_count, pragma_unroll_count);
      std::swap(target_number, instruction.target_number);
      std::swap(scope_id, instruction.scope_id);
      std::swap(parent_scope_id, instruction.parent_scope_id);
    }
 
    void add_loop_invariant(const expr2tc &invariant)
    {
      assert(is_loop_invariant());
      loop_contract_payload().invariants.push_back(invariant);
    }
    std::list<expr2tc> get_loop_invariants() const
    {
      return loop_contract_data ? loop_contract_data->invariants
                                : std::list<expr2tc>{};
    }
 
    void add_loop_assigns_target(const expr2tc &target)
    {
      assert(is_loop_invariant());
      loop_contract_payload().assigns_targets.push_back(target);
    }
    std::list<expr2tc> get_loop_assigns_targets() const
    {
      return loop_contract_data ? loop_contract_data->assigns_targets
                                : std::list<expr2tc>{};
    }

    unsigned location_number;

    unsigned loop_number;

    unsigned pragma_unroll_count;

    unsigned target_number;

    unsigned int scope_id = 0;

    unsigned int parent_scope_id = 0;

    bool is_backwards_goto() const
    {
      if (!is_goto())
        return false;
 
      for (auto target : targets)
        if (target->location_number <= location_number)
          return true;
 
      return false;
    }
 
    bool operator<(const class instructiont i1) const
    {
      if (function < i1.function)
        return true;
 
      if (location_number < i1.location_number)
        return true;
 
      return false;
    }
 
    void dump() const;
 
    void output_instruction(
      const class namespacet &ns,
      const irep_idt &identifier,
      std::ostream &out,
      bool show_location = true) const;
  };
 
  typedef std::list<class instructiont> instructionst;
 
  typedef instructionst::iterator targett;
  typedef instructionst::const_iterator const_targett;
  typedef std::list<targett> targetst;
  typedef std::list<const_targett> const_targetst;

  instructionst instructions;
 
  void get_successors(const_targett target, const_targetst &successors) const;

  void insert_swap(targett target)
  {
    assert(target != instructions.end());
    const auto next = std::next(target);
    instructions.insert(next, instructiont())->swap(*target);
  }

  void insert_swap(targett target, instructiont &instruction)
  {
    insert_swap(target);
    target->swap(instruction);
  }

  void insert_swap(targett target, goto_programt &p)
  {
    assert(target != instructions.end());
    if (p.instructions.empty())
      return;
    insert_swap(target, p.instructions.front());
    auto next = std::next(target);
    p.instructions.erase(p.instructions.begin());
    instructions.splice(next, p.instructions);
  }

  inline targett insert(targett target)
  {
    return instructions.insert(target, instructiont());
  }

  inline void destructive_append(goto_programt &p)
  {
    instructions.splice(instructions.end(), p.instructions);
  }

  inline void destructive_insert(targett target, goto_programt &p)
  {
    instructions.splice(target, p.instructions);
  }

  inline targett add_instruction()
  {
    instructions.emplace_back();
    targett tmp = instructions.end();
    return --tmp;
  }

  inline targett add_instruction(instructiont &instruction)
  {
    instructions.emplace_back(instruction);
    targett tmp = instructions.end();
    return --tmp;
  }

  inline targett add_instruction(goto_program_instruction_typet type)
  {
    instructions.emplace_back(type);
    targett tmp = instructions.end();
    return --tmp;
  }

  void dump() const;

  std::ostream &output(
    const namespacet &ns,
    const irep_idt &identifier,
    std::ostream &out) const;

  void
  update_instructions_function(const irep_idt &function_id, bool force = false)
  {
    for (auto &instruction : instructions)
    {
      if (force || instruction.function.empty())
      {
        instruction.function = function_id;
      }
    }
  }

  void compute_target_numbers();

  void compute_location_numbers(unsigned &nr)
  {
    for (auto &instruction : instructions)
      instruction.location_number = nr++;
  }

  inline void compute_location_numbers()
  {
    unsigned nr = 0;
    compute_location_numbers(nr);
  }

  void compute_loop_numbers(unsigned int &num);

  void update();

  inline bool empty() const
  {
    return instructions.empty();
  }

  goto_programt() : hide(false)
  {
  }
  virtual ~goto_programt() = default;

  inline void swap(goto_programt &program)
  {
    program.instructions.swap(instructions);
  }

  inline void clear()
  {
    instructions.clear();
  }

  void copy_from(const goto_programt &src);
 
  typedef std::set<irep_idt> decl_identifierst;
  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
};
 
bool operator<(
  const goto_programt::const_targett i1,
  const goto_programt::const_targett i2);
 
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);
  }
};
 
#endif