about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/klee/ExecutionState.h107
-rw-r--r--include/klee/Internal/Module/KInstruction.h2
-rw-r--r--include/klee/Internal/Module/KModule.h2
-rw-r--r--include/klee/Internal/Support/PrintVersion.h17
-rw-r--r--include/klee/Internal/System/Time.h9
-rw-r--r--include/klee/klee.h78
-rw-r--r--include/klee/util/ExprSMTLIBPrinter.h1
7 files changed, 144 insertions, 72 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 97b700c1..32f840f6 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -23,14 +23,14 @@
 #include <vector>
 
 namespace klee {
-  class Array;
-  class CallPathNode;
-  struct Cell;
-  struct KFunction;
-  struct KInstruction;
-  class MemoryObject;
-  class PTreeNode;
-  struct InstructionInfo;
+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);
 
@@ -39,7 +39,7 @@ struct StackFrame {
   KFunction *kf;
   CallPathNode *callPathNode;
 
-  std::vector<const MemoryObject*> allocas;
+  std::vector<const MemoryObject *> allocas;
   Cell *locals;
 
   /// Minimum distance to an uncovered instruction once the function
@@ -61,56 +61,92 @@ struct StackFrame {
   ~StackFrame();
 };
 
+/// @brief ExecutionState representing a path under exploration
 class ExecutionState {
 public:
   typedef std::vector<StackFrame> stack_ty;
 
 private:
   // unsupported, use copy constructor
-  ExecutionState &operator=(const ExecutionState&); 
-  std::map< std::string, std::string > fnAliases;
+  ExecutionState &operator=(const ExecutionState &);
+
+  std::map<std::string, std::string> fnAliases;
 
 public:
-  bool fakeState;
-  unsigned depth;
-  
-  // pc - pointer to current instruction stream
-  KInstIterator pc, prevPC;
+  // Execution - Control Flow specific
+
+  /// @brief Pointer to instruction to be executed after the current
+  /// instruction
+  KInstIterator pc;
+
+  /// @brief Pointer to instruction which is currently executed
+  KInstIterator prevPC;
+
+  /// @brief Stack representing the current instruction stream
   stack_ty stack;
+
+  /// @brief Remember from which Basic Block control flow arrived
+  /// (i.e. to select the right phi values)
+  unsigned incomingBBIndex;
+
+  // Overall state of the state - Data specific
+
+  /// @brief Address space used by this state (e.g. Global and Heap)
+  AddressSpace addressSpace;
+
+  /// @brief Constraints collected so far
   ConstraintManager constraints;
+
+  /// Statistics and information
+
+  /// @brief Costs for all queries issued for this state, in seconds
   mutable double queryCost;
+
+  /// @brief Weight assigned for importance of this state.  Can be
+  /// used for searchers to decide what paths to explore
   double weight;
-  AddressSpace addressSpace;
-  TreeOStream pathOS, symPathOS;
+
+  /// @brief Exploration depth, i.e., number of times KLEE branched for this state
+  unsigned depth;
+
+  /// @brief History of complete path: represents branches taken to
+  /// reach/create this state (both concrete and symbolic)
+  TreeOStream pathOS;
+
+  /// @brief History of symbolic path: represents symbolic branches
+  /// taken to reach/create this state
+  TreeOStream symPathOS;
+
+  /// @brief Counts how many instructions were executed since the last new
+  /// instruction was covered.
   unsigned instsSinceCovNew;
+
+  /// @brief Whether a new instruction was covered in this state
   bool coveredNew;
 
-  /// Disables forking, set by user code.
+  /// @brief Disables forking for this state. Set by user code
   bool forkDisabled;
 
-  std::map<const std::string*, std::set<unsigned> > coveredLines;
+  /// @brief Set containing which lines in which files are covered by this state
+  std::map<const std::string *, std::set<unsigned> > coveredLines;
+
+  /// @brief Pointer to the process tree of the current state
   PTreeNode *ptreeNode;
 
-  /// ordered list of symbolics: used to generate test cases. 
+  /// @brief Ordered list of symbolics: used to generate test cases.
   //
   // FIXME: Move to a shared list structure (not critical).
-  std::vector< std::pair<const MemoryObject*, const Array*> > symbolics;
+  std::vector<std::pair<const MemoryObject *, const Array *> > symbolics;
 
-  /// Set of used array names.  Used to avoid collisions.
+  /// @brief Set of used array names for this state.  Used to avoid collisions.
   std::set<std::string> arrayNames;
 
-  // Used by the checkpoint/rollback methods for fake objects.
-  // FIXME: not freeing things on branch deletion.
-  MemoryMap shadowObjects;
-
-  unsigned incomingBBIndex;
-
   std::string getFnAlias(std::string fn);
   void addFnAlias(std::string old_fn, std::string new_fn);
   void removeFnAlias(std::string fn);
-  
+
 private:
-  ExecutionState() : fakeState(false), ptreeNode(0) {}
+  ExecutionState() : ptreeNode(0) {}
 
 public:
   ExecutionState(KFunction *kf);
@@ -119,24 +155,21 @@ public:
   // use on structure
   ExecutionState(const std::vector<ref<Expr> > &assumptions);
 
-  ExecutionState(const ExecutionState& state);
+  ExecutionState(const ExecutionState &state);
 
   ~ExecutionState();
-  
+
   ExecutionState *branch();
 
   void pushFrame(KInstIterator caller, KFunction *kf);
   void popFrame();
 
   void addSymbolic(const MemoryObject *mo, const Array *array);
-  void addConstraint(ref<Expr> e) { 
-    constraints.addConstraint(e); 
-  }
+  void addConstraint(ref<Expr> e) { constraints.addConstraint(e); }
 
   bool merge(const ExecutionState &b);
   void dumpStack(llvm::raw_ostream &out) const;
 };
-
 }
 
 #endif
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index fc86070b..62f514ff 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -50,7 +50,7 @@ namespace klee {
     std::vector< std::pair<unsigned, uint64_t> > indices;
 
     /// offset - A constant offset to add to the pointer operand to execute the
-    /// insturction.
+    /// instruction.
     uint64_t offset;
   };
 }
diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h
index 80672b5e..76db4694 100644
--- a/include/klee/Internal/Module/KModule.h
+++ b/include/klee/Internal/Module/KModule.h
@@ -92,7 +92,7 @@ namespace klee {
 #endif
     
     // Some useful functions to know the address of
-    llvm::Function *dbgStopPointFn, *kleeMergeFn;
+    llvm::Function *kleeMergeFn;
 
     // Our shadow versions of LLVM structures.
     std::vector<KFunction*> functions;
diff --git a/include/klee/Internal/Support/PrintVersion.h b/include/klee/Internal/Support/PrintVersion.h
new file mode 100644
index 00000000..2c375ad2
--- /dev/null
+++ b/include/klee/Internal/Support/PrintVersion.h
@@ -0,0 +1,17 @@
+//===-- Version.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_PRINT_VERSION_H
+#define KLEE_PRINT_VERSION_H
+
+namespace klee {
+  void printVersion();
+}
+
+#endif
diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
index 5229c8c9..14d23536 100644
--- a/include/klee/Internal/System/Time.h
+++ b/include/klee/Internal/System/Time.h
@@ -10,10 +10,19 @@
 #ifndef KLEE_UTIL_TIME_H
 #define KLEE_UTIL_TIME_H
 
+#include <llvm/Support/TimeValue.h>
+
 namespace klee {
   namespace util {
+
+    /// Seconds spent by this process in user mode.
     double getUserTime();
+
+    /// Wall time in seconds.
     double getWallTime();
+
+    /// Wall time as TimeValue object.
+    llvm::sys::TimeValue getWallTimeVal();
   }
 }
 
diff --git a/include/klee/klee.h b/include/klee/klee.h
index ce92ba37..d0980395 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -1,11 +1,11 @@
-//===-- klee.h --------------------------------------------------*- C++ -*-===//
+/*===-- klee.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_H__
 #define __KLEE_H__
@@ -18,51 +18,57 @@ extern "C" {
 #endif
   
   /* Add an accesible memory object at a user specified location. It
-     is the users responsibility to make sure that these memory
-     objects do not overlap. These memory objects will also
-     (obviously) not correctly interact with external function
-     calls. */
+   * is the users responsibility to make sure that these memory
+   * objects do not overlap. These memory objects will also
+   * (obviously) not correctly interact with external function
+   * calls.
+   */
   void klee_define_fixed_object(void *addr, size_t nbytes);
 
-  /// klee_make_symbolic - Make the contents of the object pointer to by \arg
-  /// addr symbolic. 
-  ///
-  /// \arg addr - The start of the object.
-  /// \arg nbytes - The number of bytes to make symbolic; currently this *must*
-  /// be the entire contents of the object.
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /* klee_make_symbolic - Make the contents of the object pointer to by \arg
+   * addr symbolic.
+   *
+   * \arg addr - The start of the object.
+   * \arg nbytes - The number of bytes to make symbolic; currently this *must*
+   * be the entire contents of the object.
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
 
-  /// klee_range - Construct a symbolic value in the signed interval
-  /// [begin,end).
-  ///
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /* klee_range - Construct a symbolic value in the signed interval
+   * [begin,end).
+   *
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   int klee_range(int begin, int end, const char *name);
 
-  /// klee_int - Construct an unconstrained symbolic integer.
-  ///
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /*  klee_int - Construct an unconstrained symbolic integer.
+   *
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   int klee_int(const char *name);
 
-  /// klee_silent_exit - Terminate the current KLEE process without generating a
-  /// test file.
+  /* klee_silent_exit - Terminate the current KLEE process without generating a
+   * test file.
+   */
   __attribute__((noreturn))
   void klee_silent_exit(int status);
 
-  /// klee_abort - Abort the current KLEE process.
+  /* klee_abort - Abort the current KLEE process. */
   __attribute__((noreturn))
   void klee_abort(void);  
 
-  /// klee_report_error - Report a user defined error and terminate the current
-  /// KLEE process.
-  ///
-  /// \arg file - The filename to report in the error message.
-  /// \arg line - The line number to report in the error message.
-  /// \arg message - A string to include in the error message.
-  /// \arg suffix - The suffix to use for error files.
+  /* klee_report_error - Report a user defined error and terminate the current
+   * KLEE process.
+   *
+   * \arg file - The filename to report in the error message.
+   * \arg line - The line number to report in the error message.
+   * \arg message - A string to include in the error message.
+   * \arg suffix - The suffix to use for error files.
+   */
   __attribute__((noreturn))
   void klee_report_error(const char *file, 
 			 int line, 
@@ -104,6 +110,7 @@ extern "C" {
   void klee_warning(const char *message);
   void klee_warning_once(const char *message);
   void klee_prefer_cex(void *object, uintptr_t condition);
+  void klee_posix_prefer_cex(void *object, uintptr_t condition);
   void klee_mark_global(void *object);
 
   /* Return a possible constant value for the input expression. This
@@ -142,6 +149,11 @@ extern "C" {
   /* Print stack trace. */
   void klee_stack_trace(void);
 
+  /* Print range for given argument and tagged with name */
+  void klee_print_range(const char * name, int arg );
+
+  /* Merge current states together if possible */
+  void klee_merge();
 #ifdef __cplusplus
 }
 #endif
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h
index 6b0d260a..e90a49f1 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/util/ExprSMTLIBPrinter.h
@@ -319,6 +319,7 @@ protected:
   void printNotEqualExpr(const ref<NeExpr> &e);
   void printSelectExpr(const ref<SelectExpr> &e,
                                ExprSMTLIBPrinter::SMTLIB_SORT s);
+  void printAShrExpr(const ref<AShrExpr> &e);
 
   // For the set of operators that take sort "s" arguments
   void printSortArgsExpr(const ref<Expr> &e,
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 13:50:35 +0000