source: Deliverables/D2.3/8051/cparser/Ceval.ml @ 453

Last change on this file since 453 was 453, checked in by ayache, 9 years ago

Import of the Paris's sources.

File size: 8.8 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
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.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Evaluation of compile-time constants *)
17
18open C
19open Cutil
20open Machine
21
22(* Extra arith on int64 *)
23
24external int64_unsigned_to_float: int64 -> float 
25  = "cparser_int64_unsigned_to_float"
26external int64_unsigned_div: int64 -> int64 -> int64
27  = "cparser_int64_unsigned_div"
28external int64_unsigned_mod: int64 -> int64 -> int64
29  = "cparser_int64_unsigned_mod"
30external int64_unsigned_compare: int64 -> int64 -> int
31  = "cparser_int64_unsigned_compare"
32
33exception Notconst
34
35(* Reduce n to the range of representable integers of the given kind *)
36
37let normalize_int n ik =
38  if ik = IBool then
39    if n = 0L then 0L else 1L
40  else begin
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
46      if signed
47      then Int64.shift_right p a
48      else Int64.shift_right_logical p a
49    end
50  end
51
52(* Reduce n to the range of representable floats of the given kind *)
53
54let normalize_float f fk =
55  match fk with
56  | FFloat -> Int32.float_of_bits (Int32.bits_of_float f)
57  | FDouble -> f
58  | FLongDouble -> raise Notconst (* cannot accurately compute on this type *)
59
60type value =
61  | I of int64
62  | F of float
63  | S of string
64  | WS of int64 list
65
66let boolean_value v =
67  match v with
68  | I n -> n <> 0L
69  | F n -> n <> 0.0
70  | S _ | WS _ -> true
71
72let constant = function
73  | CInt(v, ik, _) -> I (normalize_int v ik)
74  | CFloat(v, fk, _) -> F (normalize_float v fk)
75  | CStr s -> S s
76  | CWStr s -> WS s
77  | CEnum(id, v) -> I v
78
79let is_signed env ty =
80  match unroll env ty with
81  | TInt(ik, _) -> is_signed_ikind ik
82  | _ -> false
83
84let 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
88  | TInt(ik, _), I n ->
89      I(normalize_int n ik)
90  | TInt(ik, _), F n ->
91      I(normalize_int (Int64.of_float n) ik)
92  | TInt(ik, _), (S _ | WS _) ->
93      if sizeof_ikind ik >= !config.sizeof_ptr
94      then v
95      else raise Notconst
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 _) ->
107      v
108  | _, _ ->
109      raise Notconst
110
111let unop env op tyres ty v =
112  let res =
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
121
122let comparison env direction ptraction tyop ty1 v1 ty2 v2 =
123  (* tyop = type at which the comparison is done *)
124  let b =
125    match cast env tyop ty1 v1, cast env tyop ty2 v2 with
126    | I n1, I n2 -> 
127        if is_signed env tyop
128        then direction (compare n1 n2) 0
129        else direction (int64_unsigned_compare n1 n2) 0 (* including pointers *)
130    | F n1, F n2 ->
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
136    | _, _ ->
137        raise Notconst
138  in if b then I 1L else I 0L
139
140let binop env op tyop tyres ty1 v1 ty2 v2 =
141  (* tyop = type at which the computation is done
142     tyres = expected result type *)
143  let res =
144    match op with
145    | Oadd ->
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
151        end else
152          raise Notconst
153    | Osub ->
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
159        end else
160          raise Notconst
161    | Omul ->
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
166        end
167    | Odiv ->
168        begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
169          | I n1, I n2 -> 
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
175        end
176    | Omod ->
177        begin match v1, v2 with
178          | I n1, I n2 -> 
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
183        end
184    | Oand ->
185        begin match v1, v2 with
186          | I n1, I n2 -> I (Int64.logand n1 n2)
187          | _, _ -> raise Notconst
188        end
189    | Oor ->
190        begin match v1, v2 with
191          | I n1, I n2 -> I (Int64.logor n1 n2)
192          | _, _ -> raise Notconst
193        end
194    | Oxor ->
195        begin match v1, v2 with
196          | I n1, I n2 -> I (Int64.logxor n1 n2)
197          | _, _ -> raise Notconst
198        end
199    | Oshl ->
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
204        end
205    | Oshr ->
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
212        end
213    | Oeq ->
214        comparison env (=) (Some false) tyop ty1 v1 ty2 v2
215    | One ->
216        comparison env (<>) (Some true) tyop ty1 v1 ty2 v2
217    | Olt ->
218        comparison env (<) None tyop ty1 v1 ty2 v2
219    | Ogt ->
220        comparison env (>) None tyop ty1 v1 ty2 v2
221    | Ole ->
222        comparison env (<=) None tyop ty1 v1 ty2 v2
223    | Oge ->
224        comparison env (>=) None tyop ty1 v1 ty2 v2
225    | Ocomma ->
226        v2
227    | Ologand ->
228        if boolean_value v1
229        then if boolean_value v2 then I 1L else I 0L
230        else I 0L
231    | Ologor ->
232        if boolean_value v1
233        then I 1L
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
238
239let rec expr env e =
240  match e.edesc with
241  | EConst c ->
242      constant c
243  | ESizeof ty ->
244      begin match sizeof env ty with
245      | None -> raise Notconst
246      | Some n -> I(Int64.of_int n)
247      end
248  | EVar _ ->
249      raise Notconst
250  | EUnop(op, e1) ->
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
256  | ECast(ty, e1) ->
257      cast env e1.etyp ty (expr env e1)
258  | ECall _ ->
259      raise Notconst
260
261let integer_expr env e =
262  try
263    match cast env e.etyp (TInt(ILongLong, [])) (expr env e) with
264    | I n -> Some n
265    | _   -> None
266  with Notconst -> None
267
268let constant_expr env ty e =
269  try
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)
276    | _   -> None
277  with Notconst -> None
Note: See TracBrowser for help on using the repository browser.