Changeset 1254 for src/RTL/RTLtoERTL.ma
 Timestamp:
 Sep 22, 2011, 4:16:06 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1252 r1254 15 15  joint_st_sequential instr _ ⇒ joint_st_sequential … instr l]. 16 16 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! *) 18 22 let 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) 21 26 on stmt_list ≝ 22 27 match stmt_list with 23 [ nil ⇒ add_graph start_lbl (ertl_st_skipdest_lbl) def28 [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def 24 29  cons stmt stmt_list ⇒ 25 30 match stmt_list with 26 [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def31 [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def 27 32  _ ⇒ 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 (* 35 39 let rec add_translates 36 40 (translate_list: list ?) (start_lbl: label) (dest_lbl: label) … … 50 54 *) 51 55 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 ≝ 56 definition 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 62 let rec fresh_regs (globals: list ident) (def: ertl_internal_function globals) (n: nat) on n ≝ 74 63 match n with 75 64 [ O ⇒ 〈def, [ ]〉 76 65  S n' ⇒ 77 let 〈def', regs'〉 ≝ fresh_regs def n' in78 let 〈def', reg〉 ≝ fresh_reg def' in66 let 〈def', regs'〉 ≝ fresh_regs globals def n' in 67 let 〈def', reg〉 ≝ fresh_reg … def' in 79 68 〈def', reg :: regs'〉 80 69 ]. 81 70 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. 71 lemma 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 // ] 82 qed. 83 84 definition 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. // 88 qed. 89 90 definition save_hdws ≝ 91 λglobals,l. 92 let save_hdws_internal ≝ 93 λdestr_srcr.λstart_lbl. 97 94 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 116 99 definition 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. 123 108 124 109 definition get_params_hdw ≝ 110 λglobals. 125 111 λparams: list register. 126 112 match params with 127 [ nil ⇒ [ get_params_hdw_internal]113 [ nil ⇒ [λstart_lbl: label. adds_graph globals [ joint_st_goto … start_lbl ] start_lbl] 128 114  _ ⇒ 129 115 let l ≝ zip_pottier ? ? params RegisterParams in 130 save_hdws l 131 ]. 116 save_hdws globals l ]. 132 117 133 118 definition get_param_stack ≝ 119 λglobals. 134 120 λoff: nat. 135 121 λdestr. 136 122 λstart_lbl, dest_lbl: label. 137 123 λdef. 138 let 〈def, addr1〉 ≝ fresh_reg def in139 let 〈def, addr2〉 ≝ fresh_reg def in140 let 〈def, tmpr〉 ≝ fresh_reg def in124 let 〈def, addr1〉 ≝ fresh_reg … def in 125 let 〈def, addr2〉 ≝ fresh_reg … def in 126 let 〈def, tmpr〉 ≝ fresh_reg … def in 141 127 let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in 142 adds_graph [143 ertl_st_frame_size addr1start_lbl;144 ertl_st_int tmpr int_offsetstart_lbl;145 ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;146 ertl_st_get_hdw tmpr RegisterSPLstart_lbl;147 ertl_st_op2 Add addr1 addr1 tmprstart_lbl;148 ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;149 ertl_st_get_hdw tmpr RegisterSPHstart_lbl;150 ertl_st_op2 Addc addr2 addr2 tmprstart_lbl;151 ertl_st_load destr addr1 addr2 start_lbl128 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*) 152 138 ] start_lbl dest_lbl def. 153 139
Note: See TracChangeset
for help on using the changeset viewer.