source: src/Clight/toCminor.ma @ 816

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

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

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