diff options
Diffstat (limited to 'cparser/Ceval.ml')
-rw-r--r-- | cparser/Ceval.ml | 277 |
1 files changed, 277 insertions, 0 deletions
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml new file mode 100644 index 00000000..0e22852d --- /dev/null +++ b/cparser/Ceval.ml @@ -0,0 +1,277 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Evaluation of compile-time constants *) + +open C +open Cutil +open Machine + +(* Extra arith on int64 *) + +external int64_unsigned_to_float: int64 -> float + = "cparser_int64_unsigned_to_float" +external int64_unsigned_div: int64 -> int64 -> int64 + = "cparser_int64_unsigned_div" +external int64_unsigned_mod: int64 -> int64 -> int64 + = "cparser_int64_unsigned_mod" +external int64_unsigned_compare: int64 -> int64 -> int + = "cparser_int64_unsigned_compare" + +exception Notconst + +(* Reduce n to the range of representable integers of the given kind *) + +let normalize_int n ik = + if ik = IBool then + if n = 0L then 0L else 1L + else begin + let bitsize = sizeof_ikind ik * 8 + and signed = is_signed_ikind ik in + if bitsize >= 64 then n else begin + let a = 64 - bitsize in + let p = Int64.shift_left n a in + if signed + then Int64.shift_right p a + else Int64.shift_right_logical p a + end + end + +(* Reduce n to the range of representable floats of the given kind *) + +let normalize_float f fk = + match fk with + | FFloat -> Int32.float_of_bits (Int32.bits_of_float f) + | FDouble -> f + | FLongDouble -> raise Notconst (* cannot accurately compute on this type *) + +type value = + | I of int64 + | F of float + | S of string + | WS of int64 list + +let boolean_value v = + match v with + | I n -> n <> 0L + | F n -> n <> 0.0 + | S _ | WS _ -> true + +let constant = function + | CInt(v, ik, _) -> I (normalize_int v ik) + | CFloat(v, fk, _) -> F (normalize_float v fk) + | CStr s -> S s + | CWStr s -> WS s + | CEnum(id, v) -> I v + +let is_signed env ty = + match unroll env ty with + | TInt(ik, _) -> is_signed_ikind ik + | _ -> false + +let cast env ty_to ty_from v = + match unroll env ty_to, v with + | TInt(IBool, _), _ -> + if boolean_value v then I 1L else I 0L + | TInt(ik, _), I n -> + I(normalize_int n ik) + | TInt(ik, _), F n -> + I(normalize_int (Int64.of_float n) ik) + | TInt(ik, _), (S _ | WS _) -> + if sizeof_ikind ik >= !config.sizeof_ptr + then v + else raise Notconst + | TFloat(fk, _), F n -> + F(normalize_float n fk) + | TFloat(fk, _), I n -> + if is_signed env ty_from + then F(normalize_float (Int64.to_float n) fk) + else F(normalize_float (int64_unsigned_to_float n) fk) + | TPtr(ty, _), I n -> + I (normalize_int n ptr_t_ikind) + | TPtr(ty, _), F n -> + if n = 0.0 then I 0L else raise Notconst + | TPtr(ty, _), (S _ | WS _) -> + v + | _, _ -> + raise Notconst + +let unop env op tyres ty v = + let res = + match op, tyres, v with + | Ominus, TInt _, I n -> I (Int64.neg n) + | Ominus, TFloat _, F n -> F (-. n) + | Oplus, TInt _, I n -> I n + | Oplus, TFloat _, F n -> F n + | Olognot, _, _ -> if boolean_value v then I 0L else I 1L + | _ -> raise Notconst + in cast env ty tyres res + +let comparison env direction ptraction tyop ty1 v1 ty2 v2 = + (* tyop = type at which the comparison is done *) + let b = + match cast env tyop ty1 v1, cast env tyop ty2 v2 with + | I n1, I n2 -> + if is_signed env tyop + then direction (compare n1 n2) 0 + else direction (int64_unsigned_compare n1 n2) 0 (* including pointers *) + | F n1, F n2 -> + direction (compare n1 n2) 0 + | (S _ | WS _), I 0L -> + begin match ptraction with None -> raise Notconst | Some b -> b end + | I 0L, (S _ | WS _) -> + begin match ptraction with None -> raise Notconst | Some b -> b end + | _, _ -> + raise Notconst + in if b then I 1L else I 0L + +let binop env op tyop tyres ty1 v1 ty2 v2 = + (* tyop = type at which the computation is done + tyres = expected result type *) + let res = + match op with + | Oadd -> + if is_arith_type env ty1 && is_arith_type env ty2 then begin + match cast env tyop ty1 v1, cast env tyop ty2 v2 with + | I n1, I n2 -> I (Int64.add n1 n2) + | F n1, F n2 -> F (n1 +. n2) + | _, _ -> raise Notconst + end else + raise Notconst + | Osub -> + if is_arith_type env ty1 && is_arith_type env ty2 then begin + match cast env tyop ty1 v1, cast env tyop ty2 v2 with + | I n1, I n2 -> I (Int64.sub n1 n2) + | F n1, F n2 -> F (n1 -. n2) + | _, _ -> raise Notconst + end else + raise Notconst + | Omul -> + begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with + | I n1, I n2 -> I (Int64.mul n1 n2) + | F n1, F n2 -> F (n1 *. n2) + | _, _ -> raise Notconst + end + | Odiv -> + begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with + | I n1, I n2 -> + if n2 = 0L then raise Notconst else + if is_signed env tyop then I (Int64.div n1 n2) + else I (int64_unsigned_div n1 n2) + | F n1, F n2 -> F (n1 /. n2) + | _, _ -> raise Notconst + end + | Omod -> + begin match v1, v2 with + | I n1, I n2 -> + if n2 = 0L then raise Notconst else + if is_signed env tyop then I (Int64.rem n1 n2) + else I (int64_unsigned_mod n1 n2) + | _, _ -> raise Notconst + end + | Oand -> + begin match v1, v2 with + | I n1, I n2 -> I (Int64.logand n1 n2) + | _, _ -> raise Notconst + end + | Oor -> + begin match v1, v2 with + | I n1, I n2 -> I (Int64.logor n1 n2) + | _, _ -> raise Notconst + end + | Oxor -> + begin match v1, v2 with + | I n1, I n2 -> I (Int64.logxor n1 n2) + | _, _ -> raise Notconst + end + | Oshl -> + begin match v1, v2 with + | I n1, I n2 when n2 >= 0L && n2 < 64L -> + I (Int64.shift_left n1 (Int64.to_int n2)) + | _, _ -> raise Notconst + end + | Oshr -> + begin match v1, v2 with + | I n1, I n2 when n2 >= 0L && n2 < 64L -> + if is_signed env tyop + then I (Int64.shift_right n1 (Int64.to_int n2)) + else I (Int64.shift_right_logical n1 (Int64.to_int n2)) + | _, _ -> raise Notconst + end + | Oeq -> + comparison env (=) (Some false) tyop ty1 v1 ty2 v2 + | One -> + comparison env (<>) (Some true) tyop ty1 v1 ty2 v2 + | Olt -> + comparison env (<) None tyop ty1 v1 ty2 v2 + | Ogt -> + comparison env (>) None tyop ty1 v1 ty2 v2 + | Ole -> + comparison env (<=) None tyop ty1 v1 ty2 v2 + | Oge -> + comparison env (>=) None tyop ty1 v1 ty2 v2 + | Ocomma -> + v2 + | Ologand -> + if boolean_value v1 + then if boolean_value v2 then I 1L else I 0L + else I 0L + | Ologor -> + if boolean_value v1 + then I 1L + else if boolean_value v2 then I 1L else I 0L + | _ -> raise Notconst + (* force normalization of result, e.g. of double to float *) + in cast env tyres tyres res + +let rec expr env e = + match e.edesc with + | EConst c -> + constant c + | ESizeof ty -> + begin match sizeof env ty with + | None -> raise Notconst + | Some n -> I(Int64.of_int n) + end + | EVar _ -> + raise Notconst + | EUnop(op, e1) -> + unop env op e.etyp e1.etyp (expr env e1) + | EBinop(op, e1, e2, ty) -> + binop env op ty e.etyp e1.etyp (expr env e1) e2.etyp (expr env e2) + | EConditional(e1, e2, e3) -> + if boolean_value (expr env e1) then expr env e2 else expr env e3 + | ECast(ty, e1) -> + cast env e1.etyp ty (expr env e1) + | ECall _ -> + raise Notconst + +let integer_expr env e = + try + match cast env e.etyp (TInt(ILongLong, [])) (expr env e) with + | I n -> Some n + | _ -> None + with Notconst -> None + +let constant_expr env ty e = + try + match unroll env ty, cast env e.etyp ty (expr env e) with + | TInt(ik, _), I n -> Some(CInt(n, ik, "")) + | TFloat(fk, _), F n -> Some(CFloat(n, fk, "")) + | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, "")) + | TPtr(_, _), S s -> Some(CStr s) + | TPtr(_, _), WS s -> Some(CWStr s) + | _ -> None + with Notconst -> None |