[766] | 1 | include "utilities/lists.ma". |
---|
[764] | 2 | include "common/Globalenvs.ma". |
---|
| 3 | include "Cminor/syntax.ma". |
---|
| 4 | include "RTLabs/syntax.ma". |
---|
| 5 | |
---|
| 6 | definition env ≝ identifier_map SymbolTag register. |
---|
[766] | 7 | definition label_env ≝ identifier_map SymbolTag label. |
---|
[764] | 8 | definition 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 | |
---|
[766] | 15 | definition 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〉). |
---|
[764] | 21 | |
---|
[766] | 22 | (* Add a statement to the graph, *without* updating the entry label. *) |
---|
| 23 | definition 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). |
---|
[764] | 28 | |
---|
[766] | 29 | (* Add a statement to the graph, making it the entry label. *) |
---|
| 30 | definition 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). |
---|
[764] | 35 | |
---|
[766] | 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. *) |
---|
| 38 | definition 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. *) |
---|
| 48 | definition 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 | |
---|
| 55 | definition 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 | |
---|
| 62 | definition choose_reg : env → expr → internal_function → res (register × internal_function) ≝ |
---|
| 63 | λenv,e,f. |
---|
| 64 | match e with |
---|
| 65 | [ Id i ⇒ |
---|
| 66 | do r ← opt_to_res … (lookup … env i); |
---|
| 67 | OK ? 〈r, f〉 |
---|
| 68 | | _ ⇒ fresh_reg f (* FIXME: add to pointers list if necessary *) |
---|
| 69 | ]. |
---|
| 70 | |
---|
| 71 | definition choose_regs : env → list expr → internal_function → res (list register × internal_function) ≝ |
---|
| 72 | λenv,es,f. |
---|
| 73 | foldr ?? (λe,acc. do 〈rs,f〉 ← acc; |
---|
| 74 | do 〈r,f'〉 ← choose_reg env e f; |
---|
| 75 | OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. |
---|
| 76 | |
---|
| 77 | let rec add_expr (env:env) (e:expr) (dst:register) (f:internal_function) on e: res internal_function ≝ |
---|
| 78 | match e with |
---|
| 79 | [ Id i ⇒ |
---|
| 80 | do r ← opt_to_res … (lookup ?? env i); |
---|
| 81 | match register_eq r dst with |
---|
| 82 | [ inl _ ⇒ OK ? f |
---|
| 83 | | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f |
---|
| 84 | ] |
---|
| 85 | | Cst c ⇒ add_fresh_to_graph (St_const dst c) f |
---|
| 86 | | Op1 op e' ⇒ |
---|
[767] | 87 | do 〈r,f〉 ← choose_reg env e' f; |
---|
| 88 | do f ← add_fresh_to_graph (St_op1 op dst r) f; |
---|
| 89 | add_expr env e' r f |
---|
[766] | 90 | | Op2 op e1 e2 ⇒ |
---|
[767] | 91 | do 〈r1,f〉 ← choose_reg env e1 f; |
---|
| 92 | do 〈r2,f〉 ← choose_reg env e2 f; |
---|
| 93 | do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f; |
---|
| 94 | do f ← add_expr env e2 r2 f; |
---|
| 95 | add_expr env e1 r1 f |
---|
[766] | 96 | | Mem q e' ⇒ |
---|
| 97 | (* FIXME: inefficient - make proper use of addressing *) |
---|
[767] | 98 | do 〈r, f〉 ← choose_reg env e' f; |
---|
| 99 | do f ← add_fresh_to_graph (St_load q (Aindexed zero) [[ r ]] dst) f; |
---|
| 100 | add_expr env e' r f |
---|
[766] | 101 | | Cond e' e1 e2 ⇒ |
---|
| 102 | let resume_at ≝ f_entry f in |
---|
[767] | 103 | do f ← add_expr env e2 dst f; |
---|
| 104 | let lfalse ≝ f_entry f in |
---|
| 105 | do f ← add_fresh_to_graph (λ_.St_skip resume_at) f; |
---|
| 106 | do f ← add_expr env e1 dst f; |
---|
| 107 | add_branch_internal env e' (f_entry f) lfalse f (add_expr env e') |
---|
[766] | 108 | | Ecost l e' ⇒ |
---|
[767] | 109 | do f ← add_expr env e' dst f; |
---|
| 110 | add_fresh_to_graph (St_cost l) f |
---|
[766] | 111 | |
---|
| 112 | (* Ugh, the termination checker isn't smart enough to notice that calling |
---|
| 113 | add_expr with e is OK, so we take it partially applied and define a proper |
---|
| 114 | add_branch afterwards. *) |
---|
| 115 | ] and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (f:internal_function) |
---|
| 116 | (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝ |
---|
| 117 | match e with |
---|
| 118 | [ Id i ⇒ |
---|
| 119 | do r ← opt_to_res … (lookup ?? env i); |
---|
| 120 | add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f |
---|
| 121 | | Cst c ⇒ |
---|
| 122 | add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f |
---|
| 123 | | Op1 op e' ⇒ |
---|
[767] | 124 | do 〈r,f〉 ← choose_reg env e' f; |
---|
| 125 | do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f; |
---|
| 126 | add_expr env e' r f |
---|
[766] | 127 | | Op2 op e1 e2 ⇒ |
---|
[767] | 128 | do 〈r1,f〉 ← choose_reg env e1 f; |
---|
| 129 | do 〈r2,f〉 ← choose_reg env e2 f; |
---|
| 130 | do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f; |
---|
| 131 | do f ← add_expr env e2 r2 f; |
---|
| 132 | add_expr env e1 r1 f |
---|
[766] | 133 | | _ ⇒ |
---|
[767] | 134 | do 〈r,f〉 ← choose_reg env e f; |
---|
| 135 | do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f; |
---|
| 136 | termination_hack_add_expr r f |
---|
[766] | 137 | ]. |
---|
| 138 | |
---|
| 139 | (* See add_branch_internal above. *) |
---|
| 140 | definition add_branch ≝ |
---|
| 141 | λenv,e,ltrue,lfalse,f. add_branch_internal env e ltrue lfalse f (add_expr env e). |
---|
| 142 | |
---|
| 143 | let rec add_exprs (env:env) (es:list expr) (dsts:list register) (f:internal_function) on es: res internal_function ≝ |
---|
| 144 | match es with |
---|
| 145 | [ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ] |
---|
| 146 | | cons e et ⇒ |
---|
| 147 | match dsts with |
---|
| 148 | [ nil ⇒ Error ? |
---|
| 149 | | cons r rt ⇒ |
---|
[767] | 150 | do f ← add_exprs env et rt f; |
---|
| 151 | add_expr env e r f |
---|
[766] | 152 | ] |
---|
| 153 | ]. |
---|
| 154 | |
---|
| 155 | let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝ |
---|
| 156 | match s with |
---|
| 157 | [ St_skip ⇒ OK ? f |
---|
| 158 | | St_assign x e ⇒ |
---|
| 159 | do dst ← opt_to_res … (lookup ?? env x); |
---|
| 160 | add_expr env e dst f |
---|
| 161 | | St_store q e1 e2 ⇒ |
---|
| 162 | (* FIXME: inefficient - make proper use of addressing *) |
---|
[767] | 163 | do 〈addr_reg, f〉 ← choose_reg env e1 f; |
---|
| 164 | do 〈val_reg, f〉 ← choose_reg env e2 f; |
---|
| 165 | do f ← add_fresh_to_graph (St_store q (Aindexed zero) [[ addr_reg ]] val_reg) f; |
---|
| 166 | do f ← add_expr env e1 addr_reg f; |
---|
| 167 | add_expr env e2 val_reg f |
---|
[766] | 168 | | St_call return_opt_id e args sig ⇒ |
---|
| 169 | do return_opt_reg ← |
---|
| 170 | match return_opt_id with |
---|
| 171 | [ None ⇒ OK ? (None ?) |
---|
| 172 | | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r) |
---|
| 173 | ]; |
---|
[767] | 174 | do 〈args_regs, f〉 ← choose_regs env args f; |
---|
| 175 | do f ← |
---|
[766] | 176 | match e with |
---|
[767] | 177 | [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f |
---|
[766] | 178 | | _ ⇒ |
---|
[767] | 179 | do 〈fnr, f〉 ← choose_reg env e f; |
---|
| 180 | do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f; |
---|
| 181 | add_expr env e fnr f |
---|
[766] | 182 | ]; |
---|
[767] | 183 | add_exprs env args args_regs f |
---|
[766] | 184 | | St_tailcall e args sig ⇒ |
---|
[767] | 185 | do 〈args_regs, f〉 ← choose_regs env args f; |
---|
| 186 | do f ← |
---|
[766] | 187 | match e with |
---|
[767] | 188 | [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f |
---|
[766] | 189 | | _ ⇒ |
---|
[767] | 190 | do 〈fnr, f〉 ← choose_reg env e f; |
---|
| 191 | do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f; |
---|
| 192 | add_expr env e fnr f |
---|
[766] | 193 | ]; |
---|
[767] | 194 | add_exprs env args args_regs f |
---|
[766] | 195 | | St_seq s1 s2 ⇒ |
---|
[767] | 196 | do f ← add_stmt env label_env s2 exits f; |
---|
| 197 | add_stmt env label_env s1 exits f |
---|
[766] | 198 | | St_ifthenelse e s1 s2 ⇒ |
---|
[767] | 199 | let l_next ≝ f_entry f in |
---|
| 200 | do f ← add_stmt env label_env s2 exits f; |
---|
[766] | 201 | let l2 ≝ f_entry f in |
---|
[767] | 202 | do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f; |
---|
| 203 | do f ← add_stmt env label_env s1 exits f; |
---|
| 204 | add_branch env e (f_entry f) l2 f |
---|
[766] | 205 | | St_loop s ⇒ |
---|
[767] | 206 | do f ← add_loop_label_to_graph f; |
---|
| 207 | let l_loop ≝ f_entry f in |
---|
| 208 | do f ← add_stmt env label_env s exits f; |
---|
| 209 | OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) |
---|
[766] | 210 | | St_block s ⇒ |
---|
| 211 | add_stmt env label_env s ((f_entry f)::exits) f |
---|
| 212 | | St_exit n ⇒ |
---|
| 213 | do l ← opt_to_res … (nth_opt ? n exits); |
---|
| 214 | add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f |
---|
[771] | 215 | | St_switch e tab n ⇒ |
---|
| 216 | do 〈r,f〉 ← choose_reg env e f; |
---|
| 217 | do l_default ← opt_to_res … (nth_opt ? n exits); |
---|
| 218 | do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f; |
---|
| 219 | do f ← foldr ?? (λcs,f. |
---|
| 220 | do f ← f; |
---|
| 221 | let 〈i,n〉 ≝ cs in |
---|
| 222 | do 〈cr,f〉 ← fresh_reg … f; |
---|
| 223 | do l_case ← opt_to_res … (nth_opt ? n exits); |
---|
| 224 | do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f; |
---|
| 225 | add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab; |
---|
| 226 | add_expr env e r f |
---|
[766] | 227 | | St_return opt_e ⇒ |
---|
[767] | 228 | do f ← add_fresh_to_graph (λ_. St_return) f; |
---|
[766] | 229 | match opt_e with |
---|
[767] | 230 | [ None ⇒ OK ? f |
---|
[766] | 231 | | Some e ⇒ |
---|
| 232 | match f_result f with |
---|
| 233 | [ None ⇒ Error ? |
---|
| 234 | | Some r ⇒ add_expr env e r f |
---|
| 235 | ] |
---|
| 236 | ] |
---|
| 237 | | St_label l s' ⇒ |
---|
[767] | 238 | do f ← add_stmt env label_env s' exits f; |
---|
[766] | 239 | do l' ← opt_to_res … (lookup ?? label_env l); |
---|
[767] | 240 | OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) |
---|
[766] | 241 | | St_goto l ⇒ |
---|
| 242 | do l' ← opt_to_res … (lookup ?? label_env l); |
---|
| 243 | add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f |
---|
| 244 | | St_cost l s' ⇒ |
---|
[767] | 245 | do f ← add_stmt env label_env s' exits f; |
---|
| 246 | add_fresh_to_graph (St_cost l) f |
---|
[766] | 247 | | _ ⇒ Error ? (* XXX implement *) |
---|
| 248 | ]. |
---|
[767] | 249 | [ @(λ_. St_skip l_next) |
---|
[766] | 250 | | @(St_skip (f_entry f)) |
---|
| 251 | | @(λ_. St_skip l) |
---|
[771] | 252 | | @(λ_. St_skip l_default) |
---|
[767] | 253 | | @(St_skip (f_entry f)) |
---|
[766] | 254 | | @(λ_.St_skip l') |
---|
| 255 | ] qed. |
---|
| 256 | |
---|
| 257 | (* Get labels from a Cminor statement. *) |
---|
| 258 | let rec labels_of (s:stmt) : list ident ≝ |
---|
| 259 | match s with |
---|
| 260 | [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
| 261 | | St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
| 262 | | St_loop s ⇒ labels_of s |
---|
| 263 | | St_block s ⇒ labels_of s |
---|
| 264 | | St_label l s ⇒ l::(labels_of s) |
---|
| 265 | | St_cost _ s ⇒ labels_of s |
---|
| 266 | | _ ⇒ [ ] |
---|
| 267 | ]. |
---|
| 268 | |
---|
[764] | 269 | definition c2ra_function (*: internal_function → internal_function*) ≝ |
---|
| 270 | λf. |
---|
[766] | 271 | let labgen0 ≝ new_universe LabelTag in |
---|
[764] | 272 | let reggen0 ≝ new_universe RegisterTag in |
---|
[766] | 273 | let cminor_labels ≝ labels_of (f_body f) in |
---|
[764] | 274 | do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f); |
---|
[766] | 275 | do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f); |
---|
| 276 | do 〈result, locals, reggen〉 ← |
---|
| 277 | match sig_res (f_sig f) with |
---|
| 278 | [ None ⇒ OK ? 〈None ?, locals0, reggen2〉 |
---|
| 279 | | Some _ ⇒ |
---|
| 280 | do 〈r,gen〉 ← fresh … reggen2; |
---|
| 281 | OK ? 〈Some ? r, r::locals0, gen〉 ]; |
---|
| 282 | do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f); |
---|
| 283 | do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels; |
---|
| 284 | do 〈l,labgen〉 ← fresh … labgen1; |
---|
| 285 | let emptyfn ≝ |
---|
| 286 | mk_internal_function |
---|
[764] | 287 | labgen |
---|
[766] | 288 | reggen |
---|
[764] | 289 | (f_sig f) |
---|
[766] | 290 | result |
---|
[764] | 291 | params |
---|
| 292 | locals |
---|
| 293 | ptrs |
---|
| 294 | (f_stacksize f) |
---|
[766] | 295 | (add ?? (empty_map …) l St_return) |
---|
| 296 | l |
---|
| 297 | l in |
---|
| 298 | add_stmt env label_env (f_body f) [ ] emptyfn |
---|
| 299 | . |
---|
[764] | 300 | |
---|
| 301 | definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
| 302 | transform_partial_program ??? |
---|
| 303 | (transf_partial_fundef ?? c2ra_function). |
---|
[766] | 304 | |
---|
| 305 | include "Cminor/initialisation.ma". |
---|
| 306 | |
---|
| 307 | definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
| 308 | λp. let p' ≝ replace_init p in cminor_to_rtlabs p. |
---|