cparser/Ceval.ml

   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
  18 open C
  19 open Cutil
  20 open Machine
  21
  22 (* Extra arith on int64 *)
  23
  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"
  32
  33 exception Notconst
  34
  35 (* Reduce n to the range of representable integers of the given kind *)
  36
  37 let 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
  54 let 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
  60 type value =
  61   | I of int64
  62   | F of float
  63   | S of string
  64   | WS of int64 list
  65
  66 let boolean_value v =
  67   match v with
  68   | I n -> n <> 0L
  69   | F n -> n <> 0.0
  70   | S _ | WS _ -> true
  71
  72 let 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
  79 let is_signed env ty =
  80   match unroll env ty with
  81   | TInt(ik, _) -> is_signed_ikind ik
  82   | _ -> false
  83
  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
  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
 111 let 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
 122 let 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
 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 *)
 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
 239 let 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
 261 let 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
 268 let 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