ExecutionState.h

Go to the documentation of this file.

//===-- ExecutionState.h ----------------------------------------*- C++ -*-===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
 
#ifndef KLEE_EXECUTIONSTATE_H
#define KLEE_EXECUTIONSTATE_H
 
#include "AddressSpace.h"
#include "MergeHandler.h"
 
#include "klee/ADT/ImmutableSet.h"
#include "klee/ADT/TreeStream.h"
#include "klee/Expr/Constraints.h"
#include "klee/Expr/Expr.h"
#include "klee/Module/KInstIterator.h"
#include "klee/Solver/Solver.h"
#include "klee/System/Time.h"
 
#include <map>
#include <memory>
#include <set>
#include <vector>
 
namespace klee {
class Array;
class CallPathNode;
struct Cell;
struct KFunction;
struct KInstruction;
class MemoryObject;
class PTreeNode;
struct InstructionInfo;
 
llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
 
struct StackFrame {
  KInstIterator caller;
  KFunction *kf;
  CallPathNode *callPathNode;
 
  std::vector<const MemoryObject *> allocas;
  Cell *locals;
 
  unsigned minDistToUncoveredOnReturn;
 
  // For vararg functions: arguments not passed via parameter are
  // stored (packed tightly) in a local (alloca) memory object. This
  // is set up to match the way the front-end generates vaarg code (it
  // does not pass vaarg through as expected). VACopy is lowered inside
  // of intrinsic lowering.
  MemoryObject *varargs;
 
  StackFrame(KInstIterator caller, KFunction *kf);
  StackFrame(const StackFrame &s);
  ~StackFrame();
};
 
class UnwindingInformation {
public:
  enum class Kind {
    SearchPhase, // first phase
    CleanupPhase // second phase
  };
 
private:
  const Kind kind;
 
public:
  // _Unwind_Exception* of the thrown exception, used in both phases
  ref<ConstantExpr> exceptionObject;
 
  Kind getKind() const { return kind; }
 
  explicit UnwindingInformation(ref<ConstantExpr> exceptionObject, Kind k)
      : kind(k), exceptionObject(exceptionObject) {}
  virtual ~UnwindingInformation() = default;
 
  virtual std::unique_ptr<UnwindingInformation> clone() const = 0;
};
 
struct SearchPhaseUnwindingInformation : public UnwindingInformation {
  // Keeps track of the stack index we have so far unwound to.
  std::size_t unwindingProgress;
 
  // MemoryObject that contains a serialized version of the last executed
  // landingpad, so we can clean it up after the personality fn returns.
  MemoryObject *serializedLandingpad = nullptr;
 
  SearchPhaseUnwindingInformation(ref<ConstantExpr> exceptionObject,
                                  std::size_t const unwindingProgress)
      : UnwindingInformation(exceptionObject,
                             UnwindingInformation::Kind::SearchPhase),
        unwindingProgress(unwindingProgress) {}
 
  std::unique_ptr<UnwindingInformation> clone() const {
    return std::make_unique<SearchPhaseUnwindingInformation>(*this);
  }
 
  static bool classof(const UnwindingInformation *u) {
    return u->getKind() == UnwindingInformation::Kind::SearchPhase;
  }
};
 
struct CleanupPhaseUnwindingInformation : public UnwindingInformation {
  // Phase 1 will try to find a catching landingpad.
  // Phase 2 will unwind up to this landingpad or return from
  // _Unwind_RaiseException if none was found.
 
  // The selector value of the catching landingpad that was found
  // during the search phase.
  ref<ConstantExpr> selectorValue;
 
  // Used to know when we have to stop unwinding and to
  // ensure that unwinding stops at the frame for which
  // we first found a handler in the search phase.
  const std::size_t catchingStackIndex;
 
  CleanupPhaseUnwindingInformation(ref<ConstantExpr> exceptionObject,
                                   ref<ConstantExpr> selectorValue,
                                   const std::size_t catchingStackIndex)
      : UnwindingInformation(exceptionObject,
                             UnwindingInformation::Kind::CleanupPhase),
        selectorValue(selectorValue),
        catchingStackIndex(catchingStackIndex) {}
 
  std::unique_ptr<UnwindingInformation> clone() const {
    return std::make_unique<CleanupPhaseUnwindingInformation>(*this);
  }
 
  static bool classof(const UnwindingInformation *u) {
    return u->getKind() == UnwindingInformation::Kind::CleanupPhase;
  }
};
 
class ExecutionState {
#ifdef KLEE_UNITTEST
public:
#else
private:
#endif
  // copy ctor
  ExecutionState(const ExecutionState &state);
 
public:
  using stack_ty = std::vector<StackFrame>;
 
  // Execution - Control Flow specific
 
  KInstIterator pc;
 
  KInstIterator prevPC;
 
  stack_ty stack;
 
  std::uint32_t incomingBBIndex;
 
  // Overall state of the state - Data specific
 
  std::uint32_t depth = 0;
 
  AddressSpace addressSpace;
 
  ConstraintSet constraints;
 
 
  mutable SolverQueryMetaData queryMetaData;
 
  TreeOStream pathOS;
 
  TreeOStream symPathOS;
 
  std::map<const std::string *, std::set<std::uint32_t>> coveredLines;
 
  PTreeNode *ptreeNode = nullptr;
 
  //
  // FIXME: Move to a shared list structure (not critical).
  std::vector<std::pair<ref<const MemoryObject>, const Array *>> symbolics;
 
  ImmutableSet<ref<Expr>> cexPreferences;
 
  std::set<std::string> arrayNames;
 
  std::vector<ref<MergeHandler>> openMergeStack;
 
  std::uint64_t steppedInstructions = 0;
 
  std::uint32_t instsSinceCovNew = 0;
 
  std::unique_ptr<UnwindingInformation> unwindingInformation;
 
  static std::uint32_t nextID;
 
  std::uint32_t id = 0;
 
  bool coveredNew = false;
 
  bool forkDisabled = false;
 
public:
#ifdef KLEE_UNITTEST
  // provide this function only in the context of unittests
  ExecutionState() = default;
#endif
  // only to create the initial state
  explicit ExecutionState(KFunction *kf);
  // no copy assignment, use copy constructor
  ExecutionState &operator=(const ExecutionState &) = delete;
  // no move ctor
  ExecutionState(ExecutionState &&) noexcept = delete;
  // no move assignment
  ExecutionState& operator=(ExecutionState &&) noexcept = delete;
  // dtor
  ~ExecutionState();
 
  ExecutionState *branch();
 
  void pushFrame(KInstIterator caller, KFunction *kf);
  void popFrame();
 
  void addSymbolic(const MemoryObject *mo, const Array *array);
 
  void addConstraint(ref<Expr> e);
  void addCexPreference(const ref<Expr> &cond);
 
  bool merge(const ExecutionState &b);
  void dumpStack(llvm::raw_ostream &out) const;
 
  std::uint32_t getID() const { return id; };
  void setID() { id = nextID++; };
};
 
struct ExecutionStateIDCompare {
  bool operator()(const ExecutionState *a, const ExecutionState *b) const {
    return a->getID() < b->getID();
  }
};
}
 
#endif /* KLEE_EXECUTIONSTATE_H */