Changeset 2214 for src/ERTL/ERTLToLTL_paolo.ma
- Timestamp:
- Jul 19, 2012, 2:42:02 PM (9 years ago)
- File:
-
- 1 edited
-
src/ERTL/ERTLToLTL_paolo.ma (modified) (26 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLToLTL_paolo.ma
r2208 r2214 1 1 2 include "LTL/LTL_paolo.ma". 2 3 include "ERTL/Interference_paolo.ma". … … 18 19 coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision. 19 20 20 definition stacksize :21 ∀globals.ℕ → joint_internal_function globals ertl_params → ℕ ≝22 λglobals.23 λspilled_no.24 λint_fun.25 spilled_no + joint_if_stacksize … int_fun.26 27 21 (* Paolo: I'm changing the following: before, spilled registers were 28 22 assigned stack addresses going from SP + #frame_size - #stack_params … … 31 25 32 26 definition preserve_carry_bit : 33 ∀globals.bool → list (joint_seq ltl_params globals) → list (joint_seq ltl_paramsglobals) ≝27 ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝ 34 28 λglobals,do_it,steps. 35 29 if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps. … … 42 36 (* spill should be byte-based from the start *) 43 37 definition set_dp_by_offset : 44 ∀globals.nat → list (joint_seq ltl_paramsglobals) ≝38 ∀globals.nat → list (joint_seq LTL globals) ≝ 45 39 λglobals,off. 46 40 [ A ← byte_of_nat off … … 53 47 54 48 definition get_stack: 55 ∀globals.Register → nat → list (joint_seq ltl_paramsglobals) ≝49 ∀globals.Register → nat → list (joint_seq LTL globals) ≝ 56 50 λglobals,r,off. 57 51 set_dp_by_offset ? off @ … … 60 54 61 55 definition set_stack_not_a : 62 ∀globals.nat → Register → list (joint_seq ltl_paramsglobals) ≝56 ∀globals.nat → Register → list (joint_seq LTL globals) ≝ 63 57 λglobals,off,r. 64 58 set_dp_by_offset ? off @ … … 67 61 68 62 definition set_stack_a : 69 ∀globals.nat → list (joint_seq ltl_paramsglobals) ≝63 ∀globals.nat → list (joint_seq LTL globals) ≝ 70 64 λglobals,off. 71 65 [ RegisterST1 ← A ] @ … … 73 67 74 68 definition set_stack : 75 ∀globals.nat → Register → list (joint_seq ltl_paramsglobals) ≝69 ∀globals.nat → Register → list (joint_seq LTL globals) ≝ 76 70 λglobals,off,r. 77 71 if eq_Register r RegisterA then … … 81 75 82 76 definition set_stack_int : 83 ∀globals.nat → beval → list (joint_seq ltl_paramsglobals) ≝77 ∀globals.nat → beval → list (joint_seq LTL globals) ≝ 84 78 λglobals,off,int. 85 79 set_dp_by_offset ? off @ … … 88 82 89 83 definition move : 90 ∀globals.bool → decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝84 ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝ 91 85 λglobals,carry_lives_after,dst,src. 92 86 match dst with … … 128 122 129 123 definition newframe : 130 ∀globals.ℕ → list (joint_seq ltl_paramsglobals) ≝124 ∀globals.ℕ → list (joint_seq LTL globals) ≝ 131 125 λglobals,stack_sz. 132 126 [ CLEAR_CARRY … … … 140 134 141 135 definition delframe : 142 ∀globals.ℕ → list (joint_seq ltl_paramsglobals) ≝136 ∀globals.ℕ → list (joint_seq LTL globals) ≝ 143 137 λglobals,stack_sz. 144 138 [ A ← RegisterSPL … … 176 170 177 171 definition translate_op2 : 178 ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝172 ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 179 173 λglobals,carry_lives_after,op,dst,arg1,arg2. 180 174 (* this won't preserve the carry bit if op does not set it: left to next function *) … … 189 183 190 184 definition translate_op2_smart : 191 ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝185 ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 192 186 λglobals,carry_lives_after,op,dst,arg1,arg2. 193 187 (* if op does not set carry bit (⇒ it does not use it either) then it must be … … 232 226 233 227 definition translate_op1 : 234 ∀globals.bool → Op1 → decision → decision → list (joint_seq ltl_paramsglobals) ≝228 ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝ 235 229 λglobals,carry_lives_after,op,dst,arg. 236 230 let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in … … 241 235 242 236 definition translate_opaccs : 243 ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝237 ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 244 238 λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2. 245 239 (* OPACCS always has dead carry bit and sets it to zero *) … … 255 249 (* does not preserve carry bit *) 256 250 definition move_to_dp : 257 ∀globals.arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝251 ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 258 252 λglobals,arg1,arg2. 259 253 if ¬arg_is_spilled arg1 then … … 272 266 273 267 definition translate_store : 274 ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝268 ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 275 269 λglobals,carry_lives_after,addr1,addr2,src. 276 270 (* requires src != RegisterA and RegisterB *) … … 286 280 287 281 definition translate_load : 288 ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝282 ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 289 283 λglobals,carry_lives_after,dst,addr1,addr2. 290 284 preserve_carry_bit ? (carry_lives_after ∧ … … 296 290 definition translate_address : 297 291 ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision → 298 list (joint_seq ltl_paramsglobals) ≝292 list (joint_seq LTL globals) ≝ 299 293 λglobals,carry_lives_after,id,prf,addr1,addr2. 300 294 preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2)) 301 (ADDRESS ltl_params? id prf it it ::295 (ADDRESS LTL ? id prf it it :: 302 296 move ? false addr1 RegisterDPL @ 303 297 move ? false addr2 RegisterDPH). … … 306 300 ∀globals.∀after : valuation register_lattice. 307 301 coloured_graph after → 308 ℕ → label → joint_step ertl_params globals → seq_block ltl_params globals (joint_step ltl_paramsglobals) ≝302 ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals) ≝ 309 303 λglobals,after,grph,stack_sz,lbl,s. 310 304 let lookup ≝ λr.colouring … grph (inl … r) in … … 317 311 match s with 318 312 [ step_seq s' ⇒ 319 match s' return λ_.seq_block ltl_params globals (joint_step ltl_paramsglobals) with313 match s' return λ_.seq_block LTL globals (joint_step LTL globals) with 320 314 [ COMMENT c ⇒ COMMENT … c 321 315 | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl … … 373 367 move (lookup r) (arg_decision_imm (byte_of_nat stack_sz)) 374 368 ] 375 | CALL_ID f n_args _ ⇒ CALL_ID ltl_params? f n_args it369 | CALL_ID f n_args _ ⇒ CALL_ID LTL ? f n_args it 376 370 | extension_call abs ⇒ match abs in void with [ ] 377 371 ] … … 381 375 382 376 definition translate_fin_step: 383 ∀globals.label → joint_fin_step ertl_params → seq_block ltl_params globals (joint_fin_step ltl_params) ≝377 ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL) ≝ 384 378 λglobals,lbl,s. 385 match s return λ_.seq_block ltl_params globals (joint_fin_step ltl_params) with379 match s return λ_.seq_block LTL globals (joint_fin_step LTL) with 386 380 [ RETURN ⇒ RETURN ? 387 381 | GOTO l ⇒ GOTO ? l … … 390 384 391 385 definition translate_internal: ∀globals: list ident. 392 joint_internal_function globals ertl_params →393 joint_internal_function globals ltl_params ≝386 joint_internal_function ERTL globals → 387 joint_internal_function LTL globals ≝ 394 388 λglobals: list ident. 395 λint_fun: joint_internal_function globals ertl_params.389 λint_fun: joint_internal_function ERTL globals. 396 390 (* initialize graph *) 397 391 let entry ≝ pi1 … (joint_if_entry … int_fun) in … … 405 399 let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in 406 400 (* initialize internal function *) 407 let init ≝ mk_joint_internal_function globals ltl_params401 let init ≝ mk_joint_internal_function LTL globals 408 402 (joint_if_luniverse … int_fun) 409 403 (joint_if_runiverse … int_fun)
Note: See TracChangeset
for help on using the changeset viewer.
