source: src/Cminor/toRTLabs.ma @ 988

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

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

File size: 11.2 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 × typ) → res (list (register×typ) × env × (universe RegisterTag)) ≝
9λen,gen. foldr ??
10 (λidt,rsengen.
11   let 〈id,ty〉 ≝ idt in
12   do 〈rs,en,gen〉 ← rsengen;
13   do 〈r,gen'〉 ← fresh … gen;
14   OK ? 〈〈r,ty〉::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
15
16definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝
17λen,gen. foldr ??
18 (λid,engen.
19   do 〈en,gen〉 ← engen;
20   do 〈r,gen'〉 ← fresh … gen;
21   OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉).
22
23(* Add a statement to the graph, *without* updating the entry label. *)
24definition fill_in_statement : label → statement → internal_function → internal_function ≝
25λl,s,f.
26  mk_internal_function (f_labgen f) (f_reggen f)
27                       (f_result f) (f_params f) (f_locals f)
28                       (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f).
29
30(* Add a statement to the graph, making it the entry label. *)
31definition add_to_graph : label → statement → internal_function → internal_function ≝
32λl,s,f.
33  mk_internal_function (f_labgen f) (f_reggen f)
34                       (f_result f) (f_params f) (f_locals f)
35                       (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f).
36
37(* Add a statement with a fresh label to the start of the function.  The
38   statement is parametrised by the *next* instruction's label. *)
39definition add_fresh_to_graph : (label → statement) → internal_function → res internal_function ≝
40λs,f.
41  do 〈l,g〉 ← fresh … (f_labgen f);
42  let s' ≝ s (f_entry f) in
43  OK ? (mk_internal_function g (f_reggen f)
44                       (f_result f) (f_params f) (f_locals f)
45                       (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
46
47(* Generate a fresh label and use it as a dangling entry point, to be filled in
48   later with the loop head. *)
49definition add_loop_label_to_graph : internal_function → res internal_function ≝
50λf.
51  do 〈l,g〉 ← fresh … (f_labgen f);
52  OK ? (mk_internal_function g (f_reggen f)
53                       (f_result f) (f_params f) (f_locals f)
54                       (f_stacksize f) (f_graph f) l (f_exit f)).
55
56definition fresh_reg : internal_function → typ → res (register × internal_function) ≝
57λf,ty.
58  do 〈r,g〉 ← fresh … (f_reggen f);
59  OK ? 〈r, mk_internal_function (f_labgen f) g
60                       (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
61                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
62
63axiom UnknownVariable : String.
64
65definition choose_reg : env → ∀ty.expr ty → internal_function → res (register × internal_function) ≝
66λenv,ty,e,f.
67  match e with
68  [ Id _ i ⇒
69      do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i);
70      OK ? 〈r, f〉
71  | _ ⇒
72      fresh_reg f ty
73  ].
74
75definition choose_regs : env → list (Σt:typ.expr t) → internal_function → res (list register × internal_function) ≝
76λenv,es,f.
77  foldr (Σt:typ.expr t) ?
78    (λe,acc. do 〈rs,f〉 ← acc;
79             do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e f ];
80             OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
81
82axiom BadCminorProgram : String.
83
84let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (f:internal_function) on e: res internal_function ≝
85match e with
86[ Id _ i ⇒
87    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
88    match register_eq r dst with
89    [ inl _ ⇒ OK ? f
90    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
91    ]
92| Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f
93| Op1 _ _ op e' ⇒
94    do 〈r,f〉 ← choose_reg env ? e' f;
95    do f ← add_fresh_to_graph (St_op1 op dst r) f;
96    add_expr env ? e' r f
97| Op2 _ _ _ op e1 e2 ⇒
98    do 〈r1,f〉 ← choose_reg env ? e1 f;
99    do 〈r2,f〉 ← choose_reg env ? e2 f;
100    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
101    do f ← add_expr env ? e2 r2 f;
102    add_expr env ? e1 r1 f
103| Mem _ _ q e' ⇒
104    do 〈r,f〉 ← choose_reg env ? e' f;
105    do f ← add_fresh_to_graph (St_load q r dst) f;
106    add_expr env ? e' r f
107| Cond _ _ _ e' e1 e2 ⇒
108    let resume_at ≝ f_entry f in
109    do f ← add_expr env ? e2 dst f;
110    let lfalse ≝ f_entry f in
111    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
112    do f ← add_expr env ? e1 dst f;
113    do 〈r,f〉 ← choose_reg env ? e' f;
114    do f ← add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f;
115    add_expr env ? e' r f
116| Ecost _ l e' ⇒
117    do f ← add_expr env ? e' dst f;
118    add_fresh_to_graph (St_cost l) f
119].
120
121(* This shouldn't occur; maybe use vectors? *)
122axiom WrongNumberOfArguments : String.
123
124let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (f:internal_function) on es: res internal_function ≝
125match es with
126[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
127| cons e et ⇒
128    match dsts with
129    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
130    | cons r rt ⇒
131        do f ← add_exprs env et rt f;
132        match e with [ dp ty e ⇒ add_expr env ty e r f ]
133    ]
134].
135
136axiom UnknownLabel : String.
137axiom ReturnMismatch : String.
138
139let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝
140match s with
141[ St_skip ⇒ OK ? f
142| St_assign _ x e ⇒
143    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
144    add_expr env ? e dst f
145| St_store _ _ q e1 e2 ⇒
146    do 〈val_reg, f〉 ← choose_reg env ? e2 f;
147    do 〈addr_reg, f〉 ← choose_reg env ? e1 f;
148    do f ← add_fresh_to_graph (St_store q addr_reg val_reg) f;
149    do f ← add_expr env ? e1 addr_reg f;
150    add_expr env ? e2 val_reg f
151| St_call return_opt_id e args ⇒
152    do return_opt_reg ←
153      match return_opt_id with
154      [ None ⇒ OK ? (None ?)
155      | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)
156      ];
157    do 〈args_regs, f〉 ← choose_regs env args f;
158    do f ←
159      match e with
160      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
161      | _ ⇒
162        do 〈fnr, f〉 ← choose_reg env ? e f;
163        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
164        add_expr env ? e fnr f
165      ];
166    add_exprs env args args_regs f
167| St_tailcall e args ⇒
168    do 〈args_regs, f〉 ← choose_regs env args f;
169    do f ←
170      match e with
171      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
172      | _ ⇒
173        do 〈fnr, f〉 ← choose_reg env ? e f;
174        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
175        add_expr env ? e fnr f
176      ];
177    add_exprs env args args_regs f
178| St_seq s1 s2 ⇒
179    do f ← add_stmt env label_env s2 exits f;
180    add_stmt env label_env s1 exits f
181| St_ifthenelse _ _ e s1 s2 ⇒
182    let l_next ≝ f_entry f in
183    do f ← add_stmt env label_env s2 exits f;
184    let l2 ≝ f_entry f in
185    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
186    do f ← add_stmt env label_env s1 exits f;
187    do 〈r,f〉 ← choose_reg env ? e f;
188    do f ← add_fresh_to_graph (λl1. St_cond r l1 l2) f;
189    add_expr env ? e r f
190| St_loop s ⇒
191    do f ← add_loop_label_to_graph f;
192    let l_loop ≝ f_entry f in
193    do f ← add_stmt env label_env s exits f;
194    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
195| St_block s ⇒
196    add_stmt env label_env s ((f_entry f)::exits) f
197| St_exit n ⇒
198    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
199    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
200| St_switch sz sg e tab n ⇒
201    do 〈r,f〉 ← choose_reg env ? e f;
202    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
203    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
204    do f ← foldr ?? (λcs,f.
205      do f ← f;
206      let 〈i,n〉 ≝ cs in
207      do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);
208      do 〈br,f〉 ← fresh_reg … f (ASTint I8 Unsigned);
209      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
210      do f ← add_fresh_to_graph (St_cond br l_case) f;
211      do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;
212      add_fresh_to_graph (St_const cr (Ointconst ? i)) f) (OK ? f) tab;
213    add_expr env ? e r f
214| St_return opt_e ⇒
215    do f ← add_fresh_to_graph (λ_. St_return) f;
216    match opt_e with
217    [ None ⇒ OK ? f
218    | Some e ⇒
219        match f_result f with
220        [ None ⇒ Error ? (msg ReturnMismatch)
221        | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e (\fst r) f ]
222        ]
223    ]
224| St_label l s' ⇒
225    do f ← add_stmt env label_env s' exits f;
226    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
227    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
228| St_goto l ⇒
229    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
230    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
231| St_cost l s' ⇒
232    do f ← add_stmt env label_env s' exits f;
233    add_fresh_to_graph (St_cost l) f
234].
235[ @(λ_. St_skip l_next)
236| @(St_skip (f_entry f))
237| @(λ_. St_skip l)
238| @(λ_. St_skip l_default)
239| @(St_skip (f_entry f))
240| @(λ_.St_skip l')
241] qed.
242
243(* Get labels from a Cminor statement. *)
244let rec labels_of (s:stmt) : list ident ≝
245match s with
246[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
247| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
248| St_loop s ⇒ labels_of s
249| St_block s ⇒ labels_of s
250| St_label l s ⇒ l::(labels_of s)
251| St_cost _ s ⇒ labels_of s
252| _ ⇒ [ ]
253].
254
255definition c2ra_function (*: internal_function → internal_function*) ≝
256λf.
257let labgen0 ≝ new_universe LabelTag in
258let reggen0 ≝ new_universe RegisterTag in
259let cminor_labels ≝ labels_of (f_body f) in
260do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
261do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
262do 〈result, locals, reggen〉 ←
263  match f_return f with
264  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
265  | Some ty ⇒
266      do 〈r,gen〉 ← fresh … reggen2;
267      OK ? 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ];
268do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
269do 〈l,labgen〉 ← fresh … labgen1;
270let emptyfn ≝
271  mk_internal_function
272    labgen
273    reggen
274    result
275    params
276    locals
277    (f_stacksize f)
278    (add ?? (empty_map …) l St_return)
279    l
280    l in
281  add_stmt env label_env (f_body f) [ ] emptyfn
282.
283
284definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
285transform_partial_program ???
286  (transf_partial_fundef ?? c2ra_function).
287
288include "Cminor/initialisation.ma".
289
290definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
291λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.