source: Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma @ 1087

Last change on this file since 1087 was 1087, checked in by campbell, 9 years ago

Experimental branch where lookups of local variables in Cminor code always
succeed.

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