represents rep prefix with the while statement in x86 #998
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The old representation inherited from BAP 0.x was representing
`repz<code>` as
```
if (RCX = 0) jmp next;
<code>;
RCX := RCX - 1;
if (RCX = 0)
jmp next;
if (ZF)
jmp start;
```
where `next` and `start` were concrete addresses of the current and
the next instructions. It goes without saying that such code
has a very bloated graph representation.
A more tight representation, which could also be nicecly reified into
a graph could be produced using BIL's `while` statement, which is
reflected to the Core Theory `repeat` term. The same instruction will
now have the following representation:
```
$0 := true;
while (RCX <> 0 & $0) {
<code>;
RCX := RCX - 1;
$0 := ZF;
}
```
which is reified into the following IR:
```
entry:
#0 := 1
goto tail
body:
<code>
RCX := RCX - 1
#0 := ZF
goto tail
tail:
when RCX <> 0 & #0 goto body
```
Which is much smaller than the original IR.
Another nice property of the new representation is that it doesn't
contain any absolute jumps therefore is rellocatable. Additionally, it
is no longer classified as jump or barrier and is a pure data effect.
Caveats
-------
So far the IR translation layer for some reason produces slightly less
optimal representation, namely
```
entry:
#0 := 1
goto bogus;
body:
<code>
RCX := RCX - 1
#0 := ZF
goto tail
bogus:
goto tail
tail:
when RCX <> 0 & #0 goto body
```
I will try to remove the `bogus: goto tail` block if possible,
otherwise we will let it for the later times, when we will have more
time.
gitoleg
approved these changes
Oct 15, 2019
gitoleg
added a commit
to gitoleg/bap
that referenced
this pull request
Oct 22, 2019
The problem After BinaryAnalysisPlatform#998, string instructions with the rep prefix are represented with the `Bil.while` statement and have the semantics of a pure data effect (and therefore do not break a basic block). However, when we reify while into IR we still have jump terms. And this wasn't anticipated by the sema lifter, which was glueing IR constituting one basic block, assuming that there will not be any complex control flow. This PR fixes this issue (which is not only specific to BinaryAnalysisPlatform#998, this PR just triggered it, in general there could be other cases, when pure data effects are reified into non-simple control structures, cf. conditional moves). Solution Instead of just appending blocks, ensure that they are connected by an explicit jump.
ivg
pushed a commit
that referenced
this pull request
Oct 23, 2019
The problem After #998, string instructions with the rep prefix are represented with the `Bil.while` statement and have the semantics of a pure data effect (and therefore do not break a basic block). However, when we reify while into IR we still have jump terms. And this wasn't anticipated by the sema lifter, which was glueing IR constituting one basic block, assuming that there will not be any complex control flow. This PR fixes this issue (which is not only specific to #998, this PR just triggered it, in general there could be other cases, when pure data effects are reified into non-simple control structures, cf. conditional moves). Solution Instead of just appending blocks, ensure that they are connected by an explicit jump.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 old representation inherited from BAP 0.x was representing
repz<code>aswhere
nextandstartwere concrete addresses of the current andthe next instructions. It goes without saying that such code
has a very bloated graph representation.
A more tight representation, which could also be nicecly reified into
a graph could be produced using BIL's
whilestatement, which isreflected to the Core Theory
repeatterm. The same instruction willnow have the following representation:
which is reified into the following IR:
Which is much smaller than the original IR.
Another nice property of the new representation is that it doesn't
contain any absolute jumps therefore is rellocatable. Additionally, it
is no longer classified as jump or barrier and is a pure data effect.
Caveats
We still have a small suboptimality in the form of a bogus
head: goto tailblock, which comes from the how we represent graphs in our denotational semantics. This block could be removed with a simple optimization pass after an instruction is lifted, but I don't think it is worthwhile to do it right now, given how scarce such kind of instructions could be.