Changeset 1197 for Deliverables/D3.3/id-lookup-branch/ERTL
- Timestamp:
- Sep 7, 2011, 12:10:27 PM (9 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 1 deleted
- 7 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
- Property svn:mergeinfo changed
/src merged: 1151-1152,1154-1183,1185-1188,1191-1196
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma
r1153 r1197 1 1 include "ASM/I8051.ma". 2 include "joint/Joint.ma". 2 3 include "utilities/BitVectorTrieSet.ma". 3 4 include "utilities/IdentifierTools.ma". … … 8 9 definition registers ≝ list register. 9 10 10 inductive ertl_statement: Type[0] ≝ 11 | ertl_st_skip: label → ertl_statement 12 | ertl_st_comment: String → label → ertl_statement 13 | ertl_st_cost: costlabel → label → ertl_statement 14 | ertl_st_get_hdw: register → Register → label → ertl_statement 15 | ertl_st_set_hdw: Register → register → label → ertl_statement 16 | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement 17 | ertl_st_new_frame: label → ertl_statement 18 | ertl_st_del_frame: label → ertl_statement 19 | ertl_st_frame_size: register → label → ertl_statement 20 | ertl_st_pop: register → label → ertl_statement 21 | ertl_st_push: register → label → ertl_statement 22 | ertl_st_addr: register → register → ident → label → ertl_statement 23 (* XXX: changed from O'Caml 24 | ertl_st_addr_h: register → ident → label → ertl_statement 25 | ertl_st_addr_l: register → ident → label → ertl_statement 26 *) 27 | ertl_st_int: register → Byte → label → ertl_statement 28 | ertl_st_move: register → register → label → ertl_statement 29 | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement 30 (* XXX: changed from O'Caml 31 | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement 32 | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement 33 *) 34 | ertl_st_op1: Op1 → register → register → label → ertl_statement 35 | ertl_st_op2: Op2 → register → register → register → label → ertl_statement 36 | ertl_st_clear_carry: label → ertl_statement 37 | ertl_st_set_carry: label → ertl_statement 38 | ertl_st_load: register → register → register → label → ertl_statement 39 | ertl_st_store: register → register → register → label → ertl_statement 40 | ertl_st_call_id: ident → nat → label → ertl_statement 41 | ertl_st_cond: register → label → label → ertl_statement 42 | ertl_st_return: ertl_statement. 11 inductive move_registers: Type[0] ≝ 12 | pseudo: register → move_registers 13 | hardware: Register → move_registers. 14 15 inductive ertl_statement_extension: Type[0] ≝ 16 | ertl_st_ext_new_frame: label → ertl_statement_extension 17 | ertl_st_ext_del_frame: label → ertl_statement_extension 18 | ertl_st_ext_frame_size: register → label → ertl_statement_extension. 43 19 44 definition ertl_statement_graph ≝ graph ertl_statement. 20 definition ertl_params: params ≝ 21 mk_params 22 register register register register 23 (move_registers × move_registers) register 24 ertl_statement_extension unit (list register) nat. 45 25 46 record ertl_internal_function: Type[0] ≝ 26 definition ertl_statement ≝ joint_statement ertl_params. 27 28 definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals). 29 30 record ertl_internal_function (globals: list ident): Type[0] ≝ 47 31 { 48 32 ertl_if_luniverse: universe LabelTag; … … 51 35 ertl_if_locals: registers; 52 36 ertl_if_stacksize: nat; 53 ertl_if_graph: ertl_statement_graph ;37 ertl_if_graph: ertl_statement_graph globals; 54 38 ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?; 55 39 ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ? 56 40 }. 57 41 58 definition ertl_function ≝ fundef ertl_internal_function. 42 definition set_luniverse ≝ 43 λglobals : list ident. 44 λint_fun : ertl_internal_function globals. 45 λluniverse: universe LabelTag. 46 let runiverse ≝ ertl_if_runiverse globals int_fun in 47 let params ≝ ertl_if_params globals int_fun in 48 let locals ≝ ertl_if_locals globals int_fun in 49 let stacksize ≝ ertl_if_stacksize globals int_fun in 50 let graph ≝ ertl_if_graph globals int_fun in 51 let entry ≝ ertl_if_entry globals int_fun in 52 let exit ≝ ertl_if_exit globals int_fun in 53 mk_ertl_internal_function globals 54 luniverse runiverse params locals 55 stacksize graph entry exit. 56 57 definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals). 59 58 60 record ertl_program : Type[0] ≝59 record ertl_program (globals: list ident): Type[0] ≝ 61 60 { 62 61 ertl_pr_vars: list (ident × nat); 63 ertl_pr_funcs: list (ident × ertl_function);62 ertl_pr_funcs: list (ident × (ertl_function globals)); 64 63 ertl_pr_main: option ident 65 64 }. 65 66 67 (* XXX: changed from O'Caml 68 | ertl_st_addr_h: register → ident → label → ertl_statement 69 | ertl_st_addr_l: register → ident → label → ertl_statement 70 *) 71 72 (* XXX: changed from O'Caml 73 | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement 74 | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement 75 *) -
Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma
r1153 r1197 1 1 include "ERTL/ERTL.ma". 2 include "ERTL/ERTLToLTLI.ma".3 2 include "LTL/LTL.ma". 4 3 include "ERTL/spill.ma". 4 include "ERTL/build.ma". 5 include "utilities/Interference.ma". 6 include "ASM/Arithmetic.ma". 7 8 (* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *) 9 10 inductive decision: Type[0] ≝ 11 | decision_spill: Byte → decision 12 | decision_colour: Register → decision. 13 14 definition interference_lookup ≝ 15 λglobals. 16 λint_fun. 17 λr. 18 let 〈liveafter, graph〉 ≝ build globals int_fun in 19 let lkup ≝ ig_lookup graph r in 20 vm_find lkup colour_colouring. 21 22 definition lookup: register → decision ≝ 23 λr. 24 match ? r with 25 [ colour_spill 26 27 axiom lookup: register → decision. 28 29 definition fresh_label ≝ 30 λglobals: list ident. 31 λluniv. 32 fresh LabelTag luniv. 33 34 definition add_graph ≝ 35 λglobals. 36 λlabel. 37 λstmt: ltl_statement globals. 38 λgraph: ltl_statement_graph globals. 39 add LabelTag ? graph label stmt. 40 41 definition generate ≝ 42 λglobals: list ident. 43 λluniv. 44 λgraph: ltl_statement_graph globals. 45 λstmt: ltl_statement globals. 46 let 〈l, luniv〉 ≝ fresh_label globals luniv in 47 let graph ≝ add_graph globals l stmt graph in 48 〈l, graph, luniv〉. 49 50 definition num_locals ≝ 51 λglobals. 52 λint_fun. 53 colour_locals + (ertl_if_stacksize globals int_fun). 54 55 definition stacksize ≝ 56 λglobals. 57 λint_fun. 58 colour_locals + (ertl_if_stacksize globals int_fun). 59 60 definition adjust_off ≝ 61 λglobals. 62 λint_fun. 63 λoff. 64 let 〈ignore, int_off〉 ≝ half_add ? int_size off in 65 let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in 66 sub. 67 68 definition get_stack: 69 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → 70 ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) 71 ≝ 72 λglobals: list ident. 73 λint_fun. 74 λgraph: graph (ltl_statement (globals)). 75 λr. 76 λoff. 77 λl. 78 let off ≝ adjust_off globals int_fun off in 79 let luniv ≝ ertl_if_luniverse globals int_fun in 80 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in 81 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in 82 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 83 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in 84 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in 85 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 86 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in 87 〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉. 88 89 definition set_stack: 90 ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte 91 → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag)) ≝ 92 λglobals: list ident. 93 λint_fun. 94 λgraph: graph (ltl_statement (globals)). 95 λoff. 96 λr. 97 λl. 98 let off ≝ adjust_off globals int_fun off in 99 let luniv ≝ ertl_if_luniverse globals int_fun in 100 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in 101 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in 102 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 103 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in 104 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in 105 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 106 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in 107 〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉. 108 109 definition write: 110 ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label → 111 ? ≝ 112 λglobals: list ident. 113 λint_fun. 114 λgraph. 115 λr. 116 λl. 117 match lookup r with 118 [ decision_spill off ⇒ 119 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in 120 let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in 121 〈RegisterSST, l, graph, luniv〉 122 | decision_colour hwr ⇒ 123 let luniv ≝ ertl_if_luniverse globals int_fun in 124 〈hwr, l, graph, luniv〉 125 ]. 126 127 definition read: 128 ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register 129 → (Register → ltl_statement globals) → ? ≝ 130 λglobals. 131 λint_fun. 132 λgraph. 133 λr. 134 λstmt. 135 match lookup r with 136 [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr) 137 | decision_spill off ⇒ 138 let temphwr ≝ RegisterSST in 139 let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in 140 let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in 141 generate globals luniv graph stmt 142 ]. 143 144 definition move ≝ 145 λglobals: list ident. 146 λint_fun. 147 λgraph: graph (ltl_statement globals). 148 λdest: decision. 149 λsrc: decision. 150 λl: label. 151 match dest with 152 [ decision_colour dest_hwr ⇒ 153 match src with 154 [ decision_colour src_hwr ⇒ 155 let luniv ≝ ertl_if_luniverse globals int_fun in 156 if eq_Register dest_hwr src_hwr then 157 〈joint_st_goto … globals l, graph, luniv〉 158 else 159 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in 160 〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉 161 | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l 162 ] 163 | decision_spill dest_off ⇒ 164 match src with 165 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l 166 | decision_spill src_off ⇒ 167 let luniv ≝ ertl_if_luniverse globals int_fun in 168 if eq_bv ? dest_off src_off then 169 〈joint_st_goto … globals l, graph, luniv〉 170 else 171 let temp_hwr ≝ RegisterSST in 172 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in 173 let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in 174 get_stack globals int_fun graph temp_hwr src_off l 175 ] 176 ]. 177 178 definition newframe ≝ 179 λglobals: list ident. 180 λint_fun: ertl_internal_function globals. 181 λgraph: ltl_statement_graph globals. 182 λl: label. 183 if eq_nat (stacksize globals int_fun) 0 then 184 〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉 185 else 186 let luniv ≝ ertl_if_luniverse globals int_fun in 187 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 188 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in 189 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in 190 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in 191 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in 192 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in 193 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in 194 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in 195 〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉. 196 197 definition delframe ≝ 198 λglobals. 199 λint_fun. 200 λgraph: graph (ltl_statement globals). 201 λl. 202 if eq_nat (stacksize globals int_fun) 0 then 203 〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉 204 else 205 let luniv ≝ ertl_if_luniverse globals int_fun in 206 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 207 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in 208 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in 209 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in 210 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in 211 〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉. 212 213 definition translate_statement ≝ 214 λglobals: list ident. 215 λint_fun. 216 λgraph: ltl_statement_graph globals. 217 λstmt: ertl_statement globals. 218 match stmt with 219 [ joint_st_sequential seq l ⇒ 220 let luniv ≝ ertl_if_luniverse globals int_fun in 221 match seq with 222 [ joint_instr_comment c ⇒ 223 〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉 224 | joint_instr_cost_label cost_lbl ⇒ 225 〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉 226 | joint_instr_pop r ⇒ 227 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 228 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 229 〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉 230 | joint_instr_push r ⇒ 231 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in 232 let int_fun ≝ set_luniverse globals int_fun luniv in 233 let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 234 〈joint_st_goto ltl_params globals l, graph, luniv〉 235 | joint_instr_cond srcr lbl_true ⇒ 236 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in 237 let int_fun ≝ set_luniverse globals int_fun luniv in 238 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 239 〈joint_st_goto ltl_params globals l, graph, luniv〉 240 | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉 241 | joint_instr_store addr1 addr2 srcr ⇒ 242 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in 243 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in 244 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 245 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 246 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 247 let int_fun ≝ set_luniverse globals int_fun luniv in 248 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 249 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 250 let int_fun ≝ set_luniverse globals int_fun luniv in 251 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 252 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in 253 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 254 〈joint_st_goto ltl_params globals l, graph, luniv〉 255 | joint_instr_load destr addr1 addr2 ⇒ 256 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in 257 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 258 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in 259 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 260 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 261 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 262 let int_fun ≝ set_luniverse globals int_fun luniv in 263 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 264 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 265 let int_fun ≝ set_luniverse globals int_fun luniv in 266 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 267 〈joint_st_goto ltl_params globals l, graph, luniv〉 268 | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉 269 | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉 270 | joint_instr_op2 op2 destr srcr ⇒ 271 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in 272 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 273 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in 274 let luniv ≝ set_luniverse globals int_fun luniv in 275 let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 276 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 277 let luniv ≝ set_luniverse globals int_fun luniv in 278 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 279 〈joint_st_goto ltl_params globals l, graph, luniv〉 280 | joint_instr_op1 op1 acc_a ⇒ 281 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in 282 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 283 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in 284 let int_fun ≝ set_luniverse globals int_fun luniv in 285 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 286 〈joint_st_goto ltl_params globals l, graph, luniv〉 287 | joint_instr_int r i ⇒ 288 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 289 〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉 290 | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒ 291 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in 292 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 293 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 294 let luniv ≝ set_luniverse globals int_fun luniv in 295 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 296 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 297 let luniv ≝ set_luniverse globals int_fun luniv in 298 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 299 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in 300 let luniv ≝ set_luniverse globals int_fun luniv in 301 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in 302 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 303 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in 304 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 305 let luniv ≝ set_luniverse globals int_fun luniv in 306 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 307 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 308 let luniv ≝ set_luniverse globals int_fun luniv in 309 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 310 〈joint_st_goto ltl_params globals l, graph, luniv〉 311 | joint_instr_move pair_regs ⇒ 312 let regl ≝ \fst pair_regs in 313 let regr ≝ \snd pair_regs in 314 match regl with 315 [ pseudo p1 ⇒ 316 match regr with 317 [ pseudo p2 ⇒ move globals int_fun graph (lookup p1) (lookup p2) l 318 | hardware h ⇒ move globals int_fun graph (lookup p1) (decision_colour h) l 319 ] 320 | hardware h1 ⇒ 321 match regr with 322 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (lookup p) l 323 | hardware h2 ⇒ 324 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in 325 〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc h2)) l, graph, luniv〉 326 ] 327 ] 328 | joint_instr_address lbl prf dpl dph ⇒ 329 let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in 330 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in 331 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in 332 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in 333 let int_fun ≝ set_luniverse globals int_fun luniv in 334 let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in 335 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in 336 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in 337 〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉 338 ] 339 | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉 340 | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉 341 | joint_st_extension ext ⇒ 342 match ext with 343 [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l 344 | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l 345 | ertl_st_ext_frame_size r l ⇒ 346 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 347 〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉 348 ] 349 ]. 5 350 6 351 definition translate_internal ≝ 352 λglobals: list ident. 7 353 λf. 8 354 λint_fun: ertl_internal_function. 9 10 let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in 11 12 let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in 13 14 let generate stmt = 15 let l = fresh_label () in 16 add_graph l stmt ; 17 l in 18 19 (* Build an interference graph for this function, and color 20 it. Define a function that allows consulting the coloring. *) 21 22 let module G = struct 23 let liveafter, graph = Build.build int_fun 24 let uses = Uses.examine_internal int_fun 25 let verbose = false 26 let () = 27 if verbose then 28 Printf.printf "Starting hardware register allocation for %s.\n" f 29 end in 30 31 let module C = Coloring.Color (G) in 32 33 let lookup r = 34 Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring 35 in 36 37 (* Restrict the interference graph to concern spilled vertices only, 38 and color it again, this time using stack slots as colors. *) 39 40 let module H = struct 41 let graph = Interference.droph (Interference.restrict G.graph (fun v -> 42 match Interference.Vertex.Map.find v C.coloring with 43 | Coloring.Spill -> 44 true 45 | Coloring.Color _ -> 46 false 47 )) 48 let verbose = false 49 let () = 50 if verbose then 51 Printf.printf "Starting stack slot allocation for %s.\n" f 52 end in 53 54 let module S = Spill.Color (H) in 55 56 (* Define a new function that consults both colorings at once. *) 57 58 let lookup r = 355 let lookup ≝ λr. 59 356 match lookup r with 60 | Coloring.Spill ->357 | colour_spill -> 61 358 ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring) 62 | Coloring.Color color ->359 | colour_colour color -> 63 360 ERTLToLTLI.Color color 64 361 in 65 66 (* We are now ready to instantiate the functor that deals with the 67 translation of instructions. The reason why we make this a 68 separate functor is purely pedagogical. Smaller modules are 69 easier to understand. *) 70 71 (* We add the additional stack size required for spilled register to the stack 72 size previously required for the function: this is the final stack size 73 required for the locals. *) 74 75 let locals = S.locals + int_fun.ERTL.f_stacksize in 76 77 (* The full stack size is then the size of the locals in the stack plus the 78 size of the formal parameters of the function. *) 79 80 let stacksize = int_fun.ERTL.f_params + locals in 81 82 let module I = ERTLToLTLI.Make (struct 83 let lookup = lookup 84 let generate = generate 85 let fresh_label = fresh_label 86 let add_graph = add_graph 87 let locals = locals 88 let stacksize = stacksize 89 end) in 90 91 (* Translate the instructions in the existing control flow graph. 92 Pure instructions whose destination pseudo-register is dead are 93 eliminated on the fly. *) 362 let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in 363 let stacksize ≝ (ertl_if_params int_fun) + locals in 364 mk_ltl_internal_function 365 globals 366 (ertl_if_luniverse int_fun) 367 (ertl_if_runiverse int_fun) 368 stacksize. 94 369 95 370 let () = … … 106 381 in 107 382 108 (* Build a [LTL] function. *)109 110 {111 LTL.f_luniverse = int_fun.ERTL.f_luniverse;112 LTL.f_stacksize = stacksize ;113 LTL.f_entry = int_fun.ERTL.f_entry;114 LTL.f_exit = int_fun.ERTL.f_exit;115 LTL.f_graph = !graph116 }117 118 383 definition translate_funct ≝ 119 384 λname_def. -
Deliverables/D3.3/id-lookup-branch/ERTL/build.ma
r1153 r1197 3 3 4 4 definition build ≝ 5 λint_fun: ertl_internal_function. 6 let liveafter ≝ analyse int_fun in 7 let graph ≝ ig_create (ertl_if_locals int_fun) in 8 let graph ≝ ig_mkiph graph (ertl_if_locals int_fun) forbidden_registers in 5 λglobals: list ident. 6 λint_fun: ertl_internal_function globals. 7 let liveafter ≝ analyse globals int_fun in 8 let graph ≝ ig_create (ertl_if_locals globals int_fun) in 9 let graph ≝ ig_mkiph graph (ertl_if_locals globals int_fun) RegistersForbidden in 9 10 let graph ≝ 10 11 foldi ? ? ? (λlabel. λstmt. λgraph. 11 12 let live ≝ liveafter label in 12 match eliminable live stmt with13 match eliminable globals live stmt with 13 14 [ Some _ ⇒ graph 14 15 | None ⇒ 15 let defined ≝ defined stmt in16 let defined ≝ defined globals stmt in 16 17 let exceptions ≝ 17 18 match stmt with 18 [ ertl_st_move _ sr _ ⇒ lattice_psingleton sr 19 | ertl_st_set_hdw _ sr _ ⇒ lattice_psingleton sr 20 | ertl_st_get_hdw _ sr _ ⇒ lattice_hsingleton sr 21 | _ ⇒ ? 19 [ joint_st_sequential seq l ⇒ 20 match seq with 21 [ joint_instr_move pair_reg ⇒ 22 let reg_r ≝ \snd pair_reg in 23 match reg_r with 24 [ hardware hw ⇒ lattice_hsingleton hw 25 | pseudo ps ⇒ lattice_psingleton ps 26 ] 27 | _ ⇒ ? 28 ] 29 | _ ⇒ ? 22 30 ] 23 31 in … … 25 33 let graph ≝ 26 34 match stmt with 27 [ ertl_st_move r1 r2 _ ⇒ ig_mkppp graph r1 r2 28 | ertl_st_get_hdw r hwr _ ⇒ ig_mkpph graph r hwr 29 | ertl_st_set_hdw hwr r _ ⇒ ig_mkpph graph r hwr 30 | _ ⇒ graph 35 [ joint_st_sequential seq l ⇒ 36 match seq with 37 [ joint_instr_move pair_reg ⇒ 38 let reg_l ≝ \fst pair_reg in 39 let reg_r ≝ \snd pair_reg in 40 match reg_l with 41 [ pseudo ps1 ⇒ 42 match reg_r with 43 [ pseudo ps2 ⇒ ig_mkppp graph ps1 ps2 44 | hardware hw ⇒ ig_mkpph graph ps1 hw 45 ] 46 | hardware hw1 ⇒ 47 match reg_r with 48 [ pseudo ps ⇒ ig_mkpph graph ps hw1 49 | hardware hw2 ⇒ graph 50 ] 51 ] 52 | _ ⇒ graph 53 ] 54 | _ ⇒ graph 31 55 ] 32 56 in graph 33 ]) (ertl_if_graph int_fun) graph57 ]) (ertl_if_graph globals int_fun) graph 34 58 in 35 59 〈liveafter, graph〉. -
Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma
r1153 r1197 35 35 36 36 definition statement_successors ≝ 37 λs: ertl_statement. 37 λglobals: list ident. 38 λs: ertl_statement globals. 38 39 match s with 39 [ ertl_st_return ⇒ [ ] 40 | ertl_st_skip l ⇒ [ l ] 41 | ertl_st_comment c l ⇒ [ l ] 42 | ertl_st_cost c l ⇒ [ l ] 43 | ertl_st_set_hdw _ _ l ⇒ [ l ] 44 | ertl_st_get_hdw _ _ l ⇒ [ l ] 45 | ertl_st_hdw_to_hdw _ _ l ⇒ [ l ] 46 | ertl_st_new_frame l ⇒ [ l ] 47 | ertl_st_del_frame l ⇒ [ l ] 48 | ertl_st_frame_size _ l ⇒ [ l ] 49 | ertl_st_push _ l ⇒ [ l ] 50 | ertl_st_pop _ l ⇒ [ l ] 51 | ertl_st_addr _ _ _ l ⇒ [ l ] 52 | ertl_st_int _ _ l ⇒ [ l ] 53 | ertl_st_move _ _ l ⇒ [ l ] 54 | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ] 55 | ertl_st_op1 _ _ _ l ⇒ [ l ] 56 | ertl_st_op2 _ _ _ _ l ⇒ [ l ] 57 | ertl_st_clear_carry l ⇒ [ l ] 58 | ertl_st_set_carry l ⇒ [ l ] 59 | ertl_st_load _ _ _ l ⇒ [ l ] 60 | ertl_st_store _ _ _ l ⇒ [ l ] 61 | ertl_st_call_id _ _ l ⇒ [ l ] 62 | ertl_st_cond _ l1 l2 ⇒ 63 list_set_add ? (eq_identifier ?) l1 [ l2 ] 40 [ joint_st_sequential seq l ⇒ 41 match seq with 42 [ joint_instr_cond acc_a_reg lbl_true ⇒ 43 list_set_add ? (eq_identifier ?) lbl_true [ l ] 44 | _ ⇒ [ l ] 45 ] 46 | joint_st_extension ext ⇒ 47 match ext with 48 [ ertl_st_ext_new_frame l ⇒ [ l ] 49 | ertl_st_ext_del_frame l ⇒ [ l ] 50 | ertl_st_ext_frame_size r l ⇒ [ l ] 51 ] 52 | joint_st_goto l ⇒ [ l ] 53 | joint_st_return ⇒ [ ] 64 54 ]. 65 55 … … 122 112 lattice_is_maximal. 123 113 124 definition defined: ertl_statement → register_lattice ≝ 125 λs. 114 definition defined ≝ 115 λglobals: list ident. 116 λs: ertl_statement globals. 126 117 match s with 127 [ ertl_st_skip _ ⇒ lattice_bottom 128 | ertl_st_comment _ _ ⇒ lattice_bottom 129 | ertl_st_cost _ _ ⇒ lattice_bottom 130 | ertl_st_push _ _⇒ lattice_bottom 131 | ertl_st_store _ _ _ _ ⇒ lattice_bottom 132 | ertl_st_cond _ _ _ ⇒ lattice_bottom 133 | ertl_st_return ⇒ lattice_bottom 134 | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry 135 | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry 136 | ertl_st_op2 op2 r _ _ _ ⇒ 137 match op2 with 138 [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 139 | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 140 | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 141 | _ ⇒ lattice_psingleton r 142 ] 143 | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r 144 | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r 145 | ertl_st_frame_size r _ ⇒ lattice_psingleton r 146 | ertl_st_pop r _ ⇒ lattice_psingleton r 147 | ertl_st_int r _ _ ⇒ lattice_psingleton r 148 | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 149 | ertl_st_move r _ _ ⇒ lattice_psingleton r 150 (* XXX: change from o'caml *) 151 | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 152 | ertl_st_load r _ _ _ ⇒ lattice_psingleton r 153 | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r 154 | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r 155 (* Potentially destroys all caller-save hardware registers. *) 156 | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉 157 | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 158 | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 118 [ joint_st_sequential seq l ⇒ 119 match seq with 120 [ joint_instr_op2 op2 r _ ⇒ 121 match op2 with 122 [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 123 | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 124 | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 125 | _ ⇒ lattice_psingleton r 126 ] 127 | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry 128 | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry 129 | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 130 | joint_instr_op1 op1 r ⇒ lattice_psingleton r 131 | joint_instr_pop r ⇒ lattice_psingleton r 132 | joint_instr_int r _ ⇒ lattice_psingleton r 133 | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 134 | joint_instr_load r _ _ ⇒ lattice_psingleton r 135 (* Potentially destroys all caller-save hardware registers. *) 136 | joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉 137 | joint_instr_comment c ⇒ lattice_bottom 138 | joint_instr_cond r lbl_true ⇒ lattice_bottom 139 | joint_instr_store acc_a dpl dph ⇒ lattice_bottom 140 | joint_instr_cost_label clabel ⇒ lattice_bottom 141 | joint_instr_push r ⇒ lattice_bottom 142 | joint_instr_move pair_reg ⇒ 143 (* first register relevant only *) 144 let r1 ≝ \fst pair_reg in 145 match r1 with 146 [ pseudo p ⇒ lattice_psingleton p 147 | hardware h ⇒ lattice_hsingleton h 148 ] 149 ] 150 | joint_st_return ⇒ lattice_bottom 151 | joint_st_extension ext ⇒ 152 match ext with 153 [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 154 | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 155 | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r 156 ] 157 | joint_st_goto l ⇒ lattice_bottom 159 158 ]. 160 159 … … 169 168 definition ret_regs ≝ list_set_of_list RegisterRets. 170 169 171 definition used: ertl_statement → register_lattice ≝ 172 λstmt. 173 match stmt with 174 [ ertl_st_skip _ ⇒ lattice_bottom 175 | ertl_st_cost _ _ ⇒ lattice_bottom 176 | ertl_st_comment _ _ ⇒ lattice_bottom 177 | ertl_st_frame_size _ _ ⇒ lattice_bottom 178 | ertl_st_pop _ _ ⇒ lattice_bottom 179 | ertl_st_addr _ _ _ _ ⇒ lattice_bottom 180 | ertl_st_int _ _ _ ⇒ lattice_bottom 181 | ertl_st_clear_carry _ ⇒ lattice_bottom 182 | ertl_st_set_carry _ ⇒ lattice_bottom 170 definition used ≝ 171 λglobals: list ident. 172 λs: ertl_statement globals. 173 match s with 174 [ joint_st_sequential seq l ⇒ 175 match seq with 176 [ joint_instr_op2 op2 acc_a r ⇒ 177 match op2 with 178 [ Addc ⇒ 179 lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry) 180 | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r) 181 ] 182 | joint_instr_clear_carry ⇒ lattice_bottom 183 | joint_instr_set_carry ⇒ lattice_bottom 184 (* acc_a and acc_b *) 185 | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 186 | joint_instr_op1 op1 r ⇒ lattice_psingleton r 187 | joint_instr_pop r ⇒ lattice_bottom 188 | joint_instr_int r _ ⇒ lattice_bottom 189 | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom 190 | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph) 183 191 (* Reads the hardware registers that are used to pass parameters. *) 184 | ertl_st_call_id _ nparams _ ⇒ 185 〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉 186 | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r 187 | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r 188 | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r 189 | ertl_st_push r _ ⇒ lattice_psingleton r 190 | ertl_st_move _ r _ ⇒ lattice_psingleton r 191 | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r 192 | ertl_st_cond r _ _ ⇒ lattice_psingleton r 193 | ertl_st_op2 op2 _ r1 r2 _ ⇒ 194 match op2 with 195 [ Addc ⇒ 196 lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry) 197 | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 198 ] 199 | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2) 200 | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 201 | ertl_st_store r1 r2 r3 _ ⇒ 202 lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3) 203 | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 204 | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 205 | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 206 ]. 207 208 definition eliminable: register_lattice → ertl_statement → option label ≝ 209 λl. 210 λstmt. 192 | joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉 193 | joint_instr_comment c ⇒ lattice_bottom 194 | joint_instr_cond r lbl_true ⇒ lattice_psingleton r 195 | joint_instr_store acc_a dpl dph ⇒ 196 lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph) 197 | joint_instr_cost_label clabel ⇒ lattice_bottom 198 | joint_instr_push r ⇒ lattice_psingleton r 199 | joint_instr_move pair_reg ⇒ 200 (* only second reg in pair relevant *) 201 let r2 ≝ \snd pair_reg in 202 match r2 with 203 [ pseudo p ⇒ lattice_psingleton p 204 | hardware h ⇒ lattice_hsingleton h 205 ] 206 ] 207 | joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 208 | joint_st_goto l ⇒ lattice_bottom 209 | joint_st_extension ext ⇒ 210 match ext with 211 [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 212 | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 213 | ertl_st_ext_frame_size r l ⇒ lattice_bottom 214 ] 215 ]. 216 217 definition eliminable ≝ 218 λglobals: list ident. 219 λl: register_lattice. 220 λs: ertl_statement globals. 211 221 let 〈pliveafter, hliveafter〉 ≝ l in 212 match stmt with 213 [ ertl_st_skip _ ⇒ None ? 214 | ertl_st_comment _ _ ⇒ None ? 215 | ertl_st_cost _ _ ⇒ None ? 216 | ertl_st_new_frame _ ⇒ None ? 217 | ertl_st_del_frame _ ⇒ None ? 218 | ertl_st_pop _ _ ⇒ None ? 219 | ertl_st_push _ _ ⇒ None ? 220 | ertl_st_clear_carry _ ⇒ None ? 221 | ertl_st_set_carry _ ⇒ None ? 222 | ertl_st_store _ _ _ _ ⇒ None ? 223 | ertl_st_call_id _ _ _ ⇒ None ? 224 | ertl_st_cond _ _ _ ⇒ None ? 225 | ertl_st_return ⇒ None ? 226 | ertl_st_get_hdw r _ l ⇒ 227 if list_set_member register (eq_identifier ?) r pliveafter ∨ 228 list_set_member Register eq_Register RegisterCarry hliveafter then 229 None ? 230 else 231 Some ? l 232 | ertl_st_frame_size r l ⇒ 233 if list_set_member register (eq_identifier ?) r pliveafter ∨ 234 list_set_member Register eq_Register RegisterCarry hliveafter then 235 None ? 236 else 237 Some ? l 238 | ertl_st_int r _ l ⇒ 239 if list_set_member register (eq_identifier ?) r pliveafter ∨ 240 list_set_member Register eq_Register RegisterCarry hliveafter then 241 None ? 242 else 243 Some ? l 244 | ertl_st_addr r1 r2 _ l ⇒ 245 if list_set_member register (eq_identifier ?) r1 pliveafter ∨ 246 list_set_member register (eq_identifier ?) r2 pliveafter ∨ 247 list_set_member Register eq_Register RegisterCarry hliveafter then 248 None ? 249 else 250 Some ? l 251 | ertl_st_move r _ l ⇒ 252 if list_set_member register (eq_identifier ?) r pliveafter ∨ 253 list_set_member Register eq_Register RegisterCarry hliveafter then 254 None ? 255 else 256 Some ? l 257 | ertl_st_opaccs _ d1 d2 _ _ l ⇒ 258 if list_set_member register (eq_identifier ?) d1 pliveafter ∨ 259 list_set_member register (eq_identifier ?) d2 pliveafter ∨ 260 list_set_member Register eq_Register RegisterCarry hliveafter then 261 None ? 262 else 263 Some ? l 264 | ertl_st_op1 _ r _ l ⇒ 265 if list_set_member register (eq_identifier ?) r pliveafter ∨ 266 list_set_member Register eq_Register RegisterCarry hliveafter then 267 None ? 268 else 269 Some ? l 270 | ertl_st_op2 _ r _ _ l ⇒ 271 if list_set_member register (eq_identifier ?) r pliveafter ∨ 272 list_set_member Register eq_Register RegisterCarry hliveafter then 273 None ? 274 else 275 Some ? l 276 | ertl_st_load r _ _ l ⇒ 277 if list_set_member register (eq_identifier ?) r pliveafter ∨ 278 list_set_member Register eq_Register RegisterCarry hliveafter then 279 None ? 280 else 281 Some ? l 282 | ertl_st_set_hdw r _ l ⇒ 283 if list_set_member Register eq_Register r hliveafter then 284 None ? 285 else 286 Some ? l 287 | ertl_st_hdw_to_hdw r _ l ⇒ 288 if list_set_member Register eq_Register r hliveafter then 289 None ? 290 else 291 Some ? l 292 ]. 293 294 definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝ 222 match s with 223 [ joint_st_sequential seq l ⇒ 224 match seq with 225 [ joint_instr_op2 op2 acc_a r ⇒ 226 if list_set_member register (eq_identifier ?) acc_a pliveafter ∨ 227 list_set_member Register eq_Register RegisterCarry hliveafter then 228 None ? 229 else 230 Some ? l 231 | joint_instr_clear_carry ⇒ None ? 232 | joint_instr_set_carry ⇒ None ? 233 | joint_instr_opaccs opaccs r1 r2 ⇒ 234 if list_set_member register (eq_identifier ?) r1 pliveafter ∨ 235 list_set_member register (eq_identifier ?) r2 pliveafter ∨ 236 list_set_member Register eq_Register RegisterCarry hliveafter then 237 None ? 238 else 239 Some ? l 240 | joint_instr_op1 op1 r ⇒ 241 if list_set_member register (eq_identifier ?) r pliveafter ∨ 242 list_set_member Register eq_Register RegisterCarry hliveafter then 243 None ? 244 else 245 Some ? l 246 | joint_instr_pop r ⇒ None ? 247 | joint_instr_int r _ ⇒ 248 if list_set_member register (eq_identifier ?) r pliveafter ∨ 249 list_set_member Register eq_Register RegisterCarry hliveafter then 250 None ? 251 else 252 Some ? l 253 | joint_instr_address _ _ r1 r2 ⇒ 254 if list_set_member register (eq_identifier ?) r1 pliveafter ∨ 255 list_set_member register (eq_identifier ?) r2 pliveafter ∨ 256 list_set_member Register eq_Register RegisterCarry hliveafter then 257 None ? 258 else 259 Some ? l 260 | joint_instr_load acc_a dpl dph ⇒ 261 if list_set_member register (eq_identifier ?) acc_a pliveafter ∨ 262 list_set_member Register eq_Register RegisterCarry hliveafter then 263 None ? 264 else 265 Some ? l 266 | joint_instr_call_id _ nparams ⇒ None ? 267 | joint_instr_comment c ⇒ None ? 268 | joint_instr_cond r lbl_true ⇒ None ? 269 | joint_instr_store acc_a dpl dph ⇒ None ? 270 | joint_instr_cost_label clabel ⇒ None ? 271 | joint_instr_push r ⇒ None ? 272 | joint_instr_move pair_reg ⇒ 273 let r1 ≝ \fst pair_reg in 274 let r2 ≝ \snd pair_reg in 275 match r1 with 276 [ pseudo p1 ⇒ 277 if list_set_member register (eq_identifier ?) p1 pliveafter ∨ 278 list_set_member Register eq_Register RegisterCarry hliveafter then 279 None ? 280 else 281 Some ? l 282 | hardware h1 ⇒ 283 if list_set_member Register eq_Register h1 hliveafter then 284 None ? 285 else 286 Some ? l 287 ] 288 ] 289 | joint_st_goto l ⇒ None ? 290 | joint_st_return ⇒ None ? 291 | joint_st_extension ext ⇒ 292 match ext with 293 [ ertl_st_ext_new_frame l ⇒ None ? 294 | ertl_st_ext_del_frame l ⇒ None ? 295 | ertl_st_ext_frame_size r l ⇒ 296 if list_set_member register (eq_identifier ?) r pliveafter ∨ 297 list_set_member Register eq_Register RegisterCarry hliveafter then 298 None ? 299 else 300 Some ? l 301 ] 302 ]. 303 304 definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝ 305 λglobals. 295 306 λstmt. 296 307 λliveafter. 297 match eliminable liveafter stmt with298 [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (usedstmt)308 match eliminable globals liveafter stmt with 309 [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt) 299 310 | Some l ⇒ liveafter 300 311 ]. … … 307 318 308 319 definition livebefore ≝ 320 λglobals: list ident. 309 321 λint_fun. 310 322 λlabel. 311 323 λliveafter: valuation. 312 match lookup ? ? (ertl_if_graph int_fun) label with324 match lookup ? ? (ertl_if_graph globals int_fun) label with 313 325 [ None ⇒ ? 314 | Some stmt ⇒ statement_semantics stmt (liveafter label)326 | Some stmt ⇒ statement_semantics globals stmt (liveafter label) 315 327 ]. 316 328 cases not_implemented (* XXX *) … … 318 330 319 331 definition liveafter ≝ 332 λglobals. 320 333 λint_fun. 321 334 λlivebefore. 322 335 λlabel. 323 336 λliveafter: valuation. 324 match lookup ? ? (ertl_if_graphint_fun) label with337 match lookup … (ertl_if_graph globals int_fun) label with 325 338 [ None ⇒ ? 326 | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.339 | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice. 327 340 lattice_join (livebefore successor liveafter) accu) 328 lattice_bottom (statement_successors stmt)341 lattice_bottom (statement_successors globals stmt) 329 342 ]. 330 343 cases not_implemented (* XXX *) 331 344 qed. 332 345 333 definition analyse: ertl_internal_function → valuation ≝ 346 definition analyse ≝ 347 λglobals. 334 348 λint_fun. 335 fix_lfp (liveafter int_fun (livebeforeint_fun)).349 fix_lfp (liveafter globals int_fun (livebefore globals int_fun)). -
Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma
r1153 r1197 21 21 (* CSC: ???????????? *) 22 22 axiom smerge: val → val → res val. 23 (*24 23 (* CSC: ???????????? In OCaml: IntValue.Int32.merge 25 24 Note also that the translation can fail; so it should be a res int! *) 26 25 axiom smerge2: list val → int. 27 *)28 26 (* CSC: I have a byte, I need a value, but it is complex to do so *) 29 27 axiom val_of_Byte: Byte → val. 30 28 axiom Byte_of_val: val → res Byte. 29 axiom val_of_nat: nat → val. 31 30 (* Map from the front-end memory model to the back-end memory model *) 32 31 axiom represent_block: block → val × val. … … 38 37 axiom val_of_address: address → val. (* CSC: only to shift the sp *) 39 38 axiom address_of_val: val → address. (* CSC: only to shift the sp *) 39 axiom addr_sub: address → nat → address. 40 axiom addr_add: address → nat → address. 40 41 (* CSC: ??? *) 41 42 axiom address_of_label: mem → label → address. … … 43 44 axiom label_of_address_chunks: Byte → Byte → label. 44 45 axiom address_of_address_chunks: Byte → Byte → address. 46 axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *) 45 47 axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *) 46 48 axiom hwreg_retrieve : mRegisterMap → Register → res val. 47 49 axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap. 48 50 49 definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).51 definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)). 50 52 51 53 (* CSC: frame reduced to this *) 52 54 definition frame: Type[0] ≝ register_env val. 53 55 56 (* CSC: exit not put in the state, like in OCaml. It is constant througout 57 execution *) 54 58 record state : Type[0] ≝ 55 59 { st_frms: list frame 56 60 ; pc: address 57 61 ; sp: address 58 (* ; exit: address *)59 62 ; locals: register_env val 60 63 ; carry: val … … 134 137 135 138 (*CSC: To be implemented *) 136 axiom fetch_statement: state → res ertl_statement. 139 140 axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals). 141 axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals). 137 142 138 143 definition init_locals : list register → register_env val ≝ … … 142 147 λreg,v,locals. update RegisterTag val locals reg v. 143 148 144 (*145 axiom WrongNumberOfParameters : String.146 147 (* CSC: modified to take in input a list of registers (untyped) *)148 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝149 match rs with150 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]151 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒152 let locals' ≝ add RegisterTag val locals r v in153 params_store rst vst locals'154 ] ].155 *)156 157 149 axiom BadRegister : String. 158 150 … … 160 152 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg). 161 153 162 (*163 axiom FailedOp : String.164 *)165 154 axiom MissingSymbol : String. 166 (*167 axiom MissingStatement : String.168 axiom FailedConstant : String. *)169 155 axiom FailedLoad : String. 170 156 axiom BadFunction : String. 171 (*axiom BadJumpTable : String.172 axiom BadJumpValue : String.173 axiom FinalState : String.174 axiom ReturnMismatch : String.175 *)176 157 177 158 (*CSC: to be implemented *) … … 200 181 (λregs.OK ? (set_regs regs st)). 201 182 202 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝ 203 λge,st. 204 ! s ← fetch_statement st; 183 definition fetch_result: state → nat → res (list val) ≝ 184 λst,registersno. 185 let retregs ≝ prefix … registersno RegisterRets in 186 mmap … (λr. hwreg_retrieve (regs st) r) retregs. 187 188 definition framesize: list ident → state → res nat ≝ 189 λglobals: list ident. 190 λst. 191 (* CSC: monadic notation missing here *) 192 bind ?? (fetch_function globals st) (λf. 193 OK ? (ertl_if_stacksize globals f)). 194 195 definition get_hwsp : state → res address ≝ 196 λst. 197 (* CSC: monadic notation missing here *) 198 bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl. 199 (* CSC: monadic notation missing here *) 200 bind ?? (Byte_of_val spl) (λspl. 201 (* CSC: monadic notation missing here *) 202 bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph. 203 (* CSC: monadic notation missing here *) 204 bind ?? (Byte_of_val sph) (λsph. 205 OK ? (address_of_address_chunks spl sph))))). 206 207 definition set_hwsp : address → state → res state ≝ 208 λsp,st. 209 let 〈spl,sph〉 ≝ address_chunks_of_address sp in 210 (* CSC: monadic notation missing here *) 211 bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs. 212 (* CSC: monadic notation missing here *) 213 bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs. 214 OK ? (set_regs regs st))). 215 216 definition retrieve: state → move_registers → res val ≝ 217 λst. 218 λr. 219 match r with 220 [ pseudo src ⇒ reg_retrieve (locals st) src 221 | hardware src ⇒ hwreg_retrieve (regs st) src 222 ]. 223 224 definition store ≝ 225 λst. 226 λv. 227 λr. 228 match r with 229 [ pseudo dst ⇒ 230 ! locals ← reg_store dst v (locals st); 231 ret ? (set_locals locals st) 232 | hardware dst ⇒ 233 ! regs ← hwreg_store dst v (regs st); 234 ret ? (set_regs regs st) 235 ]. 236 237 definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝ 238 λglobals. λge,st. 239 ! s ← fetch_statement globals st; 205 240 match s with 206 [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉 207 | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉 208 | ertl_st_int dest v l ⇒ 209 ! locals ← reg_store dest (val_of_Byte v) (locals st); 210 ret ? 〈E0, goto l (set_locals locals st)〉 211 | ertl_st_load addrl addrh dst l ⇒ 212 ! vaddrh ← reg_retrieve (locals st) addrh; 213 ! vaddrl ← reg_retrieve (locals st) addrl; 214 ! vaddr ← smerge vaddrl vaddrh; 215 ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr); 216 ! locals ← reg_store dst v (locals st); 241 [ ertl_st_lift_pre pre ⇒ 242 match pre with 243 [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉 244 | joint_st_sequential seq l ⇒ 245 match seq with 246 [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉 247 | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉 248 | joint_instr_int dest v ⇒ 249 ! locals ← reg_store dest (val_of_Byte v) (locals st); 250 ret ? 〈E0, goto l (set_locals locals st)〉 251 | joint_instr_load addrl addrh dst ⇒ 252 ! vaddrh ← reg_retrieve (locals st) addrh; 253 ! vaddrl ← reg_retrieve (locals st) addrl; 254 ! vaddr ← smerge vaddrl vaddrh; 255 ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr); 256 ! locals ← reg_store dst v (locals st); 257 ret ? 〈E0, goto l (set_locals locals st)〉 258 | joint_instr_store addrl addrh src ⇒ 259 ! vaddrh ← reg_retrieve (locals st) addrh; 260 ! vaddrl ← reg_retrieve (locals st) addrl; 261 ! vaddr ← smerge vaddrl vaddrh; 262 ! v ← reg_retrieve (locals st) src; 263 ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v); 264 ret ? 〈E0, goto l (set_m m' st)〉 265 | joint_instr_cond src ltrue ⇒ 266 ! v ← reg_retrieve (locals st) src; 267 ! b ← eval_bool_of_val v; 268 ret ? 〈E0, goto (if b then ltrue else l) st〉 269 | joint_instr_address ident prf ldest hdest ⇒ 270 ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident); 271 let 〈laddr,haddr〉 ≝ represent_block addr in 272 ! locals ← reg_store ldest laddr (locals st); 273 ! locals ← reg_store hdest haddr locals; 274 ret ? 〈E0, goto l (set_locals locals st)〉 275 | joint_instr_op1 op acc_a ⇒ 276 ! v ← reg_retrieve (locals st) acc_a; 277 ! v ← Byte_of_val v; 278 let v' ≝ val_of_Byte (op1 eval op v) in 279 ! locals ← reg_store acc_a v' (locals st); 280 ret ? 〈E0, goto l (set_locals locals st)〉 281 | joint_instr_op2 op acc_a_reg dest ⇒ 282 ! v1 ← reg_retrieve (locals st) acc_a_reg; 283 ! v1 ← Byte_of_val v1; 284 ! v2 ← reg_retrieve (locals st) acc_a_reg; 285 ! v2 ← Byte_of_val v2; 286 ! carry ← eval_bool_of_val (carry st); 287 let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in 288 let v' ≝ val_of_Byte v' in 289 let carry ≝ of_bool carry in 290 ! locals ← reg_store dest v' (locals st); 291 ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉 292 | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉 293 | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉 294 | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒ 295 ! v1 ← reg_retrieve (locals st) acc_a_reg; 296 ! v1 ← Byte_of_val v1; 297 ! v2 ← reg_retrieve (locals st) acc_b_reg; 298 ! v2 ← Byte_of_val v2; 299 let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in 300 let v1' ≝ val_of_Byte v1' in 301 let v2' ≝ val_of_Byte v2' in 302 ! locals ← reg_store acc_a_reg v1' (locals st); 303 ! locals ← reg_store acc_b_reg v2' locals; 304 ret ? 〈E0, goto l (set_locals locals st)〉 305 | joint_instr_pop dst ⇒ 306 ! 〈st,v〉 ← pop st; 307 ! locals ← reg_store dst (val_of_Byte v) (locals st); 308 ret ? 〈E0, goto l (set_locals locals st)〉 309 | joint_instr_push src ⇒ 310 ! v ← reg_retrieve (locals st) src; 311 ! v ← Byte_of_val v; 312 ! st ← push st v; 313 ret ? 〈E0, goto l st〉 314 | joint_instr_move dst_src ⇒ 315 let 〈dst, src〉 ≝ dst_src in 316 ! v ← retrieve st src; 317 ! st ← store st v dst; 318 ret ? 〈E0, goto l st〉 319 (* CSC: changed, where the meat is *) 320 | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *) 321 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); 322 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); 323 match fd with 324 [ Internal fn ⇒ 325 ! st ← save_ra st l; 326 let st ≝ save_frame st in 327 let locals ≝ init_locals (ertl_if_locals globals fn) in 328 let l' ≝ ertl_if_entry globals fn in 329 ret ? 〈 E0, goto l' (set_locals locals st)〉 330 | External fn ⇒ 331 ! params ← fetch_external_args fn st; 332 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)); 333 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 334 (* CSC: XXX bug here; I think I should split it into Byte-long 335 components; instead I am making a singleton out of it *) 336 let vs ≝ [mk_val ? evres] in 337 ! st ← set_result vs st; 338 ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉 339 ] 340 ] 341 (* CSC: changed, where the meat is *) 342 | joint_st_return ⇒ 343 ! st ← pop_frame st; 344 ! 〈st,pch〉 ← pop st; 345 ! 〈st,pcl〉 ← pop st; 346 let pc ≝ address_of_address_chunks pcl pch in 347 ret ? 〈E0,set_pc pc st〉 348 | _ ⇒ ? 349 ] 350 | ertl_st_new_frame l ⇒ 351 ! v ← framesize globals st; 352 ! sp ← get_hwsp st; 353 let newsp ≝ addr_sub sp v in 354 ! st ← set_hwsp newsp st; 355 ret ? 〈E0,goto l st〉 356 | ertl_st_del_frame l ⇒ 357 ! v ← framesize globals st; 358 ! sp ← get_hwsp st; 359 let newsp ≝ addr_add sp v in 360 ! st ← set_hwsp newsp st; 361 ret ? 〈E0,goto l st〉 362 | ertl_st_frame_size dst l ⇒ 363 ! v ← framesize globals st; 364 ! locals ← reg_store dst (val_of_nat v) (locals st); 217 365 ret ? 〈E0, goto l (set_locals locals st)〉 218 | ertl_st_store addrl addrh src l ⇒219 ! vaddrh ← reg_retrieve (locals st) addrh;220 ! vaddrl ← reg_retrieve (locals st) addrl;221 ! vaddr ← smerge vaddrl vaddrh;222 ! v ← reg_retrieve (locals st) src;223 ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);224 ret ? 〈E0, goto l (set_m m' st)〉225 | ertl_st_cond src ltrue lfalse ⇒226 ! v ← reg_retrieve (locals st) src;227 ! b ← eval_bool_of_val v;228 ret ? 〈E0, goto (if b then ltrue else lfalse) st〉229 | ertl_st_addr ldest hdest id l ⇒230 ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);231 let 〈laddr,haddr〉 ≝ represent_block addr in232 ! locals ← reg_store ldest laddr (locals st);233 ! locals ← reg_store hdest haddr locals;234 ret ? 〈E0, goto l (set_locals locals st)〉235 | ertl_st_op1 op dst src l ⇒236 ! v ← reg_retrieve (locals st) src;237 ! v ← Byte_of_val v;238 let v' ≝ val_of_Byte (op1 eval op v) in239 ! locals ← reg_store dst v' (locals st);240 ret ? 〈E0, goto l (set_locals locals st)〉241 | ertl_st_op2 op dst src1 src2 l ⇒242 ! v1 ← reg_retrieve (locals st) src1;243 ! v1 ← Byte_of_val v1;244 ! v2 ← reg_retrieve (locals st) src2;245 ! v2 ← Byte_of_val v2;246 ! carry ← eval_bool_of_val (carry st);247 let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in248 let v' ≝ val_of_Byte v' in249 let carry ≝ of_bool carry in250 ! locals ← reg_store dst v' (locals st);251 ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉252 | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒253 ! v1 ← reg_retrieve (locals st) sacc;254 ! v1 ← Byte_of_val v1;255 ! v2 ← reg_retrieve (locals st) sbacc;256 ! v2 ← Byte_of_val v2;257 let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in258 let v1' ≝ val_of_Byte v1' in259 let v2' ≝ val_of_Byte v2' in260 ! locals ← reg_store dacc v1' (locals st);261 ! locals ← reg_store dbacc v2' locals;262 ret ? 〈E0, goto l (set_locals locals st)〉263 | ertl_st_clear_carry l ⇒264 ret ? 〈E0, goto l (set_carry Vfalse st)〉265 | ertl_st_set_carry l ⇒266 ret ? 〈E0, goto l (set_carry Vtrue st)〉267 268 (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,269 ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would270 be more than enough... *)271 | ertl_st_move dst src l ⇒272 ! v ← reg_retrieve (locals st) src;273 ! locals ← reg_store dst v (locals st);274 ret ? 〈E0, goto l (set_locals locals st)〉275 | ertl_st_hdw_to_hdw dst src l ⇒276 ! v ← hwreg_retrieve (regs st) src;277 ! regs ← hwreg_store dst v (regs st);278 ret ? 〈E0, goto l (set_regs regs st)〉279 | ertl_st_get_hdw dst src l ⇒280 ! v ← hwreg_retrieve (regs st) src;281 ! locals ← reg_store dst v (locals st);282 ret ? 〈E0, goto l (set_locals locals st)〉283 | ertl_st_set_hdw dst src l ⇒284 ! v ← reg_retrieve (locals st) src;285 ! regs ← hwreg_store dst v (regs st);286 ret ? 〈E0, goto l (set_regs regs st)〉287 288 366 (* CSC: Dropped: 289 367 - rtl_st_stackaddr (becomes two get_hdw) 290 368 - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM) 291 369 - rtl_st_call_ptr (unimplemented ATM) *) 370 ]. 292 371 293 (* CSC: changed, where the meat is *) 294 | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *) 295 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); 296 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); 297 match fd with 298 [ Internal fn ⇒ 299 ! st ← save_ra st l; 300 let st ≝ save_frame st in 301 let locals ≝ init_locals (ertl_if_locals fn) in 302 let l' ≝ ertl_if_entry fn in 303 ret ? 〈 E0, goto l' (set_locals locals st)〉 304 | External fn ⇒ 305 ! params ← fetch_external_args fn st; 306 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)); 307 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 308 (* CSC: XXX bug here; I think I should split it into Byte-long 309 components; instead I am making a singleton out of it *) 310 let vs ≝ [mk_val ? evres] in 311 ! st ← set_result vs st; 312 ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉 372 axiom WrongReturnValueType: String. 373 374 definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝ 375 λglobals: list ident. 376 λexit. 377 λregistersno. 378 λst. 379 (* CSC: monadic notation missing here *) 380 match fetch_statement globals st with 381 [ Error _ ⇒ None ? 382 | OK s ⇒ 383 match s with 384 [ ertl_st_lift_pre pre ⇒ 385 match pre with 386 [ joint_st_return ⇒ 387 match fetch_ra st with 388 [ Error _ ⇒ None ? 389 | OK st_l ⇒ 390 let 〈st,l〉 ≝ st_l in 391 match label_eq l exit with 392 [ inl _ ⇒ 393 (* CSC: monadic notation missing here *) 394 match fetch_result st registersno with 395 [ Error _ ⇒ None ? 396 | OK vals ⇒ Some ? (smerge2 vals) 397 ] 398 | inr _ ⇒ None ? 399 ] 400 ] 401 | _ ⇒ None ? 313 402 ] 314 | ertl_st_return ⇒ 315 ! st ← pop_frame st; 316 ! 〈st,pch〉 ← pop st; 317 ! 〈st,pcl〉 ← pop st; 318 let pc ≝ address_of_address_chunks pcl pch in 319 ret ? 〈E0,set_pc pc st〉 320 321 (* CSC: new stuff *) 322 | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉 323 | ertl_st_new_frame _ ⇒ ? 324 | ertl_st_del_frame _ ⇒ ? 325 | ertl_st_frame_size _ _ ⇒ ? 326 | ertl_st_pop dst l ⇒ 327 ! 〈st,v〉 ← pop st; 328 ! locals ← reg_store dst (val_of_Byte v) (locals st); 329 ret ? 〈E0, goto l (set_locals locals st)〉 330 | ertl_st_push src l ⇒ 331 ! v ← reg_retrieve (locals st) src; 332 ! v ← Byte_of_val v; 333 ! st ← push st v; 334 ret ? 〈E0, goto l st〉 403 | _ ⇒ None ? 404 ] 335 405 ]. 336 406 337 axiom WrongReturnValueType: String. 338 339 definition is_final : state → option ((*CSC: why not res*) int) ≝ 340 λs. match s with 341 [ State _ _ _ ⇒ None ? 342 | Callstate _ _ _ _ _ ⇒ None ? 343 | Returnstate v _ fs _ ⇒ 344 match fs with 345 [ nil ⇒ Some ? (smerge2 v) 346 | _ ⇒ None ? ]]. 347 348 definition RTL_exec : execstep io_out io_in ≝ 349 mk_execstep … ? is_final mem_of_state eval_statement. 407 definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝ 408 λglobals. 409 λexit. 410 λregistersno. 411 mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals). 350 412 351 413 (* CSC: XXX the program type does not fit with the globalenv and init_mem -
Deliverables/D3.3/id-lookup-branch/ERTL/uses.ma
r1153 r1197 18 18 λr. 19 19 assoc_list_find register nat (eq_identifier ?) uses 0 r. 20 21 definition count ≝22 λr.23 λuses.24 (r,25 26 let count r uses = Register.Map.add r (lookup uses r + 1) uses
Note: See TracChangeset
for help on using the changeset viewer.