extracted/rTLToERTL.ml

   1 open Preamble
   2
   3 open Order
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open ErrorMessages
  12
  13 open PreIdentifiers
  14
  15 open Errors
  16
  17 open Extralib
  18
  19 open Lists
  20
  21 open Positive
  22
  23 open Identifiers
  24
  25 open Registers
  26
  27 open Exp
  28
  29 open Setoids
  30
  31 open Monad
  32
  33 open Option
  34
  35 open Extranat
  36
  37 open Vector
  38
  39 open Div_and_mod
  40
  41 open Russell
  42
  43 open Types
  44
  45 open List
  46
  47 open Util
  48
  49 open FoldStuff
  50
  51 open BitVector
  52
  53 open Arithmetic
  54
  55 open Jmeq
  56
  57 open Bool
  58
  59 open Hints_declaration
  60
  61 open Core_notation
  62
  63 open Pts
  64
  65 open Logic
  66
  67 open Relations
  68
  69 open Nat
  70
  71 open I8051
  72
  73 open RegisterSet
  74
  75 open Extra_bool
  76
  77 open Coqlib
  78
  79 open Values
  80
  81 open FrontEndVal
  82
  83 open GenMem
  84
  85 open FrontEndMem
  86
  87 open Globalenvs
  88
  89 open String
  90
  91 open Sets
  92
  93 open Listb
  94
  95 open LabelledObjects
  96
  97 open BitVectorTrie
  98
  99 open Graphs
 100
 101 open CostLabel
 102
 103 open Hide
 104
 105 open Integers
 106
 107 open AST
 108
 109 open Division
 110
 111 open Z
 112
 113 open BitVectorZ
 114
 115 open Pointers
 116
 117 open ByteValues
 118
 119 open BackEndOps
 120
 121 open Joint
 122
 123 open RTL
 124
 125 open ERTL
 126
 127 open Deqsets_extra
 128
 129 open State
 130
 131 open Bind_new
 132
 133 open BindLists
 134
 135 open Blocks
 136
 137 open TranslateUtils
 138
 139 (** val save_hdws :
 140     AST.ident List.list -> (Registers.register, I8051.register) Types.prod
 141     List.list -> Joint.joint_seq List.list **)
 142 let save_hdws globals =
 143   let save_hdws_internal = fun destr_srcr -> Joint.MOVE
 144     (Obj.magic { Types.fst = (ERTL.PSD destr_srcr.Types.fst); Types.snd =
 145       (ERTL.move_src_from_dst (ERTL.HDW destr_srcr.Types.snd)) })
 146   in
 147   List.map save_hdws_internal
 148
 149 (** val restore_hdws :
 150     AST.ident List.list -> (Joint.psd_argument, I8051.register) Types.prod
 151     List.list -> Joint.joint_seq List.list **)
 152 let restore_hdws globals =
 153   let restore_hdws_internal = fun destr_srcr -> Joint.MOVE
 154     (Obj.magic { Types.fst = (ERTL.HDW destr_srcr.Types.snd); Types.snd =
 155       (ERTL.psd_argument_move_src destr_srcr.Types.fst) })
 156   in
 157   List.map restore_hdws_internal
 158
 159 (** val get_params_hdw :
 160     AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
 161     List.list **)
 162 let get_params_hdw globals params =
 163   save_hdws globals (Util.zip_pottier params I8051.registerParams)
 164
 165 (** val get_param_stack :
 166     AST.ident List.list -> Registers.register -> Registers.register ->
 167     Registers.register -> Joint.joint_seq List.list **)
 168 let get_param_stack globals addr1 addr2 destr =
 169   List.Cons ((Joint.LOAD ((Obj.magic destr),
 170     (Obj.magic (Joint.psd_argument_from_reg addr1)),
 171     (Obj.magic (Joint.psd_argument_from_reg addr2)))), (List.Cons ((Joint.OP2
 172     (BackEndOps.Add, (Obj.magic addr1),
 173     (Obj.magic (Joint.psd_argument_from_reg addr1)),
 174     (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
 175     (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
 176     (Obj.magic (Joint.psd_argument_from_reg addr2)),
 177     (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
 178     List.Nil)))))
 179
 180 (** val get_params_stack :
 181     AST.ident List.list -> Registers.register -> Registers.register ->
 182     Registers.register -> Registers.register List.list -> Joint.joint_seq
 183     List.list **)
 184 let get_params_stack globals tmpr addr1 addr2 params =
 185   let params_length_byte =
 186     Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 187       (Nat.S (Nat.S Nat.O)))))))) (List.length params)
 188   in
 189   List.append (List.Cons
 190     ((let x =
 191         ERTL.ertl_seq_joint globals (Obj.magic (ERTL.Ertl_frame_size tmpr))
 192       in
 193      x), (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
 194     (BackEndOps.Sub, (Obj.magic tmpr),
 195     (Obj.magic (Joint.psd_argument_from_reg tmpr)),
 196     (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
 197     (List.Cons ((Joint.MOVE
 198     (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
 199       (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })), (List.Cons
 200     ((Joint.MOVE
 201     (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
 202       (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })), (List.Cons
 203     ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
 204     (Obj.magic (Joint.psd_argument_from_reg addr1)),
 205     (Obj.magic (Joint.psd_argument_from_reg tmpr)))), (List.Cons ((Joint.OP2
 206     (BackEndOps.Addc, (Obj.magic addr2),
 207     (Obj.magic (Joint.psd_argument_from_reg addr2)),
 208     (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
 209     List.Nil))))))))))))))
 210     (List.flatten (List.map (get_param_stack globals addr1 addr2) params))
 211
 212 (** val get_params :
 213     AST.ident List.list -> Registers.register -> Registers.register ->
 214     Registers.register -> Registers.register List.list -> Joint.joint_seq
 215     List.list **)
 216 let get_params globals tmpr addr1 addr2 params =
 217   let n = Nat.min (List.length params) (List.length I8051.registerParams) in
 218   let { Types.fst = hdw_params; Types.snd = stack_params } =
 219     Util.list_split n params
 220   in
 221   List.append (get_params_hdw globals hdw_params)
 222     (get_params_stack globals tmpr addr1 addr2 stack_params)
 223
 224 (** val save_return :
 225     AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
 226     List.list **)
 227 let save_return globals ret_regs =
 228   let crl = Util.reduce_strong I8051.registerSTS ret_regs in
 229   let commonl = crl.Types.fst.Types.fst in
 230   let commonr = crl.Types.snd.Types.fst in
 231   let restl = crl.Types.fst.Types.snd in
 232   List.append
 233     (Util.map2 (fun st r -> Joint.MOVE
 234       (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
 235         (ERTL.psd_argument_move_src r) })) commonl commonr)
 236     (List.map (fun st -> Joint.MOVE
 237       (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
 238         (ERTL.byte_to_ertl_snd_argument__o__psd_argument_to_move_src
 239           Joint.zero_byte) })) restl)
 240
 241 (** val assign_result : AST.ident List.list -> Joint.joint_seq List.list **)
 242 let assign_result globals =
 243   let crl = Util.reduce_strong I8051.registerRets I8051.registerSTS in
 244   let commonl = crl.Types.fst.Types.fst in
 245   let commonr = crl.Types.snd.Types.fst in
 246   Util.map2 (fun ret st -> Joint.MOVE
 247     (Obj.magic { Types.fst = (ERTL.HDW ret); Types.snd =
 248       (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl commonr
 249
 250 (** val epilogue :
 251     AST.ident List.list -> Registers.register List.list -> Registers.register
 252     -> Registers.register -> (Registers.register, I8051.register) Types.prod
 253     List.list -> Joint.joint_seq List.list Types.sig0 **)
 254 let epilogue globals ret_regs sral srah sregs =
 255   List.append
 256     (save_return globals (List.map (fun x -> Joint.Reg x) ret_regs))
 257     (List.append
 258       (restore_hdws globals
 259         (List.map (fun pr -> { Types.fst = (Joint.Reg pr.Types.fst);
 260           Types.snd = pr.Types.snd }) sregs))
 261       (List.append (List.Cons ((Joint.PUSH
 262         (Obj.magic (Joint.psd_argument_from_reg sral))), (List.Cons
 263         ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg srah))),
 264         (List.Cons
 265         ((ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_del_frame)),
 266         List.Nil)))))) (assign_result globals)))
 267
 268 (** val prologue :
 269     AST.ident List.list -> Registers.register List.list -> Registers.register
 270     -> Registers.register -> Registers.register -> Registers.register ->
 271     Registers.register -> (Registers.register, I8051.register) Types.prod
 272     List.list -> (Registers.register, Joint.joint_seq List.list)
 273     Bind_new.bind_new **)
 274 let prologue globals params sral srah tmpr addr1 addr2 sregs =
 275   let l =
 276     List.append (List.Cons
 277       ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame)
 278         in
 279        x), (List.Cons ((Joint.POP (Obj.magic srah)), (List.Cons ((Joint.POP
 280       (Obj.magic sral)), List.Nil))))))
 281       (List.append (save_hdws globals sregs)
 282         (get_params globals tmpr addr1 addr2 params))
 283   in
 284   Bind_new.Bret l
 285
 286 (** val set_params_hdw :
 287     AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
 288     List.list **)
 289 let set_params_hdw globals params =
 290   restore_hdws globals (Util.zip_pottier params I8051.registerParams)
 291
 292 (** val set_param_stack :
 293     AST.ident List.list -> Registers.register -> Registers.register ->
 294     Joint.psd_argument -> Joint.joint_seq List.list **)
 295 let set_param_stack globals addr1 addr2 arg =
 296   List.Cons ((Joint.STORE ((Obj.magic (Joint.psd_argument_from_reg addr1)),
 297     (Obj.magic (Joint.psd_argument_from_reg addr2)), (Obj.magic arg))),
 298     (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
 299     (Obj.magic (Joint.psd_argument_from_reg addr1)),
 300     (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
 301     (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
 302     (Obj.magic (Joint.psd_argument_from_reg addr2)),
 303     (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
 304     List.Nil)))))
 305
 306 (** val set_params_stack :
 307     AST.ident List.list -> Joint.psd_argument List.list ->
 308     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
 309 let set_params_stack globals params =
 310   Bind_new.Bnew (fun addr1 -> Bind_new.Bnew (fun addr2 ->
 311     let params_length_byte =
 312       Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 313         (Nat.S (Nat.S Nat.O)))))))) (List.length params)
 314     in
 315     let l =
 316       List.append (List.Cons ((Joint.MOVE
 317         (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
 318           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
 319         (List.Cons ((Joint.MOVE
 320         (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
 321           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
 322         (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
 323         (BackEndOps.Sub, (Obj.magic addr1),
 324         (Obj.magic (Joint.psd_argument_from_reg addr1)),
 325         (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
 326         (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic addr2),
 327         (Obj.magic (Joint.psd_argument_from_reg addr2)),
 328         (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
 329         List.Nil))))))))))
 330         (List.flatten
 331           (List.map (set_param_stack globals addr1 addr2) params))
 332     in
 333     Bind_new.Bret l))
 334
 335 (** val set_params :
 336     AST.ident List.list -> Joint.psd_argument List.list ->
 337     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
 338     Types.sig0 **)
 339 let set_params globals params =
 340   let n = Nat.min (List.length params) (List.length I8051.registerParams) in
 341   let hdw_stack_params = List.split params n in
 342   let hdw_params = hdw_stack_params.Types.fst in
 343   let stack_params = hdw_stack_params.Types.snd in
 344   BindLists.bappend
 345     (let l = set_params_hdw globals hdw_params in Bind_new.Bret l)
 346     (set_params_stack globals stack_params)
 347
 348 (** val fetch_result :
 349     AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
 350     List.list Types.sig0 **)
 351 let fetch_result globals ret_regs =
 352   (let crl = Util.reduce_strong I8051.registerSTS I8051.registerRets in
 353     (fun _ ->
 354     let commonl = crl.Types.fst.Types.fst in
 355     let commonr = crl.Types.snd.Types.fst in
 356     List.append
 357       (Util.map2 (fun st r -> Joint.MOVE
 358         (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
 359           (ERTL.move_src_from_dst (ERTL.HDW r)) })) commonl commonr)
 360       (let crl0 = Util.reduce_strong ret_regs I8051.registerSTS in
 361       let commonl0 = crl0.Types.fst.Types.fst in
 362       let commonr0 = crl0.Types.snd.Types.fst in
 363       Util.map2 (fun ret st -> Joint.MOVE
 364         (Obj.magic { Types.fst = (ERTL.PSD ret); Types.snd =
 365           (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl0 commonr0))) __
 366
 367 (** val translate_step :
 368     AST.ident List.list -> Graphs.label -> Joint.joint_step ->
 369     Blocks.bind_step_block **)
 370 let translate_step globals x = function
 371 | Joint.COST_LABEL lbl ->
 372   Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
 373     Joint.COST_LABEL lbl) }; Types.snd = List.Nil }
 374 | Joint.CALL (f, args, ret_regs) ->
 375   Obj.magic
 376     (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
 377       (Types.pi1 (Obj.magic (set_params globals (Obj.magic args))))
 378       (fun pref ->
 379       Obj.magic (Bind_new.Bret { Types.fst = { Types.fst =
 380         (Blocks.add_dummy_variance pref); Types.snd = (fun x0 -> Joint.CALL
 381         (f, (Obj.magic (List.length (Obj.magic args))),
 382         (Obj.magic Types.It))) }; Types.snd =
 383         (Types.pi1 (fetch_result globals (Obj.magic ret_regs))) })))
 384 | Joint.COND (r, ltrue) ->
 385   Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
 386     Joint.COND (r, ltrue)) }; Types.snd = List.Nil }
 387 | Joint.Step_seq s0 ->
 388   Bind_new.Bret
 389     (match s0 with
 390      | Joint.COMMENT msg ->
 391        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 392          globals (List.Cons ((Joint.COMMENT msg), List.Nil))
 393      | Joint.MOVE rs ->
 394        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 395          globals (List.Cons ((Joint.MOVE
 396          (Obj.magic { Types.fst = (ERTL.PSD (Obj.magic rs).Types.fst);
 397            Types.snd =
 398            (ERTL.psd_argument_move_src (Obj.magic rs).Types.snd) })),
 399          List.Nil))
 400      | Joint.POP x0 ->
 401        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 402          globals List.Nil
 403      | Joint.PUSH x0 ->
 404        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 405          globals List.Nil
 406      | Joint.ADDRESS (x0, off, r1, r2) ->
 407        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 408          globals (List.Cons ((Joint.ADDRESS (x0, off, r1, r2)), List.Nil))
 409      | Joint.OPACCS (op, destr1, destr2, srcr1, srcr2) ->
 410        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 411          globals (List.Cons ((Joint.OPACCS (op, destr1, destr2, srcr1,
 412          srcr2)), List.Nil))
 413      | Joint.OP1 (op1, destr, srcr) ->
 414        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 415          globals (List.Cons ((Joint.OP1 (op1, destr, srcr)), List.Nil))
 416      | Joint.OP2 (op2, destr, srcr1, srcr2) ->
 417        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 418          globals (List.Cons ((Joint.OP2 (op2, destr, srcr1, srcr2)),
 419          List.Nil))
 420      | Joint.CLEAR_CARRY ->
 421        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 422          globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
 423      | Joint.SET_CARRY ->
 424        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 425          globals (List.Cons (Joint.SET_CARRY, List.Nil))
 426      | Joint.LOAD (destr, addr1, addr2) ->
 427        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 428          globals (List.Cons ((Joint.LOAD (destr, addr1, addr2)), List.Nil))
 429      | Joint.STORE (addr1, addr2, srcr) ->
 430        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 431          globals (List.Cons ((Joint.STORE (addr1, addr2, srcr)), List.Nil))
 432      | Joint.Extension_seq ext ->
 433        let RTL.Rtl_stack_address (addr1, addr2) = Obj.magic ext in
 434        Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
 435          globals (List.Cons ((Joint.MOVE
 436          (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
 437            (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
 438          (List.Cons ((Joint.MOVE
 439          (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
 440            (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
 441          List.Nil)))))
 442
 443 (** val translate_fin_step :
 444     AST.ident List.list -> Registers.register List.list -> Registers.register
 445     -> Registers.register -> (Registers.register, I8051.register) Types.prod
 446     List.list -> Graphs.label -> Joint.joint_fin_step ->
 447     Blocks.bind_fin_block **)
 448 let translate_fin_step globals ret_regs ral rah to_restore x = function
 449 | Joint.GOTO lbl' ->
 450   Bind_new.Bret { Types.fst = List.Nil; Types.snd = (Joint.GOTO lbl') }
 451 | Joint.RETURN ->
 452   Bind_new.Bret { Types.fst =
 453     (Types.pi1 (epilogue globals ret_regs ral rah to_restore)); Types.snd =
 454     Joint.RETURN }
 455 | Joint.TAILCALL (x0, x1) -> assert false (* absurd case *)
 456
 457 (** val allocate_regs :
 458     ((Registers.register, I8051.register) Types.prod List.list ->
 459     (Registers.register, 'a1) Bind_new.bind_new) -> (Registers.register, 'a1)
 460     Bind_new.bind_new **)
 461 let allocate_regs f =
 462   let allocate_regs_internal = fun acc r ->
 463     Monad.m_bind0 (Monad.max_def Bind_new.bindNew) acc (fun tl ->
 464       Obj.magic (Bind_new.Bnew (fun r' ->
 465         Obj.magic
 466           (Monad.m_return0 (Monad.max_def Bind_new.bindNew) (List.Cons
 467             ({ Types.fst = r'; Types.snd = r }, tl))))))
 468   in
 469   Obj.magic
 470     (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
 471       (Util.foldl allocate_regs_internal
 472         (Monad.m_return0 (Monad.max_def Bind_new.bindNew) List.Nil)
 473         I8051.registerCalleeSaved) (fun to_save -> Obj.magic f to_save))
 474
 475 (** val translate_data :
 476     AST.ident List.list -> Joint.joint_closed_internal_function ->
 477     TranslateUtils.bound_b_graph_translate_data **)
 478 let translate_data globals def =
 479   let params = (Types.pi1 def).Joint.joint_if_params in
 480   let new_stacksize =
 481     Nat.plus (Types.pi1 def).Joint.joint_if_stacksize
 482       (Nat.minus (List.length (Obj.magic params))
 483         (List.length I8051.registerParams))
 484   in
 485   allocate_regs (fun to_save -> Bind_new.Bnew (fun ral -> Bind_new.Bnew
 486     (fun rah -> Bind_new.Bnew (fun tmpr -> Bind_new.Bnew (fun addr1 ->
 487     Bind_new.Bnew (fun addr2 ->
 488     Obj.magic
 489       (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
 490         (Obj.magic
 491           (prologue globals (Obj.magic params) ral rah tmpr addr1 addr2
 492             to_save)) (fun prologue0 ->
 493         Monad.m_return0 (Monad.max_def Bind_new.bindNew)
 494           { TranslateUtils.init_ret = (Obj.magic Types.It);
 495           TranslateUtils.init_params =
 496           (Obj.magic (List.length (Obj.magic params)));
 497           TranslateUtils.init_stack_size = new_stacksize;
 498           TranslateUtils.added_prologue = prologue0;
 499           TranslateUtils.new_regs =
 500           (List.reverse (List.Cons (addr2, (List.Cons (addr1, (List.Cons
 501             (tmpr, (List.Cons (rah, (List.Cons (ral,
 502             (List.map (fun x -> x.Types.fst) to_save))))))))))));
 503           TranslateUtils.f_step = (translate_step globals);
 504           TranslateUtils.f_fin =
 505           (translate_fin_step globals
 506             (Obj.magic (Types.pi1 def).Joint.joint_if_result) ral rah
 507             to_save) }))))))))
 508
 509 (** val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program **)
 510 let rtl_to_ertl =
 511   TranslateUtils.b_graph_transform_program RTL.rTL ERTL.eRTL translate_data
 512