symex_target_equation.h

Go to the documentation of this file.

#ifndef CPROVER_BASIC_SYMEX_EQUATION_H
#define CPROVER_BASIC_SYMEX_EQUATION_H
 
#include <cstdint>
#include <cstdio>
#include <cstring>
#include <goto-programs/goto_program.h>
#include <goto-symex/equation/symex_target.h>
#include <list>
#include <map>
#include <memory>
#include <util/config/config.h>
#include <irep2/irep2.h>
#include <util/symtab/namespace.h>
#include <util/base/threeval.h>
#include <vector>
 
class smt_convt;
 
class symex_target_equationt : public symex_targett
{
public:
  class SSA_stept;
 
  symex_target_equationt(const namespacet &_ns) : ns(_ns), output_count(0)
  {
    debug_print = config.options.get_bool_option("symex-ssa-trace");
    ssa_trace = config.options.get_bool_option("ssa-trace");
    ssa_smt_trace = config.options.get_bool_option("ssa-smt-trace");
  }
 
  // assignment to a variable - lhs must be a symbol
  void assignment(
    const expr2tc &guard,
    const expr2tc &lhs,
    const expr2tc &original_lhs,
    const expr2tc &rhs,
    const expr2tc &original_rhs,
    const sourcet &source,
    std::vector<stack_framet> stack_trace,
    const bool hidden,
    unsigned loop_number) override;
 
  // output
  void output(
    const expr2tc &guard,
    const sourcet &source,
    const std::string &fmt,
    const std::list<expr2tc> &args) override;
 
  void branching(
    const expr2tc &guard,
    const expr2tc &cond,
    const sourcet &source,
    const bool hidden,
    unsigned loop_number) override;
 
  // record an assumption
  void assumption(
    const expr2tc &guard,
    const expr2tc &cond,
    const sourcet &source,
    unsigned loop_number) override;
 
  // record an assertion
  void assertion(
    const expr2tc &guard,
    const expr2tc &cond,
    const expr2tc &cond_neg,
    const std::string &msg,
    std::vector<stack_framet> stack_trace,
    const sourcet &source,
    unsigned loop_number) override;
 
  void renumber(
    const expr2tc &guard,
    const expr2tc &symbol,
    const expr2tc &size,
    const sourcet &source) override;
 
  // `runtime_encoded_equationt` overrides `convert` and supports only the
  // default mode; incremental BMC callers must run probes through the
  // non-incremental path.
  enum class assertion_modet
  {
    Violated,
    PathReachable,
    Satisfiable
  };
 
  virtual void convert(
    smt_convt &smt_conv,
    assertion_modet mode = assertion_modet::Violated);
 
  void reconstruct_symbolic_expression(expr2tc &expr, bool keep_local_variables)
    const override;
  void replace_rec(const SSA_stept &step, expr2tc &e, bool keep_local) const;
 
  class SSA_stept
  {
  public:
    sourcet source;
    symex_targett::step_typet type;
 
    bool is_assert() const
    {
      return type == symex_targett::ASSERT;
    }
    bool is_assume() const
    {
      return type == symex_targett::ASSUME;
    }
    bool is_assignment() const
    {
      return type == symex_targett::ASSIGNMENT;
    }
    bool is_output() const
    {
      return type == symex_targett::OUTPUT;
    }
    bool is_renumber() const
    {
      return type == symex_targett::RENUMBER;
    }
    bool is_skip() const
    {
      return type == symex_targett::SKIP;
    }
    bool is_branching() const
    {
      return type == symex_targett::BREANCHING;
    }
 
    expr2tc guard;
 
    // for ASSIGNMENT; RENUMBER reuses lhs = symbol, rhs = new size
    expr2tc lhs, rhs;
    expr2tc original_lhs, original_rhs;
 
    // cond: assume/assert condition, assignment equality, or branch guard.
    // comment interned: assertion messages are a small, highly repetitive
    // set ("dereference failure", "array bounds violated", ...), so
    // irep_idt both shrinks the inline footprint (4 bytes vs a 32-byte
    // std::string) and dedups the payload across the many steps that share
    // a message.
    expr2tc cond;
    expr2tc cond_neg;
    irep_idt comment;
 
    // OUTPUT-step payload. OUTPUT steps are rare (only printf-family
    // side effects produce them), so the format string and argument
    // lists live in a lazily-allocated side struct rather than inline
    // on every SSA step. This keeps sizeof(SSA_stept) ~80 bytes smaller
    // on the assignment/assume/assert steps that dominate large
    // equations. Access through the output_* helpers below.
    struct output_datat
    {
      std::string format_string;
      std::list<expr2tc> output_args;
      std::list<expr2tc> converted_output_args; // filled during conversion
    };
    std::unique_ptr<output_datat> output_data;
 
    // One stack trace recorded per function activation record, in reverse
    // order (most recent in idx 0). Only assignment and assert steps ever
    // populate it, so — like output_data — it lives in a lazily-allocated
    // side vector rather than costing 24 bytes inline on the assume/branch/
    // renumber/output steps that never use it. Read through stack_trace(),
    // write through stack_trace_payload().
    std::unique_ptr<std::vector<stack_framet>> stack_trace_box;
 
    // Discharged assertion expression used for counterexample trace queries.
    // Conversion sets it to the discharged claim for asserts and to true
    // for ignored steps and other non-assume steps; it stays nil for
    // non-ignored assumes and before conversion.
    expr2tc cond_expr;
 
    // for slicing
    bool ignore;
 
    // for visibility
    bool hidden;
 
    // for bidirectional search
    unsigned loop_number;
 
    SSA_stept() : ignore(false), hidden(false)
    {
    }
 
    // SSA_stept is copied wholesale (e.g. the per-claim local_eq in
    // bmc.cpp), so the unique_ptr payload needs deep-copy semantics.
    // Moves stay default (cheap pointer steal).
    SSA_stept(const SSA_stept &o)
      : source(o.source),
        type(o.type),
        guard(o.guard),
        lhs(o.lhs),
        rhs(o.rhs),
        original_lhs(o.original_lhs),
        original_rhs(o.original_rhs),
        cond(o.cond),
        cond_neg(o.cond_neg),
        comment(o.comment),
        output_data(
          o.output_data ? std::make_unique<output_datat>(*o.output_data)
                        : nullptr),
        stack_trace_box(
          o.stack_trace_box
            ? std::make_unique<std::vector<stack_framet>>(*o.stack_trace_box)
            : nullptr),
        cond_expr(o.cond_expr),
        ignore(o.ignore),
        hidden(o.hidden),
        loop_number(o.loop_number)
    {
    }
    SSA_stept &operator=(const SSA_stept &o)
    {
      if (this != &o)
        *this = SSA_stept(o); // copy-and-move
      return *this;
    }
    SSA_stept(SSA_stept &&) = default;
    SSA_stept &operator=(SSA_stept &&) = default;
 
    output_datat &output_payload()
    {
      if (!output_data)
        output_data = std::make_unique<output_datat>();
      return *output_data;
    }
 
    // Read-only view of the stack trace; empty when none was recorded.
    const std::vector<stack_framet> &stack_trace() const
    {
      static const std::vector<stack_framet> empty;
      return stack_trace_box ? *stack_trace_box : empty;
    }
 
    std::vector<stack_framet> &stack_trace_payload()
    {
      if (!stack_trace_box)
        stack_trace_box = std::make_unique<std::vector<stack_framet>>();
      return *stack_trace_box;
    }
 
    void output(const namespacet &ns, std::ostream &out) const;
    void short_output(
      const namespacet &ns,
      std::ostream &out,
      bool show_ignored = false) const;
    void dump() const;
  };
 
  unsigned count_ignored_SSA_steps() const
  {
    unsigned i = 0;
    for (const auto &SSA_step : SSA_steps)
      if (SSA_step.ignore)
        i++;
    return i;
  }
 
  typedef std::list<SSA_stept> SSA_stepst;
  SSA_stepst SSA_steps;
 
  SSA_stepst::iterator get_SSA_step(unsigned s)
  {
    SSA_stepst::iterator it = SSA_steps.begin();
    for (; s != 0; s--)
    {
      assert(it != SSA_steps.end());
      it++;
    }
    return it;
  }
 
  void output(std::ostream &out) const;
  void short_output(std::ostream &out, bool show_ignored = false) const;

  bool check_for_duplicate_assigns() const;
 
  void clear()
  {
    SSA_steps.clear();
    output_count = 0;
  }
 
  unsigned int clear_assertions();
 
  std::shared_ptr<symex_targett> clone() const override
  {
    // SSA_stept's copy constructor deep-copies its unique_ptr payloads, so
    // plain member-wise duplication is safe.
    return std::shared_ptr<symex_targett>(new symex_target_equationt(*this));
  }
 
  void push_ctx() override;
  void pop_ctx() override;
 
protected:
  const namespacet &ns;
 
  bool debug_print;
  bool ssa_trace;
  bool ssa_smt_trace;
  unsigned output_count;
 
private:
  void debug_print_step(const SSA_stept &step) const;
};
 
class runtime_encoded_equationt : public symex_target_equationt
{
public:
  class dual_unsat_exception
  {
  };
 
  runtime_encoded_equationt(const namespacet &_ns, smt_convt &conv);
  ~runtime_encoded_equationt() override;
 
  void push_ctx() override;
  void pop_ctx() override;
 
  std::shared_ptr<symex_targett> clone() const override;
 
  void convert(
    smt_convt &smt_conv,
    assertion_modet mode = assertion_modet::Violated) override;
  void flush_latest_instructions();
 
  tvt ask_solver_question(const expr2tc &question);
 
  smt_convt &conv;
  struct solver_statet;
  std::unique_ptr<solver_statet> solver_state;
  std::list<SSA_stepst::iterator> scoped_end_points;
  SSA_stepst::iterator cvt_progress;
};
 
extern inline bool operator<(
  const symex_target_equationt::SSA_stepst::const_iterator a,
  const symex_target_equationt::SSA_stepst::const_iterator b)
{
  return &(*a) < &(*b);
}
 
std::ostream &
operator<<(std::ostream &out, const symex_target_equationt::SSA_stept &step);
std::ostream &
operator<<(std::ostream &out, const symex_target_equationt &equation);
 
#endif