source: src/Clight/toCminor.ma @ 1629

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

Sort out most of the fresh names stuff in Clight to Cminor.

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