source: src/Clight/toCminor.ma @ 1351

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

Tidy up some loose ends from the invariants branch merge.

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