ROSE  0.11.50.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/SymbolicExpr.h>
11 #include <Rose/Exception.h>
12 
13 #include <boost/chrono.hpp>
14 #include <boost/lexical_cast.hpp>
15 #include <boost/noncopyable.hpp>
16 #include <boost/serialization/access.hpp>
17 #include <boost/thread/mutex.hpp>
18 #include <boost/unordered_map.hpp>
19 #include <inttypes.h>
20 
21 namespace Rose {
22 namespace BinaryAnalysis {
23 
25 using SmtSolverPtr = std::shared_ptr<class SmtSolver>;
26 
28 public:
29  bool operator()(const SymbolicExpr::LeafPtr&, const SymbolicExpr::LeafPtr&) const;
30 };
31 
36 class SmtSolver: private boost::noncopyable {
37 public:
39  using Ptr = SmtSolverPtr;
40 
42  typedef std::map<std::string, bool> Availability;
43 
45  enum LinkMode {
46  LM_NONE = 0x0000,
47  LM_LIBRARY = 0x0001,
48  LM_EXECUTABLE = 0x0002,
49  LM_ANY = 0x0003,
50  };
51 
57  enum Type { NO_TYPE, BOOLEAN, BIT_VECTOR, MEM_STATE };
58 
60  typedef std::pair<std::string, Type> StringTypePair;
62 
65 
68  Exception(const std::string &mesg): Rose::Exception(mesg) {}
69  ~Exception() throw () {}
70  };
71 
74  ParseError(const std::pair<size_t /*line*/, size_t /*col*/> &loc, const std::string &mesg)
75  : Exception("input line " + boost::lexical_cast<std::string>(loc.first+1) +
76  " column " + boost::lexical_cast<std::string>(loc.second+1) + ": " + mesg) {}
77  ~ParseError() throw () {}
78  };
79 
81  enum Satisfiable { SAT_NO=0,
84  };
85 
90  struct Stats {
91  size_t ncalls;
92  size_t input_size;
93  size_t output_size;
94  size_t memoizationHits;
95  size_t nSolversCreated;
97  double prepareTime;
98  double solveTime;
99  double evidenceTime;
100  size_t nSatisfied;
101  size_t nUnsatisfied;
102  size_t nUnknown;
103  // Remember to add all data members to resetStatistics()
104 
105  Stats()
106  : ncalls(0), input_size(0), output_size(0), memoizationHits(0), nSolversCreated(0), nSolversDestroyed(0),
107  prepareTime(0.0), solveTime(0.0), evidenceTime(0.0), nSatisfied(0), nUnsatisfied(0), nUnknown(0) {
108  }
109  };
110 
123  class Transaction {
124  SmtSolver::Ptr solver_;
125  size_t nLevels_;
126  bool committed_;
127  public:
132  : solver_(solver), committed_(false) {
133  if (solver) {
134  nLevels_ = solver->nLevels();
135  solver->push();
136  } else {
137  nLevels_ = 0;
138  }
139  }
140 
143  if (solver_ && !committed_) {
144  ASSERT_require2(solver_->nLevels() > nLevels_, "something popped this transaction already");
145  while (solver_->nLevels() > nLevels_) {
146  if (solver_->nLevels() > 1) {
147  solver_->pop();
148  } else {
149  solver_->reset();
150  }
151  }
152  }
153  }
154 
156  void commit(bool b = true) {
157  committed_ = b;
158  }
159 
161  bool isCommitted() const {
162  return committed_;
163  }
164 
167  return solver_;
168  }
169  };
170 
173 
174  typedef std::set<uint64_t> Definitions;
178  public:
180  private:
181  explicit SExpr(const std::string &content): content_(content) {}
182  std::string content_;
183  std::vector<Ptr> children_;
184  public:
185  static Ptr instance(const std::string &content); // leaf node
186  static Ptr instance(size_t); // integer leaf node
187  static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());
188 
189  const std::string name() const { return content_; }
190  const std::vector<Ptr>& children() const { return children_; }
191  std::vector<Ptr>& children() { return children_; }
192  void append(const std::vector<Ptr>&);
193  void print(std::ostream&) const;
194  };
195 
196  typedef std::pair<SExpr::Ptr, Type> SExprTypePair;
197 
198  typedef boost::unordered_map<SymbolicExpr::Hash, Satisfiable> Memoization;
199 
200 private:
201  std::string name_;
202  std::vector<std::vector<SymbolicExpr::Ptr> > stack_;
203  bool errorIfReset_;
204 
205 protected:
206  LinkMode linkage_;
207  std::string outputText_;
208  std::vector<SExpr::Ptr> parsedOutput_; // the evidence output
209  TermNames termNames_; // maps ROSE exprs to SMT exprs and their basic type
210  Memoization memoization_; // cached of previously computed results
211  bool doMemoization_; // use the memoization_ table?
212  Sawyer::Optional<SymbolicExpr::Hash> latestMemoizationId_; // key for last found or inserted memoization, or nothing
213  SymbolicExpr::ExprExprHashMap latestMemoizationRewrite_; // variables rewritten, need to be undone when parsing evidence
214 
215  // Statistics
216  static boost::mutex classStatsMutex;
217  static Stats classStats; // all access must be protected by classStatsMutex
218  Stats stats;
219 
220 public:
223 
224 private:
225 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
226  friend class boost::serialization::access;
227 
228  template<class S>
229  void serialize(S &s, const unsigned /*version*/) {
230  s & BOOST_SERIALIZATION_NVP(name_);
231  s & BOOST_SERIALIZATION_NVP(stack_);
232  // linkage_ -- not serialized
233  // termNames_ -- not serialized
234  // outputText_ -- not serialized
235  // parsedOutput_ -- not serialized
236  // termNames_ -- not serialized
237  // memoization_ -- not serialized
238  // doMemoization_ -- not serialized
239  // latestMemoizationId_ -- not serialized
240  // latestMemoizationRewrite_ -- not serialized
241  // classStatsMutex -- not serialized
242  // classStats -- not serialized
243  // stats -- not serialized
244  // mlog -- not serialized
245  }
246 #endif
247 
248 protected:
257  SmtSolver(const std::string &name, unsigned linkages)
258  : name_(name), errorIfReset_(false), linkage_(LM_NONE), doMemoization_(true) {
259  init(linkages);
260  }
261 
262 public:
264  virtual Ptr create() const = 0;
265 
266  // Solvers are reference counted and should not be explicitly deleted.
267  virtual ~SmtSolver();
268 
269 
271  // Methods for creating solvers.
273 public:
274 
279  static Availability availability();
280 
287  static Ptr instance(const std::string &name);
288 
292  static Ptr bestAvailable();
293 
300  const std::string& name() const { return name_; }
301  void name(const std::string &s) { name_ = s; }
307  LinkMode linkage() const {
308  return linkage_;
309  }
310 
314  void requireLinkage(LinkMode) const;
315 
319  static LinkMode bestLinkage(unsigned linkages);
320 
326  bool memoization() const { return doMemoization_; }
327  void memoization(bool b) {
328  doMemoization_ = b;
329  if (!b)
331  }
336  return latestMemoizationId_;
337  }
338 
340  virtual void clearMemoization() {
341  memoization_.clear();
342  }
343 
345  virtual size_t memoizationNEntries() const {
346  return memoization_.size();
347  }
348 
352  virtual void timeout(boost::chrono::duration<double> seconds) = 0;
353 
354 
356  // High-level abstraction for testing satisfiability.
358 public:
359 
367  virtual Satisfiable triviallySatisfiable(const std::vector<SymbolicExpr::Ptr> &exprs);
368 
376  virtual Satisfiable satisfiable(const SymbolicExpr::Ptr&);
377  virtual Satisfiable satisfiable(const std::vector<SymbolicExpr::Ptr>&);
381  // Mid-level abstractions for testing satisfiaiblity.
384 public:
385 
390  virtual void reset();
391 
398  bool errorIfReset() const {
399  return errorIfReset_;
400  }
401  void errorIfReset(bool b) {
402  errorIfReset_ = b;
403  }
415  virtual void push();
416 
423  virtual void pop();
424 
429  virtual size_t nLevels() const { return stack_.size(); }
430 
434  virtual size_t nAssertions(size_t backtrackingLevel);
435 
437  virtual size_t nAssertions() const;
438 
444  virtual void insert(const SymbolicExpr::Ptr&);
445  virtual void insert(const std::vector<SymbolicExpr::Ptr>&);
451  virtual std::vector<SymbolicExpr::Ptr> assertions() const;
452 
457  virtual std::vector<SymbolicExpr::Ptr> assertions(size_t level) const;
458 
463  virtual Satisfiable check();
464 
470  virtual Satisfiable checkTrivial();
471 
472 
474  // High-level abstraction for solver results.
476 public:
477 
479  using Evidence = Sawyer::Container::Map<std::string /*variable name*/, SymbolicExpr::Ptr /*value*/>;
480 
488  virtual std::vector<std::string> evidenceNames() {
489  return std::vector<std::string>();
490  }
491 
497  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) {
498  return SymbolicExpr::Ptr();
499  }
500 
504  Evidence evidence();
505 
506 
508  // Mid-level abstraction for solver results.
510 public:
511 
517  virtual void clearEvidence();
518 
525  virtual SymbolicExpr::Ptr evidenceForVariable(const SymbolicExpr::Ptr &var) {
526  SymbolicExpr::LeafPtr ln = var->isLeafNode();
527  ASSERT_require(ln && ln->isVariable2());
528  return evidenceForVariable(ln->nameId());
529  }
530  virtual SymbolicExpr::Ptr evidenceForVariable(uint64_t varno) {
531  char buf[64];
532  snprintf(buf, sizeof buf, "v%" PRIu64, varno);
533  return evidenceForName(buf);
534  }
542  virtual SymbolicExpr::Ptr evidenceForAddress(uint64_t addr);
543 
544 
546  // Statistics
548 public:
549 
553  const Stats& statistics() const { return stats; }
554 
561  static Stats classStatistics();
562 
564  void resetStatistics();
565 
570  static void resetClassStatistics();
571 
572 
574  // Low-level API used in subclasses and sometimes for debugging
576 public:
585  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) = 0;
586 
587 protected:
589  virtual Satisfiable checkExe();
590 
592  virtual Satisfiable checkLib();
593 
599  virtual std::string getErrorMessage(int exitStatus);
600 
602  virtual void findVariables(const SymbolicExpr::Ptr&, VariableSet&) {}
603 
608  static void printSExpression(std::ostream&, const SExpr::Ptr&);
609 
612  virtual std::string getCommand(const std::string &config_name) = 0;
613 
615  std::vector<SExpr::Ptr> parseSExpressions(const std::string&);
616 
619  virtual void parseEvidence() {};
620 
627  static std::vector<SymbolicExpr::Ptr> normalizeVariables(const std::vector<SymbolicExpr::Ptr>&,
628  SymbolicExpr::ExprExprHashMap &index /*out*/);
629 
637  static std::vector<SymbolicExpr::Ptr> undoNormalization(const std::vector<SymbolicExpr::Ptr>&,
638  const SymbolicExpr::ExprExprHashMap &index);
639 
640 
642  // Miscellaneous
644 public:
646  virtual void selfTest();
647 
651  static void initDiagnostics();
652 
653 private:
654  void init(unsigned linkages); // Called during construction
655 };
656 
657 std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);
658 
659 // FIXME[Robb Matzke 2017-10-17]: This typedef is deprecated. Use SmtSolver instead.
660 typedef SmtSolver SMTSolver;
661 
662 } // namespace
663 } // namespace
664 
665 #endif
666 #endif
virtual void push()
Create a backtracking point.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
bool isCommitted() const
Whether the guard is canceled.
Definition: SmtSolver.h:161
Ordered set of values.
Definition: Set.h:52
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
Definition: SymbolicExpr.h:156
S-Expr parsed from SMT solver text output.
Definition: SmtSolver.h:177
virtual Satisfiable checkLib()
Check satisfiability using a library API.
virtual void clearEvidence()
Clears evidence information.
Satisfiable and evidence of satisfiability may be available.
Definition: SmtSolver.h:82
virtual SymbolicExpr::Ptr evidenceForVariable(const SymbolicExpr::Ptr &var)
Evidence of satisfiability for a bitvector variable.
Definition: SmtSolver.h:525
virtual SymbolicExpr::Ptr evidenceForName(const std::string &)
Evidence of satisfiability for a variable or memory address.
Definition: SmtSolver.h:497
Mapping from expression to expression.
Definition: SymbolicExpr.h:905
Collection of streams.
Definition: Message.h:1606
virtual void insert(const SymbolicExpr::Ptr &)
Insert assertions.
size_t nUnsatisfied
Number of times the solver returned "unsatisfied".
Definition: SmtSolver.h:101
static void printSExpression(std::ostream &, const SExpr::Ptr &)
Print an S-Expr for debugging.
size_t ncalls
Number of times satisfiable() was called.
Definition: SmtSolver.h:91
void requireLinkage(LinkMode) const
Assert required linkage.
virtual void timeout(boost::chrono::duration< double > seconds)=0
Set the timeout for the solver.
virtual void reset()
Reset solver state.
Sawyer::Optional< SymbolicExpr::Hash > latestMemoizationId() const
Id for latest memoized result, or zero.
Definition: SmtSolver.h:335
std::string outputText_
Additional output obtained by satisfiable().
Definition: SmtSolver.h:207
Small object support.
Definition: SmallObject.h:19
const std::string & name() const
Property: Name of solver for debugging.
Definition: SmtSolver.h:300
LinkMode
Bit flags to indicate the kind of solver interface.
Definition: SmtSolver.h:45
Main namespace for the ROSE library.
size_t nSolversCreated
Number of solvers created.
Definition: SmtSolver.h:95
Sawyer::Container::Map< SymbolicExpr::Ptr, SymbolicExpr::Ptr > ExprExprMap
Maps one symbolic expression to another.
Definition: SmtSolver.h:64
static Availability availability()
Availability of all known solvers.
std::set< uint64_t > Definitions
Free variables that have been defined.
Definition: SmtSolver.h:174
Satisfiable
Satisfiability constants.
Definition: SmtSolver.h:81
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
Definition: SmtSolver.h:172
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
virtual Satisfiable check()
Check satisfiability of current stack.
void resetStatistics()
Resets statistics for this solver.
static std::vector< SymbolicExpr::Ptr > normalizeVariables(const std::vector< SymbolicExpr::Ptr > &, SymbolicExpr::ExprExprHashMap &index)
Normalize expressions by renaming variables.
size_t nSatisfied
Number of times the solver returned "satisified".
Definition: SmtSolver.h:100
double prepareTime
Time spent creating assertions before solving.
Definition: SmtSolver.h:97
bool errorIfReset() const
Property: Throw an exception if the solver is reset.
Definition: SmtSolver.h:398
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:429
Exceptions for all things SMT related.
Definition: SmtSolver.h:67
static void resetClassStatistics()
Resets statistics for the class.
std::map< std::string, bool > Availability
Solver availability map.
Definition: SmtSolver.h:42
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.
Definition: SmtSolver.h:301
virtual void findVariables(const SymbolicExpr::Ptr &, VariableSet &)
Return all variables that need declarations.
Definition: SmtSolver.h:602
void errorIfReset(bool b)
Property: Throw an exception if the solver is reset.
Definition: SmtSolver.h:401
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.
Definition: SmtSolver.h:326
virtual Satisfiable checkExe()
Check satisfiability using text files and an executable.
~Transaction()
Destructor pops level unless canceled.
Definition: SmtSolver.h:142
void memoization(bool b)
Property: Perform memoization.
Definition: SmtSolver.h:327
SMT solver statistics.
Definition: SmtSolver.h:90
Exception for parse errors when reading SMT solver output.
Definition: SmtSolver.h:73
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
Definition: SmtSolver.h:257
Sawyer::Container::Map< std::string, SymbolicExpr::Ptr > Evidence
Evidence of satisfiability.
Definition: SmtSolver.h:479
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:156
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.
Definition: SmtSolver.h:131
virtual void selfTest()
Unit tests.
const Stats & statistics() const
Property: Statistics for this solver.
Definition: SmtSolver.h:553
virtual Satisfiable checkTrivial()
Check whether the stack of assertions is trivially satisfiable.
virtual void clearMemoization()
Clear memoization table.
Definition: SmtSolver.h:340
An executable is available.
Definition: SmtSolver.h:48
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.
Definition: SmtSolver.h:47
virtual void pop()
Pop a backtracking point.
Type
Type (sort) of expression.
Definition: SmtSolver.h:57
size_t nSolversDestroyed
Number of solvers destroyed.
Definition: SmtSolver.h:96
Could not be proved satisfiable or unsatisfiable.
Definition: SmtSolver.h:83
SmtSolver::Ptr solver() const
Solver being protected.
Definition: SmtSolver.h:166
virtual std::vector< SymbolicExpr::Ptr > assertions() const
All assertions.
double evidenceTime
Seconds to retrieve evidence of satisfiability.
Definition: SmtSolver.h:99
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.
Definition: SmtSolver.h:98
virtual std::vector< std::string > evidenceNames()
Names of items for which satisfiability evidence exists.
Definition: SmtSolver.h:488
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.
Definition: SmtSolver.h:60
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SmtSolver.h:36
size_t input_size
Bytes of input generated for satisfiable().
Definition: SmtSolver.h:92
Base class for all ROSE exceptions.
Definition: Rose/Exception.h:9
virtual size_t memoizationNEntries() const
Size of memoization table.
Definition: SmtSolver.h:345
virtual void parseEvidence()
Parses evidence of satisfiability.
Definition: SmtSolver.h:619
std::vector< SExpr::Ptr > parseSExpressions(const std::string &)
Parse all SExprs from the specified string.
Provably unsatisfiable.
Definition: SmtSolver.h:81
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:530
static Sawyer::Message::Facility mlog
Diagnostic facility.
Definition: SmtSolver.h:222
size_t memoizationHits
Number of times memoization supplied a result.
Definition: SmtSolver.h:94
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:25
LinkMode linkage() const
Property: How ROSE communicates with the solver.
Definition: SmtSolver.h:307
size_t nUnknown
Number of times the solver returned "unknown".
Definition: SmtSolver.h:102
virtual std::string getErrorMessage(int exitStatus)
Error message from running a solver executable.
RAII guard for solver stack.
Definition: SmtSolver.h:123
size_t output_size
Amount of output produced by the SMT solver.
Definition: SmtSolver.h:93
Evidence evidence()
All evidence of satisfiability.