Currently, during exploration (scanning phase) we handle constraints coming from branches as hard path constraints. Which means we only take 1 branch path if two concrete values are compared, or if there are conflicting constraints in the state. For example:
Two concrete values:
x = 1
if (x == 0) {
# never explored, but it can be mispredicted
}
Conflicting constraints:
x = symbolic()
if (x > 10) {
}
if (x < 5) {
}
# both branches are never both taken, but it speculative execution this is possible.
However, in speculative execution this behavior is possible. Preferable we add this as an optional feature which can be enabled/disabled via the config.
Note that in the common case (compare of a symbolic value) we do currently explore both paths.
Currently, during exploration (scanning phase) we handle constraints coming from branches as hard path constraints. Which means we only take 1 branch path if two concrete values are compared, or if there are conflicting constraints in the state. For example:
Two concrete values:
Conflicting constraints:
However, in speculative execution this behavior is possible. Preferable we add this as an optional feature which can be enabled/disabled via the config.
Note that in the common case (compare of a symbolic value) we do currently explore both paths.