1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* Evaluation of compile-time constants *)
22 (* Extra arith on int64 *)
24 external int64_unsigned_to_float: int64 -> float
25 = "cparser_int64_unsigned_to_float"
26 external int64_unsigned_div: int64 -> int64 -> int64
27 = "cparser_int64_unsigned_div"
28 external int64_unsigned_mod: int64 -> int64 -> int64
29 = "cparser_int64_unsigned_mod"
30 external int64_unsigned_compare: int64 -> int64 -> int
31 = "cparser_int64_unsigned_compare"
35 (* Reduce n to the range of representable integers of the given kind *)
37 let normalize_int n ik =
39 if n = 0L then 0L else 1L
41 let bitsize = sizeof_ikind ik * 8
42 and signed = is_signed_ikind ik in
43 if bitsize >= 64 then n else begin
44 let a = 64 - bitsize in
45 let p = Int64.shift_left n a in
47 then Int64.shift_right p a
48 else Int64.shift_right_logical p a
52 (* Reduce n to the range of representable floats of the given kind *)
54 let normalize_float f fk =
56 | FFloat -> Int32.float_of_bits (Int32.bits_of_float f)
58 | FLongDouble -> raise Notconst (* cannot accurately compute on this type *)
72 let constant = function
73 | CInt(v, ik, _) -> I (normalize_int v ik)
74 | CFloat(v, fk, _) -> F (normalize_float v fk)
79 let is_signed env ty =
80 match unroll env ty with
81 | TInt(ik, _) -> is_signed_ikind ik
84 let cast env ty_to ty_from v =
85 match unroll env ty_to, v with
86 | TInt(IBool, _), _ ->
87 if boolean_value v then I 1L else I 0L
91 I(normalize_int (Int64.of_float n) ik)
92 | TInt(ik, _), (S _ | WS _) ->
93 if sizeof_ikind ik >= !config.sizeof_ptr
96 | TFloat(fk, _), F n ->
97 F(normalize_float n fk)
98 | TFloat(fk, _), I n ->
99 if is_signed env ty_from
100 then F(normalize_float (Int64.to_float n) fk)
101 else F(normalize_float (int64_unsigned_to_float n) fk)
102 | TPtr(ty, _), I n ->
103 I (normalize_int n ptr_t_ikind)
104 | TPtr(ty, _), F n ->
105 if n = 0.0 then I 0L else raise Notconst
106 | TPtr(ty, _), (S _ | WS _) ->
111 let unop env op tyres ty v =
113 match op, tyres, v with
114 | Ominus, TInt _, I n -> I (Int64.neg n)
115 | Ominus, TFloat _, F n -> F (-. n)
116 | Oplus, TInt _, I n -> I n
117 | Oplus, TFloat _, F n -> F n
118 | Olognot, _, _ -> if boolean_value v then I 0L else I 1L
119 | _ -> raise Notconst
120 in cast env ty tyres res
122 let comparison env direction ptraction tyop ty1 v1 ty2 v2 =
123 (* tyop = type at which the comparison is done *)
125 match cast env tyop ty1 v1, cast env tyop ty2 v2 with
127 if is_signed env tyop
128 then direction (compare n1 n2) 0
129 else direction (int64_unsigned_compare n1 n2) 0 (* including pointers *)
131 direction (compare n1 n2) 0
132 | (S _ | WS _), I 0L ->
133 begin match ptraction with None -> raise Notconst | Some b -> b end
134 | I 0L, (S _ | WS _) ->
135 begin match ptraction with None -> raise Notconst | Some b -> b end
138 in if b then I 1L else I 0L
140 let binop env op tyop tyres ty1 v1 ty2 v2 =
141 (* tyop = type at which the computation is done
142 tyres = expected result type *)
146 if is_arith_type env ty1 && is_arith_type env ty2 then begin
147 match cast env tyop ty1 v1, cast env tyop ty2 v2 with
148 | I n1, I n2 -> I (Int64.add n1 n2)
149 | F n1, F n2 -> F (n1 +. n2)
150 | _, _ -> raise Notconst
154 if is_arith_type env ty1 && is_arith_type env ty2 then begin
155 match cast env tyop ty1 v1, cast env tyop ty2 v2 with
156 | I n1, I n2 -> I (Int64.sub n1 n2)
157 | F n1, F n2 -> F (n1 -. n2)
158 | _, _ -> raise Notconst
162 begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
163 | I n1, I n2 -> I (Int64.mul n1 n2)
164 | F n1, F n2 -> F (n1 *. n2)
165 | _, _ -> raise Notconst
168 begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
170 if n2 = 0L then raise Notconst else
171 if is_signed env tyop then I (Int64.div n1 n2)
172 else I (int64_unsigned_div n1 n2)
173 | F n1, F n2 -> F (n1 /. n2)
174 | _, _ -> raise Notconst
177 begin match v1, v2 with
179 if n2 = 0L then raise Notconst else
180 if is_signed env tyop then I (Int64.rem n1 n2)
181 else I (int64_unsigned_mod n1 n2)
182 | _, _ -> raise Notconst
185 begin match v1, v2 with
186 | I n1, I n2 -> I (Int64.logand n1 n2)
187 | _, _ -> raise Notconst
190 begin match v1, v2 with
191 | I n1, I n2 -> I (Int64.logor n1 n2)
192 | _, _ -> raise Notconst
195 begin match v1, v2 with
196 | I n1, I n2 -> I (Int64.logxor n1 n2)
197 | _, _ -> raise Notconst
200 begin match v1, v2 with
201 | I n1, I n2 when n2 >= 0L && n2 < 64L ->
202 I (Int64.shift_left n1 (Int64.to_int n2))
203 | _, _ -> raise Notconst
206 begin match v1, v2 with
207 | I n1, I n2 when n2 >= 0L && n2 < 64L ->
208 if is_signed env tyop
209 then I (Int64.shift_right n1 (Int64.to_int n2))
210 else I (Int64.shift_right_logical n1 (Int64.to_int n2))
211 | _, _ -> raise Notconst
214 comparison env (=) (Some false) tyop ty1 v1 ty2 v2
216 comparison env (<>) (Some true) tyop ty1 v1 ty2 v2
218 comparison env (<) None tyop ty1 v1 ty2 v2
220 comparison env (>) None tyop ty1 v1 ty2 v2
222 comparison env (<=) None tyop ty1 v1 ty2 v2
224 comparison env (>=) None tyop ty1 v1 ty2 v2
229 then if boolean_value v2 then I 1L else I 0L
234 else if boolean_value v2 then I 1L else I 0L
235 | _ -> raise Notconst
236 (* force normalization of result, e.g. of double to float *)
237 in cast env tyres tyres res
244 begin match sizeof env ty with
245 | None -> raise Notconst
246 | Some n -> I(Int64.of_int n)
251 unop env op e.etyp e1.etyp (expr env e1)
252 | EBinop(op, e1, e2, ty) ->
253 binop env op ty e.etyp e1.etyp (expr env e1) e2.etyp (expr env e2)
254 | EConditional(e1, e2, e3) ->
255 if boolean_value (expr env e1) then expr env e2 else expr env e3
257 cast env e1.etyp ty (expr env e1)
261 let integer_expr env e =
263 match cast env e.etyp (TInt(ILongLong, [])) (expr env e) with
266 with Notconst -> None
268 let constant_expr env ty e =
270 match unroll env ty, cast env e.etyp ty (expr env e) with
271 | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
272 | TFloat(fk, _), F n -> Some(CFloat(n, fk, ""))
273 | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, ""))
274 | TPtr(_, _), S s -> Some(CStr s)
275 | TPtr(_, _), WS s -> Some(CWStr s)
277 with Notconst -> None