# source:Deliverables/D3.3/id-lookup-branch/Clight/SimplifyCasts.ma@2588

Last change on this file since 2588 was 1311, checked in by campbell, 9 years ago

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

File size: 7.9 KB
Line
1include "Clight/Csyntax.ma".
2include "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
22let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝
23match 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
28definition pred_bitsize_of_intsize : intsize → nat ≝
29λsz. match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31 ].
30
31definition signed : signedness → bool ≝
32λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ].
33
34let 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
47qed.
48
49(* Compare integer types to decide if we can omit casts. *)
50
51inductive inttype_cmp : Type[0] ≝
52| itc_le : inttype_cmp
53| itc_no : inttype_cmp.
54
55definition inttype_compare ≝
56λt1,t2.
57match 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
74definition 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
81let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝
82match 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〉
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
160definition simplify_e ≝ λe. \snd (simplify_expr e (typeof e)).
161
162let rec simplify_statement (s:statement) : statement ≝
163match 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]
180and simplify_ls ls ≝
181match 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
186definition simplify_function : function → function ≝
187λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)).
188
189definition simplify_fundef : clight_fundef → clight_fundef ≝
190λf. match f with
191  [ CL_Internal f ⇒ CL_Internal (simplify_function f)
192  | _ ⇒ f
193  ].
194
195definition simplify_program : clight_program → clight_program ≝
196λp. transform_program … p simplify_fundef.
Note: See TracBrowser for help on using the repository browser.