source: src/Cminor/toRTLabs.ma @ 1070

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

Show that entry and exit labels are in the RTLabs graph.

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