Can S2E use fork to save a symbolic state

[Reaper Lu (Dingisoul)]

Hi Vitaly,

I want to let S2E fork a state on a concrete path in order to save the execution and let it switch back to the forked state to recover the execution state. Like  record and replay

But S2E cannnot fork in a concrete path

Are there any way that we can do it?

Thanks,

Dinigisoul 

[Reaper Lu (Dingisoul)]

Hi Vitaly

I have notice the code in BaseInstruction plugin , I think it can used in this situation, Is it correct ?

void BaseInstructions::forkCount(S2EExecutionState *state) {

target_ulong count;

target_ulong nameptr;

state->jumpToSymbolicCpp();

state->regs()->read(CPU_OFFSET(regs[R_EAX]), &count, sizeof count);

state->regs()->read(CPU_OFFSET(regs[R_ECX]), &nameptr, sizeof nameptr);

std::string name;

if (!state->mem()->readString(nameptr, name)) {

getWarningsStream(state) << "Could not read string at address " << hexval(nameptr) << "\n";

state->regs()->write<target_ulong>(CPU_OFFSET(regs[R_EAX]), -1);

return;

}

klee::ref<klee::Expr> var = state->createSymbolicValue<uint32_t>(name, 0);

state->regs()->write(CPU_OFFSET(regs[R_EAX]), var);

state->regs()->write<target_ulong>(CPU_OFFSET(eip), state->regs()->getPc() + 10);

getDebugStream(state) << "s2e_fork: will fork " << count << " times with variable " << var << "\n";

for (unsigned i = 1; i < count; ++i) {

klee::ref<klee::Expr> val = klee::ConstantExpr::create(i, var->getWidth());

klee::ref<klee::Expr> cond = klee::NeExpr::create(var, val);

klee::Executor::StatePair sp = s2e()->getExecutor()->forkCondition(state, cond, true);

assert(sp.first == state);

assert(sp.second && sp.second != sp.first);

}

klee::ref<klee::Expr> cond = klee::EqExpr::create(var, klee::ConstantExpr::create(0, var->getWidth()));

if (!state->addConstraint(cond)) {

s2e()->getExecutor()->terminateState(*state, "Could not add condition");

}

[Vitaly Chipounov]

Hi,

 

Yes, you can use forkCount() for that. Note that the function you pasted looks very old. The new version [1] does not require creating symbolic variables and adding constraints.

Vitaly

[1] https://github.com/S2E/s2e/blob/master/libs2eplugins/src/s2e/Plugins/Core/BaseInstructions.cpp#L729

--
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/b68f4439-6ece-486f-b1db-ec91f1973f59n%40googlegroups.com.

[Reaper Lu (Dingisoul)]

Hi Vitaly,

I want to save the state (not to switch to this state) , I find that it needs to implement my own searcher, so I implement one.

I find that s2e switch state using timer or terminate current state, can I switch the state by myself

Thanks,

Dingisoul

[Reaper Lu (Dingisoul)]

Hi Vitaly,

I have found the suspendstate API,  I will test it in my project

Thanks,

Dingisoul