ROSE  0.9.9.168
BinarySmtSolver.h
1 #ifndef Rose_BinaryAnalysis_SmtSolver_H
2 #define Rose_BinaryAnalysis_SmtSolver_H
3 
4 #ifndef __STDC_FORMAT_MACROS
5 #define __STDC_FORMAT_MACROS
6 #endif
7 
8 #include <BinarySymbolicExpr.h>
9 #include <boost/lexical_cast.hpp>
10 #include <boost/serialization/access.hpp>
11 #include <boost/thread/mutex.hpp>
12 #include <inttypes.h>
13 
14 namespace Rose {
15 namespace BinaryAnalysis {
16 
20 class SmtSolver {
21 public:
23  enum LinkMode {
24  LM_NONE = 0x0000,
25  LM_LIBRARY = 0x0001,
26  LM_EXECUTABLE = 0x0002,
27  LM_ANY = 0x0003,
28  };
29 
35  enum Type { NO_TYPE, BOOLEAN, BIT_VECTOR, MEM_STATE };
36 
38  typedef std::pair<std::string, Type> StringTypePair;
40 
43 
45  struct Exception: std::runtime_error {
46  Exception(const std::string &mesg): std::runtime_error(mesg) {}
47  ~Exception() throw () {}
48  };
49 
52  ParseError(const std::pair<size_t /*line*/, size_t /*col*/> &loc, const std::string &mesg)
53  : Exception("input line " + boost::lexical_cast<std::string>(loc.first+1) +
54  " column " + boost::lexical_cast<std::string>(loc.second+1) + ": " + mesg) {}
55  ~ParseError() throw () {}
56  };
57 
59  enum Satisfiable { SAT_NO=0,
62  };
63 
65  struct Stats {
66  Stats(): ncalls(0), input_size(0), output_size(0) {}
67  size_t ncalls;
68  size_t input_size;
69  size_t output_size;
70  };
71 
74 
75  typedef std::set<uint64_t> Definitions;
79  public:
81  private:
82  explicit SExpr(const std::string &content): content_(content) {}
83  std::string content_;
84  std::vector<Ptr> children_;
85  public:
86  static Ptr instance(const std::string &content); // leaf node
87  static Ptr instance(size_t); // integer leaf node
88  static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());
89 
90  const std::string name() const { return content_; }
91  const std::vector<Ptr>& children() const { return children_; }
92  std::vector<Ptr>& children() { return children_; }
93  void append(const std::vector<Ptr>&);
94  void print(std::ostream&) const;
95  };
96 
97  typedef std::pair<SExpr::Ptr, Type> SExprTypePair;
98 
99 private:
100  std::string name_;
101  std::vector<std::vector<SymbolicExpr::Ptr> > stack_;
102 
103 protected:
104  LinkMode linkage_;
105  std::string outputText_;
106  std::vector<SExpr::Ptr> parsedOutput_; // the evidence output
107  TermNames termNames_; // maps ROSE exprs to SMT exprs and their basic type
108 
109 
110  // Statistics
111  static boost::mutex classStatsMutex;
112  static Stats classStats; // all access must be protected by classStatsMutex
113  Stats stats;
114 
115  // Debugging
116  static Sawyer::Message::Facility mlog;
117 
118 private:
119 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
120  friend class boost::serialization::access;
121 
122  template<class S>
123  void serialize(S &s, const unsigned version) {
124  s & BOOST_SERIALIZATION_NVP(name_);
125  s & BOOST_SERIALIZATION_NVP(stack_);
126  // linkage_ -- not serialized
127  // termNames_ -- not serialized
128  // outputText_ -- not serialized
129  // parsedOutput_ -- not serialized
130  // classStatsMutex -- not serialized
131  // classStats -- not serialized
132  // stats -- not serialized
133  // mlog -- not serialized
134  }
135 #endif
136 
137 protected:
146  SmtSolver(const std::string &name, unsigned linkages)
147  : name_(name), linkage_(LM_NONE) {
148  init(linkages);
149  }
150 
151 
153  // Methods for creating solvers.
155 public:
156 
160  static SmtSolver* bestAvailable();
161 
162  virtual ~SmtSolver() {}
163 
170  const std::string& name() const { return name_; }
171  void name(const std::string &s) { name_ = s; }
177  LinkMode linkage() const {
178  return linkage_;
179  }
180 
184  void requireLinkage(LinkMode) const;
185 
189  static LinkMode bestLinkage(unsigned linkages);
190 
191 
193  // High-level abstraction for testing satisfiability.
195 public:
196 
204  virtual Satisfiable triviallySatisfiable(const std::vector<SymbolicExpr::Ptr> &exprs);
205 
213  virtual Satisfiable satisfiable(const SymbolicExpr::Ptr&);
214  virtual Satisfiable satisfiable(const std::vector<SymbolicExpr::Ptr>&);
218  // Mid-level abstractions for testing satisfiaiblity.
221 public:
222 
227  virtual void reset();
228 
238  virtual void push();
239 
246  virtual void pop();
247 
252  virtual size_t nLevels() const { return stack_.size(); }
253 
259  virtual void insert(const SymbolicExpr::Ptr&);
260  virtual void insert(const std::vector<SymbolicExpr::Ptr>&);
266  virtual std::vector<SymbolicExpr::Ptr> assertions() const;
267 
272  virtual std::vector<SymbolicExpr::Ptr> assertions(size_t level) const;
273 
278  virtual Satisfiable check();
279 
285  virtual Satisfiable checkTrivial();
286 
287 
289  // High-level abstraction for solver results.
291 public:
292 
300  virtual std::vector<std::string> evidenceNames() {
301  return std::vector<std::string>();
302  }
303 
309  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) {
310  return SymbolicExpr::Ptr();
311  }
312 
313 
315  // Mid-level abstraction for solver results.
317 public:
318 
324  virtual void clearEvidence();
325 
333  SymbolicExpr::LeafPtr ln = var->isLeafNode();
334  ASSERT_require(ln && !ln->isNumber());
335  return evidenceForVariable(ln->nameId());
336  }
337  virtual SymbolicExpr::Ptr evidenceForVariable(uint64_t varno) {
338  char buf[64];
339  snprintf(buf, sizeof buf, "v%" PRIu64, varno);
340  return evidenceForName(buf);
341  }
349  virtual SymbolicExpr::Ptr evidenceForAddress(uint64_t addr);
350 
351 
353  // Statistics
355 public:
356 
360  const Stats& statistics() const { return stats; }
361 
365  static Stats classStatistics();
366 
368  void resetStatistics() { stats = Stats(); }
369 
374  static void resetClassStatistics();
375 
376 
378  // Low-level API used in subclasses.
380 protected:
382  virtual Satisfiable checkExe();
383 
385  virtual Satisfiable checkLib();
386 
392  virtual std::string getErrorMessage(int exitStatus);
393 
395  virtual VariableSet findVariables(const SymbolicExpr::Ptr&) { return VariableSet(); }
396 
401  static void printSExpression(std::ostream&, const SExpr::Ptr&);
402 
406  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) = 0;
407 
410  virtual std::string getCommand(const std::string &config_name) = 0;
411 
413  std::vector<SExpr::Ptr> parseSExpressions(const std::string&);
414 
417  virtual void parseEvidence() {};
418 
419 
421  // Miscellaneous
423 public:
425  virtual void selfTest();
426 
430  static void initDiagnostics();
431 
432 private:
433  void init(unsigned linkages); // Called during construction
434 
435 
436 
438  // Deprecated junk
440 
441  // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
442 public:
443  virtual Satisfiable trivially_satisfiable(const std::vector<SymbolicExpr::Ptr> &exprs)
444  ROSE_DEPRECATED("use triviallySatisfiable");
445  virtual SymbolicExpr::Ptr evidence_for_variable(uint64_t varno) ROSE_DEPRECATED("use evidenceForVariable");
446  virtual SymbolicExpr::Ptr evidence_for_variable(const SymbolicExpr::Ptr &var) ROSE_DEPRECATED("use evidenceForVariable");
447  virtual SymbolicExpr::Ptr evidence_for_name(const std::string&) ROSE_DEPRECATED("use evidenceForName");
448  virtual SymbolicExpr::Ptr evidence_for_address(uint64_t addr) ROSE_DEPRECATED("use evidenceForAddress");
449  virtual std::vector<std::string> evidence_names() ROSE_DEPRECATED("use evidenceNames");
450  virtual void clear_evidence() ROSE_DEPRECATED("use clearEvidence");
451  const Stats& get_stats() const ROSE_DEPRECATED("use statistics");
452  static Stats get_class_stats() ROSE_DEPRECATED("use classStatistics");
453  void reset_stats() ROSE_DEPRECATED("use resetStatistics");
454  void reset_class_stats() ROSE_DEPRECATED("use resetClassStatistics");
455 protected:
456  virtual void generate_file(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*)
457  ROSE_DEPRECATED("use generateFile");
458  virtual std::string get_command(const std::string &config_name) ROSE_DEPRECATED("use getCommand");
459  virtual void parse_evidence() ROSE_DEPRECATED("use parseEvidence");
460 };
461 
462 std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);
463 
464 // FIXME[Robb Matzke 2017-10-17]: This typedef is deprecated. Use SmtSolver instead.
465 typedef SmtSolver SMTSolver;
466 
467 } // namespace
468 } // namespace
469 
470 #endif
virtual void push()
Create a backtracking point.
Ordered set of values.
Definition: Set.h:46
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
S-Expr parsed from SMT solver text output.
virtual Satisfiable checkLib()
Check satisfiability using a library API.
virtual void clearEvidence()
Clears evidence information.
Satisfiable and evidence of satisfiability may be available.
virtual SymbolicExpr::Ptr evidenceForVariable(const SymbolicExpr::Ptr &var)
Evidence of satisfiability for a bitvector variable.
virtual SymbolicExpr::Ptr evidenceForName(const std::string &)
Evidence of satisfiability for a variable or memory address.
Collection of streams.
Definition: Message.h:1579
virtual void insert(const SymbolicExpr::Ptr &)
Insert assertions.
static void printSExpression(std::ostream &, const SExpr::Ptr &)
Print an S-Expr for debugging.
size_t ncalls
Number of times satisfiable() was called.
void requireLinkage(LinkMode) const
Assert required linkage.
virtual void reset()
Reset solver state.
STL namespace.
std::string outputText_
Additional output obtained by satisfiable().
Small object support.
Definition: SmallObject.h:19
const std::string & name() const
Property: Name of solver for debugging.
LinkMode
Bit flags to indicate the kind of solver interface.
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.
Satisfiable
Satisfiability constants.
Reference-counting smart pointer.
Definition: SharedPointer.h:34
virtual Satisfiable check()
Check satisfiability of current stack.
void resetStatistics()
Resets statistics for this solver.
virtual size_t nLevels() const
Number of backtracking levels.
Exceptions for all things SMT related.
static void resetClassStatistics()
Resets statistics for the class.
void name(const std::string &s)
Property: Name of solver for debugging.
virtual VariableSet findVariables(const SymbolicExpr::Ptr &)
Return all variables that need declarations.
virtual void generateFile(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *)=0
Generates an input file for for the solver.
static void initDiagnostics()
Initialize diagnostic output facilities.
virtual Satisfiable checkExe()
Check satisfiability using text files and an executable.
Exception for parse errors when reading SMT solver output.
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
virtual SymbolicExpr::Ptr evidenceForAddress(uint64_t addr)
Evidence of satisfiability for a memory address.
virtual Satisfiable triviallySatisfiable(const std::vector< SymbolicExpr::Ptr > &exprs)
Determines if expressions are trivially satisfiable or unsatisfiable.
Sawyer::Container::Set< SymbolicExpr::LeafPtr > VariableSet
Set of variables.
virtual void selfTest()
Unit tests.
const Stats & statistics() const
Property: Statistics for this solver.
virtual Satisfiable checkTrivial()
Check whether the stack of assertions is trivially satisfiable.
Base class for reference counted objects.
Definition: SharedObject.h:22
A runtime library is available.
virtual void pop()
Pop a backtracking point.
Type
Type (sort) of expression.
Could not be proved satisfiable or unsatisfiable.
virtual std::vector< SymbolicExpr::Ptr > assertions() const
All assertions.
virtual Satisfiable satisfiable(const SymbolicExpr::Ptr &)
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
virtual std::vector< std::string > evidenceNames()
Names of items for which satisfiability evidence exists.
virtual std::string getCommand(const std::string &config_name)=0
Given the name of a configuration file, return the command that is needed to run the solver...
std::pair< std::string, Type > StringTypePair
Maps expression nodes to term names.
Interface to Satisfiability Modulo Theory (SMT) solvers.
size_t input_size
Bytes of input generated for satisfiable().
virtual void parseEvidence()
Parses evidence of satisfiability.
std::vector< SExpr::Ptr > parseSExpressions(const std::string &)
Parse all SExprs from the specified string.
static Stats classStatistics()
Property: Statistics across all solvers.
static LinkMode bestLinkage(unsigned linkages)
Given a bit vector of linkages, return the best one.
virtual SymbolicExpr::Ptr evidenceForVariable(uint64_t varno)
Evidence of satisfiability for a bitvector variable.
static SmtSolver * bestAvailable()
Best available solver.
LinkMode linkage() const
Property: How ROSE communicates with the solver.
virtual std::string getErrorMessage(int exitStatus)
Error message from running a solver executable.
size_t output_size
Amount of output produced by the SMT solver.