Commits

arrowdodger committed 564025b

Import r166214, r166277, r166553, r166554, r166555, r166556,
r166563, r166564, r166565, r166568, r166569, r166570,
r166573, r166574, r166581, r166582, r166585:

Nice patch by Hristina Palikareva that removes the dependency on STP
arrays from the Array and UpdateNode classes.

=============================

Added missing header file (part of the last patch).

=============================

Patch by Dan Liew: " Modified ConstantExpr::toString() to take an
optional radix (base e.g. 2,10,16). This will be needed by the
ExprSMTLIBPrinter that will soon be added."

=============================

Patch by Dan Liew: " Added "sys/resource.h" include to POSIX stub
methods. This fixes build problems (at least on my machine glibc
2.16.0-2)

The __priority_which_t and __rlimit_resource_t data types which
functions set_priority(), setrlimit() and setrlimit64() need are not
defined in any of the headers the runtime/POSIX/stubs.c includes.

It appears in the past the "sys/resource.h" was included by
"sys/wait.h" but in the recent version of glibc I am using it is not.
So to fix this I've added the include."

=============================

Patch by Dan Liew: "Moved PrintContext class out of ExprPrinter.cpp so
it can be used by other classes. It has also been improved so it can
be used with the soon to be added ExprSMTLIBPrinter classes."

=============================

Nice patch by Dan Liew that adds support for printing queries in the
SMTLIB format (part of his MSc project work).

=============================

Patch by Dan Liew: "Added -print-smtlib option to kleaver tool that
allows .pc files to be printed as SMT-LIBv2 queries."

=============================

Patch by Dan Liew: "Added SMTLIBLoggingSolver for logging queries in SMT-LIBv2 format."

=============================

Patch by Dan Liew which improves the logging options: "Removed
-use-query-pc-log and -use-stp-query-pc-log and replaced with better
command line option -use-query-log=option. Multiple comma seperated
options can be specified after -use-query-log=. In addition queries
can now be logged in SMT-LIBv2 format as well as KQuery format. The
names of logging files has changed and also KLEE now informs users
which files are being written to.

Because of the changes the test/Feature/ExprLogging.c test broke so it
was necessary to fix it."

=============================

Patch by Dan Liew: "Added support for generating .smt2 files when
writing out test cases (option --write-smt2s) in KLEE."

=============================

Patch by Dan Liew: "Added primitive test that checks kleaver's new
-print-smt option. Improved Feature/ExprLogging.c test:
- Now (primitive) checks the result of -write-smt2s
- Now (primitive) checks the result of -write-pcs
- Now (primitive) checks the result of -write-cvcs"

=============================

Patch by Dan Liew, updating klee-files.html to mention the recently
added SMTLIB options.

=============================

Patch by Dan Liew improving the description of getZExtValue (see discussion at http://keeda.stanford.edu/pipermail/klee-dev/2012-September/000928.html)

=============================

Patch by Jonathan Neuschäfer fixing inconsistency in Tutorial 1.

=============================

Code refactorings by Jonathan Neuschäfer: "move increment into for-loop
head (Just a cosmetic change to make things a bit more readable)" and
"move duplicate code to a function and also remove an old comment that
seems to be obsolete by now. (Another cosmetic change)"

=============================

Two small changes by Jonathan Neuschäfer: one that fixes a memory leak
in an example, and one that removes an already completed TODO item.

=============================

Patch by Jonathan Neuschäfer: "update symbol list for
klee_get_value*. It might be better to just get (most of) the exported
symbols right from the SpecialFunctionHandler class."

  • Participants
  • Parent commits 0c13e90

Comments (0)

Files changed (30)

 
 Build System / Configure / Release Cleanups
 --
- o Rename .bout to .ktest (klee test)
-
  o Rename .pc to .kquery (kleaver query)
 
  o Configure doesn't check for bison / flex, we don't really use these

examples/sort/sort.c

 
   for (unsigned i = 0; i != nelem; ++i)
     assert(temp1[i] == temp2[i]);
+
+  free(temp1);
+  free(temp2);
 }
 
 int main() {

include/klee/Expr.h

   /// native ConstantExpr APIs.
   const llvm::APInt &getAPValue() const { return value; }
 
-  /// getZExtValue - Return the constant value for a limited number of bits.
+  /// getZExtValue - Returns the constant value zero extended to the
+  /// return type of this method.
   ///
-  /// This routine should be used in situations where the width of the constant
-  /// is known to be limited to a certain number of bits.
+  ///\param bits - optional parameter that can be used to check that the
+  ///number of bits used by this constant is <= to the parameter
+  ///value. This is useful for checking that type casts won't truncate
+  ///useful bits.
+  ///
+  /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8);
   uint64_t getZExtValue(unsigned bits = 64) const {
     assert(getWidth() <= bits && "Value may be out of range!");
     return value.getZExtValue();
     return value.getLimitedValue(Limit);
   }
 
