source: Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma @ 1100

Last change on this file since 1100 was 1100, checked in by campbell, 9 years ago

Finally show that labels in generated Cminor programs are properly defined
on branch.

File size: 45.6 KB
Line 
1
2include "Clight/Csyntax.ma".
3include "Clight/TypeComparison.ma".
4include "utilities/lists.ma".
5(*
6let rec mem_vars_expr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
7match e with
8[ Expr ed ty ⇒
9    match ed with
10    [ Ederef e1 ⇒ mem_vars_expr mem_vars e1
11    | Eaddrof e1 ⇒ mem_vars_addr mem_vars e1
12    | Eunop _ e1 ⇒ mem_vars_expr mem_vars e1
13    | Ebinop _ e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
14                       mem_vars_expr mem_vars e2
15    | Ecast _ e1 ⇒ mem_vars_expr mem_vars e1
16    | Econdition e1 e2 e3 ⇒ mem_vars_expr mem_vars e1 ∧
17                            mem_vars_expr mem_vars e2 ∧
18                            mem_vars_expr mem_vars e3
19    | Eandbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
20                       mem_vars_expr mem_vars e2
21    | Eorbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
22                      mem_vars_expr mem_vars e2
23    | Efield e1 _ ⇒ mem_vars_expr mem_vars e1
24    | Ecost _ e1 ⇒ mem_vars_expr mem_vars e1
25    | _ ⇒ True
26    ]
27]
28and mem_vars_addr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
29match e with
30[ Expr ed ty ⇒
31    match ed with
32    [ Evar x ⇒ mem_set ? mem_vars x = true
33    | Ederef e1 ⇒ mem_vars_expr mem_vars e1
34    | Efield e1 _ ⇒ mem_vars_addr mem_vars e1
35    | _ ⇒ False (* not an lvalue *)
36    ]
37].
38
39let rec mem_vars_stmt (mem_vars:identifier_set SymbolTag) (s:statement) on s : Prop ≝
40match s with
41[ Sskip ⇒ True
42| Sassign e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
43                  mem_vars_expr mem_vars e2
44| Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ] ∧
45                    mem_vars_expr mem_vars e2 ∧
46                    All ? (mem_vars_expr mem_vars) es
47| Ssequence s1 s2 ⇒ mem_vars_stmt mem_vars s1 ∧
48                    mem_vars_stmt mem_vars s2
49| Sifthenelse e1 s1 s2 ⇒ mem_vars_expr mem_vars e1 ∧
50                         mem_vars_stmt mem_vars s1 ∧
51                         mem_vars_stmt mem_vars s2
52| Swhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧
53                 mem_vars_stmt mem_vars s1
54| Sdowhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧
55                   mem_vars_stmt mem_vars s1
56| Sfor s1 e1 s2 s3 ⇒ mem_vars_stmt mem_vars s1 ∧
57                     mem_vars_expr mem_vars e1 ∧
58                     mem_vars_stmt mem_vars s2 ∧
59                     mem_vars_stmt mem_vars s3
60| Sbreak ⇒ True
61| Scontinue ⇒ True
62| Sreturn oe1 ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ]
63| Sswitch e1 ls ⇒ mem_vars_expr mem_vars e1 ∧
64                  mem_vars_ls mem_vars ls
65| Slabel _ s1 ⇒ mem_vars_stmt mem_vars s1
66| Sgoto _ ⇒ True
67| Scost _ s1 ⇒ mem_vars_stmt mem_vars s1
68]
69and mem_vars_ls (mem_vars:identifier_set SymbolTag) (ls:labeled_statements) on ls : Prop ≝
70match ls with
71[ LSdefault s1 ⇒ mem_vars_stmt mem_vars s1
72| LScase _ s1 ls1 ⇒ mem_vars_stmt mem_vars s1 ∧
73                    mem_vars_ls mem_vars ls1
74].
75*)
76
77let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝
78match e with
79[ Expr ed ty ⇒
80    match ed with
81    [ Ederef e1 ⇒ gather_mem_vars_expr e1
82    | Eaddrof e1 ⇒ gather_mem_vars_addr e1
83    | Eunop _ e1 ⇒ gather_mem_vars_expr e1
84    | Ebinop _ e1 e2 ⇒ gather_mem_vars_expr e1 ∪
85                       gather_mem_vars_expr e2
86    | Ecast _ e1 ⇒ gather_mem_vars_expr e1
87    | Econdition e1 e2 e3 ⇒ gather_mem_vars_expr e1 ∪
88                            gather_mem_vars_expr e2 ∪
89                            gather_mem_vars_expr e3
90    | Eandbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
91                       gather_mem_vars_expr e2
92    | Eorbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
93                      gather_mem_vars_expr e2
94    | Efield e1 _ ⇒ gather_mem_vars_expr e1
95    | Ecost _ e1 ⇒ gather_mem_vars_expr e1
96    | _ ⇒ ∅
97    ]
98]
99and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝
100match e with
101[ Expr ed ty ⇒
102    match ed with
103    [ Evar x ⇒ { (x) }
104    | Ederef e1 ⇒ gather_mem_vars_expr e1
105    | Efield e1 _ ⇒ gather_mem_vars_addr e1
106    | _ ⇒ ∅ (* not an lvalue *)
107    ]
108].
109
110let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝
111match s with
112[ Sskip ⇒ ∅
113| Sassign e1 e2 ⇒ gather_mem_vars_expr e1 ∪
114                  gather_mem_vars_expr e2
115| Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] ∪
116                    gather_mem_vars_expr e2 ∪
117                    (foldl ?? (λs,e. s ∪ gather_mem_vars_expr e) ∅ es)
118| Ssequence s1 s2 ⇒ gather_mem_vars_stmt s1 ∪
119                    gather_mem_vars_stmt s2
120| Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪
121                         gather_mem_vars_stmt s1 ∪
122                         gather_mem_vars_stmt s2
123| Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
124                 gather_mem_vars_stmt s1
125| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
126                   gather_mem_vars_stmt s1
127| Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪
128                     gather_mem_vars_expr e1 ∪
129                     gather_mem_vars_stmt s2 ∪
130                     gather_mem_vars_stmt s3
131| Sbreak ⇒ ∅
132| Scontinue ⇒ ∅
133| Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ]
134| Sswitch e1 ls ⇒ gather_mem_vars_expr e1 ∪
135                  gather_mem_vars_ls ls
136| Slabel _ s1 ⇒ gather_mem_vars_stmt s1
137| Sgoto _ ⇒ ∅
138| Scost _ s1 ⇒ gather_mem_vars_stmt s1
139]
140and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝
141match ls with
142[ LSdefault s1 ⇒ gather_mem_vars_stmt s1
143| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
144                      gather_mem_vars_ls ls1
145].
146
147inductive var_type : Type[0] ≝
148| Global : region → var_type
149| Stack  : nat → var_type
150| Local  : var_type
151.
152
153definition var_types ≝ identifier_map SymbolTag var_type.
154
155axiom UndeclaredIdentifier : String.
156
157definition lookup' ≝
158λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
159
160definition local_id : var_types → ident → Prop ≝
161λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ].
162
163(* Note that the semantics allows locals to shadow globals.
164   Parameters start out as locals, but get stack allocated if their address
165   is taken.  We will add code to store them if that's the case.
166 *)
167
168definition always_alloc : type → bool ≝
169λt. match t with
170[ Tarray _ _ _ ⇒ true
171| Tstruct _ _ ⇒ true
172| Tunion _ _ ⇒ true
173| _ ⇒ false
174].
175
176definition characterise_vars : list (ident×region) → function → var_types × nat ≝
177λglobals, f.
178  let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
179  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
180  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
181    let 〈m,stack_high〉 ≝ ms in
182    let 〈id,ty〉 ≝ v in
183    let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id
184                           then 〈Stack stack_high,stack_high + sizeof ty〉
185                           else 〈Local, stack_high〉 in
186      〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
187  〈m,stacksize〉.
188
189lemma local_id_add_global : ∀vars,id,r,id'.
190  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
191#var #id #r #id'
192whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
193cases (identifier_eq ? id id')
194[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
195| #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
196] qed.
197
198lemma local_id_add_miss : ∀vars,id,t,id'.
199  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
200#vars #id #t #id' #NE
201whd in ⊢ (% → %)
202whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
203>lookup_add_miss
204[ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
205qed.
206
207lemma contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
208#A #B * // qed.
209
210lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
211((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
212∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
213#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
214
215include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *)
216
217lemma characterise_vars_all : ∀l,f,vars,n.
218  characterise_vars l f = 〈vars,n〉 →
219  ∀i. local_id vars i →
220      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
221#globals #f
222whd in ⊢ (∀_.∀_.??%? → ?)
223elim (fn_params f @ fn_vars f)
224[ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) -E; #i #H @False_ind
225  elim globals in H
226  [ normalize //
227  | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
228  ]
229| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
230  cases (identifier_eq ? id i)
231  [ #E' <E' #H % @refl
232  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
233    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
234    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
235    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
236    @(IH m0 n0)
237    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
238    | 2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE
239    ]
240  ]
241] qed.
242
243include "Cminor/syntax.ma".
244include "common/Errors.ma".
245
246alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
247
248axiom BadlyTypedAccess : String.
249axiom BadLvalue : String.
250axiom MissingField : String.
251
252alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
253alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
254
255(* XXX: For some reason matita refuses to pick the right one unless forced. *)
256alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,6,0)".
257
258definition translate_unop : type → CLunop → res CMunop ≝
259λty.λop:CLunop.
260  match op with
261  [ Onotbool ⇒ OK ? CMnotbool
262  | Onotint ⇒ OK ? Onotint
263  | Oneg ⇒
264      match ty with
265      [ Tint _ _ ⇒ OK ? Onegint
266      | Tfloat _ ⇒ OK ? Onegf
267      | _ ⇒ Error ? (msg TypeMismatch)
268      ]
269  ].
270
271definition translate_add ≝
272λty1,e1,ty2,e2,ty'.
273let ty1' ≝ typ_of_type ty1 in
274let ty2' ≝ typ_of_type ty2 in
275match classify_add ty1 ty2 with
276[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
277| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
278(* XXX using the integer size for e2 as the offset's size isn't right, because
279   if e2 produces an 8bit value then the true offset might overflow *)
280| add_case_pi ty ⇒
281    match ty2' with
282    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
283    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
284    ]
285| add_case_ip ty ⇒
286    match ty1' with
287    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
288    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
289    ]
290| add_default ⇒ Error ? (msg TypeMismatch)
291].
292
293definition translate_sub ≝
294λty1,e1,ty2,e2,ty'.
295let ty1' ≝ typ_of_type ty1 in
296let ty2' ≝ typ_of_type ty2 in
297match classify_sub ty1 ty2 with
298[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
299| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
300(* XXX choosing offset sizes? *)
301| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
302| sub_case_pp ty ⇒
303    match ty' with (* XXX overflow *)
304    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
305    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
306    ]
307| sub_default ⇒ Error ? (msg TypeMismatch)
308].
309
310definition translate_mul ≝
311λty1,e1,ty2,e2,ty'.
312let ty1' ≝ typ_of_type ty1 in
313let ty2' ≝ typ_of_type ty2 in
314match classify_mul ty1 ty2 with
315[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
316| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
317| mul_default ⇒ Error ? (msg TypeMismatch)
318].
319
320definition translate_div ≝
321λty1,e1,ty2,e2,ty'.
322let ty1' ≝ typ_of_type ty1 in
323let ty2' ≝ typ_of_type ty2 in
324match classify_div ty1 ty2 with
325[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
326| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
327| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
328| div_default ⇒ Error ? (msg TypeMismatch)
329].
330
331definition translate_mod ≝
332λty1,e1,ty2,e2,ty'.
333let ty1' ≝ typ_of_type ty1 in
334let ty2' ≝ typ_of_type ty2 in
335match classify_mod ty1 ty2 with
336[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
337| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
338| mod_default ⇒ Error ? (msg TypeMismatch)
339].
340
341definition translate_shr ≝
342λty1,e1,ty2,e2,ty'.
343let ty1' ≝ typ_of_type ty1 in
344let ty2' ≝ typ_of_type ty2 in
345match classify_shr ty1 ty2 with
346[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
347| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
348| shr_default ⇒ Error ? (msg TypeMismatch)
349].
350
351definition translate_cmp ≝
352λc,ty1,e1,ty2,e2,ty'.
353let ty1' ≝ typ_of_type ty1 in
354let ty2' ≝ typ_of_type ty2 in
355match classify_cmp ty1 ty2 with
356[ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
357| cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
358| cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
359| cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
360| cmp_default ⇒ Error ? (msg TypeMismatch)
361].
362
363definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
364λop,ty1,e1,ty2,e2,ty.
365let ty' ≝ typ_of_type ty in
366match op with
367[ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
368| Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
369| Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
370| Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
371| Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
372| Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
373| Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
374| Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
375| Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
376| Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
377| Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
378| One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
379| Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
380| Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
381| Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
382| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
383].
384
385lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
386  expr_vars ? e1 P →
387  expr_vars ? e2 P →
388  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
389  expr_vars ? e P.
390#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
391whd in ⊢ (??%? → ?)
392[ cases (classify_add ty1 ty2)
393  [ 3,4: #z ] whd in ⊢ (??%? → ?)
394  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
395    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
396    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
397  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
398    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
399    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
400  | *: #E destruct (E) % try @H1 @H2
401  ]
402| cases (classify_sub ty1 ty2)
403  [ 3,4: #z] whd in ⊢ (??%? → ?)
404  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
405    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
406    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
407  | *: #E destruct (E) % try @H1 try @H2 % // @H2
408  ]
409| cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
410    % try @H1 @H2
411| cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
412    % try @H1 @H2
413| cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
414    % try @H1 @H2
415| 6,7,8,9: #E destruct % try @H1 @H2
416| cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
417| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
418] qed.
419
420(* We'll need to implement proper translation of pointers if we really do memory
421   spaces. *)
422definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
423λr1,r2,P.
424  match r1 return λx.P x → res (P r2) with
425  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
426  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
427  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
428  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
429  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
430  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
431  ].
432
433definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
434λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
435
436notation "hvbox(« term 19 a, break term 19 b»)"
437with precedence 90 for @{ (dp ?? $a $b) }.
438
439lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x.
440  P x.
441#A #P * #a #p @p
442qed.
443
444definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
445λP,ty1,ty2.
446match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
447[ Tint sz1 sg1 ⇒ λe.
448    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
449    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e)
450    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
451    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
452    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
453    | _ ⇒ Error ? (msg TypeMismatch)
454    ]
455| Tfloat sz1 ⇒ λe.
456    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
457    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e, ?»
458    | Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *)
459    | _ ⇒ Error ? (msg TypeMismatch)
460    ]
461| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
462    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
463    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?»
464    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
465    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
466    | _ ⇒ Error ? (msg TypeMismatch)
467    ]
468| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
469    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
470    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?»
471    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
472    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
473    | _ ⇒ Error ? (msg TypeMismatch)
474    ]
475| _ ⇒ λ_. Error ? (msg TypeMismatch)
476]. whd @sig_ok qed.
477
478definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
479λty1,ty2,P,p.
480  do E ← assert_type_eq ty1 ty2;
481  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
482
483definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
484* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
485qed.
486
487definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
488* [ #sz1 #sg1 | #r1 | #sz1 ]
489* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
490[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
491  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
492| *; #P #p @(region_should_eq r1 ?? p)
493| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
494] qed.
495
496
497lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
498*
499[ 5: #r #ty #n #r' normalize #E destruct @refl
500| 6: #args #ret #r normalize #E destruct @refl
501| *: normalize #a #b try #c try #d destruct
502  [ cases a in d; normalize; cases b; normalize #E destruct
503  | cases a in c; normalize #E destruct
504  ]
505] qed.
506
507definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
508  match f return λx. f = x → ? with
509  [ OK x ⇒ g x
510  | Error msg ⇒ λ_. Error ? msg
511  ] (refl ? f).
512
513notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
514
515let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
516match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
517[ Expr ed ty ⇒
518  match ed with
519  [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
520  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
521  | Evar id ⇒
522      do c as E ← lookup' vars id;
523      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
524      [ Global r ⇒ λ_.
525          match access_mode ty with
526          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?»
527          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
528          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
529          ]
530      | Stack n ⇒ λE.
531          match access_mode ty with
532          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
533          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
534          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
535          ]
536      | Local ⇒ λE. OK ? «Id ? id, ?»
537      ] E
538  | Ederef e1 ⇒
539      do e1' ← translate_expr vars e1;
540      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
541      [ ASTptr r ⇒ λe1'.
542          match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
543          [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?»
544          | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
545                                  OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
546          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
547          ] (access_mode_typ ty)
548      | _ ⇒ λ_. Error ? (msg TypeMismatch)
549      ] e1'
550  | Eaddrof e1 ⇒
551      do e1' ← translate_addr vars e1;
552      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
553      [ ASTptr r ⇒
554          match e1' with
555          [ dp r1 e1' ⇒ region_should_eq r1 r ? e1'
556          ]
557      | _ ⇒ Error ? (msg TypeMismatch)
558      ]
559  | Eunop op e1 ⇒
560      do op' ← translate_unop ty op;
561      do e1' ← translate_expr vars e1;
562      OK ? «Op1 ?? op' e1', ?»
563  | Ebinop op e1 e2 ⇒
564      do e1' ← translate_expr vars e1;
565      do e2' ← translate_expr vars e2;
566      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
567      OK ? «e', ?»
568  | Ecast ty1 e1 ⇒
569      do e1' ← translate_expr vars e1;
570      do e' ← translate_cast ? (typeof e1) ty1 e1';
571      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
572      OK ? e'
573  | Econdition e1 e2 e3 ⇒
574      do e1' ← translate_expr vars e1;
575      do e2' ← translate_expr vars e2;
576      do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
577      do e3' ← translate_expr vars e3;
578      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
579      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with
580      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
581      | _ ⇒ λ_.Error ? (msg TypeMismatch)
582      ] e1'
583  | Eandbool e1 e2 ⇒
584      do e1' ← translate_expr vars e1;
585      do e2' ← translate_expr vars e2;
586      match ty with
587      [ Tint sz _ ⇒
588        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
589        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
590        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?»
591        | _ ⇒ λ_.Error ? (msg TypeMismatch)
592        ] e1'
593      | _ ⇒ Error ? (msg TypeMismatch)
594      ]
595  | Eorbool e1 e2 ⇒
596      do e1' ← translate_expr vars e1;
597      do e2' ← translate_expr vars e2;
598      match ty with
599      [ Tint sz _ ⇒
600        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
601        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
602        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
603        | _ ⇒ λ_.Error ? (msg TypeMismatch)
604        ] e1'
605      | _ ⇒ Error ? (msg TypeMismatch)
606      ]
607  | Esizeof ty1 ⇒
608      match ty with
609      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
610      | _ ⇒ Error ? (msg TypeMismatch)
611      ]
612  | Efield e1 id ⇒
613      match typeof e1 with
614      [ Tstruct _ fl ⇒
615          do e1' ← translate_addr vars e1;
616          match e1' with
617          [ dp r e1' ⇒
618            do off ← field_offset id fl;
619            match access_mode ty with
620            [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
621            | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
622            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
623            ]
624          ]
625      | Tunion _ _ ⇒
626          do e1' ← translate_addr vars e1;
627          match e1' with
628          [ dp r e1' ⇒
629            match access_mode ty return λx. access_mode ty = x → res ? with
630            [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
631            | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
632                                OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
633            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
634            ] (refl ? (access_mode ty))
635          ]
636      | _ ⇒ Error ? (msg BadlyTypedAccess)
637      ]
638  | Ecost l e1 ⇒
639      do e1' ← translate_expr vars e1;
640      do e' ← OK ? «Ecost ? l e1',?»;
641      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
642  ]
643] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
644match e with
645[ Expr ed _ ⇒
646  match ed with
647  [ Evar id ⇒
648      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
649      match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with
650      [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»»
651      | Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»»
652      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
653      ]
654  | Ederef e1 ⇒
655      do e1' ← translate_expr vars e1;
656      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with
657      [ ASTptr r ⇒ λe1'.OK ? «r, e1'»
658      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
659      ] e1'
660  | Efield e1 id ⇒
661      match typeof e1 with
662      [ Tstruct _ fl ⇒
663          do e1' ← translate_addr vars e1;
664          do off ← field_offset id fl;
665          match e1' with
666          [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» »)
667          ]
668      | Tunion _ _ ⇒ translate_addr vars e1
669      | _ ⇒ Error ? (msg BadlyTypedAccess)
670      ]
671  | _ ⇒ Error ? (msg BadLvalue)
672  ]
673].
674whd try @I
675[ >E @I
676| >(E ? (refl ??)) @refl
677| 3,4: @sig_ok
678| @(translate_binop_vars … E) @sig_ok
679| % [ % ] @sig_ok
680| % [ % @sig_ok ] whd @I
681| % [ % [ @sig_ok | @I ] | @sig_ok ]
682| % [ @sig_ok | @I ]
683| % [ @sig_ok | @I ]
684| >(access_mode_typ … E) @refl
685| @sig_ok
686| @sig_ok
687| % [ @sig_ok | @I ]
688] qed.
689
690inductive destination (vars:var_types) : Type[0] ≝
691| IdDest : ∀id:ident. local_id vars id → destination vars
692| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
693
694definition translate_dest ≝
695λvars,e1,ty2.
696    do q ← match access_mode ty2 with
697           [ By_value q ⇒ OK ? q
698           | By_reference r ⇒ OK ? (Mpointer r)
699           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
700           ];
701    match e1 with
702    [ Expr ed1 ty1 ⇒
703        match ed1 with
704        [ Evar id ⇒
705            do c as E ← lookup' vars id;
706            match c return λx.? → ? with
707            [ Local ⇒ λE. OK ? (IdDest vars id ?)
708            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
709            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
710            ] E
711        | _ ⇒
712            do e1' ← translate_addr vars e1;
713            match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ]
714        ]
715    ].
716whd // >E @I
717qed.
718(*
719definition translate_assign ≝
720λvars,e1,e2.
721    do e2' ← translate_expr vars e2;
722    do q ← match access_mode (typeof e2) with
723           [ By_value q ⇒ OK ? q
724           | By_reference r ⇒ OK ? (Mpointer r)
725           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
726           ];
727    match e1 with
728    [ Expr ed1 ty1 ⇒
729        match ed1 with
730        [ Evar id ⇒
731            do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
732            match c with
733            [ Local ⇒ OK ? (St_assign id e2')
734            | Global ⇒ OK ? (St_store q (Cst (Oaddrsymbol id zero)) e2')
735            | Stack n ⇒ OK ? (St_store q (Cst (Oaddrstack (repr n))) e2')
736            ]
737        | _ ⇒
738            do e1' ← translate_addr vars e1;
739            OK ? (St_store q e1' e2')
740        ]
741    ].
742*)
743
744definition lenv ≝ identifier_map SymbolTag (identifier Label).
745
746axiom MissingLabel : String.
747
748definition lookup_label ≝
749λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
750
751definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.
752
753let rec labels_defined (s:statement) : list ident ≝
754match s with
755[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
756| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
757| Swhile _ s ⇒ labels_defined s
758| Sdowhile _ s ⇒ labels_defined s
759| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
760| Sswitch _ ls ⇒ labels_defined_switch ls
761| Slabel l s ⇒ l::(labels_defined s)
762| Scost _ s ⇒ labels_defined s
763| _ ⇒ [ ]
764]
765and labels_defined_switch (ls:labeled_statements) : list ident ≝
766match ls with
767[ LSdefault s ⇒ labels_defined s
768| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
769].
770
771definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
772
773definition labels_translated : lenv → statement → stmt → Prop ≝
774λlbls,s,s'.  ∀l.
775  (Exists ? (λl'.l' = l) (labels_defined s)) →
776  ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'.
777
778definition stmt_inv ≝
779λvars. λlbls:lenv.
780  stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s).
781
782definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝
783λvars,e1,e2.
784do e2' ← translate_expr vars e2;
785do dest ← translate_dest vars e1 (typeof e2);
786match dest with
787[ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
788| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
789].
790#ls whd %
791[ % // @sig_ok
792| @I
793| % @sig_ok
794| @I
795] qed.
796
797definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
798λA,B,f,oa.
799match oa with
800[ None ⇒ OK ? (None ?)
801| Some a ⇒ do b ← f a; OK ? (Some ? b)
802].
803
804definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(Σt:typ.CMexpr t). match e with [ dp t e ⇒ expr_vars t e (local_id vars) ]) ≝
805λv,e.
806  do e' ← translate_expr v e;
807  OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?».
808whd @sig_ok
809qed.
810
811axiom FIXME : String.
812
813let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝
814match l with
815[ nil ⇒ OK ? «nil B, ?»
816| cons h t ⇒
817    do h' ← f h;
818    do t' ← mmap_sigma A B P f t;
819    OK ? «cons B h' t', ?»
820].
821whd // %
822[ @(sig_ok B P)
823| cases t' #l' #p @p
824] qed.
825
826lemma lookup_label_hit : ∀lbls,l,l'.
827  lookup_label lbls l = OK ? l' →
828  lpresent lbls l'.
829#lbls #l #l' #E whd %{l} @E
830qed.
831
832definition trans_inv : var_types → lenv → statement → stmt → Prop ≝
833λvars,lbls,s,s'. stmt_inv vars lbls s' ∧ labels_translated lbls s s'.
834
835lemma trans_inv_stmt_inv : ∀vars,lbls,s,s'.
836  trans_inv vars lbls s s' → stmt_inv vars lbls s'.
837#var #lbls #s #s' * //
838qed.
839
840lemma trans_inv_labels : ∀vars,lbls,s,s'.
841  trans_inv vars lbls s s' → labels_translated lbls s s'.
842#vars #lbls #s #s' @proj2
843qed.
844
845lemma Exists_append : ∀A,P,l1,l2.
846  Exists A P (l1@l2) →
847  Exists A P l1 ∨ Exists A P l2.
848#A #P #l1 elim l1
849[ #l2 #H %2 @H
850| #h #t #IH #l2 whd in ⊢ (% → ?) *
851  [ #H %1 %1 @H
852  | #H cases (IH l2 H) /4/
853  ]
854] qed.
855
856lemma Exists_append_l : ∀A,P,l1,l2.
857  Exists A P l1 → Exists A P (l1@l2).
858#A #P #l1 #l2 elim l1
859[ *
860| #h #t #IH *
861  [ #H %1 @H
862  | #H %2 @IH @H
863  ]
864] qed.
865
866lemma Exists_append_r : ∀A,P,l1,l2.
867  Exists A P l2 → Exists A P (l1@l2).
868#A #P #l1 #l2 elim l1
869[ #H @H
870| #h #t #IH #H %2 @IH @H
871] qed.
872
873
874let rec translate_statement (vars:var_types) (lbls:lenv) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs':stmt.trans_inv vars lbls s s') ≝
875match s return λs.res (Σs':stmt.trans_inv vars lbls s s') with
876[ Sskip ⇒ OK ? «St_skip, ?»
877| Sassign e1 e2 ⇒
878    do s' ← translate_assign vars e1 e2;
879    OK ? «eject ?? s', ?»
880| Scall ret ef args ⇒
881    do ef' ← translate_expr vars ef;
882    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
883    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
884    match ret with
885    [ None ⇒ OK ? «St_call (None ?) ef' args', ?»
886    | Some e1 ⇒
887        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
888        match dest with
889        [ IdDest id p ⇒ OK ? «St_call (Some ? id) ef' args', ?»
890        | MemDest r q e1' ⇒
891            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
892            OK ? «St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), ?»
893        ]
894    ]
895| Ssequence s1 s2 ⇒
896    do s1' ← translate_statement vars lbls tmp tmpp s1;
897    do s2' ← translate_statement vars lbls tmp tmpp s2;
898    OK ? «St_seq s1' s2', ?»
899| Sifthenelse e1 s1 s2 ⇒
900    do e1' ← translate_expr vars e1;
901    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
902    [ ASTint _ _ ⇒ λe1'.
903        do s1' ← translate_statement vars lbls tmp tmpp s1;
904        do s2' ← translate_statement vars lbls tmp tmpp s2;
905        OK ? «St_ifthenelse ?? e1' s1' s2', ?»
906    | _ ⇒ λ_.Error ? (msg TypeMismatch)
907    ] e1'
908| Swhile e1 s1 ⇒
909    do e1' ← translate_expr vars e1;
910    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
911    [ ASTint _ _ ⇒ λe1'.
912        do s1' ← translate_statement vars lbls tmp tmpp s1;
913        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
914        OK ? «St_block
915               (St_loop
916                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), ?»
917    | _ ⇒ λ_.Error ? (msg TypeMismatch)
918    ] e1'
919| Sdowhile e1 s1 ⇒
920    do e1' ← translate_expr vars e1;
921    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
922    [ ASTint _ _ ⇒ λe1'.
923        do s1' ← translate_statement vars lbls tmp tmpp s1;
924        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
925        OK ? «St_block
926               (St_loop
927                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), ?»
928    | _ ⇒ λ_.Error ? (msg TypeMismatch)
929    ] e1'
930| Sfor s1 e1 s2 s3 ⇒
931    do e1' ← translate_expr vars e1;
932    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
933    [ ASTint _ _ ⇒ λe1'.
934        do s1' ← translate_statement vars lbls tmp tmpp s1;
935        do s2' ← translate_statement vars lbls tmp tmpp s2;
936        do s3' ← translate_statement vars lbls tmp tmpp s3;
937        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
938        OK ? «St_seq s1'
939             (St_block
940               (St_loop
941                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), ?»
942    | _ ⇒ λ_.Error ? (msg TypeMismatch)
943    ] e1'
944| Sbreak ⇒ OK ? «St_exit 1, ?»
945| Scontinue ⇒ OK ? «St_exit 0, ?»
946| Sreturn ret ⇒
947    match ret with
948    [ None ⇒ OK ? «St_return (None ?), ?»
949    | Some e1 ⇒
950        do e1' ← translate_expr vars e1;
951        OK ? «St_return (Some ? (dp … e1')), ?»
952    ]
953| Sswitch e1 ls ⇒ Error ? (msg FIXME)
954| Slabel l s1 ⇒
955    do l' as E ← lookup_label lbls l;
956    do s1' ← translate_statement vars lbls tmp tmpp s1;
957    OK ? «St_label l' s1', ?»
958| Sgoto l ⇒
959    do l' as E ← lookup_label lbls l;
960    OK ? «St_goto l', ?»
961| Scost l s1 ⇒
962    do s1' ← translate_statement vars lbls tmp tmpp s1;
963    OK ? «St_cost l s1', ?»
964].
965try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
966try @I
967try @(trans_inv_stmt_inv ???? (sig_ok ? (λs.trans_inv ??? s) …))
968try @(sig_ok ? (λs.stmt_inv ?? s))
969try @(sig_ok ? (λe.expr_vars ? e ?))
970try @(sig_ok ? (λs.stmt_vars ?? s))
971try @(sig_ok ? (λs.stmt_labels ?? s))
972try @(sig_ok ? (All ??))
973try @(sig_ok ? (local_id vars))
974try @(lookup_label_hit … E)
975[ 1,3,5,6,7,13,14,15,16,18: whd #l *
976| @(sig_ok ?? s')
977| @p
978| #l #H cases (Exists_append … H)
979  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
980    %{l'} % [ @E1 | @Exists_append_l @D1 ]
981  | #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
982    %{l'} % [ @E2 | @Exists_append_r @D2 ]
983  ]
984| #l #H cases (Exists_append … H)
985  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
986    %{l'} % [ @E1 | @Exists_append_l @D1 ]
987  | #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
988    %{l'} % [ @E2 | @Exists_append_r @D2 ]
989  ]
990| cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1
991  %{l'} % [ @E1 | @Exists_append_l @D1 ]
992| cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1
993  %{l'} % [ @E1 | @Exists_append_l @D1 ]
994| #l #H cases (Exists_append … H)
995  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
996    %{l'} % [ @E1 | @Exists_append_l @D1 ]
997  | #H cases (Exists_append … H)
998    [ #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
999      %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ]
1000    | #H3 cases s3' #s3' * #S3 #L3 cases (L3 l H3) #l' * #E3 #D3
1001      %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ]
1002    ]
1003  ]
1004| cases s1' #s1' * #S1 #L1 #l0 *
1005  [ #El <El %{l'} >E % [ @refl | %1 @refl ]
1006  | #H cases (L1 l0 H) #l0' * #E1 #D1
1007    %{l0'} % [ @E1 | %2 @D1 ]
1008  ]
1009| cases s1' #s1' * #S1 #L1 @L1
1010] qed.
1011
1012
1013axiom ParamGlobalMixup : String.
1014
1015(* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
1016definition alloc_params : ∀vars:var_types.∀ls,s0. list (ident×type) → (Σs:stmt. trans_inv vars ls s0 s) → res (Σs:stmt.trans_inv vars ls s0 s) ≝
1017λvars,ls,s0,params,s. foldl ?? (λs,it.
1018  let 〈id,ty〉 ≝ it in
1019  do s ← s;
1020  do t as E ← lookup' vars id;
1021  match t return λx.? → ? with
1022  [ Local ⇒ λE. OK (Σs:stmt.?) s
1023  | Stack n ⇒ λE.
1024      do q ← match access_mode ty with
1025      [ By_value q ⇒ OK ? q
1026      | By_reference r ⇒ OK ? (Mpointer r)
1027      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
1028      ];
1029      OK ? «St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, ?»
1030  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
1031  ] E) (OK ? s) params.
1032try @conj try @conj try @conj try @conj try @conj
1033try @I
1034[ whd >E @I
1035| @(trans_inv_stmt_inv … s0) @(sig_ok … s)
1036| cases s #s * #S #L @L
1037] qed.
1038
1039definition bigid1 ≝ an_identifier SymbolTag [[
1040false;true;false;false;
1041false;false;false;false;
1042false;false;false;false;
1043false;false;false;false]].
1044definition bigid2 ≝ an_identifier SymbolTag [[
1045false;true;false;false;
1046false;false;false;false;
1047false;false;false;false;
1048false;false;false;true]].
1049
1050lemma Exists_rm : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
1051#A #P #l1 #x #l2 elim l1
1052[ normalize #H %2 @H
1053| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
1054qed.
1055
1056lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
1057#A #P #l1 #x #l2 #H elim l1
1058[ %1 @H
1059| #h #t #IH %2 @IH
1060] qed.
1061
1062lemma Exists_map : ∀A,B,P,Q,f,l.
1063Exists A P l →
1064(∀a.P a → Q (f a)) →
1065Exists B Q (map A B f l).
1066#A #B #P #Q #f #l elim l //
1067#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
1068
1069notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
1070 with precedence 10
1071for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
1072        λ${ident E}.$s ] (refl ? $t) }.
1073
1074lemma local_id_add_local : ∀vars,id,id'.
1075  local_id vars id →
1076  local_id (add ?? vars id' Local) id.
1077#vars #id #id' #H
1078whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
1079[ #E < E >lookup_add_hit //
1080| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
1081] qed.
1082
1083axiom DuplicateLabel : String.
1084
1085definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
1086λlbls0,lbls,ls.
1087 ∀l,l'. lookup_label lbls l = OK ? l' →
1088 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.
1089
1090lemma lookup_label_add : ∀lbls,l,l'.
1091  lookup_label (add … lbls l l') l = OK ? l'.
1092#lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl
1093qed.
1094
1095lemma lookup_label_miss : ∀lbls,l,l',l0.
1096  l0 ≠ l →
1097  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
1098#lbls #l #l' #l0 * #NE
1099whd in ⊢ (??%%)
1100>lookup_add_miss
1101[ @refl | @(eq_identifier_elim ?? l0 l)
1102  [ #E cases (NE E)
1103  | #_ @I
1104  ]
1105]
1106qed. 
1107
1108let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝
1109match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with
1110[ nil ⇒ OK ? «lbls, ?»
1111| cons l t ⇒
1112    match lookup_label lbls l return λx.lookup_label lbls l = x → ? with
1113    [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel)
1114    | Error _ ⇒ λLOOK.
1115        let 〈l',u1〉 ≝ fresh … u in
1116        do lbls1 ← populate_lenv t (add … lbls l l') u1;
1117        OK ? «eject … lbls1, ?»
1118    ] (refl ? (lookup_label lbls l))
1119].
1120[ #l #l' #H %2 @H
1121| cases lbls1 #lbls' #I whd in ⊢ (??%?)
1122  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
1123  [ #E %1 %1 @E
1124  | #NE cases (I l1 l1' E1)
1125    [ #H %1 %2 @H
1126    | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H
1127    ]
1128  ]
1129] qed.
1130
1131notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
1132  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
1133
1134definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝
1135λbody.
1136  do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
1137  OK ? «lbls, ?».
1138#l #l' #E cases (H l l' E) //
1139whd in ⊢ (??%? → ?) #H destruct
1140qed.
1141
1142(* FIXME: the temporary handling is nonsense, I'm afraid. *)
1143definition translate_function : list (ident×region) → function → res internal_function ≝
1144λglobals, f.
1145  do «lbls, Ilbls» ← build_label_env (fn_body f);
1146  let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in
1147  let tmp ≝ bigid1 in (* FIXME *)
1148  let tmpp ≝ bigid2 in (* FIXME *)
1149  let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in
1150  do s ← translate_statement vartypes lbls tmp tmpp (fn_body f);
1151  do «s,Is» ← alloc_params vartypes lbls ? (fn_params f) s;
1152  OK ? (mk_internal_function
1153    (opttyp_of_type (fn_return f))
1154    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
1155    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
1156    stacksize
1157    s ?).
1158[ cases Is #S #L
1159  @(stmt_P_mp ???? S)
1160  #s1 * #H1 #H2 %
1161  [ @(stmt_vars_mp … H1)
1162    #i #H cases (identifier_eq ? tmp i)
1163    [ #E <E @Exists_mid @refl
1164    | #NE1 @Exists_rm cases (identifier_eq ? tmpp i)
1165      [ #E <E @Exists_mid @refl
1166      | #NE2 @Exists_rm
1167        >map_append
1168        @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
1169                         @(local_id_add_miss ?? Local ? NE1)
1170                         @(local_id_add_miss ?? Local ? NE2) @H
1171                    | skip
1172                    | * #id #ty #E1 <E1 @refl
1173                    ]
1174      ]
1175    ]
1176  | @(stmt_labels_mp … H2)
1177    #l * #l' #LOOKUP
1178    lapply (Ilbls l' l LOOKUP) #DEFINED
1179    cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
1180    #H @H
1181  ]
1182| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
1183| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
1184] qed.
1185
1186definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
1187λglobals,f.
1188match f with
1189[ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
1190| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
1191].
1192
1193definition clight_to_cminor : clight_program → res Cminor_program ≝
1194λp.
1195  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
1196  let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
1197  let globals ≝ fun_globals @ var_globals in
1198  transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
Note: See TracBrowser for help on using the repository browser.