Changeset 1153 for Deliverables/D3.3/id-lookup-branch/ERTL
- Timestamp:
- Aug 30, 2011, 6:55:12 PM (10 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 5 edited
- 4 copied
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
- Property svn:mergeinfo changed
/src merged: 1110-1132,1136-1150
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma
r1109 r1153 20 20 | ertl_st_pop: register → label → ertl_statement 21 21 | ertl_st_push: register → label → ertl_statement 22 | ertl_st_addr: register → register → ident → label → ertl_statement 23 (* XXX: changed from O'Caml 22 24 | ertl_st_addr_h: register → ident → label → ertl_statement 23 25 | ertl_st_addr_l: register → ident → label → ertl_statement 26 *) 24 27 | ertl_st_int: register → Byte → label → ertl_statement 25 28 | ertl_st_move: register → register → label → ertl_statement 29 | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement 30 (* XXX: changed from O'Caml 26 31 | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement 27 32 | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement 33 *) 28 34 | ertl_st_op1: Op1 → register → register → label → ertl_statement 29 35 | ertl_st_op2: Op2 → register → register → register → label → ertl_statement … … 32 38 | ertl_st_load: register → register → register → label → ertl_statement 33 39 | ertl_st_store: register → register → register → label → ertl_statement 34 | ertl_st_call_id: ident → Byte→ label → ertl_statement40 | ertl_st_call_id: ident → nat → label → ertl_statement 35 41 | ertl_st_cond: register → label → label → ertl_statement 36 42 | ertl_st_return: ertl_statement. -
Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma
r1091 r1153 2 2 include "ERTL/ERTLToLTLI.ma". 3 3 include "LTL/LTL.ma". 4 include "ERTL/spill.ma". 4 5 5 6 definition translate_internal ≝ 6 7 λf. 7 8 λint_fun: ertl_internal_function. 8 mk_ltl_internal_function ? 9 (ertl_if_luniverse int_fun) 10 (ertl_if_runiverse int_fun) 11 (ertl_if_stacksize int_fun) 12 (ertl_if_graph int_fun) 13 ? 14 ?. 9 10 let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in 11 12 let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in 13 14 let generate stmt = 15 let l = fresh_label () in 16 add_graph l stmt ; 17 l in 18 19 (* Build an interference graph for this function, and color 20 it. Define a function that allows consulting the coloring. *) 21 22 let module G = struct 23 let liveafter, graph = Build.build int_fun 24 let uses = Uses.examine_internal int_fun 25 let verbose = false 26 let () = 27 if verbose then 28 Printf.printf "Starting hardware register allocation for %s.\n" f 29 end in 30 31 let module C = Coloring.Color (G) in 32 33 let lookup r = 34 Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring 35 in 36 37 (* Restrict the interference graph to concern spilled vertices only, 38 and color it again, this time using stack slots as colors. *) 39 40 let module H = struct 41 let graph = Interference.droph (Interference.restrict G.graph (fun v -> 42 match Interference.Vertex.Map.find v C.coloring with 43 | Coloring.Spill -> 44 true 45 | Coloring.Color _ -> 46 false 47 )) 48 let verbose = false 49 let () = 50 if verbose then 51 Printf.printf "Starting stack slot allocation for %s.\n" f 52 end in 53 54 let module S = Spill.Color (H) in 55 56 (* Define a new function that consults both colorings at once. *) 57 58 let lookup r = 59 match lookup r with 60 | Coloring.Spill -> 61 ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring) 62 | Coloring.Color color -> 63 ERTLToLTLI.Color color 64 in 65 66 (* We are now ready to instantiate the functor that deals with the 67 translation of instructions. The reason why we make this a 68 separate functor is purely pedagogical. Smaller modules are 69 easier to understand. *) 70 71 (* We add the additional stack size required for spilled register to the stack 72 size previously required for the function: this is the final stack size 73 required for the locals. *) 74 75 let locals = S.locals + int_fun.ERTL.f_stacksize in 76 77 (* The full stack size is then the size of the locals in the stack plus the 78 size of the formal parameters of the function. *) 79 80 let stacksize = int_fun.ERTL.f_params + locals in 81 82 let module I = ERTLToLTLI.Make (struct 83 let lookup = lookup 84 let generate = generate 85 let fresh_label = fresh_label 86 let add_graph = add_graph 87 let locals = locals 88 let stacksize = stacksize 89 end) in 90 91 (* Translate the instructions in the existing control flow graph. 92 Pure instructions whose destination pseudo-register is dead are 93 eliminated on the fly. *) 94 95 let () = 96 Label.Map.iter (fun label stmt -> 97 let stmt = 98 match Liveness.eliminable (G.liveafter label) stmt with 99 | Some successor -> 100 LTL.St_skip successor 101 | None -> 102 I.translate_statement stmt 103 in 104 graph := Label.Map.add label stmt !graph 105 ) int_fun.ERTL.f_graph 106 in 107 108 (* Build a [LTL] function. *) 109 110 { 111 LTL.f_luniverse = int_fun.ERTL.f_luniverse; 112 LTL.f_stacksize = stacksize ; 113 LTL.f_entry = int_fun.ERTL.f_entry; 114 LTL.f_exit = int_fun.ERTL.f_exit; 115 LTL.f_graph = !graph 116 } 15 117 16 118 definition translate_funct ≝ -
Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTLI.ma
r1109 r1153 83 83 [ decision_colour src_hwr ⇒ 84 84 if eq_Register dest_hwr src_hwr then 85 joint_st_ sequential ? globals (joint_instr_skip globals)l85 joint_st_goto ? globals l 86 86 else 87 87 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in … … 94 94 | decision_spill src_off ⇒ 95 95 if eq_bv ? dest_off src_off then 96 joint_st_ sequential ? globals (joint_instr_skip globals)l96 joint_st_goto ? globals l 97 97 else 98 98 let temp_hwr ≝ RegisterSST in … … 106 106 λl. 107 107 if eq_nat stacksize 0 then 108 joint_st_ sequential ? globals (joint_instr_skip globals)l108 joint_st_goto ? globals l 109 109 else 110 110 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in … … 122 122 λl. 123 123 if eq_nat stacksize 0 then 124 joint_st_ sequential ? globals (joint_instr_skip globals)l124 joint_st_goto ? globals l 125 125 else 126 126 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in … … 135 135 λstmt: ertl_statement. 136 136 match stmt with 137 [ ertl_st_skip l ⇒ joint_st_ sequential ? globals (joint_instr_skip globals)l137 [ ertl_st_skip l ⇒ joint_st_goto ? globals l 138 138 | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l 139 139 | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l … … 155 155 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in 156 156 let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 157 joint_st_ sequential ? globals (joint_instr_skip globals)l158 | ertl_st_addr _h rx l ⇒159 let 〈hdw , l〉 ≝ write globals rl in160 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw ) l) in157 joint_st_goto ? globals l 158 | ertl_st_addr rl rh x l ⇒ 159 let 〈hdw1, l〉 ≝ write globals rh l in 160 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in 161 161 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in 162 joint_st_sequential ? globals (joint_instr_address globals x ?) l 163 | ertl_st_addr_l r x l ⇒ 164 let 〈hdw, l〉 ≝ write globals r l in 165 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 162 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in 163 let 〈hdw2, l〉 ≝ write globals rl l in 164 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in 166 165 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in 167 166 joint_st_sequential ? globals (joint_instr_address globals x ?) l 167 (* | ertl_st_addr_h r x l ⇒ 168 let 〈hdw, l〉 ≝ write globals r l in 169 let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in 170 let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in 171 ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) 172 | ertl_st_addr_l r x l ⇒ 173 let 〈hdw, l〉 ≝ write globals r l in 174 let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in 175 let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in 176 ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) 177 *) 168 178 | ertl_st_int r i l ⇒ 169 179 let 〈hdw, l〉 ≝ write globals r l in 170 180 joint_st_sequential ? globals (joint_instr_int globals hdw i) l 171 181 | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l 182 | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒ 183 let 〈hdw, l〉 ≝ write globals destr1 l in 184 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 185 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in 186 let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 187 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 188 let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 189 let l ≝ generate globals (joint_st_goto ? globals l) in 190 let 〈hdw, l〉 ≝ write globals destr2 l in 191 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 192 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in 193 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in 194 let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 195 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 196 let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 197 joint_st_goto ? globals l 198 (* 172 199 | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒ 173 200 let 〈hdw, l〉 ≝ write globals destr l in … … 177 204 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 178 205 let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 179 joint_st_ sequential ? globals (joint_instr_skip globals)l206 joint_st_goto ? globals l 180 207 | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒ 181 208 let 〈hdw, l〉 ≝ write globals destr l in … … 186 213 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 187 214 let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 188 joint_st_sequential ? globals (joint_instr_skip globals) l 215 joint_st_goto ? globals l 216 *) 189 217 | ertl_st_op1 op1 destr srcr l ⇒ 190 218 let 〈hdw, l〉 ≝ write globals destr l in … … 192 220 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in 193 221 let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 194 joint_st_ sequential ? globals (joint_instr_skip globals)l222 joint_st_goto ? globals l 195 223 | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒ 196 224 let 〈hdw, l〉 ≝ write globals destr l in … … 200 228 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 201 229 let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 202 joint_st_ sequential ? globals (joint_instr_skip globals)l230 joint_st_goto ? globals l 203 231 | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l 204 232 | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l … … 213 241 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in 214 242 let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 215 joint_st_ sequential ? globals (joint_instr_skip globals)l243 joint_st_goto ? globals l 216 244 | ertl_st_store addr1 addr2 srcr l ⇒ 217 245 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in … … 225 253 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in 226 254 let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 227 joint_st_ sequential ? globals (joint_instr_skip globals)l228 | ertl_st_call_id f ignore l ⇒ 255 joint_st_goto ? globals l 256 | ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l 229 257 | ertl_st_cond srcr lbl_true lbl_false ⇒ 230 258 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in 231 259 let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 232 joint_st_ sequential ? globals (joint_instr_skip globals)l260 joint_st_goto ? globals l 233 261 | ertl_st_return ⇒ joint_st_return ? globals 234 262 ]. -
Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma
r1109 r1153 1 include "utilities/Fix.ma".2 1 include "ASM/Util.ma". 3 2 include "ERTL/ERTL.ma". … … 38 37 λs: ertl_statement. 39 38 match s with 40 [ ertl_st_return _⇒ [ ]39 [ ertl_st_return ⇒ [ ] 41 40 | ertl_st_skip l ⇒ [ l ] 42 41 | ertl_st_comment c l ⇒ [ l ] … … 50 49 | ertl_st_push _ l ⇒ [ l ] 51 50 | ertl_st_pop _ l ⇒ [ l ] 52 | ertl_st_addr_h _ _ l ⇒ [ l ] 53 | ertl_st_addr_l _ _ l ⇒ [ l ] 51 | ertl_st_addr _ _ _ l ⇒ [ l ] 54 52 | ertl_st_int _ _ l ⇒ [ l ] 55 53 | ertl_st_move _ _ l ⇒ [ l ] 56 | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ] 57 | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ] 54 | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ] 58 55 | ertl_st_op1 _ _ _ l ⇒ [ l ] 59 56 | ertl_st_op2 _ _ _ _ l ⇒ [ l ] … … 100 97 definition lattice_is_maximal: register_lattice → bool ≝ λl. false. 101 98 99 record lattice_property_sig: Type[1] ≝ 100 { 101 lp_type : Type[0]; 102 lp_property : Type[0]; 103 lp_bottom : lp_type; 104 lp_psingleton: register → lp_type; 105 lp_hsingleton: Register → lp_type; 106 lp_join : lp_type → lp_type → lp_type; 107 lp_diff : lp_type → lp_type → lp_type; 108 lp_equal : lp_type → lp_type → bool; 109 lp_is_maximal: lp_type → bool 110 }. 111 112 definition property ≝ 113 mk_lattice_property_sig 114 ((list register) × (list Register)) 115 lattice_property 116 lattice_bottom 117 lattice_psingleton 118 lattice_hsingleton 119 lattice_join 120 lattice_diff 121 lattice_equal 122 lattice_is_maximal. 123 102 124 definition defined: ertl_statement → register_lattice ≝ 103 125 λs. … … 109 131 | ertl_st_store _ _ _ _ ⇒ lattice_bottom 110 132 | ertl_st_cond _ _ _ ⇒ lattice_bottom 111 | ertl_st_return _⇒ lattice_bottom133 | ertl_st_return ⇒ lattice_bottom 112 134 | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry 113 135 | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry … … 124 146 | ertl_st_pop r _ ⇒ lattice_psingleton r 125 147 | ertl_st_int r _ _ ⇒ lattice_psingleton r 126 | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r 127 | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r 148 | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 128 149 | ertl_st_move r _ _ ⇒ lattice_psingleton r 129 | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r130 | ertl_st_opaccs _b _ r _ _ _ ⇒ lattice_psingleton r150 (* XXX: change from o'caml *) 151 | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 131 152 | ertl_st_load r _ _ _ ⇒ lattice_psingleton r 132 153 | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r … … 156 177 | ertl_st_frame_size _ _ ⇒ lattice_bottom 157 178 | ertl_st_pop _ _ ⇒ lattice_bottom 158 | ertl_st_addr_h _ _ _ ⇒ lattice_bottom 159 | ertl_st_addr_l _ _ _ ⇒ lattice_bottom 179 | ertl_st_addr _ _ _ _ ⇒ lattice_bottom 160 180 | ertl_st_int _ _ _ ⇒ lattice_bottom 161 181 | ertl_st_clear_carry _ ⇒ lattice_bottom … … 163 183 (* Reads the hardware registers that are used to pass parameters. *) 164 184 | ertl_st_call_id _ nparams _ ⇒ 165 〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams)RegisterParameters)〉185 〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉 166 186 | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r 167 187 | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r … … 177 197 | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 178 198 ] 179 | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 180 | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 199 | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2) 181 200 | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 182 201 | ertl_st_store r1 r2 r3 _ ⇒ … … 184 203 | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 185 204 | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 186 | ertl_st_return _⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉205 | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 187 206 ]. 188 207 … … 204 223 | ertl_st_call_id _ _ _ ⇒ None ? 205 224 | ertl_st_cond _ _ _ ⇒ None ? 206 | ertl_st_return _⇒ None ?225 | ertl_st_return ⇒ None ? 207 226 | ertl_st_get_hdw r _ l ⇒ 208 227 if list_set_member register (eq_identifier ?) r pliveafter ∨ … … 223 242 else 224 243 Some ? l 225 | ertl_st_addr_h r _ l ⇒ 226 if list_set_member register (eq_identifier ?) r pliveafter ∨ 227 list_set_member Register eq_Register RegisterCarry hliveafter then 228 None ? 229 else 230 Some ? l 231 | ertl_st_addr_l r _ l ⇒ 232 if list_set_member register (eq_identifier ?) r pliveafter ∨ 244 | ertl_st_addr r1 r2 _ l ⇒ 245 if list_set_member register (eq_identifier ?) r1 pliveafter ∨ 246 list_set_member register (eq_identifier ?) r2 pliveafter ∨ 233 247 list_set_member Register eq_Register RegisterCarry hliveafter then 234 248 None ? … … 241 255 else 242 256 Some ? l 243 | ertl_st_opaccs_a _ r _ _ l ⇒ 244 if list_set_member register (eq_identifier ?) r pliveafter ∨ 245 list_set_member Register eq_Register RegisterCarry hliveafter then 246 None ? 247 else 248 Some ? l 249 | ertl_st_opaccs_b _ r _ _ l ⇒ 250 if list_set_member register (eq_identifier ?) r pliveafter ∨ 257 | ertl_st_opaccs _ d1 d2 _ _ l ⇒ 258 if list_set_member register (eq_identifier ?) d1 pliveafter ∨ 259 list_set_member register (eq_identifier ?) d2 pliveafter ∨ 251 260 list_set_member Register eq_Register RegisterCarry hliveafter then 252 261 None ? … … 292 301 293 302 definition valuation ≝ label → register_lattice. 303 definition rhs ≝ valuation → lattice_property. 304 definition equations ≝ label → rhs. 305 306 axiom fix_lfp: equations → valuation. 307 308 definition livebefore ≝ 309 λint_fun. 310 λlabel. 311 λliveafter: valuation. 312 match lookup ? ? (ertl_if_graph int_fun) label with 313 [ None ⇒ ? 314 | Some stmt ⇒ statement_semantics stmt (liveafter label) 315 ]. 316 cases not_implemented (* XXX *) 317 qed. 318 319 definition liveafter ≝ 320 λint_fun. 321 λlivebefore. 322 λlabel. 323 λliveafter: valuation. 324 match lookup ? ? (ertl_if_graph int_fun) label with 325 [ None ⇒ ? 326 | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu. 327 lattice_join (livebefore successor liveafter) accu) 328 lattice_bottom (statement_successors stmt) 329 ]. 330 cases not_implemented (* XXX *) 331 qed. 294 332 295 333 definition analyse: ertl_internal_function → valuation ≝ 296 334 λint_fun. 297 let livebefore ≝ λlabel. λliveafter: valuation. 298 match lookup ? ? (ertl_if_graph int_fun) label with 299 [ None ⇒ ? 300 | Some stmt ⇒ statement_semantics stmt (liveafter label) 301 ] 302 in 303 let liveafter ≝ λlabel. λliveafter: valuation. 304 match lookup ? ? (ertl_if_graph int_fun) label with 305 [ None ⇒ ? 306 | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu. 307 lattice_join (livebefore successor liveafter) accu) 308 lattice_bottom (statement_successors stmt) 309 ] 310 in ?. 335 fix_lfp (liveafter int_fun (livebefore int_fun)).
Note: See TracChangeset
for help on using the changeset viewer.