diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 29 | ||||
| -rw-r--r-- | lib/Core/SeedInfo.cpp | 23 |
2 files changed, 23 insertions, 29 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index bc9e31f7..89072490 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4568,13 +4568,11 @@ void Executor::executeMakeSymbolic(ExecutionState &state, bindObjectInState(state, mo, false, array); state.addSymbolic(mo, array); - std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = - seedMap.find(&state); - if (it!=seedMap.end()) { // In seed mode we need to add this as a - // binding. - for (std::vector<SeedInfo>::iterator siit = it->second.begin(), - siie = it->second.end(); siit != siie; ++siit) { - SeedInfo &si = *siit; + auto found = seedMap.find(&state); + if (found != seedMap.end()) { + // In seed mode we need to add this as binding + + for (SeedInfo &si : found->second) { KTestObject *obj = si.getNextInput(mo, NamedSeedMatching); if (!obj) { @@ -4582,26 +4580,27 @@ void Executor::executeMakeSymbolic(ExecutionState &state, std::vector<unsigned char> &values = si.assignment.bindings[array]; values = std::vector<unsigned char>(mo->size, '\0'); } else if (!AllowSeedExtension) { - terminateStateOnUserError(state, "ran out of inputs during seeding"); + terminateStateOnUserError(state, + "ran out of inputs during seeding"); break; } } else { - if (obj->numBytes != mo->size && - ((!(AllowSeedExtension || ZeroSeedExtension) - && obj->numBytes < mo->size) || - (!AllowSeedTruncation && obj->numBytes > mo->size))) { - std::stringstream msg; + /* The condition below implies obj->numBytes != mo->size */ + if ((obj->numBytes < mo->size && !(AllowSeedExtension || ZeroSeedExtension)) || + (obj->numBytes > mo->size && !AllowSeedTruncation)) { + std::stringstream msg; msg << "replace size mismatch: " << mo->name << "[" << mo->size << "]" << " vs " << obj->name << "[" << obj->numBytes << "]" << " in test\n"; - terminateStateOnUserError(state, msg.str()); break; } else { + /* Either sizes are equal or seed extension/trucation is allowed */ std::vector<unsigned char> &values = si.assignment.bindings[array]; - values.insert(values.begin(), obj->bytes, + values.insert(values.begin(), obj->bytes, obj->bytes + std::min(obj->numBytes, mo->size)); + if (ZeroSeedExtension) { for (unsigned i=obj->numBytes; i<mo->size; ++i) values.push_back('\0'); diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index 55f4ed48..ddc40b26 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -74,27 +74,22 @@ void SeedInfo::patchSeed(const ExecutionState &state, std::set< std::pair<const Array*, unsigned> > directReads; std::vector< ref<ReadExpr> > reads; findReads(condition, false, reads); - for (std::vector< ref<ReadExpr> >::iterator it = reads.begin(), - ie = reads.end(); it != ie; ++it) { - ReadExpr *re = it->get(); + for (auto const &re : reads) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) { directReads.insert(std::make_pair(re->updates.root, (unsigned) CE->getZExtValue(32))); } } - - for (std::set< std::pair<const Array*, unsigned> >::iterator - it = directReads.begin(), ie = directReads.end(); it != ie; ++it) { - const Array *array = it->first; - unsigned i = it->second; + + for (auto const &[array, i] : directReads) { ref<Expr> read = ReadExpr::create(UpdateList(array, 0), ConstantExpr::alloc(i, Expr::Int32)); - // If not in bindings then this can't be a violation? - Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array); - if (it2 != assignment.bindings.end()) { + // If not in bindings, then this can't be a violation? + auto a = assignment.bindings.find(array); + if (a != assignment.bindings.end()) { ref<Expr> isSeed = EqExpr::create(read, - ConstantExpr::alloc(it2->second[i], + ConstantExpr::alloc(a->second[i], Expr::Int8)); bool res; bool success = @@ -107,9 +102,9 @@ void SeedInfo::patchSeed(const ExecutionState &state, solver->getValue(required, read, value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void) success; - it2->second[i] = value->getZExtValue(8); + a->second[i] = value->getZExtValue(8); cm.addConstraint(EqExpr::create( - read, ConstantExpr::alloc(it2->second[i], Expr::Int8))); + read, ConstantExpr::alloc(a->second[i], Expr::Int8))); } else { cm.addConstraint(isSeed); } |