diff options
Diffstat (limited to 'backend/Tunneling.v')
-rw-r--r-- | backend/Tunneling.v | 40 |
1 files changed, 13 insertions, 27 deletions
diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 18414a89..bdc8117e 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -64,9 +64,9 @@ Require Import LTL. Module U := UnionFind.UF(PTree). -Definition record_goto (uf: U.t) (pc: node) (i: instruction) : U.t := - match i with - | Lnop s => U.union uf pc s +Definition record_goto (uf: U.t) (pc: node) (b: bblock) : U.t := + match b with + | Lbranch s :: _ => U.union uf pc s | _ => uf end. @@ -77,37 +77,23 @@ Definition record_gotos (f: LTL.function) : U.t := successor [s] of every instruction by the canonical representative of its equivalence class in the union-find data structure. *) -Definition tunnel_instr (uf: U.t) (b: instruction) : instruction := - match b with - | Lnop s => - Lnop (U.repr uf s) - | Lop op args res s => - Lop op args res (U.repr uf s) - | Lload chunk addr args dst s => - Lload chunk addr args dst (U.repr uf s) - | Lstore chunk addr args src s => - Lstore chunk addr args src (U.repr uf s) - | Lcall sig ros args res s => - Lcall sig ros args res (U.repr uf s) - | Ltailcall sig ros args => - Ltailcall sig ros args - | Lbuiltin ef args res s => - Lbuiltin ef args res (U.repr uf s) - | Lcond cond args s1 s2 => - Lcond cond args (U.repr uf s1) (U.repr uf s2) - | Ljumptable arg tbl => - Ljumptable arg (List.map (U.repr uf) tbl) - | Lreturn or => - Lreturn or +Definition tunnel_instr (uf: U.t) (i: instruction) : instruction := + match i with + | Lbranch s => Lbranch (U.repr uf s) + | Lcond cond args s1 s2 => Lcond cond args (U.repr uf s1) (U.repr uf s2) + | Ljumptable arg tbl => Ljumptable arg (List.map (U.repr uf) tbl) + | _ => i end. +Definition tunnel_block (uf: U.t) (b: bblock) : bblock := + List.map (tunnel_instr uf) b. + Definition tunnel_function (f: LTL.function) : LTL.function := let uf := record_gotos f in mkfunction (fn_sig f) - (fn_params f) (fn_stacksize f) - (PTree.map (fun pc b => tunnel_instr uf b) (fn_code f)) + (PTree.map1 (tunnel_block uf) (fn_code f)) (U.repr uf (fn_entrypoint f)). Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef := |