You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: