diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2009-07-15 03:05:06 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2009-07-15 03:05:06 +0000 |
commit | 751901a5bb099ed37ce571001b4cad005be80f3d (patch) | |
tree | 9174b5b11cf72265c0994add96922910ddef0482 | |
parent | 0661cf4e1f8f4dabd900d5672b9f6c16f000a9d0 (diff) | |
download | klee-751901a5bb099ed37ce571001b4cad005be80f3d.tar.gz |
Code to answer satisfiability queries.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75735 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r-- | lib/SMT/SMTParser.cpp | 43 | ||||
-rw-r--r-- | lib/SMT/SMTParser.h | 13 | ||||
-rw-r--r-- | lib/SMT/main.cpp | 6 | ||||
-rw-r--r-- | lib/SMT/smtlib.y | 3 |
4 files changed, 50 insertions, 15 deletions
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index b6ac5480..22578f46 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -10,6 +10,8 @@ #include "SMTParser.h" #include "klee/ExprBuilder.h" +#include "klee/Solver.h" +#include "klee/Constraints.h" #include "expr/Parser.h" #include <iostream> @@ -38,7 +40,7 @@ SMTParser::SMTParser(const std::string _filename, ExprBuilder* _builder) : fileName(_filename), lineNum(1), done(false), - query(NULL), + satQuery(NULL), bvSize(0), queryParsed(false), builder(_builder) { @@ -49,7 +51,7 @@ SMTParser::SMTParser(const std::string _filename, fvarEnvs.push(FVarEnv()); } -void SMTParser::Init() { +void SMTParser::Parse() { SMTParser::parserTemp = this; void *buf = smtlib_createBuffer(smtlib_bufSize()); @@ -60,12 +62,45 @@ void SMTParser::Init() { } Decl* SMTParser::ParseTopLevelDecl() { - assert(done); - return new QueryCommand(assumptions, query, + return new QueryCommand(assumptions, builder->Not(satQuery), std::vector<ExprHandle>(), std::vector<const Array*>()); } +bool SMTParser::Solve() { + // FIXME: Support choice of solver. + bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryPCLog = true; + Solver *S, *STP = S = + UseDummySolver ? createDummySolver() : new STPSolver(true); + if (UseSTPQueryPCLog) + S = createPCLoggingSolver(S, "stp-queries.pc"); + if (UseFastCexSolver) + S = createFastCexSolver(S); + S = createCexCachingSolver(S); + S = createCachingSolver(S); + S = createIndependentSolver(S); + if (0) + S = createValidatingSolver(S, STP); + + Decl *D = this->ParseTopLevelDecl(); + if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) { + //llvm::cout << "Query " << ":\t"; + + assert("FIXME: Support counterexample query commands!"); + if (QC->Values.empty() && QC->Objects.empty()) { + bool result; + if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query), + result)) { + //std::cout << (result ? "VALID" : "INVALID") << "\n"; + return result; + } + } + } + llvm::cout << "FAIL"; + exit(1); +} + + // XXX: give more info int SMTParser::Error(const string& msg) { std::cerr << SMTParser::parserTemp->fileName << ":" diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h index 798e70b3..fd1ec044 100644 --- a/lib/SMT/SMTParser.h +++ b/lib/SMT/SMTParser.h @@ -38,16 +38,17 @@ class SMTParser : public klee::expr::Parser { bool arraysEnabled; std::vector<ExprHandle> assumptions; - klee::expr::ExprHandle query; + klee::expr::ExprHandle satQuery; int bvSize; bool queryParsed; - + klee::ExprBuilder *builder; SMTParser(const std::string filename, ExprBuilder *builder); virtual klee::expr::Decl *ParseTopLevelDecl(); + bool Solve(); virtual void SetMaxErrors(unsigned N) { } @@ -55,15 +56,15 @@ class SMTParser : public klee::expr::Parser { virtual ~SMTParser() {} - void Init(void); - + void Parse(void); + int Error(const std::string& s); int StringToInt(const std::string& s); ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w); - + void DeclareExpr(std::string name, Expr::Width w); - + ExprHandle CreateAnd(std::vector<ExprHandle>); ExprHandle CreateOr(std::vector<ExprHandle>); ExprHandle CreateXor(std::vector<ExprHandle>); diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp index 934f0702..034c4ce4 100644 --- a/lib/SMT/main.cpp +++ b/lib/SMT/main.cpp @@ -36,8 +36,8 @@ int main(int argc, char** argv) { } klee::expr::SMTParser smtParser(argv[1], Builder); - - smtParser.Init(); + smtParser.Parse(); + int result = smtParser.Solve(); - cout << smtParser.query << "\n"; + cout << (result ? "UNSAT":"SAT") << "\n"; } diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y index 28a434c9..01d3539d 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -36,9 +36,8 @@ using namespace klee::expr; #define PARSER SMTParser::parserTemp #define BUILDER SMTParser::parserTemp->builder #define DONE SMTParser::parserTemp->done -#define EXPR SMTParser::parserTemp->query #define ASSUMPTIONS SMTParser::parserTemp->assumptions -#define QUERY SMTParser::parserTemp->query +#define QUERY SMTParser::parserTemp->satQuery #define ARRAYSENABLED (SMTParser::parserTemp->arraysEnabled) #define BVSIZE (SMTParser::parserTemp->bvSize) |