Skip to content

Commit ea2f03d

Browse files
authored
Fixes handling of let-bound variables in flatten pass (#1359)
* Update LLVM backend to work with version 12 This may also work with later versions, but I did not test them * Fixes handling of let-bound variables in flatten pass 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. * Fix capture-avoiding substitution * Runs `make indent`
1 parent 5f7d744 commit ea2f03d

File tree

2 files changed

+24
-14
lines changed

2 files changed

+24
-14
lines changed

plugins/flatten/.merlin

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,3 @@
1-
PKG core_kernel
2-
PKG bap
3-
PKG ocamlgraph
1+
REC
42

5-
B _build
6-
FLG -short-paths
7-
FLG -w -4-33-40-41-42-43-34-44
3+
B ../../_build

plugins/flatten/flatten_main.ml

Lines changed: 22 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,26 @@
11
open Bap.Std
22
open Core_kernel
3-
include Self()
43

4+
include Self()
55

66
let get_direct_typ (e : exp) : Type.t = match e with
77
| Bil.Var v -> Var.typ v
88
| Bil.Unknown (_,t) -> t
99
| Bil.Int w -> Type.Imm (Word.bitwidth w)
1010
| _ -> failwith "the expression is not flattened"
1111

12+
class substituter (x : var) (x' : var) = object
13+
inherit Exp.mapper as super
14+
15+
method! map_var v =
16+
if Var.equal x v then Var x' else super#map_var v
17+
18+
method! map_let v ~exp ~body =
19+
let exp = super#map_exp exp in
20+
let body = if Var.equal x v then body else super#map_exp body in
21+
Let (v, exp, body)
22+
end
23+
1224
let flatten_exp (exp : exp) (blk : blk term) (before : tid) : exp * blk term =
1325
let is_virtual = true in
1426
let fresh = true in
@@ -61,13 +73,15 @@ let flatten_exp (exp : exp) (blk : blk term) (before : tid) : exp * blk term =
6173
Term.prepend def_t ~before blk def
6274
| Bil.Let (v, x, y) ->
6375
let x, blk = aux x blk in
64-
let y, blk = aux y blk in
65-
let vtype = Var.typ v in
66-
let var = Var.create ~is_virtual ~fresh "flt" vtype in
67-
let e = Bil.Let (v, x, y) in
68-
let def = Def.create var e in
69-
Bil.Var var,
70-
Term.prepend def_t ~before blk def
76+
let var, blk = match x with
77+
| Var v -> v, blk
78+
| _ ->
79+
let vtype = Var.typ v in
80+
let var = Var.create ~is_virtual ~fresh "flt" vtype in
81+
let def = Def.create var x in
82+
var, Term.prepend def_t ~before blk def in
83+
let y = (new substituter v var)#map_exp y in
84+
aux y blk
7185
| Bil.Unknown (_, _) -> exp, blk
7286
| Bil.Ite (x, y, z) ->
7387
let x, blk = aux x blk in

0 commit comments

Comments
 (0)