| 1 | include "basics/logic.ma". |
|---|
| 2 | |
|---|
| 3 | include "common/AST.ma". |
|---|
| 4 | include "common/CostLabel.ma". |
|---|
| 5 | include "common/FrontEndOps.ma". |
|---|
| 6 | include "common/Registers.ma". |
|---|
| 7 | |
|---|
| 8 | include "ASM/Vector.ma". |
|---|
| 9 | include "common/Graphs.ma". |
|---|
| 10 | |
|---|
| 11 | inductive statement : Type[0] ≝ |
|---|
| 12 | | St_skip : label → statement |
|---|
| 13 | | St_cost : costlabel → label → statement |
|---|
| 14 | | St_const : register → constant → label → statement |
|---|
| 15 | | St_op1 : unary_operation → register → register → label → statement (* destination source *) |
|---|
| 16 | | St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *) |
|---|
| 17 | | St_load : memory_chunk → register → register → label → statement |
|---|
| 18 | | St_store : memory_chunk → register → register → label → statement |
|---|
| 19 | | St_call_id : ident → list register → option register → label → statement |
|---|
| 20 | | St_call_ptr : register → list register → option register → label → statement |
|---|
| 21 | | St_tailcall_id : ident → list register → statement |
|---|
| 22 | | St_tailcall_ptr : register → list register → statement |
|---|
| 23 | | St_cond : register → label → label → statement |
|---|
| 24 | | St_jumptable : register → list label → statement |
|---|
| 25 | | St_return : statement |
|---|
| 26 | . |
|---|
| 27 | |
|---|
| 28 | definition labels_P : (label → Prop) → statement → Prop ≝ |
|---|
| 29 | λP,s. match s with |
|---|
| 30 | [ St_skip l ⇒ P l |
|---|
| 31 | | St_cost _ l ⇒ P l |
|---|
| 32 | | St_const _ _ l ⇒ P l |
|---|
| 33 | | St_op1 _ _ _ l ⇒ P l |
|---|
| 34 | | St_op2 _ _ _ _ l ⇒ P l |
|---|
| 35 | | St_load _ _ _ l ⇒ P l |
|---|
| 36 | | St_store _ _ _ l ⇒ P l |
|---|
| 37 | | St_call_id _ _ _ l ⇒ P l |
|---|
| 38 | | St_call_ptr _ _ _ l ⇒ P l |
|---|
| 39 | | St_tailcall_id _ _ ⇒ True |
|---|
| 40 | | St_tailcall_ptr _ _ ⇒ True |
|---|
| 41 | | St_cond _ l1 l2 ⇒ P l1 ∧ P l2 |
|---|
| 42 | | St_jumptable _ ls ⇒ All ? P ls |
|---|
| 43 | | St_return ⇒ True |
|---|
| 44 | ]. |
|---|
| 45 | |
|---|
| 46 | lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s. |
|---|
| 47 | #P #Q #H * /3/ |
|---|
| 48 | #r #l #l' * /3/ |
|---|
| 49 | qed. |
|---|
| 50 | |
|---|
| 51 | definition labels_present : graph statement → statement → Prop ≝ |
|---|
| 52 | λg,s. labels_P (present ?? g) s. |
|---|
| 53 | |
|---|
| 54 | definition graph_closed : graph statement → Prop ≝ |
|---|
| 55 | λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s. |
|---|
| 56 | |
|---|
| 57 | record internal_function : Type[0] ≝ |
|---|
| 58 | { f_labgen : universe LabelTag |
|---|
| 59 | ; f_reggen : universe RegisterTag |
|---|
| 60 | ; f_result : option (register × typ) |
|---|
| 61 | ; f_params : list (register × typ) |
|---|
| 62 | ; f_locals : list (register × typ) |
|---|
| 63 | ; f_stacksize : nat |
|---|
| 64 | ; f_graph : graph statement |
|---|
| 65 | ; f_closed : graph_closed f_graph |
|---|
| 66 | ; f_entry : Σl:label. present ?? f_graph l |
|---|
| 67 | ; f_exit : Σl:label. present ?? f_graph l |
|---|
| 68 | }. |
|---|
| 69 | |
|---|
| 70 | (* Note that the global variables will be initialised by the code in main |
|---|
| 71 | by this stage, so the only initialisation data is the amount of space to |
|---|
| 72 | allocate. *) |
|---|
| 73 | |
|---|
| 74 | definition RTLabs_program ≝ program (λ_.fundef internal_function) nat. |
|---|
