ival.ml 60.3 KB
Newer Older
1 2 3 4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
5
(*  Copyright (C) 2007-2019                                               *)
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
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Abstract_interp

(* Make sure all this is synchronized with the default value of -ilevel *)
let small_cardinal = ref 8
let small_cardinal_Int = ref (Int.of_int !small_cardinal)
let small_cardinal_log = ref 3

let set_small_cardinal i =
  assert (2 <= i && i <= 1024);
  let rec log j p =
    if i <= p then j
    else log (j+1) (2*p)
  in
  small_cardinal := i;
  small_cardinal_Int := Int.of_int i;
David Bühler's avatar
David Bühler committed
38 39 40
  small_cardinal_log := log 1 2;
  (* TODO: share this code with Int_set *)
  Int_set.set_small_cardinal i
41 42 43

let get_small_cardinal () = !small_cardinal

David Bühler's avatar
David Bühler committed
44 45
let emitter = Lattice_messages.register "Ival"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
46 47 48 49

module O = FCSet.Make(Integer)

type t =
David Bühler's avatar
David Bühler committed
50
  | Set of Int_set.t
51
  | Float of Fval.t
David Bühler's avatar
David Bühler committed
52
  | Itv of Int_interval.t
David Bühler's avatar
David Bühler committed
53 54 55 56
  (* Binary abstract operations do not model precisely float/integer operations.
     It is the responsibility of the callers to have two operands of the same
     implicit type. The only exception is for [singleton_zero], which is the
     correct representation of [0.] *)
57 58


59
module Widen_Hints = Datatype.Integer.Set
60
type size_widen_hint = Integer.t
61 62
type numerical_widen_hint = Widen_Hints.t * Fc_float.Widen_Hints.t
type widen_hint = size_widen_hint * numerical_widen_hint
63

David Bühler's avatar
David Bühler committed
64
let bottom = Set Int_set.bottom
David Bühler's avatar
David Bühler committed
65
let top = Itv Int_interval.top
66

David Bühler's avatar
David Bühler committed
67 68
let hash = function
  | Set s -> Int_set.hash s
David Bühler's avatar
David Bühler committed
69
  | Itv i -> Int_interval.hash i
David Bühler's avatar
David Bühler committed
70
  | Float f -> 3 + 17 * Fval.hash f
71 72 73

let compare e1 e2 =
  if e1==e2 then 0 else
David Bühler's avatar
David Bühler committed
74
    match e1, e2 with
David Bühler's avatar
David Bühler committed
75
    | Set s1, Set s2 -> Int_set.compare s1 s2
David Bühler's avatar
David Bühler committed
76 77
    | Itv i1, Itv i2 -> Int_interval.compare i1 i2
    | Float f1, Float f2 -> Fval.compare f1 f2
David Bühler's avatar
David Bühler committed
78 79 80 81
    | _, Set _ -> 1
    | Set _, _ -> -1
    | _, Itv _ -> 1
    | Itv _, _ -> -1
82 83 84

let equal e1 e2 = compare e1 e2 = 0

David Bühler's avatar
David Bühler committed
85
let pretty fmt = function
David Bühler's avatar
David Bühler committed
86
  | Itv i -> Int_interval.pretty fmt i
David Bühler's avatar
David Bühler committed
87
  | Float f -> Fval.pretty fmt f
David Bühler's avatar
David Bühler committed
88
  | Set s -> Int_set.pretty fmt s
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103

let min_le_elt min elt =
  match min with
  | None -> true
  | Some m -> Int.le m elt

let max_ge_elt max elt =
  match max with
  | None -> true
  | Some m -> Int.ge m elt


let fail min max r modu =
  let bound fmt = function
    | None -> Format.fprintf fmt "--"
David Bühler's avatar
David Bühler committed
104
    | Some x -> Int.pretty fmt x
105
  in
106
  Kernel.fatal "Ival: broken Itv, min=%a max=%a r=%a modu=%a"
107 108 109 110 111 112 113
    bound min bound max Int.pretty r Int.pretty modu

let is_safe_modulo r modu =
  (Int.ge r Int.zero ) && (Int.ge modu Int.one) && (Int.lt r modu)

let is_safe_bound bound r modu = match bound with
  | None -> true
114
  | Some m -> Int.equal (Int.e_rem m modu) r
115

