ROSE 0.11.145.250
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/thread/mutex.hpp>
18
19#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
20#include <boost/serialization/access.hpp>
21#endif
22
23#include <inttypes.h>
24#include <unordered_map>
25
26namespace Rose {
27namespace BinaryAnalysis {
28
30public:
31 bool operator()(const SymbolicExpression::LeafPtr&, const SymbolicExpression::LeafPtr&) const;
32};
33
35public:
36 bool operator()(const SymbolicExpression::Leaf*, const SymbolicExpression::Leaf*) const;
37};
38
43class SmtSolver: private boost::noncopyable {
44public:
46 using ExprList = std::vector<SymbolicExpression::Ptr>;
47
50
52 using Availability = std::map<std::string, bool>;
53
55 enum LinkMode {
56 LM_NONE = 0x0000,
57 LM_LIBRARY = 0x0001,
58 LM_EXECUTABLE = 0x0002,
59 LM_ANY = 0x0003,
60 };
61
67 enum Type { NO_TYPE, BOOLEAN, BIT_VECTOR, MEM_STATE };
68
70 using StringTypePair = std::pair<std::string, Type>;
72
75
78 Exception(const std::string &mesg): Rose::Exception(mesg) {}
79 ~Exception() throw () {}
80 };
81
84 ParseError(const std::pair<size_t /*line*/, size_t /*col*/> &loc, const std::string &mesg)
85 : Exception("input line " + boost::lexical_cast<std::string>(loc.first+1) +
86 " column " + boost::lexical_cast<std::string>(loc.second+1) + ": " + mesg) {}
87 ~ParseError() throw () {}
88 };
89
94 };
95
100 struct Stats {
101 size_t ncalls = 0;
102 size_t input_size = 0;
103 size_t output_size = 0;
104 size_t memoizationHits = 0;
105 size_t nSolversCreated = 0;
106 size_t nSolversDestroyed = 0;
107 double prepareTime = 0.0;
108 double longestPrepareTime = 0.0;
109 double solveTime = 0.0;
110 double longestSolveTime = 0.0;
111 double evidenceTime = 0.0;
112 double longestEvidenceTime = 0.0;
113 size_t nSatisfied = 0;
114 size_t nUnsatisfied = 0;
115 size_t nUnknown = 0;
116 // Remember to add all data members to SmtSolver::resetStatistics() and SmtSolver::Stats::print()
117
118 void print(std::ostream&, const std::string &prefix = "") const;
119 };
120
134 SmtSolver::Ptr solver_;
135 size_t nLevels_;
136 bool committed_;
137 public:
142 : solver_(solver), committed_(false) {
143 if (solver) {
144 nLevels_ = solver->nLevels();
145 solver->push();
146 } else {
147 nLevels_ = 0;
148 }
149 }
150
153 if (solver_ && !committed_) {
154 ASSERT_require2(solver_->nLevels() > nLevels_, "something popped this transaction already");
155 while (solver_->nLevels() > nLevels_) {
156 if (solver_->nLevels() > 1) {
157 solver_->pop();
158 } else {
159 solver_->reset();
160 }
161 }
162 }
163 }
164
166 void commit(bool b = true) {
167 committed_ = b;
168 }
169
171 bool isCommitted() const {
172 return committed_;
173 }
174
177 return solver_;
178 }
179 };
180
183
184 using Definitions = std::set<uint64_t>;
188 public:
190 private:
191 explicit SExpr(const std::string &content): content_(content) {}
192 std::string content_;
193 std::vector<Ptr> children_;
194 public:
195 static Ptr instance(const std::string &content); // leaf node
196 static Ptr instance(size_t); // integer leaf node
197 static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());
198
199 const std::string name() const { return content_; }
200 const std::vector<Ptr>& children() const { return children_; }
201 std::vector<Ptr>& children() { return children_; }
202 void append(const std::vector<Ptr>&);
203 void print(std::ostream&) const;
204 };
205
206 using SExprTypePair = std::pair<SExpr::Ptr, Type>;
207
233 public:
236
237 /* Return value from @ref find function. */
249
250 private:
251 using ExprExpr = std::pair<SymbolicExpression::Ptr, SymbolicExpression::Ptr>;
252
253 // The thing that is memoized
254 struct Record {
255 ExprList assertions; // "find" inputs, sorted and normalized
256 Satisfiable satisfiable; // main output of SMT solver
257 ExprExprMap evidence; // output if satisfied: sorted and normalized
258 };
259
260 // Mapping from hash of sorted-normalized assertions to the memoization record.
261 using Map = std::multimap<SymbolicExpression::Hash, Record>;
262
263 private:
264 mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects the following data members
265 Map map_; // memoization records indexed by hash of sorted-normalized assertions
266
267 protected:
268 Memoizer() {}
269
270 public:
272 static Ptr instance();
273
275 void clear();
276
286
293
301
303 size_t size() const;
304
305 public:
306 // Non-synchronized search for the sorted-normalized assertions which have the specified hash.
307 Map::iterator searchNS(SymbolicExpression::Hash, const ExprList &sortedNormalized);
308 };
309
310private:
311 std::string name_;
312 std::vector<ExprList> stack_;
313 bool errorIfReset_;
314
315protected:
316 LinkMode linkage_;
317 std::string outputText_;
318 std::vector<SExpr::Ptr> parsedOutput_; // the evidence output
319 ExprExprMap evidence_; // evidence for last check() if satisfiable
320 TermNames termNames_; // maps ROSE exprs to SMT exprs and their basic type
321 Memoizer::Ptr memoizer_; // cache of previously computed results
322 Progress::Ptr progress_; // optional progress reporting
323
324 // Statistics
325 static boost::mutex classStatsMutex;
326 static Stats classStats; // all access must be protected by classStatsMutex
327 Stats stats;
328
329public:
332
333private:
334#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
335 friend class boost::serialization::access;
336
337 template<class S>
338 void serialize(S &s, const unsigned /*version*/) {
339 s & BOOST_SERIALIZATION_NVP(name_);
340 s & BOOST_SERIALIZATION_NVP(stack_);
341 // linkage_ -- not serialized
342 // termNames_ -- not serialized
343 // outputText_ -- not serialized
344 // parsedOutput_ -- not serialized
345 // termNames_ -- not serialized
346 // memoizer_ -- not serialized
347 // classStatsMutex -- not serialized
348 // classStats -- not serialized
349 // stats -- not serialized
350 // mlog -- not serialized
351 }
352#endif
353
354protected:
363 SmtSolver(const std::string &name, unsigned linkages)
364 : name_(name), errorIfReset_(false), linkage_(LM_NONE) {
365 init(linkages);
366 }
367
368public:
372 virtual Ptr create() const = 0;
373
374 // Solvers are reference counted and should not be explicitly deleted.
375 virtual ~SmtSolver();
376
377
379 // Methods for creating solvers.
381public:
382
388
395 static Ptr instance(const std::string &name);
396
401
408 const std::string& name() const { return name_; }
409 void name(const std::string &s) { name_ = s; }
416 return linkage_;
417 }
418
423
427 static LinkMode bestLinkage(unsigned linkages);
428
443 virtual void timeout(boost::chrono::duration<double> seconds) = 0;
444
445
447 // High-level abstraction for testing satisfiability.
449public:
450
459
473 // Mid-level abstractions for testing satisfiaiblity.
475public:
476
481 virtual void reset();
482
489 bool errorIfReset() const {
490 return errorIfReset_;
491 }
492 void errorIfReset(bool b) {
493 errorIfReset_ = b;
494 }
506 virtual void push();
507
514 virtual void pop();
515
520 virtual size_t nLevels() const { return stack_.size(); }
521
525 virtual size_t nAssertions(size_t backtrackingLevel);
526
528 virtual size_t nAssertions() const;
529
535 virtual void insert(const SymbolicExpression::Ptr&);
536 virtual void insert(const ExprList&);
542 virtual ExprList assertions() const;
543
548 virtual const ExprList& assertions(size_t level) const;
549
555
562
563
565 // High-level abstraction for solver results.
567public:
568
570 using Evidence = Sawyer::Container::Map<std::string /*variable name*/, SymbolicExpression::Ptr /*value*/>;
571
579 virtual std::vector<std::string> evidenceNames() const;
580
586 virtual SymbolicExpression::Ptr evidenceForName(const std::string&) const;
587
604 // Mid-level abstraction for solver results.
606public:
607
613 virtual void clearEvidence();
614
622 SymbolicExpression::LeafPtr ln = var->isLeafNode();
623 ASSERT_require(ln && ln->isVariable2());
624 return evidenceForVariable(ln->nameId());
625 }
627 char buf[64];
628 snprintf(buf, sizeof buf, "v%" PRIu64, varno);
629 return evidenceForName(buf);
630 }
639
640
642 // Statistics
644public:
645
649 const Stats& statistics() const { return stats; }
650
658
661
666 static void resetClassStatistics();
667
679 // Low-level API used in subclasses and sometimes for debugging
681public:
690 virtual void generateFile(std::ostream&, const ExprList &exprs, Definitions*) = 0;
691
692protected:
695
698
704 virtual std::string getErrorMessage(int exitStatus);
705
708
713 static void printSExpression(std::ostream&, const SExpr::Ptr&);
714
717 virtual std::string getCommand(const std::string &config_name) = 0;
718
720 std::vector<SExpr::Ptr> parseSExpressions(const std::string&);
721
724 virtual void parseEvidence() {};
725
733
742
743
745 // Miscellaneous
747public:
749 virtual void selfTest();
750
754 static void initDiagnostics();
755
756private:
757 void init(unsigned linkages); // Called during construction
758};
759
760std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);
761
762} // namespace
763} // namespace
764
765#endif
766#endif
Extends std::map with methods that return optional values.
Definition util/Map.h:16
Memoizes calls to an SMT solver.
Definition SmtSolver.h:232
Found find(const ExprList &assertions)
Search for the specified assertions in the cache.
size_t size() const
Number of call records cached.
void insert(const Found &, Satisfiable, const ExprExprMap &evidence)
Insert a call record into the cache.
static Ptr instance()
Allocating constructor.
void clear()
Clear the entire cache as if it was just constructed.
ExprExprMap evidence(const Found &) const
Returns evidence of satisfiability.
S-Expr parsed from SMT solver text output.
Definition SmtSolver.h:187
bool isCommitted() const
Whether the guard is canceled.
Definition SmtSolver.h:171
~Transaction()
Destructor pops level unless canceled.
Definition SmtSolver.h:152
SmtSolver::Ptr solver() const
Solver being protected.
Definition SmtSolver.h:176
Transaction(const SmtSolver::Ptr &solver)
Constructor pushes level if solver is non-null.
Definition SmtSolver.h:141
void commit(bool b=true)
Cancel the popping during the destructor.
Definition SmtSolver.h:166
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition SmtSolver.h:43
const Stats & statistics() const
Property: Statistics for this solver.
Definition SmtSolver.h:649
std::map< std::string, bool > Availability
Solver availability map.
Definition SmtSolver.h:52
std::vector< SymbolicExpression::Ptr > ExprList
Ordered list of expressions.
Definition SmtSolver.h:46
const std::string & name() const
Property: Name of solver for debugging.
Definition SmtSolver.h:408
static void resetClassStatistics()
Resets statistics for the class.
virtual size_t nAssertions() const
Total number of assertions across all backtracking levels.
void requireLinkage(LinkMode) const
Assert required linkage.
void memoizer(const Memoizer::Ptr &)
Property: Memoizer.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition SmtSolver.h:49
Memoizer::Ptr memoizer() const
Property: Memoizer.
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.
virtual void generateFile(std::ostream &, const ExprList &exprs, Definitions *)=0
Generates an input file for for the solver.
virtual ExprList assertions() const
All assertions.
virtual Satisfiable check()
Check satisfiability of current stack.
virtual size_t nAssertions(size_t backtrackingLevel)
Number of assertions at a specific backtracking level.
void resetStatistics()
Resets statistics for this solver.
virtual Ptr create() const =0
Virtual constructor.
Type
Type (sort) of expression.
Definition SmtSolver.h:67
virtual SymbolicExpression::Ptr evidenceForVariable(uint64_t varno)
Evidence of satisfiability for a bitvector variable.
Definition SmtSolver.h:626
Evidence evidenceByName() const
All evidence of satisfiability.
virtual size_t nLevels() const
Number of backtracking levels.
Definition SmtSolver.h:520
static void printSExpression(std::ostream &, const SExpr::Ptr &)
Print an S-Expr for debugging.
virtual void pop()
Pop a backtracking point.
static Stats classStatistics()
Property: Statistics across all solvers.
virtual std::vector< std::string > evidenceNames() const
Names of items for which satisfiability evidence exists.
static ExprList undoNormalization(const ExprList &, const SymbolicExpression::ExprExprHashMap &index)
Undo the normalizations that were performed earlier.
virtual Satisfiable satisfiable(const SymbolicExpression::Ptr &)
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
virtual SymbolicExpression::Ptr evidenceForAddress(uint64_t addr)
Evidence of satisfiability for a memory address.
static Ptr instance(const std::string &name)
Allocate a new solver by name.
static ExprList normalizeVariables(const ExprList &, SymbolicExpression::ExprExprHashMap &index)
Normalize expressions by renaming variables.
virtual void parseEvidence()
Parses evidence of satisfiability.
Definition SmtSolver.h:724
LinkMode
Bit flags to indicate the kind of solver interface.
Definition SmtSolver.h:55
@ LM_ANY
Any available mode.
Definition SmtSolver.h:59
@ LM_EXECUTABLE
An executable is available.
Definition SmtSolver.h:58
@ LM_LIBRARY
A runtime library is available.
Definition SmtSolver.h:57
@ LM_NONE
No available linkage.
Definition SmtSolver.h:56
static LinkMode bestLinkage(unsigned linkages)
Given a bit vector of linkages, return the best one.
Satisfiable
Satisfiability constants.
Definition SmtSolver.h:91
@ SAT_UNKNOWN
Could not be proved satisfiable or unsatisfiable.
Definition SmtSolver.h:93
@ SAT_YES
Satisfiable and evidence of satisfiability may be available.
Definition SmtSolver.h:92
@ SAT_NO
Provably unsatisfiable.
Definition SmtSolver.h:91
virtual Satisfiable checkLib()
Check satisfiability using a library API.
virtual void timeout(boost::chrono::duration< double > seconds)=0
Set the timeout for the solver.
void errorIfReset(bool b)
Property: Throw an exception if the solver is reset.
Definition SmtSolver.h:492
virtual Satisfiable checkTrivial()
Check whether the stack of assertions is trivially satisfiable.
LinkMode linkage() const
Property: How ROSE communicates with the solver.
Definition SmtSolver.h:415
virtual void insert(const ExprList &)
Insert assertions.
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
Definition SmtSolver.h:363
virtual void push()
Create a backtracking point.
virtual Satisfiable satisfiable(const ExprList &)
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
virtual void clearEvidence()
Clears evidence information.
virtual void findVariables(const SymbolicExpression::Ptr &, VariableSet &)
Return all variables that need declarations.
Definition SmtSolver.h:707
static void initDiagnostics()
Initialize diagnostic output facilities.
virtual Satisfiable triviallySatisfiable(const ExprList &exprs)
Determines if expressions are trivially satisfiable or unsatisfiable.
static Ptr bestAvailable()
Best available solver.
static Availability availability()
Availability of all known solvers.
virtual SymbolicExpression::Ptr evidenceForName(const std::string &) const
Evidence of satisfiability for a variable or memory address.
bool errorIfReset() const
Property: Throw an exception if the solver is reset.
Definition SmtSolver.h:489
ExprExprMap evidence() const
All evidence of satisfiability.
std::string outputText_
Additional output obtained by satisfiable().
Definition SmtSolver.h:317
virtual void insert(const SymbolicExpression::Ptr &)
Insert assertions.
Progress::Ptr progress() const
Progress reporting object.
virtual SymbolicExpression::Ptr evidenceForVariable(const SymbolicExpression::Ptr &var)
Evidence of satisfiability for a bitvector variable.
Definition SmtSolver.h:621
virtual const ExprList & assertions(size_t level) const
Assertions for a particular level.
virtual void selfTest()
Unit tests.
void name(const std::string &s)
Property: Name of solver for debugging.
Definition SmtSolver.h:409
std::set< uint64_t > Definitions
Free variables that have been defined.
Definition SmtSolver.h:184
virtual std::string getErrorMessage(int exitStatus)
Error message from running a solver executable.
std::pair< std::string, Type > StringTypePair
Maps expression nodes to term names.
Definition SmtSolver.h:70
std::vector< SExpr::Ptr > parseSExpressions(const std::string &)
Parse all SExprs from the specified string.
virtual void reset()
Reset solver state.
static Sawyer::Message::Facility mlog
Diagnostic facility.
Definition SmtSolver.h:331
void progress(const Progress::Ptr &progress)
Progress reporting object.
virtual Satisfiable checkExe()
Check satisfiability using text files and an executable.
Leaf node of an expression tree for instruction semantics.
Base class for all ROSE exceptions.
Ordered set of values.
Definition Set.h:56
Collection of streams.
Definition Message.h:1606
Holds a value or nothing.
Definition Optional.h:56
Base class for reference counted objects.
Reference-counting intrusive smart pointer.
Small object support.
Definition SmallObject.h:19
uint64_t Hash
Hash of symbolic expression.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.
Exceptions for all things SMT related.
Definition SmtSolver.h:77
ExprList sortedNormalized
Sorted and normalized assertions, regardless if found.
Definition SmtSolver.h:240
SymbolicExpression::ExprExprHashMap rewriteMap
Mapping from provided to sortedNormalized assertions.
Definition SmtSolver.h:241
ExprExprMap evidence
Normalized evidence if found and satisfiable.
Definition SmtSolver.h:242
Sawyer::Optional< Satisfiable > satisfiable
If found, whether satisfiable.
Definition SmtSolver.h:239
Exception for parse errors when reading SMT solver output.
Definition SmtSolver.h:83
double longestPrepareTime
Longest of times added to prepareTime.
Definition SmtSolver.h:108
size_t output_size
Amount of output produced by the SMT solver.
Definition SmtSolver.h:103
double evidenceTime
Total time in seconds to retrieve evidence of satisfiability.
Definition SmtSolver.h:111
double longestSolveTime
Longest of times added to the solveTime total.
Definition SmtSolver.h:110
size_t ncalls
Number of times satisfiable() was called.
Definition SmtSolver.h:101
size_t nSatisfied
Number of times the solver returned "satisified".
Definition SmtSolver.h:113
size_t nSolversDestroyed
Number of solvers destroyed.
Definition SmtSolver.h:106
size_t memoizationHits
Number of times memoization supplied a result.
Definition SmtSolver.h:104
double longestEvidenceTime
Longest of times added to evidenceTime.
Definition SmtSolver.h:112
double prepareTime
Total time in seconds spent creating assertions before solving.
Definition SmtSolver.h:107
size_t input_size
Bytes of input generated for satisfiable().
Definition SmtSolver.h:102
double solveTime
Total time in seconds spent in solver's solve function.
Definition SmtSolver.h:109
size_t nSolversCreated
Number of solvers created.
Definition SmtSolver.h:105
size_t nUnsatisfied
Number of times the solver returned "unsatisfied".
Definition SmtSolver.h:114
size_t nUnknown
Number of times the solver returned "unknown".
Definition SmtSolver.h:115