aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp69
-rw-r--r--lib/Core/Executor.h5
-rw-r--r--lib/Core/ExecutorUtil.cpp69
3 files changed, 71 insertions, 72 deletions
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();