source: src/Clight/toCminor.ma @ 1871

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

Change Clight to Cminor compilation to use gotos rather than loops, blocks
and exits. (Commit on behalf of Ilias)

File size: 70.1 KB
Line 
1include "Clight/Csyntax.ma".
2include "Clight/TypeComparison.ma".
3include "basics/lists/list.ma".
4include "Clight/fresh.ma".
5
6(* Identify local variables that must be allocated memory. *)
7(* These are the variables whose addresses are taken. *)
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
78(* Defines where a variable should be allocated. *)
79inductive var_type : Type[0] ≝
80| Global : region → var_type  (* A global, allocated statically in a given region (which one ???)  *)
81| Stack  : nat → var_type     (* On the stack, at a given height *)
82| Local  : var_type           (* Locally (hopefully, in a register) *)
83.
84
85(* A map associating each variable identifier to its allocation mode and its type. *)
86definition var_types ≝ identifier_map SymbolTag (var_type × type).
87
88axiom UndeclaredIdentifier : String.
89
90definition lookup' ≝
91λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
92
93(* Assert that an identifier is a local variable with the given typ. *)
94definition local_id : var_types → ident → typ → Prop ≝
95λvars,id,t. match lookup' vars id with [ OK vt ⇒ match (\fst vt) with [ Global _ ⇒ False | _ ⇒ t = typ_of_type (\snd vt) ] | _ ⇒ False ].
96
97(* Note that the semantics allows locals to shadow globals.
98   Parameters start out as locals, but get stack allocated if their address
99   is taken.  We will add code to store them if that's the case.
100 *)
101
102(* Some kind of data is never allocated in registers, even if it fits, typically structured data. *)
103definition always_alloc : type → bool ≝
104λt. match t with
105[ Tarray _ _ _ ⇒ true
106| Tstruct _ _ ⇒ true
107| Tunion _ _ ⇒ true
108| _ ⇒ false
109].
110
111(* This builds a [var_types] map characterizing the allocation mode, of variables,
112 * and it returns a stack usage for the function (in bytes, according to [sizeof]) *)
113definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝
114λglobals, f.
115  (* globals are added into a map, with var_type Global, region π_2(idrt) and type π_3(idrt) *)
116  let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in
117  (* variables in the body of the function are gathered in [mem_vars] *)
118  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
119  (* iterate on the parameters and local variables of the function, with a tuple (map, stack_high) as an accumulator *)
120  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
121    let 〈m,stack_high〉 ≝ ms in
122    let 〈id,ty〉 ≝ v in         
123    let 〈c,stack_high〉 ≝
124      (* if the (local, parameter) variable is of a compound type OR if its adress is taken, we allocate it on the stack. *)
125      if always_alloc ty ∨ mem_set ? mem_vars id then
126        〈Stack stack_high,stack_high + sizeof ty〉
127      else
128        〈Local, stack_high〉
129    in
130      〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
131  〈m,stacksize〉.
132
133(* A local variable id' status is not modified by the removal of a global variable id : id' is still local *)
134lemma local_id_add_global : ∀vars,id,r,t,id',t'.
135  local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'.
136#var #id #r #t #id' #t'
137whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
138cases (identifier_eq ? id id')
139[ #E >E >lookup_add_hit whd in ⊢ (% → ?); *
140| #NE >lookup_add_miss /2/
141] qed.
142
143(* If I add a variable id ≠ id', then id' is still local *)
144lemma local_id_add_miss : ∀vars,id,vt,id',t'.
145  id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'.
146#vars #id #vt #id' #t' #NE
147whd in ⊢ (% → %);
148whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
149>lookup_add_miss
150[ #H @H | /2/ ]
151qed.
152
153(* After characterise_vars, a variable in the resulting map is either a global or a "local"(register or stack allocated) *)
154lemma characterise_vars_src : ∀gl,f,vars,n.
155  characterise_vars gl f = 〈vars,n〉 →
156  ∀id. present ?? vars id →
157   (∃r,ty. lookup' vars id = OK ? 〈Global r,ty〉 ∧ Exists ? (λx.x = 〈〈id,r〉,ty〉) gl) ∨
158   ∃t.local_id vars id t.
159#globals #f
160whd in ⊢ (∀_.∀_.??%? → ?);
161elim (fn_params f @ fn_vars f)
162[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H %1
163  elim globals in H ⊢ %;
164  [ normalize * #H cases (H (refl ??))
165  | * * #id #rg #ty #tl #IH #H
166    cases (identifier_eq ? i id)
167    [ #E <E %{rg} %{ty} % [ whd in ⊢ (??%?); >lookup_add_hit // | %1 // ]
168    | #NE cases (IH ?)
169      [ #rg' * #ty' * #H1 #H2 %{rg'} %{ty'} %
170        [ whd in ⊢ (??%?); >lookup_add_miss  [ @H1 | @NE ]
171        | %2 @H2
172        ]
173      | whd in H ⊢ %; >lookup_add_miss in H; //
174      ]
175    ]
176  ]
177| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
178  #H >(contract_pair var_types nat ?) in E;
179  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
180  cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
181  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
182  cases (identifier_eq ? i id)
183  [ 1,3: #E' <E' in EQ2:%; #EQ2 %2 %{(typ_of_type ty)}
184         destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]);
185         >lookup_add_hit @refl
186  | *: #NE cases (IH m0 n0 ? i ?)
187    [ 1,5: * #rg' * #ty' * #H1 #H2 %1 %{rg'} %{ty'} % //
188           destruct (EQ2) whd in ⊢ (??%?); >lookup_add_miss try @NE @H1
189    | 2,6: * #t #H1 %2 %{t} destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ?|_ ⇒ ?]);
190           >lookup_add_miss //
191    | 3,7: <EQ @refl
192    | *: destruct (EQ2) whd in H; >lookup_add_miss in H; //
193    ]
194  ]
195] qed.
196
197(* A local variable in a function is either a parameter or a "local" (:=register or stack alloc'd)
198 * variable, with the right type *)
199lemma characterise_vars_all : ∀l,f,vars,n.
200  characterise_vars l f = 〈vars,n〉 →
201  ∀i,t. local_id vars i t →
202        Exists ? (λx.\fst x = i ∧ typ_of_type (\snd x) = t) (fn_params f @ fn_vars f).
203#globals #f
204whd in ⊢ (∀_.∀_.??%? → ?);
205elim (fn_params f @ fn_vars f)
206[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #t #H @False_ind
207  elim globals in H;
208  [ normalize //
209  | * * #id #rg #t #tl #IH whd in ⊢ (?%?? → ?); #H @IH @(local_id_add_global … H)
210  ]
211| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i #t
212
213  #H >(contract_pair var_types nat ?) in E;
214  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
215  cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
216  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
217
218  cases (identifier_eq ? id i)
219  [ 1,3: #E' >E' in EQ2:%; #EQ2 % %
220    [ 1,3: @refl
221    | *: destruct (EQ2) change with (add ?????) in H:(?%??);
222      whd in H; whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]); >lookup_add_hit in H;
223      whd in ⊢ (% → ?); #E'' >E'' @refl
224    ]
225  | *: #NE %2 @(IH m0 n0)
226    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
227    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
228    ]
229  ]
230] qed.
231
232(* The map generated by characterise_vars is "correct" wrt the fresh ident generator of tag [u],
233   i.e. by generating fresh idents with u, we risk no collision with the idents in the map domain. *)
234lemma characterise_vars_fresh : ∀gl,f,vars,n,u.
235  characterise_vars gl f = 〈vars,n〉 →              (* If we generate a map ... *)
236  globals_fresh_for_univ ? gl u →                  (* and the globals are out of the idents generated by u *)
237  fn_fresh_for_univ f u →                          (* and the variables of the function f are cool with u too ... *)
238  fresh_map_for_univ … vars u.                     (* then there won't be collisions between the map and idents made from u *)
239#gl #f #vars #n #u #CH #GL #FN
240#id #H
241cases (characterise_vars_src … CH … H)
242[ * #rg * #ty * #H1 #H2
243  cases (Exists_All … H2 GL) * * #id' #rg' #ty' * #E #H destruct //
244| * #t #H lapply (characterise_vars_all … CH id t H) #EX
245  cases (Exists_All … EX FN) * #id' #ty' * * #E1 #E2 #H' -H destruct //
246] qed.
247
248include "Cminor/syntax.ma".
249include "common/Errors.ma".
250
251alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
252
253axiom BadlyTypedAccess : String.
254axiom BadLvalue : String.
255axiom MissingField : String.
256
257(* type_should_eq enforces that two types are equal and eliminates this equality by
258   transporting P ty1 to P ty2. If ty1 != ty2, then Error *)
259definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
260λty1,ty2,P,p.
261  do E ← assert_type_eq ty1 ty2;
262  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). 
263
264(* same gig for regions *)
265definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
266* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
267qed.
268
269(* same gig for AST typs *)
270definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
271* [ #sz1 #sg1 | #r1 | #sz1 ]
272* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
273[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
274  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
275| *; #P #p @(region_should_eq r1 ?? p)
276| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
277] qed.
278
279alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
280alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
281
282(* XXX: For some reason matita refuses to pick the right one unless forced. *)
283alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)".
284
285(* Translates a Clight unary operation into a Cminor one, while checking
286 * that the domain and codomain types are consistent. *)
287definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t') ≝
288λt,t'.λop:CLunop.
289  match op with
290  [ Onotbool ⇒
291      match t return λt. res (CMunop t t') with
292      [ ASTint sz sg ⇒
293          match t' return λt'. res (CMunop ? t') with
294          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
295          | _ ⇒ Error ? (msg TypeMismatch)
296          ]
297      | ASTptr r ⇒
298          match t' return λt'. res (CMunop ? t') with
299          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
300          | _ ⇒ Error ? (msg TypeMismatch)
301          ]
302      | _ ⇒ Error ? (msg TypeMismatch)
303      ]
304  | Onotint ⇒
305      match t' return λt'. res (CMunop t t') with
306      [ ASTint sz sg ⇒ typ_should_eq ?? (λt. CMunop t (ASTint ??)) (Onotint sz sg)
307      | _ ⇒ Error ? (msg TypeMismatch)
308      ]
309  | Oneg ⇒
310      match t' return λt'. res (CMunop t t') with
311      [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg)
312      | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz)
313      | _ ⇒ Error ? (msg TypeMismatch)
314      ]
315  ]. @I qed.
316
317(* Translates a Clight addition into a Cminor one. Four cases to consider :
318  - integer/integer add
319  - fp/fp add
320  - pointer/integer
321  - integer/pointer.
322  Consistency of the type is enforced by explicit checks.
323*)
324definition translate_add ≝
325λty1,e1,ty2,e2,ty'.
326let ty1' ≝ typ_of_type ty1 in
327let ty2' ≝ typ_of_type ty2 in
328match classify_add ty1 ty2 with
329[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
330| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
331(* XXX using the integer size for e2 as the offset's size isn't right, because
332   if e2 produces an 8bit value then the true offset might overflow *)
333| add_case_pi ty ⇒
334    match ty2' with
335    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
336    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
337    ]
338| add_case_ip ty ⇒
339    match ty1' with
340    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
341    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
342    ]
343| add_default ⇒ Error ? (msg TypeMismatch)
344].
345
346
347definition translate_sub ≝
348λty1,e1,ty2,e2,ty'.
349let ty1' ≝ typ_of_type ty1 in
350let ty2' ≝ typ_of_type ty2 in
351match classify_sub ty1 ty2 with
352[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
353| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
354(* XXX choosing offset sizes? *)
355| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
356| sub_case_pp ty ⇒
357    match ty' with (* XXX overflow *)
358    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
359    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
360    ]
361| sub_default ⇒ Error ? (msg TypeMismatch)
362].
363
364definition translate_mul ≝
365λty1,e1,ty2,e2,ty'.
366let ty1' ≝ typ_of_type ty1 in
367let ty2' ≝ typ_of_type ty2 in
368match classify_mul ty1 ty2 with
369[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
370| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
371| mul_default ⇒ Error ? (msg TypeMismatch)
372].
373
374definition translate_div ≝
375λty1,e1,ty2,e2,ty'.
376let ty1' ≝ typ_of_type ty1 in
377let ty2' ≝ typ_of_type ty2 in
378match classify_div ty1 ty2 with
379[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
380| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
381| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
382| div_default ⇒ Error ? (msg TypeMismatch)
383].
384
385definition translate_mod ≝
386λty1,e1,ty2,e2,ty'.
387let ty1' ≝ typ_of_type ty1 in
388let ty2' ≝ typ_of_type ty2 in
389match classify_mod ty1 ty2 with
390[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
391| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
392| mod_default ⇒ Error ? (msg TypeMismatch)
393].
394
395definition translate_shr ≝
396λty1,e1,ty2,e2,ty'.
397let ty1' ≝ typ_of_type ty1 in
398let ty2' ≝ typ_of_type ty2 in
399match classify_shr ty1 ty2 with
400[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
401| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
402| shr_default ⇒ Error ? (msg TypeMismatch)
403].
404
405definition translate_cmp ≝
406λc,ty1,e1,ty2,e2,ty'.
407let ty1' ≝ typ_of_type ty1 in
408let ty2' ≝ typ_of_type ty2 in
409match classify_cmp ty1 ty2 with
410[ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
411| cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
412| cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
413| cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
414| cmp_default ⇒ Error ? (msg TypeMismatch)
415].
416
417definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
418λop,ty1,e1,ty2,e2,ty.
419let ty' ≝ typ_of_type ty in
420match op with
421[ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
422| Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
423| Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
424| Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
425| Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
426| Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
427| Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
428| Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
429| Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
430| Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
431| Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
432| One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
433| Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
434| Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
435| Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
436| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
437].
438
439(* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on
440  all the variables of a program. [translate_binop_vars], given
441  a predicate verified for all variables of subexprs e1 and e2, produces
442  a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this
443  predicate. *)
444lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
445  expr_vars ? e1 P →
446  expr_vars ? e2 P →
447  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
448  expr_vars ? e P.
449#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
450whd in ⊢ (??%? → ?);
451[ cases (classify_add ty1 ty2)
452  [ 3,4: #z ] whd in ⊢ (??%? → ?);
453  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
454    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
455    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
456  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
457    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
458    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
459  | *: #E destruct (E) % try @H1 @H2
460  ]
461| cases (classify_sub ty1 ty2)
462  [ 3,4: #z] whd in ⊢ (??%? → ?);
463  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
464    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
465    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
466  | *: #E destruct (E) % try @H1 try @H2 % // @H2
467  ]
468| cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
469    % try @H1 @H2
470| cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
471    % try @H1 @H2
472| cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
473    % try @H1 @H2
474| 6,7,8,9: #E destruct % try @H1 @H2
475| cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
476| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
477] qed.
478
479(* We'll need to implement proper translation of pointers if we really do memory
480   spaces. *)
481(* This function performs leibniz-style subst if r1 = r2, and fails otherwise. *)
482definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
483λr1,r2,P.
484  match r1 return λx.P x → res (P r2) with
485  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
486  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
487  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
488  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
489  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
490  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
491  ].
492
493(* Simple application of [check_region] to translate between terms. *)
494definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
495λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
496
497axiom FIXME : String.
498
499(* Given a source and target type, translate an expession of type source to type target *)
500definition translate_cast : ∀P. ∀ty1:type.∀ty2:type. (Σe:CMexpr (typ_of_type ty1). expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
501λP,ty1,ty2.
502match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
503[ Tint sz1 sg1 ⇒ λe.
504    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
505    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
506    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)
507    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
508    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
509    | _ ⇒ Error ? (msg TypeMismatch)
510    ]
511| Tfloat sz1 ⇒ λe.
512    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
513    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?»
514    | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *)
515    | _ ⇒ Error ? (msg TypeMismatch)
516    ]
517| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
518    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
519    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ??) e, ?»
520    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
521    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
522    | _ ⇒ Error ? (msg TypeMismatch)
523    ]
524| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
525    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
526    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?»
527    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
528    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
529    | _ ⇒ Error ? (msg TypeMismatch)
530    ]
531| _ ⇒ λ_. Error ? (msg TypeMismatch)
532]. whd normalize nodelta @pi2
533qed.
534
535(* Small inversion lemma : if the access mode of a type is by reference, then it must be a ptr type. *)
536lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
537*
538[ 5: #r #ty #n #r' normalize #E destruct @refl
539| 6: #args #ret #r normalize #E destruct @refl
540| *: normalize #a #b try #c try #d destruct
541  [ cases a in d; normalize; cases b; normalize #E destruct
542  | cases a in c; normalize #E destruct
543  ]
544] qed.
545
546(* Translate Clight exprs into Cminor ones.
547  Arguments :
548  - vars:var_types, an environment mapping each variable to a couple (allocation mode, type)
549  - e:expr, the expression to be converted
550  Result : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars))
551  that is, either
552  . an error
553  . an expression e', matching the type of e, such that e' respect the property that all variables
554    in it are not global. In effect, [translate_expr] will replace global variables by constant symbols.
555*)
556let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
557match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
558[ Expr ed ty ⇒
559  match ed with
560  [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
561  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
562  | Evar id ⇒
563      do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *)
564      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
565      [ Global r ⇒ λ_.
566          (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on
567             its access mode:
568             - By_value q, where q is a memory chunk specification (whitch should match the type of the global)
569             - By_reference, and we only take the adress of the variable
570             - By_nothing : error
571           *)
572          match access_mode ty with
573          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
574          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
575          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
576          ]
577      | Stack n ⇒ λE.
578          (* We have decided that the variable should be allocated on the stack,
579           * because its adress was taken somewhere or becauste it's a structured data. *)
580          match access_mode ty with
581          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
582          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
583          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
584          ]
585          (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *)
586      | 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, ?»)
587      ] E
588  | Ederef e1 ⇒
589      do e1' ← translate_expr vars e1;
590      (* According to the way the data pointed to by e1 is accessed, the generated Cminor code will vary.
591        - if e1 is a kind of int* ptr, then we load ("Mem") the ptr returned by e1
592        - if e1 is a struct* or a function ptr, then we acess by reference, in which case we :
593           1) check the consistency of the regions in the type of e1 and in the access mode of its type
594           2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?)
595      *)
596      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
597      [ ASTptr r ⇒ λe1'.
598          match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
599          [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (pi1 … e1'), ?»
600          | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
601                                  OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
602          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
603          ] (access_mode_typ ty)
604      | _ ⇒ λ_. Error ? (msg TypeMismatch)
605      ] e1'
606  | Eaddrof e1 ⇒
607      do e1' ← translate_addr vars e1;
608      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
609      [ ASTptr r ⇒
610          match e1' with
611          [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1'
612          ]
613      | _ ⇒ Error ? (msg TypeMismatch)
614      ]
615  | Eunop op e1 ⇒
616      do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
617      do e1' ← translate_expr vars e1;
618      OK ? «Op1 ?? op' e1', ?»
619  | Ebinop op e1 e2 ⇒
620      do e1' ← translate_expr vars e1;
621      do e2' ← translate_expr vars e2;
622      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
623      OK ? «e', ?»
624  | Ecast ty1 e1 ⇒
625      do e1' ← translate_expr vars e1;
626      do e' ← translate_cast ? (typeof e1) ty1 e1';
627      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
628      OK ? e'
629  | Econdition e1 e2 e3 ⇒
630      do e1' ← translate_expr vars e1;
631      do e2' ← translate_expr vars e2;
632      do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
633      do e3' ← translate_expr vars e3;
634      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
635      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with
636      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
637      | _ ⇒ λ_.Error ? (msg TypeMismatch)
638      ] e1'
639  | Eandbool e1 e2 ⇒
640      do e1' ← translate_expr vars e1;
641      do e2' ← translate_expr vars e2;
642      match ty with
643      [ Tint sz _ ⇒
644        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
645        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
646        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?»
647        | _ ⇒ λ_.Error ? (msg TypeMismatch)
648        ] e1'
649      | _ ⇒ Error ? (msg TypeMismatch)
650      ]
651  | Eorbool e1 e2 ⇒
652      do e1' ← translate_expr vars e1;
653      do e2' ← translate_expr vars e2;
654      match ty with
655      [ Tint sz _ ⇒
656        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
657        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
658        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
659        | _ ⇒ λ_.Error ? (msg TypeMismatch)
660        ] e1'
661      | _ ⇒ Error ? (msg TypeMismatch)
662      ]
663  | Esizeof ty1 ⇒
664      match ty with
665      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
666      | _ ⇒ Error ? (msg TypeMismatch)
667      ]
668  | Efield e1 id ⇒
669      match typeof e1 with
670      [ Tstruct _ fl ⇒
671          do e1' ← translate_addr vars e1;
672          match e1' with
673          [ mk_DPair r e1' ⇒
674            do off ← field_offset id fl;
675            match access_mode ty with
676            [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
677            | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
678            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
679            ]
680          ]
681      | Tunion _ _ ⇒
682          do e1' ← translate_addr vars e1;
683          match e1' with
684          [ mk_DPair r e1' ⇒
685            match access_mode ty return λx. access_mode ty = x → res ? with
686            [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
687            | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
688                                OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
689            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
690            ] (refl ? (access_mode ty))
691          ]
692      | _ ⇒ Error ? (msg BadlyTypedAccess)
693      ]
694  | Ecost l e1 ⇒
695      do e1' ← translate_expr vars e1;
696      do e' ← OK ? «Ecost ? l e1',?»;
697      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
698  ]
699]
700
701(* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1].   *)
702and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
703match e with
704[ Expr ed _ ⇒
705  match ed with
706  [ Evar id ⇒
707      do 〈c,t〉 ← lookup' vars id;
708      match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with
709      [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol id 0), ?»❭
710      | Stack n ⇒ OK ? ❬Any, «Cst ? (Oaddrstack n), ?»❭
711      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
712      ]
713  | Ederef e1 ⇒
714      do e1' ← translate_expr vars e1;
715      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (𝚺r. Σz:CMexpr (ASTptr r). ?) with
716      [ ASTptr r ⇒ λe1'.OK ? ❬r, e1'❭
717      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
718      ] e1'
719  | Efield e1 id ⇒
720      match typeof e1 with
721      [ Tstruct _ fl ⇒
722          do e1' ← translate_addr vars e1;
723          do off ← field_offset id fl;
724          match e1' with
725          [ 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))), ?» ❭)
726          ]
727      | Tunion _ _ ⇒ translate_addr vars e1
728      | _ ⇒ Error ? (msg BadlyTypedAccess)
729      ]
730  | _ ⇒ Error ? (msg BadLvalue)
731  ]
732].
733whd try @I
734[ >E whd @refl
735| >(E ? (refl ??)) @refl
736| 3,4: @pi2
737| @(translate_binop_vars … E) @pi2
738| % [ % ] @pi2
739| % [ % @pi2 ] whd @I
740| % [ % [ @pi2 | @I ] | @pi2 ]
741| % [ @pi2 | @I ]
742| % [ @pi2 | @I ]
743| >(access_mode_typ … E) @refl
744| @pi2
745| @pi2
746| % [ @pi2 | @I ]
747] qed.
748
749inductive destination (vars:var_types) : Type[0] ≝
750| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
751| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
752
753(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
754  /Clight/ expression, not converted by translate_expr. We thus have to do part of the work
755  of [translate_expr] in this function. [translate_dest] will convert e1
756   into a proper destination for an assignement operation. We proceed by case analysis on e1.
757   - if e1 is a variable [id], then we proceed by case analysis on its allocation mode:
758      - if [id] is allocated locally (in a register), then id becomes directly
759        the target for the assignement, as (IdDest vars id t H), where t is the type
760        of id, and H asserts that id is indeed a local variable.
761      - if [id] is a global variable stored in region [r], then we perform [translate_expr]'s
762        job and return an adress, given as a constant symbol corresponding to [id], with
763        region r and memory chunk specified by the access mode of the rhs type ty2 of [e2].
764      - same thing for stack-allocated variables, except that we don't specify any region.
765   - if e1 is not a variable, we use [translate_addr] to generate a Cminor expression computing
766    the adres of e1
767*)
768definition translate_dest ≝
769λvars,e1,ty2.
770    do q ← match access_mode ty2 with
771           [ By_value q ⇒ OK ? q
772           | By_reference r ⇒ OK ? (Mpointer r)
773           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
774           ];
775    match e1 with
776    [ Expr ed1 ty1 ⇒
777        match ed1 with
778        [ Evar id ⇒
779            do 〈c,t〉 as E ← lookup' vars id;
780            match c return λx.? → ? with
781            [ Local ⇒ λE. OK ? (IdDest vars id t ?)
782            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
783            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
784            ] E
785        | _ ⇒
786            do e1' ← translate_addr vars e1;
787            match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r q e1') ]
788        ]
789    ].
790whd // >E @refl
791qed.
792
793(* [lenv] is the type of maps from Clight labels to Cminor labels. *)
794definition lenv ≝ identifier_map SymbolTag (identifier Label).
795
796axiom MissingLabel : String.
797
798(* Find the Cminor label corresponding to [l] or fail. *)
799definition lookup_label ≝
800λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
801
802(* True iff the Cminor label [l] is in the codomain of [lbls] *)
803definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.
804
805(* True iff The Clight label [l] is in the domain of [lbls] *)
806definition label_in_domain ≝ λlbls:lenv. λl. present ?? lbls l.
807
808let rec fresh_list_for_univ (l:list (identifier Label)) (u:universe Label) ≝
809match l with
810[ nil ⇒ True
811| cons elt tl ⇒ fresh_for_univ ? elt u ∧ fresh_list_for_univ tl u].
812
813record labgen : Type[0] ≝ {
814  labuniverse   : universe Label;
815  label_genlist    : list (identifier Label);
816  genlist_is_fresh : fresh_list_for_univ label_genlist labuniverse
817}.
818
819lemma fresh_list_stays_fresh : ∀l,tmp,u,u'. fresh_list_for_univ l u → 〈tmp,u'〉=fresh Label u → fresh_list_for_univ l u'.
820#l elim l
821[ 1: normalize //
822| 2: #hd #tl #Hind #tmp #u #u' #HA #HB
823  whd
824  @conj
825  [ 1: whd in HA ⊢ ?;
826    elim HA #HAleft #HAright
827    @(fresh_remains_fresh ? hd tmp u u') assumption
828  | 2: whd in HA ⊢ ?;
829    elim HA #HAleft #HAright   
830    @Hind //
831  ]
832]
833qed.
834
835definition In ≝ λelttype.λelt.λl.Exists elttype (λx.x=elt) l.   
836
837definition generate_fresh_label :
838 ∀ul. Σlul:(identifier Label × labgen).
839               (And (∀lab. In ? lab (label_genlist ul) → In ? lab (label_genlist (snd … lul)))
840                   (In ? (fst … lul) (label_genlist (snd … lul)))) ≝
841λul.
842let 〈tmp,u〉 as E ≝ fresh ? (labuniverse ul) in
843 «〈tmp, mk_labgen u (tmp::(label_genlist ul)) ?〉, ?».
844[ 1: normalize @conj
845  [ 1: @(fresh_is_fresh ? tmp u (labuniverse ul) ?) assumption
846  | 2: @fresh_list_stays_fresh // ]
847| @conj /2/
848]
849qed.
850
851let rec labels_defined (s:statement) : list ident ≝
852match s with
853[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
854| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
855| Swhile _ s ⇒ labels_defined s
856| Sdowhile _ s ⇒ labels_defined s
857| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
858| Sswitch _ ls ⇒ labels_defined_switch ls
859| Slabel l s ⇒ l::(labels_defined s)
860| Scost _ s ⇒ labels_defined s
861| _ ⇒ [ ]
862]
863and labels_defined_switch (ls:labeled_statements) : list ident ≝
864match ls with
865[ LSdefault s ⇒ labels_defined s
866| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
867].
868
869definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
870
871(* For each label l in s, there exists a matching label l' = lenv(l) defined in s' *)
872definition labels_translated : lenv → statement → stmt → Prop ≝
873λlbls,s,s'.  ∀l.
874  (Exists ? (λl'.l' = l) (labels_defined s)) →
875  ∃l'. lookup_label lbls l = (OK ? l') ∧ ldefined s' l'.
876
877
878(* Invariant on statements, holds during conversion to Cminor *)
879definition stmt_inv ≝  λvars. stmt_P (stmt_vars (local_id vars)).
880
881(* I (Ilias) decided to inline the following definition, to make explicit the data constructed.
882 * This was needed to prove some stuff in translate_statement at some point, but it might be
883 * useless now. If needed, I can revert this change.  *)
884definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝
885λvars,e1,e2.
886do e2' ← translate_expr vars e2;             
887do dest ← translate_dest vars e1 (typeof e2);
888match dest with
889[ IdDest id ty p ⇒
890    do e2' ← type_should_eq (typeof e2) ty ? e2';
891    OK ? «St_assign ? id e2', ?»
892| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
893].
894% try (//)  try (elim e2' //) elim e1' //
895qed.
896
897definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
898λA,B,f,oa.
899match oa with
900[ None ⇒ OK ? (None ?)
901| Some a ⇒ do b ← f a; OK ? (Some ? b)
902].
903
904definition 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) ]) ≝
905λv,e.
906  do e' ← translate_expr v e;
907  OK (Σe:(𝚺t:typ.CMexpr t).?) «❬?, e'❭, ?».
908whd @pi2
909qed.
910
911(* Add the list of typed variables tmpenv to the environment [var_types] with
912   the allocation mode Local. *)
913definition add_tmps : var_types → list (ident × type) → var_types ≝
914λvs,tmpenv.
915  foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs tmpenv.
916
917record tmpgen (vars:var_types) : Type[0] ≝ {
918  tmp_universe : universe SymbolTag;
919  tmp_env : list (ident × type);
920  tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe;
921  tmp_preserved :
922    ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty
923}.
924
925definition alloc_tmp : ∀vars. type → tmpgen vars → ident × (tmpgen vars) ≝
926λvars,ty,g.
927  let 〈tmp,u〉 as E ≝ fresh ? (tmp_universe ? g) in
928  〈tmp, mk_tmpgen ? u (〈tmp, ty〉::(tmp_env ? g)) ??〉.
929[ #id #ty'
930  whd in ⊢ (? → ?%??);
931  whd in ⊢ (% → %);
932  whd in ⊢ (? → match % with [_ ⇒ ? | _ ⇒ ?]); #H
933  >lookup_add_miss
934  [ @(tmp_preserved … g) @H
935  | @(fresh_distinct … E) @(tmp_ok … g)
936    lapply (tmp_preserved … g id ty' H)
937    whd in ⊢ (% → %);
938    whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
939    cases (lookup ??? id)
940    [ * | #x #_ % #E destruct ]
941  ]
942| @fresh_map_add
943  [ @(fresh_map_preserved … E) @(tmp_ok … g)
944  | @(fresh_is_fresh … E)
945  ]
946] qed.
947
948
949lemma lookup_label_hit : ∀lbls,l,l'.
950  lookup_label lbls l = OK ? l' →
951  lpresent lbls l'.
952#lbls #l #l' #E whd %{l} @E
953qed.
954
955(* TODO: is this really needed now? *)
956
957definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝
958λvars,u1,u2.
959  ∀id,ty. local_id (add_tmps vars (tmp_env … u1)) id ty → local_id (add_tmps vars (tmp_env … u2)) id ty.
960
961lemma alloc_tmp_preserves : ∀vars,tmp,u,u',q.
962  〈tmp,u'〉 = alloc_tmp ? q u → tmps_preserved vars u u'.
963#vars #tmp * #u1 #e1 #F1 #P1 * #u2 #e2 #F2 #P2 #q
964whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
965cases (fresh SymbolTag u1) in ⊢ (??%? → ???(match % with [ _ ⇒ ? ]?) → ?);
966#tmp' #u' #E1 #E2 whd in E2:(???%); destruct
967#id #ty #H whd in ⊢ (?%??); whd in H ⊢ %;
968whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
969>lookup_add_miss // @(fresh_distinct … E1) @F1
970whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]) ⊢ %;
971cases (lookup ??? id) in H ⊢ %;
972[ * | #x #_ % #E destruct ]
973qed.
974
975lemma add_tmps_oblivious : ∀vars,s,u.
976  stmt_inv vars s → stmt_inv (add_tmps vars (tmp_env vars u)) s.
977#vars #s #u #H
978@(stmt_P_mp … H)
979#s' #H1 @(stmt_vars_mp … H1) #id #t #H @(tmp_preserved ? u ?? H)
980qed.
981
982lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0.
983  〈tmp,u〉 = alloc_tmp vars ty u0 → local_id (add_tmps vars (tmp_env … u)) tmp (typ_of_type ty).
984#vars #tmp #u #ty #u0
985whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
986cases (fresh SymbolTag (tmp_universe vars u0)) in ⊢ (??%? → ???(match % with [_⇒?]?) → ?);
987* #tmp' #u' #e #E whd in E:(???%);
988destruct
989whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
990@refl
991qed.
992
993
994let rec mklabels (ul:labgen) : (identifier Label) × (identifier Label) × labgen ≝
995  match generate_fresh_label ul with
996  [ mk_Sig res1 H1 ⇒
997     let 〈entry_label, ul1〉 as E1 ≝ res1 in
998     match generate_fresh_label ul1 with
999     [ mk_Sig res2 H2 ⇒
1000        let 〈exit_label, ul2〉 as E2 ≝ res2 in
1001        〈entry_label, exit_label, ul2〉
1002     ]
1003  ].
1004
1005(* When converting loops into gotos, and in order to eliminate blocks, we have
1006 * to convert continues and breaks into goto's, too. We add some "flags" in
1007 * in argument to [translate_statement], meaning that the next encountered break
1008 * or continue has to be converted into a goto to some contained label.
1009 * ConvertTo l1 l2 means "convert continue to goto l1 and convert break to goto l2".
1010 *)
1011inductive convert_flag : Type[0] ≝
1012| DoNotConvert : convert_flag
1013| ConvertTo    : identifier Label → identifier Label → convert_flag. (* continue, break *)
1014
1015let rec labels_of_flag (flag : convert_flag) : list (identifier Label) ≝
1016match flag with
1017[ DoNotConvert ⇒ [ ]
1018| ConvertTo continue break ⇒ continue :: break :: [ ]
1019].
1020
1021(* For a top-level expression, [label-wf] collapses to "all labels are properly declared" *)
1022definition label_wf ≝
1023λ (s : statement) .λ (s' : stmt) .λ (lbls : lenv). λ (flag : convert_flag).
1024    stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'.
1025
1026(* trans_inv is the invariant which is enforced during the translation from Clight to Cminor.
1027  The involved arguments are the following:
1028  . vars:var_types, an environment mapping variables to their types and allocation modes
1029  . lbls:lenv, a mapping from old (Clight) to fresh and new (Cminor) labels,
1030  . s:statement, a Clight statement,
1031  . uv, a fresh variable generator (containing itself some invariants)
1032  . flag, wich maps "break" and "continue" to "gotos"
1033  . su', a couple of a Cminor statement and fresh variable generator.
1034*)
1035definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → ((tmpgen vars) × labgen × stmt) → Prop ≝
1036λvars,lbls,s,uv,flag,su'.
1037  let 〈uv', ul', s'〉 ≝ su' in
1038  stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧   (* remaining variables in s' are local*)
1039  labels_translated lbls s s' ∧                   (* all the labels in s are transformed in label of s' using [lbls] as a map *)
1040  tmps_preserved vars uv uv' ∧                    (* the variables generated are local and grows in a monotonic fashion *)
1041  label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*)
1042                                 
1043let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (s:statement) on s
1044  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) ≝
1045match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) with
1046[ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?»
1047| Sassign e1 e2 ⇒
1048    do e2' ← translate_expr vars e2;              (* rhs *)
1049    do dest ← translate_dest vars e1 (typeof e2); (* e1 *)
1050    match dest with
1051    [ IdDest id ty p ⇒
1052       do e2' ← type_should_eq (typeof e2) ty ? e2';
1053       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
1054    | MemDest r q e1' ⇒
1055       OK ? «〈uv, ul, St_store ? r q e1' e2'〉, ?»
1056    ]
1057| Scall ret ef args ⇒
1058    do ef' ← translate_expr vars ef;
1059    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
1060    do args' ← mmap_sigma ??? (translate_expr_sigma vars) args;
1061    match ret with
1062    [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?»
1063    | Some e1 ⇒
1064        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
1065        match dest with
1066        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
1067        | MemDest r q e1' ⇒
1068            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
1069            OK ? «〈uv1, ul, 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))〉, ?»
1070        ]
1071    ]
1072| Ssequence s1 s2 ⇒
1073    do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1;
1074    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2;
1075    OK ? «〈fgens2, St_seq s1' s2'〉, ?»
1076| Sifthenelse e1 s1 s2 ⇒
1077    do e1' ← translate_expr vars e1;
1078    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
1079    [ ASTint _ _ ⇒ λe1'.
1080         do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1;
1081         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2;
1082        OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
1083    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1084    ] e1'
1085| Swhile e1 s1 ⇒
1086    do e1' ← translate_expr vars e1;
1087    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
1088    [ ASTint _ _ ⇒ λe1'.         
1089         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
1090         match mklabels ul with
1091         [ mk_Sig result Hmklabels =>
1092              let 〈labels, ul1〉 as E1 ≝ result in
1093              let 〈entry, exit〉 as E2 ≝ labels in
1094              do «fgens2, s1',H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1;
1095              let converted_loop ≝
1096               St_label entry
1097               (St_seq
1098                 (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
1099                 (St_label exit St_skip))
1100              in         
1101              OK ? «〈fgens2, converted_loop〉, ?»
1102         ]
1103    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1104    ] e1'
1105| Sdowhile e1 s1 ⇒
1106    do e1' ← translate_expr vars e1;
1107    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
1108    [ ASTint _ _ ⇒ λe1'.
1109         match mklabels ul with
1110         [ mk_Sig result Hmklabels ⇒
1111              let 〈labels, ul1〉 as E1 ≝ result in
1112              let 〈entry, exit〉 as E2 ≝ labels in             
1113              do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1;
1114              let converted_loop ≝
1115               St_label entry
1116                 (St_seq
1117                   (St_seq
1118                     s1'
1119                     (St_ifthenelse ?? e1' (St_goto entry) St_skip)
1120                   )
1121                   (St_label exit St_skip))
1122              in
1123              (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
1124              OK ? «〈fgens2, converted_loop〉, ?»
1125         ]
1126    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1127    ] e1'
1128| Sfor s1 e1 s2 s3 ⇒
1129    do e1' ← translate_expr vars e1;
1130    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
1131    [ ASTint _ _ ⇒ λe1'.
1132         match mklabels ul with
1133         [ mk_Sig result Hmklabels ⇒
1134              let 〈labels, ul1〉 as E ≝ result in
1135              let 〈entry, exit〉 as E2 ≝ labels in                           
1136              do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» flag s1;
1137              do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) «lbls, ?» (ConvertTo entry exit) s2;
1138              do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) «lbls, ?» (ConvertTo entry exit) s3;
1139              (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
1140              let converted_loop ≝
1141                St_seq
1142                 s1'
1143                 (St_label entry
1144                   (St_seq
1145                     (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip)
1146                     (St_label exit St_skip)
1147                    ))
1148              in
1149             OK ? «〈fgens4, converted_loop〉, ?»
1150        ]
1151    | _ ⇒ λ_.Error ? (msg TypeMismatch)
1152    ] e1'
1153| Sbreak ⇒
1154   match flag return λf.flag = f → ? with
1155   [ DoNotConvert ⇒ λEflag.
1156     Error ? (msg FIXME)
1157   | ConvertTo continue_label break_label ⇒ λEflag.
1158     OK ? «〈uv, ul, St_goto break_label〉, ?»
1159   ] (refl ? flag)
1160| Scontinue ⇒
1161  match flag return λf.flag = f → ? with
1162  [ DoNotConvert ⇒ λEflag.
1163    Error ? (msg FIXME)
1164  | ConvertTo continue_label break_label ⇒ λEflag.
1165    OK ? «〈uv, ul, St_goto continue_label〉, ?»
1166  ] (refl ? flag)
1167| Sreturn ret ⇒
1168    match ret with
1169    [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?»
1170    | Some e1 ⇒
1171        do e1' ← translate_expr vars e1;
1172        OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?»
1173    ]
1174| Sswitch e1 ls ⇒ Error ? (msg FIXME)
1175| Slabel l s1 ⇒
1176    do l' as E ← lookup_label lbls l;
1177    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
1178    OK ? «〈fgens1, St_label l' s1'〉, ?»
1179| Sgoto l ⇒
1180    do l' as E ← lookup_label lbls l;
1181    OK ? «〈uv, ul, St_goto l'〉, ?»
1182| Scost l s1 ⇒
1183    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
1184    OK ? «〈fgens1, St_cost l s1'〉, ?»
1185].
1186try @conj try @conj try @conj try @conj try @conj try @conj try @conj
1187try (@I)
1188try (#l #H elim H)
1189try (#size #sign #H assumption)
1190try (#region #H assumption)
1191[ 1,5: @(tmp_preserved … p) ]
1192[ 1,3: elim e2' | 2,9: elim e1' | 4,7,14: elim ef' ]
1193[ 1,2,3,4,5,6,7 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
1194[ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
1195             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
1196             | 3: elim args' // ]
1197| 8: (* we should be able to merge this case with the previous ... *)
1198     @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
1199             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
1200             | 3: elim args' // ]
1201| 2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
1202| 3:  @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)]))
1203       [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars))
1204       [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0)
1205       | 2: assumption ]
1206       | 2: elim args' // ]
1207| 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
1208[ 1: #size #sign | 2: #reg | 3: #fsize ]
1209[ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
1210try @(match fgens1 return λx.x=fgens1 → ? with
1211     [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
1212try @(match fgens2 return λx.x=fgens2 → ? with
1213     [ mk_Prod uv2 ul2 ⇒ λHfgens2.? ] (refl ? fgens2))
1214try @(match fgens3 return λx.x=fgens3 → ? with
1215     [ mk_Prod uv3 ul3 ⇒ λHfgens3.? ] (refl ? fgens3))
1216try @(match fgens4 return λx.x=fgens4 → ? with
1217     [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4))
1218whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3;
1219try (elim H1 -H1 * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1)
1220try (elim H2 -H2 * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2)
1221try (elim H3 -H3 * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3)
1222[ 1,2: #Hind1 #Hind2 | 3,4,9,11: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
1223try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
1224[ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal)
1225| 2: #l #H cases (Exists_append ???? H) #Hcase
1226         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1227           [ 1: @(proj1 ?? Hlabel)
1228           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
1229         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1230           [ 1: @(proj1 ?? Hlabel)
1231           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
1232         ]
1233| 3,9: #id #ty #H @(Htmps_pres2 … (Htmps_pres1 id ty H)) ]
1234[ 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
1235[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1236     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
1237                | 2,5: #H %1 %2 assumption
1238                | 3,6: #H %2 assumption ]
1239(* if/then/else *)
1240| 3: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
1241| 4: whd #l #H
1242       cases (Exists_append ???? H) #Hcase
1243         [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1244           [ 1: @(proj1 ?? Hlabel)
1245           | 2: normalize @Exists_append_l @(proj2 … Hlabel) ]
1246         | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1247           [ 1: @(proj1 ?? Hlabel)
1248           | 2: normalize @Exists_append_r @(proj2 … Hlabel) ]
1249         ]
1250]                 
1251[ 1: 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ]
1252[ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1253     #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H)
1254                | 2,5: #H %1 %2 assumption
1255                | 3,6: #H %2 assumption ] ]
1256try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
1257[ 1,9,19,32: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
1258| 2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
1259| 3,10: whd #l #H normalize in H;
1260         elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
1261         @conj
1262         [ 1,3: @(proj1 … Hlabel)
1263         | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
1264              @(proj2 … Hlabel) ]
1265| 30: whd %2 %2 whd /2/
1266| 31: whd %2 whd /2/
1267| 4,16: whd %1 %1 normalize /2/
1268| 5,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1269   #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
1270              | 2,6: #H %1 %2 assumption
1271              | 3,7: #H <H %1 %1 normalize /2/
1272              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2
1273                                                 @Exists_append_r normalize /2/
1274                                               | 2,4: * ]
1275              ]
1276| 6: normalize %1 %1 %1 //                                                                                   
1277| 7,14: normalize %1 %1 %2 @Exists_append_r normalize /2/
1278| 11,13: whd %1 %1 normalize /2/
1279| 15: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
1280                   | 2: #H elim (Hlabels_tr1 label H)
1281                         #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
1282                         [ 1: // | 2: whd %2 assumption ]
1283                   ]
1284| 17: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1285   #l * try * [ 1: #H %1 %1 normalize %2 @H
1286              | 2: #H %1 %2 assumption
1287              | 3: #H %2 assumption ]
1288| 18: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
1289   #H @(Htmps_pres3 … (Htmps_pres2 … H))
1290| 20: @(stmt_P_mp … Hstmt_inv3) //
1291| 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
1292   #H @(Htmps_pres3 … H)
1293| 22: whd #l #H normalize in H;
1294      cases (Exists_append … H) #Hcase
1295      [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
1296        [ 1: @(proj1 … Hlabel)
1297        | 2: normalize @Exists_append_l @(proj2 … Hlabel)
1298        ]
1299      | 2: cases (Exists_append … Hcase) #Hcase2
1300        [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
1301          [ 1: @(proj1 … Hlabel)
1302          | 2: normalize >append_nil >append_nil >append_cons
1303               @Exists_append_r @Exists_append_l @Exists_append_r
1304               @(proj2 … Hlabel)
1305          ]
1306        | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
1307          [ 1: @(proj1 … Hlabel)
1308          | 2: normalize >append_nil >append_nil >append_cons
1309             @Exists_append_r @Exists_append_l @Exists_append_l
1310             @(proj2 … Hlabel)
1311          ]
1312        ]
1313      ]
1314| 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
1315| 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1316   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
1317              | 2: #H %1 %2 assumption
1318              | 3: #H %2 assumption ]
1319| 25: whd %1 %1 normalize /2/
1320| 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1321   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
1322                   @Exists_append_r @Exists_append_l @Exists_append_l
1323                   @Exists_append_l assumption
1324              | 2: #H %1 %2 assumption
1325              | 3: #H <H %1 %1 normalize
1326                   @Exists_append_r whd %1 //
1327              | 4: * [ 1: #H <H %1 %1 normalize
1328                       @Exists_append_r @(Exists_add ?? (nil ?))
1329                       @Exists_append_r @Exists_append_r
1330                       whd %1 //
1331                     | 2: * ]
1332              ]
1333| 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
1334   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
1335                   @Exists_append_r @Exists_append_l @Exists_append_l                   
1336                   @Exists_append_r @Exists_append_l assumption
1337              | 2: #H %1 %2 assumption
1338              | 3: #H <H %1 %1 normalize
1339                   @Exists_append_r whd %1 //
1340              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
1341                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
1342                       @Exists_append_r whd %1 //
1343                     | 2: * ]
1344              ]
1345| 28: whd %1 %1 normalize /2/
1346| 29: whd %1 %1 normalize
1347      @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
1348      whd %1 //
1349| 33: whd %1 %2 whd @(ex_intro … l) @E
1350] qed.
1351
1352axiom ParamGlobalMixup : String.
1353
1354(* params and statement aren't real parameters, they're just there for giving the invariant. *)
1355definition alloc_params :
1356 ∀vars:var_types.∀lbls,statement,uv,flag. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag su)
1357   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag su) ≝   
1358λvars,lbls,statement,uv,ul,params,s. foldl ?? (λsu,it.
1359  let 〈id,ty〉 ≝ it in
1360  do «result,Is» ← su;
1361  let 〈fgens1, s〉 as Eresult ≝ result in
1362  do 〈t,ty'〉 as E ← lookup' vars id;
1363  match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul su) with
1364  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
1365  | Stack n ⇒ λE.
1366      do q ← match access_mode ty with
1367      [ By_value q ⇒ OK ? q
1368      | By_reference r ⇒ OK ? (Mpointer r)
1369      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
1370      ];
1371      OK ? «〈fgens1, St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
1372  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
1373  ] E) (OK ? s) params.
1374whd
1375@(match fgens1 return λx.x=fgens1 → ? with
1376  [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1))
1377whd in Is ⊢ %; destruct whd in Is;
1378try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I
1379elim Is * * #Hincl #Hstmt_inv #Hlab_tr #Htmp_pr try assumption
1380@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
1381qed.
1382
1383axiom DuplicateLabel : String.
1384
1385definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
1386λlbls0,lbls,ls.
1387 ∀l,l'. lookup_label lbls l = OK ? l' →
1388 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.
1389
1390lemma lookup_label_add : ∀lbls,l,l'.
1391  lookup_label (add … lbls l l') l = OK ? l'.
1392#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
1393qed.
1394
1395lemma lookup_label_miss : ∀lbls,l,l',l0.
1396  l0 ≠ l →
1397  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
1398#lbls #l #l' #l0 #NE
1399whd in ⊢ (??%%);
1400>lookup_add_miss
1401[ @refl | @NE ]
1402qed.
1403
1404let rec populate_lenv (ls:list ident) (ul:labgen) (lbls:lenv): res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) ≝
1405match ls return λls.res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) with
1406[ nil ⇒ OK ? 〈«lbls, ?», ul〉
1407| cons l t ⇒
1408  match lookup_label lbls l return λlook. lookup_label lbls l = look → ? with
1409  [ OK _    ⇒ λ_.Error ? (msg DuplicateLabel)
1410  | Error _ ⇒ λLOOK.
1411    match generate_fresh_label … ul with
1412    [ mk_Sig ret H ⇒
1413       do 〈packed_lbls, ul1〉 ← populate_lenv t (snd ?? ret) (add … lbls l (fst ?? ret));
1414       match packed_lbls with
1415       [ mk_Sig lbls' Hinv ⇒ OK ? 〈«lbls', ?», ul1〉 ]
1416    ]
1417  ] (refl ? (lookup_label lbls l))
1418].
1419[ 1: whd #l #l' #Hlookup %2 assumption
1420| 2: whd in Hinv; whd #cl_lab #cm_lab #Hlookup
1421     @(eq_identifier_elim … l cl_lab)
1422     [ 1: #Heq %1 >Heq whd %1 //
1423     | 2: #Hneq cases (Hinv cl_lab cm_lab Hlookup)
1424           [ 1: #H %1 %2 @H
1425           | 2: #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H ]
1426     ]
1427]
1428qed.
1429
1430definition build_label_env :
1431   ∀body:statement. res ((Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) × labgen) ≝
1432λbody.
1433  let initial_labgen ≝ mk_labgen (new_universe ?) (nil ?) ?  in
1434  do 〈label_map, u〉 ← populate_lenv (labels_defined body) initial_labgen (empty_map ??);
1435  let lbls ≝ pi1 ?? label_map in
1436  let H    ≝ pi2 ?? label_map in
1437  OK ? 〈«lbls, ?», u〉.
1438[ 1: #l #l' #E cases (H l l' E) //
1439     whd in ⊢ (??%? → ?); #H destruct
1440| 2: whd @I ]
1441qed.
1442
1443lemma local_id_split : ∀vars,tmpgen,i,t.
1444  local_id (add_tmps vars (tmp_env vars tmpgen)) i t →
1445  local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env … tmpgen).
1446#vars #tmpgen #i #t
1447whd in ⊢ (?%?? → ?);
1448elim (tmp_env vars tmpgen)
1449[ #H %1 @H
1450| * #id #ty #tl #IH
1451  cases (identifier_eq ? i id)
1452  [ #E >E #H %2 whd %1 % [ @refl | whd in H; whd in H:(match % with [_⇒?|_⇒?]); >lookup_add_hit in H; #E1 >E1 @refl ]
1453  | #NE #H cases (IH ?)
1454    [ #H' %1 @H'
1455    | #H' %2 %2 @H'
1456    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
1457      >lookup_add_miss in H; [ #H @H | @NE ]
1458    ]
1459  ]
1460] qed.
1461
1462lemma Exists_squeeze : ∀A,P,l1,l2,l3.
1463  Exists A P (l1@l3) → Exists A P (l1@l2@l3).
1464#A #P #l1 #l2 #l3 #EX
1465cases (Exists_append … EX)
1466[ #EX1 @Exists_append_l @EX1
1467| #EX3 @Exists_append_r @Exists_append_r @EX3
1468] qed.
1469
1470(* This lemma allows to merge two stmt_P in one. Used in the following parts to merge an invariant on variables
1471   and an invariant on labels. *)
1472lemma stmt_P_conj : ∀ (P1:stmt → Prop). ∀ (P2:stmt → Prop). ∀ s. stmt_P P1 s → stmt_P P2 s → stmt_P (λs.P1 s ∧ P2 s) s.
1473#P1 #P2 #s elim s
1474normalize try @conj try @conj try /3/
1475[ #z0 #s #Hind1 #Hind2 * * #HA #HB #HC * * #HD #HE #HF try @conj try @conj try @conj try /2/
1476| #H5 #H6 #H7 #H8 #H9 #H10 #H11 * * #H15 #H16 #H17 * * #H20 #H21 #H22
1477  try @conj try @conj try @conj try /2/
1478| 3,4: #H24 #H25 * #H29 #H30 * #H33 #H34 try @conj try @conj try @conj try /2/
1479| 5,6: #H36 #H37 #H38 * #H42 #H43 * #H46 #H47 try @conj try @conj try @conj try /2/ ]
1480qed.
1481
1482definition translate_function :
1483  ∀tmpuniverse:universe SymbolTag.
1484  ∀globals:list (ident×region×type).
1485  ∀f:function.
1486    globals_fresh_for_univ ? globals tmpuniverse →
1487    fn_fresh_for_univ f tmpuniverse →
1488  res internal_function ≝
1489λtmpuniverse, globals, f, Fglobals, Ffn.
1490  do 〈env_pack, ul〉 ← build_label_env (fn_body f);
1491    match env_pack with
1492    [ mk_Sig lbls Ilbls ⇒
1493      let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
1494      let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
1495      do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (fn_body f);
1496      do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (fn_params f) s0;
1497      let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
1498      let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in
1499      do D ← check_distinct_env ?? (params @ vars);
1500      OK ? (mk_internal_function
1501        (opttyp_of_type (fn_return f))
1502        params
1503        vars
1504        D
1505        stacksize
1506        s1 ?)
1507  ].
1508[ 1: #i #t #Hloc whd @Hloc
1509| 2: whd #id #Hpresent normalize in Hpresent:(???%?); whd in Hpresent;
1510      @(characterise_vars_fresh … (sym_eq … E)) //
1511| 3: @(match fgens return λx.x=fgens → ? with
1512     [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens))
1513     whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %;
1514     elim Is * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hlabel_wf
1515     (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
1516     @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf))
1517     #s * #Hstmt_vars #Hstmt_labels @conj
1518     [ 1: (* prove that variables are either parameters or locals *)
1519        @(stmt_vars_mp … Hstmt_vars) #i #t #H
1520        (* Case analysis: (i, t) is either in vartypes, or in (tmp_env vartypes uv) *)
1521        cases (local_id_split … H)
1522        [ 1: #H' >map_append
1523          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))  (* * #id #ty @(〈id, typ_of_type ty〉=〈i, t〉)*)
1524                      | 2: whd @Exists_squeeze @(characterise_vars_all globals f ?? (sym_eq ??? E) i t H')
1525                      | 3: * #id #ty * #E1 #E2 <E1 <E2 @refl
1526                      ]
1527        | 2: #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l
1528          @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t))
1529                      | 2: <Hfgens @EX
1530                      | 3: * #id #ty * #E1 #E2 <E1 <E2 % @refl
1531                      ]
1532        ]
1533     | 2: (* prove that labels are properly declared. *)
1534          @(stmt_labels_mp … Hstmt_labels) #l * *
1535          [ 1: #H assumption
1536          | 2: * #cl_label #Hlookup lapply (Ilbls cl_label l Hlookup) #Hdefined
1537                cases (Hlab_trans … Hdefined) #lx * #LOOKUPx >LOOKUPx in Hlookup; #Ex destruct (Ex)
1538                #H @H
1539          ]
1540    ]
1541] qed.   
1542
1543definition translate_fundef :
1544  ∀tmpuniverse:universe SymbolTag.
1545  ∀globals:list (ident×region×type).
1546    globals_fresh_for_univ ? globals tmpuniverse →
1547  ∀f:clight_fundef.
1548    fd_fresh_for_univ f tmpuniverse →
1549  res (fundef internal_function) ≝
1550λtmpuniverse,globals,Fglobals,f.
1551match f return λf. fd_fresh_for_univ f ? → ? with
1552[ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn')
1553| CL_External fn argtys retty ⇒ λ_. OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
1554].
1555
1556(* TODO: move universe generation to higher level once we do runtime function
1557   generation.  Cheating a bit - we only need the new identifiers to be fresh
1558   for individual functions. *)
1559
1560let rec map_partial_All (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → res B)
1561  (l:list A) (H:All A P l) on l : res (list B) ≝
1562match l return λl. All A P l → ? with
1563[ nil ⇒ λ_. OK (list B) (nil B)
1564| cons hd tl ⇒ λH.
1565    do b_hd ← f hd (proj1 … H);
1566    do b_tl ← map_partial_All A B P f tl (proj2 … H);
1567      OK (list B) (cons B b_hd b_tl)
1568] H.
1569
1570definition clight_to_cminor : clight_program → res Cminor_program ≝
1571λp.
1572  let tmpuniverse ≝ universe_for_program p in
1573  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
1574  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
1575  let globals ≝ fun_globals @ var_globals in
1576  do fns ← map_partial_All ??? (λx,H. do f ← translate_fundef tmpuniverse globals ? (\snd x) H; OK ? 〈\fst x, f〉) (prog_funct ?? p) ?;
1577    OK ? (mk_program ??
1578      (map ?? (λv. 〈\fst v, \fst (\snd v)〉) (prog_vars ?? p))
1579      fns
1580      (prog_main ?? p)).
1581cases (prog_fresh p) * #H1 #H2 #H3
1582[ @(All_mp … H1) #x * //
1583| @All_append
1584  [ elim (prog_funct ?? p) in H1 ⊢ %; // * #id #fd #tl #IH * * #Hhd1 #Hhd2 #Htl % // @IH @Htl
1585  | whd in H3; elim (prog_vars ?? p) in H3 ⊢ %; // #hd #tl #IH * #Hhd #Htl % /2/
1586  ]
1587] qed.
1588
1589(* It'd be nice to go back to some generic thing like
1590
1591 transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
1592
1593   rather than the messier definition above.
1594*)
Note: See TracBrowser for help on using the repository browser.