1 #ifndef Rose_BinaryAnalysis_SmtlibSolver_H
2 #define Rose_BinaryAnalysis_SmtlibSolver_H
4 #include <BinarySmtSolver.h>
5 #include <boost/filesystem.hpp>
6 #include <boost/unordered_map.hpp>
8 namespace Rose {
9 namespace BinaryAnalysis {
12 class SmtlibSolver: public SmtSolver {
13 private:
14  boost::filesystem::path executable_; // solver program
15  std::string shellArgs_; // extra arguments for command (passed through shell)
16  ExprExprMap varsForSets_; // variables to use for sets
18 protected:
19  ExprExprMap evidence;
20  typedef boost::unordered_map<SymbolicExpr::Hash, ExprExprMap> MemoizedEvidence;
21  MemoizedEvidence memoizedEvidence;
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  }
49  virtual Ptr create() const ROSE_OVERRIDE {
50  return instance(name(), executable_, shellArgs_, linkage());
51  }
53 public:
54  virtual void reset() ROSE_OVERRIDE;
55  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) ROSE_OVERRIDE;
56  virtual std::string getCommand(const std::string &configName) ROSE_OVERRIDE;
57  virtual std::string getErrorMessage(int exitStatus) ROSE_OVERRIDE;
58  virtual void findVariables(const SymbolicExpr::Ptr&, VariableSet&) ROSE_OVERRIDE;
59  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) ROSE_OVERRIDE;
60  virtual std::vector<std::string> evidenceNames() ROSE_OVERRIDE;
61  virtual void clearEvidence() ROSE_OVERRIDE;
62  virtual void clearMemoization() ROSE_OVERRIDE;
64 protected:
71  void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
72  SymbolicExpr::LeafPtr varForSet(const SymbolicExpr::InteriorPtr &set);
75  virtual void parseEvidence() ROSE_OVERRIDE;
81  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
84  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
86 protected:
87  // Return the most common type (arbitrarily if tied). Returns NO_TYPE when there are no inputs.
88  virtual Type mostType(const std::vector<SExprTypePair>&);
90  // Cast an SMT expression(s) to some other type.
91  virtual SExprTypePair outputCast(const SExprTypePair&, Type to);
92  virtual std::vector<SExprTypePair> outputCast(const std::vector<SExprTypePair>&, Type to);
94  virtual std::string typeName(const SymbolicExpr::Ptr&);
96  // Convert a ROSE symbolic expression to an SMT solver expression. The return value is a pair consisting of an SExpr::Ptr
97  // (ROSE internal representation of an SMT solver expression) and a type indicating whether the SMT solver expression is a
98  // bit vector, a Boolean, or a memory state. Although ROSE uses a bit to represent Booleans, SMT solvers often distinguish
99  // betwen a single bit and a Boolean.
100  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&);
101  virtual std::vector<SmtSolver::SExprTypePair> outputExpressions(const std::vector<SymbolicExpr::Ptr>&);
103  // Create an SMT expression from a ROSE symbolic leaf node (constant, variable, or memory state).
104  virtual SExprTypePair outputLeaf(const SymbolicExpr::LeafPtr&);
106  // Create an expression composed of only 2-argument calls to the specified function. The arguments are all first converted
107  // to the most common argument type (which is usually a no-op since arguments are normally all the same type). If rettype
108  // is NO_TYPE then the returned type is assumed to be the same as the arguments, otherwise it is set as specified.
109  virtual SExprTypePair outputLeftAssoc(const std::string &func, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
110  virtual SExprTypePair outputLeftAssoc(const std::string &func, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
112  // Create an expression that does a shift operation.
113  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
114  virtual SExprTypePair outputLogicalShiftRight(const SymbolicExpr::InteriorPtr&);
115  virtual SExprTypePair outputShiftLeft(const SymbolicExpr::InteriorPtr&);
117  // Create a rotate expression. */
118  virtual SExprTypePair outputRotateLeft(const SymbolicExpr::InteriorPtr&);
119  virtual SExprTypePair outputRotateRight(const SymbolicExpr::InteriorPtr&);
121  // Create an expression that does either a bit-wise or boolean XOR. All arguments must be the same type, either bit vectors
122  // or Booleans, and the return value is the same as the argument type.
123  virtual SExprTypePair outputXor(const SymbolicExpr::InteriorPtr&);
125  // Create a binary expression. This is a special case of outputLeftAssoc.
126  virtual SExprTypePair outputBinary(const std::string &func, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
128  // Create a unary expression. The return type is the same as the argument type.
129  virtual SExprTypePair outputUnary(const std::string &funcName, const SExprTypePair &arg);
131  // Create a bit extraction expression, i.e., a bit vector result which is a sub-array of the input bit vector.
132  virtual SExprTypePair outputExtract(const SymbolicExpr::InteriorPtr&);
134  // Create a widening expression that returns a bit vector type. */
135  virtual SExprTypePair outputSignExtend(const SymbolicExpr::InteriorPtr&);
136  virtual SExprTypePair outputUnsignedExtend(const SymbolicExpr::InteriorPtr&);
138  // Create an if-then-else expression. The arguments should be the same type (one is cast if not) and the return type is the
139  // same as the argument types.
140  virtual SExprTypePair outputIte(const SymbolicExpr::InteriorPtr&);
142  // Create a not-equal expression. The operands can be any type and are cast to a common type before comparing. The return
143  // type is Boolean.
144  virtual SExprTypePair outputNotEqual(const SymbolicExpr::InteriorPtr&);
146  // Create a comparison expression for bit vectors. Return type is Boolean. */
147  virtual SExprTypePair outputSignedCompare(const SymbolicExpr::InteriorPtr&);
148  virtual SExprTypePair outputUnsignedCompare(const SymbolicExpr::InteriorPtr&);
149  virtual SExprTypePair outputZerop(const SymbolicExpr::InteriorPtr&);
151  // Create multiplicative expression. */
152  virtual SExprTypePair outputMultiply(const SymbolicExpr::InteriorPtr&);
153  virtual SExprTypePair outputDivide(const SymbolicExpr::InteriorPtr&, const std::string &operation);
154  virtual SExprTypePair outputModulo(const SymbolicExpr::InteriorPtr&, const std::string &operation);
156  // Create a memory read expression. The return type is a bit vector. */
157  virtual SExprTypePair outputRead(const SymbolicExpr::InteriorPtr&);
159  // Create a memory write operation. The return value is a memory state. */
160  virtual SExprTypePair outputWrite(const SymbolicExpr::InteriorPtr&);
162  // Create a set expression that represents a set of bit vectors all the same size. */
163  virtual SExprTypePair outputSet(const SymbolicExpr::InteriorPtr&);
165  // Functions that generate SMT-LIB output to a stream when given a Rose::BinaryAnalysis::SymbolicExpr
166  virtual void outputVariableDeclarations(std::ostream&, const VariableSet&);
167  virtual void outputComments(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
168  virtual void outputCommonSubexpressions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
169  virtual void outputAssertion(std::ostream&, const SymbolicExpr::Ptr&);
170 };
172 } // namespace
173 } // namespace
175 #endif
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.
STL namespace.
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.
Sawyer::Container::Map< SymbolicExpr::Ptr, SymbolicExpr::Ptr > ExprExprMap
Maps one symbolic expression to another.
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.
Type (sort) of expression.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Sawyer::SharedPointer< SmtSolver > Ptr
Reference counting pointer for 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.