source: src/Clight/toCminor.ma @ 961

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

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

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