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