ROSE  0.9.9.109
SMTSolver.h
1 #ifndef Rose_SMTSolver_H
2 #define Rose_SMTSolver_H
3 
4 #ifndef __STDC_FORMAT_MACROS
5 #define __STDC_FORMAT_MACROS
6 #endif
7 
8 #include <BinarySymbolicExpr.h>
9 #include <boost/serialization/access.hpp>
10 #include <boost/thread/mutex.hpp>
11 #include <inttypes.h>
12 
13 namespace Rose {
14 namespace BinaryAnalysis {
15 
19 class SMTSolver {
20 public:
21  struct Exception {
22  Exception(const std::string &mesg): mesg(mesg) {}
23  friend std::ostream& operator<<(std::ostream&, const SMTSolver::Exception&);
24  std::string mesg;
25  };
26 
28  enum Satisfiable { SAT_NO=0,
31  };
32 
34  struct Stats {
35  Stats(): ncalls(0), input_size(0), output_size(0) {}
36  size_t ncalls;
37  size_t input_size;
38  size_t output_size;
39  };
40 
41  typedef std::set<uint64_t> Definitions;
43 private:
44  std::string name_;
45  FILE *debug;
46  void init();
47 
48 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
49 private:
50  friend class boost::serialization::access;
51 
52  template<class S>
53  void serialize(S &s, const unsigned version) {
54  s & BOOST_SERIALIZATION_NVP(name_);
55  }
56 #endif
57 
58 public:
59  SMTSolver(): debug(NULL) { init(); }
60 
61  virtual ~SMTSolver() {}
62 
66  const std::string& name() const { return name_; }
67  void name(const std::string &s) { name_ = s; }
71  SMTSolver* instance(const std::string &name);
72 
76  virtual Satisfiable trivially_satisfiable(const std::vector<SymbolicExpr::Ptr> &exprs);
77 
81  virtual Satisfiable satisfiable(const std::vector<SymbolicExpr::Ptr>&);
82  virtual Satisfiable satisfiable(std::vector<SymbolicExpr::Ptr>, const SymbolicExpr::Ptr&);
91  virtual SymbolicExpr::Ptr evidence_for_variable(uint64_t varno) {
92  char buf[64];
93  snprintf(buf, sizeof buf, "v%" PRIu64, varno);
94  return evidence_for_name(buf);
95  }
97  SymbolicExpr::LeafPtr ln = var->isLeafNode();
98  ASSERT_require(ln && !ln->isNumber());
99  return evidence_for_variable(ln->nameId());
100  }
107  virtual SymbolicExpr::Ptr evidence_for_address(uint64_t addr);
108 
113  virtual SymbolicExpr::Ptr evidence_for_name(const std::string&) {
114  return SymbolicExpr::Ptr();
115  }
116 
119  virtual std::vector<std::string> evidence_names() {
120  return std::vector<std::string>();
121  }
122 
124  virtual void clear_evidence() {}
125 
127  void set_debug(FILE *f) { debug = f; }
128 
130  FILE *get_debug() const { return debug; }
131 
133  const Stats& get_stats() const { return stats; }
135  static Stats get_class_stats();
137  void reset_stats() { stats = Stats(); }
140  void reset_class_stats();
141 
142 protected:
146  virtual void generate_file(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs,
147  Definitions*) = 0;
148 
151  virtual std::string get_command(const std::string &config_name) = 0;
152 
155  virtual void parse_evidence() {};
156 
158  std::string output_text;
159 
160  // Statistics
161  static boost::mutex class_stats_mutex;
162  static Stats class_stats; // all access must be protected by class_stats_mutex
163  Stats stats;
164 };
165 
166 } // namespace
167 } // namespace
168 
169 #endif
virtual void parse_evidence()
Parses evidence of satisfiability.
Definition: SMTSolver.h:155
void reset_class_stats()
Resets statistics for the class.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
std::set< uint64_t > Definitions
Free variables that have been defined.
Definition: SMTSolver.h:41
virtual void clear_evidence()
Clears evidence information.
Definition: SMTSolver.h:124
FILE * get_debug() const
Obtain current debugging setting.
Definition: SMTSolver.h:130
virtual std::vector< std::string > evidence_names()
Names of items for which satisfiability evidence exists.
Definition: SMTSolver.h:119
Could not be proved satisfiable or unsatisfiable.
Definition: SMTSolver.h:30
static Stats get_class_stats()
Returns statistics for all solvers.
virtual Satisfiable satisfiable(const SymbolicExpr::Ptr &)
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
virtual SymbolicExpr::Ptr evidence_for_variable(const SymbolicExpr::Ptr &var)
Evidence of satisfiability for a bitvector variable.
Definition: SMTSolver.h:96
size_t output_size
Amount of output produced by the SMT solver.
Definition: SMTSolver.h:38
Main namespace for the ROSE library.
SMTSolver * instance(const std::string &name)
Create a solver by name.
void reset_stats()
Resets statistics for this solver.
Definition: SMTSolver.h:137
void set_debug(FILE *f)
Turns debugging on or off.
Definition: SMTSolver.h:127
const std::string & name() const
Property: Name of solver for debugging.
Definition: SMTSolver.h:66
virtual void generate_file(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *)=0
Generates an input file for for the solver.
SMT solver statistics.
Definition: SMTSolver.h:34
Provably unsatisfiable.
Definition: SMTSolver.h:28
virtual SymbolicExpr::Ptr evidence_for_name(const std::string &)
Evidence of satisfiability for a variable or memory address.
Definition: SMTSolver.h:113
virtual std::string get_command(const std::string &config_name)=0
Given the name of a configuration file, return the command that is needed to run the solver...
size_t ncalls
Number of times satisfiable() was called.
Definition: SMTSolver.h:36
Satisfiable
Satisfiability constants.
Definition: SMTSolver.h:28
Satisfiable and evidence of satisfiability may be available.
Definition: SMTSolver.h:29
virtual Satisfiable trivially_satisfiable(const std::vector< SymbolicExpr::Ptr > &exprs)
Determines if expressions are trivially satisfiable or unsatisfiable.
virtual SymbolicExpr::Ptr evidence_for_variable(uint64_t varno)
Evidence of satisfiability for a bitvector variable.
Definition: SMTSolver.h:91
const Stats & get_stats() const
Returns statistics for this solver.
Definition: SMTSolver.h:133
virtual SymbolicExpr::Ptr evidence_for_address(uint64_t addr)
Evidence of satisfiability for a memory address.
size_t input_size
Bytes of input generated for satisfiable().
Definition: SMTSolver.h:37
std::string output_text
Additional output obtained by satisfiable().
Definition: SMTSolver.h:155
void name(const std::string &s)
Property: Name of solver for debugging.
Definition: SMTSolver.h:67
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SMTSolver.h:19