 Timestamp:
 Oct 19, 2011, 6:05:50 PM (10 years ago)
 Location:
 src/ERTL
 Files:

 1 deleted
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1352 r1423 1 1 include "ERTL/ERTL.ma". 2 2 include "LTL/LTL.ma". 3 include "ERTL/spill.ma".4 3 include "ASM/Arithmetic.ma". 5 4 … … 30 29 31 30 definition num_locals ≝ 32 λglobals. 33 λint_fun. 34 colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun). 31 λspilled_no. 32 λglobals. 33 λint_fun. 34 spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun). 35 35 36 36 definition stacksize ≝ 37 λglobals. 38 λint_fun. 39 colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun). 37 λspilled_no. 38 λglobals. 39 λint_fun. 40 spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun). 40 41 41 42 definition adjust_off ≝ 43 λspilled_no. 42 44 λglobals. 43 45 λint_fun. 44 46 λoff. 45 47 let 〈ignore, int_off〉 ≝ half_add ? int_size off in 46 let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in48 let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals spilled_no globals int_fun)) int_off false in 47 49 sub. 48 50 49 51 definition get_stack: 50 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝ 52 nat → ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝ 53 λspilled_no. 51 54 λglobals: list ident. 52 55 λint_fun. … … 56 59 λl. 57 60 λoriginal_label. 58 let off ≝ adjust_off globals int_fun off in61 let off ≝ adjust_off spilled_no globals int_fun off in 59 62 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 60 63 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in … … 68 71 69 72 definition set_stack: 70 ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte73 nat → ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte 71 74 → Register → label → ? ≝ 75 λspilled_no. 72 76 λglobals: list ident. 73 77 λint_fun. … … 77 81 λl. 78 82 λoriginal_label. 79 let off ≝ adjust_off globals int_fun off in83 let off ≝ adjust_off spilled_no globals int_fun off in 80 84 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 81 85 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in 
src/ERTL/Interference.ma
r1282 r1423 1 1 include "ERTL/ERTL.ma". 2 2 include "ERTL/liveness.ma". 3 include "basics/jmeq.ma". 3 4 4 5 definition vertex ≝ register ⊎ Register. … … 17 18 ]. 18 19 20 (* prop_colouring is the non interferece 21 prop_colouring 2 and 3 together say that spilled_no is the number of spilled 22 registers *) 23 (* Wilmer: the generation of the destruct principle diverges; 24 CtrC make the file pass *) 19 25 record coloured_graph (v: valuation): Type[1] ≝ 20 { 21 colouring: vertex → decision; 22 prop_colouring: ∀l. ∀v1, v2: vertex. 23 is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 26 { colouring: vertex → decision 27 ; spilled_no: nat 28 ; prop_colouring: ∀l. ∀v1, v2: vertex. 29 is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 30 ; prop_colouring2: 31 ∀v1:vertex. (∃l. bool_to_Prop (is_member v1 (v l))) → ∀i. colouring v1 = decision_spill i → lt i spilled_no 32 ; prop_colouring3: 33 spilled_no = 0 ∨ 34 ∃l.∃v1:vertex. bool_to_Prop (is_member v1 (v l)) ∧ colouring v1 = decision_spill (minus spilled_no 1) 24 35 }. 25 36
Note: See TracChangeset
for help on using the changeset viewer.