Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

option --use-concolic-taint=true:no addConstraint #6

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+14 −4
Open

option --use-concolic-taint=true:no addConstraint #6

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions klee/include/klee/Executor.h
View file
Original file line number Diff line number Diff line change
@@ -112,6 +112,7 @@ class Executor : public Interpreter {
std::vector<TimerInfo*> timers;
PTree *processTree;
bool concolicMode;
bool concolicTaint;

/// Used to track states that have been added during the current
/// instructions step.
11 changes: 7 additions & 4 deletions klee/lib/Core/Executor.cpp
View file
Original file line number Diff line number Diff line change
@@ -354,6 +354,7 @@ Executor::Executor(const InterpreterOptions &opts,
specialFunctionHandler(0),
processTree(0),
concolicMode(false),
concolicTaint(false),
replayOut(0),
replayPath(0),
usingSeeds(0),
@@ -812,12 +813,14 @@ Executor::concolicFork(ExecutionState &current, ref<Expr> condition, bool isInte

if (current.forkDisabled) {
if (ce->isTrue()) {
//Condition is true in the current state
addConstraint(current, condition);
if(!concolicTaint)
//Condition is true in the current state
addConstraint(current, condition);
return StatePair(&current, 0);
} else {
//Condition is false in the current state
addConstraint(current, Expr::createIsZero(condition));
if(!concolicTaint)
//Condition is false in the current state
addConstraint(current, Expr::createIsZero(condition));
return StatePair(0, &current);
}
}
6 changes: 6 additions & 0 deletions qemu/s2e/S2EExecutor.cpp
View file
Original file line number Diff line number Diff line change
@@ -239,6 +239,11 @@ cl::opt<bool>
ConcolicMode("use-concolic-execution",
cl::desc("Concolic execution mode"), cl::init(true));

// Disable fork and use make_concolic to use Concolic Taint
cl::opt<bool>
ConcolicTaint("use-concolic-taint",
cl::desc("Single Concolic Taint"), cl::init(false));

cl::opt<bool>
DebugConstraints("debug-constraints",
cl::desc("Check that added constraints are satisfiable"), cl::init(false));
@@ -856,6 +861,7 @@ S2EExecutor::S2EExecutor(S2E* s2e, TCGLLVMContext *tcgLLVMContext,
g_s2e_concretize_io_writes = ConcretizeIoWrites;

concolicMode = ConcolicMode;
concolicTaint = ConcolicTaint;

if (UseFastHelpers) {
if (!ForkOnSymbolicAddress) {