source: src/Cminor/toRTLabs.ma @ 1285

Last change on this file since 1285 was 1224, checked in by sacerdot, 9 years ago

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

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 ≝
298λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
299
300include "Cminor/initialisation.ma".
301
302definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
303λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.