diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-07-25 11:50:24 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-07-25 11:50:24 +0100 |
commit | 7b53061d746e39a04b1a2d79dcced3f4b5f74fdb (patch) | |
tree | ed92b7f7f558e2f7fadaa5c3f2145453d66d874c | |
parent | d40f29066ab9d5cb998a3bb38d2082a231c50d60 (diff) | |
parent | c77b0052785a7ead9cb80a37a53de2229e2f0726 (diff) | |
download | klee-7b53061d746e39a04b1a2d79dcced3f4b5f74fdb.tar.gz |
Merge pull request #725 from ccadar/fold
Refactored some code related to constant evaluation
-rw-r--r-- | include/klee/Internal/Module/KModule.h | 4 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 69 | ||||
-rw-r--r-- | lib/Core/Executor.h | 5 | ||||
-rw-r--r-- | lib/Core/ExecutorUtil.cpp | 69 | ||||
-rw-r--r-- | lib/Module/KModule.cpp | 6 |
5 files changed, 76 insertions, 77 deletions
diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h index f0f20394..41253383 100644 --- a/include/klee/Internal/Module/KModule.h +++ b/include/klee/Internal/Module/KModule.h @@ -97,8 +97,8 @@ namespace klee { InstructionInfoTable *infos; std::vector<llvm::Constant*> constants; - std::map<llvm::Constant*, KConstant*> constantMap; - KConstant* getKConstant(llvm::Constant *c); + std::map<const llvm::Constant*, KConstant*> constantMap; + KConstant* getKConstant(const llvm::Constant *c); Cell *constantTable; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 5560a3e5..dd4c8f47 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1011,75 +1011,6 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) { ConstantExpr::alloc(1, Expr::Bool)); } -ref<klee::ConstantExpr> Executor::evalConstant(const Constant *c) { - if (const llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(c)) { - return evalConstantExpr(ce); - } else { - if (const ConstantInt *ci = dyn_cast<ConstantInt>(c)) { - return ConstantExpr::alloc(ci->getValue()); - } else if (const ConstantFP *cf = dyn_cast<ConstantFP>(c)) { - return ConstantExpr::alloc(cf->getValueAPF().bitcastToAPInt()); - } else if (const GlobalValue *gv = dyn_cast<GlobalValue>(c)) { - return globalAddresses.find(gv)->second; - } else if (isa<ConstantPointerNull>(c)) { - return Expr::createPointer(0); - } else if (isa<UndefValue>(c) || isa<ConstantAggregateZero>(c)) { - return ConstantExpr::create(0, getWidthForLLVMType(c->getType())); - } else if (const ConstantDataSequential *cds = - dyn_cast<ConstantDataSequential>(c)) { - std::vector<ref<Expr> > kids; - for (unsigned i = 0, e = cds->getNumElements(); i != e; ++i) { - ref<Expr> kid = evalConstant(cds->getElementAsConstant(i)); - kids.push_back(kid); - } - ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data()); - return cast<ConstantExpr>(res); - } else if (const ConstantStruct *cs = dyn_cast<ConstantStruct>(c)) { - const StructLayout *sl = kmodule->targetData->getStructLayout(cs->getType()); - llvm::SmallVector<ref<Expr>, 4> kids; - for (unsigned i = cs->getNumOperands(); i != 0; --i) { - unsigned op = i-1; - ref<Expr> kid = evalConstant(cs->getOperand(op)); - - uint64_t thisOffset = sl->getElementOffsetInBits(op), - nextOffset = (op == cs->getNumOperands() - 1) - ? sl->getSizeInBits() - : sl->getElementOffsetInBits(op+1); - if (nextOffset-thisOffset > kid->getWidth()) { - uint64_t paddingWidth = nextOffset-thisOffset-kid->getWidth(); - kids.push_back(ConstantExpr::create(0, paddingWidth)); - } - - kids.push_back(kid); - } - ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data()); - return cast<ConstantExpr>(res); - } else if (const ConstantArray *ca = dyn_cast<ConstantArray>(c)){ - llvm::SmallVector<ref<Expr>, 4> kids; - for (unsigned i = ca->getNumOperands(); i != 0; --i) { - unsigned op = i-1; - ref<Expr> kid = evalConstant(ca->getOperand(op)); - kids.push_back(kid); - } - ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data()); - return cast<ConstantExpr>(res); - } else if (const ConstantVector *cv = dyn_cast<ConstantVector>(c)) { - llvm::SmallVector<ref<Expr>, 8> kids; - const size_t numOperands = cv->getNumOperands(); - kids.reserve(numOperands); - for (unsigned i = 0; i < numOperands; ++i) { - kids.push_back(evalConstant(cv->getOperand(i))); - } - ref<Expr> res = ConcatExpr::createN(numOperands, kids.data()); - assert(isa<ConstantExpr>(res) && - "result of constant vector built is not a constant"); - return cast<ConstantExpr>(res); - } else { - llvm::report_fatal_error("invalid argument to evalConstant()"); - } - } -} - const Cell& Executor::eval(KInstruction *ki, unsigned index, ExecutionState &state) const { assert(index < ki->inst->getNumOperands()); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index b8411a20..c9d715ad 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -351,6 +351,8 @@ private: ref<klee::ConstantExpr> evalConstantExpr(const llvm::ConstantExpr *ce); + ref<klee::ConstantExpr> evalConstant(const llvm::Constant *c); + /// Return a unique constant value for the given expression in the /// given state, if it has one (i.e. it provably only has a single /// value). Otherwise return the original expression. @@ -440,9 +442,6 @@ public: return *interpreterHandler; } - // XXX should just be moved out to utility module - ref<klee::ConstantExpr> evalConstant(const llvm::Constant *c); - virtual void setPathWriter(TreeStreamWriter *tsw) { pathWriter = tsw; } diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index bd7c0711..59c04d14 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -33,6 +33,75 @@ using namespace llvm; namespace klee { + ref<klee::ConstantExpr> Executor::evalConstant(const Constant *c) { + if (const llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(c)) { + return evalConstantExpr(ce); + } else { + if (const ConstantInt *ci = dyn_cast<ConstantInt>(c)) { + return ConstantExpr::alloc(ci->getValue()); + } else if (const ConstantFP *cf = dyn_cast<ConstantFP>(c)) { + return ConstantExpr::alloc(cf->getValueAPF().bitcastToAPInt()); + } else if (const GlobalValue *gv = dyn_cast<GlobalValue>(c)) { + return globalAddresses.find(gv)->second; + } else if (isa<ConstantPointerNull>(c)) { + return Expr::createPointer(0); + } else if (isa<UndefValue>(c) || isa<ConstantAggregateZero>(c)) { + return ConstantExpr::create(0, getWidthForLLVMType(c->getType())); + } else if (const ConstantDataSequential *cds = + dyn_cast<ConstantDataSequential>(c)) { + std::vector<ref<Expr> > kids; + for (unsigned i = 0, e = cds->getNumElements(); i != e; ++i) { + ref<Expr> kid = evalConstant(cds->getElementAsConstant(i)); + kids.push_back(kid); + } + ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data()); + return cast<ConstantExpr>(res); + } else if (const ConstantStruct *cs = dyn_cast<ConstantStruct>(c)) { + const StructLayout *sl = kmodule->targetData->getStructLayout(cs->getType()); + llvm::SmallVector<ref<Expr>, 4> kids; + for (unsigned i = cs->getNumOperands(); i != 0; --i) { + unsigned op = i-1; + ref<Expr> kid = evalConstant(cs->getOperand(op)); + + uint64_t thisOffset = sl->getElementOffsetInBits(op), + nextOffset = (op == cs->getNumOperands() - 1) + ? sl->getSizeInBits() + : sl->getElementOffsetInBits(op+1); + if (nextOffset-thisOffset > kid->getWidth()) { + uint64_t paddingWidth = nextOffset-thisOffset-kid->getWidth(); + kids.push_back(ConstantExpr::create(0, paddingWidth)); + } + + kids.push_back(kid); + } + ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data()); + return cast<ConstantExpr>(res); + } else if (const ConstantArray *ca = dyn_cast<ConstantArray>(c)){ + llvm::SmallVector<ref<Expr>, 4> kids; + for (unsigned i = ca->getNumOperands(); i != 0; --i) { + unsigned op = i-1; + ref<Expr> kid = evalConstant(ca->getOperand(op)); + kids.push_back(kid); + } + ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data()); + return cast<ConstantExpr>(res); + } else if (const ConstantVector *cv = dyn_cast<ConstantVector>(c)) { + llvm::SmallVector<ref<Expr>, 8> kids; + const size_t numOperands = cv->getNumOperands(); + kids.reserve(numOperands); + for (unsigned i = 0; i < numOperands; ++i) { + kids.push_back(evalConstant(cv->getOperand(i))); + } + ref<Expr> res = ConcatExpr::createN(numOperands, kids.data()); + assert(isa<ConstantExpr>(res) && + "result of constant vector built is not a constant"); + return cast<ConstantExpr>(res); + } else { + llvm::report_fatal_error("invalid argument to evalConstant()"); + } + } + } + ref<ConstantExpr> Executor::evalConstantExpr(const llvm::ConstantExpr *ce) { llvm::Type *type = ce->getType(); diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 19408d65..751776b9 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -104,7 +104,7 @@ KModule::~KModule() { ie = functions.end(); it != ie; ++it) delete *it; - for (std::map<llvm::Constant*, KConstant*>::iterator it=constantMap.begin(), + for (std::map<const llvm::Constant*, KConstant*>::iterator it=constantMap.begin(), itE=constantMap.end(); it!=itE;++it) delete it->second; @@ -415,8 +415,8 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, } } -KConstant* KModule::getKConstant(Constant *c) { - std::map<llvm::Constant*, KConstant*>::iterator it = constantMap.find(c); +KConstant* KModule::getKConstant(const Constant *c) { + std::map<const llvm::Constant*, KConstant*>::iterator it = constantMap.find(c); if (it != constantMap.end()) return it->second; return NULL; |