-  /// toString - Return the constant value as a decimal string.
-  void toString(std::string &Res) const;
+  /// toString - Return the constant value as a string
+  /// \param Res specifies the string for the result to be placed in
+  /// \param radix specifies the base (e.g. 2,10,16). The default is base 10
+  void toString(std::string &Res, unsigned radix=10) const;
+
+
  
   int compareContents(const Expr &b) const { 
     const ConstantExpr &cb = static_cast<const ConstantExpr&>(b);
 
 /// Class representing a byte update of an array.
 class UpdateNode {
-  friend class UpdateList;
-  friend class STPBuilder; // for setting STPArray
+  friend class UpdateList;  
 
   mutable unsigned refCount;
-  // gross
-  mutable void *stpArray;
   // cache instead of recalc
   unsigned hashValue;
 
   unsigned hash() const { return hashValue; }
 
 private:
-  UpdateNode() : refCount(0), stpArray(0) {}
+  UpdateNode() : refCount(0) {}
   ~UpdateNode();
 
   unsigned computeHash();
 public:
   const std::string name;
   // FIXME: Not 64-bit clean.
-  unsigned size;
+  unsigned size;  
 
   /// constantValues - The constant initial values for this array, or empty for
   /// a symbolic array. If non-empty, this size of this array is equivalent to
   /// the array size.
   const std::vector< ref<ConstantExpr> > constantValues;
-
-  // FIXME: This does not belong here.
-  mutable void *stpInitialArray;
-
+  
 public:
   /// Array - Construct a new array object.
   ///
         const ref<ConstantExpr> *constantValuesBegin = 0,
         const ref<ConstantExpr> *constantValuesEnd = 0)
     : name(_name), size(_size), 
-      constantValues(constantValuesBegin, constantValuesEnd), 
-      stpInitialArray(0) {
+      constantValues(constantValuesBegin, constantValuesEnd) {      
     assert((isSymbolicArray() || constantValues.size() == size) &&
            "Invalid size for constant array!");
+    computeHash();
 #ifndef NDEBUG
     for (const ref<ConstantExpr> *it = constantValuesBegin;
          it != constantValuesEnd; ++it)
 
   Expr::Width getDomain() const { return Expr::Int32; }
   Expr::Width getRange() const { return Expr::Int8; }
+  
+  unsigned computeHash();
+  unsigned hash() const { return hashValue; }
+   
+private:
+  unsigned hashValue;
 };
 
 /// Class representing a complete list of updates into an array.

include/klee/Interpreter.h

         CheckDivZero(_CheckDivZero) {}
   };
 
+  enum LogType
+  {
+	  STP, //.CVC (STP's native language)
+	  KQUERY, //.PC files (kQuery native language)
+	  SMTLIB2 //.SMT2 files (SMTLIB version 2 files)
+  };
+
   /// InterpreterOptions - Options varying the runtime behavior during
   /// interpretation.
   struct InterpreterOptions {
   
   virtual void getConstraintLog(const ExecutionState &state,
                                 std::string &res,
-                                bool asCVC = false) = 0;
+                                LogType logFormat = STP) = 0;
 
   virtual bool getSymbolicSolution(const ExecutionState &state, 
                                    std::vector< 

include/klee/Solver.h

   /// after writing them to the given path in .pc format.
   Solver *createPCLoggingSolver(Solver *s, std::string path);
 
+  /// createSMTLIBLoggingSolver - Create a solver which will forward all queries
+  /// after writing them to the given path in .smt2 format.
+  Solver *createSMTLIBLoggingSolver(Solver *s, std::string path);
+
+
   /// createDummySolver - Create a dummy solver implementation which always
   /// fails.
   Solver *createDummySolver();

include/klee/util/ArrayExprHash.h

+//===-- ArrayExprHash.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 __UTIL_ARRAYEXPRHASH_H__
+#define __UTIL_ARRAYEXPRHASH_H__
+
+#include "klee/Expr.h"
+#include "klee/TimerStatIncrementer.h"
+#include "SolverStats.h"
+
+#include <map>
+#include <tr1/unordered_map>
+
+namespace klee {
+  
+struct ArrayHashFn  {
+  unsigned operator()(const Array* array) const {
+    return(array ? array->hash() : 0);
+  }
+};
+    
+struct ArrayCmpFn {
+  bool operator()(const Array* array1, const Array* array2) const {
+    return(array1 == array2);
+  }
+};  
+  
+struct UpdateNodeHashFn  {
+  unsigned operator()(const UpdateNode* un) const {
+    return(un ? un->hash() : 0);
+  }
+};
+    
+struct UpdateNodeCmpFn {
+  bool operator()(const UpdateNode* un1, const UpdateNode* un2) const {
+    return(un1 == un2);
+  }
+};  
+
+template<class T>
+class ArrayExprHash {  
+public:
+  
+  ArrayExprHash() {};
+  // Note: Extend the class and overload the destructor if the objects of type T
+  // that are to be hashed need to be explicitly destroyed
+  // As an example, see class STPArrayExprHash
+  virtual ~ArrayExprHash() {};
+   
+  bool lookupArrayExpr(const Array* array, T& exp) const;
+  void hashArrayExpr(const Array* array, T& exp);  
+  
+  bool lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const;
+  void hashUpdateNodeExpr(const UpdateNode* un, T& exp);  
+  
+protected:
+  typedef std::tr1::unordered_map<const Array*, T, ArrayHashFn, ArrayCmpFn> ArrayHash;
+  typedef typename ArrayHash::iterator ArrayHashIter;
+  typedef typename ArrayHash::const_iterator ArrayHashConstIter;
+  
+  typedef std::tr1::unordered_map<const UpdateNode*, T, UpdateNodeHashFn, UpdateNodeCmpFn> UpdateNodeHash;
+  typedef typename UpdateNodeHash::iterator UpdateNodeHashIter;
+  typedef typename UpdateNodeHash::const_iterator UpdateNodeHashConstIter;
+  
+  ArrayHash      _array_hash;
+  UpdateNodeHash _update_node_hash;  
+};
+
+
+template<class T>
+bool ArrayExprHash<T>::lookupArrayExpr(const Array* array, T& exp) const {
+  bool res = false;
+  
+#ifdef DEBUG
+  TimerStatIncrementer t(stats::arrayHashTime);
+#endif
+  
+  assert(array);  
+  ArrayHashConstIter it = _array_hash.find(array);
+  if (it != _array_hash.end()) {
+    exp = it->second;
+    res = true;
+  }  
+  return(res);  
+}
+
+template<class T>
+void ArrayExprHash<T>::hashArrayExpr(const Array* array, T& exp) {
+  
+#ifdef DEBUG  
+   TimerStatIncrementer t(stats::arrayHashTime);
+#endif
+   
+   assert(array);
+  _array_hash[array] = exp;
+}
+
+template<class T>
+bool ArrayExprHash<T>::lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const
+{
+  bool res = false;
+  
+#ifdef DEBUG
+  TimerStatIncrementer t(stats::arrayHashTime);
+#endif
+  
+  assert(un);
+  UpdateNodeHashConstIter it = _update_node_hash.find(un);
+  if (it != _update_node_hash.end()) {
+    exp = it->second;
+    res = true;
+  }  
+  return(res);   
+}
+
+template<class T>
+void ArrayExprHash<T>::hashUpdateNodeExpr(const UpdateNode* un, T& exp) 
+{
+#ifdef DEBUG
+  TimerStatIncrementer t(stats::arrayHashTime);
+#endif
+  
+  assert(un);
+  _update_node_hash[un] = exp;
+}
+
+}
+
+#endif

include/klee/util/ExprSMTLIBLetPrinter.h

+//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "ExprSMTLIBPrinter.h"
+#ifndef EXPRSMTLETPRINTER_H_
+#define EXPRSMTLETPRINTER_H_
+
+namespace klee
+{
+	/// This printer behaves like ExprSMTLIBPrinter except that it will abbreviate expressions
+	/// using the (let) SMT-LIBv2 command. Expression trees that appear two or more times in the Query
+	/// passed to setQuery() will be abbreviated.
+	///
+	/// This class should be used just like ExprSMTLIBPrinter.
+	class ExprSMTLIBLetPrinter : public ExprSMTLIBPrinter
+	{
+		public:
+			ExprSMTLIBLetPrinter();
+			virtual ~ExprSMTLIBLetPrinter() { }
+			virtual void generateOutput();
+		protected:
+			virtual void scan(const ref<Expr>& e);
+			virtual void reset();
+			virtual void generateBindings();
+			void printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
+			void printLetExpression();
+
+		private:
+			///Let expression binding number map.
+			std::map<const ref<Expr>,unsigned int> bindings;
+
+			/* These are effectively expression counters.
+			 * firstEO - first Occurrence of expression contains
+			 *           all expressions that occur once. It is
+			 *           only used to help us fill twoOrMoreOE
+			 *
+			 * twoOrMoreEO - Contains occur all expressions that
+			 *               that occur two or more times. These
+			 *               are the expressions that will be
+			 *               abbreviated by using (let () ()) expressions.
+			 *
+			 *
+			 *
+			 */
+			std::set<ref<Expr> > firstEO, twoOrMoreEO;
+
+			///This is the prefix string used for all abbreviations in (let) expressions.
+			static const char BINDING_PREFIX[];
+
+			/* This is needed during un-abbreviated printing.
+			 * Because we have overloaded printExpression()
+			 * the parent will call it and will abbreviate
+			 * when we don't want it to. This bool allows us
+			 * to switch it on/off easily.
+			 */
+			bool disablePrintedAbbreviations;
+
+
+
+	};
+
+	///Create a SMT-LIBv2 printer based on command line options
+	///The caller is responsible for deleting the printer
+	ExprSMTLIBPrinter* createSMTLIBPrinter();
+}
+
+#endif /* EXPRSMTLETPRINTER_H_ */

include/klee/util/ExprSMTLIBPrinter.h

+//===-- ExprSMTLIBPrinter.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_EXPRSMTLIBPRINTER_H
+#define KLEE_EXPRSMTLIBPRINTER_H
+
+#include <ostream>
+#include <string>
+#include <set>
+#include <map>
+#include <klee/Constraints.h>
+#include <klee/Expr.h>
+#include <klee/util/PrintContext.h>
+#include <klee/Solver.h>
+
+namespace klee {
+
+	///Base Class for SMTLIBv2 printer for Expr trees. It uses the QF_ABV logic. Note however the logic can be
+	///set to QF_AUFBV because some solvers (e.g. STP) complain if this logic is set to QF_ABV.
+	///
+	///This printer does not abbreviate expressions. The printer ExprSMTLIBLetPrinter does though.
+	///
+	/// It is intended to be used as follows
+	/// -# Create instance of this class
+	/// -# Set output ( setOutput() )
+	/// -# Set query to print ( setQuery() )
+	/// -# Set options using the methods prefixed with the word "set".
+	/// -# Call generateOutput()
+	///
+	/// The class can then be used again on another query ( setQuery() ).
+	/// The options set are persistent across queries (apart from setArrayValuesToGet() and PRODUCE_MODELS)
+	class ExprSMTLIBPrinter
+	{
+		public:
+
+			///Different SMTLIBv2 logics supported by this class
+			/// \sa setLogic()
+			enum SMTLIBv2Logic
+			{
+				QF_ABV,  ///< Logic using Theory of Arrays and Theory of Bitvectors
+				QF_AUFBV ///< Logic using Theory of Arrays and Theory of Bitvectors and has uninterpreted functions
+			};
+
+			///Different SMTLIBv2 options that have a boolean value that can be set
+			/// \sa setSMTLIBboolOption
+			enum SMTLIBboolOptions
+			{
+				PRINT_SUCCESS, ///< print-success SMTLIBv2 option
+				PRODUCE_MODELS,///< produce-models SMTLIBv2 option
+				INTERACTIVE_MODE ///< interactive-mode SMTLIBv2 option
+			};
+
+			///Different SMTLIBv2 bool option values
+			/// \sa setSMTLIBboolOption
+			enum SMTLIBboolValues
+			{
+				OPTION_TRUE, ///< Set option to true
+				OPTION_FALSE, ///< Set option to false
+				OPTION_DEFAULT ///< Use solver's defaults (the option will not be set in output)
+			};
+
+			enum ConstantDisplayMode
+			{
+				BINARY,///< Display bit vector constants in binary e.g. #b00101101
+				HEX, ///< Display bit vector constants in Hexidecimal e.g.#x2D
+				DECIMAL ///< Display bit vector constants in Decimal e.g. (_ bv45 8)
+			};
+
+			///Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV
+			enum SMTLIB_SORT
+			{
+				SORT_BITVECTOR,
+				SORT_BOOL
+			};
+
+
+
+			///Allows the way Constant bitvectors are printed to be changed.
+			///This setting is persistent across queries.
+			/// \return true if setting the mode was successful
+			bool setConstantDisplayMode(ConstantDisplayMode cdm);
+
+			ConstantDisplayMode getConstantDisplayMode() { return cdm;}
+
+			///Create a new printer that will print a query in the SMTLIBv2 language.
+			ExprSMTLIBPrinter();
+
+			///Set the output stream that will be printed to.
+			///This call is persistent across queries.
+			void setOutput(std::ostream& output);
+
+			///Set the query to print. This will setArrayValuesToGet()
+			///to none (i.e. no array values will be requested using
+			///the SMTLIBv2 (get-value ()) command).
+			void setQuery(const Query& q);
+
+			virtual ~ExprSMTLIBPrinter();
+
+			/// Print the query to the std::ostream
+			/// setOutput() and setQuery() must be called before calling this.
+			///
+			/// All options should be set before calling this.
+			/// \sa setConstantDisplayMode
+			/// \sa setLogic()
+			/// \sa setHumanReadable
+			/// \sa setSMTLIBboolOption
+			/// \sa setArrayValuesToGet
+			///
+			/// Mostly it does not matter what order the options are set in. However calling
+			/// setArrayValuesToGet() implies PRODUCE_MODELS is set so, if a call to setSMTLIBboolOption()
+			/// is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet() then the setSMTLIBboolOption()
+			/// call will be ineffective.
+			virtual void generateOutput();
+
+			///Set which SMTLIBv2 logic to use.
+			///This only affects what logic is used in the (set-logic <logic>) command.
+			///The rest of the printed SMTLIBv2 commands are the same regardless of the logic used.
+			///
+			/// \return true if setting logic was successful.
+			bool setLogic(SMTLIBv2Logic l);
+
+			///Sets how readable the printed SMTLIBv2 commands are.
+			/// \param hr If set to true the printed commands are made more human readable.
+			///
+			/// The printed commands are made human readable by...
+			/// - Indenting and line breaking.
+			/// - Adding comments
+			void setHumanReadable(bool hr);
+
+			///Set SMTLIB options.
+			/// These options will be printed when generateOutput() is called via
+			/// the SMTLIBv2 command (set-option :option-name <value>)
+			///
+			/// By default no options will be printed so the SMTLIBv2 solver will use
+			/// its default values for all options.
+			///
+			/// \return true if option was successfully set.
+			///
+			/// The options set are persistent across calls to setQuery() apart from the
+			/// PRODUCE_MODELS option which this printer may automatically set/unset.
+			bool setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value);
+
+			/// Set the array names that the SMTLIBv2 solver will be asked to determine.
+			/// Calling this method implies the PRODUCE_MODELS option is true and will change
+			/// any previously set value.
+			///
+			/// If no call is made to this function before ExprSMTLIBPrinter::generateOutput() then
+			/// the solver will only be asked to check satisfiability.
+			///
+			/// If the passed vector is not empty then the values of those arrays will be requested
+			/// via (get-value ()) SMTLIBv2 command in the output stream in the same order as vector.
+			void setArrayValuesToGet(const std::vector<const Array*>& a);
+
+			/// \return True if human readable mode is switched on
+			bool isHumanReadable();
+
+
+		protected:
+			///Contains the arrays found during scans
+			std::set<const Array*> usedArrays;
+
+			///Output stream to write to
+			std::ostream* o;
+
+			///The query to print
+			const Query* query;
+
+			///Determine the SMTLIBv2 sort of the expression
+			SMTLIB_SORT getSort(const ref<Expr>& e);
+
+			///Print an expression but cast it to a particular SMTLIBv2 sort first.
+			void printCastToSort(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT sort);
+
+			//Resets various internal objects for a new query
+			virtual void reset();
+
+			//Scan all constraints and the query
+			virtual void scanAll();
+
+			//Print an initial SMTLIBv2 comment before anything else is printed
+			virtual void printNotice();
+
+			//Print SMTLIBv2 options e.g. (set-option :option-name <value>) command
+			virtual void printOptions();
+
+			//Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV)
+			virtual void printSetLogic();
+
+			//Print SMTLIBv2 assertions for constant arrays
+			virtual void printArrayDeclarations();
+
+			//Print SMTLIBv2 for all constraints in the query
+			virtual void printConstraints();
+
+			//Print SMTLIBv2 assert statement for the "mangled" query
+			virtual void printQuery();
+
+			///Print the SMTLIBv2 command to check satisfiability and also optionally request for values
+			/// \sa setArrayValuesToGet()
+			virtual void printAction();
+
+			///Print the SMTLIBv2 command to exit
+			virtual void printExit();
+
+			///Print a Constant in the format specified by the current "Constant Display Mode"
+			void printConstant(const ref<ConstantExpr>& e);
+
+			///Recursively print expression
+			/// \param e is the expression to print
+			/// \param expectedSort is the sort we want. If "e" is not of the right type a cast will be performed.
+			virtual void printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
+
+			///Scan Expression recursively for Arrays in expressions. Found arrays are added to
+			/// the usedArrays vector.
+			virtual void scan(const ref<Expr>& e);
+
+			/* Rules of recursion for "Special Expression handlers" and printSortArgsExpr()
+			 *
+			 * 1. The parent of the recursion will have created an indent level for you so you don't need to add another initially.
+			 * 2. You do not need to add a line break (via printSeperator() ) at the end, the parent caller will handle that.
+			 * 3. The effect of a single recursive call should not affect the depth of the indent stack (nor the contents
+			 *    of the indent stack prior to the call). I.e. After executing a single recursive call the indent stack
+			 *    should have the same size and contents as before executing the recursive call.
+			 */
+
+			//Special Expression handlers
+			virtual void printReadExpr(const ref<ReadExpr>& e);
+			virtual void printExtractExpr(const ref<ExtractExpr>& e);
+			virtual void printCastExpr(const ref<CastExpr>& e);
+			virtual void printNotEqualExpr(const ref<NeExpr>& e);
+			virtual void printSelectExpr(const ref<SelectExpr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s);
+
+			//For the set of operators that take sort "s" arguments
+			virtual void printSortArgsExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s);
+
+			///For the set of operators that come in two sorts (e.g. (and () ()) (bvand () ()) )
+			///These are and,xor,or,not
+			/// \param e the Expression to print
+			/// \param s the sort of the expression we want
+			virtual void printLogicalOrBitVectorExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s);
+
+			///Recursively prints updatesNodes
+			virtual void printUpdatesAndArray(const UpdateNode* un, const Array* root);
+
+			///This method does the translation between Expr classes and SMTLIBv2 keywords
+			/// \return A C-string of the SMTLIBv2 keyword
+			virtual const char* getSMTLIBKeyword(const ref<Expr>& e);
+
+			virtual void printSeperator();
+
+			///Helper function for scan() that scans the expressions of an update node
+			virtual void scanUpdates(const UpdateNode* un);
+
+			///Helper printer class
+			PrintContext* p;
+
+			///This contains the query from the solver but negated for our purposes.
+			/// \sa mangleQuery()
+			ref<Expr> queryAssert;
+
+			///Indicates if there were any constant arrays founds during a scan()
+			bool haveConstantArray;
+
+
+		private:
+			SMTLIBv2Logic logicToUse;
+
+			volatile bool humanReadable;
+
+			//Map of enabled SMTLIB Options
+			std::map<SMTLIBboolOptions,bool> smtlibBoolOptions;
+
+			///This sets queryAssert to be the boolean negation of the original Query
+			void mangleQuery();
+
+			//Print a SMTLIBv2 option as a C-string
+			const char* getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option);
+
+			//Pointer to a vector of Arrays. These will be used for the (get-value () ) call.
+			const std::vector<const Array*> * arraysToCallGetValueOn;
+
+			ConstantDisplayMode cdm;
+
+	};
+
+
+
+}
+
+#endif

