1 #ifndef Rose_BinaryAnalysis_SmtlibSolver_H
2 #define Rose_BinaryAnalysis_SmtlibSolver_H
4 #include <BinarySmtSolver.h>
5 #include <boost/filesystem.hpp>
7 namespace Rose {
8 namespace BinaryAnalysis {
11 class SmtlibSolver: public SmtSolver {
12 private:
13  boost::filesystem::path executable_; // solver program
14  std::string shellArgs_; // extra arguments for command (passed through shell)
15  ExprExprMap varsForSets_; // variables to use for sets
17 protected:
18  ExprExprMap evidence;
20 public:
32  explicit SmtlibSolver(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs = "",
33  unsigned linkages = LM_EXECUTABLE)
34  : SmtSolver(name, linkages), executable_(executable), shellArgs_(shellArgs) {}
36 public:
37  virtual void reset() ROSE_OVERRIDE;
38  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) ROSE_OVERRIDE;
39  virtual std::string getCommand(const std::string &configName) ROSE_OVERRIDE;
40  virtual std::string getErrorMessage(int exitStatus) ROSE_OVERRIDE;
41  virtual VariableSet findVariables(const SymbolicExpr::Ptr&) ROSE_OVERRIDE;
42  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) ROSE_OVERRIDE;
43  virtual std::vector<std::string> evidenceNames() ROSE_OVERRIDE;
44  virtual void clearEvidence() ROSE_OVERRIDE;
46 protected:
53  void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
54  SymbolicExpr::LeafPtr varForSet(const SymbolicExpr::InteriorPtr &set);
57  virtual void parseEvidence() ROSE_OVERRIDE;
63  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
66  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
68 protected:
69  // Return the most common type (arbitrarily if tied). Returns NO_TYPE when there are no inputs.
70  virtual Type mostType(const std::vector<SExprTypePair>&);
72  // Cast an SMT expression(s) to some other type.
73  virtual SExprTypePair outputCast(const SExprTypePair&, Type to);
74  virtual std::vector<SExprTypePair> outputCast(const std::vector<SExprTypePair>&, Type to);
76  virtual std::string typeName(const SymbolicExpr::Ptr&);
78  // Convert a ROSE symbolic expression to an SMT solver expression. The return value is a pair consisting of an SExpr::Ptr
79  // (ROSE internal representation of an SMT solver expression) and a type indicating whether the SMT solver expression is a
80  // bit vector, a Boolean, or a memory state. Although ROSE uses a bit to represent Booleans, SMT solvers often distinguish
81  // betwen a single bit and a Boolean.
82  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&);
83  virtual std::vector<SmtSolver::SExprTypePair> outputExpressions(const std::vector<SymbolicExpr::Ptr>&);
85  // Create an SMT expression from a ROSE symbolic leaf node (constant, variable, or memory state).
86  virtual SExprTypePair outputLeaf(const SymbolicExpr::LeafPtr&);
88  // Create an expression composed of only 2-argument calls to the specified function. The arguments are all first converted
89  // to the most common argument type (which is usually a no-op since arguments are normally all the same type). If rettype
90  // is NO_TYPE then the returned type is assumed to be the same as the arguments, otherwise it is set as specified.
91  virtual SExprTypePair outputLeftAssoc(const std::string &func, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
92  virtual SExprTypePair outputLeftAssoc(const std::string &func, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
94  // Create an expression that does a shift operation.
95  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
96  virtual SExprTypePair outputLogicalShiftRight(const SymbolicExpr::InteriorPtr&);
97  virtual SExprTypePair outputShiftLeft(const SymbolicExpr::InteriorPtr&);
99  // Create a rotate expression. */
100  virtual SExprTypePair outputRotateLeft(const SymbolicExpr::InteriorPtr&);
101  virtual SExprTypePair outputRotateRight(const SymbolicExpr::InteriorPtr&);
103  // Create an expression that does either a bit-wise or boolean XOR. All arguments must be the same type, either bit vectors
104  // or Booleans, and the return value is the same as the argument type.
105  virtual SExprTypePair outputXor(const SymbolicExpr::InteriorPtr&);
107  // Create a binary expression. This is a special case of outputLeftAssoc.
108  virtual SExprTypePair outputBinary(const std::string &func, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
110  // Create a unary expression. The return type is the same as the argument type.
111  virtual SExprTypePair outputUnary(const std::string &funcName, const SExprTypePair &arg);
113  // Create a bit extraction expression, i.e., a bit vector result which is a sub-array of the input bit vector.
114  virtual SExprTypePair outputExtract(const SymbolicExpr::InteriorPtr&);
116  // Create a widening expression that returns a bit vector type. */
117  virtual SExprTypePair outputSignExtend(const SymbolicExpr::InteriorPtr&);
118  virtual SExprTypePair outputUnsignedExtend(const SymbolicExpr::InteriorPtr&);
120  // Create an if-then-else expression. The arguments should be the same type (one is cast if not) and the return type is the
121  // same as the argument types.
122  virtual SExprTypePair outputIte(const SymbolicExpr::InteriorPtr&);
124  // Create a not-equal expression. The operands can be any type and are cast to a common type before comparing. The return
125  // type is Boolean.
126  virtual SExprTypePair outputNotEqual(const SymbolicExpr::InteriorPtr&);
128  // Create a comparison expression for bit vectors. Return type is Boolean. */
129  virtual SExprTypePair outputSignedCompare(const SymbolicExpr::InteriorPtr&);
130  virtual SExprTypePair outputUnsignedCompare(const SymbolicExpr::InteriorPtr&);
131  virtual SExprTypePair outputZerop(const SymbolicExpr::InteriorPtr&);
133  // Create multiplicative expression. */
134  virtual SExprTypePair outputMultiply(const SymbolicExpr::InteriorPtr&);
135  virtual SExprTypePair outputUnsignedDivide(const SymbolicExpr::InteriorPtr&);
136  virtual SExprTypePair outputUnsignedModulo(const SymbolicExpr::InteriorPtr&);
138  // Create a memory read expression. The return type is a bit vector. */
139  virtual SExprTypePair outputRead(const SymbolicExpr::InteriorPtr&);
141  // Create a memory write operation. The return value is a memory state. */
142  virtual SExprTypePair outputWrite(const SymbolicExpr::InteriorPtr&);
144  // Create a set expression that represents a set of bit vectors all the same size. */
145  virtual SExprTypePair outputSet(const SymbolicExpr::InteriorPtr&);
147  // Functions that generate SMT-LIB output to a stream when given a Rose::BinaryAnalysis::SymbolicExpr
148  virtual void outputVariableDeclarations(std::ostream&, const VariableSet&);
149  virtual void outputComments(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
150  virtual void outputCommonSubexpressions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
151  virtual void outputAssertion(std::ostream&, const SymbolicExpr::Ptr&);
152 };
154 } // namespace
155 } // namespace
157 #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.
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.
std::set< uint64_t > Definitions
Free variables that have been defined.
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.
virtual VariableSet findVariables(const SymbolicExpr::Ptr &) ROSE_OVERRIDE
Return all variables that need declarations.
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.
Sawyer::Container::Set< SymbolicExpr::LeafPtr > VariableSet
Set of variables.
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.
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.
Container associating values with keys.
Definition: Sawyer/Map.h:64
SmtlibSolver(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 void parseEvidence() ROSE_OVERRIDE
Parses evidence of satisfiability.