|
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
|
| Line | |
|---|
| 1 | include "ERTLptr/liveness.ma". |
|---|
| 2 | |
|---|
| 3 | inductive decision: Type[0] ≝ |
|---|
| 4 | | decision_spill: nat → decision |
|---|
| 5 | | decision_colour: Register → decision. |
|---|
| 6 | |
|---|
| 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 *) |
|---|
| 10 | record coloured_graph (before: valuation register_lattice): Type[1] ≝ |
|---|
| 11 | { colouring: vertex → decision |
|---|
| 12 | ; spilled_no: nat |
|---|
| 13 | ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → |
|---|
| 14 | lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2 |
|---|
| 15 | ; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *) |
|---|
| 16 | ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no |
|---|
| 17 | }. |
|---|
| 18 | |
|---|
| 19 | definition coloured_graph_computer ≝ |
|---|
| 20 | ∀globals. |
|---|
| 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.
