1 #ifndef ROSE_BinaryAnalysis_SmtlibSolver_H
2 #define ROSE_BinaryAnalysis_SmtlibSolver_H
3 #include <featureTests.h>
6 #include <Rose/BinaryAnalysis/SmtSolver.h>
7 #include <boost/filesystem.hpp>
8 #include <boost/unordered_map.hpp>
10 namespace Rose {
11 namespace BinaryAnalysis {
14 class SmtlibSolver: public SmtSolver {
15 private:
16  boost::filesystem::path executable_; // solver program
17  std::string shellArgs_; // extra arguments for command (passed through shell)
18  ExprExprMap varsForSets_; // variables to use for sets
20 protected:
22  typedef boost::unordered_map<SymbolicExpr::Hash, ExprExprMap> MemoizedEvidence;
23  MemoizedEvidence memoizedEvidence;
24  Sawyer::Optional<boost::chrono::duration<double> > timeout_; // max time for solving a single set of equations in seconds
26 protected:
27  // Reference counted. Use instance() or create() instead.
28  explicit SmtlibSolver(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs = "",
29  unsigned linkages = LM_EXECUTABLE)
30  : SmtSolver(name, linkages), executable_(executable), shellArgs_(shellArgs) {}
32 public:
44  static Ptr instance(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs = "",
45  unsigned linkages = LM_EXECUTABLE) {
46  return Ptr(new SmtlibSolver(name, executable, shellArgs, linkages));
47  }
52  virtual Ptr create() const ROSE_OVERRIDE {
53  return instance(name(), executable_, shellArgs_, linkage());
54  }
56 public:
57  virtual void reset() ROSE_OVERRIDE;
58  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) ROSE_OVERRIDE;
59  virtual std::string getCommand(const std::string &configName) ROSE_OVERRIDE;
60  virtual std::string getErrorMessage(int exitStatus) ROSE_OVERRIDE;
61  virtual void findVariables(const SymbolicExpr::Ptr&, VariableSet&) ROSE_OVERRIDE;
62  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) ROSE_OVERRIDE;
63  virtual std::vector<std::string> evidenceNames() ROSE_OVERRIDE;
64  virtual void clearEvidence() ROSE_OVERRIDE;
65  virtual void clearMemoization() ROSE_OVERRIDE;
66  virtual void timeout(boost::chrono::duration<double>) ROSE_OVERRIDE;
68 protected:
75  void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
76  SymbolicExpr::LeafPtr varForSet(const SymbolicExpr::InteriorPtr &set);
79  virtual void parseEvidence() ROSE_OVERRIDE;
85  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
88  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
90 protected:
91  // Return the most common type (arbitrarily if tied). Returns NO_TYPE when there are no inputs.
92  virtual Type mostType(const std::vector<SExprTypePair>&);
94  // Cast an SMT expression(s) to some other type.
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&);
100  // Convert a ROSE symbolic expression to an SMT solver expression. The return value is a pair consisting of an SExpr::Ptr
101  // (ROSE internal representation of an SMT solver expression) and a type indicating whether the SMT solver expression is a
102  // bit vector, a Boolean, or a memory state. Although ROSE uses a bit to represent Booleans, SMT solvers often distinguish
103  // betwen a single bit and a Boolean.
104  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&);
105  virtual std::vector<SmtSolver::SExprTypePair> outputExpressions(const std::vector<SymbolicExpr::Ptr>&);
107  // Create an SMT expression from a ROSE symbolic leaf node (constant, variable, or memory state).
108  virtual SExprTypePair outputLeaf(const SymbolicExpr::LeafPtr&);
110  // Create an expression composed of only 2-argument calls to the specified function. The arguments are all first converted
111  // to the most common argument type (which is usually a no-op since arguments are normally all the same type). If rettype
112  // is NO_TYPE then the returned type is assumed to be the same as the arguments, otherwise it is set as specified.
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);
116  // Create an expression that does a shift operation.
117  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
118  virtual SExprTypePair outputLogicalShiftRight(const SymbolicExpr::InteriorPtr&);
119  virtual SExprTypePair outputShiftLeft(const SymbolicExpr::InteriorPtr&);
121  // Create a rotate expression. */
122  virtual SExprTypePair outputRotateLeft(const SymbolicExpr::InteriorPtr&);
123  virtual SExprTypePair outputRotateRight(const SymbolicExpr::InteriorPtr&);
125  // Create an expression that does either a bit-wise or boolean XOR. All arguments must be the same type, either bit vectors
126  // or Booleans, and the return value is the same as the argument type.
127  virtual SExprTypePair outputXor(const SymbolicExpr::InteriorPtr&);
129  // Create a binary expression. This is a special case of outputLeftAssoc.
130  virtual SExprTypePair outputBinary(const std::string &func, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
132  // Create a unary expression. The return type is the same as the argument type.
133  virtual SExprTypePair outputUnary(const std::string &funcName, const SExprTypePair &arg);
135  // Create a bit extraction expression, i.e., a bit vector result which is a sub-array of the input bit vector.
136  virtual SExprTypePair outputExtract(const SymbolicExpr::InteriorPtr&);
138  // Create a widening expression that returns a bit vector type. */
139  virtual SExprTypePair outputSignExtend(const SymbolicExpr::InteriorPtr&);
140  virtual SExprTypePair outputUnsignedExtend(const SymbolicExpr::InteriorPtr&);
142  // Create an if-then-else expression. The arguments should be the same type (one is cast if not) and the return type is the
143  // same as the argument types.
144  virtual SExprTypePair outputIte(const SymbolicExpr::InteriorPtr&);
146  // Create a not-equal expression. The operands can be any type and are cast to a common type before comparing. The return
147  // type is Boolean.
148  virtual SExprTypePair outputNotEqual(const SymbolicExpr::InteriorPtr&);
150  // Create a comparison expression for bit vectors. Return type is Boolean. */
151  virtual SExprTypePair outputSignedCompare(const SymbolicExpr::InteriorPtr&);
152  virtual SExprTypePair outputUnsignedCompare(const SymbolicExpr::InteriorPtr&);
153  virtual SExprTypePair outputZerop(const SymbolicExpr::InteriorPtr&);
155  // Create multiplicative expression. */
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);
160  // Create a memory read expression. The return type is a bit vector. */
161  virtual SExprTypePair outputRead(const SymbolicExpr::InteriorPtr&);
163  // Create a memory write operation. The return value is a memory state. */
164  virtual SExprTypePair outputWrite(const SymbolicExpr::InteriorPtr&);
166  // Create a set expression that represents a set of bit vectors all the same size. */
167  virtual SExprTypePair outputSet(const SymbolicExpr::InteriorPtr&);
169  // Functions that generate SMT-LIB output to a stream when given a Rose::BinaryAnalysis::SymbolicExpr
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&);
174 };
176 } // namespace
177 } // namespace
179 #endif
180 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
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.
Definition: SmtlibSolver.h:52
virtual void clearMemoization() ROSE_OVERRIDE
Clear memoization table.
virtual void timeout(boost::chrono::duration< double >) ROSE_OVERRIDE
Set the timeout for the solver.
STL namespace.
Holds a value or nothing.
Definition: Optional.h:49
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.
Definition: SmtSolver.h:300
Main namespace for the ROSE library.
std::set< uint64_t > Definitions
Free variables that have been defined.
Definition: SmtSolver.h:174
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
Definition: SmtSolver.h:172
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.
Definition: SmtSolver.h:257
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.
Definition: SmtlibSolver.h:14
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.
Definition: SmtlibSolver.h:44
virtual std::vector< std::string > evidenceNames() ROSE_OVERRIDE
Names of items for which satisfiability evidence exists.
An executable is available.
Definition: SmtSolver.h:48
Type (sort) of expression.
Definition: SmtSolver.h:57
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SmtSolver.h:36
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.
Definition: SmtSolver.h:307
Evidence evidence()
All evidence of satisfiability.
virtual void parseEvidence() ROSE_OVERRIDE
Parses evidence of satisfiability.