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:
21  Sawyer::Optional<boost::chrono::duration<double> > timeout_; // max time for solving a single set of equations in seconds
23 protected:
24  // Reference counted. Use instance() or create() instead.
25  explicit SmtlibSolver(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs = "",
26  unsigned linkages = LM_EXECUTABLE)
27  : SmtSolver(name, linkages), executable_(executable), shellArgs_(shellArgs) {}
29 public:
41  static Ptr instance(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs = "",
42  unsigned linkages = LM_EXECUTABLE) {
43  return Ptr(new SmtlibSolver(name, executable, shellArgs, linkages));
44  }
46  virtual Ptr create() const override;
48 public:
49  virtual void reset() override;
50  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpression::Ptr> &exprs, Definitions*) override;
51  virtual std::string getCommand(const std::string &configName) override;
52  virtual std::string getErrorMessage(int exitStatus) override;
53  virtual void findVariables(const SymbolicExpression::Ptr&, VariableSet&) override;
54  virtual void timeout(boost::chrono::duration<double>) override;
56 protected:
67  virtual void parseEvidence() override;
73  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpression::Ptr>&);
76  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpression::Ptr>&);
78 protected:
79  // Return the most common type (arbitrarily if tied). Returns NO_TYPE when there are no inputs.
80  virtual Type mostType(const std::vector<SExprTypePair>&);
82  // Cast an SMT expression(s) to some other type.
83  virtual SExprTypePair outputCast(const SExprTypePair&, Type to);
84  virtual std::vector<SExprTypePair> outputCast(const std::vector<SExprTypePair>&, Type to);
86  virtual std::string typeName(const SymbolicExpression::Ptr&);
88  // Convert a ROSE symbolic expression to an SMT solver expression. The return value is a pair consisting of an SExpr::Ptr
89  // (ROSE internal representation of an SMT solver expression) and a type indicating whether the SMT solver expression is a
90  // bit vector, a Boolean, or a memory state. Although ROSE uses a bit to represent Booleans, SMT solvers often distinguish
91  // betwen a single bit and a Boolean.
92  virtual SExprTypePair outputExpression(const SymbolicExpression::Ptr&);
93  virtual std::vector<SmtSolver::SExprTypePair> outputExpressions(const std::vector<SymbolicExpression::Ptr>&);
95  // Create an SMT expression from a ROSE symbolic leaf node (constant, variable, or memory state).
96  virtual SExprTypePair outputLeaf(const SymbolicExpression::LeafPtr&);
98  // Create an expression composed of only 2-argument calls to the specified function. The arguments are all first converted
99  // to the most common argument type (which is usually a no-op since arguments are normally all the same type). If rettype
100  // is NO_TYPE then the returned type is assumed to be the same as the arguments, otherwise it is set as specified.
101  virtual SExprTypePair outputLeftAssoc(const std::string &func, const SymbolicExpression::InteriorPtr&, Type rettype = NO_TYPE);
102  virtual SExprTypePair outputLeftAssoc(const std::string &func, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
104  // Create an expression that does a shift operation.
105  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpression::InteriorPtr&);
106  virtual SExprTypePair outputLogicalShiftRight0(const SymbolicExpression::InteriorPtr&);
107  virtual SExprTypePair outputLogicalShiftRight1(const SymbolicExpression::InteriorPtr&);
108  virtual SExprTypePair outputShiftLeft0(const SymbolicExpression::InteriorPtr&);
109  virtual SExprTypePair outputShiftLeft1(const SymbolicExpression::InteriorPtr&);
111  // Create a rotate expression. */
112  virtual SExprTypePair outputRotateLeft(const SymbolicExpression::InteriorPtr&);
113  virtual SExprTypePair outputRotateRight(const SymbolicExpression::InteriorPtr&);
115  // Create an expression that does either a bit-wise or boolean XOR. All arguments must be the same type, either bit vectors
116  // or Booleans, and the return value is the same as the argument type.
117  virtual SExprTypePair outputXor(const SymbolicExpression::InteriorPtr&);
119  // Create a binary expression. This is a special case of outputLeftAssoc.
120  virtual SExprTypePair outputBinary(const std::string &func, const SymbolicExpression::InteriorPtr&, Type rettype = NO_TYPE);
122  // Create a unary expression. The return type is the same as the argument type.
123  virtual SExprTypePair outputUnary(const std::string &funcName, const SExprTypePair &arg);
125  // Create a bit extraction expression, i.e., a bit vector result which is a sub-array of the input bit vector.
126  virtual SExprTypePair outputExtract(const SymbolicExpression::InteriorPtr&);
128  // Create a widening expression that returns a bit vector type. */
129  virtual SExprTypePair outputSignExtend(const SymbolicExpression::InteriorPtr&);
130  virtual SExprTypePair outputUnsignedExtend(const SymbolicExpression::InteriorPtr&);
132  // Create an if-then-else expression. The arguments should be the same type (one is cast if not) and the return type is the
133  // same as the argument types.
134  virtual SExprTypePair outputIte(const SymbolicExpression::InteriorPtr&);
136  // Create a not-equal expression. The operands can be any type and are cast to a common type before comparing. The return
137  // type is Boolean.
138  virtual SExprTypePair outputNotEqual(const SymbolicExpression::InteriorPtr&);
140  // Create a comparison expression for bit vectors. Return type is Boolean. */
141  virtual SExprTypePair outputSignedCompare(const SymbolicExpression::InteriorPtr&);
142  virtual SExprTypePair outputUnsignedCompare(const SymbolicExpression::InteriorPtr&);
143  virtual SExprTypePair outputZerop(const SymbolicExpression::InteriorPtr&);
145  // Create multiplicative expression. */
146  virtual SExprTypePair outputMultiply(const SymbolicExpression::InteriorPtr&);
147  virtual SExprTypePair outputDivide(const SymbolicExpression::InteriorPtr&, const std::string &operation);
148  virtual SExprTypePair outputModulo(const SymbolicExpression::InteriorPtr&, const std::string &operation);
150  // Create a memory read expression. The return type is a bit vector. */
151  virtual SExprTypePair outputRead(const SymbolicExpression::InteriorPtr&);
153  // Create a memory write operation. The return value is a memory state. */
154  virtual SExprTypePair outputWrite(const SymbolicExpression::InteriorPtr&);
156  // Create a set expression that represents a set of bit vectors all the same size. */
157  virtual SExprTypePair outputSet(const SymbolicExpression::InteriorPtr&);
159  // Functions that generate SMT-LIB output to a stream when given a Rose::BinaryAnalysis::SymbolicExpression
160  virtual void outputVariableDeclarations(std::ostream&, const VariableSet&);
161  virtual void outputComments(std::ostream&, const std::vector<SymbolicExpression::Ptr>&);
162  virtual void outputCommonSubexpressions(std::ostream&, const std::vector<SymbolicExpression::Ptr>&);
163  virtual void outputAssertion(std::ostream&, const SymbolicExpression::Ptr&);
164 };
166 } // namespace
167 } // namespace
169 #endif
170 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:45
Sawyer::Container::Set< SymbolicExpression::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
Definition: SmtSolver.h:178
virtual std::string getErrorMessage(int exitStatus) override
Error message from running a solver executable.
virtual void findVariables(const SymbolicExpression::Ptr &, VariableSet &) override
Return all variables that need declarations.
virtual void parseEvidence() override
Parses evidence of satisfiability.
Holds a value or nothing.
Definition: Optional.h:49
const std::string & name() const
Property: Name of solver for debugging.
Definition: SmtSolver.h:404
virtual void timeout(boost::chrono::duration< double >) override
Set the timeout for the solver.
Main namespace for the ROSE library.
std::set< uint64_t > Definitions
Free variables that have been defined.
Definition: SmtSolver.h:180
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
Definition: SmtSolver.h:359
virtual void reset() override
Reset solver state.
void varForSet(const SymbolicExpression::InteriorPtr &set, const SymbolicExpression::LeafPtr &var)
Specify variable to use for OP_SET.
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:41
An executable is available.
Definition: SmtSolver.h:54
virtual void outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &)
Generate functions for comparison of bitvectors.
Type (sort) of expression.
Definition: SmtSolver.h:63
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SmtSolver.h:39
virtual std::string getCommand(const std::string &configName) override
Given the name of a configuration file, return the command that is needed to run the solver...
virtual Ptr create() const override
Virtual constructor.
virtual void outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &)
Generate definitions for bit-wise XOR functions.