BinaryAnalysisPlatform / bap

Binary Analysis Platform
MIT License
2.07k stars 273 forks source link

Fixes handling of let-bound variables in flatten pass #1359

Closed bmourad01 closed 3 years ago

bmourad01 commented 3 years ago

The pass was incorrectly handling lexically-scoped variables introduced by "let" expressions.

For example, the following code:

00000015: PF :=
          ~low:1[let $1 = RSP >> 4 ^ RSP in
                 let $2 = $1 >> 2 ^ $1 in $2 >> 1 ^ $2]

Was transformed to:

00005ebd: #11 := RSP >> 4
00005ebe: #12 := #11 ^ RSP
00005ebf: #13 := $1 >> 2
00005ec0: #14 := #13 ^ $1
00005ec1: #15 := $2 >> 1
00005ec2: #16 := #15 ^ $2
00005ec3: #17 := let $2 = #14 in #16
00005ec4: #18 := let $1 = #12 in #17
00005ec5: #19 := low:1[#18]
00005ec6: #20 := ~#19
00000015: PF := #20

Notice how the terms at 00005ebf and so on contain lexically-scoped variables which are not bound to any expression. This commit fixes that behavior to the following:

00005ebd: #11 := RSP >> 4
00005ebe: #12 := #11 ^ RSP
00005ebf: #13 := #12 >> 2
00005ec0: #14 := #13 ^ #12
00005ec1: #15 := #14 >> 1
00005ec2: #16 := #15 ^ #14
00005ec3: #17 := low:1[#16]
00005ec4: #18 := ~#17
00000015: PF := #18

So, the pass seems better off discarding the "let" entirely.

ivg commented 3 years ago

Sorry for missing your PRs! Please, do not hesitate to poke me on Gitter if I am not reacting to the PR in the first day. I am having too many communications from Github so I miss them quite often.

The code looks good, but could you please reindent it. Simple make indent will do the work.

And thanks for the fix!