source: src/Clight/toCminor.ma @ 1627

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

Add some notions of freshness, and start using them for temporary
generation (not yet complete).

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