source: src/Clight/toCminor.ma @ 1451

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

Put type information into front-end unary ops.
Slight change to semantics: booleans produced by Onotbool can be any given
integer size.

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