Changeset 2806 for src/RTL/RTLToERTL.ma


Ignore:
Timestamp:
Mar 7, 2013, 2:51:40 PM (8 years ago)
Author:
tranquil
Message:

new b_graph_translate obligations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r2689 r2806  
    3737
    3838definition get_params_stack :
    39   ∀globals.list register →
    40   bind_new register (list (joint_seq ERTL globals)) ≝
    41   λglobals,params.
    42   νtmpr,addr1,addr2 in
     39  ∀globals.register → register → register → list register →
     40  list (joint_seq ERTL globals) ≝
     41  λglobals.
     42  λtmpr,addr1,addr2,params.
    4343  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
    4444  [ (ertl_frame_size tmpr : joint_seq ??) ;
     
    5252
    5353definition get_params ≝
    54   λglobals,params.
     54  λglobals,tmpr,addr1,addr2,params.
    5555  let n ≝ min (length … params) (length … RegisterParams) in
    5656  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
    57   get_params_hdw globals hdw_params @@ get_params_stack … stack_params.
     57  get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params.
    5858
    5959definition save_return :
     
    130130
    131131definition prologue :
    132   ∀globals.list register → register → register → list (register×Register) →
     132  ∀globals.list register → register → register → register → register → register →
     133  list (register×Register) →
    133134  bind_new register (list (joint_seq ERTL globals)) ≝
    134   λglobals,params,sral,srah,sregs.
     135  λglobals,params,sral,srah,tmpr,addr1,addr2,sregs.
    135136  [ (ertl_new_frame : joint_seq ??) ;
    136137    POP … sral ;
    137138    POP … srah
    138   ] @@ save_hdws … sregs @@ get_params … params.
     139  ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params.
    139140
    140141definition set_params_hdw :
     
    221222  match s return λ_.bind_step_block ?? with
    222223  [ step_seq s ⇒
    223     match s return λ_.bind_step_block ?? with
    224     [ PUSH _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
    225     | POP _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
    226     | MOVE rs ⇒ bret … [PSD (\fst rs) ← \snd rs]
     224    bret … match s return λ_.step_block ?? with
     225    [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
     226    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
     227    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
    227228    | ADDRESS x prf r1 r2 ⇒
    228       bret … [ADDRESS ERTL ? x prf r1 r2]
     229      [ADDRESS ERTL ? x prf r1 r2]
    229230    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    230       bret … [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
     231      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
    231232    | OP1 op1 destr srcr ⇒
    232       bret … [OP1 ERTL ? op1 destr srcr]
     233      [OP1 ERTL ? op1 destr srcr]
    233234    | OP2 op2 destr srcr1 srcr2 ⇒
    234       bret … [OP2 ERTL ? op2 destr srcr1 srcr2]
     235      [OP2 ERTL ? op2 destr srcr1 srcr2]
    235236    | CLEAR_CARRY ⇒
    236       bret … [CLEAR_CARRY ??]
     237      [CLEAR_CARRY ??]
    237238    | SET_CARRY ⇒
    238       bret … [SET_CARRY ??]
     239      [SET_CARRY ??]
    239240    | LOAD destr addr1 addr2 ⇒
    240       bret … [LOAD ERTL ? destr addr1 addr2]
     241      [LOAD ERTL ? destr addr1 addr2]
    241242    | STORE addr1 addr2 srcr ⇒
    242       bret … [STORE ERTL ? addr1 addr2 srcr]
     243      [STORE ERTL ? addr1 addr2 srcr]
    243244    | COMMENT msg ⇒
    244       bret … [COMMENT … msg]
     245      [COMMENT … msg]
    245246    | extension_seq ext ⇒
    246       match ext return λ_.bind_step_block ?? with
     247      match ext return λ_.step_block ?? with
    247248      [ rtl_stack_address addr1 addr2 ⇒
    248         bret … [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
     249        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
    249250      ]
    250251    ]
     
    273274definition allocate_regs :
    274275  ∀X : Type[0].
    275   (register → register → list (register×Register) → bind_new register X) →
     276  (list (register×Register) → bind_new register X) →
    276277  bind_new register X ≝
    277278  λX,f.
    278   νral,rah in
    279279  let allocate_regs_internal ≝
    280280    λacc : bind_new register (list (register × Register)).
     
    283283    νr' in return (〈r', r〉 :: tl) in
    284284  ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ;
    285   f ral rah to_save.
     285  f to_save.
    286286
    287287definition translate_data :
    288288 ∀globals.joint_closed_internal_function RTL globals →
    289  bind_new register (b_graph_translate_data RTL ERTL globals)
     289 bound_b_graph_translate_data RTL ERTL globals
    290290λglobals,def.
    291291let params ≝ joint_if_params … def in
    292292let new_stacksize ≝
    293293  joint_if_stacksize … def + (|params| - |RegisterParams|) in
    294 allocate_regs …
    295   (λral,rah,to_save.
    296     ! prologue ← prologue globals params ral rah to_save ;
     294allocate_regs ?
     295  (λto_save.
     296    νral,rah,tmpr,addr1,addr2 in
     297    ! prologue ← prologue globals params ral rah tmpr addr1 addr2 to_save ;
    297298    return mk_b_graph_translate_data RTL ERTL globals
    298299    (* init_ret ≝ *) it
     
    300301    (* init_stack_size ≝ *) new_stacksize
    301302    (* added_prologue ≝ *) prologue
     303    (* new_regs ≝ *) (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save)
    302304    (* f_step ≝ *) (translate_step globals)
    303305    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
    304     ???).
     306    ????).
    305307@hide_prf
    306 [ #l #c % ]
    307 #l *
     308[1,2: cases daemon (* TODO *)
     309| #l #c %
     310| #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
     311  [2: #r1 #r2 ] whd #l' #EQ destruct try %
     312  cases s in EQ; whd in match ensure_step_block; normalize nodelta
     313  try #a try #b try #c try #d try #e try #f destruct
     314  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
     315| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 %
     316]
     317(* #l *
    308318[ #l whd %{I} %{I} %1 %
    309319| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
     
    320330  try (%{I} %{I} #l %)
    321331  cases a -a #a #b whd %{I} % [ %{I} ] #l %
    322 ]
     332]*)
    323333qed.
    324334
Note: See TracChangeset for help on using the changeset viewer.