source: src/Clight/toCminor.ma @ 2588

Last change on this file since 2588 was 2588, checked in by garnier, 7 years ago

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

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