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