include/klee/util/PrintContext.h

+#ifndef PRINTCONTEXT_H_
+#define PRINTCONTEXT_H_
+
+#include <ostream>
+#include <sstream>
+#include <string>
+#include <stack>
+#include <iomanip>
+
+/// PrintContext - Helper class for pretty printing.
+/// It provides a basic wrapper around std::ostream that keeps track of
+/// how many characters have been used on the current line.
+///
+/// It also provides an optional way keeping track of the various levels of indentation
+/// by using a stack.
+/// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
+class PrintContext {
+private:
+  std::ostream &os;
+  std::stringstream ss;
+  std::string newline;
+
+  ///This is used to keep track of the stack of indentations used by
+  /// \sa breakLineI()
+  /// \sa pushIndent()
+  /// \sa popIndent()
+  std::stack<unsigned int> indentStack;
+
+public:
+  /// Number of characters on the current line.
+  unsigned pos;
+
+  PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
+  {
+	  indentStack.push(pos);
+  }
+
+  void setNewline(const std::string &_newline) {
+    newline = _newline;
+  }
+
+  void breakLine(unsigned indent=0) {
+    os << newline;
+    if (indent)
+      os << std::setw(indent) << ' ';
+    pos = indent;
+  }
+
+  ///Break line using the indent on the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& breakLineI()
+  {
+	  breakLine(indentStack.top());
+	  return *this;
+  }
+
+  ///Add the current position on the line to the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& pushIndent()
+  {
+	  indentStack.push(pos);
+	  return *this;
+  }
+
+  ///Pop the top off the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& popIndent()
+  {
+	  indentStack.pop();
+	  return *this;
+  }
+
+  /// write - Output a string to the stream and update the
+  /// position. The stream should not have any newlines.
+  void write(const std::string &s) {
+    os << s;
+    pos += s.length();
+  }
+
+  template <typename T>
+  PrintContext &operator<<(T elt) {
+    ss.str("");
+    ss << elt;
+    write(ss.str());
+    return *this;
+  }
+
+};
+
+
+#endif /* PRINTCONTEXT_H_ */

