 Timestamp:
 Sep 23, 2011, 3:04:20 PM (8 years ago)
 Location:
 src/ERTL
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1256 r1260 92 92 93 93 definition get_stack: 94 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → 95 ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) ≝ 94 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝ 96 95 λglobals: list ident. 97 96 λint_fun. … … 100 99 λoff. 101 100 λl. 101 λoriginal_label. 102 102 let off ≝ adjust_off globals int_fun off in 103 103 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in … … 105 105 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in 106 106 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 107 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in107 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in 108 108 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in 109 109 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 110 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in111 〈 joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l,graph, luniv〉.110 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in 111 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉. 112 112 113 113 definition set_stack: 114 114 ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte 115 → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag))≝115 → Register → label → ? ≝ 116 116 λglobals: list ident. 117 117 λint_fun. … … 120 120 λr. 121 121 λl. 122 λoriginal_label. 122 123 let off ≝ adjust_off globals int_fun off in 123 124 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in … … 125 126 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in 126 127 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 127 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in128 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in 128 129 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in 129 130 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 130 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in 131 〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l, graph, luniv〉. 131 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in 132 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉. 133 132 134 133 135 definition write ≝ 134 136 λglobals: list ident. 135 λint_fun .137 λint_fun: ertl_internal_function globals. 136 138 λvaluation. 137 139 λcoloured_graph. … … 139 141 λr. 140 142 λl. 143 λoriginal_label: label. 141 144 match colouring valuation coloured_graph (inl … r) with 142 145 [ decision_spill off ⇒ 143 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST lin144 let 〈 l, graph, int_fun〉 ≝ generate globals luniv graph stmtin146 let luniv ≝ joint_if_luniverse … int_fun in 147 let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in 145 148 〈RegisterSST, l, graph, luniv〉 146 149  decision_colour hwr ⇒ … … 151 154 definition read ≝ 152 155 λglobals: list ident. 153 λint_fun .156 λint_fun: ertl_internal_function globals. 154 157 λvaluation. 155 158 λcoloured_graph. … … 157 160 λr. 158 161 λstmt. 162 λoriginal_label: label. 159 163 match colouring valuation coloured_graph (inl … r) with 160 [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt hwr) 164 [ decision_colour hwr ⇒ 165 let luniv ≝ joint_if_luniverse … int_fun in 166 〈add_graph globals original_label (stmt hwr) graph, luniv〉 161 167  decision_spill off ⇒ 162 168 let temphwr ≝ RegisterSST in 163 let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt temphwr)in164 let 〈 stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) lin165 ge nerate globals luniv graph stmt169 let luniv ≝ joint_if_luniverse … int_fun in 170 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in 171 get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l original_label 166 172 ]. 167 173 … … 173 179 λsrc: decision. 174 180 λl: label. 181 λoriginal_label. 175 182 match dest with 176 183 [ decision_colour dest_hwr ⇒ … … 179 186 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 180 187 if eq_Register dest_hwr src_hwr then 181 〈 joint_st_goto … globals l,graph, luniv〉188 〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉 182 189 else 183 190 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in 184 〈 joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l,graph, luniv〉185  decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l 191 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l) graph, luniv〉 192  decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label 186 193 ] 187 194  decision_spill dest_off ⇒ 188 195 match src with 189 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l 196 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label 190 197  decision_spill src_off ⇒ 191 198 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 192 199 if eq_nat dest_off src_off then 193 〈 joint_st_goto … globals l,graph, luniv〉200 〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉 194 201 else 195 202 let temp_hwr ≝ RegisterSST in 196 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l in 197 let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in 198 get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l 203 let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in 204 get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label 199 205 ] 200 206 ]. … … 205 211 λgraph: ltl_statement_graph globals. 206 212 λl: label. 213 λoriginal_label: label. 207 214 if eq_nat (stacksize globals int_fun) 0 then 208 〈joint_st_goto … globals l, graph, (joint_if_luniverse globals (ertl_params globals) int_fun)〉 215 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 216 〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉 209 217 else 210 218 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 211 219 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 212 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in220 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in 213 221 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in 214 222 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in 215 223 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in 216 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in224 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in 217 225 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in 218 226 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in 219 〈 joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l,graph, luniv〉.227 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l) graph, luniv〉. 220 228 221 229 definition delframe ≝ … … 224 232 λgraph: graph (ltl_statement globals). 225 233 λl. 234 λoriginal_label: label. 226 235 if eq_nat (stacksize globals int_fun) 0 then 227 〈joint_st_goto (ltl_params globals) globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉 236 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 237 〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉 228 238 else 229 239 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 230 240 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 231 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in241 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in 232 242 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in 233 243 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in 234 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in235 〈 joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l,graph, luniv〉.244 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in 245 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉. 236 246 237 247 definition translate_statement ≝ … … 242 252 λgraph: ltl_statement_graph globals. 243 253 λstmt: ertl_statement globals. 254 λoriginal_label: label. 244 255 match stmt with 245 256 [ joint_st_sequential seq l ⇒ … … 247 258 match seq with 248 259 [ joint_instr_comment c ⇒ 249 〈 joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l,graph, luniv〉260 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l) graph, luniv〉 250 261  joint_instr_cost_label cost_lbl ⇒ 251 〈 joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l,graph, luniv〉262 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l) graph, luniv〉 252 263  joint_instr_pop r ⇒ 253 264 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in 254 265 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 255 〈 joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l,graph, luniv〉266 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l) graph, luniv〉 256 267  joint_instr_push r ⇒ 257 268 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in 258 269 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 259 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 260 〈joint_st_goto … globals l, graph, luniv〉 270 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 271 let int_fun' ≝ set_luniverse globals ? int_fun luniv in 272 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l frees) in 273 〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉 274  _ ⇒ ? 275 ] 276  _ ⇒ ? 277 ]. 261 278  joint_instr_cond srcr lbl_true ⇒ 262 279 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in 263 280 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 264 281 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 265 〈 joint_st_goto (ltl_params globals) globals l,graph, luniv〉266  joint_instr_call_id f ignore ⇒ 〈 joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l,graph, luniv〉282 〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉 283  joint_instr_call_id f ignore ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l) graph, luniv〉 267 284  joint_instr_store addr1 addr2 srcr ⇒ 268 285 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in … … 278 295 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in 279 296 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 280 〈 joint_st_goto (ltl_params globals) globals l,graph, luniv〉297 〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉 281 298  joint_instr_load destr addr1 addr2 ⇒ 282 299 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in … … 291 308 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 292 309 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 293 〈 joint_st_goto (ltl_params globals) globals l,graph, luniv〉294  joint_instr_clear_carry ⇒ 〈 joint_st_sequential … globals (joint_instr_clear_carry … globals) l,graph, luniv〉295  joint_instr_set_carry ⇒ 〈 joint_st_sequential … globals (joint_instr_set_carry … globals) l,graph, luniv〉296  joint_instr_op2 op2 destr srcr ⇒310 〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉 311  joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) graph, luniv〉 312  joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_set_carry … globals) l) graph, luniv〉 313  joint_instr_op2 op2 destr srcr1 srcr2 ⇒ 297 314 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in 298 315 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 299 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in300 let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 301 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) in316 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it it RegisterB) l) in 317 let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 318 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 302 319 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 303 320 let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 321 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 322 〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉 323  joint_instr_op1 op1 destr srcr ⇒ 324 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in 325 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 326 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it it) l) in 327 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 304 328 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 305 〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉 306  joint_instr_op1 op1 acc_a ⇒ 307 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a l in 308 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 309 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in 310 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 311 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 312 〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉 329 〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉 313 330  joint_instr_int r i ⇒ 314 331 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in 315 〈 joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l,graph, luniv〉332 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l) graph, luniv〉 316 333  joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒ 317 334 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in … … 334 351 let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 335 352 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 336 〈 joint_st_goto … globals l,graph, luniv〉353 〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉 337 354  joint_instr_move pair_regs ⇒ 338 355 let regl ≝ \fst pair_regs in … … 341 358 [ pseudo p1 ⇒ 342 359 match regr with 343 [ pseudo p2 ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l 344  hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l 360 [ pseudo p2 ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label 361  hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label 345 362 ] 346 363  hardware h1 ⇒ 347 364 match regr with 348 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l 365 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label 349 366  hardware h2 ⇒ 350 367 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in 351 〈 joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l,graph, luniv〉368 〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l) graph, luniv〉 352 369 ] 353 370 ] 371  _ ⇒ ? 372 ] 373  _ ⇒ ? 374 ]. 375 354 376  joint_instr_address lbl prf dpl dph ⇒ 355 377 let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l in … … 364 386  joint_instr_extension ext ⇒ 365 387 match ext with 366 [ ertl_st_ext_new_frame l⇒ newframe globals int_fun graph l367  ertl_st_ext_del_frame l⇒ delframe globals int_fun graph l368  ertl_st_ext_frame_size r l⇒388 [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l 389  ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l 390  ertl_st_ext_frame_size r ⇒ 369 391 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in 370 392 〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉 … … 375 397 ]. 376 398 377 axiomSm_leq_n_m_leq_n:399 lemma Sm_leq_n_m_leq_n: 378 400 ∀m, n: nat. 379 401 S m ≤ n → m ≤ n. 402 #m #n /2/ 403 qed. 380 404 381 405 let rec mapi_aux 382 406 (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat) 383 407 on n: n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → BitVectorTrie b n ≝ 384 match n return λn . n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → BitVectorTrie b n with408 match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → BitVectorTrie b n with 385 409 [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16. 386 match trie return λx . λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with410 match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with 387 411 [ Leaf l ⇒ λprf. Leaf … (f accu l) 388 412  Stub s ⇒ λprf. Stub … s … … 390 414 ] (refl … 0) 391 415  S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16  (S n')). 392 match trie return λx . λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with416 match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with 393 417 [ Leaf l ⇒ λabsrd. ⊥ 394 418  Stub s ⇒ λprf. Stub … s 395 419  Node n'' l r ⇒ λprf. 396 420 Node ? n'' ? ? 397 (* (mapi_aux a b f n' ? (l⌈n'' ↦ n'⌉) ((false ::: accu)⌈S (16  S n') ↦ 16  n'⌉)) 398 (mapi_aux a b f n' ? (r⌈n'' ↦ n'⌉) ((true ::: accu)⌈S (16  S n') ↦ 16  n'⌉))*) 399 ] (refl ? (S n')) 421 ] (refl nat (S n')) 400 422 ]. 401 423 [ 1,2: destruct(absrd) … … 420 442 ] 421 443 qed. 444 445 definition mapi ≝ 446 λa, b: Type[0]. 447 λf: label → a → b. 448 λtrie: BitVectorTrie a 16. 449 let f' ≝ λbv: BitVector 16. λa. 450 f (an_identifier LabelTag bv) a 451 in 452 mapi_aux a b f' 16 ? trie [[]]. 453 // 454 qed. 422 455 423 check mapi_aux.424 425 456 definition translate_internal ≝ 426 457 λglobals. 427 458 λint_fun. 428 let uses ≝ examine_internal globals int_fun in 429 let 459 let graph ≝ ((empty_map …) : ltl_statement_graph globals) in 460 let valuation ≝ analyse globals int_fun in 461 let coloured_graph ≝ build valuation in 462 let liveafter ≝ analyse globals int_fun in 463 let blah ≝ mapi … (λlabel. λstmt_graph_luniv. 464 let stmt ≝ 465 match eliminable globals (liveafter label) stmt with 466 [ Some successor ⇒ 〈joint_st_goto … successor, graph, joint_if_luniverse … int_fun〉 467  None ⇒ translate_statement globals int_fun valuation coloured_graph graph stmt 468 ] 469 in 470 ?) (joint_if_code … int_fun) 471 in ?. 472 473 474 475 let stmt = 476 match Liveness.eliminable (G.liveafter label) stmt with 477  Some successor > 478 LTL.St_skip successor 479  None > 480 I.translate_statement stmt 481 in 482 graph := Label.Map.add label stmt !graph 483 ) int_fun.ERTL.f_graph 430 484 431 485 definition translate_funct ≝ 
src/ERTL/liveness.ma
r1250 r1260 80 80 [ joint_st_sequential seq l ⇒ 81 81 match seq with 82 [ joint_instr_op2 op2 r _ ⇒82 [ joint_instr_op2 op2 r1 r2 _ ⇒ 83 83 match op2 with 84 [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r )85  Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r )86  Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)87  _ ⇒ lattice_psingleton r 84 [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1) 85  Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1) 86  Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1) 87  _ ⇒ lattice_psingleton r1 88 88 ] 89 89  joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry 90 90  joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry 91 91  joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 92  joint_instr_op1 op1 r ⇒ lattice_psingleton r92  joint_instr_op1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 93 93  joint_instr_pop r ⇒ lattice_psingleton r 94 94  joint_instr_int r _ ⇒ lattice_psingleton r … … 111 111  joint_instr_extension ext ⇒ 112 112 match ext with 113 [ ertl_st_ext_new_frame l⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)114  ertl_st_ext_del_frame l⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)115  ertl_st_ext_frame_size r l⇒ lattice_psingleton r]]113 [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 114  ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 115  ertl_st_ext_frame_size r ⇒ lattice_psingleton r]] 116 116  joint_st_return ⇒ lattice_bottom 117 117  joint_st_goto l ⇒ lattice_bottom … … 126 126 [ joint_st_sequential seq l ⇒ 127 127 match seq with 128 [ joint_instr_op2 op2 acc_a r ⇒128 [ joint_instr_op2 op2 acc_a r1 r2 ⇒ 129 129 match op2 with 130 130 [ Addc ⇒ 131 lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)132  _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)131 lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry) 132  _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 133 133 ] 134 134  joint_instr_clear_carry ⇒ lattice_bottom … … 136 136 (* acc_a and acc_b *) 137 137  joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 138  joint_instr_op1 op1 r ⇒ lattice_psingleton r138  joint_instr_op1 op1 r1 r2 ⇒ lattice_psingleton r2 139 139  joint_instr_pop r ⇒ lattice_bottom 140 140  joint_instr_int r _ ⇒ lattice_bottom … … 158 158  joint_instr_extension ext ⇒ 159 159 match ext with 160 [ ertl_st_ext_new_frame l⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)161  ertl_st_ext_del_frame l⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)162  ertl_st_ext_frame_size r l⇒ lattice_bottom]]160 [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 161  ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 162  ertl_st_ext_frame_size r ⇒ lattice_bottom]] 163 163  joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉 164 164  joint_st_goto l ⇒ lattice_bottom … … 173 173 [ joint_st_sequential seq l ⇒ 174 174 match seq with 175 [ joint_instr_op2 op2 acc_a r⇒176 if set_member … (eq_identifier …) acc_apliveafter ∨175 [ joint_instr_op2 op2 r1 r2 r3 ⇒ 176 if set_member … (eq_identifier …) r1 pliveafter ∨ 177 177 set_member … eq_Register RegisterCarry hliveafter then 178 178 None ? … … 188 188 else 189 189 Some ? l 190  joint_instr_op1 op1 r ⇒191 if set_member … (eq_identifier …) r pliveafter ∨190  joint_instr_op1 op1 r1 r2 ⇒ 191 if set_member … (eq_identifier …) r1 pliveafter ∨ 192 192 set_member … eq_Register RegisterCarry hliveafter then 193 193 None ? … … 237 237  joint_instr_extension ext ⇒ 238 238 match ext with 239 [ ertl_st_ext_new_frame l⇒ None ?240  ertl_st_ext_del_frame l⇒ None ?241  ertl_st_ext_frame_size r l⇒239 [ ertl_st_ext_new_frame ⇒ None ? 240  ertl_st_ext_del_frame ⇒ None ? 241  ertl_st_ext_frame_size r ⇒ 242 242 if set_member ? (eq_identifier RegisterTag) r pliveafter ∨ 243 243 set_member ? eq_Register RegisterCarry hliveafter then 
src/ERTL/uses.ma
r1253 r1260 41 41  joint_instr_address lbl prf r1 r2 ⇒ count r1 (count r2 uses) 42 42  joint_instr_opaccs opaccs acc_a acc_b ⇒ count acc_a (count acc_b uses) 43  joint_instr_op1 op1 r1 ⇒ count r1 uses44  joint_instr_op2 op2 r1 r2 ⇒ count r1 (count r2 uses)43  joint_instr_op1 op1 r1 r2 ⇒ count r1 (count r2 uses) 44  joint_instr_op2 op2 r1 r2 r3 ⇒ count r1 (count r2 (count r3 uses)) 45 45  joint_instr_load destr r1 r2 ⇒ count r1 (count r2 (count destr uses)) 46 46  joint_instr_store srcr r1 r2 ⇒ count r1 (count r2 (count srcr uses)) … … 48 48  joint_instr_extension ext ⇒ 49 49 match ext with 50 [ ertl_st_ext_new_frame l⇒ uses51  ertl_st_ext_del_frame l⇒ uses52  ertl_st_ext_frame_size r l⇒ count r uses]]50 [ ertl_st_ext_new_frame ⇒ uses 51  ertl_st_ext_del_frame ⇒ uses 52  ertl_st_ext_frame_size r ⇒ count r uses]] 53 53  joint_st_return ⇒ uses 54 54  joint_st_goto l ⇒ uses
Note: See TracChangeset
for help on using the changeset viewer.