 Timestamp:
 Sep 21, 2011, 11:24:02 AM (10 years ago)
 Location:
 src/ERTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1230 r1232 7 7 8 8 (* XXX: define an interference graph for a function and colour it, allowing 9 the consultation of registers. *)9 the consultation of registers. 10 10 definition initial_colouring ≝ 11 11 λglobals. … … 46 46  decision_spill ⇒ ? 47 47 ]. 48 *) 49 50 definition lookup ≝ colouring. 48 51 49 52 definition fresh_label ≝ … … 51 54 λluniv. 52 55 fresh LabelTag luniv. 56 57 definition ltl_statement_graph ≝ 58 λglobals. 59 graph … (ltl_statement globals). 53 60 54 61 definition add_graph ≝ … … 71 78 λglobals. 72 79 λint_fun. 73 colour_locals + ( ertl_if_stacksize globalsint_fun).80 colour_locals + (joint_if_stacksize globals ertl_params (ertl_sem_params_ globals) int_fun). 74 81 75 82 definition stacksize ≝ 76 83 λglobals. 77 84 λint_fun. 78 colour_locals + ( ertl_if_stacksize globalsint_fun).85 colour_locals + (joint_if_stacksize globals ertl_params (ertl_sem_params_ globals) int_fun). 79 86 80 87 definition adjust_off ≝ … … 88 95 definition get_stack: 89 96 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → 90 ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) 91 ≝ 97 ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) ≝ 92 98 λglobals: list ident. 93 99 λint_fun. … … 97 103 λl. 98 104 let off ≝ adjust_off globals int_fun off in 99 let luniv ≝ ertl_if_luniverse globalsint_fun in105 let luniv ≝ joint_if_luniverse globals … int_fun in 100 106 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in 101 107 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in … … 117 123 λl. 118 124 let off ≝ adjust_off globals int_fun off in 119 let luniv ≝ ertl_if_luniverse globalsint_fun in125 let luniv ≝ joint_if_luniverse globals … int_fun in 120 126 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in 121 127 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in … … 127 133 〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉. 128 134 129 definition write :130 ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label →131 ? ≝132 λ globals: list ident.133 λ int_fun.135 definition write ≝ 136 λglobals: list ident. 137 λint_fun. 138 λvaluation. 139 λcoloured_graph. 134 140 λgraph. 135 141 λr. 136 142 λl. 137 match lookup rwith143 match lookup valuation coloured_graph (inl … r) with 138 144 [ decision_spill off ⇒ 139 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph offRegisterSST l in145 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l in 140 146 let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in 141 147 〈RegisterSST, l, graph, luniv〉 142 148  decision_colour hwr ⇒ 143 let luniv ≝ ertl_if_luniverse globalsint_fun in149 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in 144 150 〈hwr, l, graph, luniv〉 145 151 ]. 146 152 147 definition read :148 ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register149 → (Register → ltl_statement globals) → ? ≝150 λ globals.151 λ int_fun.153 definition read ≝ 154 λglobals: list ident. 155 λint_fun. 156 λvaluation. 157 λcoloured_graph. 152 158 λgraph. 153 159 λr. 154 160 λstmt. 155 match lookup rwith156 [ decision_colour hwr ⇒ generate globals ( ertl_if_luniverse globalsint_fun) graph (stmt hwr)161 match lookup valuation coloured_graph (inl … r) with 162 [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun) graph (stmt hwr) 157 163  decision_spill off ⇒ 158 164 let temphwr ≝ RegisterSST in 159 let 〈l, graph, luniv〉 ≝ generate globals ( ertl_if_luniverse globalsint_fun) graph (stmt temphwr) in160 let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr offl in165 let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals … int_fun) graph (stmt temphwr) in 166 let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in 161 167 generate globals luniv graph stmt 162 168 ]. … … 173 179 match src with 174 180 [ decision_colour src_hwr ⇒ 175 let luniv ≝ ertl_if_luniverse globalsint_fun in181 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in 176 182 if eq_Register dest_hwr src_hwr then 177 183 〈joint_st_goto … globals l, graph, luniv〉 … … 179 185 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in 180 186 〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉 181  decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_offl187  decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l 182 188 ] 183 189  decision_spill dest_off ⇒ 184 190 match src with 185 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_offsrc_hwr l191 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l 186 192  decision_spill src_off ⇒ 187 let luniv ≝ ertl_if_luniverse globalsint_fun in188 if eq_ bv ?dest_off src_off then193 let luniv ≝ joint_if_luniverse globals … int_fun in 194 if eq_nat dest_off src_off then 189 195 〈joint_st_goto … globals l, graph, luniv〉 190 196 else 191 197 let temp_hwr ≝ RegisterSST in 192 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_offtemp_hwr l in198 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l in 193 199 let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in 194 get_stack globals int_fun graph temp_hwr src_offl200 get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l 195 201 ] 196 202 ]. … … 202 208 λl: label. 203 209 if eq_nat (stacksize globals int_fun) 0 then 204 〈joint_st_goto ltl_params globals l, graph, ( ertl_if_luniverse globalsint_fun)〉210 〈joint_st_goto ltl_params globals l, graph, (joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun)〉 205 211 else 206 let luniv ≝ ertl_if_luniverse globalsint_fun in212 let luniv ≝ joint_if_luniverse globals … int_fun in 207 213 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 208 214 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in … … 221 227 λl. 222 228 if eq_nat (stacksize globals int_fun) 0 then 223 〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globalsint_fun〉229 〈joint_st_goto ltl_params globals l, graph, joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun〉 224 230 else 225 let luniv ≝ ertl_if_luniverse globalsint_fun in231 let luniv ≝ joint_if_luniverse globals … int_fun in 226 232 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 227 233 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in … … 234 240 λglobals: list ident. 235 241 λint_fun. 242 λvaluation. 243 λcoloured_graph: coloured_graph valuation. 236 244 λgraph: ltl_statement_graph globals. 237 245 λstmt: ertl_statement globals. 238 246 match stmt with 239 247 [ joint_st_sequential seq l ⇒ 240 let luniv ≝ ertl_if_luniverse globalsint_fun in248 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in 241 249 match seq with 242 250 [ joint_instr_comment c ⇒ … … 245 253 〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉 246 254  joint_instr_pop r ⇒ 247 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in255 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in 248 256 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 249 257 〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉 250 258  joint_instr_push r ⇒ 251 259 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in 252 let int_fun ≝ set_luniverse globals int_fun luniv in253 let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in260 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 261 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 254 262 〈joint_st_goto ltl_params globals l, graph, luniv〉 255 263  joint_instr_cond srcr lbl_true ⇒ 256 264 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in 257 let int_fun ≝ set_luniverse globals int_fun luniv in258 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in265 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 266 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 259 267 〈joint_st_goto ltl_params globals l, graph, luniv〉 260 268  joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉 … … 265 273 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 266 274 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 267 let int_fun ≝ set_luniverse globals int_fun luniv in268 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in275 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 276 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 269 277 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 270 let int_fun ≝ set_luniverse globals int_fun luniv in271 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in278 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 279 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 272 280 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in 273 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in281 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 274 282 〈joint_st_goto ltl_params globals l, graph, luniv〉 275 283  joint_instr_load destr addr1 addr2 ⇒ 276 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in284 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in 277 285 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 278 286 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in … … 280 288 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 281 289 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 282 let int_fun ≝ set_luniverse globals int_fun luniv in283 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in290 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 291 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 284 292 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 285 let int_fun ≝ set_luniverse globals int_fun luniv in286 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in293 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 294 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 287 295 〈joint_st_goto ltl_params globals l, graph, luniv〉 288 296  joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉 289 297  joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉 290 298  joint_instr_op2 op2 destr srcr ⇒ 291 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in299 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in 292 300 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 293 301 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in 294 let luniv ≝ set_luniverse globals int_fun luniv in295 let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in302 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 303 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 296 304 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 in298 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in305 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 306 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 299 307 〈joint_st_goto ltl_params globals l, graph, luniv〉 300 308  joint_instr_op1 op1 acc_a ⇒ 301 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in309 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a l in 302 310 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 303 311 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in 304 let int_fun ≝ set_luniverse globals int_fun luniv in305 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in312 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 313 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 306 314 〈joint_st_goto ltl_params globals l, graph, luniv〉 307 315  joint_instr_int r i ⇒ 308 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in316 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in 309 317 〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉 310 318  joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒ 311 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in319 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in 312 320 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 313 321 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 314 let luniv ≝ set_luniverse globals int_fun luniv in315 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) in322 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 323 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 316 324 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 317 let luniv ≝ set_luniverse globals int_fun luniv in318 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) in325 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 326 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 319 327 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in 320 let luniv ≝ set_luniverse globals int_fun luniv in321 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in328 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 329 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in 322 330 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 323 331 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in 324 332 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 325 let luniv ≝ set_luniverse globals int_fun luniv in326 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) in333 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 334 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 327 335 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 328 let luniv ≝ set_luniverse globals int_fun luniv in329 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) in336 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 337 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 330 338 〈joint_st_goto ltl_params globals l, graph, luniv〉 331 339  joint_instr_move pair_regs ⇒ … … 335 343 [ pseudo p1 ⇒ 336 344 match regr with 337 [ pseudo p2 ⇒ move globals int_fun graph (lookup p1) (lookup p2) l338  hardware h ⇒ move globals int_fun graph (lookup p1) (decision_colour h) l345 [ pseudo p2 ⇒ move globals int_fun graph (lookup valuation coloured_graph (inl … p1)) (lookup valuation coloured_graph (inl … p2)) l 346  hardware h ⇒ move globals int_fun graph (lookup valuation coloured_graph (inl … p1)) (decision_colour h) l 339 347 ] 340 348  hardware h1 ⇒ 341 349 match regr with 342 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (lookup p) l350 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (lookup valuation coloured_graph (inl … p)) l 343 351  hardware h2 ⇒ 344 352 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in … … 347 355 ] 348 356  joint_instr_address lbl prf dpl dph ⇒ 349 let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in357 let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l in 350 358 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in 351 359 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in 352 360 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in 353 let int_fun ≝ set_luniverse globals int_fun luniv in354 let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in361 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in 362 let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in 355 363 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in 356 364 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in 357 365 〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉 358 366 ] 359  joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globalsint_fun〉360  joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globalsint_fun〉367  joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse globals … int_fun〉 368  joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse globals … int_fun〉 361 369  joint_st_extension ext ⇒ 362 370 match ext with … … 364 372  ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l 365 373  ertl_st_ext_frame_size r l ⇒ 366 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in374 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in 367 375 〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉 368 376 ] … … 370 378 371 379 definition translate_internal ≝ 372 λglobals: list ident. 373 λf. 374 λint_fun: ertl_internal_function. 375 let lookup ≝ λr. 376 match lookup r with 377  colour_spill > 378 ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring) 379  colour_colour color > 380 ERTLToLTLI.Color color 381 in 382 let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in 383 let stacksize ≝ (ertl_if_params int_fun) + locals in 384 mk_ltl_internal_function 385 globals 386 (ertl_if_luniverse int_fun) 387 (ertl_if_runiverse int_fun) 388 stacksize. 389 390 let () = 391 Label.Map.iter (fun label stmt > 392 let stmt = 393 match Liveness.eliminable (G.liveafter label) stmt with 394  Some successor > 395 LTL.St_skip successor 396  None > 397 I.translate_statement stmt 398 in 399 graph := Label.Map.add label stmt !graph 400 ) int_fun.ERTL.f_graph 401 in 380 λglobals. 381 λint_fun. 382 ?. 402 383 403 384 definition translate_funct ≝ 
