[751] | 1 | |
---|
| 2 | include "common/FrontEndOps.ma". |
---|
| 3 | include "common/CostLabel.ma". |
---|
[1603] | 4 | include "basics/lists/list.ma". |
---|
[751] | 5 | |
---|
[880] | 6 | (* TODO: consider making the typing stricter. *) |
---|
[751] | 7 | |
---|
[880] | 8 | inductive expr : typ → Type[0] ≝ |
---|
| 9 | | Id : ∀t. ident → expr t |
---|
| 10 | | Cst : ∀t. constant → expr t |
---|
[1369] | 11 | | Op1 : ∀t,t'. unary_operation t t' → expr t → expr t' |
---|
[880] | 12 | | Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t' |
---|
[881] | 13 | | Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t |
---|
[880] | 14 | | Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t |
---|
| 15 | | Ecost : ∀t. costlabel → expr t → expr t. |
---|
| 16 | |
---|
[1316] | 17 | (* Assert a predicate on every variable or parameter identifier. *) |
---|
[1626] | 18 | let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝ |
---|
[1316] | 19 | match e with |
---|
[1626] | 20 | [ Id t i ⇒ P i t |
---|
[1316] | 21 | | Cst _ _ ⇒ True |
---|
| 22 | | Op1 _ _ _ e ⇒ expr_vars ? e P |
---|
| 23 | | Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P |
---|
| 24 | | Mem _ _ _ e ⇒ expr_vars ? e P |
---|
| 25 | | Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P |
---|
| 26 | | Ecost _ _ e ⇒ expr_vars ? e P |
---|
| 27 | ]. |
---|
| 28 | |
---|
| 29 | lemma expr_vars_mp : ∀t,e,P,Q. |
---|
[1626] | 30 | (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q. |
---|
[1316] | 31 | #t0 #e elim e normalize /3/ |
---|
| 32 | [ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2 |
---|
| 33 | % /3/ |
---|
| 34 | | #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/ |
---|
| 35 | ] qed. |
---|
| 36 | |
---|
| 37 | axiom Label : String. |
---|
| 38 | |
---|
[751] | 39 | inductive stmt : Type[0] ≝ |
---|
| 40 | | St_skip : stmt |
---|
[880] | 41 | | St_assign : ∀t. ident → expr t → stmt |
---|
[881] | 42 | | St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt |
---|
[816] | 43 | (* ident for returned value, expression to identify fn, args. *) |
---|
[1626] | 44 | | St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt |
---|
[1605] | 45 | | St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt |
---|
[751] | 46 | | St_seq : stmt → stmt → stmt |
---|
[880] | 47 | | St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt |
---|
[751] | 48 | | St_loop : stmt → stmt |
---|
| 49 | | St_block : stmt → stmt |
---|
| 50 | | St_exit : nat → stmt |
---|
| 51 | (* expr to switch on, table of 〈switch value, #blocks to exit〉, default *) |
---|
[961] | 52 | | St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt |
---|
[1605] | 53 | | St_return : option (𝚺t. expr t) → stmt |
---|
[1316] | 54 | | St_label : identifier Label → stmt → stmt |
---|
| 55 | | St_goto : identifier Label → stmt |
---|
[751] | 56 | | St_cost : costlabel → stmt → stmt. |
---|
| 57 | |
---|
[1316] | 58 | let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝ |
---|
| 59 | match s with |
---|
| 60 | [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 |
---|
| 61 | | St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 |
---|
| 62 | | St_loop s' ⇒ P s ∧ stmt_P P s' |
---|
| 63 | | St_block s' ⇒ P s ∧ stmt_P P s' |
---|
| 64 | | St_label _ s' ⇒ P s ∧ stmt_P P s' |
---|
| 65 | | St_cost _ s' ⇒ P s ∧ stmt_P P s' |
---|
| 66 | | _ ⇒ P s |
---|
| 67 | ]. |
---|
| 68 | |
---|
| 69 | lemma stmt_P_P : ∀P,s. stmt_P P s → P s. |
---|
| 70 | #P * normalize /2/ |
---|
| 71 | [ #s1 #s2 * * /2/ |
---|
| 72 | | #sz #sg #e #s1 #s2 * * /2/ |
---|
| 73 | | 3,4: #s * /2/ |
---|
| 74 | | 5,6: #i #s normalize * /2/ |
---|
| 75 | ] qed. |
---|
| 76 | |
---|
| 77 | (* Assert a predicate on every variable or parameter identifier. *) |
---|
[1626] | 78 | definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝ |
---|
[1316] | 79 | λP,s. |
---|
| 80 | match s with |
---|
[1626] | 81 | [ St_assign t i e ⇒ P i t ∧ expr_vars ? e P |
---|
[1316] | 82 | | St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P |
---|
[1626] | 83 | | St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es |
---|
[1603] | 84 | | St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es |
---|
[1316] | 85 | | St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P |
---|
| 86 | | St_switch _ _ e _ _ ⇒ expr_vars ? e P |
---|
[1603] | 87 | | St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ] |
---|
[1316] | 88 | | _ ⇒ True |
---|
| 89 | ]. |
---|
| 90 | |
---|
| 91 | definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝ |
---|
| 92 | λP,s. |
---|
| 93 | match s with |
---|
| 94 | [ St_label l _ ⇒ P l |
---|
| 95 | | St_goto l ⇒ P l |
---|
| 96 | | _ ⇒ True |
---|
| 97 | ]. |
---|
| 98 | |
---|
| 99 | lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s. |
---|
| 100 | #P #Q #H #s elim s /2/ |
---|
| 101 | [ #s1 #s2 #H1 #H2 normalize * * /4/ |
---|
| 102 | | #sz #sg #e #s1 #s2 #H1 #H2 * * /5/ |
---|
| 103 | | #s #H * /5/ |
---|
| 104 | | #s #H * /5/ |
---|
| 105 | | #l #s #H * /5/ |
---|
| 106 | | #l #s #H * /5/ |
---|
| 107 | ] qed. |
---|
| 108 | |
---|
[1626] | 109 | lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s. |
---|
[1316] | 110 | #P #Q #H #s elim s normalize |
---|
| 111 | [ // |
---|
| 112 | | #t #id #e * /4/ |
---|
| 113 | | #t #r #q #e1 #e2 * /4/ |
---|
| 114 | | * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ] |
---|
| 115 | | #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ] |
---|
| 116 | | #s1 #s2 #H1 #H2 * /3/ |
---|
| 117 | | #sz #sg #e #s1 #s2 #H1 #H2 /5/ |
---|
| 118 | | 8,9: #s #H1 #H2 /2/ |
---|
| 119 | | // |
---|
| 120 | | /5/ |
---|
| 121 | | * normalize [ // | *; normalize /3/ ] |
---|
| 122 | | /2/ |
---|
| 123 | | // |
---|
| 124 | | /2/ |
---|
| 125 | ] qed. |
---|
| 126 | |
---|
| 127 | lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s. |
---|
| 128 | #P #Q #H #s elim s normalize /2/ qed. |
---|
| 129 | |
---|
| 130 | (* Get labels from a Cminor statement. *) |
---|
| 131 | let rec labels_of (s:stmt) : list (identifier Label) ≝ |
---|
| 132 | match s with |
---|
| 133 | [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
| 134 | | St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
| 135 | | St_loop s ⇒ labels_of s |
---|
| 136 | | St_block s ⇒ labels_of s |
---|
| 137 | | St_label l s ⇒ l::(labels_of s) |
---|
| 138 | | St_cost _ s ⇒ labels_of s |
---|
| 139 | | _ ⇒ [ ] |
---|
| 140 | ]. |
---|
| 141 | |
---|
[751] | 142 | record internal_function : Type[0] ≝ |
---|
[886] | 143 | { f_return : option typ |
---|
| 144 | ; f_params : list (ident × typ) |
---|
| 145 | ; f_vars : list (ident × typ) |
---|
[751] | 146 | ; f_stacksize : nat |
---|
| 147 | ; f_body : stmt |
---|
[1626] | 148 | (* Ensure that variables appear in the params and vars list with the |
---|
| 149 | correct typ; and that all goto labels used are declared. *) |
---|
| 150 | ; f_inv : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧ |
---|
[1316] | 151 | stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body |
---|
[751] | 152 | }. |
---|
| 153 | |
---|
[1147] | 154 | (* We define two closely related versions of Cminor, the first with the original |
---|
| 155 | initialisation data for global variables, and the second where the code is |
---|
| 156 | responsible for initialisation and we only give the size of each variable. *) |
---|
| 157 | |
---|
[1224] | 158 | definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data). |
---|
[1139] | 159 | |
---|
[1224] | 160 | definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat. |
---|