[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 | |
---|
[780] | 62 | definition fresh_ptr_reg : internal_function → res (register × internal_function) ≝ |
---|
| 63 | λf. |
---|
| 64 | do 〈r,g〉 ← fresh … (f_reggen f); |
---|
| 65 | OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) |
---|
| 66 | (f_result f) (f_params f) (r::(f_locals f)) (r::(f_ptrs f)) |
---|
| 67 | (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. |
---|
| 68 | |
---|
| 69 | let rec expr_yields_pointer (e:expr) (ptrs:list ident) : bool ≝ |
---|
| 70 | match e with |
---|
| 71 | [ Id i ⇒ exists ? (eq_identifier ? i) ptrs |
---|
| 72 | | Cst c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ] |
---|
| 73 | | Op1 op e' ⇒ |
---|
| 74 | match op with |
---|
| 75 | [ Oid ⇒ expr_yields_pointer e' ptrs |
---|
| 76 | | Optrofint _ ⇒ true |
---|
| 77 | | _ ⇒ false |
---|
| 78 | ] |
---|
| 79 | | Op2 op e1 e2 ⇒ |
---|
| 80 | match op with |
---|
| 81 | [ Oaddp ⇒ true |
---|
| 82 | | Osubpi ⇒ true |
---|
| 83 | | _ ⇒ false |
---|
| 84 | ] |
---|
| 85 | | Mem q e' ⇒ |
---|
| 86 | match q with |
---|
| 87 | [ Mpointer _ ⇒ true |
---|
| 88 | | _ ⇒ false |
---|
| 89 | ] |
---|
| 90 | (* Both branches ought to be the same? *) |
---|
| 91 | | Cond e' e1 e2 ⇒ (expr_yields_pointer e1 ptrs) ∨ (expr_yields_pointer e2 ptrs) |
---|
| 92 | | Ecost _ e' ⇒ expr_yields_pointer e' ptrs |
---|
| 93 | ]. |
---|
| 94 | |
---|
| 95 | definition choose_reg : env → expr → list ident → internal_function → res (register × internal_function) ≝ |
---|
| 96 | λenv,e,ptrs,f. |
---|
[766] | 97 | match e with |
---|
| 98 | [ Id i ⇒ |
---|
| 99 | do r ← opt_to_res … (lookup … env i); |
---|
| 100 | OK ? 〈r, f〉 |
---|
[780] | 101 | | _ ⇒ |
---|
| 102 | if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f |
---|
[766] | 103 | ]. |
---|
| 104 | |
---|
[780] | 105 | definition choose_regs : env → list expr → list ident → internal_function → res (list register × internal_function) ≝ |
---|
| 106 | λenv,es,ptrs,f. |
---|
[766] | 107 | foldr ?? (λe,acc. do 〈rs,f〉 ← acc; |
---|
[780] | 108 | do 〈r,f'〉 ← choose_reg env e ptrs f; |
---|
[766] | 109 | OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. |
---|
| 110 | |
---|
[780] | 111 | let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝ |
---|
[766] | 112 | match e with |
---|
| 113 | [ Id i ⇒ |
---|
| 114 | do r ← opt_to_res … (lookup ?? env i); |
---|
| 115 | match register_eq r dst with |
---|
| 116 | [ inl _ ⇒ OK ? f |
---|
| 117 | | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f |
---|
| 118 | ] |
---|
| 119 | | Cst c ⇒ add_fresh_to_graph (St_const dst c) f |
---|
| 120 | | Op1 op e' ⇒ |
---|
[780] | 121 | do 〈r,f〉 ← choose_reg env e' ptrs f; |
---|
[767] | 122 | do f ← add_fresh_to_graph (St_op1 op dst r) f; |
---|
[780] | 123 | add_expr env e' r ptrs f |
---|
[766] | 124 | | Op2 op e1 e2 ⇒ |
---|
[780] | 125 | do 〈r1,f〉 ← choose_reg env e1 ptrs f; |
---|
| 126 | do 〈r2,f〉 ← choose_reg env e2 ptrs f; |
---|
[767] | 127 | do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f; |
---|
[780] | 128 | do f ← add_expr env e2 r2 ptrs f; |
---|
| 129 | add_expr env e1 r1 ptrs f |
---|
[766] | 130 | | Mem q e' ⇒ |
---|
[780] | 131 | add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e') |
---|
[766] | 132 | | Cond e' e1 e2 ⇒ |
---|
| 133 | let resume_at ≝ f_entry f in |
---|
[780] | 134 | do f ← add_expr env e2 dst ptrs f; |
---|
[767] | 135 | let lfalse ≝ f_entry f in |
---|
| 136 | do f ← add_fresh_to_graph (λ_.St_skip resume_at) f; |
---|
[780] | 137 | do f ← add_expr env e1 dst ptrs f; |
---|
| 138 | add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr env e') |
---|
[766] | 139 | | Ecost l e' ⇒ |
---|
[780] | 140 | do f ← add_expr env e' dst ptrs f; |
---|
[767] | 141 | add_fresh_to_graph (St_cost l) f |
---|
[766] | 142 | |
---|
| 143 | (* Ugh, the termination checker isn't smart enough to notice that calling |
---|
| 144 | add_expr with e is OK, so we take it partially applied and define a proper |
---|
[772] | 145 | add_<whatever> afterwards. *) |
---|
| 146 | ] |
---|
| 147 | and add_with_addressing_internal (env:env) (e:expr) |
---|
| 148 | (s:∀m:addressing. addr m → label → statement) |
---|
[780] | 149 | (ptrs:list ident) |
---|
[772] | 150 | (f:internal_function) |
---|
[780] | 151 | (termination_hack:register → list ident → internal_function → res internal_function) |
---|
[772] | 152 | on e : res internal_function ≝ |
---|
| 153 | let add_default : unit → res internal_function ≝ λ_. |
---|
[780] | 154 | do 〈r, f〉 ← choose_reg env e ptrs f; |
---|
[772] | 155 | do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f; |
---|
[780] | 156 | termination_hack r ptrs f |
---|
[772] | 157 | in |
---|
| 158 | match e with |
---|
| 159 | [ Cst c ⇒ |
---|
| 160 | match c with |
---|
| 161 | [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f |
---|
| 162 | | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f |
---|
| 163 | | _ ⇒ Error ? (* int and float constants are nonsense here *) |
---|
| 164 | ] |
---|
| 165 | | Op2 op e1 e2 ⇒ |
---|
| 166 | match op with |
---|
| 167 | [ Oaddp ⇒ |
---|
| 168 | let add_generic_addp : unit → res internal_function ≝ λ_. |
---|
[780] | 169 | do 〈r1, f〉 ← choose_reg env e1 ptrs f; |
---|
| 170 | do 〈r2, f〉 ← choose_reg env e2 ptrs f; |
---|
[772] | 171 | do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f; |
---|
[780] | 172 | do f ← add_expr env e2 r2 ptrs f; |
---|
| 173 | add_expr env e1 r1 ptrs f |
---|
[772] | 174 | in |
---|
| 175 | match e1 with |
---|
| 176 | [ Cst c ⇒ |
---|
| 177 | match c with |
---|
| 178 | [ Oaddrsymbol id i ⇒ |
---|
[780] | 179 | do 〈r, f〉 ← choose_reg env e ptrs f; |
---|
[772] | 180 | do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f; |
---|
[780] | 181 | add_expr env e2 r ptrs f |
---|
[772] | 182 | | _ ⇒ add_generic_addp it |
---|
| 183 | ] |
---|
| 184 | | _ ⇒ add_generic_addp it |
---|
| 185 | ] |
---|
| 186 | | _ ⇒ add_default it |
---|
| 187 | ] |
---|
| 188 | | _ ⇒ add_default it |
---|
| 189 | ] |
---|
| 190 | (* and again *) |
---|
[780] | 191 | and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function) |
---|
| 192 | (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝ |
---|
[766] | 193 | match e with |
---|
| 194 | [ Id i ⇒ |
---|
| 195 | do r ← opt_to_res … (lookup ?? env i); |
---|
| 196 | add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f |
---|
| 197 | | Cst c ⇒ |
---|
| 198 | add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f |
---|
| 199 | | Op1 op e' ⇒ |
---|
[780] | 200 | do 〈r,f〉 ← choose_reg env e' ptrs f; |
---|
[767] | 201 | do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f; |
---|
[780] | 202 | add_expr env e' r ptrs f |
---|
[766] | 203 | | Op2 op e1 e2 ⇒ |
---|
[780] | 204 | do 〈r1,f〉 ← choose_reg env e1 ptrs f; |
---|
| 205 | do 〈r2,f〉 ← choose_reg env e2 ptrs f; |
---|
[767] | 206 | do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f; |
---|
[780] | 207 | do f ← add_expr env e2 r2 ptrs f; |
---|
| 208 | add_expr env e1 r1 ptrs f |
---|
[766] | 209 | | _ ⇒ |
---|
[780] | 210 | do 〈r,f〉 ← choose_reg env e ptrs f; |
---|
[767] | 211 | do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f; |
---|
[780] | 212 | termination_hack_add_expr r ptrs f |
---|
[766] | 213 | ]. |
---|
| 214 | |
---|
[772] | 215 | (* See comment above. *) |
---|
| 216 | definition add_with_addressing ≝ |
---|
[780] | 217 | λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e). |
---|
[766] | 218 | definition add_branch ≝ |
---|
[780] | 219 | λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e). |
---|
[766] | 220 | |
---|
[780] | 221 | let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝ |
---|
[766] | 222 | match es with |
---|
| 223 | [ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ] |
---|
| 224 | | cons e et ⇒ |
---|
| 225 | match dsts with |
---|
| 226 | [ nil ⇒ Error ? |
---|
| 227 | | cons r rt ⇒ |
---|
[780] | 228 | do f ← add_exprs env et rt ptrs f; |
---|
| 229 | add_expr env e r ptrs f |
---|
[766] | 230 | ] |
---|
| 231 | ]. |
---|
| 232 | |
---|
[780] | 233 | let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (ptrs:list ident) (f:internal_function) on s : res internal_function ≝ |
---|
[766] | 234 | match s with |
---|
| 235 | [ St_skip ⇒ OK ? f |
---|
| 236 | | St_assign x e ⇒ |
---|
| 237 | do dst ← opt_to_res … (lookup ?? env x); |
---|
[780] | 238 | add_expr env e dst ptrs f |
---|
[766] | 239 | | St_store q e1 e2 ⇒ |
---|
[780] | 240 | do 〈val_reg, f〉 ← choose_reg env e2 ptrs f; |
---|
| 241 | do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f; |
---|
| 242 | add_expr env e2 val_reg ptrs f |
---|
[766] | 243 | | St_call return_opt_id e args sig ⇒ |
---|
| 244 | do return_opt_reg ← |
---|
| 245 | match return_opt_id with |
---|
| 246 | [ None ⇒ OK ? (None ?) |
---|
| 247 | | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r) |
---|
| 248 | ]; |
---|
[780] | 249 | do 〈args_regs, f〉 ← choose_regs env args ptrs f; |
---|
[767] | 250 | do f ← |
---|
[766] | 251 | match e with |
---|
[767] | 252 | [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f |
---|
[766] | 253 | | _ ⇒ |
---|
[780] | 254 | do 〈fnr, f〉 ← choose_reg env e ptrs f; |
---|
[767] | 255 | do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f; |
---|
[780] | 256 | add_expr env e fnr ptrs f |
---|
[766] | 257 | ]; |
---|
[780] | 258 | add_exprs env args args_regs ptrs f |
---|
[766] | 259 | | St_tailcall e args sig ⇒ |
---|
[780] | 260 | do 〈args_regs, f〉 ← choose_regs env args ptrs f; |
---|
[767] | 261 | do f ← |
---|
[766] | 262 | match e with |
---|
[767] | 263 | [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f |
---|
[766] | 264 | | _ ⇒ |
---|
[780] | 265 | do 〈fnr, f〉 ← choose_reg env e ptrs f; |
---|
[767] | 266 | do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f; |
---|
[780] | 267 | add_expr env e fnr ptrs f |
---|
[766] | 268 | ]; |
---|
[780] | 269 | add_exprs env args args_regs ptrs f |
---|
[766] | 270 | | St_seq s1 s2 ⇒ |
---|
[780] | 271 | do f ← add_stmt env label_env s2 exits ptrs f; |
---|
| 272 | add_stmt env label_env s1 exits ptrs f |
---|
[766] | 273 | | St_ifthenelse e s1 s2 ⇒ |
---|
[767] | 274 | let l_next ≝ f_entry f in |
---|
[780] | 275 | do f ← add_stmt env label_env s2 exits ptrs f; |
---|
[766] | 276 | let l2 ≝ f_entry f in |
---|
[767] | 277 | do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f; |
---|
[780] | 278 | do f ← add_stmt env label_env s1 exits ptrs f; |
---|
| 279 | add_branch env e (f_entry f) l2 ptrs f |
---|
[766] | 280 | | St_loop s ⇒ |
---|
[767] | 281 | do f ← add_loop_label_to_graph f; |
---|
| 282 | let l_loop ≝ f_entry f in |
---|
[780] | 283 | do f ← add_stmt env label_env s exits ptrs f; |
---|
[767] | 284 | OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) |
---|
[766] | 285 | | St_block s ⇒ |
---|
[780] | 286 | add_stmt env label_env s ((f_entry f)::exits) ptrs f |
---|
[766] | 287 | | St_exit n ⇒ |
---|
| 288 | do l ← opt_to_res … (nth_opt ? n exits); |
---|
| 289 | add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f |
---|
[771] | 290 | | St_switch e tab n ⇒ |
---|
[780] | 291 | do 〈r,f〉 ← choose_reg env e ptrs f; |
---|
[771] | 292 | do l_default ← opt_to_res … (nth_opt ? n exits); |
---|
| 293 | do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f; |
---|
| 294 | do f ← foldr ?? (λcs,f. |
---|
| 295 | do f ← f; |
---|
| 296 | let 〈i,n〉 ≝ cs in |
---|
| 297 | do 〈cr,f〉 ← fresh_reg … f; |
---|
| 298 | do l_case ← opt_to_res … (nth_opt ? n exits); |
---|
| 299 | do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f; |
---|
| 300 | add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab; |
---|
[780] | 301 | add_expr env e r ptrs f |
---|
[766] | 302 | | St_return opt_e ⇒ |
---|
[767] | 303 | do f ← add_fresh_to_graph (λ_. St_return) f; |
---|
[766] | 304 | match opt_e with |
---|
[767] | 305 | [ None ⇒ OK ? f |
---|
[766] | 306 | | Some e ⇒ |
---|
| 307 | match f_result f with |
---|
| 308 | [ None ⇒ Error ? |
---|
[780] | 309 | | Some r ⇒ add_expr env e r ptrs f |
---|
[766] | 310 | ] |
---|
| 311 | ] |
---|
| 312 | | St_label l s' ⇒ |
---|
[780] | 313 | do f ← add_stmt env label_env s' exits ptrs f; |
---|
[766] | 314 | do l' ← opt_to_res … (lookup ?? label_env l); |
---|
[767] | 315 | OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) |
---|
[766] | 316 | | St_goto l ⇒ |
---|
| 317 | do l' ← opt_to_res … (lookup ?? label_env l); |
---|
| 318 | add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f |
---|
| 319 | | St_cost l s' ⇒ |
---|
[780] | 320 | do f ← add_stmt env label_env s' exits ptrs f; |
---|
[767] | 321 | add_fresh_to_graph (St_cost l) f |
---|
[766] | 322 | ]. |
---|
[767] | 323 | [ @(λ_. St_skip l_next) |
---|
[766] | 324 | | @(St_skip (f_entry f)) |
---|
| 325 | | @(λ_. St_skip l) |
---|
[771] | 326 | | @(λ_. St_skip l_default) |
---|
[767] | 327 | | @(St_skip (f_entry f)) |
---|
[766] | 328 | | @(λ_.St_skip l') |
---|
| 329 | ] qed. |
---|
| 330 | |
---|
| 331 | (* Get labels from a Cminor statement. *) |
---|
| 332 | let rec labels_of (s:stmt) : list ident ≝ |
---|
| 333 | match s with |
---|
| 334 | [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
| 335 | | St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
| 336 | | St_loop s ⇒ labels_of s |
---|
| 337 | | St_block s ⇒ labels_of s |
---|
| 338 | | St_label l s ⇒ l::(labels_of s) |
---|
| 339 | | St_cost _ s ⇒ labels_of s |
---|
| 340 | | _ ⇒ [ ] |
---|
| 341 | ]. |
---|
| 342 | |
---|
[764] | 343 | definition c2ra_function (*: internal_function → internal_function*) ≝ |
---|
| 344 | λf. |
---|
[766] | 345 | let labgen0 ≝ new_universe LabelTag in |
---|
[764] | 346 | let reggen0 ≝ new_universe RegisterTag in |
---|
[766] | 347 | let cminor_labels ≝ labels_of (f_body f) in |
---|
[764] | 348 | do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f); |
---|
[766] | 349 | do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f); |
---|
| 350 | do 〈result, locals, reggen〉 ← |
---|
| 351 | match sig_res (f_sig f) with |
---|
| 352 | [ None ⇒ OK ? 〈None ?, locals0, reggen2〉 |
---|
| 353 | | Some _ ⇒ |
---|
| 354 | do 〈r,gen〉 ← fresh … reggen2; |
---|
| 355 | OK ? 〈Some ? r, r::locals0, gen〉 ]; |
---|
| 356 | do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f); |
---|
| 357 | do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels; |
---|
| 358 | do 〈l,labgen〉 ← fresh … labgen1; |
---|
| 359 | let emptyfn ≝ |
---|
| 360 | mk_internal_function |
---|
[764] | 361 | labgen |
---|
[766] | 362 | reggen |
---|
[764] | 363 | (f_sig f) |
---|
[766] | 364 | result |
---|
[764] | 365 | params |
---|
| 366 | locals |
---|
| 367 | ptrs |
---|
| 368 | (f_stacksize f) |
---|
[766] | 369 | (add ?? (empty_map …) l St_return) |
---|
| 370 | l |
---|
| 371 | l in |
---|
[780] | 372 | add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn |
---|
[766] | 373 | . |
---|
[764] | 374 | |
---|
| 375 | definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
| 376 | transform_partial_program ??? |
---|
| 377 | (transf_partial_fundef ?? c2ra_function). |
---|
[766] | 378 | |
---|
| 379 | include "Cminor/initialisation.ma". |
---|
| 380 | |
---|
| 381 | definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
| 382 | λp. let p' ≝ replace_init p in cminor_to_rtlabs p. |
---|