Changeset 1311 for Deliverables/D3.3/idlookupbranch/RTL
 Timestamp:
 Oct 6, 2011, 6:45:54 PM (10 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 1 deleted
 5 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch
 Property svn:mergeinfo changed
/src merged: 1198,12061233,12361260,12621264,1266,12681271,12741276,12781290,1292
 Property svn:mergeinfo changed

Deliverables/D3.3/idlookupbranch/RTL/RTL.ma
r1153 r1311 1 include "basics/list.ma". 2 include "common/Registers.ma". 3 include "common/AST.ma". 4 include "common/Graphs.ma". 5 include "common/CostLabel.ma". 1 include "joint/Joint.ma". 6 2 7 definition registers ≝ list register. 3 (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they 4 are not sequential. Thus there is a dummy label at the moment in the code. 5 To be fixed once we understand exactly what to do with tail calls. *) 6 inductive rtl_statement_extension: Type[0] ≝ 7  rtl_st_ext_address: register → register → rtl_statement_extension 8  rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension 9  rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension 10  rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension. 8 11 9 inductive rtl_statement: Type[0] ≝ 10  rtl_st_skip: label → rtl_statement 11  rtl_st_cost: costlabel → label → rtl_statement 12 (* ldest, hdest, symbol, next *) 13  rtl_st_addr: register → register → ident → label → rtl_statement 14 (* ldest, hdest, next *) 15  rtl_st_stack_addr: register → register → label → rtl_statement 16  rtl_st_int: register → Byte → label → rtl_statement 17 (* dest, src, next *) 18  rtl_st_move: register → register → label → rtl_statement 19  rtl_st_clear_carry: label → rtl_statement 20 (* op, acc dest, bacc dest, acc src, bacc src, next *) 21  rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement 22 (* op, dest, src, next *) 23  rtl_st_op1: Op1 → register → register → label → rtl_statement 24 (* op, dest, src1, src2, next *) 25  rtl_st_op2: Op2 → register → register → register → label → rtl_statement 26  rtl_st_load: register → register → register → label → rtl_statement 27  rtl_st_store: register → register → register → label → rtl_statement 28  rtl_st_call_id: ident → registers → registers → label → rtl_statement 29  rtl_st_call_ptr: register → register → registers → registers → label → rtl_statement 30  rtl_st_tailcall_id: ident → registers → rtl_statement 31  rtl_st_tailcall_ptr: register → register → registers → rtl_statement 32  rtl_st_cond: register → label → label → rtl_statement 33  rtl_st_set_carry: label → rtl_statement 34  rtl_st_return: rtl_statement. 35 36 definition rtl_statement_graph ≝ graph rtl_statement. 12 definition rtl_params__: params__ ≝ 13 mk_params__ register register register register (register × register) register 14 (list register) (list register) rtl_statement_extension. 15 definition rtl_params_: params_ ≝ graph_params_ rtl_params__. 16 definition rtl_params0: params0 ≝ mk_params0 rtl_params__ (list register) (list register). 17 definition rtl_params1: params1 ≝ rtl_ertl_params1 rtl_params0. 18 definition rtl_params: ∀globals. params globals ≝ rtl_ertl_params rtl_params0. 37 19 38 record rtl_internal_function: Type[0] ≝ 39 { 40 rtl_if_luniverse: universe LabelTag; 41 rtl_if_runiverse: universe RegisterTag; 42 (* rtl_if_sig: signature;  dropped in front end *) 43 rtl_if_result : registers; 44 rtl_if_params : registers; 45 rtl_if_locals : registers; 46 rtl_if_stacksize: nat; 47 rtl_if_graph : rtl_statement_graph; 48 rtl_if_entry : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?; 49 rtl_if_exit : Σl: label. lookup ? ? rtl_if_graph l ≠ None ? 50 }. 20 definition rtl_statement ≝ joint_statement rtl_params_. 51 21 52 definition rtl_function_definition ≝ fundef rtl_internal_function. 53 54 record rtl_program: Type[0] ≝ 55 { 56 rtl_pr_vars: list (ident × nat); 57 rtl_pr_functs: list (ident × rtl_function_definition); 58 rtl_pr_main: option ident 59 }. 22 definition rtl_internal_function ≝ 23 λglobals. joint_internal_function … (rtl_params globals). 24 25 definition rtl_program ≝ joint_program rtl_params. 26 27 (************ Same without tail calls ****************) 28 29 (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they 30 are not sequential. Thus there is a dummy label at the moment in the code. 31 To be fixed once we understand exactly what to do with tail calls. *) 32 inductive rtlntc_statement_extension: Type[0] ≝ 33  rtlntc_st_ext_address: register → register → rtlntc_statement_extension 34  rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension. 35 36 definition rtlntc_params__: params__ ≝ 37 mk_params__ register register register register (register × register) register 38 (list register) (list register) rtlntc_statement_extension. 39 definition rtlntc_params_: params_ ≝ graph_params_ rtlntc_params__. 40 definition rtlntc_params0: params0 ≝ mk_params0 rtlntc_params__ (list register) (list register). 41 definition rtlntc_params1: params1 ≝ rtl_ertl_params1 rtlntc_params0. 42 definition rtlntc_params: ∀globals. params globals ≝ rtl_ertl_params rtlntc_params0. 43 44 definition rtlntc_statement ≝ joint_statement rtlntc_params_. 45 46 definition rtlntc_internal_function ≝ 47 λglobals. joint_internal_function … (rtlntc_params globals). 48 49 definition rtlntc_program ≝ joint_program rtlntc_params. 
Deliverables/D3.3/idlookupbranch/RTL/RTLTailcall.ma
r1081 r1311 2 2 3 3 definition simplify_stmt ≝ 4 λglobals. 4 5 λexit: label. 5 6 λlbl: label. 6 λstmt .7 λgraph: rtl_statement_graph.7 λstmt: rtl_statement globals. 8 λgraph: codeT … (rtlntc_params globals). 8 9 match stmt with 9 [ rtl_st_tailcall_id f args ⇒ 10 add ? ? graph lbl (rtl_st_call_id f args [ ] exit) 11  rtl_st_tailcall_ptr f1 f2 args ⇒ 12 add ? ? graph lbl (rtl_st_call_ptr f1 f2 args [ ] exit) 13  _ ⇒ graph 14 ]. 10 [ sequential seq DUMMY ⇒ 11 match seq with 12 [ extension ext ⇒ 13 match ext with 14 [ rtl_st_ext_tailcall_id f args ⇒ 15 add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit) 16  rtl_st_ext_tailcall_ptr f1 f2 args ⇒ 17 add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit) 18  _ ⇒ graph ] 19  _ ⇒ graph ] 20  _ ⇒ graph ]. 15 21 16 22 definition simplify_graph ≝ 23 λglobals. 17 24 λexit: label. 18 λgraph: rtl_statement_graph.19 foldi ? ? ? (simplify_stmt exit) graph graph.25 λgraph: codeT … (rtl_params globals). 26 foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …). 20 27 21 28 axiom simplify_graph_preserves_labels: 22 ∀g: rtl_statement_graph. 29 ∀globals. 30 ∀g: codeT … (rtl_params globals). 23 31 ∀l: label. 24 32 ∀exit: label. 25 lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?.33 lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?. 26 34 27 definition simplify_internal ≝ 28 λdef. 29 let rtl_if_luniverse' ≝ rtl_if_luniverse def in 30 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 31 let rtl_if_result' ≝ rtl_if_result def in 32 let rtl_if_params' ≝ rtl_if_params def in 33 let rtl_if_locals' ≝ rtl_if_locals def in 34 let rtl_if_stacksize' ≝ rtl_if_stacksize def in 35 let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in 36 let rtl_if_entry' ≝ rtl_if_entry def in 37 let rtl_if_exit' ≝ rtl_if_exit def in 38 mk_rtl_internal_function 39 rtl_if_luniverse' rtl_if_runiverse' 40 rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize' 41 rtl_if_graph' ? ?. 42 normalize nodelta 43 [1: cases rtl_if_entry' 44 #ENTRY #ENTRY_PRF 45 % 46 [1: @ENTRY 47 2: @simplify_graph_preserves_labels 48 @ENTRY_PRF 49 ] 50 2: cases rtl_if_exit' 51 #EXIT #EXIT_PRF 52 % 53 [1: @EXIT 54 2: @simplify_graph_preserves_labels 55 @EXIT_PRF 56 ] 57 ] 35 definition simplify_internal : 36 ∀globals. 37 joint_internal_function … (rtl_params globals) → 38 joint_internal_function … (rtlntc_params globals) 39 ≝ 40 λglobals,def. 41 let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in 42 mk_joint_internal_function … 43 (joint_if_luniverse … def) (joint_if_runiverse … def) 44 (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def) 45 (joint_if_stacksize … def) graph 46 (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)). 47 [ cases (joint_if_entry … def)  cases (joint_if_exit … def) ] 48 #l #IH @simplify_graph_preserves_labels @IH 58 49 qed. 59 50 60 definition simplify_funct ≝ 61 λid_def: ident × ?. 62 let 〈id, def〉 ≝ id_def in 63 let def' ≝ 64 match def with 65 [ Internal def ⇒ Internal ? (simplify_internal def) 66  External def ⇒ External ? def 67 ] 68 in 69 〈id, def'〉. 70 71 definition tailcall_simplify ≝ 72 λp. 73 let rtl_pr_vars' ≝ rtl_pr_vars p in 74 let rtl_pr_functs' ≝ map ? ? simplify_funct (rtl_pr_functs p) in 75 let rtl_pr_main' ≝ rtl_pr_main p in 76 mk_rtl_program rtl_pr_vars' rtl_pr_functs' rtl_pr_main'. 51 definition tailcall_simplify : rtl_program → rtlntc_program ≝ 52 λp. transform_program … p (transf_fundef … (simplify_internal …)). 
Deliverables/D3.3/idlookupbranch/RTL/RTLtoERTL.ma
r1153 r1311 1 include "RTL/RTL.ma".2 1 include "RTL/RTLTailcall.ma". 3 2 include "utilities/RegisterSet.ma". 4 3 include "common/Identifiers.ma". 5 4 include "ERTL/ERTL.ma". 6 7 definition change_exit_label ≝ 8 λl: label. 9 λp: ertl_internal_function. 10 λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?. 11 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 12 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 13 let ertl_if_params' ≝ ertl_if_params p in 14 let ertl_if_locals' ≝ ertl_if_locals p in 15 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 16 let ertl_if_graph' ≝ ertl_if_graph p in 17 let ertl_if_entry' ≝ ertl_if_entry p in 18 let ertl_if_exit' ≝ l in 19 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 20 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 21 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 22 @prf 23 qed. 24 25 definition change_entry_label ≝ 26 λl: label. 27 λp: ertl_internal_function. 28 λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?. 29 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 30 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 31 let ertl_if_params' ≝ ertl_if_params p in 32 let ertl_if_locals' ≝ ertl_if_locals p in 33 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 34 let ertl_if_graph' ≝ ertl_if_graph p in 35 let ertl_if_entry' ≝ l in 36 let ertl_if_exit' ≝ ertl_if_exit p in 37 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 38 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 39 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 40 @prf 41 qed. 42 43 definition add_graph ≝ 44 λl: label. 45 λstmt. 46 λp. 47 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 48 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 49 let ertl_if_params' ≝ ertl_if_params p in 50 let ertl_if_locals' ≝ ertl_if_locals p in 51 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 52 let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in 53 let ertl_if_entry' ≝ ertl_if_entry p in 54 let ertl_if_exit' ≝ ertl_if_exit p in 55 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 56 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 57 ertl_if_graph' ? ?. 58 normalize nodelta; 59 [1: generalize in match ertl_if_entry'; 60 #HYP 61 cases HYP 62 #LBL #LBL_PRF 63 % 64 [1: @LBL 65 2: @graph_add_lookup 66 @LBL_PRF 67 ] 68 2: generalize in match ertl_if_exit'; 69 #HYP 70 cases HYP 71 #LBL #LBL_PRF 72 % 73 [1: @LBL 74 2: @graph_add_lookup 75 @LBL_PRF 76 ] 77 ] 78 qed. 79 80 definition fresh_label ≝ 81 λdef. 82 fresh LabelTag (ertl_if_luniverse def). 83 84 definition change_label ≝ 85 λl. 86 λe: ertl_statement. 87 match e with 88 [ ertl_st_skip _ ⇒ ertl_st_skip l 89  ertl_st_comment s _ ⇒ ertl_st_comment s l 90  ertl_st_cost c _ ⇒ ertl_st_cost c l 91  ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l 92  ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l 93  ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l 94  ertl_st_new_frame _ ⇒ ertl_st_new_frame l 95  ertl_st_del_frame _ ⇒ ertl_st_del_frame l 96  ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l 97  ertl_st_pop r _ ⇒ ertl_st_pop r l 98  ertl_st_push r _ ⇒ ertl_st_push r l 99  ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l 100  ertl_st_int r i _ ⇒ ertl_st_int r i l 101  ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l 102  ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l 103  ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l 104  ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l 105  ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l 106  ertl_st_set_carry _ ⇒ ertl_st_set_carry l 107  ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l 108  ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l 109  ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l 110  ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2 111  ertl_st_return ⇒ ertl_st_return 112 ]. 113 114 let rec adds_graph 115 (stmt_list: list ertl_statement) (start_lbl: label) 116 (dest_lbl: label) (def: ertl_internal_function) 117 on stmt_list ≝ 118 match stmt_list with 119 [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def 120  cons stmt stmt_list ⇒ 121 match stmt_list with 122 [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def 123  _ ⇒ 124 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in 125 let stmt ≝ change_label tmp_lbl stmt in 126 let def ≝ add_graph start_lbl stmt def in 127 adds_graph stmt_list tmp_lbl dest_lbl def 128 ] 129 ]. 130 131 let rec add_translates 132 (translate_list: list ?) (start_lbl: label) (dest_lbl: label) 133 (def: ertl_internal_function) 134 on translate_list ≝ 135 match translate_list with 136 [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def 137  cons trans translate_list ⇒ 138 match translate_list with 139 [ nil ⇒ trans start_lbl dest_lbl def 140  _ ⇒ 141 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in 142 let def ≝ trans start_lbl tmp_lbl def in 143 add_translates translate_list tmp_lbl dest_lbl def 144 ] 145 ]. 146 147 axiom register_fresh: universe RegisterTag → register. 148 149 definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝ 150 λdef. 151 let r ≝ register_fresh (ertl_if_runiverse def) in 152 let locals ≝ r :: ertl_if_locals def in 153 let ertl_if_luniverse' ≝ ertl_if_luniverse def in 154 let ertl_if_runiverse' ≝ ertl_if_runiverse def in 155 let ertl_if_params' ≝ ertl_if_params def in 156 let ertl_if_locals' ≝ locals in 157 let ertl_if_stacksize' ≝ ertl_if_stacksize def in 158 let ertl_if_graph' ≝ ertl_if_graph def in 159 let ertl_if_entry' ≝ ertl_if_entry def in 160 let ertl_if_exit' ≝ ertl_if_exit def in 161 〈mk_ertl_internal_function 162 ertl_if_luniverse' ertl_if_runiverse' ertl_if_params' 163 ertl_if_locals' ertl_if_stacksize' ertl_if_graph' 164 ertl_if_entry' ertl_if_exit', r〉. 165 166 let rec fresh_regs 167 (def: ertl_internal_function) (n: nat) 168 on n ≝ 169 match n with 170 [ O ⇒ 〈def, [ ]〉 171  S n' ⇒ 172 let 〈def', regs'〉 ≝ fresh_regs def n' in 173 let 〈def', reg〉 ≝ fresh_reg def' in 174 〈def', reg :: regs'〉 175 ]. 176 177 axiom fresh_regs_length: 178 ∀def: ertl_internal_function. 179 ∀n: nat. 180 (\snd (fresh_regs def n)) = n. 181 182 definition fresh_regs_strong: ? → ∀n: nat. Σregs: ertl_internal_function × (list register). \snd regs = n ≝ 183 λdef: ertl_internal_function. 184 λn: nat. 185 fresh_regs def n. 186 @fresh_regs_length 187 qed. 188 189 definition save_hdws_internal ≝ 190 λdestr_srcr: register × Register. 191 λstart_lbl: label. 5 include "joint/TranslateUtils.ma". 6 7 definition save_hdws ≝ 8 λglobals,l. 9 let save_hdws_internal ≝ 10 λdestr_srcr.λstart_lbl. 192 11 let 〈destr, srcr〉 ≝ destr_srcr in 193 adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl. 194 195 definition save_hdws ≝ 196 λl. 197 map ? ? save_hdws_internal l. 198 199 definition restore_hdws_internal ≝ 200 λdestr_srcr: Register × register. 201 λstart_lbl: label. 202 let 〈destr, srcr〉 ≝ destr_srcr in 203 adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl. 204 205 definition swap_components ≝ 206 λA, B: Type[0]. 207 λp: A × B. 208 let 〈l, r〉 ≝ p in 209 〈r, l〉. 210 12 adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl 13 in 14 map ? ? save_hdws_internal l. 15 211 16 definition restore_hdws ≝ 212 λl. 213 map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l). 214 215 definition get_params_hdw_internal ≝ 216 λstart_lbl: label. 217 adds_graph [ ertl_st_skip start_lbl ] start_lbl. 17 λglobals,l. 18 let restore_hdws_internal ≝ 19 λsrcr_destr: register × Register. 20 λstart_lbl: label. 21 let 〈srcr, destr〉 ≝ srcr_destr in 22 adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl 23 in 24 map ? ? restore_hdws_internal l. 218 25 219 26 definition get_params_hdw ≝ 27 λglobals. 220 28 λparams: list register. 221 29 match params with 222 [ nil ⇒ [ get_params_hdw_internal]30 [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl] 223 31  _ ⇒ 224 32 let l ≝ zip_pottier ? ? params RegisterParams in 225 save_hdws l 226 ]. 33 save_hdws globals l ]. 227 34 228 35 definition get_param_stack ≝ 36 λglobals. 229 37 λoff: nat. 230 38 λdestr. 231 39 λstart_lbl, dest_lbl: label. 232 40 λdef. 233 let 〈def, addr1〉 ≝ fresh_reg def in234 let 〈def, addr2〉 ≝ fresh_reg def in235 let 〈def, tmpr〉 ≝ fresh_reg def in41 let 〈def, addr1〉 ≝ fresh_reg … def in 42 let 〈def, addr2〉 ≝ fresh_reg … def in 43 let 〈def, tmpr〉 ≝ fresh_reg … def in 236 44 let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in 237 adds_graph [238 ertl_st_frame_size addr1 start_lbl;239 ertl_st_int tmpr int_offset start_lbl;240 ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;241 ertl_st_get_hdw tmpr RegisterSPL start_lbl;242 ertl_st_op2 Add addr1 addr1 tmpr start_lbl;243 ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;244 ertl_st_get_hdw tmpr RegisterSPH start_lbl;245 ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;246 ertl_st_load destr addr1 addr2 start_lbl45 adds_graph ertl_params1 globals [ 46 sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1)); 47 sequential ertl_params_ … (INT … tmpr int_offset); 48 sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr); 49 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉); 50 sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr); 51 sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0)); 52 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); 53 sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr); 54 sequential ertl_params_ … (LOAD … destr addr1 addr2) 247 55 ] start_lbl dest_lbl def. 248 56 249 57 definition get_params_stack ≝ 250 λ params.58 λglobals,params. 251 59 match params with 252 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ] 253  _ ⇒ 254 let f ≝ λi. λr. get_param_stack i r in 255 mapi ? ? f params 256 ]. 60 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ] 61  _ ⇒ mapi ? ? (get_param_stack globals) params ]. 257 62 258 63 definition get_params ≝ 259 λ params.260 let n ≝ min (length ? params) (length ?RegisterParams) in261 let 〈hdw_params, stack_params〉 ≝ list_split ?n params in262 let hdw_params ≝ get_params_hdw hdw_params in263 hdw_params @ (get_params_stack stack_params).264 64 λglobals,params. 65 let n ≝ min (length … params) (length … RegisterParams) in 66 let 〈hdw_params, stack_params〉 ≝ list_split … n params in 67 let hdw_params ≝ get_params_hdw globals hdw_params in 68 hdw_params @ (get_params_stack … stack_params). 69 265 70 definition add_prologue ≝ 71 λglobals. 266 72 λparams: list register. 267 73 λsral. … … 269 75 λsregs. 270 76 λdef. 271 let start_lbl ≝ ertl_if_entrydef in272 let 〈tmp_lbl, nuniv〉 ≝ fresh_labeldef in273 match lookup ? ? (ertl_if_graphdef) start_lbl274 return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_functionwith275 [ None ⇒ λnone_absrd. ?77 let start_lbl ≝ joint_if_entry … (ertl_params globals) def in 78 let 〈tmp_lbl, def〉 ≝ fresh_label … def in 79 match lookup … (joint_if_code … def) start_lbl 80 return λx. x ≠ None ? → ertl_internal_function globals with 81 [ None ⇒ λnone_absrd. ⊥ 276 82  Some last_stmt ⇒ λsome_prf. 277 83 let def ≝ 278 add_translates 279 ((adds_graph [280 ertl_st_new_frame start_lbl84 add_translates … 85 ((adds_graph ertl_params1 … [ 86 sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) 281 87 ]) :: 282 (adds_graph [283 ertl_st_pop sral start_lbl;284 ertl_st_pop srah start_lbl88 (adds_graph ertl_params1 … [ 89 sequential ertl_params_ … (POP … sral); 90 sequential ertl_params_ … (POP … srah) 285 91 ]) :: 286 (save_hdws sregs) @287 (get_params params))92 (save_hdws … sregs) @ 93 (get_params … params)) 288 94 start_lbl tmp_lbl def 289 95 in 290 add_graph tmp_lbl last_stmt def96 add_graph … tmp_lbl last_stmt def 291 97 ] ?. 292 cases not_implemented (* dep. types here *) 98 [ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *) 99  cases (none_absrd) /2/ ] 293 100 qed. 294 101 295 102 definition save_return ≝ 103 λglobals. 296 104 λret_regs. 297 105 λstart_lbl: label. 298 106 λdest_lbl: label. 299 λdef: ertl_internal_function .300 let 〈def, tmpr〉 ≝ fresh_reg def in107 λdef: ertl_internal_function globals. 108 let 〈def, tmpr〉 ≝ fresh_reg … def in 301 109 match reduce_strong ? ? RegisterSTS ret_regs with 302 110 [ dp crl crl_proof ⇒ … … 305 113 let restl ≝ \snd (\fst crl) in 306 114 let restr ≝ \snd (\snd crl) in 307 let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lblin308 let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lblin309 let saves ≝ map2 ? ? ?f_save commonl commonr crl_proof in310 let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lblin311 let defaults ≝ map ? ?f_default restl in312 adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def115 let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in 116 let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in 117 let saves ≝ map2 … f_save commonl commonr crl_proof in 118 let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in 119 let defaults ≝ map … f_default restl in 120 adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def 313 121 ]. 314 122 315 123 definition assign_result ≝ 316 λ start_lbl: label.124 λglobals.λstart_lbl: label. 317 125 match reduce_strong ? ? RegisterRets RegisterSTS with 318 126 [ dp crl crl_proof ⇒ 319 127 let commonl ≝ \fst (\fst crl) in 320 128 let commonr ≝ \fst (\snd crl) in 321 let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lblin129 let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in 322 130 let insts ≝ map2 ? ? ? f commonl commonr crl_proof in 323 adds_graph insts start_lbl131 adds_graph ertl_params1 … insts start_lbl 324 132 ]. 325 133 326 134 definition add_epilogue ≝ 135 λglobals. 327 136 λret_regs. 328 137 λsral. … … 330 139 λsregs. 331 140 λdef. 332 let start_lbl ≝ ertl_if_exitdef in333 let 〈tmp_lbl, nuniv〉 ≝ fresh_labeldef in334 match lookup ? ? (ertl_if_graphdef) start_lbl335 return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ?with336 [ None ⇒ λnone_abs d. ?141 let start_lbl ≝ joint_if_exit … (ertl_params globals) def in 142 let 〈tmp_lbl, def〉 ≝ fresh_label … def in 143 match lookup … (joint_if_code … def) start_lbl 144 return λx. x ≠ None ? → ertl_internal_function globals with 145 [ None ⇒ λnone_absrd. ⊥ 337 146  Some last_stmt ⇒ λsome_prf. 338 147 let def ≝ 339 add_translates (340 [save_return ret_regs] @341 restore_hdws sregs @342 [adds_graph [343 ertl_st_push srah start_lbl;344 ertl_st_push sral start_lbl148 add_translates ertl_params1 … ( 149 [save_return globals ret_regs] @ 150 restore_hdws … sregs @ 151 [adds_graph ertl_params1 … [ 152 sequential ertl_params_ … (PUSH … srah); 153 sequential ertl_params_ … (PUSH … sral) 345 154 ]] @ 346 [adds_graph [347 ertl_st_del_frame start_lbl155 [adds_graph ertl_params1 … [ 156 sequential ertl_params_ … (extension … ertl_st_ext_del_frame) 348 157 ]] @ 349 [assign_result ]158 [assign_result globals] 350 159 ) start_lbl tmp_lbl def 351 160 in 352 let def ≝ add_graphtmp_lbl last_stmt def in353 change_exit_label tmp_lbl def?161 let def' ≝ add_graph … tmp_lbl last_stmt def in 162 set_joint_if_exit … tmp_lbl def' ? 354 163 ] ?. 355 cases not_implemented (* dep types here, bug in matita too! *) 164 [ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *) 165  cases (none_absrd) /2/ 166  cases daemon (* CSC: XXXXX *) 167 ] 356 168 qed. 357 169 358 definition allocate_regs_internal ≝ 359 λr: Register. 360 λdef_sregs. 361 let 〈def, sregs〉 ≝ def_sregs in 362 let 〈def, r'〉 ≝ fresh_reg def in 363 〈def, 〈r', r〉 :: sregs〉. 364 170 365 171 definition allocate_regs ≝ 172 λglobals. 366 173 λrs. 367 174 λsaved: rs_set rs. 368 175 λdef. 176 let allocate_regs_internal ≝ 177 λr: Register. 178 λdef_sregs. 179 let 〈def, sregs〉 ≝ def_sregs in 180 let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in 181 〈def, 〈r', r〉 :: sregs〉 182 in 369 183 rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉. 370 184 371 185 definition add_pro_and_epilogue ≝ 186 λglobals. 372 187 λparams. 373 188 λret_regs. 374 189 λdef. 375 match fresh_regs_strong def 2 with190 match fresh_regs_strong … globals def 2 with 376 191 [ dp def_sra def_sra_proof ⇒ 377 192 let def ≝ \fst def_sra in … … 379 194 let sral ≝ nth_safe ? 0 sra ? in 380 195 let srah ≝ nth_safe ? 1 sra ? in 381 let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in382 let def ≝ add_prologue params sral srah sregs def in383 let def ≝ add_epilogue ret_regs sral srah sregs def in196 let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in 197 let def ≝ add_prologue … params sral srah sregs def in 198 let def ≝ add_epilogue … ret_regs sral srah sregs def in 384 199 def 385 200 ]. 386 [1: >def_sra_proof // 387 2: >def_sra_proof // 388 ] 201 >def_sra_proof // 389 202 qed. 390 203 391 204 definition set_params_hdw ≝ 392 λ params.205 λglobals,params. 393 206 match params with 394 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]207 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl] 395 208  _ ⇒ 396 209 let l ≝ zip_pottier ? ? params RegisterParams in 397 restore_hdws l210 restore_hdws globals l 398 211 ]. 399 212 400 213 definition set_param_stack ≝ 214 λglobals. 401 215 λoff. 402 216 λsrcr. 403 217 λstart_lbl: label. 404 218 λdest_lbl: label. 405 λdef: ertl_internal_function .406 let 〈def, addr1〉 ≝ fresh_reg def in407 let 〈def, addr2〉 ≝ fresh_reg def in408 let 〈def, tmpr〉 ≝ fresh_reg def in219 λdef: ertl_internal_function globals. 220 let 〈def, addr1〉 ≝ fresh_reg … def in 221 let 〈def, addr2〉 ≝ fresh_reg … def in 222 let 〈def, tmpr〉 ≝ fresh_reg … def in 409 223 let 〈ignore, int_off〉 ≝ half_add ? off int_size in 410 adds_graph [411 ertl_st_int addr1 int_off start_lbl;412 ertl_st_get_hdw tmpr RegisterSPL start_lbl;413 ertl_st_clear_carry start_lbl;414 ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;415 ertl_st_get_hdw tmpr RegisterSPH start_lbl;416 ertl_st_int addr2 (zero ?) start_lbl;417 ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;418 ertl_st_store addr1 addr2 srcr start_lbl224 adds_graph ertl_params1 … [ 225 sequential ertl_params_ … (INT … addr1 int_off); 226 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉); 227 sequential ertl_params_ … (CLEAR_CARRY …); 228 sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1); 229 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); 230 sequential ertl_params_ … (INT … addr2 (zero ?)); 231 sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2); 232 sequential ertl_params_ … (STORE … addr1 addr2 srcr) 419 233 ] start_lbl dest_lbl def. 420 234 421 235 definition set_params_stack ≝ 422 λ params.236 λglobals,params. 423 237 match params with 424 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]238 [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl] 425 239  _ ⇒ 426 let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in 427 mapi ? ? f params 428 ]. 429 430 axiom min_fst: 431 ∀m, n: nat. 432 min m n ≤ m. 240 let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in 241 mapi ? ? f params]. 433 242 434 243 definition set_params ≝ 435 λ params.244 λglobals,params. 436 245 let n ≝ min (params) (RegisterParams) in 437 246 let hdw_stack_params ≝ split ? params n ? in 438 247 let hdw_params ≝ \fst hdw_stack_params in 439 248 let stack_params ≝ \snd hdw_stack_params in 440 set_params_hdw hdw_params @ set_params_stackstack_params.441 @min_fst 249 set_params_hdw globals hdw_params @ set_params_stack globals stack_params. 250 /2/ 442 251 qed. 443 252 444 253 definition fetch_result ≝ 254 λglobals. 445 255 λret_regs. 446 256 λstart_lbl: label. … … 449 259 let commonl ≝ \fst (\fst crl) in 450 260 let commonr ≝ \fst (\snd crl) in 451 let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st ret start_lblin261 let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in 452 262 let saves ≝ map2 ? ? ? f_save commonl commonr ? in 453 263 match reduce_strong ? ? ret_regs RegisterSTS with … … 455 265 let commonl ≝ \fst (\fst crl) in 456 266 let commonr ≝ \fst (\snd crl) in 457 let f_restore ≝ λr. λst. ertl_st_get_hdw r st start_lblin267 let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in 458 268 let restores ≝ map2 ? ? ? f_restore commonl commonr ? in 459 adds_graph (saves @ restores) start_lbl 460 ] 461 ]. 462 [ normalize nodelta; @second_crl_proof 463  @first_crl_proof 464 ] 269 adds_graph ertl_params1 … (saves @ restores) start_lbl]]. 270 [@second_crl_proof  @first_crl_proof] 465 271 qed. 466 272 467 273 definition translate_call_id ≝ 468 λ f.274 λglobals,f. 469 275 λargs. 470 276 λret_regs. … … 473 279 λdef. 474 280 let nb_args ≝ args in 475 add_translates (476 set_params args @ [477 adds_graph [ ertl_st_call_id f nb_args start_lbl];478 fetch_result ret_regs281 add_translates ertl_params1 globals ( 282 set_params … args @ [ 283 adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ]; 284 fetch_result … ret_regs 479 285 ] 480 286 ) start_lbl dest_lbl def. 481 287 482 definition translate_stmt ≝ 288 definition translate_stmt : 289 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals 290 ≝ 291 λglobals. 483 292 λlbl. 484 293 λstmt. 485 294 λdef. 486 295 match stmt with 487 [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def 488  rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def 489  rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def 490  rtl_st_stack_addr r1 r2 lbl' ⇒ 491 adds_graph [ 492 ertl_st_get_hdw r1 RegisterSPL lbl; 493 ertl_st_get_hdw r2 RegisterSPH lbl 494 ] lbl lbl' def 495  rtl_st_int r i lbl' ⇒ add_graph lbl (ertl_st_int r i lbl') def 496  rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def 497  rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒ 498 add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def 499 (* XXX: change from o'caml 500 adds_graph [ 501 ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl; 502 ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl 503 ] lbl lbl' def 504 *) 505  rtl_st_op1 op1 destr srcr lbl' ⇒ 506 add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def 507  rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒ 508 add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def 509  rtl_st_clear_carry lbl' ⇒ 510 add_graph lbl (ertl_st_clear_carry lbl') def 511  rtl_st_set_carry lbl' ⇒ 512 add_graph lbl (ertl_st_set_carry lbl') def 513  rtl_st_load destr addr1 addr2 lbl' ⇒ 514 add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def 515  rtl_st_store addr1 addr2 srcr lbl' ⇒ 516 add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def 517  rtl_st_call_id f args ret_regs lbl' ⇒ 518 translate_call_id f args ret_regs lbl lbl' def 519  rtl_st_cond srcr lbl_true lbl_false ⇒ 520 add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def 521  rtl_st_return ⇒ 522 add_graph lbl ertl_st_return def 523  _ ⇒ ? (* assert false: not implemented or should not happen *) 524 ]. 525 cases not_implemented 526 qed. 296 [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def 297  RETURN ⇒ add_graph … lbl (RETURN …) def 298  sequential seq lbl' ⇒ 299 match seq with 300 [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *) 301  POP _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *) 302  CALL_ID f args ret_regs ⇒ 303 translate_call_id … f args ret_regs lbl lbl' def 304  MOVE rs ⇒ 305 let 〈r1,r2〉 ≝ rs in 306 let rs ≝ 〈pseudo r1, pseudo r2〉 in 307 add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def 308  extension ext ⇒ 309 match ext with 310 [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *) 311  rtlntc_st_ext_address r1 r2 ⇒ 312 adds_graph ertl_params1 … [ 313 sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉); 314 sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) 315 ] lbl lbl' def] 316 (*CSC: everything is just copied to retype it from now on; 317 the problem is call_id that takes different parameters, but that is patternmatched 318 above. It could be made nicer at the cost of making all the rest of the code uglier *) 319  COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def 320  ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def 321  INT r i ⇒ add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def 322  OPACCS op destr1 destr2 srcr1 srcr2 ⇒ 323 add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def 324  OP1 op1 destr srcr ⇒ 325 add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def 326  OP2 op2 destr srcr1 srcr2 ⇒ 327 add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def 328  CLEAR_CARRY ⇒ 329 add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def 330  SET_CARRY ⇒ 331 add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def 332  LOAD destr addr1 addr2 ⇒ 333 add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def 334  STORE addr1 addr2 srcr ⇒ 335 add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def 336  COND srcr lbl_true ⇒ 337 add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def 338  COMMENT msg ⇒ 339 add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def 340 ]]. 341 @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *) 342 qed. 527 343 528 344 (* hack with empty graphs used here *) 529 345 definition translate_funct_internal ≝ 530 λ def.531 let nb_params ≝  rtl_if_paramsdef in346 λglobals.λdef:rtlntc_internal_function globals. 347 let nb_params ≝ joint_if_params ?? def in 532 348 let added_stacksize ≝ max 0 (nb_params  RegisterParams) in 533 let new_locals ≝ nub_by ? (eq_identifier ?) (( rtl_if_locals def) @ (rtl_if_paramsdef)) in534 let entry' ≝ rtl_if_entrydef in535 let exit' ≝ rtl_if_exitdef in536 let graph' ≝ add ? ? (empty_map ? ?) entry' ( ertl_st_skipentry') in537 let graph' ≝ add ? ? graph' exit' ( ertl_st_skipexit') in349 let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in 350 let entry' ≝ joint_if_entry … def in 351 let exit' ≝ joint_if_exit … def in 352 let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in 353 let graph' ≝ add ? ? graph' exit' (GOTO … exit') in 538 354 let def' ≝ 539 mk_ ertl_internal_function540 ( rtl_if_luniverse def) (rtl_if_runiverse def)541 nb_params new_locals (( rtl_if_stacksizedef) + added_stacksize)355 mk_joint_internal_function globals (ertl_params globals) 356 (joint_if_luniverse … def) (joint_if_runiverse … def) it 357 nb_params new_locals ((joint_if_stacksize … def) + added_stacksize) 542 358 graph' ? ? in 543 let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in 544 let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in 545 def'. 546 [1: % 547 [1: @entry' 548 2: normalize nodelta 549 @graph_add_lookup 550 @graph_add 551 ] 552 2: % 553 [1: @exit' 554 2: normalize nodelta 555 @graph_add 556 ] 359 let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in 360 add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'. 361 whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction 362 makes the next application fail. Why? *) 363 % 364 [ @entry'  @graph_add_lookup @graph_add 365  @exit'  @graph_add ] 366 qed. 367 368 definition generate ≝ 369 λglobals. 370 λstmt. 371 λdef: joint_internal_function … (ertl_params globals). 372 let 〈entry, def〉 ≝ fresh_label … def in 373 let graph ≝ add … (joint_if_code … def) entry stmt in 374 set_joint_if_graph … (ertl_params globals) graph def ??. 375 [ (*% [ @entry  @graph_add ]*) cases daemon (*CSC: XXX *) 376  (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL  @graph_add_lookup @LBL_PRF 377 *) cases daemon (*CSC: XXX *) 557 378 ] 558 379 qed. 559 560 definition translate_funct ≝ 561 λid_def: ident × ?. 562 let 〈id, def〉 ≝ id_def in 563 let def' ≝ 564 match def with 565 [ Internal def ⇒ Internal ? (translate_funct_internal def) 566  External def ⇒ External ? def 567 ] in 568 〈id, def'〉. 569 570 definition generate ≝ 571 λstmt. 572 λdef. 573 let 〈entry, nuniv〉 ≝ fresh_label def in 574 let graph ≝ add ? ? (ertl_if_graph def) entry stmt in 575 mk_ertl_internal_function 576 nuniv (ertl_if_runiverse def) (ertl_if_params def) 577 (ertl_if_locals def) (ertl_if_stacksize def) graph 578 ? ?. 579 [1: % 580 [1: @entry 581 2: normalize nodelta; 582 @graph_add 583 ] 584 2: generalize in match (ertl_if_exit def) 585 #HYP 586 cases HYP 587 #LBL #LBL_PRF 588 % 589 [1: @LBL 590 2: normalize nodelta; 591 @graph_add_lookup 592 @LBL_PRF 593 ] 594 ] 595 qed. 596 597 let rec find_and_remove_first_cost_label_internal 598 (def: ertl_internal_function) (lbl: label) (num_nodes: nat) 380 381 let rec find_and_remove_first_cost_label_internal (globals: list ident) 382 (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat) 599 383 on num_nodes ≝ 600 384 match num_nodes with 601 385 [ O ⇒ 〈None ?, def〉 602 386  S num_nodes' ⇒ 603 match lookup ? ? (ertl_if_graphdef) lbl with387 match lookup … (joint_if_code … def) lbl with 604 388 [ None ⇒ 〈None ?, def〉 605  Some stmt ⇒ 389  Some stmt ⇒ 606 390 match stmt with 607 [ ertl_st_cost cost_lbl next_lbl ⇒ 608 〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉 609  ertl_st_cond _ _ _ ⇒ 〈None ?, def〉 610  ertl_st_return ⇒ 〈None ?, def〉 611  ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 612  ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 613  ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 614  ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 615  ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 616  ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 617  ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 618  ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 619  ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 620  ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 621  ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 622  ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 623  ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 624  ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 625  ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 626  ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 627  ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 628  ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 629  ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 630  ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 631  ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 632 ] 633 ] 634 ]. 391 [ sequential inst lbl ⇒ 392 match inst with 393 [ COST_LABEL cost_lbl ⇒ 394 〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉 395  _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] 396  RETURN ⇒ 〈None …, def〉 397  GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' 398 ]]]. 635 399 636 400 definition find_and_remove_first_cost_label ≝ 637 λ def.638 find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (ertl_if_graphdef)).401 λglobals,def. 402 find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)). 639 403 640 404 definition move_first_cost_label_up_internal ≝ 641 λ def.642 let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in405 λglobals,def. 406 let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in 643 407 match cost_label with 644 408 [ None ⇒ def 645  Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entrydef)) def409  Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def 646 410 ]. 647 411 648 definition move_first_cost_label_up ≝ 649 λA: Type[0]. 650 λid_def: A × ?. 651 let 〈id, def〉 ≝ id_def in 652 let def' ≝ 653 match def with 654 [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun) 655  External ext ⇒ def 656 ] 657 in 658 〈id, def'〉. 659 660 definition translate ≝ 661 λp. 412 definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). 413 414 definition translate : rtl_program → ertl_program ≝ 415 λp. 662 416 let p ≝ tailcall_simplify p in (* tailcall simplification here *) 663 let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct) in 664 let vars ≝ map ? ? f (rtl_pr_functs p) in 665 mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p). 417 transform_program ??? p (transf_fundef ?? (translate_funct …)). 
Deliverables/D3.3/idlookupbranch/RTL/semantics.ma
r1153 r1311 264 264 [ nil ⇒ Some ? (smerge2 v) 265 265  _ ⇒ None ? ]]. 266 266 (* 267 267 definition RTL_exec : execstep io_out io_in ≝ 268 268 mk_execstep … ? is_final mem_of_state eval_statement. 269 269 *) 270 270 (* CSC: XXX the program type does not fit with the globalenv and init_mem 271 271 definition make_initial_state : rtl_program → res (genv × state) ≝
Note: See TracChangeset
for help on using the changeset viewer.