 Timestamp:
 Aug 29, 2011, 2:42:43 PM (9 years ago)
 Location:
 src/ERTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1110 r1124 3 3 include "LTL/LTL.ma". 4 4 5 (*6 5 definition translate_internal ≝ 7 6 λf. … … 14 13 ? 15 14 ?. 16 *)17 15 18 16 definition translate_funct ≝ 
src/ERTL/liveness.ma
r1107 r1124 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 ] … … 100 99 definition lattice_is_maximal: register_lattice → bool ≝ λl. false. 101 100 101 record lattice_property_sig: Type[1] ≝ 102 { 103 lp_type : Type[0]; 104 lp_property : Type[0]; 105 lp_bottom : lp_type; 106 lp_psingleton: register → lp_type; 107 lp_hsingleton: Register → lp_type; 108 lp_join : lp_type → lp_type → lp_type; 109 lp_diff : lp_type → lp_type → lp_type; 110 lp_equal : lp_type → lp_type → bool; 111 lp_is_maximal: lp_type → bool 112 }. 113 114 definition property ≝ 115 mk_lattice_property_sig 116 ((list register) × (list Register)) 117 lattice_property 118 lattice_bottom 119 lattice_psingleton 120 lattice_hsingleton 121 lattice_join 122 lattice_diff 123 lattice_equal 124 lattice_is_maximal. 125 102 126 definition defined: ertl_statement → register_lattice ≝ 103 127 λs. … … 109 133  ertl_st_store _ _ _ _ ⇒ lattice_bottom 110 134  ertl_st_cond _ _ _ ⇒ lattice_bottom 111  ertl_st_return _⇒ lattice_bottom135  ertl_st_return ⇒ lattice_bottom 112 136  ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry 113 137  ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry … … 184 208  ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 185 209  ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 186  ertl_st_return _⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉210  ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 187 211 ]. 188 212 … … 204 228  ertl_st_call_id _ _ _ ⇒ None ? 205 229  ertl_st_cond _ _ _ ⇒ None ? 206  ertl_st_return _⇒ None ?230  ertl_st_return ⇒ None ? 207 231  ertl_st_get_hdw r _ l ⇒ 208 232 if list_set_member register (eq_identifier ?) r pliveafter ∨ … … 292 316 293 317 definition valuation ≝ label → register_lattice. 318 definition rhs ≝ valuation → lattice_property. 319 definition equations ≝ label → rhs. 320 321 axiom fix_lfp: equations → valuation. 322 323 definition livebefore ≝ 324 λint_fun. 325 λlabel. 326 λliveafter: valuation. 327 match lookup ? ? (ertl_if_graph int_fun) label with 328 [ None ⇒ ? 329  Some stmt ⇒ statement_semantics stmt (liveafter label) 330 ]. 331 cases not_implemented (* XXX *) 332 qed. 333 334 definition liveafter ≝ 335 λint_fun. 336 λlivebefore. 337 λlabel. 338 λliveafter: valuation. 339 match lookup ? ? (ertl_if_graph int_fun) label with 340 [ None ⇒ ? 341  Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu. 342 lattice_join (livebefore successor liveafter) accu) 343 lattice_bottom (statement_successors stmt) 344 ]. 345 cases not_implemented (* XXX *) 346 qed. 294 347 295 348 definition analyse: ertl_internal_function → valuation ≝ 296 349 λ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 ?. 350 fix_lfp (liveafter int_fun (livebefore int_fun)).
Note: See TracChangeset
for help on using the changeset viewer.