source: src/Clight/toCminor.ma @ 880

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

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File size: 27.8 KB
RevLine 
[816]1
2include "Clight/Csyntax.ma".
[880]3include "Clight/TypeComparison.ma".
[816]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 : 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 → function → var_types × nat ≝
169λglobals, f.
170  let m ≝ foldl ?? (λm,id. add ?? m id Global) (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 ≝
[880]213λty1,e1,ty2,e2,ty'.
214let ty1' ≝ typ_of_type ty1 in
215let ty2' ≝ typ_of_type ty2 in
[816]216match classify_add ty1 ty2 with
[880]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))))))
[816]221| add_default ⇒ Error ? (msg TypeMismatch)
222].
223
224definition translate_sub ≝
[880]225λty1,e1,ty2,e2,ty'.
226let ty1' ≝ typ_of_type ty1 in
227let ty2' ≝ typ_of_type ty2 in
[816]228match classify_sub ty1 ty2 with
[880]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)))))
[816]233| sub_default ⇒ Error ? (msg TypeMismatch)
234].
235
236definition translate_mul ≝
[880]237λty1,e1,ty2,e2,ty'.
238let ty1' ≝ typ_of_type ty1 in
239let ty2' ≝ typ_of_type ty2 in
[816]240match classify_mul ty1 ty2 with
[880]241[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
242| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
[816]243| mul_default ⇒ Error ? (msg TypeMismatch)
244].
245
246definition translate_div ≝
[880]247λty1,e1,ty2,e2,ty'.
248let ty1' ≝ typ_of_type ty1 in
249let ty2' ≝ typ_of_type ty2 in
[816]250match classify_div ty1 ty2 with
[880]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)
[816]254| div_default ⇒ Error ? (msg TypeMismatch)
255].
256
257definition translate_mod ≝
[880]258λty1,e1,ty2,e2,ty'.
259let ty1' ≝ typ_of_type ty1 in
260let ty2' ≝ typ_of_type ty2 in
[816]261match classify_mod ty1 ty2 with
[880]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)
[816]264| mod_default ⇒ Error ? (msg TypeMismatch)
265].
266
267definition translate_shr ≝
[880]268λty1,e1,ty2,e2,ty'.
269let ty1' ≝ typ_of_type ty1 in
270let ty2' ≝ typ_of_type ty2 in
[816]271match classify_shr ty1 ty2 with
[880]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)
[816]274| shr_default ⇒ Error ? (msg TypeMismatch)
275].
276
277definition translate_cmp ≝
[880]278λc,ty1,e1,ty2,e2,ty'.
279let ty1' ≝ typ_of_type ty1 in
280let ty2' ≝ typ_of_type ty2 in
[816]281match classify_cmp ty1 ty2 with
[880]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)
[816]286| cmp_default ⇒ Error ? (msg TypeMismatch)
287].
288
[880]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
[816]292match op with
[880]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'
[816]309].
310
[880]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)
[816]337    | _ ⇒ Error ? (msg TypeMismatch)
338    ]
[880]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 *)
[816]343    | _ ⇒ Error ? (msg TypeMismatch)
344    ]
[880]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
[816]350    | _ ⇒ Error ? (msg TypeMismatch)
351    ]
[880]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
[816]357    | _ ⇒ Error ? (msg TypeMismatch)
358    ]
[880]359| _ ⇒ λ_. Error ? (msg TypeMismatch)
[816]360].
361
[880]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 typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
368* [ #sz1 #sg1 | #r1 | #sz1 ]
369* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
370[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
371  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
372| *; cases r1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
373| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
374] qed.
375
376let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝
[816]377match e with
378[ Expr ed ty ⇒
379  match ed with
[880]380  [ Econst_int i ⇒ OK ? (Cst ? (Ointconst i))
381  | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
[816]382  | Evar id ⇒
383      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
384      match c with
385      [ Global ⇒
386          match access_mode ty with
[880]387          [ By_value q ⇒ OK ? (Mem ? q (Cst ? (Oaddrsymbol id zero)))
388          | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
[816]389          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
390          ]
391      | Stack n ⇒
392          match access_mode ty with
[880]393          [ By_value q ⇒ OK ? (Mem ? q (Cst ? (Oaddrstack (repr n))))
394          | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
[816]395          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
396          ]
[880]397      | Local ⇒ OK ? (Id ? id)
[816]398      ]
399  | Ederef e1 ⇒
400      do e1' ← translate_expr vars e1;
[880]401      do e1' ← typ_should_eq ? (ASTptr Any) ? e1';
402      do e' ← match access_mode ty with
403      [ By_value q ⇒ OK ? (Mem ? q e1')
[816]404      | By_reference _ ⇒ OK ? e1'
405      | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
[880]406      ];
407      typ_should_eq ? (typ_of_type (typeof e)) ? e'
408  | Eaddrof e1 ⇒
409      do e1' ← translate_addr vars e1;
410      match typ_of_type (typeof e) return λx.res (CMexpr x) with
411      [ ASTptr r ⇒ match r return λx.res (CMexpr (ASTptr x)) with [ Any ⇒ OK ? e1' | _ ⇒ Error ? (msg TypeMismatch) ]
412      | _ ⇒ Error ? (msg TypeMismatch)
[816]413      ]
414  | Eunop op e1 ⇒
415      do op' ← translate_unop ty op;
416      do e1' ← translate_expr vars e1;
[880]417      OK ? (Op1 ?? op' e1')
[816]418  | Ebinop op e1 e2 ⇒
419      do e1' ← translate_expr vars e1;
420      do e2' ← translate_expr vars e2;
[880]421      translate_binop op (typeof e1) e1' (typeof e2) e2' (typeof e)
[816]422  | Ecast ty1 e1 ⇒
423      do e1' ← translate_expr vars e1;
[880]424      do e' ← translate_cast (typeof e1) ty1 e1';
425      typ_should_eq ? (typ_of_type (typeof e)) ? e'
[816]426  | Econdition e1 e2 e3 ⇒
427      do e1' ← translate_expr vars e1;
428      do e2' ← translate_expr vars e2;
[880]429      do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
[816]430      do e3' ← translate_expr vars e3;
[880]431      do e3' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e3';
432      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
433      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')
434      | _ ⇒ λ_.Error ? (msg TypeMismatch)
435      ] e1'
[816]436  | Eandbool e1 e2 ⇒
437      do e1' ← translate_expr vars e1;
438      do e2' ← translate_expr vars e2;
[880]439      do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
440      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type (typeof e))) with
441      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst zero)))
442      | _ ⇒ λ_.Error ? (msg TypeMismatch)
443      ] e1'
[816]444  | Eorbool e1 e2 ⇒
445      do e1' ← translate_expr vars e1;
446      do e2' ← translate_expr vars e2;
[880]447      do e2' ← type_should_eq ? (typeof e) (λx.CMexpr (typ_of_type x)) e2';
448      match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type (typeof e))) with
449      [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst one)) e2')
450      | _ ⇒ λ_.Error ? (msg TypeMismatch)
451      ] e1'
452  | Esizeof ty1 ⇒ OK ? (Cst ? (Ointconst (repr (sizeof ty1))))
[816]453  | Efield e1 id ⇒
[880]454      do e' ← match typeof e1 with
[816]455      [ Tstruct _ fl ⇒
456          do e1' ← translate_addr vars e1;
457          do off ← field_offset id fl;
458          match access_mode ty with
[880]459          [ By_value q ⇒ OK ? (Mem ? q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off)))))
460          | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst (repr off))))
[816]461          | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
462          ]
463      | Tunion _ _ ⇒
464          do e1' ← translate_addr vars e1;
465          match access_mode ty with
[880]466          [ By_value q ⇒ OK ? (Mem ? q e1')
[816]467          | By_reference _ ⇒ OK ? e1'
468          | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
469          ]
470      | _ ⇒ Error ? (msg BadlyTypedAccess)
[880]471      ];
472      typ_should_eq ? (typ_of_type (typeof e)) ? e'
[816]473  | Ecost l e1 ⇒
474      do e1' ← translate_expr vars e1;
[880]475      do e' ← OK ? (Ecost ? l e1');
476      typ_should_eq ? (typ_of_type (typeof e)) ? e'
[816]477  ]
[880]478] and translate_addr (vars:var_types) (e:expr) on e : res (CMexpr (ASTptr Any)) ≝
[816]479match e with
480[ Expr ed _ ⇒
481  match ed with
482  [ Evar id ⇒
483      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
484      match c with
[880]485      [ Global ⇒ OK ? (Cst ? (Oaddrsymbol id zero))
486      | Stack n ⇒ OK ? (Cst ? (Oaddrstack (repr n)))
[816]487      | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
488      ]
[880]489  | Ederef e1 ⇒
490      do e1' ← translate_expr vars e1;
491      match typ_of_type (typeof e1) return λx. CMexpr x → res (CMexpr (ASTptr Any)) with
492      [ ASTptr r ⇒ match r return λx. CMexpr (ASTptr x) → res (CMexpr (ASTptr Any)) with [ Any ⇒ λe1'.OK ? e1' | _ ⇒ λ_.Error ? (msg BadlyTypedAccess) ]
493      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
494      ] e1'
[816]495  | Efield e1 id ⇒
496      match typeof e1 with
497      [ Tstruct _ fl ⇒
498          do e1' ← translate_addr vars e1;
499          do off ← field_offset id fl;
[880]500          OK ? (Op2 (ASTptr Any) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr Any) Oaddp e1' (Cst ? (Ointconst (repr off))))
[816]501      | Tunion _ _ ⇒ translate_addr vars e1
502      | _ ⇒ Error ? (msg BadlyTypedAccess)
503      ]
504  | _ ⇒ Error ? (msg BadLvalue)
505  ]
506].
507
508inductive destination : Type[0] ≝
509| IdDest : ident → destination
[880]510| MemDest : memory_chunk → CMexpr (ASTptr Any) → destination.
[816]511
512definition translate_dest ≝
513λvars,e1,ty2.
514    do q ← match access_mode ty2 with
515           [ By_value q ⇒ OK ? q
516           | By_reference r ⇒ OK ? (Mpointer r)
517           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
518           ];
519    match e1 with
520    [ Expr ed1 ty1 ⇒
521        match ed1 with
522        [ Evar id ⇒
523            do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
524            match c with
525            [ Local ⇒ OK ? (IdDest id)
[880]526            | Global ⇒ OK ? (MemDest q (Cst ? (Oaddrsymbol id zero)))
527            | Stack n ⇒ OK ? (MemDest q (Cst ? (Oaddrstack (repr n))))
[816]528            ]
529        | _ ⇒
530            do e1' ← translate_addr vars e1;
531            OK ? (MemDest q e1')
532        ]
533    ].
534(*
535definition translate_assign ≝
536λvars,e1,e2.
537    do e2' ← translate_expr vars e2;
538    do q ← match access_mode (typeof e2) with
539           [ By_value q ⇒ OK ? q
540           | By_reference r ⇒ OK ? (Mpointer r)
541           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
542           ];
543    match e1 with
544    [ Expr ed1 ty1 ⇒
545        match ed1 with
546        [ Evar id ⇒
547            do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
548            match c with
549            [ Local ⇒ OK ? (St_assign id e2')
550            | Global ⇒ OK ? (St_store q (Cst (Oaddrsymbol id zero)) e2')
551            | Stack n ⇒ OK ? (St_store q (Cst (Oaddrstack (repr n))) e2')
552            ]
553        | _ ⇒
554            do e1' ← translate_addr vars e1;
555            OK ? (St_store q e1' e2')
556        ]
557    ].
558*)
559definition translate_assign ≝
560λvars,e1,e2.
561do e2' ← translate_expr vars e2;
562do dest ← translate_dest vars e1 (typeof e2);
563match dest with
[880]564[ IdDest id ⇒ OK ? (St_assign ? id e2')
565| MemDest q e1' ⇒ OK ? (St_store ? q e1' e2')
[816]566].
567
568definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
569λA,B,f,oa.
570match oa with
571[ None ⇒ OK ? (None ?)
572| Some a ⇒ do b ← f a; OK ? (Some ? b)
573].
574
[880]575definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝
576λv,e.
577  do e' ← translate_expr v e;
578  OK ? (dp ? (λt:typ.CMexpr t) ? e').
579
[816]580axiom FIXME : String.
581
582let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝
583match s with
584[ Sskip ⇒ OK ? St_skip
585| Sassign e1 e2 ⇒ translate_assign vars e1 e2
586| Scall ret ef args ⇒
587    do ef' ← translate_expr vars ef;
[880]588    do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
589    do args' ← mmap … (translate_expr_sigma vars) args;
[816]590    match ret with
591    [ None ⇒ OK ? (St_call (None ?) ef' args')
592    | Some e1 ⇒
593        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
594        match dest with
595        [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')
596        | MemDest q e1' ⇒
597            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
[880]598            OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store ? (typ_of_memory_chunk q) q e1' (Id ? tmp)))
[816]599        ]
600    ]
601| Ssequence s1 s2 ⇒
602    do s1' ← translate_statement vars tmp tmpp s1;
603    do s2' ← translate_statement vars tmp tmpp s2;
604    OK ? (St_seq s1' s2')
605| Sifthenelse e1 s1 s2 ⇒
606    do e1' ← translate_expr vars e1;
[880]607    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
608    [ ASTint _ _ ⇒ λe1'.
609        do s1' ← translate_statement vars tmp tmpp s1;
610        do s2' ← translate_statement vars tmp tmpp s2;
611        OK ? (St_ifthenelse ?? e1' s1' s2')
612    | _ ⇒ λ_.Error ? (msg TypeMismatch)
613    ] e1'
[816]614| Swhile e1 s1 ⇒
615    do e1' ← translate_expr vars e1;
[880]616    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
617    [ ASTint _ _ ⇒ λe1'.
618        do s1' ← translate_statement vars tmp tmpp s1;
619        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
620        OK ? (St_block
621               (St_loop
622                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))))
623    | _ ⇒ λ_.Error ? (msg TypeMismatch)
624    ] e1'
[816]625| Sdowhile e1 s1 ⇒
626    do e1' ← translate_expr vars e1;
[880]627    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
628    [ ASTint _ _ ⇒ λe1'.
629        do s1' ← translate_statement vars tmp tmpp s1;
630        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
631        OK ? (St_block
632               (St_loop
633                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))))
634    | _ ⇒ λ_.Error ? (msg TypeMismatch)
635    ] e1'
[816]636| Sfor s1 e1 s2 s3 ⇒
637    do e1' ← translate_expr vars e1;
[880]638    match typ_of_type (typeof e1) return λx.CMexpr x → ? with
639    [ ASTint _ _ ⇒ λe1'.
640        do s1' ← translate_statement vars tmp tmpp s1;
641        do s2' ← translate_statement vars tmp tmpp s2;
642        do s3' ← translate_statement vars tmp tmpp s3;
643        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
644        OK ? (St_seq s1'
645             (St_block
646               (St_loop
647                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))))
648    | _ ⇒ λ_.Error ? (msg TypeMismatch)
649    ] e1'
[816]650| Sbreak ⇒ OK ? (St_exit 1)
651| Scontinue ⇒ OK ? (St_exit 0)
652| Sreturn ret ⇒
[880]653    match ret with
654    [ None ⇒ OK ? (St_return (None ?))
655    | Some e1 ⇒
656        do e1' ← translate_expr vars e1;
657        OK ? (St_return (Some ? (dp … e1')))
658    ]
[816]659| Sswitch e1 ls ⇒ Error ? (msg FIXME)
660| Slabel l s1 ⇒
661    do s1' ← translate_statement vars tmp tmpp s1;
662    OK ? (St_label l s1')
663| Sgoto l ⇒ OK ? (St_goto l)
664| Scost l s1 ⇒
665    do s1' ← translate_statement vars tmp tmpp s1;
666    OK ? (St_cost l s1')
667].
668
669
670definition is_pointer : type → bool ≝
671λty.
672  match ty with
673  [ Tpointer _ _ ⇒ true
674  | Tfunction _ _ ⇒ true
675  | _ ⇒ false
676  ].
677
678definition bigid1 ≝ an_identifier SymbolTag [[
679false;true;false;false;
680false;false;false;false;
681false;false;false;false;
682false;false;false;false]].
683definition bigid2 ≝ an_identifier SymbolTag [[
684false;true;false;false;
685false;false;false;false;
686false;false;false;false;
687false;false;false;true]].
688
689definition translate_function : list ident → function → res internal_function ≝
690λglobals, f.
691  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
692  let tmp ≝ bigid1 in (* FIXME *)
693  let tmpp ≝ bigid2 in (* FIXME *)
694  let p_ptrs ≝ filter ? (λx. is_pointer (\snd x)) (fn_params f) in
695  let v_ptrs ≝ (filter ? (λx. is_pointer (\snd x)) (fn_vars f)) in
696  do s ← translate_statement vartypes tmp tmpp (fn_body f);
697  OK ? (mk_internal_function
698    (signature_of_type (type_of_params (fn_params f)) (fn_return f))
699    (map ?? (fst ??) (fn_params f))
700    (tmp::tmpp::(map ?? (fst ??) (fn_vars f)))
701    (tmpp::(map ?? (fst ??) p_ptrs) @ (map ?? (fst ??) v_ptrs))
702    stacksize
703    s).
704
705definition translate_fundef : list ident → clight_fundef → res (fundef internal_function) ≝
706λglobals,f.
707match f with
708[ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
709| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
710].
711
712definition clight_to_cminor : clight_program → res Cminor_program ≝
713λp.
714  let globals ≝ (prog_funct_names ?? p)@(prog_var_names ?? p) in
715  transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
Note: See TracBrowser for help on using the repository browser.