[1198] | 1 | include "Clight/Csyntax.ma". |
---|
| 2 | include "Clight/TypeComparison.ma". |
---|
| 3 | |
---|
| 4 | (* Attempt to remove unnecessary integer casts in Clight programs. |
---|
| 5 | |
---|
| 6 | This differs from the OCaml prototype by attempting to recursively determine |
---|
| 7 | whether subexpressions can be changed rather than using a fixed size pattern. |
---|
| 8 | As a result more complex expressions such as (char)((int)x + (int)y + (int)z) |
---|
| 9 | where x,y and z are chars can be simplified. |
---|
| 10 | |
---|
| 11 | A possible improvement that doesn't quite fit into this scheme would be to |
---|
| 12 | spot that casts can be removed in expressions like (int)x == (int)y where |
---|
| 13 | x and y have some smaller integer type. |
---|
| 14 | *) |
---|
| 15 | |
---|
| 16 | (* Attempt to squeeze integer constant into a given type. |
---|
| 17 | |
---|
| 18 | This might be too conservative --- if we're going to cast it anyway, can't |
---|
| 19 | I just ignore the fact that the integer doesn't fit? |
---|
| 20 | *) |
---|
| 21 | |
---|
| 22 | let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝ |
---|
| 23 | match n return λn. BitVector (n+S m) → option (BitVector (S m)) with |
---|
| 24 | [ O ⇒ λv. Some ? v |
---|
| 25 | | S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ? |
---|
| 26 | ] v. |
---|
| 27 | |
---|
| 28 | definition pred_bitsize_of_intsize : intsize → nat ≝ |
---|
| 29 | λsz. match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31 ]. |
---|
| 30 | |
---|
| 31 | definition signed : signedness → bool ≝ |
---|
| 32 | λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ]. |
---|
| 33 | |
---|
| 34 | let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝ |
---|
| 35 | let bit ≝ signed sg ∧ head' … i in |
---|
| 36 | match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz') |
---|
| 37 | return λn,m,x.BitVector (S n) → option (BitVector (S m)) with |
---|
| 38 | [ nat_lt _ _ ⇒ λi. None ? (* refuse to make constants larger *) |
---|
| 39 | | nat_eq _ ⇒ λi. Some ? i |
---|
| 40 | | nat_gt x y ⇒ λi. |
---|
| 41 | match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with |
---|
| 42 | [ Some i' ⇒ if signed sg' then if eq_b bit (head' … i') then Some ? i' else None ? else Some ? i' |
---|
| 43 | | None ⇒ None ? |
---|
| 44 | ] |
---|
| 45 | ] i. |
---|
| 46 | >(commutative_plus_faster (S x)) @refl |
---|
| 47 | qed. |
---|
| 48 | |
---|
| 49 | (* Compare integer types to decide if we can omit casts. *) |
---|
| 50 | |
---|
| 51 | inductive inttype_cmp : Type[0] ≝ |
---|
| 52 | | itc_le : inttype_cmp |
---|
| 53 | | itc_no : inttype_cmp. |
---|
| 54 | |
---|
| 55 | definition inttype_compare ≝ |
---|
| 56 | λt1,t2. |
---|
| 57 | match t1 with |
---|
| 58 | [ Tint sz sg ⇒ |
---|
| 59 | match t2 with |
---|
| 60 | [ Tint sz' sg' ⇒ |
---|
| 61 | match sz with |
---|
| 62 | [ I8 ⇒ itc_le |
---|
| 63 | | I16 ⇒ match sz' with [ I8 ⇒ itc_no | _ ⇒ itc_le ] |
---|
| 64 | | I32 ⇒ match sz' with [ I32 ⇒ itc_le | _ ⇒ itc_no ] |
---|
| 65 | ] |
---|
| 66 | | _ ⇒ itc_no |
---|
| 67 | ] |
---|
| 68 | | _ ⇒ itc_no |
---|
| 69 | ]. |
---|
| 70 | |
---|
| 71 | (* Operations where it is safe to use a smaller integer type on the assumption |
---|
| 72 | that we would cast it down afterwards anyway. *) |
---|
| 73 | |
---|
| 74 | definition binop_simplifiable ≝ |
---|
| 75 | λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ]. |
---|
| 76 | |
---|
| 77 | (* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and |
---|
| 78 | returns a flag stating whether the desired type was achieved and a simplified |
---|
| 79 | version of e. *) |
---|
| 80 | |
---|
| 81 | let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝ |
---|
| 82 | match e with |
---|
| 83 | [ Expr ed ty ⇒ |
---|
| 84 | match ed with |
---|
| 85 | [ Econst_int sz i ⇒ |
---|
| 86 | match ty with |
---|
| 87 | [ Tint _ sg ⇒ |
---|
| 88 | match ty' with |
---|
| 89 | [ Tint sz' sg' ⇒ |
---|
| 90 | match simplify_int sz sz' sg sg' i with |
---|
| 91 | [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉 |
---|
| 92 | | None ⇒ 〈false, e〉 |
---|
| 93 | ] |
---|
| 94 | | _ ⇒ 〈false, e〉 ] |
---|
| 95 | | _ ⇒ 〈false, e〉 ] |
---|
| 96 | | Ederef e1 ⇒ |
---|
| 97 | let ty1 ≝ typeof e1 in |
---|
| 98 | 〈type_eq ty ty',Expr (Ederef (\snd (simplify_expr e1 ty1))) ty〉 |
---|
| 99 | | Eaddrof e1 ⇒ |
---|
| 100 | let ty1 ≝ typeof e1 in |
---|
| 101 | 〈type_eq ty ty',Expr (Eaddrof (\snd (simplify_expr e1 ty1))) ty〉 |
---|
| 102 | | Eunop op e1 ⇒ |
---|
| 103 | let ty1 ≝ typeof e1 in |
---|
| 104 | 〈type_eq ty ty',Expr (Eunop op (\snd (simplify_expr e1 ty1))) ty〉 |
---|
| 105 | | Ebinop op e1 e2 ⇒ |
---|
| 106 | if binop_simplifiable op then |
---|
| 107 | let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty' in |
---|
| 108 | let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in |
---|
| 109 | if desired_type1 ∧ desired_type2 then |
---|
| 110 | 〈true, Expr (Ebinop op e1' e2') ty'〉 |
---|
| 111 | else |
---|
| 112 | let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in |
---|
| 113 | let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in |
---|
| 114 | 〈false, Expr (Ebinop op e1' e2') ty〉 |
---|
| 115 | else |
---|
| 116 | let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in |
---|
| 117 | let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in |
---|
| 118 | 〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉 |
---|
| 119 | | Ecast ty e1 ⇒ |
---|
| 120 | match inttype_compare ty' ty with |
---|
| 121 | [ itc_le ⇒ |
---|
| 122 | let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in |
---|
| 123 | if desired_type then 〈true, e1'〉 else |
---|
| 124 | let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in |
---|
| 125 | if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉 |
---|
| 126 | | itc_no ⇒ |
---|
| 127 | let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in |
---|
| 128 | if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉 |
---|
| 129 | ] |
---|
| 130 | | Econdition e1 e2 e3 ⇒ |
---|
| 131 | let 〈irrelevant, e1'〉 ≝ simplify_expr e1 (typeof e1) in (* TODO try to reduce size *) |
---|
| 132 | let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in |
---|
| 133 | let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty' in |
---|
| 134 | if desired_type2 ∧ desired_type3 then |
---|
| 135 | 〈true, Expr (Econdition e1' e2' e3') ty'〉 |
---|
| 136 | else |
---|
| 137 | let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in |
---|
| 138 | let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty in |
---|
| 139 | 〈false, Expr (Econdition e1' e2' e3') ty〉 |
---|
| 140 | (* Could probably do better with these, too. *) |
---|
| 141 | | Eandbool e1 e2 ⇒ |
---|
| 142 | let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in |
---|
| 143 | let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in |
---|
| 144 | 〈type_eq ty ty', Expr (Eandbool e1' e2') ty〉 |
---|
| 145 | | Eorbool e1 e2 ⇒ |
---|
| 146 | let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in |
---|
| 147 | let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in |
---|
| 148 | 〈type_eq ty ty', Expr (Eorbool e1' e2') ty〉 |
---|
| 149 | (* Could also improve Esizeof *) |
---|
| 150 | | Efield e1 f ⇒ |
---|
| 151 | let ty1 ≝ typeof e1 in |
---|
| 152 | 〈type_eq ty ty',Expr (Efield (\snd (simplify_expr e1 ty1)) f) ty〉 |
---|
| 153 | | Ecost l e1 ⇒ |
---|
| 154 | let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in |
---|
| 155 | 〈desired_type, Expr (Ecost l e1') (typeof e1')〉 |
---|
| 156 | | _ ⇒ 〈type_eq ty ty',e〉 |
---|
| 157 | ] |
---|
| 158 | ]. |
---|
| 159 | |
---|
| 160 | definition simplify_e ≝ λe. \snd (simplify_expr e (typeof e)). |
---|
| 161 | |
---|
| 162 | let rec simplify_statement (s:statement) : statement ≝ |
---|
| 163 | match s with |
---|
| 164 | [ Sskip ⇒ Sskip |
---|
| 165 | | Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2) |
---|
| 166 | | Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es) |
---|
| 167 | | Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2) |
---|
| 168 | | Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *) |
---|
| 169 | | Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) |
---|
| 170 | | Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) |
---|
| 171 | | Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *) |
---|
| 172 | | Sbreak ⇒ Sbreak |
---|
| 173 | | Scontinue ⇒ Scontinue |
---|
| 174 | | Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo) |
---|
| 175 | | Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls) |
---|
| 176 | | Slabel l s1 ⇒ Slabel l (simplify_statement s1) |
---|
| 177 | | Sgoto l ⇒ Sgoto l |
---|
| 178 | | Scost l s1 ⇒ Scost l (simplify_statement s1) |
---|
| 179 | ] |
---|
| 180 | and simplify_ls ls ≝ |
---|
| 181 | match ls with |
---|
| 182 | [ LSdefault s ⇒ LSdefault (simplify_statement s) |
---|
| 183 | | LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls') |
---|
| 184 | ]. |
---|
| 185 | |
---|
| 186 | definition simplify_function : function → function ≝ |
---|
| 187 | λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)). |
---|
| 188 | |
---|
| 189 | definition simplify_fundef : clight_fundef → clight_fundef ≝ |
---|
| 190 | λf. match f with |
---|
| 191 | [ CL_Internal f ⇒ CL_Internal (simplify_function f) |
---|
| 192 | | _ ⇒ f |
---|
| 193 | ]. |
---|
| 194 | |
---|
| 195 | definition simplify_program : clight_program → clight_program ≝ |
---|
[1224] | 196 | λp. transform_program … p simplify_fundef. |
---|