ROSE  0.9.10.103
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 
111  class Transaction {
112  SmtSolver::Ptr solver_;
113  bool committed_;
114  public:
119  : solver_(solver), committed_(false) {
120  if (solver)
121  solver->push();
122  }
123 
126  if (solver_ && !committed_) {
127  if (solver_->nLevels() > 1) {
128  solver_->pop();
129  } else {
130  solver_->reset();
131  }
132  }
133  }
134 
136  void commit(bool b = true) {
137  committed_ = b;
138  }
139 
141  bool isCommitted() const {
142  return committed_;
143  }
144 
147  return solver_;
148  }
149  };
150 
153 
154  typedef std::set<uint64_t> Definitions;
158  public:
159  typedef Sawyer::SharedPointer<SExpr> Ptr;
160  private:
161  explicit SExpr(const std::string &content): content_(content) {}
162  std::string content_;
163  std::vector<Ptr> children_;
164  public:
165  static Ptr instance(const std::string &content); // leaf node
166  static Ptr instance(size_t); // integer leaf node
167  static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());
168 
169  const std::string name() const { return content_; }
170  const std::vector<Ptr>& children() const { return children_; }
171  std::vector<Ptr>& children() { return children_; }
172  void append(const std::vector<Ptr>&);
173  void print(std::ostream&) const;
174  };
175 
176  typedef std::pair<SExpr::Ptr, Type> SExprTypePair;
177 
178  typedef boost::unordered_map<SymbolicExpr::Hash, Satisfiable> Memoization;
179 
180 private:
181  std::string name_;
182  std::vector<std::vector<SymbolicExpr::Ptr> > stack_;
183  bool errorIfReset_;
184 
185 protected:
186  LinkMode linkage_;
187  std::string outputText_;
188  std::vector<SExpr::Ptr> parsedOutput_; // the evidence output
189  TermNames termNames_; // maps ROSE exprs to SMT exprs and their basic type
190  Memoization memoization_; // cached of previously computed results
191  bool doMemoization_; // use the memoization_ table?
192  SymbolicExpr::Hash latestMemoizationId_; // key for last found or inserted memoization, or zero
193  SymbolicExpr::ExprExprHashMap latestMemoizationRewrite_; // variables rewritten, need to be undone when parsing evidence
194 
195  // Statistics
196  static boost::mutex classStatsMutex;
197  static Stats classStats; // all access must be protected by classStatsMutex
198  Stats stats;
199 
200 public:
203 
204 private:
205 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
206  friend class boost::serialization::access;
207 
208  template<class S>
209  void serialize(S &s, const unsigned /*version*/) {
210  s & BOOST_SERIALIZATION_NVP(name_);
211  s & BOOST_SERIALIZATION_NVP(stack_);
212  // linkage_ -- not serialized
213  // termNames_ -- not serialized
214  // outputText_ -- not serialized
215  // parsedOutput_ -- not serialized
216  // termNames_ -- not serialized
217  // memoization_ -- not serialized
218  // doMemoization_ -- not serialized
219  // latestMemoizationId_ -- not serialized
220  // latestMemoizationRewrite_ -- not serialized
221  // classStatsMutex -- not serialized
222  // classStats -- not serialized
223  // stats -- not serialized
224  // mlog -- not serialized
225  }
226 #endif
227 
228 protected:
237  SmtSolver(const std::string &name, unsigned linkages)
238  : name_(name), errorIfReset_(false), linkage_(LM_NONE), doMemoization_(true), latestMemoizationId_(0) {
239  init(linkages);
240  }
241 
242 public:
244  virtual Ptr create() const = 0;
245 
246  // Solvers are reference counted and should not be explicitly deleted.
247  virtual ~SmtSolver();
248 
249 
251  // Methods for creating solvers.
253 public:
254 
259  static Availability availability();
260 
267  static Ptr instance(const std::string &name);
268 
272  static Ptr bestAvailable();
273 
280  const std::string& name() const { return name_; }
281  void name(const std::string &s) { name_ = s; }
287  LinkMode linkage() const {
288  return linkage_;
289  }
290 
294  void requireLinkage(LinkMode) const;
295 
299  static LinkMode bestLinkage(unsigned linkages);
300 
306  bool memoization() const { return doMemoization_; }
307  void memoization(bool b) {
308  doMemoization_ = b;
309  if (!b)
311  }
316  return latestMemoizationId_;
317  }
318 
320  virtual void clearMemoization() {
321  memoization_.clear();
322  }
323 
325  virtual size_t memoizationNEntries() const {
326  return memoization_.size();
327  }
328 
329 
331  // High-level abstraction for testing satisfiability.
333 public:
334 
342  virtual Satisfiable triviallySatisfiable(const std::vector<SymbolicExpr::Ptr> &exprs);
343 
351  virtual Satisfiable satisfiable(const SymbolicExpr::Ptr&);
352  virtual Satisfiable satisfiable(const std::vector<SymbolicExpr::Ptr>&);
356  // Mid-level abstractions for testing satisfiaiblity.
359 public:
360 
365  virtual void reset();
366 
373  bool errorIfReset() const {
374  return errorIfReset_;
375  }
376  void errorIfReset(bool b) {
377  errorIfReset_ = b;
378  }
390  virtual void push();
391 
398  virtual void pop();
399 
404  virtual size_t nLevels() const { return stack_.size(); }
405 
409  virtual size_t nAssertions(size_t backtrackingLevel);
410 
412  virtual size_t nAssertions() const;
413 
419  virtual void insert(const SymbolicExpr::Ptr&);
420  virtual void insert(const std::vector<SymbolicExpr::Ptr>&);
426  virtual std::vector<SymbolicExpr::Ptr> assertions() const;
427 
432  virtual std::vector<SymbolicExpr::Ptr> assertions(size_t level) const;
433 
438  virtual Satisfiable check();
439 
445  virtual Satisfiable checkTrivial();
446 
447 
449  // High-level abstraction for solver results.
451 public:
452 
460  virtual std::vector<std::string> evidenceNames() {
461  return std::vector<std::string>();
462  }
463 
469  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) {
470  return SymbolicExpr::Ptr();
471  }
472 
473 
475  // Mid-level abstraction for solver results.
477 public:
478 
484  virtual void clearEvidence();
485 
493  SymbolicExpr::LeafPtr ln = var->isLeafNode();
494  ASSERT_require(ln && !ln->isNumber());
495  return evidenceForVariable(ln->nameId());
496  }
497  virtual SymbolicExpr::Ptr evidenceForVariable(uint64_t varno) {
498  char buf[64];
499  snprintf(buf, sizeof buf, "v%" PRIu64, varno);
500  return evidenceForName(buf);
501  }
509  virtual SymbolicExpr::Ptr evidenceForAddress(uint64_t addr);
510 
511 
513  // Statistics
515 public:
516 
520  const Stats& statistics() const { return stats; }
521 
528  static Stats classStatistics();
529 
531  void resetStatistics();
532 
537  static void resetClassStatistics();
538 
539 
541  // Low-level API used in subclasses.
543 protected:
545  virtual Satisfiable checkExe();
546 
548  virtual Satisfiable checkLib();
549 
555  virtual std::string getErrorMessage(int exitStatus);
556 
558  virtual VariableSet findVariables(const SymbolicExpr::Ptr&) { return VariableSet(); }
559 
564  static void printSExpression(std::ostream&, const SExpr::Ptr&);
565 
569  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) = 0;
570 
573  virtual std::string getCommand(const std::string &config_name) = 0;
574 
576  std::vector<SExpr::Ptr> parseSExpressions(const std::string&);
577 
580  virtual void parseEvidence() {};
581 
588  static std::vector<SymbolicExpr::Ptr> normalizeVariables(const std::vector<SymbolicExpr::Ptr>&,
589  SymbolicExpr::ExprExprHashMap &index /*out*/);
590 
598  static std::vector<SymbolicExpr::Ptr> undoNormalization(const std::vector<SymbolicExpr::Ptr>&,
599  const SymbolicExpr::ExprExprHashMap &index);
600 
601 
603  // Miscellaneous
605 public:
607  virtual void selfTest();
608 
612  static void initDiagnostics();
613 
614 private:
615  void init(unsigned linkages); // Called during construction
616 
617 
618 
620  // Deprecated junk
622 
623  // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
624 public:
625  virtual Satisfiable trivially_satisfiable(const std::vector<SymbolicExpr::Ptr> &exprs)
626  ROSE_DEPRECATED("use triviallySatisfiable");
627  virtual SymbolicExpr::Ptr evidence_for_variable(uint64_t varno) ROSE_DEPRECATED("use evidenceForVariable");
628  virtual SymbolicExpr::Ptr evidence_for_variable(const SymbolicExpr::Ptr &var) ROSE_DEPRECATED("use evidenceForVariable");
629  virtual SymbolicExpr::Ptr evidence_for_name(const std::string&) ROSE_DEPRECATED("use evidenceForName");
630  virtual SymbolicExpr::Ptr evidence_for_address(uint64_t addr) ROSE_DEPRECATED("use evidenceForAddress");
631  virtual std::vector<std::string> evidence_names() ROSE_DEPRECATED("use evidenceNames");
632  virtual void clear_evidence() ROSE_DEPRECATED("use clearEvidence");
633  const Stats& get_stats() const ROSE_DEPRECATED("use statistics");
634  static Stats get_class_stats() ROSE_DEPRECATED("use classStatistics");
635  void reset_stats() ROSE_DEPRECATED("use resetStatistics");
636  void reset_class_stats() ROSE_DEPRECATED("use resetClassStatistics");
637 protected:
638  virtual void generate_file(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*)
639  ROSE_DEPRECATED("use generateFile");
640  virtual std::string get_command(const std::string &config_name) ROSE_DEPRECATED("use getCommand");
641  virtual void parse_evidence() ROSE_DEPRECATED("use parseEvidence");
642 };
643 
644 std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);
645 
646 // FIXME[Robb Matzke 2017-10-17]: This typedef is deprecated. Use SmtSolver instead.
647 typedef SmtSolver SMTSolver;
648 
649 } // namespace
650 } // namespace
651 
652 #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.
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.
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 VariableSet findVariables(const SymbolicExpr::Ptr &)
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: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.
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.