source: src/Clight/toCminor.ma @ 1194

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

Remove old, commented out code.

File size: 26.8 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
546let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝
547match s with
548[ Sskip ⇒ OK ? St_skip
549| Sassign e1 e2 ⇒ translate_assign vars e1 e2
550| Scall ret ef args ⇒
551    do ef' ← translate_expr vars ef;
552    do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
553    do args' ← mmap … (translate_expr_sigma vars) args;
554    match ret with
555    [ None ⇒ OK ? (St_call (None ?) ef' args')
556    | Some e1 ⇒
557        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
558        match dest with
559        [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')
560        | MemDest r q e1' ⇒
561            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
562            OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))
563        ]
564    ]
565| Ssequence s1 s2 ⇒
566    do s1' ← translate_statement vars tmp tmpp s1;
567    do s2' ← translate_statement vars tmp tmpp s2;
568    OK ? (St_seq s1' s2')
569| Sifthenelse e1 s1 s2 ⇒
570    do e1' ← translate_expr vars e1;
571    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
572    [ ASTint _ _ ⇒ λe1'.
573        do s1' ← translate_statement vars tmp tmpp s1;
574        do s2' ← translate_statement vars tmp tmpp s2;
575        OK ? (St_ifthenelse ?? e1' s1' s2')
576    | _ ⇒ λ_.Error ? (msg TypeMismatch)
577    ] e1'
578| Swhile e1 s1 ⇒
579    do e1' ← translate_expr vars e1;
580    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
581    [ ASTint _ _ ⇒ λe1'.
582        do s1' ← translate_statement vars tmp tmpp s1;
583        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
584        OK ? (St_block
585               (St_loop
586                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))))
587    | _ ⇒ λ_.Error ? (msg TypeMismatch)
588    ] e1'
589| Sdowhile e1 s1 ⇒
590    do e1' ← translate_expr vars e1;
591    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
592    [ ASTint _ _ ⇒ λe1'.
593        do s1' ← translate_statement vars tmp tmpp s1;
594        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
595        OK ? (St_block
596               (St_loop
597                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))))
598    | _ ⇒ λ_.Error ? (msg TypeMismatch)
599    ] e1'
600| Sfor s1 e1 s2 s3 ⇒
601    do e1' ← translate_expr vars e1;
602    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
603    [ ASTint _ _ ⇒ λe1'.
604        do s1' ← translate_statement vars tmp tmpp s1;
605        do s2' ← translate_statement vars tmp tmpp s2;
606        do s3' ← translate_statement vars tmp tmpp s3;
607        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
608        OK ? (St_seq s1'
609             (St_block
610               (St_loop
611                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))))
612    | _ ⇒ λ_.Error ? (msg TypeMismatch)
613    ] e1'
614| Sbreak ⇒ OK ? (St_exit 1)
615| Scontinue ⇒ OK ? (St_exit 0)
616| Sreturn ret ⇒
617    match ret with
618    [ None ⇒ OK ? (St_return (None ?))
619    | Some e1 ⇒
620        do e1' ← translate_expr vars e1;
621        OK ? (St_return (Some ? (dp … e1')))
622    ]
623| Sswitch e1 ls ⇒ Error ? (msg FIXME)
624| Slabel l s1 ⇒
625    do s1' ← translate_statement vars tmp tmpp s1;
626    OK ? (St_label l s1')
627| Sgoto l ⇒ OK ? (St_goto l)
628| Scost l s1 ⇒
629    do s1' ← translate_statement vars tmp tmpp s1;
630    OK ? (St_cost l s1')
631].
632
633axiom ParamGlobalMixup : String.
634
635definition alloc_params : var_types → list (ident×type) → stmt → res stmt ≝
636λvars,params,s. foldl ?? (λs,it.
637  let 〈id,ty〉 ≝ it in
638  do s ← s;
639  do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
640  match t with
641  [ Local ⇒ OK ? s
642  | Stack n ⇒
643      do q ← match access_mode ty with
644      [ By_value q ⇒ OK ? q
645      | By_reference r ⇒ OK ? (Mpointer r)
646      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
647      ];
648      OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s)
649  | Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id]
650  ]) (OK ? s) params.
651
652definition bigid1 ≝ an_identifier SymbolTag [[
653false;true;false;false;
654false;false;false;false;
655false;false;false;false;
656false;false;false;false]].
657definition bigid2 ≝ an_identifier SymbolTag [[
658false;true;false;false;
659false;false;false;false;
660false;false;false;false;
661false;false;false;true]].
662
663(* FIXME: the temporary handling is nonsense, I'm afraid. *)
664definition translate_function : list (ident×region) → function → res internal_function ≝
665λglobals, f.
666  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
667  let tmp ≝ bigid1 in (* FIXME *)
668  let tmpp ≝ bigid2 in (* FIXME *)
669  do s ← translate_statement vartypes tmp tmpp (fn_body f);
670  do s ← alloc_params vartypes (fn_params f) s;
671  OK ? (mk_internal_function
672    (opttyp_of_type (fn_return f))
673    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
674    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
675    stacksize
676    s).
677
678definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
679λglobals,f.
680match f with
681[ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
682| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
683].
684
685definition clight_to_cminor : clight_program → res Cminor_program ≝
686λp.
687  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
688  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
689  let globals ≝ fun_globals @ var_globals in
690  transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.
Note: See TracBrowser for help on using the repository browser.