Changeset 1282 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 Sep 28, 2011, 11:50:32 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1281 r1282 58 58 let off ≝ adjust_off globals int_fun off in 59 59 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 60 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc r)) l) in61 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_load… globals it it it) l) in62 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterDPH)) l) in63 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in64 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_int… globals RegisterA (zero ?)) l) in65 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterDPL)) l) in66 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in67 〈add_graph globals original_label ( joint_st_sequential (ltl_params globals) globals (joint_instr_int… (ltl_params globals) globals RegisterA off) l) graph, luniv〉.60 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in 61 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (LOAD … globals it it it) l) in 62 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in 63 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in 64 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in 65 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in 66 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in 67 〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉. 68 68 69 69 definition set_stack: … … 79 79 let off ≝ adjust_off globals int_fun off in 80 80 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 81 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_store… globals it it it) l) in82 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (to_acc r)) l) in83 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterDPH)) l) in84 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in85 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_int… globals RegisterA (zero ?)) l) in86 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterDPL)) l) in87 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in88 〈add_graph globals original_label ( joint_st_sequential (ltl_params globals) globals (joint_instr_int… (ltl_params globals) globals RegisterA off) l) graph, luniv〉.81 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in 82 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc r)) l) in 83 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in 84 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in 85 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in 86 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in 87 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in 88 〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉. 89 89 90 90 … … 142 142 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 143 143 if eq_Register dest_hwr src_hwr then 144 〈add_graph globals original_label ( joint_st_goto… globals l) graph, luniv〉144 〈add_graph globals original_label (GOTO … globals l) graph, luniv〉 145 145 else 146 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc dest_hwr)) l) in147 〈add_graph globals original_label ( joint_st_sequential (ltl_params globals) globals (joint_instr_move… globals (to_acc src_hwr)) l) graph, luniv〉146 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in 147 〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉 148 148  decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label 149 149 ] … … 154 154 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 155 155 if eq_nat dest_off src_off then 156 〈add_graph globals original_label ( joint_st_goto… globals l) graph, luniv〉156 〈add_graph globals original_label (GOTO … globals l) graph, luniv〉 157 157 else 158 158 let temp_hwr ≝ RegisterSST in … … 170 170 if eq_nat (stacksize globals int_fun) 0 then 171 171 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 172 〈add_graph globals original_label ( joint_st_goto… globals l) graph, luniv〉172 〈add_graph globals original_label (GOTO … globals l) graph, luniv〉 173 173 else 174 174 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 175 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterSPH)) l) in176 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in177 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_int… globals RegisterDPH (zero ?)) l) in178 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (to_acc RegisterSPH)) l) in179 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterSPL)) l) in180 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in181 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_clear_carry… globals) l) in182 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) in183 〈add_graph globals original_label ( joint_st_sequential (ltl_params globals) globals (joint_instr_move… globals (to_acc RegisterSPL)) l) graph, luniv〉.175 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in 176 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPH) l) in 177 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPH (zero ?)) l) in 178 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterSPH)) l) in 179 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in 180 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in 181 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in 182 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in 183 〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉. 184 184 185 185 definition delframe ≝ … … 191 191 if eq_nat (stacksize globals int_fun) 0 then 192 192 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 193 〈add_graph globals original_label ( joint_st_goto(ltl_params globals) globals l) graph, luniv〉193 〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉 194 194 else 195 195 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 196 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterSPH)) l) in197 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in198 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_int… globals RegisterA (zero ?)) l) in199 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterSPL)) l) in200 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in201 〈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〉.196 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in 197 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in 198 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in 199 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in 200 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in 201 〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉. 202 202 203 203 definition translate_statement: … … 213 213 λoriginal_label: label. 214 214 match stmt with 215 [ joint_st_sequential seq l ⇒215 [ sequential seq l ⇒ 216 216 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 217 217 match seq with 218 [ joint_instr_commentc ⇒219 〈add_graph globals original_label ( joint_st_sequential … (joint_instr_comment… c) l) graph, luniv〉220  joint_instr_cost_labelcost_lbl ⇒221 〈add_graph globals original_label ( joint_st_sequential … (joint_instr_cost_label… cost_lbl) l) graph, luniv〉222  joint_instr_popr ⇒218 [ COMMENT c ⇒ 219 〈add_graph globals original_label (sequential … (COMMENT … c) l) graph, luniv〉 220  COST_LABEL cost_lbl ⇒ 221 〈add_graph globals original_label (sequential … (COST_LABEL … cost_lbl) l) graph, luniv〉 222  POP r ⇒ 223 223 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 224 224 let int_fun ≝ set_luniverse globals ? int_fun luniv in 225 225 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in 226 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc hdw)) l) in227 〈add_graph globals original_label ( joint_st_sequential ltl_params_ globals (joint_instr_pop… it) l) graph, luniv〉228  joint_instr_pushr ⇒229 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_push …it) l) in230 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 231 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 232 let int_fun ≝ set_luniverse globals ? int_fun luniv in 233 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in234 〈add_graph globals original_label ( joint_st_goto… fresh_lbl) graph, luniv〉235  joint_instr_condsrcr lbl_true ⇒236 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_cond… it lbl_true) l) in226 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in 227 〈add_graph globals original_label (sequential ltl_params_ globals (POP … it) l) graph, luniv〉 228  PUSH r ⇒ 229 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (PUSH … globals it) l) in 230 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 231 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 232 let int_fun ≝ set_luniverse globals ? int_fun luniv in 233 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 234 〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉 235  COND srcr lbl_true ⇒ 236 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (COND … it lbl_true) l) in 237 237 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 238 238 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 239 239 let int_fun' ≝ set_luniverse globals ? int_fun luniv in 240 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in241 〈add_graph globals original_label ( joint_st_goto… fresh_lbl) graph, luniv〉242  joint_instr_call_id f ignore ignore' ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id… f ignore ignore') l) graph, luniv〉243  joint_instr_storeaddr1 addr2 srcr ⇒244 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_store… it it it) l) in245 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (to_acc RegisterST1)) l) in246 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc RegisterDPH)) l) in247 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (to_acc RegisterST0)) l) in248 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc RegisterDPL)) l) in249 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 250 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 251 let int_fun ≝ set_luniverse globals ? int_fun luniv in 252 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in253 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc RegisterST0)) fresh_lbl) in254 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 255 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 256 let int_fun ≝ set_luniverse globals ? int_fun luniv in 257 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in258 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc RegisterST1)) fresh_lbl) in259 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 260 let int_fun ≝ set_luniverse globals ? int_fun luniv in 261 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in262 〈add_graph globals original_label ( joint_st_goto… l) graph, luniv〉263  joint_instr_loaddestr addr1 addr2 ⇒240 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 241 〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉 242  CALL_ID f ignore ignore' ⇒ 〈add_graph globals original_label (sequential … (CALL_ID … f ignore ignore') l) graph, luniv〉 243  STORE addr1 addr2 srcr ⇒ 244 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (STORE … it it it) l) in 245 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST1)) l) in 246 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in 247 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in 248 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in 249 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 250 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 251 let int_fun ≝ set_luniverse globals ? int_fun luniv in 252 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 253 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in 254 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 255 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 256 let int_fun ≝ set_luniverse globals ? int_fun luniv in 257 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 258 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST1)) fresh_lbl) in 259 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 260 let int_fun ≝ set_luniverse globals ? int_fun luniv in 261 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 262 〈add_graph globals original_label (GOTO … l) graph, luniv〉 263  LOAD destr addr1 addr2 ⇒ 264 264 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 265 265 let int_fun ≝ set_luniverse globals ? int_fun luniv in 266 266 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in 267 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc hdw)) l) in268 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_load… it it it) l) in269 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc RegisterDPH)) l) in270 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (to_acc RegisterST0)) l) in271 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc RegisterDPL)) l) in272 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 273 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 274 let int_fun ≝ set_luniverse globals ? int_fun luniv in 275 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in276 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc RegisterST0)) fresh_lbl) in277 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 278 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 279 let int_fun ≝ set_luniverse globals ? int_fun luniv in 280 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in281 〈add_graph globals original_label ( joint_st_goto… fresh_lbl) graph, luniv〉282  joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_clear_carry…) l) graph, luniv〉283  joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_set_carry…) l) graph, luniv〉284  joint_instr_op2 op2 destr srcr1 srcr2 ⇒267 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in 268 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (LOAD … it it it) l) in 269 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in 270 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in 271 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in 272 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 273 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 274 let int_fun ≝ set_luniverse globals ? int_fun luniv in 275 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 276 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in 277 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 278 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 279 let int_fun ≝ set_luniverse globals ? int_fun luniv in 280 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 281 〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉 282  CLEAR_CARRY ⇒ 〈add_graph globals original_label (sequential … (CLEAR_CARRY …) l) graph, luniv〉 283  SET_CARRY ⇒ 〈add_graph globals original_label (sequential … (SET_CARRY …) l) graph, luniv〉 284  OP2 op2 destr srcr1 srcr2 ⇒ 285 285 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 286 286 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 287 287 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in 288 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc hdw)) l) in289 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_op2 … op2 it it RegisterB) l) in290 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 291 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 292 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in293 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc RegisterB)) fresh_lbl) in294 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 295 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 296 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in297 〈add_graph globals original_label ( joint_st_goto… l) graph, luniv〉298  joint_instr_op1 op1 destr srcr ⇒288 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in 289 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP2 … op2 it it RegisterB) l) in 290 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 291 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 292 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 293 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterB)) fresh_lbl) in 294 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 295 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 296 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 297 〈add_graph globals original_label (GOTO … l) graph, luniv〉 298  OP1 op1 destr srcr ⇒ 299 299 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 300 300 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 301 301 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in 302 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc hdw)) l) in303 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_op1 … op1 it it) l) in304 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 305 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 306 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 307 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move… (to_acc hdw)) l) fresh_lbl in308 〈add_graph globals original_label ( joint_st_goto… l) graph, luniv〉309  joint_instr_intr i ⇒302 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in 303 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP1 … op1 it it) l) in 304 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 305 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 306 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 307 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in 308 〈add_graph globals original_label (GOTO … l) graph, luniv〉 309  INT r i ⇒ 310 310 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 311 311 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 312 312 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in 313 〈add_graph globals original_label ( joint_st_sequential ltl_params_ globals (joint_instr_int… hdw i) l) graph, luniv〉314  joint_instr_movepair_regs ⇒313 〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉 314  MOVE pair_regs ⇒ 315 315 let regl ≝ \fst pair_regs in 316 316 let regr ≝ \snd pair_regs in … … 325 325 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label 326 326  hardware h2 ⇒ 327 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc h1)) l) in328 〈add_graph globals original_label ( joint_st_sequential ltl_params_ … (joint_instr_move… (to_acc h2)) l) graph, luniv〉327 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in 328 〈add_graph globals original_label (sequential ltl_params_ … (MOVE … (to_acc h2)) l) graph, luniv〉 329 329 ] 330 330 ] 331  joint_instr_addresslbl prf dpl dph ⇒331  ADDRESS lbl prf dpl dph ⇒ 332 332 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 333 333 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 334 334 let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in 335 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc hdw1)) l) in336 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (to_acc RegisterDPH)) l) in337 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_address… globals lbl prf it it) l) in335 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw1)) l) in 336 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPH)) l) in 337 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (ADDRESS … globals lbl prf it it) l) in 338 338 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 339 339 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 340 340 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 341 341 let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in 342 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc hdw2)) l) in343 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (to_acc RegisterDPL)) l) in344 〈add_graph globals original_label ( joint_st_sequential ltl_params_ globals (joint_instr_address… lbl prf it it) l) graph, luniv〉345  joint_instr_extension ext ⇒342 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw2)) l) in 343 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPL)) l) in 344 〈add_graph globals original_label (sequential ltl_params_ globals (ADDRESS … lbl prf it it) l) graph, luniv〉 345  extension ext ⇒ 346 346 match ext with 347 347 [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label … … 351 351 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 352 352 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in 353 〈add_graph globals original_label ( joint_st_sequential ltl_params_ globals (joint_instr_int… hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉353 〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉 354 354 ] 355  joint_instr_opaccsopaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒355  OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ 356 356 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 357 357 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in 358 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_move… (from_acc hdw)) l) in359 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … (joint_instr_opaccs… opaccs it it it it) l) in360 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 361 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 362 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 363 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move… globals (to_acc hdw)) l) fresh_lbl in364 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterB)) fresh_lbl) in365 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 366 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 367 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 368 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move… globals (to_acc hdw)) l) fresh_lbl in369 〈add_graph globals original_label ( joint_st_goto… globals fresh_lbl) graph, luniv〉358 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in 359 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OPACCS … opaccs it it it it) l) in 360 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 361 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 362 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 363 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in 364 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterB)) fresh_lbl) in 365 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 366 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 367 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 368 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in 369 〈add_graph globals original_label (GOTO … globals fresh_lbl) graph, luniv〉 370 370 ] 371  joint_st_return ⇒ 〈add_graph globals original_label (joint_st_returnltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉372  joint_st_goto l ⇒ 〈add_graph globals original_label (joint_st_gotoltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉371  RETURN ⇒ 〈add_graph globals original_label (RETURN ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉 372  GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉 373 373 ]. 374 374 … … 435 435 let 〈graph, luniv〉 ≝ graph_luniv in 436 436 match eliminable globals (valuation label) stmt with 437 [ Some successor ⇒ 〈add_graph globals label ( joint_st_goto… successor) graph, luniv〉437 [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉 438 438  None ⇒ 439 439 translate_statement globals int_fun valuation coloured_graph graph stmt label
Note: See TracChangeset
for help on using the changeset viewer.