about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2017-07-25 11:50:24 +0100
committerGitHub <noreply@github.com>2017-07-25 11:50:24 +0100
commit7b53061d746e39a04b1a2d79dcced3f4b5f74fdb (patch)
treeed92b7f7f558e2f7fadaa5c3f2145453d66d874c /lib
parentd40f29066ab9d5cb998a3bb38d2082a231c50d60 (diff)
parentc77b0052785a7ead9cb80a37a53de2229e2f0726 (diff)
downloadklee-7b53061d746e39a04b1a2d79dcced3f4b5f74fdb.tar.gz
Merge pull request #725 from ccadar/fold
Refactored some code related to constant evaluation
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp69
-rw-r--r--lib/Core/Executor.h5
-rw-r--r--lib/Core/ExecutorUtil.cpp69
-rw-r--r--lib/Module/KModule.cpp6
4 files changed, 74 insertions, 75 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();
 
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;