source: src/Cminor/toRTLabs.ma @ 880

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

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

File size: 15.6 KB
Line 
1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5
6definition env ≝ identifier_map SymbolTag register.
7definition label_env ≝ identifier_map SymbolTag label.
8definition populate_env : env → universe RegisterTag → list ident → res (list register × env × (universe RegisterTag)) ≝
9λen,gen. foldr ??
10 (λid,rsengen.
11   do 〈rs,en,gen〉 ← rsengen;
12   do 〈r,gen'〉 ← fresh … gen;
13   OK ? 〈r::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
14
15definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝
16λen,gen. foldr ??
17 (λid,engen.
18   do 〈en,gen〉 ← engen;
19   do 〈r,gen'〉 ← fresh … gen;
20   OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉).
21
22(* Add a statement to the graph, *without* updating the entry label. *)
23definition fill_in_statement : label → statement → internal_function → internal_function ≝
24λl,s,f.
25  mk_internal_function (f_labgen f) (f_reggen f) (f_sig f)
26                       (f_result f) (f_params f) (f_locals f) (f_ptrs f)
27                       (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f).
28
29(* Add a statement to the graph, making it the entry label. *)
30definition add_to_graph : label → statement → internal_function → internal_function ≝
31λl,s,f.
32  mk_internal_function (f_labgen f) (f_reggen f) (f_sig f)
33                       (f_result f) (f_params f) (f_locals f) (f_ptrs f)
34                       (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f).
35
36(* Add a statement with a fresh label to the start of the function.  The
37   statement is parametrised by the *next* instruction's label. *)
38definition add_fresh_to_graph : (label → statement) → internal_function → res internal_function ≝
39λs,f.
40  do 〈l,g〉 ← fresh … (f_labgen f);
41  let s' ≝ s (f_entry f) in
42  OK ? (mk_internal_function g (f_reggen f) (f_sig f)
43                       (f_result f) (f_params f) (f_locals f) (f_ptrs f)
44                       (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
45
46(* Generate a fresh label and use it as a dangling entry point, to be filled in
47   later with the loop head. *)
48definition add_loop_label_to_graph : internal_function → res internal_function ≝
49λf.
50  do 〈l,g〉 ← fresh … (f_labgen f);
51  OK ? (mk_internal_function g (f_reggen f) (f_sig f)
52                       (f_result f) (f_params f) (f_locals f) (f_ptrs f)
53                       (f_stacksize f) (f_graph f) l (f_exit f)).
54
55definition fresh_reg : internal_function → res (register × internal_function) ≝
56λf.
57  do 〈r,g〉 ← fresh … (f_reggen f);
58  OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f)
59                       (f_result f) (f_params f) (r::(f_locals f)) (f_ptrs f)
60                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
61
62definition fresh_ptr_reg : internal_function → res (register × internal_function) ≝
63λf.
64  do 〈r,g〉 ← fresh … (f_reggen f);
65  OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f)
66                       (f_result f) (f_params f) (r::(f_locals f)) (r::(f_ptrs f))
67                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
68
69let rec expr_yields_pointer (ty:typ) (e:expr ty) (ptrs:list ident) on e : bool ≝
70match e with
71[ Id _ i ⇒ exists ? (eq_identifier ? i) ptrs
72| Cst _ c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ]
73| Op1 _ _ op e' ⇒
74    match op with
75    [ Oid ⇒ expr_yields_pointer ? e' ptrs
76    | Optrofint _ ⇒ true
77    | _ ⇒ false
78    ]
79| Op2 _ _ _ op e1 e2 ⇒
80    match op with
81    [ Oaddp ⇒ true
82    | Osubpi ⇒ true
83    | _ ⇒ false
84    ]
85| Mem _ q e' ⇒
86    match q with
87    [ Mpointer _ ⇒ true
88    | _ ⇒ false
89    ]
90(* Both branches ought to be the same? *)
91| Cond _ _ _ e' e1 e2 ⇒ (expr_yields_pointer ? e1 ptrs) ∨ (expr_yields_pointer ? e2 ptrs)
92| Ecost _ _ e' ⇒ expr_yields_pointer ? e' ptrs
93].
94
95axiom UnknownVariable : String.
96
97definition choose_reg : env → ∀t.expr t → list ident → internal_function → res (register × internal_function) ≝
98λenv,ty,e,ptrs,f.
99  match e with
100  [ Id _ i ⇒
101      do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i);
102      OK ? 〈r, f〉
103  | _ ⇒
104      if expr_yields_pointer ? e ptrs then fresh_ptr_reg f else fresh_reg f
105  ].
106
107definition choose_regs : env → list (Σt:typ.expr t) → list ident → internal_function → res (list register × internal_function) ≝
108λenv,es,ptrs,f.
109  foldr (Σt:typ.expr t) ?
110    (λe,acc. do 〈rs,f〉 ← acc;
111             do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e ptrs f ];
112             OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
113
114axiom BadCminorProgram : String.
115
116let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
117match e with
118[ Id _ i ⇒
119    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
120    match register_eq r dst with
121    [ inl _ ⇒ OK ? f
122    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
123    ]
124| Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f
125| Op1 _ _ op e' ⇒
126    do 〈r,f〉 ← choose_reg env ? e' ptrs f;
127    do f ← add_fresh_to_graph (St_op1 op dst r) f;
128    add_expr env ? e' r ptrs f
129| Op2 _ _ _ op e1 e2 ⇒
130    do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
131    do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
132    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
133    do f ← add_expr env ? e2 r2 ptrs f;
134    add_expr env ? e1 r1 ptrs f
135| Mem _ q e' ⇒
136    add_with_addressing_internal env ? e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env ? e')
137| Cond _ _ _ e' e1 e2 ⇒
138    let resume_at ≝ f_entry f in
139    do f ← add_expr env ? e2 dst ptrs f;
140    let lfalse ≝ f_entry f in
141    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
142    do f ← add_expr env ? e1 dst ptrs f;
143    add_branch_internal env ? e' (f_entry f) lfalse ptrs f (add_expr env ? e')
144| Ecost _ l e' ⇒
145    do f ← add_expr env ? e' dst ptrs f;
146    add_fresh_to_graph (St_cost l) f
147   
148(* Ugh, the termination checker isn't smart enough to notice that calling
149   add_expr with e is OK, so we take it partially applied and define a proper
150   add_<whatever> afterwards. *)
151]
152and add_with_addressing_internal (env:env) (ty:typ) (e:expr ty)
153                          (s:∀m:addressing. addr m → label → statement)
154                          (ptrs:list ident)
155                          (f:internal_function)
156                          (termination_hack:register → list ident → internal_function → res internal_function)
157                          on e : res internal_function ≝
158let add_default : unit → res internal_function ≝ λ_.
159    do 〈r, f〉 ← choose_reg env ? e ptrs f;
160    do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
161    termination_hack r ptrs f
162in
163match e with
164[ Cst _ c ⇒
165    match c with
166    [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
167    | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f
168    | _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *)
169    ]
170| Op2 _ _ _ op e1 e2 ⇒
171    match op with
172    [ Oaddp ⇒
173        let add_generic_addp : unit → res internal_function ≝ λ_.
174          do 〈r1, f〉 ← choose_reg env ? e1 ptrs f;
175          do 〈r2, f〉 ← choose_reg env ? e2 ptrs f;
176          do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
177          do f ← add_expr env ? e2 r2 ptrs f;
178          add_expr env ? e1 r1 ptrs f
179        in
180        match e1 with
181        [ Cst _ c ⇒
182            match c with
183            [ Oaddrsymbol id i ⇒
184                do 〈r, f〉 ← choose_reg env ? e ptrs f;
185                do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
186                add_expr env ? e2 r ptrs f
187            | _ ⇒ add_generic_addp it
188            ]
189        | _ ⇒ add_generic_addp it
190        ]
191    | _ ⇒ add_default it
192    ]
193| _ ⇒ add_default it
194]
195(* and again *)
196and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
197        (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝
198match e with
199[ Id _ i ⇒
200    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
201    add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
202| Cst _ c ⇒
203    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
204| Op1 _ _ op e' ⇒
205    do 〈r,f〉 ← choose_reg env ? e' ptrs f;
206    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
207    add_expr env ? e' r ptrs f
208| Op2 _ _ _ op e1 e2 ⇒
209    do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
210    do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
211    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
212    do f ← add_expr env ? e2 r2 ptrs f;
213    add_expr env ? e1 r1 ptrs f
214| _ ⇒
215    do 〈r,f〉 ← choose_reg env ? e ptrs f;
216    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
217    termination_hack_add_expr r ptrs f
218].
219
220(* See comment above. *)
221definition add_with_addressing ≝
222λenv,ty,e,s,ptrs,f. add_with_addressing_internal env ty e s ptrs f (add_expr env ty e).
223definition add_branch ≝
224λenv,ty,e,ltrue,lfalse,ptrs,f. add_branch_internal env ty e ltrue lfalse ptrs f (add_expr env ty e).
225
226(* This shouldn't occur; maybe use vectors? *)
227axiom WrongNumberOfArguments : String.
228
229let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
230match es with
231[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
232| cons e et ⇒
233    match dsts with
234    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
235    | cons r rt ⇒
236        do f ← add_exprs env et rt ptrs f;
237        match e with [ dp ty e ⇒ add_expr env ty e r ptrs f ]
238    ]
239].
240
241axiom UnknownLabel : String.
242axiom ReturnMismatch : String.
243
244let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (ptrs:list ident) (f:internal_function) on s : res internal_function ≝
245match s with
246[ St_skip ⇒ OK ? f
247| St_assign _ x e ⇒
248    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
249    add_expr env ? e dst ptrs f
250| St_store _ q e1 e2 ⇒
251    do 〈val_reg, f〉 ← choose_reg env ? e2 ptrs f;
252    do f ← add_with_addressing env ? e1 (λm,rs. St_store q m rs val_reg) ptrs f;
253    add_expr env ? e2 val_reg ptrs f
254| St_call return_opt_id e args ⇒
255    do return_opt_reg ←
256      match return_opt_id with
257      [ None ⇒ OK ? (None ?)
258      | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)
259      ];
260    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
261    do f ←
262      match e with
263      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
264      | _ ⇒
265        do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
266        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
267        add_expr env ? e fnr ptrs f
268      ];
269    add_exprs env args args_regs ptrs f
270| St_tailcall e args ⇒
271    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
272    do f ←
273      match e with
274      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
275      | _ ⇒
276        do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
277        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
278        add_expr env ? e fnr ptrs f
279      ];
280    add_exprs env args args_regs ptrs f
281| St_seq s1 s2 ⇒
282    do f ← add_stmt env label_env s2 exits ptrs f;
283    add_stmt env label_env s1 exits ptrs f
284| St_ifthenelse _ _ e s1 s2 ⇒
285    let l_next ≝ f_entry f in
286    do f ← add_stmt env label_env s2 exits ptrs f;
287    let l2 ≝ f_entry f in
288    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
289    do f ← add_stmt env label_env s1 exits ptrs f;
290    add_branch env ? e (f_entry f) l2 ptrs f
291| St_loop s ⇒
292    do f ← add_loop_label_to_graph f;
293    let l_loop ≝ f_entry f in
294    do f ← add_stmt env label_env s exits ptrs f;
295    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
296| St_block s ⇒
297    add_stmt env label_env s ((f_entry f)::exits) ptrs f
298| St_exit n ⇒
299    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
300    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
301| St_switch _ _ e tab n ⇒
302    do 〈r,f〉 ← choose_reg env ? e ptrs f;
303    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
304    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
305    do f ← foldr ?? (λcs,f.
306      do f ← f;
307      let 〈i,n〉 ≝ cs in
308      do 〈cr,f〉 ← fresh_reg … f;
309      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
310      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
311      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
312    add_expr env ? e r ptrs f
313| St_return opt_e ⇒
314    do f ← add_fresh_to_graph (λ_. St_return) f;
315    match opt_e with
316    [ None ⇒ OK ? f
317    | Some e ⇒
318        match f_result f with
319        [ None ⇒ Error ? (msg ReturnMismatch)
320        | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e r ptrs f ]
321        ]
322    ]
323| St_label l s' ⇒
324    do f ← add_stmt env label_env s' exits ptrs f;
325    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
326    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
327| St_goto l ⇒
328    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
329    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
330| St_cost l s' ⇒
331    do f ← add_stmt env label_env s' exits ptrs f;
332    add_fresh_to_graph (St_cost l) f
333].
334[ @(λ_. St_skip l_next)
335| @(St_skip (f_entry f))
336| @(λ_. St_skip l)
337| @(λ_. St_skip l_default)
338| @(St_skip (f_entry f))
339| @(λ_.St_skip l')
340] qed.
341
342(* Get labels from a Cminor statement. *)
343let rec labels_of (s:stmt) : list ident ≝
344match s with
345[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
346| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
347| St_loop s ⇒ labels_of s
348| St_block s ⇒ labels_of s
349| St_label l s ⇒ l::(labels_of s)
350| St_cost _ s ⇒ labels_of s
351| _ ⇒ [ ]
352].
353
354definition c2ra_function (*: internal_function → internal_function*) ≝
355λf.
356let labgen0 ≝ new_universe LabelTag in
357let reggen0 ≝ new_universe RegisterTag in
358let cminor_labels ≝ labels_of (f_body f) in
359do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
360do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
361do 〈result, locals, reggen〉 ←
362  match sig_res (f_sig f) with
363  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
364  | Some _ ⇒
365      do 〈r,gen〉 ← fresh … reggen2;
366      OK ? 〈Some ? r, r::locals0, gen〉 ];
367do ptrs ← mmap ?? (λid. opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id)) (f_ptrs f);
368do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
369do 〈l,labgen〉 ← fresh … labgen1;
370let emptyfn ≝
371  mk_internal_function
372    labgen
373    reggen
374    (f_sig f)
375    result
376    params
377    locals
378    ptrs
379    (f_stacksize f)
380    (add ?? (empty_map …) l St_return)
381    l
382    l in
383  add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn
384.
385
386definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
387transform_partial_program ???
388  (transf_partial_fundef ?? c2ra_function).
389
390include "Cminor/initialisation.ma".
391
392definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
393λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.