Changeset 1056 for src/Clight/label.ma
- Timestamp:
- Jul 5, 2011, 4:25:41 PM (10 years ago)
- File:
-
- 1 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 short-circuiting 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
Note: See TracChangeset
for help on using the changeset viewer.