source: src/Clight/toCminor.ma @ 1206

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

First stage of fixing temporary generation in Clight/toCminor.ma.

File size: 27.1 KB
Line 
1
2include "Clight/Csyntax.ma".
3include "Clight/TypeComparison.ma".
4include "utilities/lists.ma".
5
6(* Identify local variables that must be allocated memory. *)
7
8let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝
9match e with
10[ Expr ed ty ⇒
11    match ed with
12    [ Ederef e1 ⇒ gather_mem_vars_expr e1
13    | Eaddrof e1 ⇒ gather_mem_vars_addr e1
14    | Eunop _ e1 ⇒ gather_mem_vars_expr e1
15    | Ebinop _ e1 e2 ⇒ gather_mem_vars_expr e1 ∪
16                       gather_mem_vars_expr e2
17    | Ecast _ e1 ⇒ gather_mem_vars_expr e1
18    | Econdition e1 e2 e3 ⇒ gather_mem_vars_expr e1 ∪
19                            gather_mem_vars_expr e2 ∪
20                            gather_mem_vars_expr e3
21    | Eandbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
22                       gather_mem_vars_expr e2
23    | Eorbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
24                      gather_mem_vars_expr e2
25    | Efield e1 _ ⇒ gather_mem_vars_expr e1
26    | Ecost _ e1 ⇒ gather_mem_vars_expr e1
27    | _ ⇒ ∅
28    ]
29]
30and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝
31match e with
32[ Expr ed ty ⇒
33    match ed with
34    [ Evar x ⇒ { (x) }
35    | Ederef e1 ⇒ gather_mem_vars_expr e1
36    | Efield e1 _ ⇒ gather_mem_vars_addr e1
37    | _ ⇒ ∅ (* not an lvalue *)
38    ]
39].
40
41let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝
42match s with
43[ Sskip ⇒ ∅
44| Sassign e1 e2 ⇒ gather_mem_vars_expr e1 ∪
45                  gather_mem_vars_expr e2
46| Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] ∪
47                    gather_mem_vars_expr e2 ∪
48                    (foldl ?? (λs,e. s ∪ gather_mem_vars_expr e) ∅ es)
49| Ssequence s1 s2 ⇒ gather_mem_vars_stmt s1 ∪
50                    gather_mem_vars_stmt s2
51| Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪
52                         gather_mem_vars_stmt s1 ∪
53                         gather_mem_vars_stmt s2
54| Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
55                 gather_mem_vars_stmt s1
56| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
57                   gather_mem_vars_stmt s1
58| Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪
59                     gather_mem_vars_expr e1 ∪
60                     gather_mem_vars_stmt s2 ∪
61                     gather_mem_vars_stmt s3
62| Sbreak ⇒ ∅
63| Scontinue ⇒ ∅
64| Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ]
65| Sswitch e1 ls ⇒ gather_mem_vars_expr e1 ∪
66                  gather_mem_vars_ls ls
67| Slabel _ s1 ⇒ gather_mem_vars_stmt s1
68| Sgoto _ ⇒ ∅
69| Scost _ s1 ⇒ gather_mem_vars_stmt s1
70]
71and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝
72match ls with
73[ LSdefault s1 ⇒ gather_mem_vars_stmt s1
74| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
75                      gather_mem_vars_ls ls1
76].
77
78inductive var_type : Type[0] ≝
79| Global : region → var_type
80| Stack  : nat → var_type
81| Local  : var_type
82.
83
84definition var_types ≝ identifier_map SymbolTag var_type.
85
86(* Note that the semantics allows locals to shadow globals.
87   Parameters start out as locals, but get stack allocated if their address
88   is taken.  We will add code to store them if that's the case.
89 *)
90
91definition always_alloc : type → bool ≝
92λt. match t with
93[ Tarray _ _ _ ⇒ true
94| Tstruct _ _ ⇒ true
95| Tunion _ _ ⇒ true
96| _ ⇒ false
97].
98
99definition characterise_vars : list (ident×region) → function → var_types × nat ≝
100λglobals, f.
101  let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
102  let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in
103  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
104  let 〈m,stacksize〉 ≝ foldl ?? (λms,v.
105    let 〈m,stack_high〉 ≝ ms in
106    let 〈id,ty〉 ≝ v in
107    let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id
108                           then 〈Stack stack_high,stack_high + sizeof ty〉
109                           else 〈Local, stack_high〉 in
110      〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
111  〈m,stacksize〉.
112
113
114include "Cminor/syntax.ma".
115include "common/Errors.ma".
116
117alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
118
119axiom UndeclaredIdentifier : String.
120axiom BadlyTypedAccess : String.
121axiom BadLvalue : String.
122axiom MissingField : String.
123
124alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
125alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
126
127(* XXX: For some reason matita refuses to pick the right one unless forced. *)
128alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,6,0)".
129
130definition translate_unop : type → CLunop → res CMunop ≝
131λty.λop:CLunop.
132  match op with
133  [ Onotbool ⇒ OK ? CMnotbool
134  | Onotint ⇒ OK ? Onotint
135  | Oneg ⇒
136      match ty with
137      [ Tint _ _ ⇒ OK ? Onegint
138      | Tfloat _ ⇒ OK ? Onegf
139      | _ ⇒ Error ? (msg TypeMismatch)
140      ]
141  ].
142
143definition translate_add ≝
144λty1,e1,ty2,e2,ty'.
145let ty1' ≝ typ_of_type ty1 in
146let ty2' ≝ typ_of_type ty2 in
147match classify_add ty1 ty2 with
148[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
149| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
150(* XXX using the integer size for e2 as the offset's size isn't right, because
151   if e2 produces an 8bit value then the true offset might overflow *)
152| add_case_pi ty ⇒
153    match ty2' with
154    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
155    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
156    ]
157| add_case_ip ty ⇒
158    match ty1' with
159    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
160    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
161    ]
162| add_default ⇒ Error ? (msg TypeMismatch)
163].
164
165definition translate_sub ≝
166λty1,e1,ty2,e2,ty'.
167let ty1' ≝ typ_of_type ty1 in
168let ty2' ≝ typ_of_type ty2 in
169match classify_sub ty1 ty2 with
170[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
171| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
172(* XXX choosing offset sizes? *)
173| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
174| sub_case_pp ty ⇒
175    match ty' with (* XXX overflow *)
176    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
177    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
178    ]
179| sub_default ⇒ Error ? (msg TypeMismatch)
180].
181
182definition translate_mul ≝
183λty1,e1,ty2,e2,ty'.
184let ty1' ≝ typ_of_type ty1 in
185let ty2' ≝ typ_of_type ty2 in
186match classify_mul ty1 ty2 with
187[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
188| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
189| mul_default ⇒ Error ? (msg TypeMismatch)
190].
191
192definition translate_div ≝
193λty1,e1,ty2,e2,ty'.
194let ty1' ≝ typ_of_type ty1 in
195let ty2' ≝ typ_of_type ty2 in
196match classify_div ty1 ty2 with
197[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
198| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
199| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
200| div_default ⇒ Error ? (msg TypeMismatch)
201].
202
203definition translate_mod ≝
204λty1,e1,ty2,e2,ty'.
205let ty1' ≝ typ_of_type ty1 in
206let ty2' ≝ typ_of_type ty2 in
207match classify_mod ty1 ty2 with
208[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
209| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
210| mod_default ⇒ Error ? (msg TypeMismatch)
211].
212
213definition translate_shr ≝
214λty1,e1,ty2,e2,ty'.
215let ty1' ≝ typ_of_type ty1 in
216let ty2' ≝ typ_of_type ty2 in
217match classify_shr ty1 ty2 with
218[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
219| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
220| shr_default ⇒ Error ? (msg TypeMismatch)
221].
222
223definition translate_cmp ≝
224λc,ty1,e1,ty2,e2,ty'.
225let ty1' ≝ typ_of_type ty1 in
226let ty2' ≝ typ_of_type ty2 in
227match classify_cmp ty1 ty2 with
228[ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
229| cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
230| cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
231| cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
232| cmp_default ⇒ Error ? (msg TypeMismatch)
233].
234
235definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
236λop,ty1,e1,ty2,e2,ty.
237let ty' ≝ typ_of_type ty in
238match op with
239[ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
240| Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
241| Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
242| Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
243| Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
244| Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
245| Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
246| Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
247| Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
248| Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
249| Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
250| One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
251| Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
252| Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
253| Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
254| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
255].
256
257
258(* We'll need to implement proper translation of pointers if we really do memory
259   spaces. *)
260definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
261λr1,r2,P.
262  match r1 return λx.P x → res (P r2) with
263  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
264  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
265  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
266  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
267  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
268  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
269  ].
270
271definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝
272λr1,r2,e. check_region r1 r2 ? e.
273
274definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝
275λty1,ty2.
276match ty1 return λx.CMexpr (typ_of_type x) → ? with
277[ Tint sz1 sg1 ⇒ λe.
278    match ty2 return λx.res (CMexpr (typ_of_type x)) with
279    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e)
280    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
281    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
282    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
283    | _ ⇒ Error ? (msg TypeMismatch)
284    ]
285| Tfloat sz1 ⇒ λe.
286    match ty2 return λx.res (CMexpr (typ_of_type x)) with
287    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e)
288    | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
289    | _ ⇒ Error ? (msg TypeMismatch)
290    ]
291| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
292    match ty2 return λx.res (CMexpr (typ_of_type x)) with
293    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)
294    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
295    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
296    | _ ⇒ Error ? (msg TypeMismatch)
297    ]
298| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
299    match ty2 return λx.res (CMexpr (typ_of_type x)) with
300    [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)
301    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
302    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
303    | _ ⇒ Error ? (msg TypeMismatch)
304    ]
305| _ ⇒ λ_. Error ? (msg TypeMismatch)
306].
307
308definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
309λty1,ty2,P,p.
310  do E ← assert_type_eq ty1 ty2;
311  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
312
313definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
314* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
315qed.
316
317definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
318* [ #sz1 #sg1 | #r1 | #sz1 ]
319* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
320[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
321  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
322| *; #P #p @(region_should_eq r1 ?? p)
323| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
324] qed.
325
326
327lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
328*
329[ 5: #r #ty #n #r' normalize #E destruct @refl
330| 6: #args #ret #r normalize #E destruct @refl
331| *: normalize #a #b try #c try #d destruct
332  [ cases a in d; normalize; cases b; normalize #E destruct
333  | cases a in c; normalize #E destruct
334  ]
335] qed.
336
337let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝
338match e return λe. res (CMexpr (typ_of_type (typeof e))) with
339[ Expr ed ty ⇒
340  match ed with
341  [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))
342  | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
343  | Evar id ⇒
344      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
345      match c with
346      [ Global r ⇒
347          match access_mode ty with
348          [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))
349          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))
350          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
351          ]
352      | Stack n ⇒
353          match access_mode ty with
354          [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))
355          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))
356          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
357          ]
358      | Local ⇒ OK ? (Id ? id)
359      ]
360  | Ederef e1 ⇒
361      do e1' ← translate_expr vars e1;
362      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
363      [ ASTptr r ⇒ λe1'.
364          match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
365          [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
366          | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
367          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
368          ] (refl ? (access_mode ty))
369      | _ ⇒ λ_. Error ? (msg TypeMismatch)
370      ] e1'
371  | Eaddrof e1 ⇒
372      do e1' ← translate_addr vars e1;
373      match typ_of_type ty return λx.res (CMexpr x) with
374      [ ASTptr r ⇒
375          match e1' with
376          [ dp r1 e1' ⇒ region_should_eq r1 r ? e1'
377          ]
378      | _ ⇒ Error ? (msg TypeMismatch)
379      ]
380  | Eunop op e1 ⇒
381      do op' ← translate_unop ty op;
382      do e1' ← translate_expr vars e1;
383      OK ? (Op1 ?? op' e1')
384  | Ebinop op e1 e2 ⇒
385      do e1' ← translate_expr vars e1;
386      do e2' ← translate_expr vars e2;
387      translate_binop op (typeof e1) e1' (typeof e2) e2' ty
388  | Ecast ty1 e1 ⇒
389      do e1' ← translate_expr vars e1;
390      do e' ← translate_cast (typeof e1) ty1 e1';
391      typ_should_eq ? (typ_of_type ty) ? e'
392  | Econdition e1 e2 e3 ⇒
393      do e1' ← translate_expr vars e1;
394      do e2' ← translate_expr vars e2;
395      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
396      do e3' ← translate_expr vars e3;
397      do e3' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e3';
398      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
399      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')
400      | _ ⇒ λ_.Error ? (msg TypeMismatch)
401      ] e1'
402  | Eandbool e1 e2 ⇒
403      do e1' ← translate_expr vars e1;
404      do e2' ← translate_expr vars e2;
405      match ty with
406      [ Tint sz _ ⇒
407        do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
408        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
409        [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))
410        | _ ⇒ λ_.Error ? (msg TypeMismatch)
411        ] e1'
412      | _ ⇒ Error ? (msg TypeMismatch)
413      ]
414  | Eorbool e1 e2 ⇒
415      do e1' ← translate_expr vars e1;
416      do e2' ← translate_expr vars e2;
417      match ty with
418      [ Tint sz _ ⇒
419        do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
420        match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
421        [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')
422        | _ ⇒ λ_.Error ? (msg TypeMismatch)
423        ] e1'
424      | _ ⇒ Error ? (msg TypeMismatch)
425      ]
426  | Esizeof ty1 ⇒
427      match ty with
428      [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))
429      | _ ⇒ Error ? (msg TypeMismatch)
430      ]
431  | Efield e1 id ⇒
432      do e' ← match typeof e1 with
433      [ Tstruct _ fl ⇒
434          do e1' ← translate_addr vars e1;
435          match e1' with
436          [ dp r e1' ⇒
437            do off ← field_offset id fl;
438            match access_mode ty with
439            [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
440            | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))
441            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
442            ]
443          ]
444      | Tunion _ _ ⇒
445          do e1' ← translate_addr vars e1;
446          match e1' with
447          [ dp r e1' ⇒
448            match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with
449            [ By_value q ⇒ λ_. OK ? (Mem ?? q e1')
450            | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉
451            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
452            ] (refl ? (access_mode ty))
453          ]
454      | _ ⇒ Error ? (msg BadlyTypedAccess)
455      ];
456      typ_should_eq ? (typ_of_type ty) ? e'
457  | Ecost l e1 ⇒
458      do e1' ← translate_expr vars e1;
459      do e' ← OK ? (Ecost ? l e1');
460      typ_should_eq ? (typ_of_type ty) ? e'
461  ]
462] and translate_addr (vars:var_types) (e:expr) on e : res (Σr.CMexpr (ASTptr r)) ≝
463match e with
464[ Expr ed _ ⇒
465  match ed with
466  [ Evar id ⇒
467      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
468      match c return λ_. res (Σr.CMexpr (ASTptr r)) with
469      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
470      | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))
471      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
472      ]
473  | Ederef e1 ⇒
474      do e1' ← translate_expr vars e1;
475      match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with
476      [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')
477      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
478      ] e1'
479  | Efield e1 id ⇒
480      match typeof e1 with
481      [ Tstruct _ fl ⇒
482          do e1' ← translate_addr vars e1;
483          do off ← field_offset id fl;
484          match e1' with
485          [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
486          ]
487      | Tunion _ _ ⇒ translate_addr vars e1
488      | _ ⇒ Error ? (msg BadlyTypedAccess)
489      ]
490  | _ ⇒ Error ? (msg BadLvalue)
491  ]
492].
493>(access_mode_typ … E) @refl
494qed.
495
496inductive destination : Type[0] ≝
497| IdDest : ident → destination
498| MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination.
499
500definition translate_dest ≝
501λvars,e1,ty2.
502    do q ← match access_mode ty2 with
503           [ By_value q ⇒ OK ? q
504           | By_reference r ⇒ OK ? (Mpointer r)
505           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
506           ];
507    match e1 with
508    [ Expr ed1 ty1 ⇒
509        match ed1 with
510        [ Evar id ⇒
511            do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
512            match c with
513            [ Local ⇒ OK ? (IdDest id)
514            | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0)))
515            | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n)))
516            ]
517        | _ ⇒
518            do e1' ← translate_addr vars e1;
519            match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]
520        ]
521    ].
522
523definition translate_assign ≝
524λvars,e1,e2.
525do e2' ← translate_expr vars e2;
526do dest ← translate_dest vars e1 (typeof e2);
527match dest with
528[ IdDest id ⇒ OK ? (St_assign ? id e2')
529| MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2')
530].
531
532definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
533λA,B,f,oa.
534match oa with
535[ None ⇒ OK ? (None ?)
536| Some a ⇒ do b ← f a; OK ? (Some ? b)
537].
538
539definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝
540λv,e.
541  do e' ← translate_expr v e;
542  OK ? (dp ? (λt:typ.CMexpr t) ? e').
543
544axiom FIXME : String.
545
546record tmpgen : Type[0] ≝ {
547  tmp_universe : universe SymbolTag;
548  tmp_env : list (ident × typ)
549}.
550
551definition alloc_tmp : memory_chunk → tmpgen → ident × tmpgen ≝
552λc,g.
553  let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in
554  〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉.
555
556let rec translate_statement (vars:var_types) (u:tmpgen) (s:statement) on s : res (stmt×tmpgen) ≝
557match s with
558[ Sskip ⇒ OK ? 〈St_skip, u〉
559| Sassign e1 e2 ⇒ do s' ← translate_assign vars e1 e2; OK ? 〈s',u〉
560| Scall ret ef args ⇒
561    do ef' ← translate_expr vars ef;
562    do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
563    do args' ← mmap … (translate_expr_sigma vars) args;
564    match ret with
565    [ None ⇒ OK ? 〈St_call (None ?) ef' args', u〉
566    | Some e1 ⇒
567        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
568        match dest with
569        [ IdDest id ⇒ OK ? 〈St_call (Some ? id) ef' args', u〉
570        | MemDest r q e1' ⇒
571            let 〈tmp, u〉 ≝ alloc_tmp q u in
572            OK ? 〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉
573        ]
574    ]
575| Ssequence s1 s2 ⇒
576    do 〈s1', u〉 ← translate_statement vars u s1;
577    do 〈s2', u〉 ← translate_statement vars u s2;
578    OK ? 〈St_seq s1' s2', u〉
579| Sifthenelse e1 s1 s2 ⇒
580    do e1' ← translate_expr vars e1;
581    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
582    [ ASTint _ _ ⇒ λe1'.
583        do 〈s1', u〉 ← translate_statement vars u s1;
584        do 〈s2', u〉 ← translate_statement vars u s2;
585        OK ? 〈St_ifthenelse ?? e1' s1' s2', u〉
586    | _ ⇒ λ_.Error ? (msg TypeMismatch)
587    ] e1'
588| Swhile e1 s1 ⇒
589    do e1' ← translate_expr vars e1;
590    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
591    [ ASTint _ _ ⇒ λe1'.
592        do 〈s1', u〉 ← translate_statement vars u s1;
593        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
594        OK ? 〈St_block
595               (St_loop
596                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉
597    | _ ⇒ λ_.Error ? (msg TypeMismatch)
598    ] e1'
599| Sdowhile e1 s1 ⇒
600    do e1' ← translate_expr vars e1;
601    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
602    [ ASTint _ _ ⇒ λe1'.
603        do 〈s1',u〉 ← translate_statement vars u s1;
604        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
605        OK ? 〈St_block
606               (St_loop
607                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉
608    | _ ⇒ λ_.Error ? (msg TypeMismatch)
609    ] e1'
610| Sfor s1 e1 s2 s3 ⇒
611    do e1' ← translate_expr vars e1;
612    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
613    [ ASTint _ _ ⇒ λe1'.
614        do 〈s1', u〉 ← translate_statement vars u s1;
615        do 〈s2', u〉 ← translate_statement vars u s2;
616        do 〈s3', u〉 ← translate_statement vars u s3;
617        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
618        OK ? 〈St_seq s1'
619             (St_block
620               (St_loop
621                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉
622    | _ ⇒ λ_.Error ? (msg TypeMismatch)
623    ] e1'
624| Sbreak ⇒ OK ? 〈St_exit 1, u〉
625| Scontinue ⇒ OK ? 〈St_exit 0, u〉
626| Sreturn ret ⇒
627    match ret with
628    [ None ⇒ OK ? 〈St_return (None ?), u〉
629    | Some e1 ⇒
630        do e1' ← translate_expr vars e1;
631        OK ? 〈St_return (Some ? (dp … e1')), u〉
632    ]
633| Sswitch e1 ls ⇒ Error ? (msg FIXME)
634| Slabel l s1 ⇒
635    do 〈s1', u〉 ← translate_statement vars u s1;
636    OK ? 〈St_label l s1', u〉
637| Sgoto l ⇒ OK ? 〈St_goto l, u〉
638| Scost l s1 ⇒
639    do 〈s1', u〉 ← translate_statement vars u s1;
640    OK ? 〈St_cost l s1', u〉
641].
642
643axiom ParamGlobalMixup : String.
644
645definition alloc_params : var_types → list (ident×type) → stmt → res stmt ≝
646λvars,params,s. foldl ?? (λs,it.
647  let 〈id,ty〉 ≝ it in
648  do s ← s;
649  do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
650  match t with
651  [ Local ⇒ OK ? s
652  | Stack n ⇒
653      do q ← match access_mode ty with
654      [ By_value q ⇒ OK ? q
655      | By_reference r ⇒ OK ? (Mpointer r)
656      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
657      ];
658      OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s)
659  | Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id]
660  ]) (OK ? s) params.
661
662definition bigu ≝ mk_universe SymbolTag [[
663false;true;false;false;
664false;false;false;false;
665false;false;false;false;
666false;false;false;false]] false.
667
668(* FIXME: the temporary handling is a bit dodgy, I'm afraid. *)
669definition translate_function : list (ident×region) → function → res internal_function ≝
670λglobals, f.
671  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
672  let tmp ≝ mk_tmpgen bigu [ ] in (* FIXME *)
673  do 〈s,tmp〉 ← translate_statement vartypes tmp (fn_body f);
674  do s ← alloc_params vartypes (fn_params f) s;
675  OK ? (mk_internal_function
676    (opttyp_of_type (fn_return f))
677    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
678    ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
679    stacksize
680    s).
681
682definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
683λglobals,f.
684match f with
685[ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
686| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
687].
688
689definition clight_to_cminor : clight_program → res Cminor_program ≝
690λp.
691  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
692  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
693  let globals ≝ fun_globals @ var_globals in
694  transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.
Note: See TracBrowser for help on using the repository browser.