ExprSMTLIBPrinter.h

Go to the documentation of this file.

//===-- 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 "klee/Expr/Constraints.h"
#include "klee/Expr/Expr.h"
#include "klee/Solver/Solver.h"
#include "klee/Support/PrintContext.h"
 
#include <map>
#include <set>
#include <string>
 
namespace llvm {
class raw_ostream;
}
 
namespace klee {
 
class ExprSMTLIBPrinter {
public:
  enum SMTLIBv2Logic {
    QF_ABV,  
    QF_AUFBV 
  };
 
  enum SMTLIBboolOptions {
    PRINT_SUCCESS,   
    PRODUCE_MODELS,  
    INTERACTIVE_MODE 
  };
 
  enum SMTLIBboolValues {
    OPTION_TRUE,   
    OPTION_FALSE,  
    OPTION_DEFAULT 
  };
 
  enum ConstantDisplayMode {
    BINARY, 
    HEX,    
    DECIMAL 
  };
 
  enum AbbreviationMode {
    ABBR_NONE, 
    ABBR_LET,  
    ABBR_NAMED 
  };
 
  enum SMTLIB_SORT { SORT_BITVECTOR, SORT_BOOL };
 
  bool setConstantDisplayMode(ConstantDisplayMode cdm);
 
  ConstantDisplayMode getConstantDisplayMode() { return cdm; }
 
  void setAbbreviationMode(AbbreviationMode am) { abbrMode = am; }
 
  ExprSMTLIBPrinter();
 
  void setOutput(llvm::raw_ostream &output);
 
  void setQuery(const Query &q);
 
  ~ExprSMTLIBPrinter();
 
  void generateOutput();
 
  bool setLogic(SMTLIBv2Logic l);
 
  void setHumanReadable(bool hr);
 
  bool setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value);
 
  void setArrayValuesToGet(const std::vector<const Array *> &a);
 
  bool isHumanReadable();
 
protected:
  std::set<const Array *> usedArrays;
 
  std::set<ref<Expr> > seenExprs;
 
  typedef std::map<const ref<Expr>, int> BindingMap;
 
  BindingMap bindings;
 
  std::vector<BindingMap> orderedBindings;
 
  llvm::raw_ostream *o;
 
  const Query *query;
 
  SMTLIB_SORT getSort(const ref<Expr> &e);
 
  void printCastToSort(const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT sort);
 
  // Resets various internal objects for a new query
  void reset();
 
  // Scan all constraints and the query
  void scanAll();
 
  // Print an initial SMTLIBv2 comment before anything else is printed
  void printNotice();
 
  // Print SMTLIBv2 options e.g. (set-option :option-name <value>) command
  void printOptions();
 
  // Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV)
  void printSetLogic();
 
  // Print SMTLIBv2 assertions for constant arrays
  void printArrayDeclarations();
 
  // Print SMTLIBv2 for the query optimised for human readability
  void printHumanReadableQuery();
 
  // Print SMTLIBv2 for the query optimised for minimal query size.
  // This does not imply ABBR_LET or ABBR_NAMED (although it would be wise
  // to use them to minimise the query size further)
  void printMachineReadableQuery();
 
  void printQueryInSingleAssert();
 
  void printAction();
 
  void printExit();
 
  void printConstant(const ref<ConstantExpr> &e);
 
  void printExpression(const ref<Expr> &e, SMTLIB_SORT expectedSort);
 
  void scan(const ref<Expr> &e);
 
  void scanBindingExprDeps();
 
  /* 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
  void printReadExpr(const ref<ReadExpr> &e);
  void printExtractExpr(const ref<ExtractExpr> &e);
  void printCastExpr(const ref<CastExpr> &e);
  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,
                                 ExprSMTLIBPrinter::SMTLIB_SORT s);
 
  void printLogicalOrBitVectorExpr(const ref<Expr> &e,
                                           ExprSMTLIBPrinter::SMTLIB_SORT s);
 
  void printUpdatesAndArray(const UpdateNode *un, const Array *root);
 
  const char *getSMTLIBKeyword(const ref<Expr> &e);
 
  void printSeperator();
 
  void scanUpdates(const UpdateNode *un);
 
  PrintContext *p;
 
  ref<Expr> queryAssert;
 
  bool haveConstantArray;
 
private:
  SMTLIBv2Logic logicToUse;
 
  volatile bool humanReadable;
 
  // Map of enabled SMTLIB Options
  std::map<SMTLIBboolOptions, bool> smtlibBoolOptions;
 
  // Print a SMTLIBv2 option as a C-string
  const char *
  getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option);
 
  void printFullExpression(const ref<Expr> &e, SMTLIB_SORT expectedSort);
 
  void printAssert(const ref<Expr> &e);
 
  // Pointer to a vector of Arrays. These will be used for the (get-value () )
  // call.
  const std::vector<const Array *> *arraysToCallGetValueOn;
 
  ConstantDisplayMode cdm;
  AbbreviationMode abbrMode;
};
}
 
#endif /* KLEE_EXPRSMTLIBPRINTER_H */