[639] | 1 | include "basics/logic.ma". |
---|
| 2 | |
---|
[747] | 3 | include "common/AST.ma". |
---|
[720] | 4 | include "common/CostLabel.ma". |
---|
[702] | 5 | include "common/FrontEndOps.ma". |
---|
| 6 | include "common/Registers.ma". |
---|
[639] | 7 | |
---|
[702] | 8 | include "ASM/Vector.ma". |
---|
| 9 | include "common/Graphs.ma". |
---|
[639] | 10 | |
---|
| 11 | inductive statement : Type[0] ≝ |
---|
| 12 | | St_skip : label → statement |
---|
| 13 | | St_cost : costlabel → label → statement |
---|
[1878] | 14 | | St_const : ∀t. register → constant t → label → statement |
---|
| 15 | | St_op1 : ∀t',t. unary_operation t t' → register → register → label → statement (* destination source *) |
---|
| 16 | | St_op2 : ∀t',t1,t2. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *) |
---|
[1872] | 17 | | St_load : typ → register → register → label → statement |
---|
| 18 | | St_store : typ → register → register → label → statement |
---|
[816] | 19 | | St_call_id : ident → list register → option register → label → statement |
---|
| 20 | | St_call_ptr : register → list register → option register → label → statement |
---|
[1680] | 21 | (* We're not using these just now, and they'd make the Traces.ma proofs more difficult. |
---|
[816] | 22 | | St_tailcall_id : ident → list register → statement |
---|
| 23 | | St_tailcall_ptr : register → list register → statement |
---|
[1680] | 24 | *) |
---|
[888] | 25 | | St_cond : register → label → label → statement |
---|
[765] | 26 | | St_return : statement |
---|
[639] | 27 | . |
---|
| 28 | |
---|
[1626] | 29 | definition env_has : list (register × typ) → register → typ → Prop ≝ |
---|
| 30 | λl,r,t. Exists ? (λx. 〈r,t〉 = x) l. |
---|
| 31 | |
---|
| 32 | definition statement_typed : list (register × typ) → statement → Prop ≝ |
---|
| 33 | λe,s. match s with |
---|
[1878] | 34 | [ St_const t r _ _ ⇒ env_has e r t |
---|
| 35 | | St_op1 t' t _ r' r _ ⇒ env_has e r' t' ∧ env_has e r t |
---|
| 36 | | St_op2 t' t1 t2 _ r' r1 r2 _ ⇒ env_has e r1 t1 ∧ env_has e r2 t2 ∧ env_has e r' t' |
---|
[2287] | 37 | | St_load t' addr dst _ ⇒ env_has e dst t' ∧ env_has e addr ASTptr |
---|
| 38 | | St_store t' addr src _ ⇒ env_has e src t' ∧ env_has e addr ASTptr |
---|
[2292] | 39 | | St_call_id id args dst _ ⇒ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True]) |
---|
| 40 | | St_call_ptr fnptr args dst _ ⇒ env_has e fnptr ASTptr ∧ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True]) |
---|
| 41 | | St_cond r _ _ ⇒ ∃t. env_has e r t |
---|
[1626] | 42 | | _ ⇒ True |
---|
| 43 | ]. |
---|
| 44 | |
---|
[1316] | 45 | definition labels_P : (label → Prop) → statement → Prop ≝ |
---|
| 46 | λP,s. match s with |
---|
| 47 | [ St_skip l ⇒ P l |
---|
| 48 | | St_cost _ l ⇒ P l |
---|
[1878] | 49 | | St_const _ _ _ l ⇒ P l |
---|
[1369] | 50 | | St_op1 _ _ _ _ _ l ⇒ P l |
---|
[1872] | 51 | | St_op2 _ _ _ _ _ _ _ l ⇒ P l |
---|
[1316] | 52 | | St_load _ _ _ l ⇒ P l |
---|
| 53 | | St_store _ _ _ l ⇒ P l |
---|
| 54 | | St_call_id _ _ _ l ⇒ P l |
---|
| 55 | | St_call_ptr _ _ _ l ⇒ P l |
---|
[1680] | 56 | (* |
---|
[1316] | 57 | | St_tailcall_id _ _ ⇒ True |
---|
| 58 | | St_tailcall_ptr _ _ ⇒ True |
---|
[1680] | 59 | *) |
---|
[1316] | 60 | | St_cond _ l1 l2 ⇒ P l1 ∧ P l2 |
---|
| 61 | | St_return ⇒ True |
---|
| 62 | ]. |
---|
| 63 | |
---|
| 64 | lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s. |
---|
| 65 | #P #Q #H * /3/ |
---|
| 66 | #r #l #l' * /3/ |
---|
| 67 | qed. |
---|
| 68 | |
---|
| 69 | definition labels_present : graph statement → statement → Prop ≝ |
---|
| 70 | λg,s. labels_P (present ?? g) s. |
---|
| 71 | |
---|
[1626] | 72 | definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝ |
---|
| 73 | λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n. |
---|
| 74 | |
---|
[1316] | 75 | definition graph_closed : graph statement → Prop ≝ |
---|
[1626] | 76 | λg. forall_nodes ? (labels_present g) g. |
---|
| 77 | definition graph_typed : list (register × typ) → graph statement → Prop ≝ |
---|
| 78 | λe. forall_nodes ? (statement_typed e). |
---|
[1316] | 79 | |
---|
[639] | 80 | record internal_function : Type[0] ≝ |
---|
[738] | 81 | { f_labgen : universe LabelTag |
---|
| 82 | ; f_reggen : universe RegisterTag |
---|
[887] | 83 | ; f_result : option (register × typ) |
---|
| 84 | ; f_params : list (register × typ) |
---|
| 85 | ; f_locals : list (register × typ) |
---|
[639] | 86 | ; f_stacksize : nat |
---|
| 87 | ; f_graph : graph statement |
---|
[1316] | 88 | ; f_closed : graph_closed f_graph |
---|
[1626] | 89 | ; f_typed : graph_typed (f_locals @ f_params) f_graph |
---|
[1316] | 90 | ; f_entry : Σl:label. present ?? f_graph l |
---|
| 91 | ; f_exit : Σl:label. present ?? f_graph l |
---|
[639] | 92 | }. |
---|
| 93 | |
---|
[764] | 94 | (* Note that the global variables will be initialised by the code in main |
---|
[1139] | 95 | by this stage, so the only initialisation data is the amount of space to |
---|
| 96 | allocate. *) |
---|
[639] | 97 | |
---|
[1675] | 98 | definition RTLabs_program ≝ program (λ_.fundef internal_function) nat. |
---|
| 99 | |
---|
| 100 | |
---|
| 101 | |
---|
| 102 | |
---|