ROSE  0.11.101.0
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/SymbolicExpression.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 public:
27  bool operator()(const SymbolicExpression::LeafPtr&, const SymbolicExpression::LeafPtr&) const;
28 };
29 
31 public:
32  bool operator()(const SymbolicExpression::Leaf*, const SymbolicExpression::Leaf*) const;
33 };
34 
39 class SmtSolver: private boost::noncopyable {
40 public:
42  using ExprList = std::vector<SymbolicExpression::Ptr>;
43 
45  using Ptr = SmtSolverPtr;
46 
48  using Availability = std::map<std::string, bool>;
49 
51  enum LinkMode {
52  LM_NONE = 0x0000,
53  LM_LIBRARY = 0x0001,
54  LM_EXECUTABLE = 0x0002,
55  LM_ANY = 0x0003,
56  };
57 
63  enum Type { NO_TYPE, BOOLEAN, BIT_VECTOR, MEM_STATE };
64 
66  using StringTypePair = std::pair<std::string, Type>;
68 
71 
74  Exception(const std::string &mesg): Rose::Exception(mesg) {}
75  ~Exception() throw () {}
76  };
77 
80  ParseError(const std::pair<size_t /*line*/, size_t /*col*/> &loc, const std::string &mesg)
81  : Exception("input line " + boost::lexical_cast<std::string>(loc.first+1) +
82  " column " + boost::lexical_cast<std::string>(loc.second+1) + ": " + mesg) {}
83  ~ParseError() throw () {}
84  };
85 
87  enum Satisfiable { SAT_NO=0,
90  };
91 
96  struct Stats {
97  size_t ncalls = 0;
98  size_t input_size = 0;
99  size_t output_size = 0;
100  size_t memoizationHits = 0;
101  size_t nSolversCreated = 0;
102  size_t nSolversDestroyed = 0;
103  double prepareTime = 0.0;
104  double longestPrepareTime = 0.0;
105  double solveTime = 0.0;
106  double longestSolveTime = 0.0;
107  double evidenceTime = 0.0;
108  double longestEvidenceTime = 0.0;
109  size_t nSatisfied = 0;
110  size_t nUnsatisfied = 0;
111  size_t nUnknown = 0;
112  // Remember to add all data members to SmtSolver::resetStatistics() and SmtSolver::Stats::print()
113 
114  void print(std::ostream&, const std::string &prefix = "") const;
115  };
116 
129  class Transaction {
130  SmtSolver::Ptr solver_;
131  size_t nLevels_;
132  bool committed_;
133  public:
138  : solver_(solver), committed_(false) {
139  if (solver) {
140  nLevels_ = solver->nLevels();
141  solver->push();
142  } else {
143  nLevels_ = 0;
144  }
145  }
146 
149  if (solver_ && !committed_) {
150  ASSERT_require2(solver_->nLevels() > nLevels_, "something popped this transaction already");
151  while (solver_->nLevels() > nLevels_) {
152  if (solver_->nLevels() > 1) {
153  solver_->pop();
154  } else {
155  solver_->reset();
156  }
157  }
158  }
159  }
160 
162  void commit(bool b = true) {
163  committed_ = b;
164  }
165 
167  bool isCommitted() const {
168  return committed_;
169  }
170 
173  return solver_;
174  }
175  };
176 
179 
180  using Definitions = std::set<uint64_t>;
184  public:
186  private:
187  explicit SExpr(const std::string &content): content_(content) {}
188  std::string content_;
189  std::vector<Ptr> children_;
190  public:
191  static Ptr instance(const std::string &content); // leaf node
192  static Ptr instance(size_t); // integer leaf node
193  static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());
194 
195  const std::string name() const { return content_; }
196  const std::vector<Ptr>& children() const { return children_; }
197  std::vector<Ptr>& children() { return children_; }
198  void append(const std::vector<Ptr>&);
199  void print(std::ostream&) const;
200  };
201 
202  using SExprTypePair = std::pair<SExpr::Ptr, Type>;
203 
229  public:
232 
233  /* Return value from @ref find function. */
234  struct Found {
241  explicit operator bool() const {
242  return satisfiable;
243  }
244  };
245 
246  private:
247  using ExprExpr = std::pair<SymbolicExpression::Ptr, SymbolicExpression::Ptr>;
248 
249  // The thing that is memoized
250  struct Record {
251  ExprList assertions; // "find" inputs, sorted and normalized
252  Satisfiable satisfiable; // main output of SMT solver
253  ExprExprMap evidence; // output if satisfied: sorted and normalized
254  };
255 
256  // Mapping from hash of sorted-normalized assertions to the memoization record.
257  using Map = std::multimap<SymbolicExpression::Hash, Record>;
258 
259  private:
260  mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects the following data members
261  Map map_; // memoization records indexed by hash of sorted-normalized assertions
262 
263  protected:
264  Memoizer() {}
265 
266  public:
268  static Ptr instance();
269 
271  void clear();
272 
281  Found find(const ExprList &assertions);
282 
288  ExprExprMap evidence(const Found&) const;
289 
296  void insert(const Found&, Satisfiable, const ExprExprMap &evidence);
297 
299  size_t size() const;
300 
301  public:
302  // Non-synchronized search for the sorted-normalized assertions which have the specified hash.
303  Map::iterator searchNS(SymbolicExpression::Hash, const ExprList &sortedNormalized);
304  };
305 
306 private:
307  std::string name_;
308  std::vector<ExprList> stack_;
309  bool errorIfReset_;
310 
311 protected:
312  LinkMode linkage_;
313  std::string outputText_;
314  std::vector<SExpr::Ptr> parsedOutput_; // the evidence output
315  ExprExprMap evidence_; // evidence for last check() if satisfiable
316  TermNames termNames_; // maps ROSE exprs to SMT exprs and their basic type
317  Memoizer::Ptr memoizer_; // cache of previously computed results
318  Progress::Ptr progress_; // optional progress reporting
319 
320  // Statistics
321  static boost::mutex classStatsMutex;
322  static Stats classStats; // all access must be protected by classStatsMutex
323  Stats stats;
324 
325 public:
328 
329 private:
330 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
331  friend class boost::serialization::access;
332 
333  template<class S>
334  void serialize(S &s, const unsigned /*version*/) {
335  s & BOOST_SERIALIZATION_NVP(name_);
336  s & BOOST_SERIALIZATION_NVP(stack_);
337  // linkage_ -- not serialized
338  // termNames_ -- not serialized
339  // outputText_ -- not serialized
340  // parsedOutput_ -- not serialized
341  // termNames_ -- not serialized
342  // memoizer_ -- not serialized
343  // classStatsMutex -- not serialized
344  // classStats -- not serialized
345  // stats -- not serialized
346  // mlog -- not serialized
347  }
348 #endif
349 
350 protected:
359  SmtSolver(const std::string &name, unsigned linkages)
360  : name_(name), errorIfReset_(false), linkage_(LM_NONE) {
361  init(linkages);
362  }
363 
364 public:
368  virtual Ptr create() const = 0;
369 
370  // Solvers are reference counted and should not be explicitly deleted.
371  virtual ~SmtSolver();
372 
373 
375  // Methods for creating solvers.
377 public:
378 
383  static Availability availability();
384 
391  static Ptr instance(const std::string &name);
392 
396  static Ptr bestAvailable();
397 
404  const std::string& name() const { return name_; }
405  void name(const std::string &s) { name_ = s; }
411  LinkMode linkage() const {
412  return linkage_;
413  }
414 
418  void requireLinkage(LinkMode) const;
419 
423  static LinkMode bestLinkage(unsigned linkages);
424 
432  Memoizer::Ptr memoizer() const;
433  void memoizer(const Memoizer::Ptr&);
439  virtual void timeout(boost::chrono::duration<double> seconds) = 0;
440 
441 
443  // High-level abstraction for testing satisfiability.
445 public:
446 
454  virtual Satisfiable triviallySatisfiable(const ExprList &exprs);
455 
464  virtual Satisfiable satisfiable(const ExprList&);
468  // Mid-level abstractions for testing satisfiaiblity.
471 public:
472 
477  virtual void reset();
478 
485  bool errorIfReset() const {
486  return errorIfReset_;
487  }
488  void errorIfReset(bool b) {
489  errorIfReset_ = b;
490  }
502  virtual void push();
503 
510  virtual void pop();
511 
516  virtual size_t nLevels() const { return stack_.size(); }
517 
521  virtual size_t nAssertions(size_t backtrackingLevel);
522 
524  virtual size_t nAssertions() const;
525 
531  virtual void insert(const SymbolicExpression::Ptr&);
532  virtual void insert(const ExprList&);
538  virtual ExprList assertions() const;
539 
544  virtual const ExprList& assertions(size_t level) const;
545 
550  virtual Satisfiable check();
551 
557  virtual Satisfiable checkTrivial();
558 
559 
561  // High-level abstraction for solver results.
563 public:
564 
566  using Evidence = Sawyer::Container::Map<std::string /*variable name*/, SymbolicExpression::Ptr /*value*/>;
567 
575  virtual std::vector<std::string> evidenceNames() const;
576 
582  virtual SymbolicExpression::Ptr evidenceForName(const std::string&) const;
583 
595  Evidence evidenceByName() const;
596  ExprExprMap evidence() const;
599  // Mid-level abstraction for solver results.
602 public:
603 
609  virtual void clearEvidence();
610 
617  virtual SymbolicExpression::Ptr evidenceForVariable(const SymbolicExpression::Ptr &var) {
618  SymbolicExpression::LeafPtr ln = var->isLeafNode();
619  ASSERT_require(ln && ln->isVariable2());
620  return evidenceForVariable(ln->nameId());
621  }
622  virtual SymbolicExpression::Ptr evidenceForVariable(uint64_t varno) {
623  char buf[64];
624  snprintf(buf, sizeof buf, "v%" PRIu64, varno);
625  return evidenceForName(buf);
626  }
634  virtual SymbolicExpression::Ptr evidenceForAddress(uint64_t addr);
635 
636 
638  // Statistics
640 public:
641 
645  const Stats& statistics() const { return stats; }
646 
653  static Stats classStatistics();
654 
656  void resetStatistics();
657 
662  static void resetClassStatistics();
663 
669  Progress::Ptr progress() const;
670  void progress(const Progress::Ptr &progress);
674  // Low-level API used in subclasses and sometimes for debugging
677 public:
686  virtual void generateFile(std::ostream&, const ExprList &exprs, Definitions*) = 0;
687 
688 protected:
690  virtual Satisfiable checkExe();
691 
693  virtual Satisfiable checkLib();
694 
700  virtual std::string getErrorMessage(int exitStatus);
701 
703  virtual void findVariables(const SymbolicExpression::Ptr&, VariableSet&) {}
704 
709  static void printSExpression(std::ostream&, const SExpr::Ptr&);
710 
713  virtual std::string getCommand(const std::string &config_name) = 0;
714 
716  std::vector<SExpr::Ptr> parseSExpressions(const std::string&);
717 
720  virtual void parseEvidence() {};
721 
729 
738 
739 
741  // Miscellaneous
743 public:
745  virtual void selfTest();
746 
750  static void initDiagnostics();
751 
752 private:
753  void init(unsigned linkages); // Called during construction
754 };
755 
756 std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);
757 
758 } // namespace
759 } // namespace
760 
761 #endif
762 #endif
virtual void push()
Create a backtracking point.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:45
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:167
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:235
virtual void findVariables(const SymbolicExpression::Ptr &, VariableSet &)
Return all variables that need declarations.
Definition: SmtSolver.h:703
virtual void insert(const SymbolicExpression::Ptr &)
Insert assertions.
Memoizer::Ptr memoizer() const
Property: Memoizer.
S-Expr parsed from SMT solver text output.
Definition: SmtSolver.h:183
virtual Satisfiable checkLib()
Check satisfiability using a library API.
double longestPrepareTime
Longest of times added to prepareTime.
Definition: SmtSolver.h:104
virtual void clearEvidence()
Clears evidence information.
Satisfiable and evidence of satisfiability may be available.
Definition: SmtSolver.h:88
Collection of streams.
Definition: Message.h:1606
Sawyer::SharedPointer< Memoizer > Ptr
Reference counting pointer.
Definition: SmtSolver.h:231
size_t nUnsatisfied
Number of times the solver returned "unsatisfied".
Definition: SmtSolver.h:110
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:108
size_t ncalls
Number of times satisfiable() was called.
Definition: SmtSolver.h:97
void requireLinkage(LinkMode) const
Assert required linkage.
Memoizes calls to an SMT solver.
Definition: SmtSolver.h:228
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:238
std::string outputText_
Additional output obtained by satisfiable().
Definition: SmtSolver.h:313
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:404
LinkMode
Bit flags to indicate the kind of solver interface.
Definition: SmtSolver.h:51
Main namespace for the ROSE library.
size_t nSolversCreated
Number of solvers created.
Definition: SmtSolver.h:101
static Availability availability()
Availability of all known solvers.
Satisfiable
Satisfiability constants.
Definition: SmtSolver.h:87
virtual SymbolicExpression::Ptr evidenceForName(const std::string &) const
Evidence of satisfiability for a variable or memory address.
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:109
double prepareTime
Total time in seconds spent creating assertions before solving.
Definition: SmtSolver.h:103
bool errorIfReset() const
Property: Throw an exception if the solver is reset.
Definition: SmtSolver.h:485
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:516
Exceptions for all things SMT related.
Definition: SmtSolver.h:73
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:180
Sawyer::Container::Map< SymbolicExpression::Ptr, SymbolicExpression::Ptr > ExprExprMap
Maps one symbolic expression to another.
Definition: SmtSolver.h:70
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:405
void errorIfReset(bool b)
Property: Throw an exception if the solver is reset.
Definition: SmtSolver.h:488
ExprExprMap evidence(const Found &) const
Returns evidence of satisfiability.
static void initDiagnostics()
Initialize diagnostic output facilities.
std::map< std::string, bool > Availability
Solver availability map.
Definition: SmtSolver.h:48
virtual Satisfiable checkExe()
Check satisfiability using text files and an executable.
~Transaction()
Destructor pops level unless canceled.
Definition: SmtSolver.h:148
virtual SymbolicExpression::Ptr evidenceForVariable(const SymbolicExpression::Ptr &var)
Evidence of satisfiability for a bitvector variable.
Definition: SmtSolver.h:617
double longestSolveTime
Longest of times added to the solveTime total.
Definition: SmtSolver.h:106
SMT solver statistics.
Definition: SmtSolver.h:96
Exception for parse errors when reading SMT solver output.
Definition: SmtSolver.h:79
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:359
size_t size() const
Number of call records cached.
virtual SymbolicExpression::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:162
Extends std::map with methods that return optional values.
Definition: Map.h:10
uint64_t Hash
Hash of symbolic expression.
Binary analysis.
Transaction(const SmtSolver::Ptr &solver)
Constructor pushes level if solver is non-null.
Definition: SmtSolver.h:137
virtual SymbolicExpression::Ptr evidenceForVariable(uint64_t varno)
Evidence of satisfiability for a bitvector variable.
Definition: SmtSolver.h:622
virtual void selfTest()
Unit tests.
const Stats & statistics() const
Property: Statistics for this solver.
Definition: SmtSolver.h:645
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:54
virtual ExprList assertions() const
All assertions.
Base class for reference counted objects.
Definition: SharedObject.h:64
A runtime library is available.
Definition: SmtSolver.h:53
virtual void pop()
Pop a backtracking point.
Type
Type (sort) of expression.
Definition: SmtSolver.h:63
size_t nSolversDestroyed
Number of solvers destroyed.
Definition: SmtSolver.h:102
Could not be proved satisfiable or unsatisfiable.
Definition: SmtSolver.h:89
SmtSolver::Ptr solver() const
Solver being protected.
Definition: SmtSolver.h:172
Leaf node of an expression tree for instruction semantics.
std::vector< SymbolicExpression::Ptr > ExprList
Ordered list of expressions.
Definition: SmtSolver.h:42
void insert(const Found &, Satisfiable, const ExprExprMap &evidence)
Insert a call record into the cache.
virtual Satisfiable satisfiable(const SymbolicExpression::Ptr &)
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
double evidenceTime
Total time in seconds to retrieve evidence of satisfiability.
Definition: SmtSolver.h:107
static ExprList undoNormalization(const ExprList &, const SymbolicExpression::ExprExprHashMap &index)
Undo the normalizations that were performed earlier.
double solveTime
Total time in seconds spent in solver's solve function.
Definition: SmtSolver.h:105
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:236
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SmtSolver.h:39
size_t input_size
Bytes of input generated for satisfiable().
Definition: SmtSolver.h:98
Base class for all ROSE exceptions.
Definition: Rose/Exception.h:9
static ExprList normalizeVariables(const ExprList &, SymbolicExpression::ExprExprHashMap &index)
Normalize expressions by renaming variables.
virtual void parseEvidence()
Parses evidence of satisfiability.
Definition: SmtSolver.h:720
std::vector< SExpr::Ptr > parseSExpressions(const std::string &)
Parse all SExprs from the specified string.
Provably unsatisfiable.
Definition: SmtSolver.h:87
std::pair< std::string, Type > StringTypePair
Maps expression nodes to term names.
Definition: SmtSolver.h:66
static Stats classStatistics()
Property: Statistics across all solvers.
static LinkMode bestLinkage(unsigned linkages)
Given a bit vector of linkages, return the best one.
SymbolicExpression::ExprExprHashMap rewriteMap
Mapping from provided to sortedNormalized assertions.
Definition: SmtSolver.h:237
static Sawyer::Message::Facility mlog
Diagnostic facility.
Definition: SmtSolver.h:327
virtual std::vector< std::string > evidenceNames() const
Names of items for which satisfiability evidence exists.
size_t memoizationHits
Number of times memoization supplied a result.
Definition: SmtSolver.h:100
LinkMode linkage() const
Property: How ROSE communicates with the solver.
Definition: SmtSolver.h:411
size_t nUnknown
Number of times the solver returned "unknown".
Definition: SmtSolver.h:111
virtual std::string getErrorMessage(int exitStatus)
Error message from running a solver executable.
RAII guard for solver stack.
Definition: SmtSolver.h:129
size_t output_size
Amount of output produced by the SMT solver.
Definition: SmtSolver.h:99