ROSE  0.9.11.155
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()
100  : ncalls(0), input_size(0), output_size(0), memoizationHits(0), nSolversCreated(0), nSolversDestroyed(0),
101  prepareTime(0.0), solveTime(0.0), evidenceTime(0.0) {
102  }
103  };
104 
117  class Transaction {
118  SmtSolver::Ptr solver_;
119  size_t nLevels_;
120  bool committed_;
121  public:
126  : solver_(solver), committed_(false) {
127  if (solver) {
128  nLevels_ = solver->nLevels();
129  solver->push();
130  } else {
131  nLevels_ = 0;
132  }
133  }
134 
137  if (solver_ && !committed_) {
138  ASSERT_require2(solver_->nLevels() > nLevels_, "something popped this transaction already");
139  while (solver_->nLevels() > nLevels_) {
140  if (solver_->nLevels() > 1) {
141  solver_->pop();
142  } else {
143  solver_->reset();
144  }
145  }
146  }
147  }
148 
150  void commit(bool b = true) {
151  committed_ = b;
152  }
153 
155  bool isCommitted() const {
156  return committed_;
157  }
158 
161  return solver_;
162  }
163  };
164 
167 
168  typedef std::set<uint64_t> Definitions;
172  public:
173  typedef Sawyer::SharedPointer<SExpr> Ptr;
174  private:
175  explicit SExpr(const std::string &content): content_(content) {}
176  std::string content_;
177  std::vector<Ptr> children_;
178  public:
179  static Ptr instance(const std::string &content); // leaf node
180  static Ptr instance(size_t); // integer leaf node
181  static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());
182 
183  const std::string name() const { return content_; }
184  const std::vector<Ptr>& children() const { return children_; }
185  std::vector<Ptr>& children() { return children_; }
186  void append(const std::vector<Ptr>&);
187  void print(std::ostream&) const;
188  };
189 
190  typedef std::pair<SExpr::Ptr, Type> SExprTypePair;
191 
192  typedef boost::unordered_map<SymbolicExpr::Hash, Satisfiable> Memoization;
193 
194 private:
195  std::string name_;
196  std::vector<std::vector<SymbolicExpr::Ptr> > stack_;
197  bool errorIfReset_;
198 
199 protected:
200  LinkMode linkage_;
201  std::string outputText_;
202  std::vector<SExpr::Ptr> parsedOutput_; // the evidence output
203  TermNames termNames_; // maps ROSE exprs to SMT exprs and their basic type
204  Memoization memoization_; // cached of previously computed results
205  bool doMemoization_; // use the memoization_ table?
206  SymbolicExpr::Hash latestMemoizationId_; // key for last found or inserted memoization, or zero
207  SymbolicExpr::ExprExprHashMap latestMemoizationRewrite_; // variables rewritten, need to be undone when parsing evidence
208 
209  // Statistics
210  static boost::mutex classStatsMutex;
211  static Stats classStats; // all access must be protected by classStatsMutex
212  Stats stats;
213 
214 public:
216  static Sawyer::Message::Facility mlog;
217 
218 private:
219 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
220  friend class boost::serialization::access;
221 
222  template<class S>
223  void serialize(S &s, const unsigned /*version*/) {
224  s & BOOST_SERIALIZATION_NVP(name_);
225  s & BOOST_SERIALIZATION_NVP(stack_);
226  // linkage_ -- not serialized
227  // termNames_ -- not serialized
228  // outputText_ -- not serialized
229  // parsedOutput_ -- not serialized
230  // termNames_ -- not serialized
231  // memoization_ -- not serialized
232  // doMemoization_ -- not serialized
233  // latestMemoizationId_ -- not serialized
234  // latestMemoizationRewrite_ -- not serialized
235  // classStatsMutex -- not serialized
236  // classStats -- not serialized
237  // stats -- not serialized
238  // mlog -- not serialized
239  }
240 #endif
241 
242 protected:
251  SmtSolver(const std::string &name, unsigned linkages)
252  : name_(name), errorIfReset_(false), linkage_(LM_NONE), doMemoization_(true), latestMemoizationId_(0) {
253  init(linkages);
254  }
255 
256 public:
258  virtual Ptr create() const = 0;
259 
260  // Solvers are reference counted and should not be explicitly deleted.
261  virtual ~SmtSolver();
262 
263 
265  // Methods for creating solvers.
267 public:
268 
273  static Availability availability();
274 
281  static Ptr instance(const std::string &name);
282 
286  static Ptr bestAvailable();
287 
294  const std::string& name() const { return name_; }
295  void name(const std::string &s) { name_ = s; }
301  LinkMode linkage() const {
302  return linkage_;
303  }
304 
308  void requireLinkage(LinkMode) const;
309 
313  static LinkMode bestLinkage(unsigned linkages);
314 
320  bool memoization() const { return doMemoization_; }
321  void memoization(bool b) {
322  doMemoization_ = b;
323  if (!b)
325  }
330  return latestMemoizationId_;
331  }
332 
334  virtual void clearMemoization() {
335  memoization_.clear();
336  }
337 
339  virtual size_t memoizationNEntries() const {
340  return memoization_.size();
341  }
342 
343 
345  // High-level abstraction for testing satisfiability.
347 public:
348 
356  virtual Satisfiable triviallySatisfiable(const std::vector<SymbolicExpr::Ptr> &exprs);
357 
365  virtual Satisfiable satisfiable(const SymbolicExpr::Ptr&);
366  virtual Satisfiable satisfiable(const std::vector<SymbolicExpr::Ptr>&);
370  // Mid-level abstractions for testing satisfiaiblity.
373 public:
374 
379  virtual void reset();
380 
387  bool errorIfReset() const {
388  return errorIfReset_;
389  }
390  void errorIfReset(bool b) {
391  errorIfReset_ = b;
392  }
404  virtual void push();
405 
412  virtual void pop();
413 
418  virtual size_t nLevels() const { return stack_.size(); }
419 
423  virtual size_t nAssertions(size_t backtrackingLevel);
424 
426  virtual size_t nAssertions() const;
427 
433  virtual void insert(const SymbolicExpr::Ptr&);
434  virtual void insert(const std::vector<SymbolicExpr::Ptr>&);
440  virtual std::vector<SymbolicExpr::Ptr> assertions() const;
441 
446  virtual std::vector<SymbolicExpr::Ptr> assertions(size_t level) const;
447 
452  virtual Satisfiable check();
453 
459  virtual Satisfiable checkTrivial();
460 
461 
463  // High-level abstraction for solver results.
465 public:
466 
474  virtual std::vector<std::string> evidenceNames() {
475  return std::vector<std::string>();
476  }
477 
483  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) {
484  return SymbolicExpr::Ptr();
485  }
486 
487 
489  // Mid-level abstraction for solver results.
491 public:
492 
498  virtual void clearEvidence();
499 
507  SymbolicExpr::LeafPtr ln = var->isLeafNode();
508  ASSERT_require(ln && ln->isVariable2());
509  return evidenceForVariable(ln->nameId());
510  }
511  virtual SymbolicExpr::Ptr evidenceForVariable(uint64_t varno) {
512  char buf[64];
513  snprintf(buf, sizeof buf, "v%" PRIu64, varno);
514  return evidenceForName(buf);
515  }
523  virtual SymbolicExpr::Ptr evidenceForAddress(uint64_t addr);
524 
525 
527  // Statistics
529 public:
530 
534  const Stats& statistics() const { return stats; }
535 
542  static Stats classStatistics();
543 
545  void resetStatistics();
546 
551  static void resetClassStatistics();
552 
553 
555  // Low-level API used in subclasses.
557 protected:
559  virtual Satisfiable checkExe();
560 
562  virtual Satisfiable checkLib();
563 
569  virtual std::string getErrorMessage(int exitStatus);
570 
572  virtual void findVariables(const SymbolicExpr::Ptr&, VariableSet&) {}
573 
578  static void printSExpression(std::ostream&, const SExpr::Ptr&);
579 
583  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) = 0;
584 
587  virtual std::string getCommand(const std::string &config_name) = 0;
588 
590  std::vector<SExpr::Ptr> parseSExpressions(const std::string&);
591 
594  virtual void parseEvidence() {};
595 
602  static std::vector<SymbolicExpr::Ptr> normalizeVariables(const std::vector<SymbolicExpr::Ptr>&,
603  SymbolicExpr::ExprExprHashMap &index /*out*/);
604 
612  static std::vector<SymbolicExpr::Ptr> undoNormalization(const std::vector<SymbolicExpr::Ptr>&,
613  const SymbolicExpr::ExprExprHashMap &index);
614 
615 
617  // Miscellaneous
619 public:
621  virtual void selfTest();
622 
626  static void initDiagnostics();
627 
628 private:
629  void init(unsigned linkages); // Called during construction
630 
631 
632 
634  // Deprecated junk
636 
637  // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
638 public:
639  virtual Satisfiable trivially_satisfiable(const std::vector<SymbolicExpr::Ptr> &exprs)
640  ROSE_DEPRECATED("use triviallySatisfiable");
641  virtual SymbolicExpr::Ptr evidence_for_variable(uint64_t varno) ROSE_DEPRECATED("use evidenceForVariable");
642  virtual SymbolicExpr::Ptr evidence_for_variable(const SymbolicExpr::Ptr &var) ROSE_DEPRECATED("use evidenceForVariable");
643  virtual SymbolicExpr::Ptr evidence_for_name(const std::string&) ROSE_DEPRECATED("use evidenceForName");
644  virtual SymbolicExpr::Ptr evidence_for_address(uint64_t addr) ROSE_DEPRECATED("use evidenceForAddress");
645  virtual std::vector<std::string> evidence_names() ROSE_DEPRECATED("use evidenceNames");
646  virtual void clear_evidence() ROSE_DEPRECATED("use clearEvidence");
647  const Stats& get_stats() const ROSE_DEPRECATED("use statistics");
648  static Stats get_class_stats() ROSE_DEPRECATED("use classStatistics");
649  void reset_stats() ROSE_DEPRECATED("use resetStatistics");
650  void reset_class_stats() ROSE_DEPRECATED("use resetClassStatistics");
651 protected:
652  virtual void generate_file(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*)
653  ROSE_DEPRECATED("use generateFile");
654  virtual std::string get_command(const std::string &config_name) ROSE_DEPRECATED("use getCommand");
655  virtual void parse_evidence() ROSE_DEPRECATED("use parseEvidence");
656 };
657 
658 std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);
659 
660 // FIXME[Robb Matzke 2017-10-17]: This typedef is deprecated. Use SmtSolver instead.
661 typedef SmtSolver SMTSolver;
662 
663 } // namespace
664 } // namespace
665 
666 #endif
virtual void push()
Create a backtracking point.
bool isCommitted() const
Whether the guard is canceled.
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.
Mapping from expression to expression.
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.
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.
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 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.
bool errorIfReset() const
Property: Throw an exception if the solver is reset.
virtual size_t nAssertions() const
Total number of assertions across all backtracking levels.
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.
virtual Ptr create() const =0
Virtual constructor.
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 void findVariables(const SymbolicExpr::Ptr &, VariableSet &)
Return all variables that need declarations.
void errorIfReset(bool b)
Property: Throw an exception if the solver is reset.
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.
~Transaction()
Destructor pops level unless canceled.
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.
void commit(bool b=true)
Cancel the popping during the destructor.
virtual Satisfiable triviallySatisfiable(const std::vector< SymbolicExpr::Ptr > &exprs)
Determines if expressions are trivially satisfiable or unsatisfiable.
Transaction(const SmtSolver::Ptr &solver)
Constructor pushes level if solver is non-null.
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:64
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.
SmtSolver::Ptr solver() const
Solver being protected.
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'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.