Last change
on this file since 2982 was
2942,
checked in by sacerdot, 8 years ago

Many changes:
 Coloured graphs are now specified in terms of livebefore
 Type of livebefore changed so that it is now a valuation transformer
 Several axioms can now be inhabited in ERTLptrToLTLProof
Problems:
ERTLtoERTLptrOK is broken beyond my understanding. This pass should have
been unaffected by the changes, but it is not so. Why?

File size:
932 bytes

Rev  Line  

[2693]  1  include "ERTLptr/liveness.ma". 

[1127]  2  

[1229]  3  inductive decision: Type[0] ≝ 

[1232]  4   decision_spill: nat → decision 

[1229]  5   decision_colour: Register → decision. 

 6  

[1423]  7  (* prop_colouring is the non interferece 

 8  prop_colouring 2 and 3 together say that spilled_no is the number of spilled 

 9  registers *) 

[2942]  10  record coloured_graph (before: valuation register_lattice): Type[1] ≝ 

[1423]  11  { colouring: vertex → decision 

 12  ; spilled_no: nat 

[2845]  13  ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → 

[2942]  14  lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2 

[2286]  15  ; prop_spilled_no: (*CSC: the existguarded premise is just to make the proof more general *) 

[2942]  16  ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no 

[1229]  17  }. 

 18  

[2739]  19  definition coloured_graph_computer ≝ 

 20  ∀globals. 

[2942]  21  ∀fn:joint_internal_function ERTLptr globals. 

 22  ∀liveafter. 

 23  coloured_graph (livebefore globals fn liveafter). 

Note: See
TracBrowser
for help on using the repository browser.