lib/Core/Executor.cpp

 #include "klee/TimerStatIncrementer.h"
 #include "klee/util/Assignment.h"
 #include "klee/util/ExprPPrinter.h"
+#include "klee/util/ExprSMTLIBLetPrinter.h"
 #include "klee/util/ExprUtil.h"
 #include "klee/util/GetElementPtrTypeIterator.h"
 #include "klee/Config/Version.h"
 	      cl::desc("Use counterexample caching (default=on)"));
 
   cl::opt<bool>
-  UseQueryPCLog("use-query-pc-log",
-                cl::init(false),
-		cl::desc("Log all queries into queries.pc (default=off)"));
-  
-  cl::opt<bool>
-  UseSTPQueryPCLog("use-stp-query-pc-log",
-                   cl::init(false),
-		   cl::desc("Log all queries sent to STP into queries.pc (default=off)"));
-
-  cl::opt<bool>
   NoExternals("no-externals", 
            cl::desc("Do not allow external function calls (default=off)"));
 
   STPOptimizeDivides("stp-optimize-divides", 
                  cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP (default=on)"),
                  cl::init(true));
+
+
+  /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
+   * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
+   * wants to patch their copy of LLVM just for these options.
+   */
+  cl::list<klee::QueryLoggingSolver> queryLoggingOptions("use-query-log",
+		  cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."),
+		  cl::values(
+					  clEnumValN(klee::ALL_PC,"all:pc","All queries in .pc (KQuery) format"),
+					  clEnumValN(klee::ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"),
+					  clEnumValN(klee::SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"),
+					  clEnumValN(klee::SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .pc (SMT-LIBv2) format"),
+					  clEnumValEnd
+		             ), cl::CommaSeparated
+  );
+
+
 }
 
 
 namespace klee {
   RNG theRNG;
+
+  //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
+  template <typename T>
+  static bool optionIsSet(cl::list<T> list, T option)
+  {
+	  return std::find(list.begin(), list.end(), option) != list.end();
+  }
+
+
 }
 
 Solver *constructSolverChain(STPSolver *stpSolver,
-                             std::string queryLogPath,
-                             std::string stpQueryLogPath,
+                             std::string querySMT2LogPath,
+                             std::string baseSolverQuerySMT2LogPath,
                              std::string queryPCLogPath,
-                             std::string stpQueryPCLogPath) {
+                             std::string baseSolverQueryPCLogPath) {
   Solver *solver = stpSolver;
 
-  if (UseSTPQueryPCLog)
+  if (optionIsSet(queryLoggingOptions,SOLVER_PC))
+  {
     solver = createPCLoggingSolver(solver, 
-                                   stpQueryLogPath);
+                                   baseSolverQueryPCLogPath);
+    klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str());
+  }
+
+  if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB))
+  {
+    solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath);
+    klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str());
+  }
 
   if (UseFastCexSolver)
     solver = createFastCexSolver(solver);
   if (DebugValidateSolver)
     solver = createValidatingSolver(solver, stpSolver);
 
-  if (UseQueryPCLog)
+  if (optionIsSet(queryLoggingOptions,ALL_PC))
+  {
     solver = createPCLoggingSolver(solver, 
                                    queryPCLogPath);
+    klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str());
+  }
   
