Changeset 1056
 Timestamp:
 Jul 5, 2011, 4:25:41 PM (9 years ago)
 Location:
 src
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/label.ma
r961 r1056 1 1 include "Clight/Csyntax.ma". 2 2 3 definition add_cost_before : statement → universe CostTag → res (statement × (universe CostTag)) ≝3 definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝ 4 4 λs,gen. 5 do 〈l,gen〉 ← fresh … gen;6 OK ?〈Scost l s, gen〉.5 let 〈l,gen〉 ≝ fresh … gen in 6 〈Scost l s, gen〉. 7 7 8 definition add_cost_after : statement → universe CostTag → res (statement × (universe CostTag)) ≝8 definition add_cost_after : statement → universe CostTag → statement × (universe CostTag) ≝ 9 9 λs,gen. 10 do 〈l,gen〉 ← fresh … gen;11 OK ?〈Ssequence s (Scost l Sskip), gen〉.10 let 〈l,gen〉 ≝ fresh … gen in 11 〈Ssequence s (Scost l Sskip), gen〉. 12 12 13 definition add_cost_expr : expr → universe CostTag → res (expr × (universe CostTag)) ≝13 definition add_cost_expr : expr → universe CostTag → expr × (universe CostTag) ≝ 14 14 λe,gen. 15 do 〈l,gen〉 ← fresh … gen;16 OK ?〈Expr (Ecost l e) (typeof e), gen〉.15 let 〈l,gen〉 ≝ fresh … gen in 16 〈Expr (Ecost l e) (typeof e), gen〉. 17 17 18 18 let rec label_expr (e:expr) (costgen:universe CostTag) 19 on e : res (expr × (universe CostTag)) ≝19 on e : expr × (universe CostTag) ≝ 20 20 match e with 21 [ Expr ed ty ⇒ do 〈ed,costgen〉 ← label_expr_descr ed costgen;22 OK ?〈Expr ed ty, costgen〉21 [ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen in 22 〈Expr ed ty, costgen〉 23 23 ] 24 24 and label_expr_descr (e:expr_descr) (costgen:universe CostTag) 25 on e : res (expr_descr × (universe CostTag)) ≝25 on e : expr_descr × (universe CostTag) ≝ 26 26 match e with 27 27 [ Ederef e' ⇒ 28 do 〈e',costgen〉 ← label_expr e' costgen;29 OK ?〈Ederef e', costgen〉28 let 〈e',costgen〉 ≝ label_expr e' costgen in 29 〈Ederef e', costgen〉 30 30  Eaddrof e' ⇒ 31 do 〈e',costgen〉 ← label_expr e' costgen;32 OK ?〈Eaddrof e', costgen〉31 let 〈e',costgen〉 ≝ label_expr e' costgen in 32 〈Eaddrof e', costgen〉 33 33  Eunop op e' ⇒ 34 do 〈e',costgen〉 ← label_expr e' costgen;35 OK ?〈Eunop op e', costgen〉34 let 〈e',costgen〉 ≝ label_expr e' costgen in 35 〈Eunop op e', costgen〉 36 36  Ebinop op e1 e2 ⇒ 37 do 〈e1,costgen〉 ← label_expr e1 costgen;38 do 〈e2,costgen〉 ← label_expr e2 costgen;39 OK ?〈Ebinop op e1 e2, costgen〉37 let 〈e1,costgen〉 ≝ label_expr e1 costgen in 38 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 39 〈Ebinop op e1 e2, costgen〉 40 40  Ecast ty e' ⇒ 41 do 〈e',costgen〉 ← label_expr e' costgen;42 OK ?〈Ecast ty e', costgen〉41 let 〈e',costgen〉 ≝ label_expr e' costgen in 42 〈Ecast ty e', costgen〉 43 43  Econdition e' e1 e2 ⇒ 44 do 〈e',costgen〉 ← label_expr e' costgen;45 do 〈e1,costgen〉 ← label_expr e1 costgen;46 do 〈e1,costgen〉 ← add_cost_expr e1 costgen;47 do 〈e2,costgen〉 ← label_expr e2 costgen;48 do 〈e2,costgen〉 ← add_cost_expr e2 costgen;49 OK ?〈Econdition e' e1 e2, costgen〉44 let 〈e',costgen〉 ≝ label_expr e' costgen in 45 let 〈e1,costgen〉 ≝ label_expr e1 costgen in 46 let 〈e1,costgen〉 ≝ add_cost_expr e1 costgen in 47 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 48 let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in 49 〈Econdition e' e1 e2, costgen〉 50 50 (* andbool and orbool are changed to conditionals to capture their 51 51 shortcircuiting cost difference *) 52 52  Eandbool e1 e2 ⇒ 53 do 〈e1,costgen〉 ← label_expr e1 costgen;54 do 〈e2,costgen〉 ← label_expr e2 costgen;55 do 〈e2,costgen〉 ← add_cost_expr e2 costgen;56 do 〈ef,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen;57 OK ?〈Econdition e1 e2 ef, costgen〉53 let 〈e1,costgen〉 ≝ label_expr e1 costgen in 54 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 55 let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in 56 let 〈ef,costgen〉 ≝ add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen in 57 〈Econdition e1 e2 ef, costgen〉 58 58  Eorbool e1 e2 ⇒ 59 do 〈e1,costgen〉 ← label_expr e1 costgen;60 do 〈et,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen;61 do 〈e2,costgen〉 ← label_expr e2 costgen;62 do 〈e2,costgen〉 ← add_cost_expr e2 costgen;63 OK ?〈Econdition e1 et e2, costgen〉59 let 〈e1,costgen〉 ≝ label_expr e1 costgen in 60 let 〈et,costgen〉 ≝ add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen in 61 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 62 let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in 63 〈Econdition e1 et e2, costgen〉 64 64 65 65  Efield e' id ⇒ 66 do 〈e',costgen〉 ← label_expr e' costgen;67 OK ?〈Efield e' id, costgen〉66 let 〈e',costgen〉 ≝ label_expr e' costgen in 67 〈Efield e' id, costgen〉 68 68 (* The prototype asserts on preexisting cost labels, but I'd quite like to 69 69 keep them. *) 70 70  Ecost l e' ⇒ 71 do 〈e',costgen〉 ← label_expr e' costgen;72 OK ?〈Ecost l e', costgen〉71 let 〈e',costgen〉 ≝ label_expr e' costgen in 72 〈Ecost l e', costgen〉 73 73 74 74 (* The remaining expressions don't have subexpressions. *) 75  _ ⇒ OK ?〈e,costgen〉75  _ ⇒ 〈e,costgen〉 76 76 ]. 77 77 78 78 let rec label_exprs (l:list expr) (costgen:universe CostTag) 79 on l : res (list expr × (universe CostTag)) ≝79 on l : list expr × (universe CostTag) ≝ 80 80 match l with 81 [ nil ⇒ OK ?〈nil ?,costgen〉81 [ nil ⇒ 〈nil ?,costgen〉 82 82  cons e es ⇒ 83 do 〈e,costgen〉 ← label_expr e costgen;84 do 〈es,costgen〉 ← label_exprs es costgen;85 OK ?〈e::es,costgen〉83 let 〈e,costgen〉 ≝ label_expr e costgen in 84 let 〈es,costgen〉 ≝ label_exprs es costgen in 85 〈e::es,costgen〉 86 86 ]. 87 87 88 88 definition label_opt_expr ≝ 89 89 λoe,costgen. match oe with 90 [ None ⇒ OK ?〈None ?, costgen〉91  Some e ⇒ do 〈e,costgen〉 ← label_expr e costgen; OK ?〈Some ? e,costgen〉90 [ None ⇒ 〈None ?, costgen〉 91  Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉 92 92 ]. 93 93 94 94 95 95 let rec label_statement (s:statement) (costgen:universe CostTag) 96 on s : res (statement × (universe CostTag)) ≝96 on s : statement × (universe CostTag) ≝ 97 97 match s with 98 [ Sskip ⇒ OK ?〈Sskip,costgen〉98 [ Sskip ⇒ 〈Sskip,costgen〉 99 99  Sassign e1 e2 ⇒ 100 do 〈e1,costgen〉 ← label_expr e1 costgen;101 do 〈e2,costgen〉 ← label_expr e2 costgen;102 OK ?〈Sassign e1 e2, costgen〉100 let 〈e1,costgen〉 ≝ label_expr e1 costgen in 101 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 102 〈Sassign e1 e2, costgen〉 103 103  Scall e_ret e_fn e_args ⇒ 104 do 〈e_ret,costgen〉 ← label_opt_expr e_ret costgen;105 do 〈e_fn,costgen〉 ← label_expr e_fn costgen;106 do 〈e_args,costgen〉 ← label_exprs e_args costgen;107 OK ?〈Scall e_ret e_fn e_args, costgen〉104 let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in 105 let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in 106 let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in 107 〈Scall e_ret e_fn e_args, costgen〉 108 108  Ssequence s1 s2 ⇒ 109 do 〈s1,costgen〉 ← label_statement s1 costgen;110 do 〈s2,costgen〉 ← label_statement s2 costgen;111 OK ?〈Ssequence s1 s2, costgen〉109 let 〈s1,costgen〉 ≝ label_statement s1 costgen in 110 let 〈s2,costgen〉 ≝ label_statement s2 costgen in 111 〈Ssequence s1 s2, costgen〉 112 112  Sifthenelse e s1 s2 ⇒ 113 do 〈e,costgen〉 ← label_expr e costgen;114 do 〈s1,costgen〉 ← label_statement s1 costgen;115 do 〈s1,costgen〉 ← add_cost_before s1 costgen;116 do 〈s2,costgen〉 ← label_statement s2 costgen;117 do 〈s2,costgen〉 ← add_cost_before s2 costgen;118 OK ?〈Sifthenelse e s1 s2, costgen〉113 let 〈e,costgen〉 ≝ label_expr e costgen in 114 let 〈s1,costgen〉 ≝ label_statement s1 costgen in 115 let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in 116 let 〈s2,costgen〉 ≝ label_statement s2 costgen in 117 let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in 118 〈Sifthenelse e s1 s2, costgen〉 119 119  Swhile e s' ⇒ 120 do 〈e,costgen〉 ← label_expr e costgen;121 do 〈s',costgen〉 ← label_statement s' costgen;122 do 〈s',costgen〉 ← add_cost_before s' costgen;123 do 〈s,costgen〉 ← add_cost_after (Swhile e s') costgen;124 OK ?〈s,costgen〉120 let 〈e,costgen〉 ≝ label_expr e costgen in 121 let 〈s',costgen〉 ≝ label_statement s' costgen in 122 let 〈s',costgen〉 ≝ add_cost_before s' costgen in 123 let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in 124 〈s,costgen〉 125 125  Sdowhile e s' ⇒ 126 do 〈e,costgen〉 ← label_expr e costgen;127 do 〈s',costgen〉 ← label_statement s' costgen;128 do 〈s',costgen〉 ← add_cost_before s' costgen;129 do 〈s,costgen〉 ← add_cost_after (Sdowhile e s') costgen;130 OK ?〈s,costgen〉126 let 〈e,costgen〉 ≝ label_expr e costgen in 127 let 〈s',costgen〉 ≝ label_statement s' costgen in 128 let 〈s',costgen〉 ≝ add_cost_before s' costgen in 129 let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in 130 〈s,costgen〉 131 131  Sfor s1 e s2 s3 ⇒ 132 do 〈e,costgen〉 ← label_expr e costgen;133 do 〈s1,costgen〉 ← label_statement s1 costgen;134 do 〈s2,costgen〉 ← label_statement s2 costgen;135 do 〈s3,costgen〉 ← label_statement s3 costgen;136 do 〈s3,costgen〉 ← add_cost_before s3 costgen;137 do 〈s,costgen〉 ← add_cost_after (Sfor s1 e s2 s3) costgen;138 OK ?〈s,costgen〉139  Sbreak ⇒ OK ?〈Sbreak,costgen〉140  Scontinue ⇒ OK ?〈Scontinue,costgen〉132 let 〈e,costgen〉 ≝ label_expr e costgen in 133 let 〈s1,costgen〉 ≝ label_statement s1 costgen in 134 let 〈s2,costgen〉 ≝ label_statement s2 costgen in 135 let 〈s3,costgen〉 ≝ label_statement s3 costgen in 136 let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in 137 let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in 138 〈s,costgen〉 139  Sbreak ⇒ 〈Sbreak,costgen〉 140  Scontinue ⇒ 〈Scontinue,costgen〉 141 141  Sreturn opt_e ⇒ 142 do 〈opt_e,costgen〉 ← label_opt_expr opt_e costgen;143 OK ?〈Sreturn opt_e,costgen〉142 let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in 143 〈Sreturn opt_e,costgen〉 144 144  Sswitch e ls ⇒ 145 do 〈e,costgen〉 ← label_expr e costgen;146 do 〈ls,costgen〉 ← label_lstatements ls costgen;147 OK ?〈Sswitch e ls, costgen〉145 let 〈e,costgen〉 ≝ label_expr e costgen in 146 let 〈ls,costgen〉 ≝ label_lstatements ls costgen in 147 〈Sswitch e ls, costgen〉 148 148  Slabel l s' ⇒ 149 do 〈s',costgen〉 ← label_statement s' costgen;150 do 〈s',costgen〉 ← add_cost_before s' costgen;151 OK ?〈Slabel l s', costgen〉152  Sgoto l ⇒ OK ?〈Sgoto l, costgen〉149 let 〈s',costgen〉 ≝ label_statement s' costgen in 150 let 〈s',costgen〉 ≝ add_cost_before s' costgen in 151 〈Slabel l s', costgen〉 152  Sgoto l ⇒ 〈Sgoto l, costgen〉 153 153 154 154 (* The prototype asserts on preexisting cost labels, but I'd quite like to 155 155 keep them. *) 156 156  Scost l s' ⇒ 157 do 〈s',costgen〉 ← label_statement s' costgen;158 OK ?〈Scost l s', costgen〉157 let 〈s',costgen〉 ≝ label_statement s' costgen in 158 〈Scost l s', costgen〉 159 159 ] 160 160 and label_lstatements (ls:labeled_statements) (costgen:universe CostTag) 161 on ls : res (labeled_statements × (universe CostTag)) ≝161 on ls : labeled_statements × (universe CostTag) ≝ 162 162 match ls with 163 163 [ LSdefault s ⇒ 164 do 〈s,costgen〉 ← label_statement s costgen;165 do 〈s,costgen〉 ← add_cost_before s costgen;166 OK ?〈LSdefault s, costgen〉164 let 〈s,costgen〉 ≝ label_statement s costgen in 165 let 〈s,costgen〉 ≝ add_cost_before s costgen in 166 〈LSdefault s, costgen〉 167 167  LScase sz i s ls' ⇒ 168 do 〈s,costgen〉 ← label_statement s costgen;169 do 〈s,costgen〉 ← add_cost_before s costgen;170 do 〈ls',costgen〉 ← label_lstatements ls' costgen;171 OK ?〈LScase sz i s ls', costgen〉168 let 〈s,costgen〉 ≝ label_statement s costgen in 169 let 〈s,costgen〉 ≝ add_cost_before s costgen in 170 let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in 171 〈LScase sz i s ls', costgen〉 172 172 ]. 173 173 … … 175 175 λf. 176 176 let costgen ≝ new_universe CostTag in 177 do 〈body,costgen〉 ← label_statement (fn_body f) costgen; 178 do 〈body,costgen〉 ← add_cost_before body costgen; 177 let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in 178 let 〈body,costgen〉 ≝ add_cost_before body costgen in 179 do u ← check_universe_ok ? costgen; 179 180 OK ? (mk_function (fn_return f) (fn_params f) (fn_vars f) body). 180 181 
src/Cminor/toRTLabs.ma
r961 r1056 6 6 definition env ≝ identifier_map SymbolTag register. 7 7 definition label_env ≝ identifier_map SymbolTag label. 8 definition populate_env : env → universe RegisterTag → list (ident × typ) → res (list (register×typ) × env × (universe RegisterTag)) ≝8 definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝ 9 9 λen,gen. foldr ?? 10 10 (λidt,rsengen. 11 11 let 〈id,ty〉 ≝ idt in 12 do 〈rs,en,gen〉 ← rsengen;13 do 〈r,gen'〉 ← fresh … gen;14 OK ? 〈〈r,ty〉::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).15 16 definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝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 16 definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝ 17 17 λen,gen. foldr ?? 18 18 (λid,engen. 19 do 〈en,gen〉 ← engen;20 do 〈r,gen'〉 ← fresh … gen;21 OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉).19 let 〈en,gen〉 ≝ engen in 20 let 〈r,gen'〉 ≝ fresh … gen in 21 〈add ?? en id r, gen'〉) 〈en, gen〉. 22 22 23 23 (* Add a statement to the graph, *without* updating the entry label. *) … … 37 37 (* Add a statement with a fresh label to the start of the function. The 38 38 statement is parametrised by the *next* instruction's label. *) 39 definition add_fresh_to_graph : (label → statement) → internal_function → resinternal_function ≝39 definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝ 40 40 λs,f. 41 do 〈l,g〉 ← fresh … (f_labgen f);41 let 〈l,g〉 ≝ fresh … (f_labgen f) in 42 42 let s' ≝ s (f_entry f) in 43 OK ?(mk_internal_function g (f_reggen f)43 (mk_internal_function g (f_reggen f) 44 44 (f_result f) (f_params f) (f_locals f) 45 45 (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)). … … 47 47 (* Generate a fresh label and use it as a dangling entry point, to be filled in 48 48 later with the loop head. *) 49 definition add_loop_label_to_graph : internal_function → resinternal_function ≝49 definition add_loop_label_to_graph : internal_function → internal_function ≝ 50 50 λf. 51 do 〈l,g〉 ← fresh … (f_labgen f);52 OK ?(mk_internal_function g (f_reggen f)51 let 〈l,g〉 ≝ fresh … (f_labgen f) in 52 (mk_internal_function g (f_reggen f) 53 53 (f_result f) (f_params f) (f_locals f) 54 54 (f_stacksize f) (f_graph f) l (f_exit f)). 55 55 56 definition fresh_reg : internal_function → typ → re s (register × internal_function)≝56 definition fresh_reg : internal_function → typ → register × internal_function ≝ 57 57 λf,ty. 58 do 〈r,g〉 ← fresh … (f_reggen f);59 OK ?〈r, mk_internal_function (f_labgen f) g58 let 〈r,g〉 ≝ fresh … (f_reggen f) in 59 〈r, mk_internal_function (f_labgen f) g 60 60 (f_result f) (f_params f) (〈r,ty〉::(f_locals f)) 61 61 (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. … … 70 70 OK ? 〈r, f〉 71 71  _ ⇒ 72 fresh_reg f ty72 OK ? (fresh_reg f ty) 73 73 ]. 74 74 … … 88 88 match register_eq r dst with 89 89 [ inl _ ⇒ OK ? f 90  inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f90  inr _ ⇒ OK ? (add_fresh_to_graph (St_op1 Oid dst r) f) 91 91 ] 92  Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f92  Cst _ c ⇒ OK ? (add_fresh_to_graph (St_const dst c) f) 93 93  Op1 _ _ op e' ⇒ 94 94 do 〈r,f〉 ← choose_reg env ? e' f; 95 do f ← add_fresh_to_graph (St_op1 op dst r) f;95 let f ≝ add_fresh_to_graph (St_op1 op dst r) f in 96 96 add_expr env ? e' r f 97 97  Op2 _ _ _ op e1 e2 ⇒ 98 98 do 〈r1,f〉 ← choose_reg env ? e1 f; 99 99 do 〈r2,f〉 ← choose_reg env ? e2 f; 100 do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;100 let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in 101 101 do f ← add_expr env ? e2 r2 f; 102 102 add_expr env ? e1 r1 f 103 103  Mem _ _ q e' ⇒ 104 104 do 〈r,f〉 ← choose_reg env ? e' f; 105 do f ← add_fresh_to_graph (St_load q r dst) f;105 let f ≝ add_fresh_to_graph (St_load q r dst) f in 106 106 add_expr env ? e' r f 107 107  Cond _ _ _ e' e1 e2 ⇒ … … 109 109 do f ← add_expr env ? e2 dst f; 110 110 let lfalse ≝ f_entry f in 111 do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;111 let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in 112 112 do f ← add_expr env ? e1 dst f; 113 113 do 〈r,f〉 ← choose_reg env ? e' f; 114 do f ← add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f;114 let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in 115 115 add_expr env ? e' r f 116 116  Ecost _ l e' ⇒ 117 117 do f ← add_expr env ? e' dst f; 118 add_fresh_to_graph (St_cost l) f118 OK ? (add_fresh_to_graph (St_cost l) f) 119 119 ]. 120 120 … … 146 146 do 〈val_reg, f〉 ← choose_reg env ? e2 f; 147 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;148 let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in 149 149 do f ← add_expr env ? e1 addr_reg f; 150 150 add_expr env ? e2 val_reg f … … 158 158 do f ← 159 159 match e with 160 [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f160 [ Id _ id ⇒ OK ? (add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f) 161 161  _ ⇒ 162 162 do 〈fnr, f〉 ← choose_reg env ? e f; 163 do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;163 let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in 164 164 add_expr env ? e fnr f 165 165 ]; … … 169 169 do f ← 170 170 match e with 171 [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f171 [ Id _ id ⇒ OK ? (add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f) 172 172  _ ⇒ 173 173 do 〈fnr, f〉 ← choose_reg env ? e f; 174 do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;174 let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in 175 175 add_expr env ? e fnr f 176 176 ]; … … 183 183 do f ← add_stmt env label_env s2 exits f; 184 184 let l2 ≝ f_entry f in 185 do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;185 let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in 186 186 do f ← add_stmt env label_env s1 exits f; 187 187 do 〈r,f〉 ← choose_reg env ? e f; 188 do f ← add_fresh_to_graph (λl1. St_cond r l1 l2) f;188 let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in 189 189 add_expr env ? e r f 190 190  St_loop s ⇒ 191 do f ← add_loop_label_to_graph f;191 let f ≝ add_loop_label_to_graph f in 192 192 let l_loop ≝ f_entry f in 193 193 do f ← add_stmt env label_env s exits f; … … 197 197  St_exit n ⇒ 198 198 do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 199 add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f199 OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f) 200 200  St_switch sz sg e tab n ⇒ 201 201 do 〈r,f〉 ← choose_reg env ? e f; 202 202 do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 203 do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;203 let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in 204 204 do f ← foldr ?? (λcs,f. 205 205 do f ← f; 206 206 let 〈i,n〉 ≝ cs in 207 do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);208 do 〈br,f〉 ← fresh_reg … f (ASTint I8 Unsigned);207 let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in 208 let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in 209 209 do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 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;212 add_fresh_to_graph (St_const cr (Ointconst ? i)) f) (OK ? f) tab;210 let f ≝ add_fresh_to_graph (St_cond br l_case) f in 211 let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in 212 OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab; 213 213 add_expr env ? e r f 214 214  St_return opt_e ⇒ 215 do f ← add_fresh_to_graph (λ_. St_return) f;215 let f ≝ add_fresh_to_graph (λ_. St_return) f in 216 216 match opt_e with 217 217 [ None ⇒ OK ? f … … 228 228  St_goto l ⇒ 229 229 do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); 230 add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f230 OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f) 231 231  St_cost l s' ⇒ 232 232 do f ← add_stmt env label_env s' exits f; 233 add_fresh_to_graph (St_cost l) f233 OK ? (add_fresh_to_graph (St_cost l) f) 234 234 ]. 235 235 [ @(λ_. St_skip l_next) … … 258 258 let reggen0 ≝ new_universe RegisterTag in 259 259 let cminor_labels ≝ labels_of (f_body f) in 260 do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f); 261 do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f); 262 do 〈result, locals, reggen〉 ← 260 let 〈params, env1, reggen1〉 ≝ populate_env (empty_map …) reggen0 (f_params f) in 261 let 〈locals0, env, reggen2〉 ≝ populate_env env1 reggen1 (f_vars f) in 262 let 〈result, locals, reggen〉 ≝ 263 263 match f_return f with 264 [ None ⇒ OK ?〈None ?, locals0, reggen2〉264 [ None ⇒ 〈None ?, locals0, reggen2〉 265 265  Some ty ⇒ 266 do 〈r,gen〉 ← fresh … reggen2;267 OK ? 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ];268 do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels; 269 do 〈l,labgen〉 ← fresh … labgen1; 266 let 〈r,gen〉 ≝ fresh … reggen2 in 267 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in 268 let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in 269 let 〈l,labgen〉 ≝ fresh … labgen1 in 270 270 let emptyfn ≝ 271 271 mk_internal_function … … 279 279 l 280 280 l in 281 add_stmt env label_env (f_body f) [ ] emptyfn 281 do f ← add_stmt env label_env (f_body f) [ ] emptyfn; 282 do u1 ← check_universe_ok ? (f_labgen f); 283 do u2 ← check_universe_ok ? (f_reggen f); 284 OK ? f 282 285 . 283 286 
src/RTLabs/import.ma
r898 r1056 2 2 include "RTLabs/semantics.ma". 3 3 4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝ 5 5 match n with 6 [ O ⇒ OK ?〈[[ ]], g〉7  S m ⇒ do 〈ls, g'〉 ← n_idents m tag g;8 do 〈l, g''〉 ← fresh ? g';9 OK ?〈l:::ls, g''〉6 [ O ⇒ 〈[[ ]], g〉 7  S m ⇒ let 〈ls, g'〉 ≝ n_idents m tag g in 8 let 〈l, g''〉 ≝ fresh ? g' in 9 〈l:::ls, g''〉 10 10 ]. 11 11 … … 24 24 definition make_register : 25 25 (pre_register → option register) → pre_register → universe RegisterTag → 26 res ((nat → option register) × (universe RegisterTag) × register)≝26 (nat → option register) × (universe RegisterTag) × register ≝ 27 27 λm,reg,g. 28 28 match m reg with 29 [ Some r' ⇒ OK ?〈〈m,g〉,r'〉30  None ⇒ do 〈r',g'〉 ← fresh ? g;31 OK ?〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉29 [ Some r' ⇒ 〈〈m,g〉,r'〉 30  None ⇒ let 〈r',g'〉 ≝ fresh ? g in 31 〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉 32 32 ] 33 33 . … … 35 35 definition make_registers_list : 36 36 (nat → option register) → list (pre_register × typ) → universe RegisterTag → 37 res ((nat → option register) × (universe RegisterTag) × (list (register×typ))) ≝37 (nat → option register) × (universe RegisterTag) × (list (register×typ)) ≝ 38 38 λm,lrs,g. 39 foldr ?? (λrst,acc. do 〈acc',l〉 ← acc;40 let 〈rs,ty〉 ≝ rst in41 let 〈m,g〉 ≝ acc' in42 do 〈mg,rs'〉 ← make_register m rs g;43 OK ? 〈mg,〈rs',ty〉::l〉) (OK ? 〈〈m,g〉,[ ]〉)lrs.39 foldr ?? (λrst,acc. let 〈acc',l〉 ≝ acc in 40 let 〈rs,ty〉 ≝ rst in 41 let 〈m,g〉 ≝ acc' in 42 let 〈mg,rs'〉 ≝ make_register m rs g in 43 〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs. 44 44 45 45 axiom MissingRegister : String. 46 46 axiom MissingLabel : String. 47 47 48 (* Doesn't check for identifier overflow, but don't really need to care here. *) 48 49 definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝ 49 50 λpre_f. 50 51 let rgen0 ≝ new_universe RegisterTag in 51 do 〈rmapgen1, result〉 ←match pf_result pre_f with52 [ None ⇒ OK ?〈〈λ_.None ?, rgen0〉, None ?〉53  Some rt ⇒ do 〈x,y〉 ← make_register (λ_.None ?) (\fst rt) rgen0; OK ?〈x,Some ? 〈y,\snd rt〉〉54 ];52 let 〈rmapgen1, result〉 ≝ match pf_result pre_f with 53 [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉 54  Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉 55 ] in 55 56 let 〈rmap1, rgen1〉 ≝ rmapgen1 in 56 do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;57 let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in 57 58 let 〈rmap2, rgen2〉 ≝ rmapgen2 in 58 do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;59 let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in 59 60 let 〈rmap3, rgen3〉 ≝ rmapgen3 in 60 61 let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in 61 62 let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in 62 do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);63 let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in 63 64 let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in 64 65 do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0. 
src/RTLabs/syntax.ma
r1051 r1056 13 13  St_skip : label → statement 14 14  St_cost : costlabel → label → statement 15  St_const : register → c ast → label → statement15  St_const : register → constant → label → statement 16 16  St_op1 : unary_operation → register → register → label → statement 17 17  St_op2 : binary_operation → register → register → register → label → statement 
src/common/Identifiers.ma
r1055 r1056 22 22 λtag. mk_universe tag (zero ?) false. 23 23 24 definition fresh ≝ 24 (* Fresh identifier generation uses delayed overflow checking. To make sure 25 that the identifiers really were fresh, use the check_universe_ok function 26 below afterwards. *) 27 definition fresh : ∀tag:String. universe tag → identifier tag × (universe tag) ≝ 25 28 λtag. 26 29 λuniv: universe tag. … … 32 35 // 33 36 qed. 37 38 axiom TooManyIdentifiers : String. 39 40 definition check_universe_ok : ∀tag:String. universe tag → res unit ≝ 41 λtag, univ. 42 if counter_overflow ? univ 43 then Error ? (msg TooManyIdentifiers) 44 else OK ? it. 34 45 35 46 definition eq_identifier ≝
Note: See TracChangeset
for help on using the changeset viewer.