Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tweak jumping and eval cond #1142

Merged
merged 4 commits into from
Jun 23, 2020

Conversation

ivg
Copy link
Member

@ivg ivg commented Jun 19, 2020

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 the jumping 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 the on-cond signal and makes it safe to use it in the Lisp code. It is very tempting though, to try to implement a safe on-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 the on-cond signal at all.

Addresses #1124

ivg added 2 commits June 19, 2020 18:05
Now the guard condition is computed from all outcoming edges, which
simplifies taint analysis and symbolic execution. This is true for
both jumping and eval-cond.
now, when eval-cond takes into account path constraint (i.e., that
previous branches in the same basic block were not taken) we can
simplify the code of the symbolic executor that is responsible for
executing physical (i.e., represented with actual basic blocks)
braches as we now have to investigate only non-taken branches.
@ivg ivg requested a review from gitoleg June 19, 2020 22:32
@ivg ivg self-assigned this Jun 19, 2020
@ivg ivg force-pushed the tweak-jumping-and-eval-cond branch from 0f19da4 to 4308304 Compare June 22, 2020 13:27
We might put it back before the release, but right now it is the
easiest and less error-prone solution.
@ivg ivg force-pushed the tweak-jumping-and-eval-cond branch from 4308304 to a1c4ce8 Compare June 22, 2020 17:38
Since functional tests take five times more time on the Mac OS X
machines, it is not surprising that we are occasionally hitting the
timeout on them, see also BinaryAnalysisPlatform#1136. I hope that double would be enough.
@ivg ivg merged commit 582e9e4 into BinaryAnalysisPlatform:master Jun 23, 2020
@ivg ivg deleted the tweak-jumping-and-eval-cond branch March 9, 2022 17:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant