aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/ExecutionState.cpp34
-rw-r--r--lib/Core/Executor.cpp13
-rw-r--r--lib/Core/ExecutorTimers.cpp2
-rw-r--r--lib/Core/ExecutorUtil.cpp5
-rw-r--r--lib/Core/ExternalDispatcher.cpp4
-rw-r--r--lib/Core/ImpliedValue.cpp6
-rw-r--r--lib/Core/Memory.cpp23
-rw-r--r--lib/Core/Searcher.cpp22
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp22
9 files changed, 66 insertions, 65 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 9eb560b8..694b21b1 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -147,7 +147,7 @@ std::ostream &klee::operator<<(std::ostream &os, const MemoryMap &mm) {
bool ExecutionState::merge(const ExecutionState &b) {
if (DebugLogStateMerge)
- llvm::cerr << "-- attempting merge of A:"
+ std::cerr << "-- attempting merge of A:"
<< this << " with B:" << &b << "--\n";
if (pc != b.pc)
return false;
@@ -185,21 +185,21 @@ bool ExecutionState::merge(const ExecutionState &b) {
commonConstraints.begin(), commonConstraints.end(),
std::inserter(bSuffix, bSuffix.end()));
if (DebugLogStateMerge) {
- llvm::cerr << "\tconstraint prefix: [";
+ std::cerr << "\tconstraint prefix: [";
for (std::set< ref<Expr> >::iterator it = commonConstraints.begin(),
ie = commonConstraints.end(); it != ie; ++it)
- llvm::cerr << *it << ", ";
- llvm::cerr << "]\n";
- llvm::cerr << "\tA suffix: [";
+ std::cerr << *it << ", ";
+ std::cerr << "]\n";
+ std::cerr << "\tA suffix: [";
for (std::set< ref<Expr> >::iterator it = aSuffix.begin(),
ie = aSuffix.end(); it != ie; ++it)
- llvm::cerr << *it << ", ";
- llvm::cerr << "]\n";
- llvm::cerr << "\tB suffix: [";
+ std::cerr << *it << ", ";
+ std::cerr << "]\n";
+ std::cerr << "\tB suffix: [";
for (std::set< ref<Expr> >::iterator it = bSuffix.begin(),
ie = bSuffix.end(); it != ie; ++it)
- llvm::cerr << *it << ", ";
- llvm::cerr << "]\n";
+ std::cerr << *it << ", ";
+ std::cerr << "]\n";
}
// We cannot merge if addresses would resolve differently in the
@@ -212,9 +212,9 @@ bool ExecutionState::merge(const ExecutionState &b) {
// and not the other
if (DebugLogStateMerge) {
- llvm::cerr << "\tchecking object states\n";
- llvm::cerr << "A: " << addressSpace.objects << "\n";
- llvm::cerr << "B: " << b.addressSpace.objects << "\n";
+ std::cerr << "\tchecking object states\n";
+ std::cerr << "A: " << addressSpace.objects << "\n";
+ std::cerr << "B: " << b.addressSpace.objects << "\n";
}
std::set<const MemoryObject*> mutated;
@@ -226,22 +226,22 @@ bool ExecutionState::merge(const ExecutionState &b) {
if (ai->first != bi->first) {
if (DebugLogStateMerge) {
if (ai->first < bi->first) {
- llvm::cerr << "\t\tB misses binding for: " << ai->first->id << "\n";
+ std::cerr << "\t\tB misses binding for: " << ai->first->id << "\n";
} else {
- llvm::cerr << "\t\tA misses binding for: " << bi->first->id << "\n";
+ std::cerr << "\t\tA misses binding for: " << bi->first->id << "\n";
}
}
return false;
}
if (ai->second != bi->second) {
if (DebugLogStateMerge)
- llvm::cerr << "\t\tmutated: " << ai->first->id << "\n";
+ std::cerr << "\t\tmutated: " << ai->first->id << "\n";
mutated.insert(ai->first);
}
}
if (ai!=ae || bi!=be) {
if (DebugLogStateMerge)
- llvm::cerr << "\t\tmappings differ\n";
+ std::cerr << "\t\tmappings differ\n";
return false;
}
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 35238793..d865bcb5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1074,7 +1074,8 @@ void Executor::executeGetValue(ExecutionState &state,
void Executor::stepInstruction(ExecutionState &state) {
if (DebugPrintInstructions) {
printFileLine(state, state.pc);
- llvm::cerr << std::setw(10) << stats::instructions << " " << *state.pc->inst;
+ std::cerr << std::setw(10) << stats::instructions << " ";
+ llvm::errs() << *(state.pc->inst);
}
if (statsTracker)
@@ -1273,9 +1274,9 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
void Executor::printFileLine(ExecutionState &state, KInstruction *ki) {
const InstructionInfo &ii = *ki->info;
if (ii.file != "")
- llvm::cerr << " " << ii.file << ":" << ii.line << ":";
+ std::cerr << " " << ii.file << ":" << ii.line << ":";
else
- llvm::cerr << " [no debug info]:";
+ std::cerr << " [no debug info]:";
}
@@ -2374,7 +2375,7 @@ void Executor::run(ExecutionState &initialState) {
dump:
if (DumpStatesOnHalt && !states.empty()) {
- llvm::cerr << "KLEE: halting execution, dumping remaining states\n";
+ std::cerr << "KLEE: halting execution, dumping remaining states\n";
for (std::set<ExecutionState*>::iterator
it = states.begin(), ie = states.end();
it != ie; ++it) {
@@ -2558,7 +2559,7 @@ void Executor::callExternalFunction(ExecutionState &state,
return;
if (NoExternals && !okExternals.count(function->getName())) {
- llvm::cerr << "KLEE:ERROR: Calling not-OK external function : "
+ std::cerr << "KLEE:ERROR: Calling not-OK external function : "
<< function->getNameStr() << "\n";
terminateStateOnError(state, "externals disallowed", "user.err");
return;
@@ -2653,7 +2654,7 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
Expr::getMinBytesForWidth(e->getWidth()));
ref<Expr> res = Expr::createTempRead(array, e->getWidth());
ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
- llvm::cerr << "Making symbolic: " << eq << "\n";
+ std::cerr << "Making symbolic: " << eq << "\n";
state.addConstraint(eq);
return res;
}
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 0c274d5c..8934a6cd 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -47,7 +47,7 @@ public:
~HaltTimer() {}
void run() {
- llvm::cerr << "KLEE: HaltTimer invoked\n";
+ std::cerr << "KLEE: HaltTimer invoked\n";
executor->setHaltExecution(true);
}
};
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 69bb2017..32fee991 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -24,7 +24,6 @@
#include "llvm/ModuleProvider.h"
#include "llvm/Support/CallSite.h"
#include "llvm/Support/GetElementPtrTypeIterator.h"
-#include "llvm/Support/Streams.h"
#include "llvm/Target/TargetData.h"
#include <iostream>
#include <cassert>
@@ -47,8 +46,8 @@ namespace klee {
switch (ce->getOpcode()) {
default :
ce->dump();
- llvm::cerr << "error: unknown ConstantExpr type\n"
- << "opcode: " << ce->getOpcode() << "\n";
+ std::cerr << "error: unknown ConstantExpr type\n"
+ << "opcode: " << ce->getOpcode() << "\n";
abort();
case Instruction::Trunc:
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index e5b00b7f..94dad33c 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -18,11 +18,11 @@
#include "llvm/ExecutionEngine/GenericValue.h"
#include "llvm/Support/CallSite.h"
#include "llvm/System/DynamicLibrary.h"
-#include "llvm/Support/Streams.h"
#include "llvm/Support/raw_ostream.h"
#include "llvm/Target/TargetSelect.h"
#include <setjmp.h>
#include <signal.h>
+#include <iostream>
using namespace llvm;
using namespace klee;
@@ -73,7 +73,7 @@ ExternalDispatcher::ExternalDispatcher() {
std::string error;
executionEngine = ExecutionEngine::createJIT(MP, &error);
if (!executionEngine) {
- llvm::cerr << "unable to make jit: " << error << "\n";
+ std::cerr << "unable to make jit: " << error << "\n";
abort();
}
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index a3d30f76..56c1d1a9 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -246,9 +246,9 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
} else {
if (it!=found.end()) {
ref<Expr> binding = it->second;
- llvm::cerr << "checkForImpliedValues: " << e << " = " << value << "\n"
- << "\t\t implies " << var << " == " << binding
- << " (error)\n";
+ std::cerr << "checkForImpliedValues: " << e << " = " << value << "\n"
+ << "\t\t implies " << var << " == " << binding
+ << " (error)\n";
assert(0);
}
}
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index aa170ceb..08c0696c 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -22,6 +22,7 @@
#include <llvm/Instruction.h>
#include <llvm/Value.h>
#include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
#include <iostream>
#include <cassert>
@@ -65,7 +66,7 @@ MemoryObject::~MemoryObject() {
}
void MemoryObject::getAllocInfo(std::string &result) const {
- std::ostringstream info;
+ llvm::raw_string_ostream info(result);
info << "MO" << id << "[" << size << "]";
@@ -83,7 +84,7 @@ void MemoryObject::getAllocInfo(std::string &result) const {
info << " (no allocation info)";
}
- result = info.str();
+ info.flush();
}
/***/
@@ -558,23 +559,23 @@ void ObjectState::write64(unsigned offset, uint64_t value) {
}
void ObjectState::print() {
- llvm::cerr << "-- ObjectState --\n";
- llvm::cerr << "\tMemoryObject ID: " << object->id << "\n";
- llvm::cerr << "\tRoot Object: " << updates.root << "\n";
- llvm::cerr << "\tSize: " << size << "\n";
+ std::cerr << "-- ObjectState --\n";
+ std::cerr << "\tMemoryObject ID: " << object->id << "\n";
+ std::cerr << "\tRoot Object: " << updates.root << "\n";
+ std::cerr << "\tSize: " << size << "\n";
- llvm::cerr << "\tBytes:\n";
+ std::cerr << "\tBytes:\n";
for (unsigned i=0; i<size; i++) {
- llvm::cerr << "\t\t["<<i<<"]"
+ std::cerr << "\t\t["<<i<<"]"
<< " concrete? " << isByteConcrete(i)
<< " known-sym? " << isByteKnownSymbolic(i)
<< " flushed? " << isByteFlushed(i) << " = ";
ref<Expr> e = read8(i);
- llvm::cerr << e << "\n";
+ std::cerr << e << "\n";
}
- llvm::cerr << "\tUpdates:\n";
+ std::cerr << "\tUpdates:\n";
for (const UpdateNode *un=updates.head; un; un=un->next) {
- llvm::cerr << "\t\t[" << un->index << "] = " << un->value << "\n";
+ std::cerr << "\t\t[" << un->index << "] = " << un->value << "\n";
}
}
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 4c94c59b..6fa75a26 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -374,17 +374,17 @@ ExecutionState &MergingSearcher::selectState() {
}
if (DebugLogMerge)
- llvm::cerr << "-- all at merge --\n";
+ std::cerr << "-- all at merge --\n";
for (std::map<Instruction*, std::vector<ExecutionState*> >::iterator
it = merges.begin(), ie = merges.end(); it != ie; ++it) {
if (DebugLogMerge) {
- llvm::cerr << "\tmerge: " << it->first << " [";
+ std::cerr << "\tmerge: " << it->first << " [";
for (std::vector<ExecutionState*>::iterator it2 = it->second.begin(),
ie2 = it->second.end(); it2 != ie2; ++it2) {
ExecutionState *state = *it2;
- llvm::cerr << state << ", ";
+ std::cerr << state << ", ";
}
- llvm::cerr << "]\n";
+ std::cerr << "]\n";
}
// merge states
@@ -403,13 +403,13 @@ ExecutionState &MergingSearcher::selectState() {
}
}
if (DebugLogMerge && !toErase.empty()) {
- llvm::cerr << "\t\tmerged: " << base << " with [";
+ std::cerr << "\t\tmerged: " << base << " with [";
for (std::set<ExecutionState*>::iterator it = toErase.begin(),
ie = toErase.end(); it != ie; ++it) {
- if (it!=toErase.begin()) llvm::cerr << ", ";
- llvm::cerr << *it;
+ if (it!=toErase.begin()) std::cerr << ", ";
+ std::cerr << *it;
}
- llvm::cerr << "]\n";
+ std::cerr << "]\n";
}
for (std::set<ExecutionState*>::iterator it = toErase.begin(),
ie = toErase.end(); it != ie; ++it) {
@@ -427,7 +427,7 @@ ExecutionState &MergingSearcher::selectState() {
}
if (DebugLogMerge)
- llvm::cerr << "-- merge complete, continuing --\n";
+ std::cerr << "-- merge complete, continuing --\n";
return selectState();
}
@@ -475,7 +475,7 @@ ExecutionState &BatchingSearcher::selectState() {
if (lastState) {
double delta = util::getWallTime()-lastStartTime;
if (delta>timeBudget*1.1) {
- llvm::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n";
+ std::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n";
timeBudget = delta;
}
}
@@ -541,7 +541,7 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
if (baseSearcher->empty()) {
time *= 2;
- llvm::cerr << "KLEE: increasing time budget to: " << time << "\n";
+ std::cerr << "KLEE: increasing time budget to: " << time << "\n";
baseSearcher->update(0, pausedStates, std::set<ExecutionState*>());
pausedStates.clear();
}
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 45202c19..ba86428d 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -216,7 +216,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state,
//XXX:DRE:TAINT
if(state.underConstrained) {
- llvm::cerr << "TAINT: skipping abort fail\n";
+ std::cerr << "TAINT: skipping abort fail\n";
executor.terminateState(state);
} else {
executor.terminateStateOnError(state, "abort failure", "abort.err");
@@ -244,7 +244,7 @@ void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state,
"invalid number of arguments to klee_alias_function");
std::string old_fn = readStringAtAddress(state, arguments[0]);
std::string new_fn = readStringAtAddress(state, arguments[1]);
- //llvm::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n";
+ //std::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n";
if (old_fn == new_fn)
state.removeFnAlias(old_fn);
else state.addFnAlias(old_fn, new_fn);
@@ -257,7 +257,7 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state,
//XXX:DRE:TAINT
if(state.underConstrained) {
- llvm::cerr << "TAINT: skipping assertion:"
+ std::cerr << "TAINT: skipping assertion:"
<< readStringAtAddress(state, arguments[0]) << "\n";
executor.terminateState(state);
} else
@@ -273,7 +273,7 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state,
//XXX:DRE:TAINT
if(state.underConstrained) {
- llvm::cerr << "TAINT: skipping assertion:"
+ std::cerr << "TAINT: skipping assertion:"
<< readStringAtAddress(state, arguments[0]) << "\n";
executor.terminateState(state);
} else
@@ -291,7 +291,7 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state,
//XXX:DRE:TAINT
if(state.underConstrained) {
- llvm::cerr << "TAINT: skipping klee_report_error:"
+ std::cerr << "TAINT: skipping klee_report_error:"
<< readStringAtAddress(state, arguments[2]) << ":"
<< readStringAtAddress(state, arguments[3]) << "\n";
executor.terminateState(state);
@@ -409,7 +409,7 @@ void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
"invalid number of arguments to klee_print_expr");
std::string msg_str = readStringAtAddress(state, arguments[0]);
- llvm::cerr << msg_str << ":" << arguments[1] << "\n";
+ std::cerr << msg_str << ":" << arguments[1] << "\n";
}
void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
@@ -456,7 +456,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
"invalid number of arguments to klee_print_range");
std::string msg_str = readStringAtAddress(state, arguments[0]);
- llvm::cerr << msg_str << ":" << arguments[1];
+ std::cerr << msg_str << ":" << arguments[1];
if (!isa<ConstantExpr>(arguments[1])) {
// FIXME: Pull into a unique value method?
ref<ConstantExpr> value;
@@ -468,15 +468,15 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
res);
assert(success && "FIXME: Unhandled solver failure");
if (res) {
- llvm::cerr << " == " << value;
+ std::cerr << " == " << value;
} else {
- llvm::cerr << " ~= " << value;
+ std::cerr << " ~= " << value;
std::pair< ref<Expr>, ref<Expr> > res =
executor.solver->getRange(state, arguments[1]);
- llvm::cerr << " (in [" << res.first << ", " << res.second <<"])";
+ std::cerr << " (in [" << res.first << ", " << res.second <<"])";
}
}
- llvm::cerr << "\n";
+ std::cerr << "\n";
}
void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state,
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-22 22:28:02 +0000