+  if (optionIsSet(queryLoggingOptions,ALL_SMTLIB))
+  {
+    solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath);
+    klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str());
+  }
+
   return solver;
 }
 
   STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
   Solver *solver = 
     constructSolverChain(stpSolver,
-                         interpreterHandler->getOutputFilename("queries.qlog"),
-                         interpreterHandler->getOutputFilename("stp-queries.qlog"),
-                         interpreterHandler->getOutputFilename("queries.pc"),
-                         interpreterHandler->getOutputFilename("stp-queries.pc"));
+                         interpreterHandler->getOutputFilename("all-queries.smt2"),
+                         interpreterHandler->getOutputFilename("solver-queries.smt2"),
+                         interpreterHandler->getOutputFilename("all-queries.pc"),
+                         interpreterHandler->getOutputFilename("solver-queries.pc"));
   
   this->solver = new TimingSolver(solver, stpSolver);
 
 
 void Executor::getConstraintLog(const ExecutionState &state,
                                 std::string &res,
-                                bool asCVC) {
-  if (asCVC) {
-    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
-    char *log = solver->stpSolver->getConstraintLog(query);
-    res = std::string(log);
-    free(log);
-  } else {
-    std::ostringstream info;
-    ExprPPrinter::printConstraints(info, state.constraints);
-    res = info.str();    
+                                Interpreter::LogType logFormat) {
+
+  std::ostringstream info;
+
+  switch(logFormat)
+  {
+  case STP:
+  {
+	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
+	  char *log = solver->stpSolver->getConstraintLog(query);
+	  res = std::string(log);
+	  free(log);
   }
+	  break;
+
+  case KQUERY:
+  {
+	  std::ostringstream info;
+	  ExprPPrinter::printConstraints(info, state.constraints);
+	  res = info.str();
+  }
+	  break;
+
+  case SMTLIB2:
+  {
+	  std::ostringstream info;
+	  ExprSMTLIBPrinter* printer = createSMTLIBPrinter();
+	  printer->setOutput(info);
+	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
+	  printer->setQuery(query);
+	  printer->generateOutput();
+	  res = info.str();
+	  delete printer;
+  }
+	  break;
+
+  default:
+	  klee_warning("Executor::getConstraintLog() : Log format not supported!");
+  }
+
 }
 
 bool Executor::getSymbolicSolution(const ExecutionState &state,

lib/Core/Executor.h

   class TreeStreamWriter;
   template<class T> class ref;
 
+  ///The different query logging solvers that can switched on/off
+  enum QueryLoggingSolver
+  {
+	  ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format
+	  ALL_SMTLIB, ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) format
+	  SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format
+	  SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
+  };
+
+
   /// \todo Add a context object to keep track of data only live
   /// during an instruction step. Should contain addedStates,
   /// removedStates, and haltExecution, among others.
 
   virtual void getConstraintLog(const ExecutionState &state,
                                 std::string &res,
-                                bool asCVC = false);
+                                Interpreter::LogType logFormat = Interpreter::STP);
 
   virtual bool getSymbolicSolution(const ExecutionState &state, 
                                    std::vector< 

lib/Core/StatsTracker.cpp

              << "'CexCacheTime',"
              << "'ForkTime',"
              << "'ResolveTime',"
+#ifdef DEBUG
+	     << "'ArrayHashTime',"
+#endif
              << ")\n";
   statsFile->flush();
 }
              << "," << stats::cexCacheTime / 1000000.
              << "," << stats::forkTime / 1000000.
              << "," << stats::resolveTime / 1000000.
+#ifdef DEBUG
+             << "," << stats::arrayHashTime / 1000000.
+#endif
              << ")\n";
   statsFile->flush();
 }

lib/Expr/Expr.cpp

   }
 }
 