src/ERTL/Interference.ma
r1230 r1232 15 15 definition vertex ≝ register ⊎ Register. 16 16 17 record graph: Type[0] ≝ 17 inductive decision: Type[0] ≝ 18  decision_spill: nat → decision 19  decision_colour: Register → decision. 20 21 definition is_member ≝ 22 λvertex. 23 λregister_lattice. 24 let 〈l, r〉 ≝ register_lattice in 25 match vertex with 26 [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l 27  inr v ⇒ set_member ? eq_Register v r 28 ]. 29 30 record coloured_graph (v: valuation): Type[1] ≝ 18 31 { 19 interferes: vertex → vertex → bool 32 colouring: vertex → decision; 33 prop_colouring: ∀l. ∀v1, v2: vertex. 34 is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 20 35 }. 21 36 22 axiom build: ∀globals: list ident. ertl_internal_function globals → valuation × graph. 23 24 inductive decision: Type[0] ≝ 25  decision_spill: decision 26  decision_colour: Register → decision. 27 28 record coloured_graph (d: Type[0]): Type[1] ≝ 29 { 30 the_graph: graph; 31 colouring: register → d; 32 prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2 33 }. 34 35 definition initial_colouring ≝ coloured_graph decision. 36 axiom colour_initial: graph → initial_colouring. 37 definition stack_colouring ≝ coloured_graph nat. 38 axiom colour_stack: graph → stack_colouring. 39 37 axiom build: ∀valuation. coloured_graph valuation. 40 38 41 39 (* definition vertex_set ≝ set vertex. *) … … 517 515 nmr = PrioritySet.remove x graph.nmr; 518 516 } 519 *)520 521 *)522 517 523 518 axiom ig_mkppp: graph → register → register → graph. … … 527 522 axiom ig_remove: graph → vertex → graph. 528 523 axiom ig_freeze: graph → vertex → graph. 529 axiom ig_restrict: graph → ( register → bool) → graph. (* XXX: change *)524 axiom ig_restrict: graph → (vertex → bool) → graph. 530 525 axiom ig_droph: graph → graph. 531 526 axiom ig_lookup: graph → register → vertex. … … 545 540 definition ig_phedge ≝ vertex × Register. 546 541 axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge. 542 *) 543 *)
Note: See TracChangeset
for help on using the changeset viewer.