1 #ifndef Rose_BinaryAnalysis_SmtlibSolver_H
2 #define Rose_BinaryAnalysis_SmtlibSolver_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <BinarySmtSolver.h>
7 #include <boost/filesystem.hpp>
8 #include <boost/unordered_map.hpp>
16 boost::filesystem::path executable_;
17 std::string shellArgs_;
22 typedef boost::unordered_map<SymbolicExpr::Hash, ExprExprMap> MemoizedEvidence;
23 MemoizedEvidence memoizedEvidence;
28 explicit SmtlibSolver(
const std::string &
name,
const boost::filesystem::path &executable,
const std::string &shellArgs =
"",
30 :
SmtSolver(name, linkages), executable_(executable), shellArgs_(shellArgs) {}
44 static Ptr instance(
const std::string &name,
const boost::filesystem::path &executable,
const std::string &shellArgs =
"",
57 virtual void reset() ROSE_OVERRIDE;
66 virtual
void timeout(
boost::chrono::duration<
double>) ROSE_OVERRIDE;
75 void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
76 SymbolicExpr::LeafPtr
varForSet(const SymbolicExpr::InteriorPtr &set);
92 virtual
Type mostType(const
std::vector<SExprTypePair>&);
95 virtual SExprTypePair outputCast(const SExprTypePair&,
Type to);
96 virtual
std::vector<SExprTypePair> outputCast(const
std::vector<SExprTypePair>&,
Type to);
98 virtual
std::
string typeName(const SymbolicExpr::Ptr&);
104 virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&);
105 virtual
std::vector<
SmtSolver::SExprTypePair> outputExpressions(const
std::vector<SymbolicExpr::Ptr>&);
108 virtual SExprTypePair outputLeaf(const SymbolicExpr::LeafPtr&);
113 virtual SExprTypePair outputLeftAssoc(const
std::
string &func, const SymbolicExpr::InteriorPtr&,
Type rettype = NO_TYPE);
114 virtual SExprTypePair outputLeftAssoc(const
std::
string &func, const
std::vector<SExprTypePair>&,
Type rettype = NO_TYPE);
117 virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
118 virtual SExprTypePair outputLogicalShiftRight(const SymbolicExpr::InteriorPtr&);
119 virtual SExprTypePair outputShiftLeft(const SymbolicExpr::InteriorPtr&);
122 virtual SExprTypePair outputRotateLeft(const SymbolicExpr::InteriorPtr&);
123 virtual SExprTypePair outputRotateRight(const SymbolicExpr::InteriorPtr&);
127 virtual SExprTypePair outputXor(const SymbolicExpr::InteriorPtr&);
130 virtual SExprTypePair outputBinary(const
std::
string &func, const SymbolicExpr::InteriorPtr&,
Type rettype = NO_TYPE);
133 virtual SExprTypePair outputUnary(const
std::
string &funcName, const SExprTypePair &arg);
136 virtual SExprTypePair outputExtract(const SymbolicExpr::InteriorPtr&);
139 virtual SExprTypePair outputSignExtend(const SymbolicExpr::InteriorPtr&);
140 virtual SExprTypePair outputUnsignedExtend(const SymbolicExpr::InteriorPtr&);
144 virtual SExprTypePair outputIte(const SymbolicExpr::InteriorPtr&);
148 virtual SExprTypePair outputNotEqual(const SymbolicExpr::InteriorPtr&);
151 virtual SExprTypePair outputSignedCompare(const SymbolicExpr::InteriorPtr&);
152 virtual SExprTypePair outputUnsignedCompare(const SymbolicExpr::InteriorPtr&);
153 virtual SExprTypePair outputZerop(const SymbolicExpr::InteriorPtr&);
156 virtual SExprTypePair outputMultiply(const SymbolicExpr::InteriorPtr&);
157 virtual SExprTypePair outputDivide(const SymbolicExpr::InteriorPtr&, const
std::
string &operation);
158 virtual SExprTypePair outputModulo(const SymbolicExpr::InteriorPtr&, const
std::
string &operation);
161 virtual SExprTypePair outputRead(const SymbolicExpr::InteriorPtr&);
164 virtual SExprTypePair outputWrite(const SymbolicExpr::InteriorPtr&);
167 virtual SExprTypePair outputSet(const SymbolicExpr::InteriorPtr&);
170 virtual
void outputVariableDeclarations(
std::ostream&, const
VariableSet&);
171 virtual
void outputComments(
std::ostream&, const
std::vector<SymbolicExpr::Ptr>&);
172 virtual
void outputCommonSubexpressions(
std::ostream&, const
std::vector<SymbolicExpr::Ptr>&);
173 virtual
void outputAssertion(
std::ostream&, const SymbolicExpr::Ptr&);
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var)
Specify variable to use for OP_SET.
virtual SymbolicExpr::Ptr evidenceForName(const std::string &) ROSE_OVERRIDE
Evidence of satisfiability for a variable or memory address.
virtual Ptr create() const ROSE_OVERRIDE
Virtual constructor.
virtual void clearMemoization() ROSE_OVERRIDE
Clear memoization table.
virtual void timeout(boost::chrono::duration< double >) ROSE_OVERRIDE
Set the timeout for the solver.
Holds a value or nothing.
virtual void generateFile(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_OVERRIDE
Generates an input file for for the solver.
const std::string & name() const
Property: Name of solver for debugging.
Main namespace for the ROSE library.
std::set< uint64_t > Definitions
Free variables that have been defined.
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
virtual void reset() ROSE_OVERRIDE
Reset solver state.
virtual void outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
Generate definitions for bit-wise XOR functions.
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
virtual std::string getCommand(const std::string &configName) ROSE_OVERRIDE
Given the name of a configuration file, return the command that is needed to run the solver...
virtual void clearEvidence() ROSE_OVERRIDE
Clears evidence information.
Wrapper around solvers that speak SMT-LIB.
static Ptr instance(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE)
Construct a solver using the specified program.
virtual std::vector< std::string > evidenceNames() ROSE_OVERRIDE
Names of items for which satisfiability evidence exists.
An executable is available.
Type
Type (sort) of expression.
Interface to Satisfiability Modulo Theory (SMT) solvers.
virtual std::string getErrorMessage(int exitStatus) ROSE_OVERRIDE
Error message from running a solver executable.
virtual void outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
Generate functions for comparison of bitvectors.
virtual void findVariables(const SymbolicExpr::Ptr &, VariableSet &) ROSE_OVERRIDE
Return all variables that need declarations.
LinkMode linkage() const
Property: How ROSE communicates with the solver.
virtual void parseEvidence() ROSE_OVERRIDE
Parses evidence of satisfiability.