aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp17
-rw-r--r--lib/Core/ExecutorUtil.cpp6
-rw-r--r--lib/Core/Memory.cpp4
-rw-r--r--lib/Core/MemoryManager.cpp2
-rw-r--r--lib/Core/SeedInfo.cpp6
5 files changed, 30 insertions, 5 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index fece4af9..ab2e106a 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -628,6 +628,7 @@ void Executor::branch(ExecutionState &state,
solver->getValue(state, siit->assignment.evaluate(conditions[i]),
res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (res->getConstantValue())
break;
}
@@ -683,6 +684,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
ref<ConstantExpr> value;
bool success = solver->getValue(current, condition, value);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
addConstraint(current, EqExpr::create(value, condition));
condition = value;
}
@@ -752,6 +754,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
bool success =
solver->getValue(current, siit->assignment.evaluate(condition), res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(res)) {
if (CE->getConstantValue()) {
trueSeed = true;
@@ -817,6 +820,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
bool success =
solver->getValue(current, siit->assignment.evaluate(condition), res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (res->getConstantValue()) {
trueSeeds.push_back(*siit);
} else {
@@ -889,6 +893,7 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
bool success =
solver->mustBeFalse(state, siit->assignment.evaluate(condition), res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (res) {
siit->patchSeed(state, condition, solver);
warn = true;
@@ -1026,6 +1031,7 @@ Executor::toConstant(ExecutionState &state,
ref<ConstantExpr> value;
bool success = solver->getValue(state, e, value);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
std::ostringstream os;
os << "silently concretizing (reason: " << reason << ") expression " << e
@@ -1052,6 +1058,7 @@ void Executor::executeGetValue(ExecutionState &state,
ref<ConstantExpr> value;
bool success = solver->getValue(state, e, value);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
bindLocal(target, state, value);
} else {
std::set< ref<Expr> > values;
@@ -1061,6 +1068,7 @@ void Executor::executeGetValue(ExecutionState &state,
bool success =
solver->getValue(state, siit->assignment.evaluate(e), value);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
values.insert(value);
}
@@ -1409,6 +1417,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
bool result;
bool success = solver->mayBeTrue(state, match, result);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (result) {
std::map<BasicBlock*, ref<Expr> >::iterator it =
targets.insert(std::make_pair(si->getSuccessor(i),
@@ -1419,6 +1428,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
bool res;
bool success = solver->mayBeTrue(state, isDefault, res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (res)
targets.insert(std::make_pair(si->getSuccessor(0), isDefault));
@@ -1532,6 +1542,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
ref<ConstantExpr> value;
bool success = solver->getValue(*free, v, value);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
StatePair res = fork(*free, EqExpr::create(v, value), true);
if (res.first) {
void *addr = (void*) (unsigned long) value->getConstantValue();
@@ -2358,6 +2369,7 @@ std::string Executor::getAddressInfo(ExecutionState &state,
ref<ConstantExpr> value;
bool success = solver->getValue(state, address, value);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
example = value->getConstantValue();
info << "\texample: " << example << "\n";
std::pair< ref<Expr>, ref<Expr> > res = solver->getRange(state, address);
@@ -2524,6 +2536,7 @@ void Executor::callExternalFunction(ExecutionState &state,
ref<ConstantExpr> ce;
bool success = solver->getValue(state, *ai, ce);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &args[i]);
} else {
ref<Expr> arg = toUnique(state, *ai);
@@ -2663,6 +2676,7 @@ void Executor::executeAlloc(ExecutionState &state,
ref<ConstantExpr> example;
bool success = solver->getValue(state, size, example);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
// Try and start with a small example
while (example->getConstantValue() > 128) {
@@ -2672,6 +2686,7 @@ void Executor::executeAlloc(ExecutionState &state,
bool res;
bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (!res)
break;
example = tmp;
@@ -2684,11 +2699,13 @@ void Executor::executeAlloc(ExecutionState &state,
ref<ConstantExpr> tmp;
bool success = solver->getValue(*fixedSize.second, size, tmp);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
bool res;
success = solver->mustBeTrue(*fixedSize.second,
EqExpr::create(tmp, size),
res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (res) {
executeAlloc(*fixedSize.second, tmp, isLocal,
target, zeroMemory, reallocFrom);
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 62aa45db..1e346e89 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -45,6 +45,9 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
if (numOperands > 2) op3 = evalConstant(ce->getOperand(2));
switch (ce->getOpcode()) {
+ default :
+ assert(0 && "unknown ConstantExpr type");
+
case Instruction::Trunc: return ExtractExpr::createByteOff(op1,
0,
Expr::getWidthForLLVMType(type));
@@ -135,9 +138,6 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
case Instruction::FPToSI:
case Instruction::FCmp:
assert(0 && "floating point ConstantExprs unsupported");
-
- default :
- assert(0 && "unknown ConstantExpr type");
}
}
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 5a3af34c..8f144456 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -362,24 +362,24 @@ ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
return read((unsigned) CE->getConstantValue(), width);
} else {
switch (width) {
+ default: assert(0 && "invalid type");
case Expr::Bool: return read1(offset);
case Expr::Int8: return read8(offset);
case Expr::Int16: return read16(offset);
case Expr::Int32: return read32(offset);
case Expr::Int64: return read64(offset);
- default: assert(0 && "invalid type");
}
}
}
ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
switch (width) {
+ default: assert(0 && "invalid type");
case Expr::Bool: return read1(offset);
case Expr::Int8: return read8(offset);
case Expr::Int16: return read16(offset);
case Expr::Int32: return read32(offset);
case Expr::Int64: return read64(offset);
- default: assert(0 && "invalid type");
}
}
diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp
index cec7b7d1..72c1b67f 100644
--- a/lib/Core/MemoryManager.cpp
+++ b/lib/Core/MemoryManager.cpp
@@ -50,12 +50,14 @@ MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, bool isGlobal
MemoryObject *MemoryManager::allocateFixed(uint64_t address, uint64_t size,
const llvm::Value *allocSite) {
+#ifndef NDEBUG
for (objects_ty::iterator it = objects.begin(), ie = objects.end();
it != ie; ++it) {
MemoryObject *mo = *it;
assert(!(address+size > mo->address && address < mo->address+mo->size) &&
"allocated an overlapping object");
}
+#endif
++stats::allocations;
MemoryObject *res = new MemoryObject(address, size, false, true, true,
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index f328823b..6fcfe596 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -97,10 +97,12 @@ void SeedInfo::patchSeed(const ExecutionState &state,
bool res;
bool success = solver->mustBeFalse(tmp, isSeed, res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (res) {
ref<ConstantExpr> value;
bool success = solver->getValue(tmp, read, value);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
it2->second[i] = value->getConstantValue();
tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
} else {
@@ -112,6 +114,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
bool res;
bool success = solver->mayBeTrue(state, assignment.evaluate(condition), res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (res)
return;
@@ -127,10 +130,12 @@ void SeedInfo::patchSeed(const ExecutionState &state,
bool res;
bool success = solver->mustBeFalse(tmp, isSeed, res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
if (res) {
ref<ConstantExpr> value;
bool success = solver->getValue(tmp, read, value);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
it->second[i] = value->getConstantValue();
tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
} else {
@@ -145,6 +150,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
bool success =
solver->mayBeTrue(state, assignment.evaluate(condition), res);
assert(success && "FIXME: Unhandled solver failure");
+ (void) success;
assert(res && "seed patching failed");
}
#endif
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-24 04:22:49 +0000