Skip to content

Commit e7107dd

Browse files
authored
Merge pull request #109 from S2E/issue/xxx-executor-ref3
Various refactorings (round #3)
2 parents af00fc9 + 190e126 commit e7107dd

File tree

8 files changed

+150
-214
lines changed

8 files changed

+150
-214
lines changed

klee/include/klee/Executor.h

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -107,8 +107,6 @@ class Executor {
107107
/// \invariant \ref addedStates and \ref removedStates are disjoint.
108108
StateSet m_removedStates;
109109

110-
llvm::Function *getTargetFunction(llvm::Value *calledVal);
111-
112110
void executeInstruction(ExecutionState &state, KInstruction *ki);
113111

114112
void initializeGlobalObject(ExecutionState &state, const ObjectStatePtr &os, const llvm::Constant *c,
@@ -127,16 +125,11 @@ class Executor {
127125
void executeMemoryOperation(ExecutionState &state, bool isWrite, ref<Expr> address,
128126
ref<Expr> value /* undef if read */, KInstruction *target /* undef if write */);
129127

130-
/// The current state is about to be branched.
131-
/// Give a chance to S2E to checkpoint the current device state
132-
/// so that the branched state gets it as well.
133-
virtual void notifyBranch(ExecutionState &state);
134-
135128
/// When the fork is complete and state properly updated,
136129
/// notify the S2EExecutor, so that it can generate an onFork event.
137130
/// Sending notification after the fork completed
138131
/// allows plugins to kill states and exit to the CPU loop safely.
139-
virtual void notifyFork(ExecutionState &originalState, ref<Expr> &condition, Executor::StatePair &targets);
132+
virtual void notifyFork(ExecutionState &originalState, ref<Expr> &condition, Executor::StatePair &targets) = 0;
140133

141134
const Cell &eval(KInstruction *ki, unsigned index, LLVMExecutionState &state) const;
142135

@@ -166,8 +159,6 @@ class Executor {
166159
// remove state from queue and delete
167160
virtual void terminateState(ExecutionState &state);
168161

169-
virtual void terminateState(ExecutionState &state, const std::string &reason);
170-
171162
virtual const llvm::Module *setModule(llvm::Module *module);
172163

173164
/*** State accessor methods ***/

klee/lib/Core/Executor.cpp

Lines changed: 35 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -290,11 +290,6 @@ void Executor::initializeGlobals(ExecutionState &state) {
290290
}
291291
}
292292

293-
void Executor::notifyBranch(ExecutionState &state) {
294-
// Should not get here
295-
pabort("Must go through S2E");
296-
}
297-
298293
Executor::StatePair Executor::fork(ExecutionState &current, const ref<Expr> &condition_,
299294
bool keepConditionTrueInCurrentState) {
300295
auto condition = current.simplifyExpr(condition_);
@@ -361,7 +356,6 @@ Executor::StatePair Executor::fork(ExecutionState &current, const ref<Expr> &con
361356
}
362357

363358
// Branch
364-
notifyBranch(current);
365359
auto branchedState = current.clone();
366360
m_addedStates.insert(branchedState);
367361

@@ -405,7 +399,6 @@ Executor::StatePair Executor::fork(ExecutionState &current) {
405399
return StatePair(&current, nullptr);
406400
}
407401

408-
notifyBranch(current);
409402
auto clonedState = current.clone();
410403
m_addedStates.insert(clonedState);
411404

@@ -415,11 +408,6 @@ Executor::StatePair Executor::fork(ExecutionState &current) {
415408
return StatePair(&current, clonedState);
416409
}
417410

418-
void Executor::notifyFork(ExecutionState &originalState, ref<Expr> &condition, Executor::StatePair &targets) {
419-
// Should not get here
420-
pabort("Must go through S2E");
421-
}
422-
423411
const Cell &Executor::eval(KInstruction *ki, unsigned index, LLVMExecutionState &state) const {
424412
assert(index < ki->inst->getNumOperands());
425413
int vnumber = ki->operands[index];
@@ -449,6 +437,41 @@ static inline const llvm::fltSemantics *fpWidthToSemantics(unsigned width) {
449437
}
450438
}
451439

440+
/// Compute the true target of a function call, resolving LLVM aliases
441+
/// and bitcasts.
442+
static Function *getTargetFunction(Value *calledVal) {
443+
SmallPtrSet<const GlobalValue *, 3> Visited;
444+
445+
Constant *c = dyn_cast<Constant>(calledVal);
446+
if (!c) {
447+
return 0;
448+
}
449+
450+
while (true) {
451+
if (GlobalValue *gv = dyn_cast<GlobalValue>(c)) {
452+
if (!Visited.insert(gv).second) {
453+
return 0;
454+
}
455+
456+
if (Function *f = dyn_cast<Function>(gv)) {
457+
return f;
458+
} else if (GlobalAlias *ga = dyn_cast<GlobalAlias>(gv)) {
459+
c = ga->getAliasee();
460+
} else {
461+
return 0;
462+
}
463+
} else if (llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(c)) {
464+
if (ce->getOpcode() == Instruction::BitCast) {
465+
c = ce->getOperand(0);
466+
} else {
467+
return 0;
468+
}
469+
} else {
470+
return 0;
471+
}
472+
}
473+
}
474+
452475
void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, std::vector<ref<Expr>> &arguments) {
453476
Instruction *i = ki->inst;
454477
auto &llvmState = state.llvm;
@@ -679,41 +702,6 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
679702
}
680703
}
681704

682-
/// Compute the true target of a function call, resolving LLVM aliases
683-
/// and bitcasts.
684-
Function *Executor::getTargetFunction(Value *calledVal) {
685-
SmallPtrSet<const GlobalValue *, 3> Visited;
686-
687-
Constant *c = dyn_cast<Constant>(calledVal);
688-
if (!c) {
689-
return 0;
690-
}
691-
692-
while (true) {
693-
if (GlobalValue *gv = dyn_cast<GlobalValue>(c)) {
694-
if (!Visited.insert(gv).second) {
695-
return 0;
696-
}
697-
698-
if (Function *f = dyn_cast<Function>(gv)) {
699-
return f;
700-
} else if (GlobalAlias *ga = dyn_cast<GlobalAlias>(gv)) {
701-
c = ga->getAliasee();
702-
} else {
703-
return 0;
704-
}
705-
} else if (llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(c)) {
706-
if (ce->getOpcode() == Instruction::BitCast) {
707-
c = ce->getOperand(0);
708-
} else {
709-
return 0;
710-
}
711-
} else {
712-
return 0;
713-
}
714-
}
715-
}
716-
717705
void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
718706
*klee::stats::instructions += 1;
719707
auto &llvmState = state.llvm;
@@ -1584,11 +1572,6 @@ void Executor::terminateState(ExecutionState &state) {
15841572
}
15851573
}
15861574

1587-
void Executor::terminateState(ExecutionState &state, const std::string &reason) {
1588-
*klee_warning_stream << "Terminating state: " << reason << "\n";
1589-
terminateState(state);
1590-
}
1591-
15921575
extern "C" {
15931576
typedef uint64_t (*external_fcn_t)(...);
15941577
}

libs2e/src/s2e-kvm-vm.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ int VM::memoryReadWrite(kvm_mem_rw *mem) {
144144

145145
int VM::registerFixedRegion(kvm_fixed_region *region) {
146146
#ifdef CONFIG_SYMBEX_MP
147-
s2e_register_ram2(region->name, region->host_address, region->size, region->flags & KVM_MEM_SHARED_CONCRETE);
147+
s2e_register_ram(region->name, region->host_address, region->size, region->flags & KVM_MEM_SHARED_CONCRETE);
148148
#endif
149149
return 0;
150150
}

libs2ecore/include/s2e/S2EExecutionState.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,8 @@ class S2EExecutionState : public klee::ExecutionState, public klee::IConcretizer
153153
/** Set when execution enters doInterrupt, reset when it exits. */
154154
bool m_runningExceptionEmulationCode;
155155

156+
llvm::SmallVector<klee::ObjectKey, 8> m_saveOnContextSwitch;
157+
156158
virtual void addressSpaceChange(const klee::ObjectKey &key, const klee::ObjectStateConstPtr &oldState,
157159
const klee::ObjectStatePtr &newState);
158160

@@ -195,6 +197,7 @@ class S2EExecutionState : public klee::ExecutionState, public klee::IConcretizer
195197

196198
m_memIoVaddr = state.m_memIoVaddr;
197199
m_runningExceptionEmulationCode = state.m_runningExceptionEmulationCode;
200+
m_saveOnContextSwitch = state.m_saveOnContextSwitch;
198201
}
199202

200203
virtual klee::ExecutionStatePtr clone();
@@ -306,6 +309,10 @@ class S2EExecutionState : public klee::ExecutionState, public klee::IConcretizer
306309
/** Copy concrete values to the execution state storage */
307310
void switchToSymbolic();
308311

312+
void registerRam(uint64_t size, uint64_t hostAddress, bool isSharedConcrete, const char *name);
313+
void saveSharedConcreteMemory();
314+
void restoreSharedConcreteMemory();
315+
309316
bool isForkingEnabled() const {
310317
return !forkDisabled;
311318
}

libs2ecore/include/s2e/S2EExecutor.h

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,6 @@ class S2EExecutor : public klee::Executor {
5959

6060
klee::KFunction *m_dummyMain;
6161

62-
std::vector<klee::ObjectKey> m_saveOnContextSwitch;
63-
6462
bool m_executeAlwaysKlee;
6563

6664
bool m_forkProcTerminateCurrentState;
@@ -104,9 +102,6 @@ class S2EExecutor : public klee::Executor {
104102
void initializeExecution(S2EExecutionState *initialState, bool executeAlwaysKlee);
105103

106104
void registerCpu(S2EExecutionState *initialState, CPUX86State *cpuEnv);
107-
void registerRam(S2EExecutionState *initialState, struct MemoryDesc *region, uint64_t startAddress, uint64_t size,
108-
uint64_t hostAddress, bool isSharedConcrete, bool saveOnContextSwitch = true,
109-
const char *name = "");
110105

111106
void registerSharedExternalObject(S2EExecutionState *state, void *address, unsigned size);
112107

@@ -209,8 +204,6 @@ class S2EExecutor : public klee::Executor {
209204

210205
void doLoadBalancing();
211206

212-
void notifyBranch(klee::ExecutionState &state);
213-
214207
void initializeStateSwitchTimer();
215208
static void stateSwitchTimerCallback(void *opaque);
216209

libs2ecore/include/s2e/s2e_libcpu.h

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -102,10 +102,7 @@ void s2e_initialize_execution(int execute_always_klee);
102102

103103
void s2e_register_cpu(struct CPUX86State *cpu_env);
104104

105-
void s2e_register_ram(struct MemoryDesc *region, uint64_t start_address, uint64_t size, uint64_t host_address,
106-
int is_shared_concrete, int save_on_context_switch, const char *name);
107-
108-
void s2e_register_ram2(const char *name, uint64_t host_address, uint64_t size, int is_shared_concrete);
105+
void s2e_register_ram(const char *name, uint64_t host_address, uint64_t size, int is_shared_concrete);
109106

110107
uintptr_t se_get_host_address(uint64_t paddr);
111108

libs2ecore/src/S2EExecutionState.cpp

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,17 @@ extern llvm::cl::opt<bool> PrintForkingStatus;
5656
extern llvm::cl::opt<bool> VerboseStateDeletion;
5757
extern llvm::cl::opt<bool> DebugConstraints;
5858

59+
// clang-format off
60+
namespace {
61+
// This should be true by default, because otherwise overheads are way too high.
62+
// Drawback is that execution is not fully consistent by default.
63+
llvm::cl::opt<bool>
64+
StateSharedMemory("state-shared-memory",
65+
llvm::cl::desc("Allow unimportant memory regions (like video RAM) to be shared between states"),
66+
llvm::cl::init(true));
67+
}
68+
// clang-format on
69+
5970
namespace s2e {
6071

6172
using namespace klee;
@@ -89,11 +100,29 @@ ExecutionStatePtr S2EExecutionState::clone() {
89100
// This means that we must clean owned-by-us flag in S2E TLB.
90101
assert(m_active);
91102

103+
s2e_kvm_flush_disk();
104+
92105
m_tlb.clearTlbOwnership();
93106
#if defined(SE_ENABLE_PHYSRAM_TLB)
94107
m_tlb.clearRamTlb();
95108
#endif
96109

110+
saveSharedConcreteMemory();
111+
112+
// We must not save the current tb, because this pointer will become
113+
// stale on state restore. If a signal occurs while restoring the state,
114+
// its handler will try to unlink a stale tb, which could cause a hang
115+
// or a crash.
116+
auto old_tb = env->current_tb;
117+
env->current_tb = nullptr;
118+
m_registers.saveConcreteState();
119+
env->current_tb = old_tb;
120+
121+
cpu_disable_ticks();
122+
s2e_kvm_save_device_state();
123+
m_timersState = timers_state;
124+
cpu_enable_ticks();
125+
97126
S2EExecutionState *ret = new S2EExecutionState(*this);
98127

99128
ret->m_stateID = g_s2e->fetchAndIncrementStateId();
@@ -109,6 +138,78 @@ ExecutionStatePtr S2EExecutionState::clone() {
109138
return ret;
110139
}
111140

141+
void S2EExecutionState::registerRam(uint64_t size, uint64_t hostAddress, bool isSharedConcrete, const char *name) {
142+
#ifdef CONFIG_SYMBEX_MP
143+
assert(m_stateID == 0 && "Ram registration must be done in the initial state");
144+
assert((size & ~TARGET_PAGE_MASK) == 0);
145+
assert((hostAddress & ~TARGET_PAGE_MASK) == 0);
146+
147+
g_s2e->getDebugStream() << "Adding memory block (size = " << hexval(size) << ", hostAddr = " << hexval(hostAddress)
148+
<< ", isSharedConcrete=" << isSharedConcrete << ", name=" << name << ")\n";
149+
150+
for (uint64_t addr = hostAddress; addr < hostAddress + size; addr += SE_RAM_OBJECT_SIZE) {
151+
152+
auto os = addExternalObject((void *) addr, SE_RAM_OBJECT_SIZE, false, isSharedConcrete);
153+
154+
os->setMemoryPage(true);
155+
156+
if (!isSharedConcrete) {
157+
os->setSplittable(true);
158+
os->setNotifyOnConcretenessChange(true);
159+
}
160+
161+
#ifdef S2E_DEBUG_MEMOBJECT_NAME
162+
std::stringstream ss;
163+
ss << name << "_" << std::hex << (addr - hostAddress);
164+
mo->setName(ss.str());
165+
#endif
166+
167+
if (isSharedConcrete && !StateSharedMemory) {
168+
m_saveOnContextSwitch.push_back(os->getKey());
169+
}
170+
}
171+
172+
if (!isSharedConcrete) {
173+
// mprotecting does not actually free the RAM, it's still committed,
174+
// we need to explicitely unmap it.
175+
// mprotect((void*) hostAddress, size, PROT_NONE);
176+
if (munmap((void *) hostAddress, size) < 0) {
177+
g_s2e->getWarningsStream(nullptr) << "Could not unmap host RAM\n";
178+
exit(-1);
179+
}
180+
181+
// Make sure that the memory space is reserved and won't be used anymore
182+
// so that there are no conflicts with klee memory objects.
183+
void *newhost = mmap((void *) hostAddress, size, PROT_NONE, MAP_ANONYMOUS | MAP_FIXED | MAP_PRIVATE, 0, 0);
184+
if (newhost == MAP_FAILED || newhost != (void *) hostAddress) {
185+
g_s2e->getWarningsStream(nullptr) << "Could not map host RAM\n";
186+
exit(-1);
187+
}
188+
}
189+
190+
m_asCache.registerPool(hostAddress, size);
191+
#endif
192+
}
193+
194+
void S2EExecutionState::saveSharedConcreteMemory() {
195+
for (auto &mo : m_saveOnContextSwitch) {
196+
auto os = addressSpace().findObject(mo.address);
197+
auto wos = addressSpace().getWriteable(os);
198+
uint8_t *store = wos->getConcreteBuffer();
199+
assert(store);
200+
memcpy(store, (uint8_t *) mo.address, mo.size);
201+
}
202+
}
203+
204+
void S2EExecutionState::restoreSharedConcreteMemory() {
205+
for (auto &mo : m_saveOnContextSwitch) {
206+
auto os = addressSpace().findObject(mo.address);
207+
const uint8_t *store = os->getConcreteBuffer();
208+
assert(store);
209+
memcpy((uint8_t *) mo.address, store, mo.size);
210+
}
211+
}
212+
112213
/***/
113214

114215
void S2EExecutionState::enableForking() {

0 commit comments

Comments
 (0)