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 (typeof e1) in |
---|
117 | let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) 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 ≝ |
---|
196 | λp. transform_program … p simplify_fundef. |
---|