summaryrefslogtreecommitdiff
path: root/cparser/Ceval.ml
blob: 504f7e08b6e90fd23bb3141ae6ae2a7def5420ca (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
(* *********************************************************************)
(*                                                                     *)
(*              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 *)

(* Unsigned comparison: do signed comparison after shifting range *)

let int64_unsigned_compare x y =
  Int64.compare (Int64.add x Int64.min_int) (Int64.add y Int64.min_int)

(* Unsigned division and modulus: synthesized from signed division
   as described in "Hacker's Delight", section 9.3. *)

let int64_unsigned_div n d =
  if d < 0L then
    if int64_unsigned_compare n d < 0 then 0L else 1L
  else begin
    let q = Int64.shift_left (Int64.div (Int64.shift_right_logical n 1) d) 1 in
    let r = Int64.sub n (Int64.mul q d) in
    if int64_unsigned_compare r d >= 0 then Int64.succ q else q
  end

let int64_unsigned_mod n d =
  if d < 0L then
    if int64_unsigned_compare n d < 0 then n else Int64.sub n d
  else begin
    let q = Int64.shift_left (Int64.div (Int64.shift_right_logical n 1) d) 1 in
    let r = Int64.sub n (Int64.mul q d) in
    if int64_unsigned_compare r d >= 0 then Int64.sub r d else r
  end

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 *)

type value =
  | I of int64
  | S of string
  | WS of int64 list

let boolean_value v =
  match v with
  | I n -> n <> 0L
  | S _ | WS _ -> true

let constant = function
  | CInt(v, ik, _) -> I (normalize_int v ik)
  | CFloat(v, fk) -> raise Notconst
  | 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
  | TEnum(_, _) -> is_signed_ikind enum_ikind
  | _ -> 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, _), (S _ | WS _) ->
      if sizeof_ikind ik >= !config.sizeof_ptr
      then v
      else raise Notconst
  | TPtr(ty, _), I n ->
      I (normalize_int n ptr_t_ikind)
  | TPtr(ty, _), (S _ | WS _) ->
      v
  | TEnum(_, _), I n ->
      I (normalize_int n enum_ikind)
  | _, _ ->
      raise Notconst

let unop env op tyres ty v =
  let res =
   match op, tyres, v with
   | Ominus, TInt _, I n -> I (Int64.neg n)
   | Oplus, TInt _, I n -> I n
   | Olognot, _, _ -> if boolean_value v then I 0L else I 1L
   | Onot, _, I n -> I (Int64.lognot n)
   | _ -> 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 *)
    | (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)
          | _, _ -> 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)
          | _, _ -> 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)
          | _, _ -> 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)
          | _, _ -> 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
  | EAlignof ty ->
      begin match alignof 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 cast env e.etyp e2.etyp (expr env e2)
      else cast env e.etyp e3.etyp (expr env e3)
  (* | ECast(TInt (_, _), EConst (CFloat (_, _))) -> TODO *)
  | ECast(ty, e1) ->
      cast env ty e1.etyp (expr env e1)
  | ECall _ ->
      raise Notconst

let integer_expr env e =
  try
    match cast env (TInt(ILongLong, [])) e.etyp (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 ty e.etyp (expr env e) with
    | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
    | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, ""))
    | TPtr(_, _), S s -> Some(CStr s)
    | TPtr(_, _), WS s -> Some(CWStr s)
    | TEnum(_, _), I n -> Some(CInt(n, enum_ikind, ""))
    | _   -> None
  with Notconst -> None