aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-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
-rw-r--r--lib/Expr/Constraints.cpp3
-rw-r--r--lib/Expr/Expr.cpp38
-rw-r--r--lib/Solver/CexCachingSolver.cpp2
-rw-r--r--lib/Solver/FastCexSolver.cpp7
-rw-r--r--lib/Solver/STPBuilder.cpp2
10 files changed, 78 insertions, 74 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;
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 5869a852..8f89f88a 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -122,7 +122,8 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
switch (e->getKind()) {
case Expr::Constant:
- assert(e->getConstantValue() && "attempt to add invalid (false) constraint");
+ assert(cast<ConstantExpr>(e)->getConstantValue() &&
+ "attempt to add invalid (false) constraint");
break;
// split to enable finer grained independence and other optimizations
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index f95369f4..c645f37c 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -189,11 +189,6 @@ unsigned ReadExpr::computeHash() {
return hashValue;
}
-uint64_t Expr::getConstantValue() const {
- assert(getKind() == Constant);
- return static_cast<const ConstantExpr*>(this)->asUInt64;
-}
-
ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
unsigned numArgs = args.size();
@@ -428,22 +423,26 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
ref<Expr> ConcatExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
Expr::Width w = l->getWidth() + r->getWidth();
- /* Constant folding */
- if (l->getKind() == Expr::Constant && r->getKind() == Expr::Constant) {
- // XXX: should fix this constant limitation soon
- assert(w <= 64 && "ConcatExpr::create(): don't support concats describing constants greater than 64 bits yet");
-
- uint64_t res = (l->getConstantValue() << r->getWidth()) + r->getConstantValue();
- return ConstantExpr::create(res, w);
+ // Fold concatenation of constants.
+ //
+ // FIXME: concat 0 x -> zext x ?
+ if (ConstantExpr *lCE = dyn_cast<ConstantExpr>(l)) {
+ if (ConstantExpr *rCE = dyn_cast<ConstantExpr>(r)) {
+ assert(w <= 64 && "ConcatExpr::create(): don't support concats describing constants greater than 64 bits yet");
+
+ uint64_t res = (lCE->getConstantValue() << rCE->getWidth()) +
+ rCE->getConstantValue();
+ return ConstantExpr::create(res, w);
+ }
}
// Merge contiguous Extracts
- if (l->getKind() == Expr::Extract && r->getKind() == Expr::Extract) {
- const ExtractExpr* ee_left = cast<ExtractExpr>(l);
- const ExtractExpr* ee_right = cast<ExtractExpr>(r);
- if (ee_left->expr == ee_right->expr &&
- ee_right->offset + ee_right->width == ee_left->offset) {
- return ExtractExpr::create(ee_left->expr, ee_right->offset, w);
+ if (ExtractExpr *ee_left = dyn_cast<ExtractExpr>(l)) {
+ if (ExtractExpr *ee_right = dyn_cast<ExtractExpr>(r)) {
+ if (ee_left->expr == ee_right->expr &&
+ ee_right->offset + ee_right->width == ee_left->offset) {
+ return ExtractExpr::create(ee_left->expr, ee_right->offset, w);
+ }
}
}
@@ -949,7 +948,8 @@ static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &cl,
return res;
for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
- if (un->index != first_idx_match && un->value->getConstantValue() == ct) {
+ if (un->index != first_idx_match &&
+ cast<ConstantExpr>(un->value)->getConstantValue() == ct) {
ref<Expr> curr_eq = EqExpr::create(un->index, rd->index);
res = OrExpr::create(curr_eq, res);
}
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 1eaec4d9..9c233530 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -220,7 +220,7 @@ bool CexCachingSolver::computeValidity(const Query& query,
assert(isa<ConstantExpr>(q) &&
"assignment evaluation did not result in constant");
- if (q->getConstantValue()) {
+ if (cast<ConstantExpr>(q)->getConstantValue()) {
if (!getAssignment(query, a))
return false;
result = !a ? Solver::True : Solver::Unknown;
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 1a1cfe62..6d9c8551 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -730,10 +730,9 @@ public:
bool exprMustBeValue(ref<Expr> e, uint64_t value) {
CexConstifier cc(objectValues);
ref<Expr> v = cc.visit(e);
- if (!isa<ConstantExpr>(v)) return false;
- // XXX reenable once all reads and vars are fixed
- // assert(v.isConstant() && "not all values have been fixed");
- return v->getConstantValue() == value;
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(v))
+ return CE->getConstantValue() == value;
+ return false;
}
};
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 88bdd2b0..5b3fdd60 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -449,7 +449,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
switch (e->getKind()) {
case Expr::Constant: {
- uint64_t asUInt64 = e->getConstantValue();
+ uint64_t asUInt64 = cast<ConstantExpr>(e)->getConstantValue();
*width_out = e->getWidth();
if (*width_out > 64)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-16 05:35:49 +0000