source: src/Cminor/toRTLabs.ma @ 1212

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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

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