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