1 | |
---|
2 | include "common/FrontEndOps.ma". |
---|
3 | include "common/CostLabel.ma". |
---|
4 | include "basics/lists/list.ma". |
---|
5 | |
---|
6 | (* TODO: consider making the typing stricter. *) |
---|
7 | |
---|
8 | inductive expr : typ → Type[0] ≝ |
---|
9 | | Id : ∀t. ident → expr t |
---|
10 | | Cst : ∀t. constant → expr t |
---|
11 | | Op1 : ∀t,t'. unary_operation t t' → expr t → expr t' |
---|
12 | | Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t' |
---|
13 | | Mem : ∀t,r. expr (ASTptr r) → expr t |
---|
14 | | Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t |
---|
15 | | Ecost : ∀t. costlabel → expr t → expr t. |
---|
16 | |
---|
17 | (* Assert a predicate on every variable or parameter identifier. *) |
---|
18 | let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝ |
---|
19 | match e with |
---|
20 | [ Id t i ⇒ P i t |
---|
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. |
---|
30 | (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q. |
---|
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 | |
---|
39 | inductive stmt : Type[0] ≝ |
---|
40 | | St_skip : stmt |
---|
41 | | St_assign : ∀t. ident → expr t → stmt |
---|
42 | | St_store : ∀t,r. expr (ASTptr r) → expr t → stmt |
---|
43 | (* ident for returned value, expression to identify fn, args. *) |
---|
44 | | St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt |
---|
45 | (* We don't use these at the moment, and they're getting in the way. |
---|
46 | | St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt |
---|
47 | *) |
---|
48 | | St_seq : stmt → stmt → stmt |
---|
49 | | St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt |
---|
50 | | St_loop : stmt → stmt |
---|
51 | | St_block : stmt → stmt |
---|
52 | | St_exit : nat → stmt |
---|
53 | (* expr to switch on, table of 〈switch value, #blocks to exit〉, default *) |
---|
54 | | St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt |
---|
55 | | St_return : option (𝚺t. expr t) → stmt |
---|
56 | | St_label : identifier Label → stmt → stmt |
---|
57 | | St_goto : identifier Label → stmt |
---|
58 | | St_cost : costlabel → stmt → stmt. |
---|
59 | |
---|
60 | let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝ |
---|
61 | match s with |
---|
62 | [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 |
---|
63 | | St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 |
---|
64 | | St_loop s' ⇒ P s ∧ stmt_P P s' |
---|
65 | | St_block s' ⇒ P s ∧ stmt_P P s' |
---|
66 | | St_label _ s' ⇒ P s ∧ stmt_P P s' |
---|
67 | | St_cost _ s' ⇒ P s ∧ stmt_P P s' |
---|
68 | | _ ⇒ P s |
---|
69 | ]. |
---|
70 | |
---|
71 | lemma stmt_P_P : ∀P,s. stmt_P P s → P s. |
---|
72 | #P * normalize /2/ |
---|
73 | [ #s1 #s2 * * /2/ |
---|
74 | | #sz #sg #e #s1 #s2 * * /2/ |
---|
75 | | 3,4: #s * /2/ |
---|
76 | | 5,6: #i #s normalize * /2/ |
---|
77 | ] qed. |
---|
78 | |
---|
79 | (* Assert a predicate on every variable or parameter identifier. *) |
---|
80 | definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝ |
---|
81 | λP,s. |
---|
82 | match s with |
---|
83 | [ St_assign t i e ⇒ P i t ∧ expr_vars ? e P |
---|
84 | | St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P |
---|
85 | | 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 |
---|
86 | (* |
---|
87 | | St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es |
---|
88 | *) |
---|
89 | | St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P |
---|
90 | | St_switch _ _ e _ _ ⇒ expr_vars ? e P |
---|
91 | | St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ] |
---|
92 | | _ ⇒ True |
---|
93 | ]. |
---|
94 | |
---|
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,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s. |
---|
114 | #P #Q #H #s elim s normalize |
---|
115 | [ // |
---|
116 | | #t #id #e * /4/ |
---|
117 | | #t #r #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 | (* |
---|
120 | | #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ] |
---|
121 | *) |
---|
122 | | #s1 #s2 #H1 #H2 * /3/ |
---|
123 | | #sz #sg #e #s1 #s2 #H1 #H2 /5/ |
---|
124 | | 7,8: #s #H1 #H2 /2/ |
---|
125 | | // |
---|
126 | | /5/ |
---|
127 | | * normalize [ // | *; normalize /3/ ] |
---|
128 | | /2/ |
---|
129 | | // |
---|
130 | | /2/ |
---|
131 | ] qed. |
---|
132 | |
---|
133 | lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s. |
---|
134 | #P #Q #H #s elim s normalize /2/ qed. |
---|
135 | |
---|
136 | (* Get labels from a Cminor statement. *) |
---|
137 | let rec labels_of (s:stmt) : list (identifier Label) ≝ |
---|
138 | match s with |
---|
139 | [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
140 | | St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
141 | | St_loop s ⇒ labels_of s |
---|
142 | | St_block s ⇒ labels_of s |
---|
143 | | St_label l s ⇒ l::(labels_of s) |
---|
144 | | St_cost _ s ⇒ labels_of s |
---|
145 | | _ ⇒ [ ] |
---|
146 | ]. |
---|
147 | |
---|
148 | record internal_function : Type[0] ≝ |
---|
149 | { f_return : option typ |
---|
150 | ; f_params : list (ident × typ) |
---|
151 | ; f_vars : list (ident × typ) |
---|
152 | ; f_distinct : distinct_env … (f_params @ f_vars) |
---|
153 | ; f_stacksize : nat |
---|
154 | ; f_body : stmt |
---|
155 | (* Ensure that variables appear in the params and vars list with the |
---|
156 | correct typ; and that all goto labels used are declared. *) |
---|
157 | ; f_inv : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧ |
---|
158 | stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body |
---|
159 | }. |
---|
160 | |
---|
161 | (* We define two closely related versions of Cminor, the first with the original |
---|
162 | initialisation data for global variables, and the second where the code is |
---|
163 | responsible for initialisation and we only give the size of each variable. *) |
---|
164 | |
---|
165 | definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data). |
---|
166 | |
---|
167 | definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat. |
---|