Changeset 1254 for src/RTL


Ignore:
Timestamp:
Sep 22, 2011, 4:16:06 PM (9 years ago)
Author:
sacerdot
Message:

More progress towards porting of RTLtoERTL to joint syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTL/RTLtoERTL.ma

    r1252 r1254  
    1515  | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l].
    1616
    17 (* 
     17(*CSC: bad programming habit: the code below puts everywhere a fake
     18  label and then adds_graph fixes them *)
     19(*CSC: the code is artificially fixed to work on ertl_statements, but
     20  it works on every graph_params *)
     21(*CSC: this is just an instance of add_translates below! *)
    1822let rec adds_graph
    19   (stmt_list: list ertl_statement) (start_lbl: label)
    20   (dest_lbl: label) (def: ertl_internal_function)
     23  (globals: list ident)
     24  (stmt_list: list (ertl_statement globals)) (start_lbl: label)
     25  (dest_lbl: label) (def: ertl_internal_function globals)
    2126    on stmt_list ≝
    2227  match stmt_list with
    23   [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
     28  [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
    2429  | cons stmt stmt_list ⇒
    2530    match stmt_list with
    26     [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def
     31    [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def
    2732    | _ ⇒
    28       let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    29       let stmt ≝ change_label tmp_lbl stmt in
    30       let def ≝ add_graph start_lbl stmt def in
    31         adds_graph stmt_list tmp_lbl dest_lbl def
    32     ]
    33   ].
    34 
     33      let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
     34      let stmt ≝ change_label … stmt tmp_lbl in
     35      let def ≝ add_graph … start_lbl stmt def in
     36        adds_graph globals stmt_list tmp_lbl dest_lbl def]].
     37
     38(*
    3539let rec add_translates
    3640  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
    … …  
    5054*)
    5155
    52 axiom register_fresh: universe RegisterTag → register.
    53 
    54 definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝
    55   λdef.
    56     let r ≝ register_fresh (ertl_if_runiverse def) in
    57     let locals ≝ r :: ertl_if_locals def in
    58     let ertl_if_luniverse' ≝ ertl_if_luniverse def in
    59     let ertl_if_runiverse' ≝ ertl_if_runiverse def in
    60     let ertl_if_params' ≝ ertl_if_params def in
    61     let ertl_if_locals' ≝ locals in
    62     let ertl_if_stacksize' ≝ ertl_if_stacksize def in
    63     let ertl_if_graph' ≝ ertl_if_graph def in
    64     let ertl_if_entry' ≝ ertl_if_entry def in
    65     let ertl_if_exit' ≝ ertl_if_exit def in
    66       〈mk_ertl_internal_function
    67         ertl_if_luniverse' ertl_if_runiverse' ertl_if_params'
    68         ertl_if_locals' ertl_if_stacksize' ertl_if_graph'
    69         ertl_if_entry' ertl_if_exit', r〉.
    70 
    71 let rec fresh_regs
    72   (def: ertl_internal_function) (n: nat)
    73     on n ≝
     56definition fresh_reg:
     57 ∀globals. ertl_internal_function globals → (ertl_internal_function globals) × register ≝
     58  λglobals,def.
     59    let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     60     〈set_locals … (set_runiverse … def runiverse) (r::joint_if_locals … def), r〉.
     61
     62let rec fresh_regs (globals: list ident) (def: ertl_internal_function globals) (n: nat) on n ≝
    7463  match n with
    7564  [ O ⇒ 〈def, [ ]〉
    7665  | S n' ⇒
    77     let 〈def', regs'〉 ≝ fresh_regs def n' in
    78     let 〈def', reg〉 ≝ fresh_reg def' in
     66    let 〈def', regs'〉 ≝ fresh_regs globals def n' in
     67    let 〈def', reg〉 ≝ fresh_reg … def' in
    7968      〈def', reg :: regs'〉
    8069  ].
    8170 
    82 axiom fresh_regs_length:
    83   ∀def: ertl_internal_function.
    84   ∀n: nat.
    85     |(\snd (fresh_regs def n))| = n.
    86 
    87 definition fresh_regs_strong: ? → ∀n: nat. Σregs: ertl_internal_function × (list register). |\snd regs| = n ≝
    88   λdef: ertl_internal_function.
    89   λn: nat.
    90     fresh_regs def n.
    91   @fresh_regs_length
    92 qed.
    93  
    94 definition save_hdws_internal ≝
    95   λdestr_srcr: register × Register.
    96   λstart_lbl: label.
     71lemma fresh_regs_length:
     72 ∀globals.∀def: ertl_internal_function globals. ∀n: nat.
     73  |(\snd (fresh_regs … def n))| = n.
     74 #globals #def #n elim n
     75  [ %
     76  | #m whd in ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?)
     77    cases (fresh_regs globals def m) normalize nodelta
     78    #def' #regs #EQ change in EQ with (|regs| = m) <EQ
     79    change with
     80    (|let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ?| = ?)
     81    cases (fresh … (joint_if_runiverse … def')) normalize // ]
     82qed.
     83
     84definition fresh_regs_strong:
     85 ∀globals. ertl_internal_function globals →
     86  ∀n: nat. Σregs: (ertl_internal_function globals) × (list register). |\snd regs| = n ≝
     87 λdef,n.fresh_regs def n. //
     88qed.
     89
     90definition save_hdws ≝
     91 λglobals,l.
     92  let save_hdws_internal ≝
     93   λdestr_srcr.λstart_lbl.
    9794    let 〈destr, srcr〉 ≝ destr_srcr in
    98       adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
    99  
    100 definition save_hdws ≝
    101   λl.
    102     map ? ? save_hdws_internal l.
    103    
    104 definition restore_hdws_internal ≝
    105   λdestr_srcr: Register × register.
    106   λstart_lbl: label.
    107     let 〈destr, srcr〉 ≝ destr_srcr in
    108     adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
    109    
    110 definition swap_components ≝
    111   λA, B: Type[0].
    112   λp: A × B.
    113   let 〈l, r〉 ≝ p in
    114   〈r, l〉.
    115    
     95     adds_graph globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
     96  in
     97   map ? ? save_hdws_internal l.
     98
    11699definition restore_hdws ≝
    117   λl.
    118     map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).
    119 
    120 definition get_params_hdw_internal ≝
    121   λstart_lbl: label.
    122     adds_graph [ ertl_st_skip start_lbl ] start_lbl.
     100  λglobals,l.
     101   let restore_hdws_internal ≝
     102    λsrcr_destr: register × Register.
     103    λstart_lbl: label.
     104     let 〈srcr, destr〉 ≝ srcr_destr in
     105     adds_graph globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
     106   in
     107    map ? ? restore_hdws_internal l.
    123108
    124109definition get_params_hdw ≝
     110  λglobals.
    125111  λparams: list register.
    126112  match params with
    127   [ nil ⇒ [get_params_hdw_internal]
     113  [ nil ⇒ [λstart_lbl: label. adds_graph globals [ joint_st_goto … start_lbl ] start_lbl]
    128114  | _ ⇒
    129115    let l ≝ zip_pottier ? ? params RegisterParams in
    130       save_hdws l
    131   ].
     116      save_hdws globals l ].
    132117
    133118definition get_param_stack ≝
     119  λglobals.
    134120  λoff: nat.
    135121  λdestr.
    136122  λstart_lbl, dest_lbl: label.
    137123  λdef.
    138   let 〈def, addr1〉 ≝ fresh_reg def in
    139   let 〈def, addr2〉 ≝ fresh_reg def in
    140   let 〈def, tmpr〉 ≝ fresh_reg def in
     124  let 〈def, addr1〉 ≝ fresh_reg … def in
     125  let 〈def, addr2〉 ≝ fresh_reg … def in
     126  let 〈def, tmpr〉 ≝ fresh_reg … def in
    141127  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    142   adds_graph [
    143     ertl_st_frame_size addr1 start_lbl;
    144     ertl_st_int tmpr int_offset start_lbl;
    145     ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
    146     ertl_st_get_hdw tmpr RegisterSPL start_lbl;
    147     ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
    148     ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
    149     ertl_st_get_hdw tmpr RegisterSPH start_lbl;
    150     ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
    151     ertl_st_load destr addr1 addr2 start_lbl
     128  adds_graph globals [
     129    joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl;
     130    joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl;
     131    joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl(*;
     132    joint_st_sequential … (joint_instr_get_hdw … tmpr RegisterSPL) start_lbl;
     133    joint_st_sequential … (joint_instr_op2 … Add addr1 addr1 tmpr) start_lbl;
     134    joint_st_sequential … (joint_instr_int … addr2 (bitvector_of_nat 8 0)) start_lbl;
     135    joint_st_sequential … (joint_instr_get_hdw … tmpr RegisterSPH) start_lbl;
     136    joint_st_sequential … (joint_instr_op2 … Addc addr2 addr2 tmpr) start_lbl;
     137    joint_st_sequential … (joint_instr_load … destr addr1 addr2) start_lbl*)
    152138  ] start_lbl dest_lbl def.
    153139 
Note: See TracChangeset for help on using the changeset viewer.