Commit 9aaaf2ce authored by Cristian Cadar's avatar Cristian Cadar Committed by Dan Liew
Browse files

Nice patch by Dan Liew that adds support for printing queries in the

SMTLIB format (part of his MSc project work).

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8
parent dc391fc6
//===-- 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_ */
//===-- 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
//===-- 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();
}
}
This diff is collapsed.