116
(* Sanity check for Itv's arguments *)
117 118 119 120 121 122 123
let check min max r modu =
  if not (is_safe_modulo r modu
          && is_safe_bound min r modu
          && is_safe_bound max r modu)
  then fail min max r modu


David Bühler's avatar
David Bühler committed
124
let cardinal_zero_or_one = function
125
  | Itv _ -> false
David Bühler's avatar
David Bühler committed
126
  | Set s -> Int_set.cardinal s <= 1
127 128 129
  | Float f -> Fval.is_singleton f

let is_singleton_int v = match v with
David Bühler's avatar
David Bühler committed
130 131
  | Float _ | Itv _ -> false
  | Set s -> Int_set.cardinal s = 1
132

David Bühler's avatar
David Bühler committed
133 134
(* TODO *)
let is_bottom x = equal x bottom
135

David Bühler's avatar
David Bühler committed
136 137 138 139
let zero = Set Int_set.zero
let one = Set Int_set.one
let minus_one = Set Int_set.minus_one
let zero_or_one = Set Int_set.zero_or_one
140 141
let float_zeros = Float Fval.zeros

David Bühler's avatar
David Bühler committed
142 143
let positive_integers = Itv (Int_interval.inject_range (Some Int.zero) None)
let negative_integers = Itv (Int_interval.inject_range None (Some Int.zero))
144 145 146

let is_zero x = x == zero

David Bühler's avatar
David Bühler committed
147
let inject_singleton e = Set (Int_set.inject_singleton e)
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171

let inject_float f =
  if Fval.(equal plus_zero f)
  then zero
  else Float f

let inject_float_interval flow fup =
  let flow = Fval.F.of_float flow in
  let fup = Fval.F.of_float fup in
  (* make sure that zero float is also zero int *)
  if Fval.F.equal Fval.F.plus_zero flow && Fval.F.equal Fval.F.plus_zero fup
  then zero
  else Float (Fval.inject Fval.Double flow fup)

(*  let minus_zero = Float (Fval.minus_zero, Fval.minus_zero) *)

let is_one = equal one

let project_float v =
  if is_zero v
  then Fval.plus_zero
  else
    match v with
    | Float f -> f
172
    | Itv _ | Set _ -> assert false (* by hypothesis that it is a float *)
173

174 175
let is_float = function
  | Float _ -> true
176
  | Itv _ -> false
177 178 179
  | Set _ as i -> equal zero i || equal bottom i

let is_int = function
180
  | Itv _ | Set _ -> true
181 182
  | Float _ -> false

David Bühler's avatar
David Bühler committed
183
let contains_zero = function
David Bühler's avatar
David Bühler committed
184
  | Itv i -> Int_interval.mem Int.zero i
David Bühler's avatar
David Bühler committed
185
  | Set s -> Int_set.mem Int.zero s >= 0
186 187
  | Float f -> Fval.contains_a_zero f

David Bühler's avatar
David Bühler committed
188
let contains_non_zero = function
189
  | Itv _ -> true (* at least two values *)
David Bühler's avatar
David Bühler committed
190
  | Set _ as s -> not (is_zero s || is_bottom s)
191 192 193 194 195
  | Float f -> Fval.contains_non_zero f


exception Not_Singleton_Int

David Bühler's avatar
David Bühler committed
196
let project_int = function
David Bühler's avatar
David Bühler committed
197 198
  | Set s ->
    if Int_set.cardinal s = 1 then Int_set.min s else raise Not_Singleton_Int
David Bühler's avatar
David Bühler committed
199
  | _ -> raise Not_Singleton_Int
200

201 202 203 204 205
let is_small_set = function
  | Set _ -> true
  | _ -> false

let project_small_set = function
David Bühler's avatar
David Bühler committed
206
  | Set a -> Some (Int_set.to_list a)
207 208
  | _ -> None

David Bühler's avatar
David Bühler committed
209
let cardinal = function
David Bühler's avatar
David Bühler committed
210 211 212
  | Itv i -> Int_interval.cardinal i
  | Set s -> Some (Int.of_int (Int_set.cardinal s))
  | Float f -> if Fval.is_singleton f then Some Int.one else None
213 214 215

let cardinal_estimate v ~size =
  match v with
David Bühler's avatar
David Bühler committed
216
  | Set s -> Int.of_int (Int_set.cardinal s)
David Bühler's avatar
David Bühler committed
217
  | Itv i -> Extlib.opt_conv (Int.two_power size) (Int_interval.cardinal i)
218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
  | Float f ->
    if Fval.is_singleton f
    then Int.one
    else
      let bits_of_float =
        if Integer.(equal size (of_int 32))
        then Fval.bits_of_float32_list
        else if Integer.(equal size (of_int 64))
        then Fval.bits_of_float64_list
        else (fun _ -> [Int.zero, Int.pred (Int.two_power size)])
      in
      let bits_list = bits_of_float f in
      let count acc (min, max) = Int.add acc (Int.length min max) in
      List.fold_left count Int.zero bits_list

let cardinal_less_than v n =
  let c =
    match v with
David Bühler's avatar
David Bühler committed
236
    | Itv i -> Extlib.the ~exn:Not_less_than (Int_interval.cardinal i)
David Bühler's avatar
David Bühler committed
237
    | Set s -> Int.of_int (Int_set.cardinal s)
David Bühler's avatar
David Bühler committed
238
    | Float f ->
David Bühler's avatar
David Bühler committed
239
      if Fval.is_singleton f then Int.one else raise Not_less_than
240 241 242 243 244 245 246 247 248 249 250 251 252 253
  in
  if Int.le c (Int.of_int n)
  then Int.to_int c (* This is smaller than the original [n] *)
  else raise Not_less_than

let cardinal_is_less_than v n =
  match cardinal v with
  | None -> false
  | Some c -> Int.le c (Int.of_int n)

let make ~min ~max ~rem ~modu =
  match min, max with
  | Some mn, Some mx ->
    if Int.gt mx mn then
254
      let l = Int.succ (Int.e_div (Int.sub mx mn) modu) in
255 256
      if Int.le l !small_cardinal_Int
      then
David Bühler's avatar
David Bühler committed
257
        let l = Int.to_int l in
258 259
        let s = Array.make l Int.zero in
        let v = ref mn in
David Bühler's avatar
David Bühler committed
260
        let i = ref 0 in
261 262
        while (!i < l)
        do
David Bühler's avatar
David Bühler committed
263 264 265
          s.(!i) <- !v;
          v := Int.add modu !v;
          incr i
266
        done;
David Bühler's avatar
David Bühler committed
267
        assert (Int.equal !v (Int.add modu mx));
David Bühler's avatar
David Bühler committed
268
        Set (Int_set.inject_array s l)
David Bühler's avatar
David Bühler committed
269
      else Itv (Int_interval.make ~min ~max ~rem ~modu)
270 271 272
    else if Int.equal mx mn
    then inject_singleton mn
    else bottom
David Bühler's avatar
David Bühler committed
273
  | _ -> Itv (Int_interval.make ~min ~max ~rem ~modu)
274 275 276 277 278 279 280 281 282

let inject_top min max rem modu =
  check min max rem modu;
  make ~min ~max ~rem ~modu

let inject_interval ~min ~max ~rem:r ~modu =
  assert (is_safe_modulo r modu);
  let fix_bound fix bound = match bound with
    | None -> None
283
    | Some b -> Some (if Int.equal b (Int.e_rem r modu) then b else fix b)
284 285 286 287 288 289
  in
  let min = fix_bound (fun min -> Int.round_up_to_r ~min ~r ~modu) min
  and max = fix_bound (fun max -> Int.round_down_to_r ~max ~r ~modu) max in
  make ~min ~max ~rem:r ~modu


David Bühler's avatar
David Bühler committed
290 291 292 293
let inject_set_or_bottom = function
  | `Bottom -> bottom
  | `Value s -> Set s

David Bühler's avatar
David Bühler committed
294 295 296 297 298 299 300 301 302 303 304 305 306
let inject_itv_or_bottom = function
  | `Bottom -> bottom
  | `Value i ->
    match Int_interval.cardinal i with
    | None -> Itv i
    | Some card ->
      if Int.le card !small_cardinal_Int
      then
        let min, max, rem, modu = Int_interval.min_max_rem_modu i in
        make ~min ~max ~rem ~modu
      else Itv i


307 308 309
let subdiv_int v =
  match v with
  | Float _ -> raise Can_not_subdiv
David Bühler's avatar
David Bühler committed
310
  | Set s -> let s1, s2 = Int_set.subdivide s in Set s1, Set s2
David Bühler's avatar
David Bühler committed
311 312 313 314 315 316 317 318 319 320 321
  | Itv i ->
    let i1, i2 = Int_interval.subdivide i in
    (* Redo make in case an interval should be converted into a set. *)
    let t1 =
      let min, max, rem, modu = Int_interval.min_max_rem_modu i1 in
      make ~min ~max ~rem ~modu
    and t2 =
      let min, max, rem, modu = Int_interval.min_max_rem_modu i2 in
      make ~min ~max ~rem ~modu
    in
    t1, t2
322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338

let subdivide ~size = function
  | Float fval ->
    let fkind = match Integer.to_int size with
      | 32 -> Fval.Single
      | 64 -> Fval.Double
      | _ -> raise Can_not_subdiv (* see Value/Value#105 *)
    in
    let f1, f2 = Fval.subdiv_float_interval fkind fval in
    inject_float f1, inject_float f2
  | ival -> subdiv_int ival

let inject_range min max = inject_top min max Int.zero Int.one

let top_float = Float Fval.top
let top_single_precision_float = Float Fval.top

David Bühler's avatar
David Bühler committed
339 340 341 342
let make_top_from_set s =
  let min = Int_set.min s in
  let modu =
    Int_set.fold
343
      (fun acc x ->
David Bühler's avatar
David Bühler committed
344 345 346
         if Int.equal x min
         then acc
         else Int.pgcd (Int.sub x min) acc)
347 348 349
      Int.zero
      s
  in
David Bühler's avatar
David Bühler committed
350 351 352 353
  let rem = Int.e_rem min modu in
  let max = Some (Int_set.max s) in
  let min = Some min in
  min, max, rem, modu
354

David Bühler's avatar
David Bühler committed
355
let make_itv_from_set s =
David Bühler's avatar
David Bühler committed
356
  let min, max, rem, modu = make_top_from_set s in
David Bühler's avatar
David Bühler committed
357 358 359 360 361 362 363 364 365
  Int_interval.make ~min ~max ~rem ~modu

let make_itv = function
  | Itv i -> i
  | Set s -> make_itv_from_set s
  | Float _ -> Int_interval.top

let make_range = function
  | Itv i -> i
David Bühler's avatar
David Bühler committed
366 367 368
  | Set s ->
    let min, max = Int_set.min s, Int_set.max s in
    Int_interval.inject_range (Some min) (Some max)
David Bühler's avatar
David Bühler committed
369
  | Float _ -> Int_interval.top
370

David Bühler's avatar
David Bühler committed
371 372 373
let inject_pre_itv ~min ~max ~modu =
  let rem = Int.e_rem min modu in
  Itv (Int_interval.make ~min:(Some min) ~max:(Some max) ~rem ~modu)
374

David Bühler's avatar
David Bühler committed
375 376 377
let inject_set_or_top = function
  | `Set s -> Set s
  | `Top (min, max, modu) -> inject_pre_itv ~min ~max ~modu
378 379 380 381

let min_max_r_mod t =
  match t with
  | Set s ->
David Bühler's avatar
David Bühler committed
382 383 384
    assert (Int_set.cardinal s >= 2);
    make_top_from_set s
  | Itv i -> Int_interval.min_max_rem_modu i
385 386 387 388 389
  | Float _ -> None, None, Int.zero, Int.one

let min_and_max t =
  match t with
  | Set s ->
David Bühler's avatar
David Bühler committed
390
    let l = Int_set.cardinal s in
391 392
    if l = 0
    then raise Error_Bottom
David Bühler's avatar
David Bühler committed
393
    else Some (Int_set.min s), Some (Int_set.max s)
David Bühler's avatar
David Bühler committed
394
  | Itv i -> Int_interval.min_and_max i
395 396 397 398 399 400 401 402 403
  | Float _ -> None, None

let min_and_max_float t =
  match t with
  | Set _ when is_zero t -> Some (Fval.F.plus_zero, Fval.F.plus_zero), false
  | Float f -> Fval.min_and_max f
  | _ -> assert false

let has_greater_min_bound t1 t2 =
404
  if is_float t1 && is_float t2
405 406 407 408 409 410 411 412 413 414 415
  then Fval.has_greater_min_bound (project_float t1) (project_float t2)
  else
    let m1, _ = min_and_max t1 in
    let m2, _ = min_and_max t2 in
    match m1, m2 with
    | None, None -> 0
    | None, Some _ -> -1
    | Some _, None -> 1
    | Some m1, Some m2 -> Int.compare m1 m2

let has_smaller_max_bound t1 t2 =
416
  if is_float t1 && is_float t2
417 418 419 420 421 422 423 424 425 426
  then Fval.has_smaller_max_bound (project_float t1) (project_float t2)
  else
    let _, m1 = min_and_max t1 in
    let _, m2 = min_and_max t2 in
    match m1, m2 with
    | None, None -> 0
    | None, Some _ -> -1
    | Some _, None -> 1
    | Some m1, Some m2 -> Int.compare m2 m1

427
let widen (bitsize,(wh,fh)) t1 t2 =
428 429 430 431 432
  if equal t1 t2 || cardinal_zero_or_one t1 then t2
  else
    match t2 with
    | Float f2 ->
      let f1 = project_float t1 in
433 434 435 436 437 438 439 440 441 442
      let prec =
        if Integer.equal bitsize (Integer.of_int 32)
        then Float_sig.Single
        else if Integer.equal bitsize (Integer.of_int 64)
        then Float_sig.Double
        else if Integer.equal bitsize (Integer.of_int 128)
        then Float_sig.Long_Double
        else Float_sig.Single
      in
      Float (Fval.widen fh prec f1 f2)
443
    | Itv _ | Set _ ->
David Bühler's avatar
David Bühler committed
444 445 446
      let i1 = make_itv t1
      and i2 = make_itv t2 in
      inject_itv_or_bottom (`Value (Int_interval.widen (bitsize, wh) i1 i2))
447 448 449

let meet v1 v2 =
  if v1 == v2 then v1 else
David Bühler's avatar
David Bühler committed
450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470
    let result =
      match v1,v2 with
      | Itv i1, Itv i2 -> inject_itv_or_bottom (Int_interval.meet i1 i2)
      | Set s1 , Set s2 -> inject_set_or_bottom (Int_set.meet s1 s2)
      | Set s, Itv itv
      | Itv itv, Set s ->
        inject_set_or_bottom (Int_set.filter (fun i -> Int_interval.mem i itv) s)
      | Float(f1), Float(f2) -> begin
          match Fval.meet f1 f2 with
          | `Value f -> inject_float f
          | `Bottom -> bottom
        end
      | (Float f as ff), (Itv _ | Set _ as o)
      | (Itv _ | Set _ as o), (Float f as ff) ->
        if equal o top then ff
        else if contains_zero o && Fval.contains_plus_zero f then zero
        else bottom
    in
    (*      Format.printf "meet: %a /\\ %a -> %a@\n"
            pretty v1 pretty v2 pretty result;*)
    result
471 472 473 474

let intersects v1 v2 =
  v1 == v2 ||
  match v1, v2 with
475
  | Itv _, Itv _ -> not (is_bottom (meet v1 v2)) (* YYY: slightly inefficient *)
David Bühler's avatar
David Bühler committed
476
  | Set s1 , Set s2 -> Int_set.intersects s1 s2
David Bühler's avatar
David Bühler committed
477
  | Set s, Itv itv | Itv itv, Set s ->
David Bühler's avatar
David Bühler committed
478
    Int_set.exists (fun i -> Int_interval.mem i itv) s
479 480 481 482 483 484 485 486 487 488
  | Float f1, Float f2 -> begin
      match Fval.forward_comp Comp.Eq f1 f2 with
      | Comp.False -> false
      | Comp.True | Comp.Unknown -> true
    end
  | Float f, other | other, Float f ->
    equal top other || (Fval.contains_plus_zero f && contains_zero other)

let narrow v1 v2 =
  match v1, v2 with
David Bühler's avatar
David Bühler committed
489
  | Set s1, Set s2 -> inject_set_or_bottom (Int_set.narrow s1 s2)
490
  | Float _, Float _ | (Itv _| Set _), (Itv _ | Set _) ->
David Bühler's avatar
David Bühler committed
491
    meet v1 v2 (* meet is exact *)
492 493
  | v, (Itv _ as t) when equal t top -> v
  | (Itv _ as t), v when equal t top -> v
494 495 496 497 498
  | Float f, (Set _ as s) | (Set _ as s), Float f when is_zero s -> begin
      match Fval.narrow f Fval.zeros with
      | `Value f -> inject_float f
      | `Bottom -> bottom
    end
499
  | Float _, (Set _ | Itv _) | (Set _ | Itv _), Float _ ->
David Bühler's avatar
David Bühler committed
500 501
    (* ill-typed case. It is better to keep the operation symmetric *)
    top
502 503

let link v1 v2 = match v1, v2 with
David Bühler's avatar
David Bühler committed
504
  | Set s1, Set s2 -> inject_set_or_top (Int_set.link s1 s2)
David Bühler's avatar
David Bühler committed
505 506
  | Itv i1, Itv i2 -> Itv (Int_interval.link i1 i2)
  | Itv i, Set s | Set s, Itv i ->
David Bühler's avatar
David Bühler committed
507 508 509 510 511 512 513 514 515 516 517
    let min, max, rem, modu = Int_interval.min_max_rem_modu i in
    let move_bound add = function
      | None -> None
      | Some bound ->
        let cur = ref bound in
        Int_set.iter (fun e -> if Int.equal e (add !cur modu) then cur := e) s;
        Some !cur
    in
    let min = move_bound Int.sub min
    and max = move_bound Int.add max in
    inject_top min max rem modu
518 519 520 521 522 523 524
  | _ -> bottom


let join v1 v2 =
  let result =
    if v1 == v2 then v1 else
      match v1,v2 with
David Bühler's avatar
David Bühler committed
525
      | Itv i1, Itv i2 -> Itv (Int_interval.join i1 i2)
David Bühler's avatar
David Bühler committed
526
      | Set i1, Set i2 -> inject_set_or_top (Int_set.join i1 i2)
David Bühler's avatar
David Bühler committed
527 528
      | Set s, (Itv i as t)
      | (Itv i as t), Set s ->
David Bühler's avatar
David Bühler committed
529 530 531 532 533 534 535 536
        let min, max, r, modu = Int_interval.min_max_rem_modu i in
        let l = Int_set.cardinal s in
        if l = 0 then t
        else
          let f modu elt = Int.pgcd modu (Int.abs (Int.sub r elt)) in
          let modu = Int_set.fold f modu s in
          let rem = Int.e_rem r modu in
          let min = match min with
537
              None -> None
David Bühler's avatar
David Bühler committed
538 539 540
            | Some m -> Some (Int.min m (Int_set.min s))
          in
          let max = match max with
541
              None -> None
David Bühler's avatar
David Bühler committed
542 543 544 545
            | Some m -> Some (Int.max m (Int_set.max s))
          in
          check min max rem modu;
          Itv (Int_interval.make ~min ~max ~rem ~modu)
546
      | Float(f1), Float(f2) ->
David Bühler's avatar
David Bühler committed
547
        inject_float (Fval.join f1 f2)
548
      | Float (f) as ff, other | other, (Float (f) as ff) ->
David Bühler's avatar
David Bühler committed
549 550 551 552
        if is_zero other
        then inject_float (Fval.join Fval.plus_zero f)
        else if is_bottom other then ff
        else top
553
  in
David Bühler's avatar
David Bühler committed
554 555
  (*  Format.printf "mod_join %a %a -> %a@."
      pretty v1 pretty v2 pretty result; *)
556 557
  result

558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593
let complement_int_under ~size ~signed i =
  let e = Int.two_power_of_int (if signed then size - 1 else size) in
  let b = if signed then Int.neg e else Int.zero in
  let e = Int.pred e in
  let inject_range min max = `Value (inject_range (Some min) (Some max)) in
  match i with
  | Float _ -> `Bottom
  | Set [||] -> inject_range b e
  | Set set ->
    let l = Array.length set in
    let array = Array.make (l + 2) Int.zero in
    array.(0) <- b;
    Array.blit set 0 array 1 l;
    array.(l+1) <- e;
    let index = ref (-1) in
    let max_delta = ref Int.zero in
    for i = 0 to l do
      let delta = Int.sub array.(i+1) array.(i) in
      if Int.gt delta !max_delta then begin
        index := i;
        max_delta := delta
      end
    done;
    inject_range array.(!index) array.(!index + 1)
  | Top (min, max, _rem, _modu) ->
    match min, max with
    | None, None -> `Bottom
    | Some min, None -> inject_range b (Int.pred min)
    | None, Some max -> inject_range (Int.succ max) e
    | Some min, Some max ->
      let delta_min = Int.sub min b in
      let delta_max = Int.sub e max in
      if Int.le delta_min delta_max
      then inject_range (Int.succ max) e
      else inject_range b (Int.pred min)

594 595
let fold_int f v acc =
  match v with
David Bühler's avatar
David Bühler committed
596 597
  | Float _ -> raise Error_Top
  | Itv i -> Int_interval.fold_int f i acc
David Bühler's avatar
David Bühler committed
598
  | Set s -> Int_set.fold (fun acc x -> f x acc) acc s
599 600 601 602 603

let fold_enum f v acc =
  match v with
  | Float fl when Fval.is_singleton fl -> f v acc
  | Float _ -> raise Error_Top
604
  | Set _ | Itv _ -> fold_int (fun x acc -> f (inject_singleton x) acc) v acc
605 606 607 608

let is_included t1 t2 =
  (t1 == t2) ||
  match t1,t2 with
David Bühler's avatar
David Bühler committed
609
  | Set s, _ when Int_set.cardinal s = 0 -> true
David Bühler's avatar
David Bühler committed
610
  | Itv i1, Itv i2 -> Int_interval.is_included i1 i2
611
  | Itv _, Set _ -> false (* Itv _ represents more elements
612
                             than can be represented by Set _ *)
David Bühler's avatar
David Bühler committed
613
  | Set s, Itv i ->
David Bühler's avatar
David Bühler committed
614
    let min, max, rem, modu = Int_interval.min_max_rem_modu i in
615
    (* Inclusion of bounds is needed for the entire inclusion *)
David Bühler's avatar
David Bühler committed
616 617 618 619
    min_le_elt min (Int_set.min s) && max_ge_elt max (Int_set.max s)
    && (Int.equal Int.one modu (* Top side contains all integers, we're done *)
        || Int_set.for_all (fun x -> Int.equal (Int.e_rem x modu) rem) s)
  | Set s1, Set s2 -> Int_set.is_included s1 s2
620 621 622
  | Float f1, Float f2 -> Fval.is_included f1 f2
  | Float _, _ -> equal t2 top
  | Set _, Float f -> is_zero t1 && Fval.contains_plus_zero f
623
  | Itv _, Float _ -> false
624 625 626

let add_singleton_int i v = match v with
  | Float _ -> assert false
David Bühler's avatar
David Bühler committed
627
  | Set s -> Set (Int_set.add_singleton i s)
David Bühler's avatar
David Bühler committed
628
  | Itv itv -> Itv (Int_interval.add_singleton_int i itv)
629

David Bühler's avatar
David Bühler committed
630
let add_int v1 v2 =
631 632
  match v1,v2 with
  | Float _, _ | _, Float _ -> assert false
David Bühler's avatar
David Bühler committed
633
  | Set s1, Set s2 -> inject_set_or_top (Int_set.add s1 s2)
David Bühler's avatar
David Bühler committed
634
  | Itv i1, Itv i2 -> Itv (Int_interval.add i1 i2)
David Bühler's avatar
David Bühler committed
635
  | Set s, Itv i | Itv i, Set s ->
David Bühler's avatar
David Bühler committed
636 637 638 639 640 641 642 643
    let l = Int_set.cardinal s in
    if l = 0
    then bottom
    else if l = 1
    then (* only one element *)
      Itv (Int_interval.add_singleton_int (Int_set.min s) i)
    else
      Itv (Int_interval.add i (make_itv_from_set s))
644 645 646

let add_int_under v1 v2 = match v1,v2 with
  | Float _, _ | _, Float _ -> assert false
David Bühler's avatar
David Bühler committed
647
  | Set s1, Set s2 -> inject_set_or_top (Int_set.add_under s1 s2)
David Bühler's avatar
David Bühler committed
648
  | Itv i1, Itv i2 -> inject_itv_or_bottom (Int_interval.add_under i1 i2)
David Bühler's avatar
David Bühler committed
649 650 651 652 653 654 655 656 657 658 659
  | Set s, Itv i | Itv i, Set s ->
    let l = Int_set.cardinal s in
    if l = 0
    then bottom
    else
      begin
        if l <> 1
        then log_imprecision "Ival.add_int_under";
        (* This is precise if [s] has only one element. Otherwise, this is not worse
           than another computation. *)
        Itv (Int_interval.add_singleton_int (Int_set.min s) i)
660 661 662 663 664 665
      end


let neg_int v =
  match v with
  | Float _ -> assert false
David Bühler's avatar
David Bühler committed
666
  | Set s -> Set (Int_set.neg s)
David Bühler's avatar
David Bühler committed
667
  | Itv i -> Itv (Int_interval.neg i)
668 669 670 671 672 673

let sub_int v1 v2 = add_int v1 (neg_int v2)
let sub_int_under v1 v2 = add_int_under v1 (neg_int v2)

let min_int s =
  match s with
David Bühler's avatar
David Bühler committed
674
  | Itv i -> fst (Int_interval.min_and_max i)
675
  | Set s -> 
David Bühler's avatar
David Bühler committed
676 677 678
    if Int_set.cardinal s = 0
    then raise Error_Bottom
    else Some (Int_set.min s)
679 680 681 682 683
  | Float _ -> None


let max_int s =
  match s with
David Bühler's avatar
David Bühler committed
684
  | Itv i -> snd (Int_interval.min_and_max i)
David Bühler's avatar
David Bühler committed
685 686 687 688
  | Set s ->
    if Int_set.cardinal s = 0
    then raise Error_Bottom
    else Some (Int_set.max s)
689 690 691 692 693 694 695 696 697 698
  | Float _ -> None


(* TODO: rename this function to scale_int *)
let scale f v =
  if Int.is_zero f
  then zero
  else
    match v with
    | Float _ -> top
David Bühler's avatar
David Bühler committed
699
    | Itv i-> Itv (Int_interval.scale f i)
David Bühler's avatar
David Bühler committed
700
    | Set s -> Set (Int_set.scale f s)
701 702 703



David Bühler's avatar
David Bühler committed
704
let scale_div_common ~pos f v scale_interval degenerate_float =
705 706
  assert (not (Int.is_zero f));
  match v with
David Bühler's avatar
David Bühler committed
707
  | Itv i -> inject_itv_or_bottom (scale_interval ~pos f i)
David Bühler's avatar
David Bühler committed
708
  | Set s -> inject_set_or_bottom (Int_set.scale_div ~pos f s)
709 710 711
  | Float _ -> degenerate_float

let scale_div ~pos f v =
David Bühler's avatar
David Bühler committed
712 713
  let scale_div ~pos f x = `Value (Int_interval.scale_div ~pos f x) in
  scale_div_common ~pos f v scale_div top
714 715

let scale_div_under ~pos f v =
David Bühler's avatar
David Bühler committed
716 717 718
  (* TODO: a more precise result could be obtained by transforming
     Itv(min,max,r,m) into Itv(min,max,r/f,m/gcd(m,f)). But this is
     more complex to implement when pos or f is negative. *)
David Bühler's avatar
David Bühler committed
719
  scale_div_common ~pos f v Int_interval.scale_div_under bottom
720 721

let div_set x sy =
David Bühler's avatar
David Bühler committed
722
  Int_set.fold
723
    (fun acc elt ->
David Bühler's avatar
David Bühler committed
724 725 726
       if Int.is_zero elt
       then acc
       else join acc (scale_div ~pos:false elt x))
727 728 729 730 731 732 733 734
    bottom
    sy

let div x y =
  (*if (intersects y negative || intersects x negative) then ignore
    (CilE.warn_once "using 'round towards zero' semantics for '/',
    which only became specified in C99."); *)
  match y with
David Bühler's avatar
David Bühler committed
735 736
  | Set sy -> div_set x sy
  | Itv iy -> inject_itv_or_bottom (Int_interval.div (make_range x) iy)
737 738 739 740 741 742
  | Float _ -> assert false

(* [scale_rem ~pos:false f v] is an over-approximation of the set of
   elements [x mod f] for [x] in [v].

   [scale_rem ~pos:true f v] is an over-approximation of the set of
743
   elements [x e_rem f] for [x] in [v].
744 745 746 747 748
*)
let scale_rem ~pos f v =
  if Int.is_zero f then bottom
  else
    match v with
David Bühler's avatar
David Bühler committed
749
    | Itv i -> inject_itv_or_bottom (`Value (Int_interval.scale_rem ~pos f i))
David Bühler's avatar
David Bühler committed
750
    | Set s -> inject_set_or_top (Int_set.scale_rem ~pos f s)
751 752 753 754 755
    | Float _ -> top

let c_rem x y =
  match y with
  | Float _ -> top
David Bühler's avatar
David Bühler committed
756 757 758
  | Itv iy ->
    if is_bottom x then bottom
    else inject_itv_or_bottom (Int_interval.c_rem (make_range x) iy)
759
  | Set yy ->
David Bühler's avatar
David Bühler committed
760 761 762 763 764 765 766 767
    match x with
    | Set xx -> inject_set_or_top (Int_set.c_rem xx yy)
    | Float _ -> top
    | Itv _ ->
      let f acc y =
        join (scale_rem ~pos:false y x) acc
      in
      Int_set.fold f bottom yy
768 769 770 771 772 773 774

module AllValueHashtbl =
  Hashtbl.Make
    (struct
      type t = Int.t * bool * int
      let equal (a,b,c:t) (d,e,f:t) = b=e && c=f && Int.equal a d
      let hash (a,b,c:t) = 
David Bühler's avatar
David Bühler committed
775
        257 * (Hashtbl.hash b) + 17 * (Hashtbl.hash c) + Int.hash a
776 777 778 779 780 781 782
    end)

let all_values_table = AllValueHashtbl.create 7

let create_all_values_modu ~modu ~signed ~size =
  let t = modu, signed, size in
  try
David Bühler's avatar
David Bühler committed
783
    AllValueHashtbl.find all_values_table t
784 785 786 787 788
  with Not_found ->
    let mn, mx =
      if signed then
        let b = Int.two_power_of_int (size-1) in
        (Int.round_up_to_r ~min:(Int.neg b) ~modu ~r:Int.zero,
David Bühler's avatar
David Bühler committed
789
         Int.round_down_to_r ~max:(Int.pred b) ~modu ~r:Int.zero)
790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805
      else
        let b = Int.two_power_of_int size in
        Int.zero,
        Int.round_down_to_r ~max:(Int.pred b) ~modu ~r:Int.zero
    in
    let r = inject_top (Some mn) (Some mx) Int.zero modu in
    AllValueHashtbl.add all_values_table t r;
    r

let create_all_values ~signed ~size =
  if size <= !small_cardinal_log then
    (* We may need to create a set. Use slow path *)
    create_all_values_modu ~signed ~size ~modu:Int.one
  else
  if signed then
    let b = Int.two_power_of_int (size-1) in
David Bühler's avatar
David Bühler committed
806
    Itv (Int_interval.inject_range (Some (Int.neg b)) (Some (Int.pred b)))
807 808
  else
    let b = Int.two_power_of_int size in
David Bühler's avatar
David Bühler committed
809
    Itv (Int_interval.inject_range (Some Int.zero) (Some (Int.pred b)))
810 811 812 813 814 815 816 817

let big_int_64 = Int.of_int 64
let big_int_32 = Int.thirtytwo

let cast_int_to_int ~size ~signed value =
  if equal top value
  then create_all_values ~size:(Int.to_int size) ~signed
  else
David Bühler's avatar
David Bühler committed
818 819 820 821
    let result =
      let factor = Int.two_power size in
      let mask = Int.two_power (Int.pred size) in
      let rem_f value = Int.cast ~size ~signed ~value
822
      in
David Bühler's avatar
David Bühler committed
823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839
      let not_p_factor = Int.neg factor in
      let best_effort r m =
        let modu = Int.pgcd factor m in
        let rr = Int.e_rem r modu in
        let min_val = Some (if signed then
                              Int.round_up_to_r ~min:(Int.neg mask) ~r:rr ~modu
                            else
                              Int.round_up_to_r ~min:Int.zero ~r:rr ~modu)
        in
        let max_val = Some (if signed then
                              Int.round_down_to_r ~max:(Int.pred mask) ~r:rr ~modu
                            else
                              Int.round_down_to_r ~max:(Int.pred factor)
                                ~r:rr
                                ~modu)
        in
        inject_top min_val max_val rr modu
840
      in
David Bühler's avatar
David Bühler committed
841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867
      match value with
      | Itv i->
        begin
          let mn, mx, r, m = Int_interval.min_max_rem_modu i in
          match mn, mx with
          | Some mn, Some mx ->
            let highbits_mn,highbits_mx =
              if signed then
                Int.logand (Int.add mn mask) not_p_factor,
                Int.logand (Int.add mx mask) not_p_factor
              else
                Int.logand mn not_p_factor, Int.logand mx not_p_factor
            in
            if Int.equal highbits_mn highbits_mx
            then
              if Int.is_zero highbits_mn
              then value
              else
                let new_min = rem_f mn in
                let new_r = Int.e_rem new_min m in
                inject_top (Some new_min) (Some (rem_f mx)) new_r m
            else best_effort r m
          | _, _ -> best_effort r m
        end
      | Set s -> begin
          let all =
            create_all_values ~size:(Int.to_int size) ~signed
David Bühler's avatar
David Bühler committed
868
          in
David Bühler's avatar
David Bühler committed
869 870 871 872 873 874 875 876
          if is_included value all
          then value
          else Set (Int_set.map rem_f s)
        end
      | Float _ -> assert false
    in
    (* If sharing is no longer preserved, please change Cvalue.V.cast *)
    if equal result value then value else result
877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899

let reinterpret_float_as_int ~signed ~size f =
  let reinterpret_list l =
    let reinterpret_one (b, e) =
      let i = inject_range (Some b) (Some e) in
      cast_int_to_int ~size ~signed i
    in
    let l = List.map reinterpret_one l in
    List.fold_left join bottom l
  in
  if Int.equal size big_int_64
  then
    let itvs = Fval.bits_of_float64_list f in
    reinterpret_list itvs
  else
  if Int.equal size big_int_32
  then
    let itvs = Fval.bits_of_float32_list f in
    reinterpret_list itvs
  else top

let reinterpret_as_int ~size ~signed i =
  match i with
900
  | Set _ | Itv _ ->
901 902 903 904 905 906 907 908
    (* On integers, cast and reinterpretation are the same operation *)
    cast_int_to_int ~signed ~size i
  | Float f -> reinterpret_float_as_int ~signed ~size f

let cast_float_to_float fkind v =
  match v with
  | Float f ->
    begin match fkind with
David Bühler's avatar
David Bühler committed
909 910 911
      | Fval.Real | Fval.Long_Double | Fval.Double -> v
      | Fval.Single ->
        inject_float (Fval.round_to_single_precision_float f)
912 913
    end
  | Set _ when is_zero v -> zero
914
  | Set _ | Itv _ -> top_float
915 916


David Bühler's avatar
David Bühler committed
917
(* TODO rename to mul_int *)
David Bühler's avatar
David Bühler committed
918
let mul v1 v2 =
919 920 921 922 923 924 925 926
  (*    Format.printf "mul. Args: '%a' '%a'@\n" pretty v1 pretty v2; *)
  let result =
    if is_one v1 then v2 
    else if is_zero v2 || is_zero v1 then zero
    else if is_one v2 then v1 
    else
      match v1,v2 with
      | Float _, _ | _, Float _ ->
David Bühler's avatar
David Bühler committed
927
        top
David Bühler's avatar
David Bühler committed
928
      | Set s1, Set s2 -> inject_set_or_top (Int_set.mul s1 s2)
David Bühler's avatar
David Bühler committed
929 930
      | Itv i1, Itv i2 -> Itv (Int_interval.mul i1 i2)
      | Set s, Itv i | Itv i, Set s ->
David Bühler's avatar
David Bühler committed
931 932 933 934 935 936
        let l = Int_set.cardinal s in
        if l = 0
        then bottom
        else if l = 1
        then Itv (Int_interval.scale (Int_set.min s) i)
        else Itv (Int_interval.mul i (make_itv_from_set s))
937 938 939 940 941 942 943 944 945 946
  in
  (* Format.printf "mul. result : %a@\n" pretty result;*)
  result

(** Computes [x (op) ({y >= 0} * 2^n)], as an auxiliary function for
    [shift_left] and [shift_right]. [op] and [scale] must verify
    [scale a b == op (inject_singleton a) b] *)
let shift_aux scale op (x: t) (y: t) =
  let y = narrow (inject_range (Some Int.zero) None) y in
  try
David Bühler's avatar
David Bühler committed
947 948 949 950 951 952 953 954 955
    match y with
    | Set s ->
      Int_set.fold (fun acc n -> join acc (scale (Int.two_power n) x)) bottom s
    | _ ->
      let min_factor = Extlib.opt_map Int.two_power (min_int y) in
      let max_factor = Extlib.opt_map Int.two_power (max_int y) in
      let modu = match min_factor with None -> Int.one | Some m -> m in
      let factor = inject_top min_factor max_factor Int.zero modu in
      op x factor
956
  with Z.Overflow ->
957 958 959 960
    Lattice_messages.emit_imprecision emitter "Ival.shift_aux";
    (* We only preserve the sign of the result *)
    if is_included x positive_integers then positive_integers
    else
David Bühler's avatar
David Bühler committed
961 962
    if is_included x negative_integers then negative_integers
    else top
963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984

let shift_right x y = shift_aux (scale_div ~pos:true) div x y
let shift_left x y = shift_aux scale mul x y


let interp_boolean ~contains_zero ~contains_non_zero =
  match contains_zero, contains_non_zero with
  | true, true -> zero_or_one
  | true, false -> zero
  | false, true -> one
  | false, false -> bottom


module Infty = struct
  let lt0 = function
    | None -> true
    | Some a -> Int.lt a Int.zero

  let div a b = match a with
    | None -> None
    | Some a -> match b with
      | None -> Some Int.zero
985
      | Some b -> Some (Int.e_div a b)
986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039

  let neg = function
    | Some a -> Some (Int.neg a)
    | None -> None
end

let backward_mult_pos_left min_right max_right result =
  let min_res, max_res = min_and_max result in
  let min_left =
    Infty.div min_res (if Infty.lt0 min_res then Some min_right else max_right)
  and max_left =
    Infty.div max_res (if Infty.lt0 max_res then max_right else Some min_right)
  in
  inject_range min_left max_left

let backward_mult_neg_left min_right max_right result =
  backward_mult_pos_left (Integer.neg max_right) (Infty.neg min_right) (neg_int result)

let backward_mult_int_left ~right ~result =
  match min_and_max right with
  | None, None -> `Value None
  | Some a, Some b when a > b -> `Bottom

  | Some a, Some b when a = Int.zero && b = Int.zero ->
    if contains_zero result then `Value None else `Bottom

  | Some a, max when a > Int.zero ->
    `Value (Some (backward_mult_pos_left a max result))

  | Some a, max when a >= Int.zero ->
    if contains_zero result
    then `Value None
    else `Value (Some (backward_mult_pos_left Int.one max result))

  | min, Some b when b < Int.zero ->
    `Value (Some (backward_mult_neg_left min b result))

  | min, Some b when b = Int.zero ->
    if contains_zero result
    then `Value None
    else `Value (Some (backward_mult_neg_left min Int.minus_one result))

  | min, max ->
    if contains_zero result
    then `Value None
    else
      `Value (Some (join
                      (backward_mult_pos_left Int.one max result)
                      (backward_mult_neg_left min Int.one result)))


let backward_le_int max v =
  match v with
  | Float _ -> v
David Bühler's avatar
David Bühler committed
1040
  | Set _ | Itv _ -> narrow v (Itv (Int_interval.inject_range None max))
1041 1042 1043 1044

let backward_ge_int min v =
  match v with
  | Float _ -> v
David Bühler's avatar
David Bühler committed
1045
  | Set _ | Itv _ -> narrow v (Itv (Int_interval.inject_range min None))
1046

David Bühler's avatar
David Bühler committed
1047 1048
let backward_lt_int max v = backward_le_int (Extlib.opt_map Int.pred max) v
let backward_gt_int min v = backward_ge_int (Extlib.opt_map Int.succ min) v
1049

David Bühler's avatar
David Bühler committed
1050 1051 1052
let diff_if_one value rem =
  match rem with
  | Set s when Int_set.cardinal s = 1 ->
David Bühler's avatar
David Bühler committed
1053
    begin
David Bühler's avatar
David Bühler committed
1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078
      let v = Int_set.