Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The semantics of eval-cond and jumping observations is corrected. The conditional expression of the
eval-cond
observation now takes into account preceding guard conditions, which fixes wrong path constraints created by the symbolic executor as well as simplifies the symbolic executor code (which no longer requires the analysis of which branch is taken and which is not).The conditional expression of the
jumping
expression, which is still always true, is now computed from all path constraints of the outcoming edges of the basic block, which simplifies taint analysis.Finally, we implement the
on-cond
Lisp signal in terms of thejumping
observation. And while it sounds bad, as we broke the one-to-one correspondence between observation name and signal name, it restores the previous semantics of theon-cond
signal and makes it safe to use it in the Lisp code. It is very tempting though, to try to implement a safeon-cond
signal with 2.1.0 semantics, which will enable tracking conditional expressions that happen in Lisp code and primitives and improve analysis precision. But it may require a substantial amount of work so at the end we may decide to remove theon-cond
signal at all.Addresses #1124