aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp74
-rw-r--r--lib/Core/Executor.h3
-rw-r--r--lib/Core/ImpliedValue.cpp10
-rw-r--r--lib/Core/ImpliedValue.h3
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp10
5 files changed, 52 insertions, 48 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index aa8681dc..21356af9 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1015,31 +1015,31 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
/* Concretize the given expression, and return a possible constant value.
'reason' is just a documentation string stating the reason for concretization. */
-ref<Expr> Executor::toConstant(ExecutionState &state,
- ref<Expr> e,
- const char *reason) {
+ref<klee::ConstantExpr>
+Executor::toConstant(ExecutionState &state,
+ ref<Expr> e,
+ const char *reason) {
e = state.constraints.simplifyExpr(e);
- if (!isa<ConstantExpr>(e)) {
- ref<ConstantExpr> value;
- bool success = solver->getValue(state, e, value);
- assert(success && "FIXME: Unhandled solver failure");
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
+ return CE;
+
+ ref<ConstantExpr> value;
+ bool success = solver->getValue(state, e, value);
+ assert(success && "FIXME: Unhandled solver failure");
- std::ostringstream os;
- os << "silently concretizing (reason: " << reason << ") expression " << e
- << " to value " << value
- << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")";
+ std::ostringstream os;
+ os << "silently concretizing (reason: " << reason << ") expression " << e
+ << " to value " << value
+ << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")";
- if (AllExternalWarnings)
- klee_warning(reason, os.str().c_str());
- else
- klee_warning_once(reason, "%s", os.str().c_str());
+ if (AllExternalWarnings)
+ klee_warning(reason, os.str().c_str());
+ else
+ klee_warning_once(reason, "%s", os.str().c_str());
- addConstraint(state, EqExpr::create(e, value));
+ addConstraint(state, EqExpr::create(e, value));
- return value;
- } else {
- return e;
- }
+ return value;
}
void Executor::executeGetValue(ExecutionState &state,
@@ -1909,8 +1909,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
case Instruction::FPTrunc: {
FPTruncInst *fi = cast<FPTruncInst>(i);
Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
- ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
- "floating point");
+ ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+ "floating point");
uint64_t value = floats::trunc(arg->getConstantValue(),
resultType,
arg->getWidth());
@@ -1921,8 +1921,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
case Instruction::FPExt: {
FPExtInst *fi = cast<FPExtInst>(i);
Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
- ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
- "floating point");
+ ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+ "floating point");
uint64_t value = floats::ext(arg->getConstantValue(),
resultType,
arg->getWidth());
@@ -1933,8 +1933,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
case Instruction::FPToUI: {
FPToUIInst *fi = cast<FPToUIInst>(i);
Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
- ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
- "floating point");
+ ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+ "floating point");
uint64_t value = floats::toUnsignedInt(arg->getConstantValue(),
resultType,
arg->getWidth());
@@ -1945,8 +1945,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
case Instruction::FPToSI: {
FPToSIInst *fi = cast<FPToSIInst>(i);
Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
- ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
- "floating point");
+ ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+ "floating point");
uint64_t value = floats::toSignedInt(arg->getConstantValue(),
resultType,
arg->getWidth());
@@ -1957,8 +1957,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
case Instruction::UIToFP: {
UIToFPInst *fi = cast<UIToFPInst>(i);
Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
- ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
- "floating point");
+ ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+ "floating point");
uint64_t value = floats::UnsignedIntToFP(arg->getConstantValue(),
resultType);
bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
@@ -1968,8 +1968,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
case Instruction::SIToFP: {
SIToFPInst *fi = cast<SIToFPInst>(i);
Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
- ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
- "floating point");
+ ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value,
+ "floating point");
uint64_t value = floats::SignedIntToFP(arg->getConstantValue(),
resultType,
arg->getWidth());
@@ -1980,10 +1980,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
case Instruction::FCmp: {
FCmpInst *fi = cast<FCmpInst>(i);
Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
- ref<Expr> left = toConstant(state, eval(ki, 0, state).value,
- "floating point");
- ref<Expr> right = toConstant(state, eval(ki, 1, state).value,
- "floating point");
+ ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value,
+ "floating point");
+ ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value,
+ "floating point");
uint64_t leftVal = left->getConstantValue();
uint64_t rightVal = right->getConstantValue();
@@ -2804,7 +2804,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
solver->setTimeout(stpTimeout);
if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
address = toConstant(state, address, "resolveOne failure");
- success = state.addressSpace.resolveOne(address->getConstantValue(), op);
+ success = state.addressSpace.resolveOne(cast<ConstantExpr>(address)->getConstantValue(), op);
}
solver->setTimeout(0);
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index ba65cf5a..013d3bb8 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -319,7 +319,8 @@ private:
/// should generally be avoided.
///
/// \param purpose An identify string to printed in case of concretization.
- ref<Expr> toConstant(ExecutionState &state, ref<Expr> e, const char *purpose);
+ ref<klee::ConstantExpr> toConstant(ExecutionState &state, ref<Expr> e,
+ const char *purpose);
/// Bind a constant value for e to the given target. NOTE: This
/// function may fork state if the state has multiple seeds.
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 6ad0f5d2..e1daca2f 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -30,7 +30,8 @@ static void _getImpliedValue(ref<Expr> e,
ImpliedValueList &results) {
switch (e->getKind()) {
case Expr::Constant: {
- assert(value == e->getConstantValue() && "error in implied value calculation");
+ assert(value == cast<ConstantExpr>(e)->getConstantValue() &&
+ "error in implied value calculation");
break;
}
@@ -203,14 +204,15 @@ void ImpliedValue::getImpliedValues(ref<Expr> e,
void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
ref<ConstantExpr> value) {
std::vector<ref<ReadExpr> > reads;
- std::map<ref<ReadExpr>, ref<Expr> > found;
+ std::map<ref<ReadExpr>, ref<ConstantExpr> > found;
ImpliedValueList results;
getImpliedValues(e, value, results);
for (ImpliedValueList::iterator i = results.begin(), ie = results.end();
i != ie; ++i) {
- std::map<ref<ReadExpr>, ref<Expr> >::iterator it = found.find(i->first);
+ std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it =
+ found.find(i->first);
if (it != found.end()) {
assert(it->second->getConstantValue() == i->second->getConstantValue() &&
"I don't think so Scott");
@@ -247,7 +249,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
ref<ConstantExpr> possible;
bool success = S->getValue(Query(assume, var), possible);
assert(success && "FIXME: Unhandled solver failure");
- std::map<ref<ReadExpr>, ref<Expr> >::iterator it = found.find(var);
+ std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it = found.find(var);
bool res;
success = S->mustBeTrue(Query(assume, EqExpr::create(var, possible)), res);
assert(success && "FIXME: Unhandled solver failure");
diff --git a/lib/Core/ImpliedValue.h b/lib/Core/ImpliedValue.h
index cbc55dc5..6bdb6c66 100644
--- a/lib/Core/ImpliedValue.h
+++ b/lib/Core/ImpliedValue.h
@@ -26,7 +26,8 @@ namespace klee {
class ReadExpr;
class Solver;
- typedef std::vector< std::pair<ref<ReadExpr>, ref<Expr> > > ImpliedValueList;
+ typedef std::vector< std::pair<ref<ReadExpr>,
+ ref<ConstantExpr> > > ImpliedValueList;
namespace ImpliedValue {
void getImpliedValues(ref<Expr> e, ref<ConstantExpr> cvalue,
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index ea2594eb..2ee73457 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -419,7 +419,7 @@ void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state,
assert(isa<ConstantExpr>(arguments[0]) &&
"symbolic argument given to klee_under_constrained!");
- unsigned v = arguments[0]->getConstantValue();
+ unsigned v = cast<ConstantExpr>(arguments[0])->getConstantValue();
llvm::cerr << "argument = " << v << " under=" << state.underConstrained << "\n";
if(v) {
assert(state.underConstrained == false &&
@@ -599,14 +599,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
} else {
ObjectPair op;
- if (!state.addressSpace.resolveOne(address->getConstantValue(), op)) {
+ if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address)->getConstantValue(), op)) {
executor.terminateStateOnError(state,
"check_memory_access: memory error",
"ptr.err",
executor.getAddressInfo(state, address));
} else {
ref<Expr> chk = op.first->getBoundsCheckPointer(address,
- size->getConstantValue());
+ cast<ConstantExpr>(size)->getConstantValue());
if (!cast<ConstantExpr>(chk)->getConstantValue()) {
executor.terminateStateOnError(state,
"check_memory_access: memory error",
@@ -636,8 +636,8 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
assert(isa<ConstantExpr>(arguments[1]) &&
"expect constant size argument to klee_define_fixed_object");
- uint64_t address = arguments[0]->getConstantValue();
- uint64_t size = arguments[1]->getConstantValue();
+ uint64_t address = cast<ConstantExpr>(arguments[0])->getConstantValue();
+ uint64_t size = cast<ConstantExpr>(arguments[1])->getConstantValue();
MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst);
executor.bindObjectInState(state, mo, false);
mo->isUserSpecified = true; // XXX hack;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-14 18:28:30 +0000