Assign default concrete values to symbolic values when calling s2e_make_symbolic in concolic mode

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Fixed s2e_assume()

In concolic mode, directly assign values to check if the expression is true.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Properly check whether a concrete address is inbound, given the access size.

The access size was disregarded before. Although this seemed fine for 4K pages,
it may not be true anymore with smaller subpages (e.g., 128 bytes).
An access can span two subpages.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>

Conflicts:

	klee/lib/Core/AddressSpace.cpp
Fork at page level instead of byte level.

Allows to keep the address symbolic and avoid too much path explosion.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>

Conflicts:

	klee/lib/Core/Executor.cpp
Don't evaluate expressions in the solver in concolic mode.

The solver must not be coupled with the concolic stuff.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>

Conflicts:

	klee/lib/Core/TimingSolver.cpp
klee_get_value() should concretize the value.

Turns out that it didn't, which may cause problems in
some parts of softmmu. Maybe that's not how it was meant to
work in the original KLEE, but for S2E, we don't care.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Tweaked toConstant, toConstantSilent, toUnique for concolic execution.

They should use the assignment map instead of calling the constraint solver.
Otherwise, calling them would lead to possibly inconsistent values, e.g., if
the solver disagrees with the assignment map, and the returned value is used
later to build a constraint.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Disable special function handlers that have no use in S2E

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Made fork-on-symbolic-address the default option.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
use-fast-helpers and !fork-on-symbolic-address is unsupported for now

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Don't build textual expression if it's not going to be printed

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Compilation fix

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Don't call symbolic mmio checks if there is no symbolic hardware.

Avoids concretizing memory addresses.
This is a quick workaround anyway, something deeper will have to be
done once we get back to symbolic hardware.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>

Conflicts:

	qemu/s2e/Plugins/CorePlugin.cpp
	qemu/softmmu_template.h
Mark with assert(false) all the stuff that is not supposed to happen in S2E while in concolic mode.

A quick review shows that this KLEE stuff will never be called when running in S2E,
but we never know...

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
g_s2e_enable_mmio_checks should be registered as external variable.

Forgot to do it in commit 4fe2b7a0de

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>

Conflicts:

	qemu/s2e/S2EExecutor.cpp
Optimized access to always-concrete memory

Don't waste time creating a string if the written value / address are concrete.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Concolic execution with DFS is now the default setting for S2E

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Set a 16MB stack for QEMU threads. Avoids most stack overflows in the constraint solver.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
Disable counter-example cache for now. Seems to cause crashes in concolic mode.

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>
s2e_assume for S2E BIOS

Signed-off-by: Vitaly Chipounov <vitaly.chipounov@epfl.ch>