source: src/Cminor/toRTLabs.ma @ 797

Last change on this file since 797 was 797, checked in by campbell, 10 years ago

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 15.3 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 (e:expr) (ptrs:list ident) : 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 → expr → list ident → internal_function → res (register × internal_function) ≝
98λenv,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 expr → list ident → internal_function → res (list register × internal_function) ≝
108λenv,es,ptrs,f.
109  foldr ?? (λe,acc. do 〈rs,f〉 ← acc;
110                    do 〈r,f'〉 ← choose_reg env e ptrs f;
111                    OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
112
113axiom BadCminorProgram : String.
114
115let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
116match e with
117[ Id i ⇒
118    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
119    match register_eq r dst with
120    [ inl _ ⇒ OK ? f
121    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
122    ]
123| Cst c ⇒ add_fresh_to_graph (St_const dst c) f
124| Op1 op e' ⇒
125    do 〈r,f〉 ← choose_reg env e' ptrs f;
126    do f ← add_fresh_to_graph (St_op1 op dst r) f;
127    add_expr env e' r ptrs f
128| Op2 op e1 e2 ⇒
129    do 〈r1,f〉 ← choose_reg env e1 ptrs f;
130    do 〈r2,f〉 ← choose_reg env e2 ptrs f;
131    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
132    do f ← add_expr env e2 r2 ptrs f;
133    add_expr env e1 r1 ptrs f
134| Mem q e' ⇒
135    add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e')
136| Cond e' e1 e2 ⇒
137    let resume_at ≝ f_entry f in
138    do f ← add_expr env e2 dst ptrs f;
139    let lfalse ≝ f_entry f in
140    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
141    do f ← add_expr env e1 dst ptrs f;
142    add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr env e')
143| Ecost l e' ⇒
144    do f ← add_expr env e' dst ptrs f;
145    add_fresh_to_graph (St_cost l) f
146   
147(* Ugh, the termination checker isn't smart enough to notice that calling
148   add_expr with e is OK, so we take it partially applied and define a proper
149   add_<whatever> afterwards. *)
150]
151and add_with_addressing_internal (env:env) (e:expr)
152                          (s:∀m:addressing. addr m → label → statement)
153                          (ptrs:list ident)
154                          (f:internal_function)
155                          (termination_hack:register → list ident → internal_function → res internal_function)
156                          on e : res internal_function ≝
157let add_default : unit → res internal_function ≝ λ_.
158    do 〈r, f〉 ← choose_reg env e ptrs f;
159    do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
160    termination_hack r ptrs f
161in
162match e with
163[ Cst c ⇒
164    match c with
165    [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
166    | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f
167    | _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *)
168    ]
169| Op2 op e1 e2 ⇒
170    match op with
171    [ Oaddp ⇒
172        let add_generic_addp : unit → res internal_function ≝ λ_.
173          do 〈r1, f〉 ← choose_reg env e1 ptrs f;
174          do 〈r2, f〉 ← choose_reg env e2 ptrs f;
175          do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
176          do f ← add_expr env e2 r2 ptrs f;
177          add_expr env e1 r1 ptrs f
178        in
179        match e1 with
180        [ Cst c ⇒
181            match c with
182            [ Oaddrsymbol id i ⇒
183                do 〈r, f〉 ← choose_reg env e ptrs f;
184                do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
185                add_expr env e2 r ptrs f
186            | _ ⇒ add_generic_addp it
187            ]
188        | _ ⇒ add_generic_addp it
189        ]
190    | _ ⇒ add_default it
191    ]
192| _ ⇒ add_default it
193]
194(* and again *)
195and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
196        (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝
197match e with
198[ Id i ⇒
199    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
200    add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
201| Cst c ⇒
202    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
203| Op1 op e' ⇒
204    do 〈r,f〉 ← choose_reg env e' ptrs f;
205    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
206    add_expr env e' r ptrs f
207| Op2 op e1 e2 ⇒
208    do 〈r1,f〉 ← choose_reg env e1 ptrs f;
209    do 〈r2,f〉 ← choose_reg env e2 ptrs f;
210    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
211    do f ← add_expr env e2 r2 ptrs f;
212    add_expr env e1 r1 ptrs f
213| _ ⇒
214    do 〈r,f〉 ← choose_reg env e ptrs f;
215    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
216    termination_hack_add_expr r ptrs f
217].
218
219(* See comment above. *)
220definition add_with_addressing ≝
221λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e).
222definition add_branch ≝
223λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e).
224
225(* This shouldn't occur; maybe use vectors? *)
226axiom WrongNumberOfArguments : String.
227
228let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
229match es with
230[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
231| cons e et ⇒
232    match dsts with
233    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
234    | cons r rt ⇒
235        do f ← add_exprs env et rt ptrs f;
236        add_expr env e r ptrs f
237    ]
238].
239
240axiom UnknownLabel : String.
241axiom ReturnMismatch : String.
242
243let 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 ≝
244match s with
245[ St_skip ⇒ OK ? f
246| St_assign x e ⇒
247    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
248    add_expr env e dst ptrs f
249| St_store q e1 e2 ⇒
250    do 〈val_reg, f〉 ← choose_reg env e2 ptrs f;
251    do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f;
252    add_expr env e2 val_reg ptrs f
253| St_call return_opt_id e args sig ⇒
254    do return_opt_reg ←
255      match return_opt_id with
256      [ None ⇒ OK ? (None ?)
257      | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)
258      ];
259    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
260    do f ←
261      match e with
262      [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f
263      | _ ⇒
264        do 〈fnr, f〉 ← choose_reg env e ptrs f;
265        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f;
266        add_expr env e fnr ptrs f
267      ];
268    add_exprs env args args_regs ptrs f
269| St_tailcall e args sig ⇒
270    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
271    do f ←
272      match e with
273      [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f
274      | _ ⇒
275        do 〈fnr, f〉 ← choose_reg env e ptrs f;
276        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f;
277        add_expr env e fnr ptrs f
278      ];
279    add_exprs env args args_regs ptrs f
280| St_seq s1 s2 ⇒
281    do f ← add_stmt env label_env s2 exits ptrs f;
282    add_stmt env label_env s1 exits ptrs f
283| St_ifthenelse e s1 s2 ⇒
284    let l_next ≝ f_entry f in
285    do f ← add_stmt env label_env s2 exits ptrs f;
286    let l2 ≝ f_entry f in
287    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
288    do f ← add_stmt env label_env s1 exits ptrs f;
289    add_branch env e (f_entry f) l2 ptrs f
290| St_loop s ⇒
291    do f ← add_loop_label_to_graph f;
292    let l_loop ≝ f_entry f in
293    do f ← add_stmt env label_env s exits ptrs f;
294    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
295| St_block s ⇒
296    add_stmt env label_env s ((f_entry f)::exits) ptrs f
297| St_exit n ⇒
298    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
299    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
300| St_switch e tab n ⇒
301    do 〈r,f〉 ← choose_reg env e ptrs f;
302    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
303    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
304    do f ← foldr ?? (λcs,f.
305      do f ← f;
306      let 〈i,n〉 ≝ cs in
307      do 〈cr,f〉 ← fresh_reg … f;
308      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
309      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
310      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
311    add_expr env e r ptrs f
312| St_return opt_e ⇒
313    do f ← add_fresh_to_graph (λ_. St_return) f;
314    match opt_e with
315    [ None ⇒ OK ? f
316    | Some e ⇒
317        match f_result f with
318        [ None ⇒ Error ? (msg ReturnMismatch)
319        | Some r ⇒ add_expr env e r ptrs f
320        ]
321    ]
322| St_label l s' ⇒
323    do f ← add_stmt env label_env s' exits ptrs f;
324    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
325    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
326| St_goto l ⇒
327    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
328    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
329| St_cost l s' ⇒
330    do f ← add_stmt env label_env s' exits ptrs f;
331    add_fresh_to_graph (St_cost l) f
332].
333[ @(λ_. St_skip l_next)
334| @(St_skip (f_entry f))
335| @(λ_. St_skip l)
336| @(λ_. St_skip l_default)
337| @(St_skip (f_entry f))
338| @(λ_.St_skip l')
339] qed.
340
341(* Get labels from a Cminor statement. *)
342let rec labels_of (s:stmt) : list ident ≝
343match s with
344[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
345| St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
346| St_loop s ⇒ labels_of s
347| St_block s ⇒ labels_of s
348| St_label l s ⇒ l::(labels_of s)
349| St_cost _ s ⇒ labels_of s
350| _ ⇒ [ ]
351].
352
353definition c2ra_function (*: internal_function → internal_function*) ≝
354λf.
355let labgen0 ≝ new_universe LabelTag in
356let reggen0 ≝ new_universe RegisterTag in
357let cminor_labels ≝ labels_of (f_body f) in
358do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
359do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
360do 〈result, locals, reggen〉 ←
361  match sig_res (f_sig f) with
362  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
363  | Some _ ⇒
364      do 〈r,gen〉 ← fresh … reggen2;
365      OK ? 〈Some ? r, r::locals0, gen〉 ];
366do ptrs ← mmap ?? (λid. opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id)) (f_ptrs f);
367do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
368do 〈l,labgen〉 ← fresh … labgen1;
369let emptyfn ≝
370  mk_internal_function
371    labgen
372    reggen
373    (f_sig f)
374    result
375    params
376    locals
377    ptrs
378    (f_stacksize f)
379    (add ?? (empty_map …) l St_return)
380    l
381    l in
382  add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn
383.
384
385definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
386transform_partial_program ???
387  (transf_partial_fundef ?? c2ra_function).
388
389include "Cminor/initialisation.ma".
390
391definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
392λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.