source: src/Clight/toCminor.ma @ 1605

Last change on this file since 1605 was 1605, checked in by sacerdot, 8 years ago

Porting to last standard library of Matita.

File size: 42.9 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.
85
86axiom UndeclaredIdentifier : String.
87
88definition lookup' ≝
89λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
90
91definition local_id : var_types → ident → Prop ≝
92λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ].
93
94(* Note that the semantics allows locals to shadow globals.
95   Parameters start out as locals, but get stack allocated if their address
96   is taken.  We will add code to store them if that's the case.
97 *)
98
99definition always_alloc : type → bool ≝
100λt. match t with
101[ Tarray _ _ _ ⇒ true
102| Tstruct _ _ ⇒ true
103| Tunion _ _ ⇒ true
104| _ ⇒ false
105].
106
107definition characterise_vars : list (ident×region) → function → var_types × nat ≝
108λglobals, f.
109  let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
110  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
111  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
112    let 〈m,stack_high〉 ≝ ms in
113    let 〈id,ty〉 ≝ v in
114    let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id
115                           then 〈Stack stack_high,stack_high + sizeof ty〉
116                           else 〈Local, stack_high〉 in
117      〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
118  〈m,stacksize〉.
119
120lemma local_id_add_global : ∀vars,id,r,id'.
121  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
122#var #id #r #id'
123whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
124cases (identifier_eq ? id id')
125[ #E >E >lookup_add_hit whd in ⊢ (% → ?); *
126| #NE >lookup_add_miss /2/
127] qed.
128
129lemma local_id_add_miss : ∀vars,id,t,id'.
130  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
131#vars #id #t #id' #NE
132whd in ⊢ (% → %);
133whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
134>lookup_add_miss
135[ #H @H | /2/ ]
136qed.
137
138lemma characterise_vars_all : ∀l,f,vars,n.
139  characterise_vars l f = 〈vars,n〉 →
140  ∀i. local_id vars i →
141      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
142#globals #f
143whd in ⊢ (∀_.∀_.??%? → ?);
144elim (fn_params f @ fn_vars f)
145[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind
146  elim globals in H;
147  [ normalize //
148  | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H)
149  ]
150| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
151  cases (identifier_eq ? id i)
152  [ #E' <E' #H % @refl
153  | #NE #H whd %2 >(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    @(IH m0 n0)
158    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
159    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
160    ]
161  ]
162] qed.
163
164include "Cminor/syntax.ma".
165include "common/Errors.ma".
166
167alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
168
169axiom BadlyTypedAccess : String.
170axiom BadLvalue : String.
171axiom MissingField : String.
172
173
174definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
175λty1,ty2,P,p.
176  do E ← assert_type_eq ty1 ty2;
177  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
178
179definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
180* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
181qed.
182
183definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
184* [ #sz1 #sg1 | #r1 | #sz1 ]
185* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
186[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
187  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
188| *; #P #p @(region_should_eq r1 ?? p)
189| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
190] qed.
191
192
193alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
194alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
195
196(* XXX: For some reason matita refuses to pick the right one unless forced. *)
197alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)".
198
199definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t') ≝
200λt,t'.λop:CLunop.
201  match op with
202  [ Onotbool ⇒
203      match t return λt. res (CMunop t t') with
204      [ ASTint sz sg ⇒
205          match t' return λt'. res (CMunop ? t') with
206          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
207          | _ ⇒ Error ? (msg TypeMismatch)
208          ]
209      | ASTptr r ⇒
210          match t' return λt'. res (CMunop ? t') with
211          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
212          | _ ⇒ Error ? (msg TypeMismatch)
213          ]
214      | _ ⇒ Error ? (msg TypeMismatch)
215      ]
216  | Onotint ⇒
217      match t' return λt'. res (CMunop t t') with
218      [ ASTint sz sg ⇒ typ_should_eq ?? (λt. CMunop t (ASTint ??)) (Onotint sz sg)
219      | _ ⇒ Error ? (msg TypeMismatch)
220      ]
221  | Oneg ⇒
222      match t' return λt'. res (CMunop t t') with
223      [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg)
224      | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz)
225      | _ ⇒ Error ? (msg TypeMismatch)
226      ]
227  ]. @I qed.
228
229definition translate_add ≝
230λty1,e1,ty2,e2,ty'.
231let ty1' ≝ typ_of_type ty1 in
232let ty2' ≝ typ_of_type ty2 in
233match classify_add ty1 ty2 with
234[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
235| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
236(* XXX using the integer size for e2 as the offset's size isn't right, because
237   if e2 produces an 8bit value then the true offset might overflow *)
238| add_case_pi ty ⇒
239    match ty2' with
240    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
241    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
242    ]
243| add_case_ip ty ⇒
244    match ty1' with
245    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
246    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
247    ]
248| add_default ⇒ Error ? (msg TypeMismatch)
249].
250
251definition translate_sub ≝
252λty1,e1,ty2,e2,ty'.
253let ty1' ≝ typ_of_type ty1 in
254let ty2' ≝ typ_of_type ty2 in
255match classify_sub ty1 ty2 with
256[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
257| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
258(* XXX choosing offset sizes? *)
259| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
260| sub_case_pp ty ⇒
261    match ty' with (* XXX overflow *)
262    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
263    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
264    ]
265| sub_default ⇒ Error ? (msg TypeMismatch)
266].
267
268definition translate_mul ≝
269λty1,e1,ty2,e2,ty'.
270let ty1' ≝ typ_of_type ty1 in
271let ty2' ≝ typ_of_type ty2 in
272match classify_mul ty1 ty2 with
273[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
274| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
275| mul_default ⇒ Error ? (msg TypeMismatch)
276].
277
278definition translate_div ≝
279λty1,e1,ty2,e2,ty'.
280let ty1' ≝ typ_of_type ty1 in
281let ty2' ≝ typ_of_type ty2 in
282match classify_div ty1 ty2 with
283[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
284| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
285| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
286| div_default ⇒ Error ? (msg TypeMismatch)
287].
288
289definition translate_mod ≝
290λty1,e1,ty2,e2,ty'.
291let ty1' ≝ typ_of_type ty1 in
292let ty2' ≝ typ_of_type ty2 in
293match classify_mod ty1 ty2 with
294[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
295| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
296| mod_default ⇒ Error ? (msg TypeMismatch)
297].
298
299definition translate_shr ≝
300λty1,e1,ty2,e2,ty'.
301let ty1' ≝ typ_of_type ty1 in
302let ty2' ≝ typ_of_type ty2 in
303match classify_shr ty1 ty2 with
304[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
305| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
306| shr_default ⇒ Error ? (msg TypeMismatch)
307].
308
309definition translate_cmp ≝
310λc,ty1,e1,ty2,e2,ty'.
311let ty1' ≝ typ_of_type ty1 in
312let ty2' ≝ typ_of_type ty2 in
313match classify_cmp ty1 ty2 with
314[ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
315| cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
316| cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
317| cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
318| cmp_default ⇒ Error ? (msg TypeMismatch)
319].
320
321definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
322λop,ty1,e1,ty2,e2,ty.
323let ty' ≝ typ_of_type ty in
324match op with
325[ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
326| Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
327| Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
328| Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
329| Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
330| Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
331| Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
332| Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
333| Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
334| Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
335| Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
336| One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
337| Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
338| Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
339| Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
340| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
341].
342
343lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
344  expr_vars ? e1 P →
345  expr_vars ? e2 P →
346  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
347  expr_vars ? e P.
348#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
349whd in ⊢ (??%? → ?);
350[ cases (classify_add ty1 ty2)
351  [ 3,4: #z ] whd in ⊢ (??%? → ?);
352  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
353    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
354    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
355  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
356    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
357    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
358  | *: #E destruct (E) % try @H1 @H2
359  ]
360| cases (classify_sub ty1 ty2)
361  [ 3,4: #z] whd in ⊢ (??%? → ?);
362  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
363    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
364    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
365  | *: #E destruct (E) % try @H1 try @H2 % // @H2
366  ]
367| cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
368    % try @H1 @H2
369| cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
370    % try @H1 @H2
371| cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
372    % try @H1 @H2
373| 6,7,8,9: #E destruct % try @H1 @H2
374| cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
375| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
376] qed.
377
378(* We'll need to implement proper translation of pointers if we really do memory
379   spaces. *)
380definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
381λr1,r2,P.
382  match r1 return λx.P x → res (P r2) with
383  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
384  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
385  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
386  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
387  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
388  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
389  ].
390
391definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
392λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
393
394axiom FIXME : String.
395
396definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
397λP,ty1,ty2.
398match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
399[ Tint sz1 sg1 ⇒ λe.
400    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
401    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
402    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)
403    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
404    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
405    | _ ⇒ Error ? (msg TypeMismatch)
406    ]
407| Tfloat sz1 ⇒ λe.
408    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
409    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?»
410    | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *)
411    | _ ⇒ Error ? (msg TypeMismatch)
412    ]
413| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
414    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
415    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ??) e, ?»
416    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
417    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
418    | _ ⇒ Error ? (msg TypeMismatch)
419    ]
420| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
421    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
422    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?»
423    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
424    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
425    | _ ⇒ Error ? (msg TypeMismatch)
426    ]
427| _ ⇒ λ_. Error ? (msg TypeMismatch)
428]. whd normalize nodelta @pi2
429qed.
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 (pi1 … 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          [ mk_DPair 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          [ mk_DPair 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          [ mk_DPair 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          [ 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))), ?» »)
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 ⊢ (???% → ?); #E
740#id #H
741cases (identifier_eq ? id tmp)
742destruct #E
743whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
744[ >E >lookup_add_hit @I
745| cases E #NE >lookup_add_miss [ @H | /2/
746] qed.
747
748definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝
749λvars,lbls,s,u,su'.
750  let 〈s',u'〉 ≝ su' in
751  stmt_inv (add_tmps vars u') lbls s' ∧
752  labels_translated lbls s s' ∧
753  tmps_preserved vars u u'.
754
755lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su.
756  trans_inv vars lbls s u su → stmt_inv (add_tmps vars (\snd su)) lbls (\fst su).
757#var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1
758qed.
759
760lemma trans_inv_labels : ∀vars,lbls,s,u,su.
761  trans_inv vars lbls s u su → labels_translated lbls s (\fst su).
762#vars #lbls #s #u * #s' #u' * * #_ #H #_ @H
763qed.
764
765lemma local_id_add_local_oblivious : ∀vars,id,id'.
766  local_id vars id → local_id (add ?? vars id' Local) id.
767#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
768cases (identifier_eq ? id id')
769[ #E >E >lookup_add_hit @I
770| #NE >lookup_add_miss [ @H | /2/
771] qed.
772
773lemma local_id_add_tmps_oblivious : ∀vars,id,u.
774  local_id vars id → local_id (add_tmps vars u) id.
775#vars #id * #u #l #H elim l
776[ //
777| * #id' #ty #tl @local_id_add_local_oblivious
778] qed.
779
780lemma add_tmps_oblivious : ∀vars,lbls,s,u.
781  stmt_inv vars lbls s → stmt_inv (add_tmps vars u) lbls s.
782#vars #lbls #s #u #H
783@(stmt_P_mp … H)
784#s' * #H1 #H2 %
785[ @(stmt_vars_mp … H1)
786  #id @local_id_add_tmps_oblivious
787| @H2
788] qed.
789
790lemma local_id_fresh_tmp : ∀tmp,u,q,u0,vars.
791  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
792#tmp #u #q #u0 #vars
793whd in ⊢ (???% → ?); #E
794destruct
795whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
796@I
797qed.
798
799let 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) ≝
800match s return λs.res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) with
801[ Sskip ⇒ OK ? «〈St_skip, u〉, ?»
802| Sassign e1 e2 ⇒
803    do s' ← translate_assign vars e1 e2;
804    OK ? «〈eject ?? s', u〉, ?»
805| Scall ret ef args ⇒
806    do ef' ← translate_expr vars ef;
807    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
808    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
809    match ret with
810    [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?»
811    | Some e1 ⇒
812        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
813        match dest with
814        [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?»
815        | MemDest r q e1' ⇒
816            let 〈tmp, u〉 as Etmp ≝ alloc_tmp q u in
817            OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?»
818        ]
819    ]
820| Ssequence s1 s2 ⇒
821     do «s1', u1, H1» ← translate_statement vars lbls u s1;
822     do «s2', u2, H2» ← translate_statement vars lbls u1 s2;
823    OK ? «〈St_seq s1' s2', u2〉, ?»
824| Sifthenelse e1 s1 s2 ⇒
825    do e1' ← translate_expr vars e1;
826    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
827    [ ASTint _ _ ⇒ λe1'.
828         do «s1', u, H1» ← translate_statement vars lbls u s1;
829         do «s2', u, H2» ← translate_statement vars lbls u s2;
830        OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?»
831    | _ ⇒ λ_.Error ? (msg TypeMismatch)
832    ] e1'
833| Swhile e1 s1 ⇒
834    do e1' ← translate_expr vars e1;
835    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
836    [ ASTint _ _ ⇒ λe1'.
837         do «s1', u, H1» ← translate_statement vars lbls u s1;
838        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
839        OK ? «〈St_block
840               (St_loop
841                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉, ?»
842    | _ ⇒ λ_.Error ? (msg TypeMismatch)
843    ] e1'
844| Sdowhile e1 s1 ⇒
845    do e1' ← translate_expr vars e1;
846    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
847    [ ASTint _ _ ⇒ λe1'.
848         do «s1',u, H1» ← translate_statement vars lbls u s1;
849        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
850        OK ? «〈St_block
851               (St_loop
852                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉, ?»
853    | _ ⇒ λ_.Error ? (msg TypeMismatch)
854    ] e1'
855| Sfor s1 e1 s2 s3 ⇒
856    do e1' ← translate_expr vars e1;
857    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
858    [ ASTint _ _ ⇒ λe1'.
859         do «s1', u, H1» ← translate_statement vars lbls u s1;
860         do «s2', u, H2» ← translate_statement vars lbls u s2;
861         do «s3', u, H3» ← translate_statement vars lbls u s3;
862        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
863        OK ? «〈St_seq s1'
864             (St_block
865               (St_loop
866                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉, ?»
867    | _ ⇒ λ_.Error ? (msg TypeMismatch)
868    ] e1'
869| Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?»
870| Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?»
871| Sreturn ret ⇒
872    match ret with
873    [ None ⇒ OK ? «〈St_return (None ?), u〉, ?»
874    | Some e1 ⇒
875        do e1' ← translate_expr vars e1;
876        OK ? «〈St_return (Some ? (dp … e1')), u〉, ?»
877    ]
878| Sswitch e1 ls ⇒ Error ? (msg FIXME)
879| Slabel l s1 ⇒
880    do l' as E ← lookup_label lbls l;
881     do «s1', u, H1» ← translate_statement vars lbls u s1;
882    OK ? «〈St_label l' s1', u〉, ?»
883| Sgoto l ⇒
884    do l' as E ← lookup_label lbls l;
885    OK ? «〈St_goto l', u〉, ?»
886| Scost l s1 ⇒
887     do «s1', u, H1» ← translate_statement vars lbls u s1;
888    OK ? «〈St_cost l s1', u〉, ?»
889].
890try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
891try @I
892try (#l #H @(match H in False with [ ]))
893try (#id #H @H)
894[ @add_tmps_oblivious @(use_sig ?? s')
895| @local_id_add_tmps_oblivious @p
896]
897try (@use_sig' #x @expr_vars_mp #i @local_id_add_tmps_oblivious)
898[ 1,3,6: @use_sig' #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious
899| 2,4: @(local_id_fresh_tmp … Etmp)
900| @(alloc_tmp_preserves … Etmp)
901| 7,11: @(stmt_P_mp … (π1 (π1 H1))) #s * #H3 #H4 % [ 1,3: @(stmt_vars_mp … H3) cases H2 #_ #H @H | *: @H4 ]
902| 8,12: @(trans_inv_stmt_inv … H2)
903| 9,13: #l #H cases (Exists_append … H)
904  [ 1,3: #H3 cases H1 * #S1 #L1 #T1 cases (L1 l H3) #l' * #E1 #D1
905    %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
906  | *: #H3 cases H2 * #S2 #L2 #T2 cases (L2 l H3) #l' * #E2 #D2
907    %{l'} % [ 1,3: @E2 | *: @Exists_append_r @D2 ]
908  ]
909| 10,14: cases H2 #_ #TP2 #id #L @TP2 cases H1 #_ #TP1 @TP1 @L
910| 15,18: @(π1 (π1 H1))
911| 16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1
912  %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
913| 17,20: @(π2 H1)
914(* Sfor *)
915| @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @(π2 H2) @H | @H5 ]
916| @(π1 (π1 H3))
917| @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @H | @H5 ]
918| #l #H cases (Exists_append … H)
919  [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1
920    %{l'} % [ @E1 | @Exists_append_l @D1 ]
921  | #EX cases (Exists_append … EX)
922    [ #EX2 cases H2 * #S2 #L2 #_ cases (L2 l EX2) #l' * #E2 #D2
923      %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ]
924    | #EX3 cases H3 * #S3 #L3 #_ cases (L3 l EX3) #l' * #E3 #D3
925      %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ]
926    ]
927  ]
928| #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H
929(* Slabel *)
930| %{l} @E
931| @(π1 (π1 H1))
932| #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
933| @(π2 H1)
934(* Sgoto *)
935| %{l} @E
936| @(π1 (π1 H1))
937(* Scost *)
938| @(π2 (π1 H1))
939| @(π2 H1)
940] qed.
941
942
943axiom ParamGlobalMixup : String.
944
945(* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
946definition 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) ≝
947λvars,ls,s0,u,params,s. foldl ?? (λsu,it.
948  let 〈id,ty〉 ≝ it in
949   do «s,u, Is» ← su;
950  do t as E ← lookup' vars id;
951  match t return λx.? → ? with
952  [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is»
953  | Stack n ⇒ λE.
954      do q ← match access_mode ty with
955      [ By_value q ⇒ OK ? q
956      | By_reference r ⇒ OK ? (Mpointer r)
957      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
958      ];
959      OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, u〉, ?»
960  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
961  ] E) (OK ? s) params.
962try @conj try @conj try @conj try @conj try @conj try @conj
963try @I
964[ @(expr_vars_mp … (λid. local_id_add_tmps_oblivious vars id u)) whd >E @I
965| @(π1 (π1 Is))
966| @(π2 (π1 Is))
967| @(π2 Is)
968] qed.
969
970(*
971lemma local_id_add_local : ∀vars,id,id'.
972  local_id vars id →
973  local_id (add ?? vars id' Local) id.
974#vars #id #id' #H
975whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
976[ #E < E >lookup_add_hit //
977| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
978] qed.
979*)
980axiom DuplicateLabel : String.
981
982definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
983λlbls0,lbls,ls.
984 ∀l,l'. lookup_label lbls l = OK ? l' →
985 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.
986
987lemma lookup_label_add : ∀lbls,l,l'.
988  lookup_label (add … lbls l l') l = OK ? l'.
989#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
990qed.
991
992lemma lookup_label_miss : ∀lbls,l,l',l0.
993  l0 ≠ l →
994  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
995#lbls #l #l' #l0 #NE
996whd in ⊢ (??%%);
997>lookup_add_miss
998[ @refl | @NE ]
999qed. 
1000
1001let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝
1002match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with
1003[ nil ⇒ OK ? «lbls, ?»
1004| cons l t ⇒
1005    match lookup_label lbls l return λx.lookup_label lbls l = x → ? with
1006    [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel)
1007    | Error _ ⇒ λLOOK.
1008        let 〈l',u1〉 ≝ fresh … u in
1009        do lbls1 ← populate_lenv t (add … lbls l l') u1;
1010        OK ? «eject … lbls1, ?»
1011    ] (refl ? (lookup_label lbls l))
1012].
1013[ #l #l' #H %2 @H
1014| cases lbls1 #lbls' #I whd in ⊢ (??%?);
1015  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
1016  [ #E %1 %1 @E
1017  | #NE cases (I l1 l1' E1)
1018    [ #H %1 %2 @H
1019    | #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H
1020    ]
1021  ]
1022] qed.
1023
1024definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝
1025λbody.
1026  do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
1027  OK ? «lbls, ?».
1028#l #l' #E cases (H l l' E) //
1029whd in ⊢ (??%? → ?); #H destruct
1030qed.
1031
1032lemma local_id_split : ∀vars,tmpgen,i.
1033  local_id (add_tmps vars tmpgen) i →
1034  local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
1035#vars #tmpgen #i
1036whd in ⊢ (?%? → ?);
1037elim (tmp_env tmpgen)
1038[ #H %1 @H
1039| * #id #ty #tl #IH
1040  cases (identifier_eq ? i id)
1041  [ #E >E #H %2 whd %1 @refl
1042  | #NE #H cases (IH ?)
1043    [ #H' %1 @H'
1044    | #H' %2 %2 @H'
1045    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
1046      >lookup_add_miss in H; [ #H @H | @NE ]
1047    ]
1048  ]
1049] qed.
1050
1051lemma Exists_squeeze : ∀A,P,l1,l2,l3.
1052  Exists A P (l1@l3) → Exists A P (l1@l2@l3).
1053#A #P #l1 #l2 #l3 #EX
1054cases (Exists_append … EX)
1055[ #EX1 @Exists_append_l @EX1
1056| #EX3 @Exists_append_r @Exists_append_r @EX3
1057] qed.
1058
1059definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝
1060λtmpuniverse, globals, f.
1061  do «lbls, Ilbls» ← build_label_env (fn_body f);
1062  let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
1063  let tmp ≝ mk_tmpgen tmpuniverse [ ] in
1064  do s ← translate_statement vartypes lbls tmp (fn_body f);
1065   do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
1066  OK ? (mk_internal_function
1067    (opttyp_of_type (fn_return f))
1068    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
1069    ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
1070    stacksize
1071    s ?).
1072cases Is * #S #L #TP
1073@(stmt_P_mp ???? S)
1074#s1 * #H1 #H2 %
1075[ @(stmt_vars_mp … H1)
1076  #i #H
1077  cases (local_id_split … H)
1078  [ #H' @Exists_squeeze >map_append
1079    @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) @H'
1080                | skip
1081                | * #id #ty #E1 <E1 @refl
1082                ]
1083  | #EX @Exists_append_r @Exists_append_l @EX
1084  ]
1085| @(stmt_labels_mp … H2)
1086  #l * #l' #LOOKUP
1087  lapply (Ilbls l' l LOOKUP) #DEFINED
1088  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex)
1089  #H @H
1090] qed.
1091
1092definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝
1093λtmpuniverse,globals,f.
1094match f with
1095[ CL_Internal fn ⇒ do fn' ← translate_function tmpuniverse globals fn; OK ? (Internal ? fn')
1096| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
1097].
1098
1099(* TODO: move universe generation to higher level once we do runtime function
1100   generation.  Cheating a bit - we only need the new identifiers to be fresh
1101   for individual functions. *)
1102include "Clight/fresh.ma".
1103
1104definition clight_to_cminor : clight_program → res Cminor_program ≝
1105λp.
1106  let tmpuniverse ≝ universe_for_program p in
1107  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
1108  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
1109  let globals ≝ fun_globals @ var_globals in
1110  transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
Note: See TracBrowser for help on using the repository browser.