ROSE  0.9.10.2
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/noncopyable.hpp>
11 #include <boost/serialization/access.hpp>
12 #include <boost/thread/mutex.hpp>
13 #include <boost/unordered_map.hpp>
14 #include <inttypes.h>
15 #include <Sawyer/SharedObject.h>
16 #include <Sawyer/SharedPointer.h>
17 
18 namespace Rose {
19 namespace BinaryAnalysis {
20 
23 
25 public:
26  bool operator()(const SymbolicExpr::LeafPtr&, const SymbolicExpr::LeafPtr&) const;
27 };
28 
33 class SmtSolver: public Sawyer::SharedObject, private boost::noncopyable {
34 public:
37 
39  typedef std::map<std::string, bool> Availability;
40 
42  enum LinkMode {
43  LM_NONE = 0x0000,
44  LM_LIBRARY = 0x0001,
45  LM_EXECUTABLE = 0x0002,
46  LM_ANY = 0x0003,
47  };
48 
54  enum Type { NO_TYPE, BOOLEAN, BIT_VECTOR, MEM_STATE };
55 
57  typedef std::pair<std::string, Type> StringTypePair;
59 
62 
64  struct Exception: std::runtime_error {
65  Exception(const std::string &mesg): std::runtime_error(mesg) {}
66  ~Exception() throw () {}
67  };
68 
71  ParseError(const std::pair<size_t /*line*/, size_t /*col*/> &loc, const std::string &mesg)
72  : Exception("input line " + boost::lexical_cast<std::string>(loc.first+1) +
73  " column " + boost::lexical_cast<std::string>(loc.second+1) + ": " + mesg) {}
74  ~ParseError() throw () {}
75  };
76 
78  enum Satisfiable { SAT_NO=0,
81  };
82 
87  struct Stats {
88  size_t ncalls;
89  size_t input_size;
90  size_t output_size;
91  size_t memoizationHits;
92  size_t nSolversCreated;
94  double prepareTime;
95  double solveTime;
96  double evidenceTime;
97  // Remember to add all data members to resetStatistics()
98 
99  Stats()
101  prepareTime(0.0), solveTime(0.0), evidenceTime(0.0) {
102  }
103  };
104 
107 
108  typedef std::set<uint64_t> Definitions;
112  public:
114  private:
115  explicit SExpr(const std::string &content): content_(content) {}
116  std::string content_;
117  std::vector<Ptr> children_;
118  public:
119  static Ptr instance(const std::string &content); // leaf node
120  static Ptr instance(size_t); // integer leaf node
121  static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());
122 
123  const std::string name() const { return content_; }
124  const std::vector<Ptr>& children() const { return children_; }
125  std::vector<Ptr>& children() { return children_; }
126  void append(const std::vector<Ptr>&);
127  void print(std::ostream&) const;
128  };
129 
130  typedef std::pair<SExpr::Ptr, Type> SExprTypePair;
131 
132  typedef boost::unordered_map<SymbolicExpr::Hash, Satisfiable> Memoization;
133 
134 private:
135  std::string name_;
136  std::vector<std::vector<SymbolicExpr::Ptr> > stack_;
137 
138 protected:
139  LinkMode linkage_;
140  std::string outputText_;
141  std::vector<SExpr::Ptr> parsedOutput_; // the evidence output
142  TermNames termNames_; // maps ROSE exprs to SMT exprs and their basic type
143  Memoization memoization_; // cached of previously computed results
144  bool doMemoization_; // use the memoization_ table?
145  SymbolicExpr::Hash latestMemoizationId_; // key for last found or inserted memoization, or zero
146  SymbolicExpr::ExprExprHashMap latestMemoizationRewrite_; // variables rewritten, need to be undone when parsing evidence
147 
148  // Statistics
149  static boost::mutex classStatsMutex;
150  static Stats classStats; // all access must be protected by classStatsMutex
151  Stats stats;
152 
153 public:
156 
157 private:
158 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
159  friend class boost::serialization::access;
160 
161  template<class S>
162  void serialize(S &s, const unsigned /*version*/) {
163  s & BOOST_SERIALIZATION_NVP(name_);
164  s & BOOST_SERIALIZATION_NVP(stack_);
165  // linkage_ -- not serialized
166  // termNames_ -- not serialized
167  // outputText_ -- not serialized
168  // parsedOutput_ -- not serialized
169  // termNames_ -- not serialized
170  // memoization_ -- not serialized
171  // doMemoization_ -- not serialized
172  // latestMemoizationId_ -- not serialized
173  // latestMemoizationRewrite_ -- not serialized
174  // classStatsMutex -- not serialized
175  // classStats -- not serialized
176  // stats -- not serialized
177  // mlog -- not serialized
178  }
179 #endif
180 
181 protected:
190  SmtSolver(const std::string &name, unsigned linkages)
191  : name_(name), linkage_(LM_NONE), doMemoization_(true), latestMemoizationId_(0) {
192  init(linkages);
193  }
194 
195 public:
197  virtual Ptr create() const = 0;
198 
199  // Solvers are reference counted and should not be explicitly deleted.
200  virtual ~SmtSolver();
201 
202 
204  // Methods for creating solvers.
206 public:
207 
212  static Availability availability();
213 
220  static Ptr instance(const std::string &name);
221 
225  static Ptr bestAvailable();
226 
233  const std::string& name() const { return name_; }
234  void name(const std::string &s) { name_ = s; }
240  LinkMode linkage() const {
241  return linkage_;
242  }
243 
247  void requireLinkage(LinkMode) const;
248 
252  static LinkMode bestLinkage(unsigned linkages);
253 
259  bool memoization() const { return doMemoization_; }
260  void memoization(bool b) {
261  doMemoization_ = b;
262  if (!b)
264  }
269  return latestMemoizationId_;
270  }
271 
273  virtual void clearMemoization() {
274  memoization_.clear();
275  }
276 
278  virtual size_t memoizationNEntries() const {
279  return memoization_.size();
280  }
281 
282 
284  // High-level abstraction for testing satisfiability.
286 public:
287 
295  virtual Satisfiable triviallySatisfiable(const std::vector<SymbolicExpr::Ptr> &exprs);
296 
304  virtual Satisfiable satisfiable(const SymbolicExpr::Ptr&);
305  virtual Satisfiable satisfiable(const std::vector<SymbolicExpr::Ptr>&);
309  // Mid-level abstractions for testing satisfiaiblity.
312 public:
313 
318  virtual void reset();
319 
329  virtual void push();
330 
337  virtual void pop();
338 
343  virtual size_t nLevels() const { return stack_.size(); }
344 
348  virtual size_t nAssertions(size_t backtrackingLevel);
349 
355  virtual void insert(const SymbolicExpr::Ptr&);
356  virtual void insert(const std::vector<SymbolicExpr::Ptr>&);
362  virtual std::vector<SymbolicExpr::Ptr> assertions() const;
363 
368  virtual std::vector<SymbolicExpr::Ptr> assertions(size_t level) const;
369 
374  virtual Satisfiable check();
375 
381  virtual Satisfiable checkTrivial();
382 
383 
385  // High-level abstraction for solver results.
387 public:
388 
396  virtual std::vector<std::string> evidenceNames() {
397  return std::vector<std::string>();
398  }
399 
405  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) {
406  return SymbolicExpr::Ptr();
407  }
408 
409 
411  // Mid-level abstraction for solver results.
413 public:
414 
420  virtual void clearEvidence();
421 
429  SymbolicExpr::LeafPtr ln = var->isLeafNode();
430  ASSERT_require(ln && !ln->isNumber());
431  return evidenceForVariable(ln->nameId());
432  }
433  virtual SymbolicExpr::Ptr evidenceForVariable(uint64_t varno) {
434  char buf[64];
435  snprintf(buf, sizeof buf, "v%" PRIu64, varno);
436  return evidenceForName(buf);
437  }
445  virtual SymbolicExpr::Ptr evidenceForAddress(uint64_t addr);
446 
447 
449  // Statistics
451 public:
452 
456  const Stats& statistics() const { return stats; }
457 
464  static Stats classStatistics();
465 
467  void resetStatistics();
468 
473  static void resetClassStatistics();
474 
475 
477  // Low-level API used in subclasses.
479 protected:
481  virtual Satisfiable checkExe();
482 
484  virtual Satisfiable checkLib();
485 
491  virtual std::string getErrorMessage(int exitStatus);
492 
495 
500  static void printSExpression(std::ostream&, const SExpr::Ptr&);
501 
505  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) = 0;
506 
509  virtual std::string getCommand(const std::string &config_name) = 0;
510 
512  std::vector<SExpr::Ptr> parseSExpressions(const std::string&);
513 
516  virtual void parseEvidence() {};
517 
524  static std::vector<SymbolicExpr::Ptr> normalizeVariables(const std::vector<SymbolicExpr::Ptr>&,
525  SymbolicExpr::ExprExprHashMap &index /*out*/);
526 
534  static std::vector<SymbolicExpr::Ptr> undoNormalization(const std::vector<SymbolicExpr::Ptr>&,
535  const SymbolicExpr::ExprExprHashMap &index);
536 
537 
539  // Miscellaneous
541 public:
543  virtual void selfTest();
544 
548  static void initDiagnostics();
549 
550 private:
551  void init(unsigned linkages); // Called during construction
552 
553 
554 
556  // Deprecated junk
558 
559  // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
560 public:
561  virtual Satisfiable trivially_satisfiable(const std::vector<SymbolicExpr::Ptr> &exprs)
562  ROSE_DEPRECATED("use triviallySatisfiable");
563  virtual SymbolicExpr::Ptr evidence_for_variable(uint64_t varno) ROSE_DEPRECATED("use evidenceForVariable");
564  virtual SymbolicExpr::Ptr evidence_for_variable(const SymbolicExpr::Ptr &var) ROSE_DEPRECATED("use evidenceForVariable");
565  virtual SymbolicExpr::Ptr evidence_for_name(const std::string&) ROSE_DEPRECATED("use evidenceForName");
566  virtual SymbolicExpr::Ptr evidence_for_address(uint64_t addr) ROSE_DEPRECATED("use evidenceForAddress");
567  virtual std::vector<std::string> evidence_names() ROSE_DEPRECATED("use evidenceNames");
568  virtual void clear_evidence() ROSE_DEPRECATED("use clearEvidence");
569  const Stats& get_stats() const ROSE_DEPRECATED("use statistics");
570  static Stats get_class_stats() ROSE_DEPRECATED("use classStatistics");
571  void reset_stats() ROSE_DEPRECATED("use resetStatistics");
572  void reset_class_stats() ROSE_DEPRECATED("use resetClassStatistics");
573 protected:
574  virtual void generate_file(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*)
575  ROSE_DEPRECATED("use generateFile");
576  virtual std::string get_command(const std::string &config_name) ROSE_DEPRECATED("use getCommand");
577  virtual void parse_evidence() ROSE_DEPRECATED("use parseEvidence");
578 };
579 
580 std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);
581 
582 // FIXME[Robb Matzke 2017-10-17]: This typedef is deprecated. Use SmtSolver instead.
583 typedef SmtSolver SMTSolver;
584 
585 } // namespace
586 } // namespace
587 
588 #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.
uint64_t Hash
Hash of symbolic expression.
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.
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.
size_t nSolversCreated
Number of solvers created.
Sawyer::Container::Map< SymbolicExpr::Ptr, SymbolicExpr::Ptr > ExprExprMap
Maps one symbolic expression to another.
static Availability availability()
Availability of all known solvers.
virtual Ptr create() const =0
Virtual constructor.
std::set< uint64_t > Definitions
Free variables that have been defined.
Satisfiable
Satisfiability constants.
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
virtual size_t nAssertions(size_t backtrackingLevel)
Number of assertions at a specific backtracking level.
virtual Satisfiable check()
Check satisfiability of current stack.
void resetStatistics()
Resets statistics for this solver.
Sawyer::SharedPointer< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
static std::vector< SymbolicExpr::Ptr > normalizeVariables(const std::vector< SymbolicExpr::Ptr > &, SymbolicExpr::ExprExprHashMap &index)
Normalize expressions by renaming variables.
double prepareTime
Time spent creating assertions before solving.
virtual size_t nLevels() const
Number of backtracking levels.
Exceptions for all things SMT related.
static void resetClassStatistics()
Resets statistics for the class.
std::map< std::string, bool > Availability
Solver availability map.
static Ptr bestAvailable()
Best available solver.
static Ptr instance(const std::string &name)
Allocate a new solver by name.
void name(const std::string &s)
Property: Name of solver for debugging.
virtual VariableSet findVariables(const SymbolicExpr::Ptr &)
Return all variables that need declarations.
SymbolicExpr::Hash latestMemoizationId() const
Id for latest memoized result, or zero.
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.
bool memoization() const
Property: Perform memoization.
virtual Satisfiable checkExe()
Check satisfiability using text files and an executable.
void memoization(bool b)
Property: Perform memoization.
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.
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.
virtual void clearMemoization()
Clear memoization table.
static std::vector< SymbolicExpr::Ptr > undoNormalization(const std::vector< SymbolicExpr::Ptr > &, const SymbolicExpr::ExprExprHashMap &index)
Undo the normalizations that were performed earlier.
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.
size_t nSolversDestroyed
Number of solvers destroyed.
Could not be proved satisfiable or unsatisfiable.
virtual std::vector< SymbolicExpr::Ptr > assertions() const
All assertions.
double evidenceTime
Seconds to retrieve evidence of satisfiability.
virtual Satisfiable satisfiable(const SymbolicExpr::Ptr &)
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
double solveTime
Seconds spent in solver&#39;s solve function.
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.
Sawyer::SharedPointer< SmtSolver > Ptr
Reference counting pointer for SMT solvers.
size_t input_size
Bytes of input generated for satisfiable().
virtual size_t memoizationNEntries() const
Size of memoization table.
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 Sawyer::Message::Facility mlog
Diagnostic facility.
size_t memoizationHits
Number of times memoization supplied a result.
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.