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

Last change on this file since 1102 was 1102, checked in by campbell, 8 years ago

Tidy up branch

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