-void ConstantExpr::toString(std::string &Res) const {
-  Res = value.toString(10, false);
+void ConstantExpr::toString(std::string &Res, unsigned radix) const {
+  Res = value.toString(radix, false);
 }
 
 ref<ConstantExpr> ConstantExpr::Concat(const ref<ConstantExpr> &RHS) {
 extern "C" void vc_DeleteExpr(void*);
 
 Array::~Array() {
-  // FIXME: This shouldn't be necessary.
-  if (stpInitialArray) {
-    ::vc_DeleteExpr(stpInitialArray);
-    stpInitialArray = 0;
-  }
+}
+
+unsigned Array::computeHash() {
+  unsigned res = 0;
+  for (unsigned i = 0, e = name.size(); i != e; ++i)
+    res = (res * Expr::MAGIC_HASH_CONSTANT) + name[i];
+  return res; 
 }
 
 /***/

lib/Expr/ExprPPrinter.cpp

 //
 //===----------------------------------------------------------------------===//
 
+#include "klee/util/PrintContext.h"
 #include "klee/util/ExprPPrinter.h"
 
 #include "klee/Constraints.h"
   PCAllConstWidths("pc-all-const-widths",  llvm::cl::init(false));
 }
 
-/// PrintContext - Helper class for storing extra information for
-/// the pretty printer.
-class PrintContext {
-private:
-  std::ostream &os;
-  std::stringstream ss;
-  std::string newline;
-
-public:
-  /// Number of characters on the current line.
-  unsigned pos;
-
-public:
-  PrintContext(std::ostream &_os) : os(_os), newline("\n"), pos(0) {}
-
-  void setNewline(const std::string &_newline) {
-    newline = _newline;
-  }
-
-  void breakLine(unsigned indent=0) {
-    os << newline;
-    if (indent)
-      os << std::setw(indent) << ' ';
-    pos = indent;
-  }
-
-  /// write - Output a string to the stream and update the
-  /// position. The stream should not have any newlines.
-  void write(const std::string &s) {
-    os << s;
-    pos += s.length();
-  }
-
-  template <typename T>
-  PrintContext &operator<<(T elt) {
-    ss.str("");
-    ss << elt;
-    write(ss.str());
-    return *this;
-  }
-};
-
 class PPrinter : public ExprPPrinter {
 public:
   std::set<const Array*> usedArrays;

lib/Expr/ExprSMTLIBLetPrinter.cpp

+//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <iostream>
+#include "llvm/Support/CommandLine.h"
+#include "klee/util/ExprSMTLIBLetPrinter.h"
+
+using namespace std;
+
+namespace ExprSMTLIBOptions
+{
+	llvm::cl::opt<bool> useLetExpressions("smtlib-use-let-expressions",
+			llvm::cl::desc("Enables generated SMT-LIBv2 files to use (let) expressions (default=on)"),
+			llvm::cl::init(true)
+	);
+}
+
+namespace klee
+{
+	const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B";
+
+
+	ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter() :
+	bindings(), firstEO(), twoOrMoreEO(),
+	disablePrintedAbbreviations(false)
+	{
+	}
+
+	void ExprSMTLIBLetPrinter::generateOutput()
+	{
+		if(p==NULL || query == NULL || o ==NULL)
+		{
+			std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl;
+			return;
+		}
+
+		generateBindings();
+
+		if(isHumanReadable()) printNotice();
+		printOptions();
+		printSetLogic();
+		printArrayDeclarations();
+		printLetExpression();
+		printAction();
+		printExit();
+	}
+
+	void ExprSMTLIBLetPrinter::scan(const ref<Expr>& e)
+	{
+		if(isa<ConstantExpr>(e))
+			return; //we don't need to scan simple constants
+
+		if(firstEO.insert(e).second)
+		{
+			//We've not seen this expression before
+
+			if(const ReadExpr* re = dyn_cast<ReadExpr>(e))
+			{
+
+				//Attempt to insert array and if array wasn't present before do more things
+				if(usedArrays.insert(re->updates.root).second)
+				{
+
+					//check if the array is constant
+					if( re->updates.root->isConstantArray())
+						haveConstantArray=true;
+
+					//scan the update list
+					scanUpdates(re->updates.head);
+
+				}
+
+			}
+
+			//recurse into the children
+			Expr* ep = e.get();
+			for(unsigned int i=0; i < ep->getNumKids(); i++)
+				scan(ep->getKid(i));
+		}
+		else
+		{
+			/* We must of seen the expression before. Add it to
+			 * the set of twoOrMoreOccurances. We don't need to
+			 * check if the insertion fails.
+			 */
+			twoOrMoreEO.insert(e);
+		}
+	}
+
+	void ExprSMTLIBLetPrinter::generateBindings()
+	{
+		//Assign a number to each binding that will be used
+		unsigned int counter=0;
+		for(set<ref<Expr> >::const_iterator i=twoOrMoreEO.begin();
+				i!= twoOrMoreEO.end(); ++i)
+		{
+			bindings.insert(std::make_pair(*i,counter));
+			++counter;
+		}
+	}
+
+	void ExprSMTLIBLetPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
+	{
+		map<const ref<Expr>,unsigned int>::const_iterator i= bindings.find(e);
+
+		if(disablePrintedAbbreviations || i == bindings.end())
+		{
+			/*There is no abbreviation for this expression so print it normally.
+			 * Do this by using the parent method.
+			 */
+			ExprSMTLIBPrinter::printExpression(e,expectedSort);
+		}
+		else
+		{
+			//Use binding name e.g. "?B1"
+
+			/* Handle the corner case where the expectedSort
+			 * doesn't match the sort of the abbreviation. Not really very efficient (calls bindings.find() twice),
+			 * we'll cast and call ourself again but with the correct expectedSort.
+			 */
+			if(getSort(e) != expectedSort)
+			{
+				printCastToSort(e,expectedSort);
+				return;
+			}
+
+			// No casting is needed in this depth of recursion, just print the abbreviation
+			*p << BINDING_PREFIX << i->second;
+		}
+	}
+
+	void ExprSMTLIBLetPrinter::reset()
+	{
+		//Let parent clean up first
+		ExprSMTLIBPrinter::reset();
+
+		firstEO.clear();
+		twoOrMoreEO.clear();
+		bindings.clear();
+	}
+
+	void ExprSMTLIBLetPrinter::printLetExpression()
+	{
+		*p << "(assert"; p->pushIndent(); printSeperator();
+
+		if(bindings.size() !=0 )
+		{
+			//Only print let expression if we have bindings to use.
+			*p << "(let"; p->pushIndent(); printSeperator();
+			*p << "( "; p->pushIndent();
+
+			//Print each binding
+			for(map<const ref<Expr>, unsigned int>::const_iterator i= bindings.begin();
+					i!=bindings.end(); ++i)
+			{
+				printSeperator();
+				*p << "(" << BINDING_PREFIX << i->second << " ";
+				p->pushIndent();
+
+				//Disable abbreviations so none are used here.
+				disablePrintedAbbreviations=true;
+
+				//We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
+				printExpression(i->first,getSort(i->first));
+
+				p->popIndent();
+				printSeperator();
+				*p << ")";
+			}
+
+
+			p->popIndent(); printSeperator();
+			*p << ")";
+			printSeperator();
+
+			//Re-enable printing abbreviations.
+			disablePrintedAbbreviations=false;
+
+		}
+
+		//print out Expressions with abbreviations.
+		unsigned int numberOfItems= query->constraints.size() +1; //+1 for query
+		unsigned int itemsLeft=numberOfItems;
+		vector<ref<Expr> >::const_iterator constraint=query->constraints.begin();
+
+		/* Produce nested (and () () statements. If the constraint set
+		 * is empty then we will only print the "queryAssert".
+		 */
+		for(; itemsLeft !=0; --itemsLeft)
+		{
+			if(itemsLeft >=2)
+			{
+				*p << "(and"; p->pushIndent(); printSeperator();
+				printExpression(*constraint,SORT_BOOL); //We must and together bool expressions
+				printSeperator();
+				++constraint;
+				continue;
+			}
+			else
+			{
+				// must have 1 item left (i.e. the "queryAssert")
+				if(isHumanReadable()) { *p << "; query"; p->breakLineI();}
+				printExpression(queryAssert,SORT_BOOL); //The query must be a bool expression
+
+			}
+		}
+
+		/* Produce closing brackets for nested "and statements".
+		 * Number of "nested ands" = numberOfItems -1
+		 */
+		itemsLeft= numberOfItems -1;
+		for(; itemsLeft!=0; --itemsLeft)
+		{
+			p->popIndent(); printSeperator();
+			*p << ")";
+		}
+
+
+
+		if(bindings.size() !=0)
+		{
+			//end let expression
+			p->popIndent(); printSeperator();
+			*p << ")";  printSeperator();
+		}
+
+		//end assert
+		p->popIndent(); printSeperator();
+		*p << ")";
+		p->breakLineI();
+	}
+
+	ExprSMTLIBPrinter* createSMTLIBPrinter()
+	{
+		if(ExprSMTLIBOptions::useLetExpressions)
+			return new ExprSMTLIBLetPrinter();
+		else
+			return new ExprSMTLIBPrinter();
+	}
+
+
+}
+

lib/Expr/ExprSMTLIBPrinter.cpp

+//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#include <iostream>
+
+#include "llvm/Support/Casting.h"
+#include "llvm/Support/CommandLine.h"
+#include "klee/util/ExprSMTLIBPrinter.h"
+
+using namespace std;
+
+namespace ExprSMTLIBOptions
+{
+	//Command line options
+	llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode> argConstantDisplayMode
+	("smtlib-display-constants", llvm::cl::desc("Sets how bitvector constants are written in generated SMT-LIBv2 files (default=dec)"),
+	llvm::cl::values( clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin","Use binary form (e.g. #b00101101)"),
+					  clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex","Use Hexadecimal form (e.g. #x2D)"),
+					  clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec","Use decimal form (e.g. (_ bv45 8) )"),
+					  clEnumValEnd
+					),
+					llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL)
+
+
+	);
+
+	llvm::cl::opt<bool> humanReadableSMTLIB("smtlib-human-readable",
+				llvm::cl::desc("Enables generated SMT-LIBv2 files to be human readable (default=off)"),
+				llvm::cl::init(false)
+
+
+	);
+
+}
+
+
+namespace klee
+{
+
+	ExprSMTLIBPrinter::ExprSMTLIBPrinter() :
+		usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false), logicToUse(QF_AUFBV),
+		humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB), smtlibBoolOptions(), arraysToCallGetValueOn(NULL)
+	{
+		setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode);
+	}
+
+	ExprSMTLIBPrinter::~ExprSMTLIBPrinter()
+	{
+		if(p!=NULL)
+			delete p;
+	}
+
+	void ExprSMTLIBPrinter::setOutput(std::ostream& output)
+	{
+		o = &output;
+		if(p!=NULL)
+			delete p;
+
+		p = new PrintContext(output);
+	}
+
+	void ExprSMTLIBPrinter::setQuery(const Query& q)
+	{
+		query = &q;
+		reset(); // clear the data structures
+		scanAll();
+		mangleQuery();
+	}
+
+	void ExprSMTLIBPrinter::reset()
+	{
+		usedArrays.clear();
+		haveConstantArray=false;
+
+		/* Clear the PRODUCE_MODELS option if it was automatically set.
+		 * We need to do this because the next query might not need the
+		 * (get-value) SMT-LIBv2 command.
+		 */
+		if(arraysToCallGetValueOn !=NULL)
+			setSMTLIBboolOption(PRODUCE_MODELS,OPTION_DEFAULT);
+
+		arraysToCallGetValueOn=NULL;
+
+
+	}
+
+	bool ExprSMTLIBPrinter::isHumanReadable()
+	{
+		return humanReadable;
+	}
+
+	bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm)
+	{
+		if(cdm > DECIMAL)
+			return false;
+
+		this->cdm = cdm;
+		return true;
+	}
+
+	void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr>& e)
+	{
+		/* Handle simple boolean constants */
+
+		if(e->isTrue())
+		{
+			*p << "true";
+			return;
+		}
+
+		if(e->isFalse())
+		{
+			*p << "false";
+			return;
+		}
+
+		/* Handle bitvector constants */
+
+		std::string value;
+
+		/* SMTLIBv2 deduces the bit-width (should be 8-bits in our case)
+		 * from the length of the string (e.g. zero is #b00000000). LLVM
+		 * doesn't know about this so we need to pad the printed output
+		 * with the appropriate number of zeros (zeroPad)
+		 */
+		unsigned int zeroPad=0;
+
+		switch(cdm)
+		{
+			case BINARY:
+				e->toString(value,2);
+				*p << "#b";
+
+				zeroPad = e->getWidth() - value.length();
+
+				for(unsigned int count=0; count < zeroPad; count++)
+					*p << "0";
+
+				*p << value ;
+				break;
+
+			case HEX:
+				e->toString(value,16);
+				*p << "#x";
+
+				zeroPad =  (e->getWidth() / 4) - value.length();
+				for(unsigned int count=0; count < zeroPad; count++)
+					*p << "0";
+
+				*p << value ;
+				break;
+
+			case DECIMAL:
+				e->toString(value,10);
+				*p << "(_ bv" << value<< " " << e->getWidth() << ")";
+				break;
+
+			default:
+				std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant display mode" << std::endl;
+		}
+	}
+
+	void ExprSMTLIBPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
+	{
+		//check if casting might be necessary
+		if(getSort(e) != expectedSort)
+		{
+			printCastToSort(e,expectedSort);
+			return;
+		}
+
+
+		switch(e->getKind())
+		{
+			case Expr::Constant:
+				printConstant(cast<ConstantExpr>(e));
+				return; //base case
+
+			case Expr::NotOptimized:
+				//skip to child
+				printExpression(e->getKid(0),expectedSort);
+				return;
+
+			case Expr::Read:
+				printReadExpr(cast<ReadExpr>(e));
+				return;
+
+			case Expr::Extract:
+				printExtractExpr(cast<ExtractExpr>(e));
+				return;
+
+			case Expr::SExt:
+			case Expr::ZExt:
+				printCastExpr(cast<CastExpr>(e));
+				return;
+
+			case Expr::Ne:
+				printNotEqualExpr(cast<NeExpr>(e));
+				return;
+
+			case Expr::Select:
+				//the if-then-else expression.
+				printSelectExpr(cast<SelectExpr>(e),expectedSort);
+				return;
+
+			case Expr::Eq:
+				/* The "=" operator is special in that it can take any sort but we must
+				 * enforce that both arguments are the same type. We do this a lazy way
+				 * by enforcing the second argument is of the same type as the first.
+				 */
+				printSortArgsExpr(e,getSort(e->getKid(0)));
+
+				return;
+
+			case Expr::And:
+			case Expr::Or:
+			case Expr::Xor:
+			case Expr::Not:
+				/* These operators have a bitvector version and a bool version.
+				 * For these operators only (e.g. wouldn't apply to bvult) if the expected sort the
+				 * expression is T then that implies the arguments are also of type T.
+				 */
+				printLogicalOrBitVectorExpr(e,expectedSort);
+
+				return;
+
+
+			default:
+				/* The remaining operators (Add,Sub...,Ult,Ule,..)
+				 * Expect SORT_BITVECTOR arguments
+				 */
+				printSortArgsExpr(e,SORT_BITVECTOR);
+				return;
+		}
+	}
+
+	void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr>& e)
+	{
+		*p << "(" << getSMTLIBKeyword(e) << " ";
+		p->pushIndent();
+
+		printSeperator();
+
+		//print array with updates recursively
+		printUpdatesAndArray(e->updates.head,e->updates.root);
+
+		//print index
+		printSeperator();
+		printExpression(e->index,SORT_BITVECTOR);
+
+		p->popIndent();
+		printSeperator();
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr>& e)
+	{
+		unsigned int lowIndex= e->offset;
+		unsigned int highIndex= lowIndex + e->width -1;
+
+		*p << "((_ " << getSMTLIBKeyword(e) << " " << highIndex << "  " << lowIndex << ") ";
+
+		p->pushIndent(); //add indent for recursive call
+		printSeperator();
+
+		//recurse
+		printExpression(e->getKid(0),SORT_BITVECTOR);
+
+		p->popIndent(); //pop indent added for the recursive call
+		printSeperator();
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr>& e)
+	{
+		/* sign_extend and zero_extend behave slightly unusually in SMTLIBv2
+		 * instead of specifying of what bit-width we would like to extend to
+		 * we specify how many bits to add to the child expression
+		 *
+		 * e.g
+		 * ((_ sign_extend 64) (_ bv5 32))
+		 *
+		 * gives a (_ BitVec 96) instead of (_ BitVec 64)
+		 *
+		 * So we must work out how many bits we need to add.
+		 *
+		 * (e->width) is the desired number of bits
+		 * (e->src->getWidth()) is the number of bits in the child
+		 */
+		unsigned int numExtraBits= (e->width) - (e->src->getWidth());
+
+		*p << "((_ " << getSMTLIBKeyword(e) << " " <<
+				numExtraBits << ") ";
+
+		p->pushIndent(); //add indent for recursive call
+		printSeperator();
+
+		//recurse
+		printExpression(e->src,SORT_BITVECTOR);
+
+		p->popIndent(); //pop indent added for recursive call
+		printSeperator();
+
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::printNotEqualExpr(const ref<NeExpr>& e)
+	{
+		*p << "(not (";
+		p->pushIndent();
+		*p << "=" << " ";
+		p->pushIndent();
+		printSeperator();
+
+		/* The "=" operators allows both sorts. We assume
+		 * that the second argument sort should be forced to be the same sort as the
+		 * first argument
+		 */
+		SMTLIB_SORT s = getSort(e->getKid(0));
+
+		printExpression(e->getKid(0),s);
+		printSeperator();
+		printExpression(e->getKid(1),s);
+		p->popIndent();
+		printSeperator();
+
+		*p << ")";
+		p->popIndent();
+		printSeperator();
+		*p << ")";
+	}
+
+
+	const char* ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr>& e)
+	{
+
+		switch(e->getKind())
+		{
+			case Expr::Read: return "select";
+			case Expr::Select: return "ite";
+			case Expr::Concat: return "concat";
+			case Expr::Extract: return "extract";
+			case Expr::ZExt: return "zero_extend";
+			case Expr::SExt: return "sign_extend";
+
+			case Expr::Add: return "bvadd";
+			case Expr::Sub: return "bvsub";
+			case Expr::Mul: return "bvmul";
+			case Expr::UDiv: return "bvudiv";
+			case Expr::SDiv: return "bvsdiv";
+			case Expr::URem: return "bvurem";
+			case Expr::SRem: return "bvsrem";
+
+
+			/* And, Xor, Not and Or are not handled here because there different versions
+			 * for different sorts. See printLogicalOrBitVectorExpr()
+			 */
+
+
+			case Expr::Shl: return "bvshl";
+			case Expr::LShr: return "bvlshr";
+			case Expr::AShr: return "bvashr";
+
+			case Expr::Eq: return "=";
+
+			//Not Equal does not exist directly in SMTLIBv2
+
+			case Expr::Ult: return "bvult";
+			case Expr::Ule: return "bvule";
+			case Expr::Ugt: return "bvugt";
+			case Expr::Uge: return "bvuge";
+
+			case Expr::Slt: return "bvslt";
+			case Expr::Sle: return "bvsle";
+			case Expr::Sgt: return "bvsgt";
+			case Expr::Sge: return "bvsge";
+
+			default:
+				return "<error>";
+
+		}
+	}
+
+	void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode* un, const Array* root)
+	{
+		if(un!=NULL)
+		{
+			*p << "(store ";
+			p->pushIndent();
+			printSeperator();
+
+			//recurse to get the array or update that this store operations applies to
+			printUpdatesAndArray(un->next,root);
+
+			printSeperator();
+
+			//print index
+			printExpression(un->index,SORT_BITVECTOR);
+			printSeperator();
+
+			//print value that is assigned to this index of the array
+			printExpression(un->value,SORT_BITVECTOR);
+
+			p->popIndent();
+			printSeperator();
+			*p << ")";
+		}
+		else
+		{
+			//The base case of the recursion
+			*p << root->name;
+		}
+
+	}
+
+	void ExprSMTLIBPrinter::scanAll()
+	{
+		//perform scan of all expressions
+		for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++)
+			scan(*i);
+
+		//Scan the query too
+		scan(query->expr);
+	}
+
+	void ExprSMTLIBPrinter::generateOutput()
+	{
+		if(p==NULL || query == NULL || o ==NULL)
+		{
+			std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. Output or query bad!" << std::endl;
+			return;
+		}
+
+		if(humanReadable) printNotice();
+		printOptions();
+		printSetLogic();
+		printArrayDeclarations();
+		printConstraints();
+		printQuery();
+		printAction();
+		printExit();
+	}
+
+	void ExprSMTLIBPrinter::printSetLogic()
+	{
+		*o << "(set-logic ";
+		switch(logicToUse)
+		{
+		case QF_ABV: *o << "QF_ABV"; break;
+		case QF_AUFBV: *o << "QF_AUFBV" ; break;
+		}
+		*o << " )" << std::endl;
+	}
+
+
+	void ExprSMTLIBPrinter::printArrayDeclarations()
+	{
+		//Assume scan() has been called
+		if(humanReadable)
+			*o << "; Array declarations" << endl;
+
+		//declare arrays
+		for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++)
+		{
+			*o << "(declare-fun " << (*it)->name << " () "
+				 "(Array (_ BitVec " << (*it)->getDomain() << ") "
+				 "(_ BitVec " << (*it)->getRange() << ") ) )" << endl;
+		}
+
+		//Set array values for constant values
+		if(haveConstantArray)
+		{
+			if(humanReadable)
+				*o << "; Constant Array Definitions" << endl;
+
+			const Array* array;
+
+			//loop over found arrays
+			for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++)
+			{
+				array= *it;
+				int byteIndex=0;
+				if(array->isConstantArray())
+				{
+					/*loop over elements in the array and generate an assert statement
+					  for each one
+					 */
+					for(vector< ref<ConstantExpr> >::const_iterator ce= array->constantValues.begin();
+							ce != array->constantValues.end(); ce++, byteIndex++)
+					{
+						*p << "(assert (";
+						p->pushIndent();
+						*p <<           "= ";
+						p->pushIndent();
+						printSeperator();
+
+						*p << "(select " << array->name << " (_ bv" << byteIndex << " " << array->getDomain() << ") )";
+						printSeperator();
+						printConstant((*ce));
+
+						p->popIndent();
+						printSeperator();
+						*p << ")";
+						p->popIndent();
+						printSeperator();
+						*p << ")";
+
+						p->breakLineI();
+
+					}
+				}
+			}
+		}
+	}
+
+	void ExprSMTLIBPrinter::printConstraints()
+	{
+		if(humanReadable)
+			*o << "; Constraints" << endl;
+
+		//Generate assert statements for each constraint
+		for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++)
+		{
+			*p << "(assert ";
+			p->pushIndent();
+			printSeperator();
+
+			//recurse into Expression
+			printExpression(*i,SORT_BOOL);
+
+			p->popIndent();
+			printSeperator();
+			*p << ")"; p->breakLineI();
+		}
+
+	}
+
+	void ExprSMTLIBPrinter::printAction()
+	{
+		//Ask solver to check for satisfiability
+		*o << "(check-sat)" << endl;
+
+		/* If we has arrays to find the values of then we'll
+		 * ask the solver for the value of each bitvector in each array
+		 */
+		if(arraysToCallGetValueOn!=NULL && !arraysToCallGetValueOn->empty())
+		{
+
+			const Array* theArray=0;
+
+			//loop over the array names
+			for(vector<const Array*>::const_iterator it = arraysToCallGetValueOn->begin(); it != arraysToCallGetValueOn->end(); it++)
+			{
+				theArray=*it;
+				//Loop over the array indices
+				for(unsigned int index=0; index < theArray->size; ++index)
+				{
+					*o << "(get-value ( (select " << (**it).name <<
+					     " (_ bv" << index << " " << theArray->getDomain() << ") ) ) )" << endl;
+				}
+
+			}
+
+
+		}
+	}
+
+	void ExprSMTLIBPrinter::scan(const ref<Expr>& e)
+	{
+		if(e.isNull())
+		{
+			std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!" << std::endl;
+			return;
+		}
+
+		if(isa<ConstantExpr>(e))
+			return; //we don't need to scan simple constants
+
+		if(const ReadExpr* re = dyn_cast<ReadExpr>(e))
+		{
+
+			//Attempt to insert array and if array wasn't present before do more things
+			if(usedArrays.insert(re->updates.root).second)
+			{
+
+				//check if the array is constant
+				if( re->updates.root->isConstantArray())
+					haveConstantArray=true;
+
+				//scan the update list
+				scanUpdates(re->updates.head);
+
+			}
+
+		}
+
+		//recurse into the children
+		Expr* ep = e.get();
+		for(unsigned int i=0; i < ep->getNumKids(); i++)
+			scan(ep->getKid(i));
+	}
+
+
+	void ExprSMTLIBPrinter::scanUpdates(const UpdateNode* un)
+	{
+		while(un != NULL)
+		{
+			scan(un->index);
+			scan(un->value);
+			un= un->next;
+		}
+	}
+
+
+	void ExprSMTLIBPrinter::printExit()
+	{
+		*o << "(exit)" << endl;
+	}
+
+	bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l)
+	{
+		if(l > QF_AUFBV)
+			return false;
+
+		logicToUse=l;
+		return true;
+	}
+
+	void ExprSMTLIBPrinter::printSeperator()
+	{
+		if(humanReadable)
+			p->breakLineI();
+		else
+			p->write(" ");
+	}
+
+	void ExprSMTLIBPrinter::printNotice()
+	{
+		*o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl;
+	}
+
+	void ExprSMTLIBPrinter::setHumanReadable(bool hr)
+	{
+		humanReadable=hr;
+	}
+
+	void ExprSMTLIBPrinter::printOptions()
+	{
+		//Print out SMTLIBv2 boolean options
+		for(std::map<SMTLIBboolOptions,bool>::const_iterator i= smtlibBoolOptions.begin(); i!= smtlibBoolOptions.end(); i++)
+		{
+			*o << "(set-option :" << getSMTLIBOptionString(i->first) <<
+			" " << ((i->second)?"true":"false") << ")" << endl;
+		}
+	}
+
+	void ExprSMTLIBPrinter::printQuery()
+	{
+		if(humanReadable)
+		{
+			*p << "; Query from solver turned into an assert";
+			p->breakLineI();
+		}
+
+		p->pushIndent();
+		*p << "(assert";
+		p->pushIndent();
+		printSeperator();
+
+		printExpression(queryAssert,SORT_B