ROSE  0.11.83.2
SmtSolver.h
1 #ifndef ROSE_BinaryAnalysis_SmtSolver_H
2 #define ROSE_BinaryAnalysis_SmtSolver_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #ifndef __STDC_FORMAT_MACROS
7 #define __STDC_FORMAT_MACROS
8 #endif
9 
10 #include <Rose/BinaryAnalysis/SymbolicExpr.h>
11 #include <Rose/Exception.h>
12 #include <Rose/Progress.h>
13 
14 #include <boost/chrono.hpp>
15 #include <boost/lexical_cast.hpp>
16 #include <boost/noncopyable.hpp>
17 #include <boost/serialization/access.hpp>
18 #include <boost/thread/mutex.hpp>
19 #include <inttypes.h>
20 #include <unordered_map>
21 
22 namespace Rose {
23 namespace BinaryAnalysis {
24 
26 using SmtSolverPtr = std::shared_ptr<class SmtSolver>;
27 
29 public:
30  bool operator()(const SymbolicExpr::LeafPtr&, const SymbolicExpr::LeafPtr&) const;
31 };
32 
34 public:
35  bool operator()(const SymbolicExpr::Leaf*, const SymbolicExpr::Leaf*) const;
36 };
37 
42 class SmtSolver: private boost::noncopyable {
43 public:
45  using ExprList = std::vector<SymbolicExpr::Ptr>;
46 
48  using Ptr = SmtSolverPtr;
49 
51  using Availability = std::map<std::string, bool>;
52 
54  enum LinkMode {
55  LM_NONE = 0x0000,
56  LM_LIBRARY = 0x0001,
57  LM_EXECUTABLE = 0x0002,
58  LM_ANY = 0x0003,
59  };
60 
66  enum Type { NO_TYPE, BOOLEAN, BIT_VECTOR, MEM_STATE };
67 
69  using StringTypePair = std::pair<std::string, Type>;
71 
74 
77  Exception(const std::string &mesg): Rose::Exception(mesg) {}
78  ~Exception() throw () {}
79  };
80 
83  ParseError(const std::pair<size_t /*line*/, size_t /*col*/> &loc, const std::string &mesg)
84  : Exception("input line " + boost::lexical_cast<std::string>(loc.first+1) +
85  " column " + boost::lexical_cast<std::string>(loc.second+1) + ": " + mesg) {}
86  ~ParseError() throw () {}
87  };
88 
90  enum Satisfiable { SAT_NO=0,
93  };
94 
99  struct Stats {
100  size_t ncalls = 0;
101  size_t input_size = 0;
102  size_t output_size = 0;
103  size_t memoizationHits = 0;
104  size_t nSolversCreated = 0;
105  size_t nSolversDestroyed = 0;
106  double prepareTime = 0.0;
107  double longestPrepareTime = 0.0;
108  double solveTime = 0.0;
109  double longestSolveTime = 0.0;
110  double evidenceTime = 0.0;
111  double longestEvidenceTime = 0.0;
112  size_t nSatisfied = 0;
113  size_t nUnsatisfied = 0;
114  size_t nUnknown = 0;
115  // Remember to add all data members to SmtSolver::resetStatistics() and SmtSolver::Stats::print()
116 
117  void print(std::ostream&, const std::string &prefix = "") const;
118  };
119 
132  class Transaction {
133  SmtSolver::Ptr solver_;
134  size_t nLevels_;
135  bool committed_;
136  public:
141  : solver_(solver), committed_(false) {
142  if (solver) {
143  nLevels_ = solver->nLevels();
144  solver->push();
145  } else {
146  nLevels_ = 0;
147  }
148  }
149 
152  if (solver_ && !committed_) {
153  ASSERT_require2(solver_->nLevels() > nLevels_, "something popped this transaction already");
154  while (solver_->nLevels() > nLevels_) {
155  if (solver_->nLevels() > 1) {
156  solver_->pop();
157  } else {
158  solver_->reset();
159  }
160  }
161  }
162  }
163 
165  void commit(bool b = true) {
166  committed_ = b;
167  }
168 
170  bool isCommitted() const {
171  return committed_;
172  }
173 
176  return solver_;
177  }
178  };
179 
182 
183  using Definitions = std::set<uint64_t>;
187  public:
189  private:
190  explicit SExpr(const std::string &content): content_(content) {}
191  std::string content_;
192  std::vector<Ptr> children_;
193  public:
194  static Ptr instance(const std::string &content); // leaf node
195  static Ptr instance(size_t); // integer leaf node
196  static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());
197 
198  const std::string name() const { return content_; }
199  const std::vector<Ptr>& children() const { return children_; }
200  std::vector<Ptr>& children() { return children_; }
201  void append(const std::vector<Ptr>&);
202  void print(std::ostream&) const;
203  };
204 
205  using SExprTypePair = std::pair<SExpr::Ptr, Type>;
206 
232  public:
235 
236  /* Return value from @ref find function. */
237  struct Found {
244  explicit operator bool() const {
245  return satisfiable;
246  }
247  };
248 
249  private:
250  using ExprExpr = std::pair<SymbolicExpr::Ptr, SymbolicExpr::Ptr>;
251 
252  // The thing that is memoized
253  struct Record {
254  ExprList assertions; // "find" inputs, sorted and normalized
255  Satisfiable satisfiable; // main output of SMT solver
256  ExprExprMap evidence; // output if satisfied: sorted and normalized
257  };
258 
259  // Mapping from hash of sorted-normalized assertions to the memoization record.
260  using Map = std::multimap<SymbolicExpr::Hash, Record>;
261 
262  private:
263  mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects the following data members
264  Map map_; // memoization records indexed by hash of sorted-normalized assertions
265 
266  protected:
267  Memoizer() {}
268 
269  public:
271  static Ptr instance();
272 
274  void clear();
275 
284  Found find(const ExprList &assertions);
285 
291  ExprExprMap evidence(const Found&) const;
292 
299  void insert(const Found&, Satisfiable, const ExprExprMap &evidence);
300 
302  size_t size() const;
303 
304  public:
305  // Non-synchronized search for the sorted-normalized assertions which have the specified hash.
306  Map::iterator searchNS(SymbolicExpr::Hash, const ExprList &sortedNormalized);
307  };
308 
309 private:
310  std::string name_;
311  std::vector<ExprList> stack_;
312  bool errorIfReset_;
313 
314 protected:
315  LinkMode linkage_;
316  std::string outputText_;
317  std::vector<SExpr::Ptr> parsedOutput_; // the evidence output
318  ExprExprMap evidence_; // evidence for last check() if satisfiable
319  TermNames termNames_; // maps ROSE exprs to SMT exprs and their basic type
320  Memoizer::Ptr memoizer_; // cache of previously computed results
321  Progress::Ptr progress_; // optional progress reporting
322 
323  // Statistics
324  static boost::mutex classStatsMutex;
325  static Stats classStats; // all access must be protected by classStatsMutex
326  Stats stats;
327 
328 public:
331 
332 private:
333 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
334  friend class boost::serialization::access;
335 
336  template<class S>
337  void serialize(S &s, const unsigned /*version*/) {
338  s & BOOST_SERIALIZATION_NVP(name_);
339  s & BOOST_SERIALIZATION_NVP(stack_);
340  // linkage_ -- not serialized
341  // termNames_ -- not serialized
342  // outputText_ -- not serialized
343  // parsedOutput_ -- not serialized
344  // termNames_ -- not serialized
345  // memoizer_ -- not serialized
346  // classStatsMutex -- not serialized
347  // classStats -- not serialized
348  // stats -- not serialized
349  // mlog -- not serialized
350  }
351 #endif
352 
353 protected:
362  SmtSolver(const std::string &name, unsigned linkages)
363  : name_(name), errorIfReset_(false), linkage_(LM_NONE) {
364  init(linkages);
365  }
366 
367 public:
371  virtual Ptr create() const = 0;
372 
373  // Solvers are reference counted and should not be explicitly deleted.
374  virtual ~SmtSolver();
375 
376 
378  // Methods for creating solvers.
380 public:
381 
386  static Availability availability();
387 
394  static Ptr instance(const std::string &name);
395 
399  static Ptr bestAvailable();
400 
407  const std::string& name() const { return name_; }
408  void name(const std::string &s) { name_ = s; }
414  LinkMode linkage() const {
415  return linkage_;
416  }
417 
421  void requireLinkage(LinkMode) const;
422 
426  static LinkMode bestLinkage(unsigned linkages);
427 
435  Memoizer::Ptr memoizer() const;
436  void memoizer(const Memoizer::Ptr&);
442  virtual void timeout(boost::chrono::duration<double> seconds) = 0;
443 
444 
446  // High-level abstraction for testing satisfiability.
448 public:
449 
457  virtual Satisfiable triviallySatisfiable(const ExprList &exprs);
458 
466  virtual Satisfiable satisfiable(const SymbolicExpr::Ptr&);
467  virtual Satisfiable satisfiable(const ExprList&);
471  // Mid-level abstractions for testing satisfiaiblity.
474 public:
475 
480  virtual void reset();
481 
488  bool errorIfReset() const {
489  return errorIfReset_;
490  }
491  void errorIfReset(bool b) {
492  errorIfReset_ = b;
493  }
505  virtual void push();
506 
513  virtual void pop();
514 
519  virtual size_t nLevels() const { return stack_.size(); }
520 
524  virtual size_t nAssertions(size_t backtrackingLevel);
525 
527  virtual size_t nAssertions() const;
528 
534  virtual void insert(const SymbolicExpr::Ptr&);
535  virtual void insert(const ExprList&);
541  virtual ExprList assertions() const;
542 
547  virtual const ExprList& assertions(size_t level) const;
548 
553  virtual Satisfiable check();
554 
560  virtual Satisfiable checkTrivial();
561 
562 
564  // High-level abstraction for solver results.
566 public:
567 
569  using Evidence = Sawyer::Container::Map<std::string /*variable name*/, SymbolicExpr::Ptr /*value*/>;
570 
578  virtual std::vector<std::string> evidenceNames() const;
579 
585  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) const;
586 
598  Evidence evidenceByName() const;
599  ExprExprMap evidence() const;
602  // Mid-level abstraction for solver results.
605 public:
606 
612  virtual void clearEvidence();
613 
620  virtual SymbolicExpr::Ptr evidenceForVariable(const SymbolicExpr::Ptr &var) {
621  SymbolicExpr::LeafPtr ln = var->isLeafNode();
622  ASSERT_require(ln && ln->isVariable2());
623  return evidenceForVariable(ln->nameId());
624  }
625  virtual SymbolicExpr::Ptr evidenceForVariable(uint64_t varno) {
626  char buf[64];
627  snprintf(buf, sizeof buf, "v%" PRIu64, varno);
628  return evidenceForName(buf);
629  }
637  virtual SymbolicExpr::Ptr evidenceForAddress(uint64_t addr);
638 
639 
641  // Statistics
643 public:
644 
648  const Stats& statistics() const { return stats; }
649 
656  static Stats classStatistics();
657 
659  void resetStatistics();
660 
665  static void resetClassStatistics();
666 
672  Progress::Ptr progress() const;
673  void progress(const Progress::Ptr &progress);
677  // Low-level API used in subclasses and sometimes for debugging
680 public:
689  virtual void generateFile(std::ostream&, const ExprList &exprs, Definitions*) = 0;
690 
691 protected:
693  virtual Satisfiable checkExe();
694 
696  virtual Satisfiable checkLib();
697 
703  virtual std::string getErrorMessage(int exitStatus);
704 
706  virtual void findVariables(const SymbolicExpr::Ptr&, VariableSet&) {}
707 
712  static void printSExpression(std::ostream&, const SExpr::Ptr&);
713 
716  virtual std::string getCommand(const std::string &config_name) = 0;
717 
719  std::vector<SExpr::Ptr> parseSExpressions(const std::string&);
720 
723  virtual void parseEvidence() {};
724 
731  static ExprList normalizeVariables(const ExprList&, SymbolicExpr::ExprExprHashMap &index /*out*/);
732 
741 
742 
744  // Miscellaneous
746 public:
748  virtual void selfTest();
749 
753  static void initDiagnostics();
754 
755 private:
756  void init(unsigned linkages); // Called during construction
757 };
758 
759 std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);
760 
761 } // namespace
762 } // namespace
763 
764 #endif
765 #endif
virtual void push()
Create a backtracking point.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:48
virtual Satisfiable triviallySatisfiable(const ExprList &exprs)
Determines if expressions are trivially satisfiable or unsatisfiable.
bool isCommitted() const
Whether the guard is canceled.
Definition: SmtSolver.h:170
Ordered set of values.
Definition: Set.h:52
ExprExprMap evidence() const
All evidence of satisfiability.
Sawyer::Optional< Satisfiable > satisfiable
If found, whether satisfiable.
Definition: SmtSolver.h:238
Memoizer::Ptr memoizer() const
Property: Memoizer.
S-Expr parsed from SMT solver text output.
Definition: SmtSolver.h:186
uint64_t Hash
Hash of symbolic expression.
Definition: SymbolicExpr.h:181
Leaf node of an expression tree for instruction semantics.
virtual Satisfiable checkLib()
Check satisfiability using a library API.
double longestPrepareTime
Longest of times added to prepareTime.
Definition: SmtSolver.h:107
virtual void clearEvidence()
Clears evidence information.
Satisfiable and evidence of satisfiability may be available.
Definition: SmtSolver.h:91
virtual SymbolicExpr::Ptr evidenceForVariable(const SymbolicExpr::Ptr &var)
Evidence of satisfiability for a bitvector variable.
Definition: SmtSolver.h:620
Mapping from expression to expression.
Definition: SymbolicExpr.h:939
Collection of streams.
Definition: Message.h:1606
Sawyer::SharedPointer< Memoizer > Ptr
Reference counting pointer.
Definition: SmtSolver.h:234
virtual void insert(const SymbolicExpr::Ptr &)
Insert assertions.
size_t nUnsatisfied
Number of times the solver returned "unsatisfied".
Definition: SmtSolver.h:113
static void printSExpression(std::ostream &, const SExpr::Ptr &)
Print an S-Expr for debugging.
double longestEvidenceTime
Longest of times added to evidenceTime.
Definition: SmtSolver.h:111
size_t ncalls
Number of times satisfiable() was called.
Definition: SmtSolver.h:100
void requireLinkage(LinkMode) const
Assert required linkage.
Memoizes calls to an SMT solver.
Definition: SmtSolver.h:231
virtual void timeout(boost::chrono::duration< double > seconds)=0
Set the timeout for the solver.
void clear()
Clear the entire cache as if it was just constructed.
virtual void reset()
Reset solver state.
ExprExprMap evidence
Normalized evidence if found and satisfiable.
Definition: SmtSolver.h:241
std::string outputText_
Additional output obtained by satisfiable().
Definition: SmtSolver.h:316
Small object support.
Definition: SmallObject.h:19
static Ptr instance()
Allocating constructor.
const std::string & name() const
Property: Name of solver for debugging.
Definition: SmtSolver.h:407
LinkMode
Bit flags to indicate the kind of solver interface.
Definition: SmtSolver.h:54
Main namespace for the ROSE library.
size_t nSolversCreated
Number of solvers created.
Definition: SmtSolver.h:104
virtual SymbolicExpr::Ptr evidenceForName(const std::string &) const
Evidence of satisfiability for a variable or memory address.
static Availability availability()
Availability of all known solvers.
Satisfiable
Satisfiability constants.
Definition: SmtSolver.h:90
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
virtual Satisfiable check()
Check satisfiability of current stack.
void resetStatistics()
Resets statistics for this solver.
size_t nSatisfied
Number of times the solver returned "satisified".
Definition: SmtSolver.h:112
double prepareTime
Total time in seconds spent creating assertions before solving.
Definition: SmtSolver.h:106
bool errorIfReset() const
Property: Throw an exception if the solver is reset.
Definition: SmtSolver.h:488
virtual size_t nAssertions() const
Total number of assertions across all backtracking levels.
virtual size_t nLevels() const
Number of backtracking levels.
Definition: SmtSolver.h:519
Exceptions for all things SMT related.
Definition: SmtSolver.h:76
static void resetClassStatistics()
Resets statistics for the class.
Progress::Ptr progress() const
Progress reporting object.
virtual Ptr create() const =0
Virtual constructor.
std::set< uint64_t > Definitions
Free variables that have been defined.
Definition: SmtSolver.h:183
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.
Definition: SmtSolver.h:408
virtual void findVariables(const SymbolicExpr::Ptr &, VariableSet &)
Return all variables that need declarations.
Definition: SmtSolver.h:706
void errorIfReset(bool b)
Property: Throw an exception if the solver is reset.
Definition: SmtSolver.h:491
ExprExprMap evidence(const Found &) const
Returns evidence of satisfiability.
static void initDiagnostics()
Initialize diagnostic output facilities.
SymbolicExpr::ExprExprHashMap rewriteMap
Mapping from provided to sortedNormalized assertions.
Definition: SmtSolver.h:240
std::map< std::string, bool > Availability
Solver availability map.
Definition: SmtSolver.h:51
virtual Satisfiable checkExe()
Check satisfiability using text files and an executable.
~Transaction()
Destructor pops level unless canceled.
Definition: SmtSolver.h:151
double longestSolveTime
Longest of times added to the solveTime total.
Definition: SmtSolver.h:109
SMT solver statistics.
Definition: SmtSolver.h:99
Exception for parse errors when reading SMT solver output.
Definition: SmtSolver.h:82
Found find(const ExprList &assertions)
Search for the specified assertions in the cache.
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
Definition: SmtSolver.h:362
size_t size() const
Number of call records cached.
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.
Definition: SmtSolver.h:165
Sawyer::Container::Map< SymbolicExpr::Ptr, SymbolicExpr::Ptr > ExprExprMap
Maps one symbolic expression to another.
Definition: SmtSolver.h:73
Extends std::map with methods that return optional values.
Definition: Map.h:10
Transaction(const SmtSolver::Ptr &solver)
Constructor pushes level if solver is non-null.
Definition: SmtSolver.h:140
std::vector< SymbolicExpr::Ptr > ExprList
Ordered list of expressions.
Definition: SmtSolver.h:45
virtual void selfTest()
Unit tests.
const Stats & statistics() const
Property: Statistics for this solver.
Definition: SmtSolver.h:648
virtual void generateFile(std::ostream &, const ExprList &exprs, Definitions *)=0
Generates an input file for for the solver.
Evidence evidenceByName() const
All evidence of satisfiability.
virtual Satisfiable checkTrivial()
Check whether the stack of assertions is trivially satisfiable.
An executable is available.
Definition: SmtSolver.h:57
virtual ExprList assertions() const
All assertions.
Base class for reference counted objects.
Definition: SharedObject.h:64
A runtime library is available.
Definition: SmtSolver.h:56
virtual void pop()
Pop a backtracking point.
Type
Type (sort) of expression.
Definition: SmtSolver.h:66
size_t nSolversDestroyed
Number of solvers destroyed.
Definition: SmtSolver.h:105
Could not be proved satisfiable or unsatisfiable.
Definition: SmtSolver.h:92
SmtSolver::Ptr solver() const
Solver being protected.
Definition: SmtSolver.h:175
void insert(const Found &, Satisfiable, const ExprExprMap &evidence)
Insert a call record into the cache.
double evidenceTime
Total time in seconds to retrieve evidence of satisfiability.
Definition: SmtSolver.h:110
static ExprList normalizeVariables(const ExprList &, SymbolicExpr::ExprExprHashMap &index)
Normalize expressions by renaming variables.
virtual Satisfiable satisfiable(const SymbolicExpr::Ptr &)
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
double solveTime
Total time in seconds spent in solver's solve function.
Definition: SmtSolver.h:108
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...
ExprList sortedNormalized
Sorted and normalized assertions, regardless if found.
Definition: SmtSolver.h:239
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SmtSolver.h:42
size_t input_size
Bytes of input generated for satisfiable().
Definition: SmtSolver.h:101
Base class for all ROSE exceptions.
Definition: Rose/Exception.h:9
virtual void parseEvidence()
Parses evidence of satisfiability.
Definition: SmtSolver.h:723
std::vector< SExpr::Ptr > parseSExpressions(const std::string &)
Parse all SExprs from the specified string.
Provably unsatisfiable.
Definition: SmtSolver.h:90
std::pair< std::string, Type > StringTypePair
Maps expression nodes to term names.
Definition: SmtSolver.h:69
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.
Definition: SmtSolver.h:625
static Sawyer::Message::Facility mlog
Diagnostic facility.
Definition: SmtSolver.h:330
virtual std::vector< std::string > evidenceNames() const
Names of items for which satisfiability evidence exists.
static ExprList undoNormalization(const ExprList &, const SymbolicExpr::ExprExprHashMap &index)
Undo the normalizations that were performed earlier.
size_t memoizationHits
Number of times memoization supplied a result.
Definition: SmtSolver.h:103
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:26
LinkMode linkage() const
Property: How ROSE communicates with the solver.
Definition: SmtSolver.h:414
size_t nUnknown
Number of times the solver returned "unknown".
Definition: SmtSolver.h:114
virtual std::string getErrorMessage(int exitStatus)
Error message from running a solver executable.
RAII guard for solver stack.
Definition: SmtSolver.h:132
size_t output_size
Amount of output produced by the SMT solver.
Definition: SmtSolver.h:102