source: src/Clight/toCminor.ma @ 886

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

Put types into parameter and variable lists in Cminor.
Temporarily breaks translation to RTLabs.

File size: 29.0 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
155(* Note that the semantics allows locals to shadow globals.
156   Parameters start out as locals, but get stack allocated if their address
157   is taken.  We will add code to store them if that's the case.
158 *)
159
160definition always_alloc : type → bool ≝
161λt. match t with
162[ Tarray _ _ _ ⇒ true
163| Tstruct _ _ ⇒ true
164| Tunion _ _ ⇒ true
165| _ ⇒ false
166].
167
168definition characterise_vars : list (ident×region) → function → var_types × nat ≝
169λglobals, f.
170  let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
171  let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in
172  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
173  let 〈m,stacksize〉 ≝ foldl ?? (λms,v.
174    let 〈m,stack_high〉 ≝ ms in
175    let 〈id,ty〉 ≝ v in
176    let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id
177                           then 〈Stack stack_high,stack_high + sizeof ty〉
178                           else 〈Local, stack_high〉 in
179      〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_vars f) in
180  〈m,stacksize〉.
181
182
183include "Cminor/syntax.ma".
184include "common/Errors.ma".
185
186alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
187
188axiom UndeclaredIdentifier : String.
189axiom BadlyTypedAccess : String.
190axiom BadLvalue : String.
191axiom MissingField : String.
192
193alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
194alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
195
196(* XXX: For some reason matita refuses to pick the right one unless forced. *)
197alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,6,0)".
198
199definition translate_unop : type → CLunop → res CMunop ≝
200λty.λop:CLunop.
201  match op with
202  [ Onotbool ⇒ OK ? CMnotbool
203  | Onotint ⇒ OK ? Onotint
204  | Oneg ⇒
205      match ty with
206      [ Tint _ _ ⇒ OK ? Onegint
207      | Tfloat _ ⇒ OK ? Onegf
208      | _ ⇒ Error ? (msg TypeMismatch)
209      ]
210  ].
211
212definition translate_add ≝
213λty1,e1,ty2,e2,ty'.
214let ty1' ≝ typ_of_type ty1 in
215let ty2' ≝ typ_of_type ty2 in
216match classify_add ty1 ty2 with
217[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
218| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
219| add_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
220| add_case_ip ty ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst (repr (sizeof ty))))))
221| add_default ⇒ Error ? (msg TypeMismatch)
222].
223
224definition translate_sub ≝
225λty1,e1,ty2,e2,ty'.
226let ty1' ≝ typ_of_type ty1 in
227let ty2' ≝ typ_of_type ty2 in
228match classify_sub ty1 ty2 with
229[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
230| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
231| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst (repr (sizeof ty))))))
232| sub_case_pp ty ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' Osubpp e1 e2) (Cst ? (Ointconst (repr (sizeof ty)))))
233| sub_default ⇒ Error ? (msg TypeMismatch)
234].
235
236definition translate_mul ≝
237λty1,e1,ty2,e2,ty'.
238let ty1' ≝ typ_of_type ty1 in
239let ty2' ≝ typ_of_type ty2 in
240match classify_mul ty1 ty2 with
241[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
242| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
243| mul_default ⇒ Error ? (msg TypeMismatch)
244].
245
246definition translate_div ≝
247λty1,e1,ty2,e2,ty'.
248let ty1' ≝ typ_of_type ty1 in
249let ty2' ≝ typ_of_type ty2 in
250match classify_div ty1 ty2 with
251[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) (* FIXME: should be 8 bit only *)
252| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
253| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
254| div_default ⇒ Error ? (msg TypeMismatch)
255].
256
257definition translate_mod ≝
258λty1,e1,ty2,e2,ty'.
259let ty1' ≝ typ_of_type ty1 in
260let ty2' ≝ typ_of_type ty2 in
261match classify_mod ty1 ty2 with
262[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) (* FIXME: should be 8 bit only *)
263| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
264| mod_default ⇒ Error ? (msg TypeMismatch)
265].
266
267definition translate_shr ≝
268λty1,e1,ty2,e2,ty'.
269let ty1' ≝ typ_of_type ty1 in
270let ty2' ≝ typ_of_type ty2 in
271match classify_shr ty1 ty2 with
272[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) (* FIXME: should be 8 bit only *)
273| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
274| shr_default ⇒ Error ? (msg TypeMismatch)
275].
276
277definition translate_cmp ≝
278λc,ty1,e1,ty2,e2,ty'.
279let ty1' ≝ typ_of_type ty1 in
280let ty2' ≝ typ_of_type ty2 in
281match classify_cmp ty1 ty2 with
282[ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
283| cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
284| cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
285| cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
286| cmp_default ⇒ Error ? (msg TypeMismatch)
287].
288
289definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
290λop,ty1,e1,ty2,e2,ty.
291let ty' ≝ typ_of_type ty in
292match op with
293[ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
294| Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
295| Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
296| Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
297| Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
298| Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
299| Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
300| Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
301| Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
302| Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
303| Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
304| One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
305| Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
306| Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
307| Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
308| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
309].
310
311
312(* We'll need to implement proper translation of pointers if we really do memory
313   spaces. *)
314definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
315λr1,r2,P.
316  match r1 return λx.P x → res (P r2) with
317  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
318  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
319  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
320  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
321  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
322  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
323  ].
324
325definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝
326λr1,r2,e. check_region r1 r2 ? e.
327
328definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝
329λty1,ty2.
330match ty1 return λx.CMexpr (typ_of_type x) → ? with
331[ Tint sz1 sg1 ⇒ λe.
332    match ty2 return λx.res (CMexpr (typ_of_type x)) with
333    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME: do we need to do zero/sign ext?  Ought to be 8 bit anyway... *)
334    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
335    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
336    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
337    | _ ⇒ Error ? (msg TypeMismatch)
338    ]
339| Tfloat sz1 ⇒ λe.
340    match ty2 return λx.res (CMexpr (typ_of_type x)) with
341    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat | _ ⇒ Ointoffloat]) e)
342    | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
343    | _ ⇒ Error ? (msg TypeMismatch)
344    ]
345| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
346    match ty2 return λx.res (CMexpr (typ_of_type x)) with
347    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? Ointofptr e)
348    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
349    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
350    | _ ⇒ Error ? (msg TypeMismatch)
351    ]
352| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
353    match ty2 return λx.res (CMexpr (typ_of_type x)) with
354    [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) Ointofptr e)
355    | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
356    | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
357    | _ ⇒ Error ? (msg TypeMismatch)
358    ]
359| _ ⇒ λ_. Error ? (msg TypeMismatch)
360].
361
362definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
363λty1,ty2,P,p.
364  do E ← assert_type_eq ty1 ty2;
365  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
366
367definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
368* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
369qed.
370
371definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
372* [ #sz1 #sg1 | #r1 | #sz1 ]
373* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
374[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
375  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
376| *; #P #p @(region_should_eq r1 ?? p)
377| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
378] qed.
379
380
381lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
382*
383[ 5: #r #ty #n #r' normalize #E destruct @refl
384| 6: #args #ret #r normalize #E destruct @refl
385| *: normalize #a #b try #c try #d destruct
386  [ cases a in d; normalize; cases b; normalize #E destruct
387  | cases a in c; normalize #E destruct
388  ]
389] qed.
390
391let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝
392match e return λe. res (CMexpr (typ_of_type (typeof e))) with
393[ Expr ed ty ⇒
394  match ed with
395  [ Econst_int i ⇒ OK ? (Cst ? (Ointconst i))
396  | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
397  | Evar id ⇒
398      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
399      match c with
400      [ Global r ⇒
401          match access_mode ty with
402          [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id zero)))
403          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
404          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
405          ]
406      | Stack n ⇒
407          match access_mode ty with
408          [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack (repr n))))
409          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
410          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
411          ]
412      | Local ⇒ OK ? (Id ? id)
413      ]
414  | Ederef e1 ⇒
415      do e1' ← translate_expr vars e1;
416      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
417      [ ASTptr r ⇒ λe1'.
418          match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
419          [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
420          | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
421          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
422          ] (refl ? (access_mode ty))
423      | _ ⇒ λ_. Error ? (msg TypeMismatch)
424      ] e1'
425  | Eaddrof e1 ⇒
426      do e1' ← translate_addr vars e1;
427      match typ_of_type ty return λx.res (CMexpr x) with
428      [ ASTptr r ⇒
429          match e1' with
430          [ dp r1 e1' ⇒ region_should_eq r1 r ? e1'
431          ]
432      | _ ⇒ Error ? (msg TypeMismatch)
433      ]
434  | Eunop op e1 ⇒
435      do op' ← translate_unop ty op;
436      do e1' ← translate_expr vars e1;
437      OK ? (Op1 ?? op' e1')
438  | Ebinop op e1 e2 ⇒
439      do e1' ← translate_expr vars e1;
440      do e2' ← translate_expr vars e2;
441      translate_binop op (typeof e1) e1' (typeof e2) e2' ty
442  | Ecast ty1 e1 ⇒
443      do e1' ← translate_expr vars e1;
444      do e' ← translate_cast (typeof e1) ty1 e1';
445      typ_should_eq ? (typ_of_type ty) ? e'
446  | Econdition e1 e2 e3 ⇒
447      do e1' ← translate_expr vars e1;
448      do e2' ← translate_expr vars e2;
449      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
450      do e3' ← translate_expr vars e3;
451      do e3' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e3';
452      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
453      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')
454      | _ ⇒ λ_.Error ? (msg TypeMismatch)
455      ] e1'
456  | Eandbool e1 e2 ⇒
457      do e1' ← translate_expr vars e1;
458      do e2' ← translate_expr vars e2;
459      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
460      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
461      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst zero)))
462      | _ ⇒ λ_.Error ? (msg TypeMismatch)
463      ] e1'
464  | Eorbool e1 e2 ⇒
465      do e1' ← translate_expr vars e1;
466      do e2' ← translate_expr vars e2;
467      do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
468      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
469      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst one)) e2')
470      | _ ⇒ λ_.Error ? (msg TypeMismatch)
471      ] e1'
472  | Esizeof ty1 ⇒ OK ? (Cst ? (Ointconst (repr (sizeof ty1))))
473  | Efield e1 id ⇒
474      do e' ← match typeof e1 with
475      [ Tstruct _ fl ⇒
476          do e1' ← translate_addr vars e1;
477          match e1' with
478          [ dp r e1' ⇒
479            do off ← field_offset id fl;
480            match access_mode ty with
481            [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off)))))
482            | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off))))
483            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
484            ]
485          ]
486      | Tunion _ _ ⇒
487          do e1' ← translate_addr vars e1;
488          match e1' with
489          [ dp r e1' ⇒
490            match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with
491            [ By_value q ⇒ λ_. OK ? (Mem ?? q e1')
492            | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉
493            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
494            ] (refl ? (access_mode ty))
495          ]
496      | _ ⇒ Error ? (msg BadlyTypedAccess)
497      ];
498      typ_should_eq ? (typ_of_type ty) ? e'
499  | Ecost l e1 ⇒
500      do e1' ← translate_expr vars e1;
501      do e' ← OK ? (Ecost ? l e1');
502      typ_should_eq ? (typ_of_type ty) ? e'
503  ]
504] and translate_addr (vars:var_types) (e:expr) on e : res (Σr.CMexpr (ASTptr r)) ≝
505match e with
506[ Expr ed _ ⇒
507  match ed with
508  [ Evar id ⇒
509      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
510      match c return λ_. res (Σr.CMexpr (ASTptr r)) with
511      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id zero)))
512      | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack (repr n))))
513      | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
514      ]
515  | Ederef e1 ⇒
516      do e1' ← translate_expr vars e1;
517      match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with
518      [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')
519      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
520      ] e1'
521  | Efield e1 id ⇒
522      match typeof e1 with
523      [ Tstruct _ fl ⇒
524          do e1' ← translate_addr vars e1;
525          do off ← field_offset id fl;
526          match e1' with
527          [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst (repr off)))))
528          ]
529      | Tunion _ _ ⇒ translate_addr vars e1
530      | _ ⇒ Error ? (msg BadlyTypedAccess)
531      ]
532  | _ ⇒ Error ? (msg BadLvalue)
533  ]
534].
535>(access_mode_typ … E) @refl
536qed.
537
538inductive destination : Type[0] ≝
539| IdDest : ident → destination
540| MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination.
541
542definition translate_dest ≝
543λvars,e1,ty2.
544    do q ← match access_mode ty2 with
545           [ By_value q ⇒ OK ? q
546           | By_reference r ⇒ OK ? (Mpointer r)
547           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
548           ];
549    match e1 with
550    [ Expr ed1 ty1 ⇒
551        match ed1 with
552        [ Evar id ⇒
553            do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
554            match c with
555            [ Local ⇒ OK ? (IdDest id)
556            | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id zero)))
557            | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack (repr n))))
558            ]
559        | _ ⇒
560            do e1' ← translate_addr vars e1;
561            match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]
562        ]
563    ].
564(*
565definition translate_assign ≝
566λvars,e1,e2.
567    do e2' ← translate_expr vars e2;
568    do q ← match access_mode (typeof e2) with
569           [ By_value q ⇒ OK ? q
570           | By_reference r ⇒ OK ? (Mpointer r)
571           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
572           ];
573    match e1 with
574    [ Expr ed1 ty1 ⇒
575        match ed1 with
576        [ Evar id ⇒
577            do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
578            match c with
579            [ Local ⇒ OK ? (St_assign id e2')
580            | Global ⇒ OK ? (St_store q (Cst (Oaddrsymbol id zero)) e2')
581            | Stack n ⇒ OK ? (St_store q (Cst (Oaddrstack (repr n))) e2')
582            ]
583        | _ ⇒
584            do e1' ← translate_addr vars e1;
585            OK ? (St_store q e1' e2')
586        ]
587    ].
588*)
589definition translate_assign ≝
590λvars,e1,e2.
591do e2' ← translate_expr vars e2;
592do dest ← translate_dest vars e1 (typeof e2);
593match dest with
594[ IdDest id ⇒ OK ? (St_assign ? id e2')
595| MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2')
596].
597
598definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
599λA,B,f,oa.
600match oa with
601[ None ⇒ OK ? (None ?)
602| Some a ⇒ do b ← f a; OK ? (Some ? b)
603].
604
605definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝
606λv,e.
607  do e' ← translate_expr v e;
608  OK ? (dp ? (λt:typ.CMexpr t) ? e').
609
610axiom FIXME : String.
611
612let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝
613match s with
614[ Sskip ⇒ OK ? St_skip
615| Sassign e1 e2 ⇒ translate_assign vars e1 e2
616| Scall ret ef args ⇒
617    do ef' ← translate_expr vars ef;
618    do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
619    do args' ← mmap … (translate_expr_sigma vars) args;
620    match ret with
621    [ None ⇒ OK ? (St_call (None ?) ef' args')
622    | Some e1 ⇒
623        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
624        match dest with
625        [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')
626        | MemDest r q e1' ⇒
627            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
628            OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))
629        ]
630    ]
631| Ssequence s1 s2 ⇒
632    do s1' ← translate_statement vars tmp tmpp s1;
633    do s2' ← translate_statement vars tmp tmpp s2;
634    OK ? (St_seq s1' s2')
635| Sifthenelse e1 s1 s2 ⇒
636    do e1' ← translate_expr vars e1;
637    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
638    [ ASTint _ _ ⇒ λe1'.
639        do s1' ← translate_statement vars tmp tmpp s1;
640        do s2' ← translate_statement vars tmp tmpp s2;
641        OK ? (St_ifthenelse ?? e1' s1' s2')
642    | _ ⇒ λ_.Error ? (msg TypeMismatch)
643    ] e1'
644| Swhile e1 s1 ⇒
645    do e1' ← translate_expr vars e1;
646    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
647    [ ASTint _ _ ⇒ λe1'.
648        do s1' ← translate_statement vars tmp tmpp s1;
649        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
650        OK ? (St_block
651               (St_loop
652                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))))
653    | _ ⇒ λ_.Error ? (msg TypeMismatch)
654    ] e1'
655| Sdowhile e1 s1 ⇒
656    do e1' ← translate_expr vars e1;
657    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
658    [ ASTint _ _ ⇒ λe1'.
659        do s1' ← translate_statement vars tmp tmpp s1;
660        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
661        OK ? (St_block
662               (St_loop
663                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))))
664    | _ ⇒ λ_.Error ? (msg TypeMismatch)
665    ] e1'
666| Sfor s1 e1 s2 s3 ⇒
667    do e1' ← translate_expr vars e1;
668    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
669    [ ASTint _ _ ⇒ λe1'.
670        do s1' ← translate_statement vars tmp tmpp s1;
671        do s2' ← translate_statement vars tmp tmpp s2;
672        do s3' ← translate_statement vars tmp tmpp s3;
673        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
674        OK ? (St_seq s1'
675             (St_block
676               (St_loop
677                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))))
678    | _ ⇒ λ_.Error ? (msg TypeMismatch)
679    ] e1'
680| Sbreak ⇒ OK ? (St_exit 1)
681| Scontinue ⇒ OK ? (St_exit 0)
682| Sreturn ret ⇒
683    match ret with
684    [ None ⇒ OK ? (St_return (None ?))
685    | Some e1 ⇒
686        do e1' ← translate_expr vars e1;
687        OK ? (St_return (Some ? (dp … e1')))
688    ]
689| Sswitch e1 ls ⇒ Error ? (msg FIXME)
690| Slabel l s1 ⇒
691    do s1' ← translate_statement vars tmp tmpp s1;
692    OK ? (St_label l s1')
693| Sgoto l ⇒ OK ? (St_goto l)
694| Scost l s1 ⇒
695    do s1' ← translate_statement vars tmp tmpp s1;
696    OK ? (St_cost l s1')
697].
698
699
700definition bigid1 ≝ an_identifier SymbolTag [[
701false;true;false;false;
702false;false;false;false;
703false;false;false;false;
704false;false;false;false]].
705definition bigid2 ≝ an_identifier SymbolTag [[
706false;true;false;false;
707false;false;false;false;
708false;false;false;false;
709false;false;false;true]].
710
711(* FIXME: the temporary handling is nonsense, I'm afraid. *)
712definition translate_function : list (ident×region) → function → res internal_function ≝
713λglobals, f.
714  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
715  let tmp ≝ bigid1 in (* FIXME *)
716  let tmpp ≝ bigid2 in (* FIXME *)
717  do s ← translate_statement vartypes tmp tmpp (fn_body f);
718  OK ? (mk_internal_function
719    (opttyp_of_type (fn_return f))
720    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
721    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
722    stacksize
723    s).
724
725definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
726λglobals,f.
727match f with
728[ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
729| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
730].
731
732definition clight_to_cminor : clight_program → res Cminor_program ≝
733λp.
734  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
735  let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
736  let globals ≝ fun_globals @ var_globals in
737  transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
Note: See TracBrowser for help on using the repository browser.