ROSE  0.11.98.0
SmtlibSolver.h
1 #ifndef ROSE_BinaryAnalysis_SmtlibSolver_H
2 #define ROSE_BinaryAnalysis_SmtlibSolver_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/SmtSolver.h>
7 #include <boost/filesystem.hpp>
8 #include <boost/unordered_map.hpp>
9 
10 namespace Rose {
11 namespace BinaryAnalysis {
12 
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
19 
20 protected:
21  Sawyer::Optional<boost::chrono::duration<double> > timeout_; // max time for solving a single set of equations in seconds
22 
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) {}
28 
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  }
45 
46  virtual Ptr create() const override;
47 
48 public:
49  virtual void reset() override;
50  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::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 SymbolicExpr::Ptr&, VariableSet&) override;
54  virtual void timeout(boost::chrono::duration<double>) override;
55 
56 protected:
63  void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
67  virtual void parseEvidence() override;
68 
73  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
74 
76  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
77 
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>&);
81 
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);
85 
86  virtual std::string typeName(const SymbolicExpr::Ptr&);
87 
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 SymbolicExpr::Ptr&);
93  virtual std::vector<SmtSolver::SExprTypePair> outputExpressions(const std::vector<SymbolicExpr::Ptr>&);
94 
95  // Create an SMT expression from a ROSE symbolic leaf node (constant, variable, or memory state).
96  virtual SExprTypePair outputLeaf(const SymbolicExpr::LeafPtr&);
97 
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 SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
102  virtual SExprTypePair outputLeftAssoc(const std::string &func, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
103 
104  // Create an expression that does a shift operation.
105  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
106  virtual SExprTypePair outputLogicalShiftRight0(const SymbolicExpr::InteriorPtr&);
107  virtual SExprTypePair outputLogicalShiftRight1(const SymbolicExpr::InteriorPtr&);
108  virtual SExprTypePair outputShiftLeft0(const SymbolicExpr::InteriorPtr&);
109  virtual SExprTypePair outputShiftLeft1(const SymbolicExpr::InteriorPtr&);
110 
111  // Create a rotate expression. */
112  virtual SExprTypePair outputRotateLeft(const SymbolicExpr::InteriorPtr&);
113  virtual SExprTypePair outputRotateRight(const SymbolicExpr::InteriorPtr&);
114 
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 SymbolicExpr::InteriorPtr&);
118 
119  // Create a binary expression. This is a special case of outputLeftAssoc.
120  virtual SExprTypePair outputBinary(const std::string &func, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
121 
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);
124 
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 SymbolicExpr::InteriorPtr&);
127 
128  // Create a widening expression that returns a bit vector type. */
129  virtual SExprTypePair outputSignExtend(const SymbolicExpr::InteriorPtr&);
130  virtual SExprTypePair outputUnsignedExtend(const SymbolicExpr::InteriorPtr&);
131 
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 SymbolicExpr::InteriorPtr&);
135 
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 SymbolicExpr::InteriorPtr&);
139 
140  // Create a comparison expression for bit vectors. Return type is Boolean. */
141  virtual SExprTypePair outputSignedCompare(const SymbolicExpr::InteriorPtr&);
142  virtual SExprTypePair outputUnsignedCompare(const SymbolicExpr::InteriorPtr&);
143  virtual SExprTypePair outputZerop(const SymbolicExpr::InteriorPtr&);
144 
145  // Create multiplicative expression. */
146  virtual SExprTypePair outputMultiply(const SymbolicExpr::InteriorPtr&);
147  virtual SExprTypePair outputDivide(const SymbolicExpr::InteriorPtr&, const std::string &operation);
148  virtual SExprTypePair outputModulo(const SymbolicExpr::InteriorPtr&, const std::string &operation);
149 
150  // Create a memory read expression. The return type is a bit vector. */
151  virtual SExprTypePair outputRead(const SymbolicExpr::InteriorPtr&);
152 
153  // Create a memory write operation. The return value is a memory state. */
154  virtual SExprTypePair outputWrite(const SymbolicExpr::InteriorPtr&);
155 
156  // Create a set expression that represents a set of bit vectors all the same size. */
157  virtual SExprTypePair outputSet(const SymbolicExpr::InteriorPtr&);
158 
159  // Functions that generate SMT-LIB output to a stream when given a Rose::BinaryAnalysis::SymbolicExpr
160  virtual void outputVariableDeclarations(std::ostream&, const VariableSet&);
161  virtual void outputComments(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
162  virtual void outputCommonSubexpressions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
163  virtual void outputAssertion(std::ostream&, const SymbolicExpr::Ptr&);
164 };
165 
166 } // namespace
167 } // namespace
168 
169 #endif
170 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:45
void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var)
Specify variable to use for OP_SET.
virtual std::string getErrorMessage(int exitStatus) override
Error message from running a solver executable.
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
Definition: SmtSolver.h:178
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
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:359
virtual void reset() override
Reset solver state.
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
Binary analysis.
An executable is available.
Definition: SmtSolver.h:54
Type
Type (sort) of expression.
Definition: SmtSolver.h:63
virtual void findVariables(const SymbolicExpr::Ptr &, VariableSet &) override
Return all variables that need declarations.
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 void outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
Generate functions for comparison of bitvectors.
virtual Ptr create() const override
Virtual constructor.