<commit_before>open GobConfig
open Pretty
open IntervalOps
open CircularInterval
open CircularIntOps
open IntOps

module GU = Goblintutil
module JB = Json
module M = Messages

let (%) = Batteries.(%)
let (|?) = Batteries.(|?)

module type Arith =
sig
  type t
  val neg: t -> t
  val add: t -> t -> t
  val sub: t -> t -> t
  val mul: t -> t -> t
  val div: t -> t -> t
  val rem: t -> t -> t

  val lt: t -> t -> t
  val gt: t -> t -> t
  val le: t -> t -> t
  val ge: t -> t -> t
  val eq: t -> t -> t
  val ne: t -> t -> t

  val bitnot: t -> t
  val bitand: t -> t -> t
  val bitor : t -> t -> t
  val bitxor: t -> t -> t

  val shift_left : t -> t -> t
  val shift_right: t -> t -> t

  val lognot: t -> t
  val logand: t -> t -> t
  val logor : t -> t -> t

end

module type ArithIkind =
sig
  type t
  val neg: Cil.ikind -> t -> t
  val add: Cil.ikind -> t -> t -> t
  val sub: Cil.ikind -> t -> t -> t
  val mul: Cil.ikind -> t -> t -> t
  val div: Cil.ikind -> t -> t -> t
  val rem: Cil.ikind -> t -> t -> t

  val lt: Cil.ikind -> t -> t -> t
  val gt: Cil.ikind -> t -> t -> t
  val le: Cil.ikind -> t -> t -> t
  val ge: Cil.ikind -> t -> t -> t
  val eq: Cil.ikind -> t -> t -> t
  val ne: Cil.ikind -> t -> t -> t

  val bitnot: Cil.ikind -> t -> t
  val bitand: Cil.ikind -> t -> t -> t
  val bitor : Cil.ikind -> t -> t -> t
  val bitxor: Cil.ikind -> t -> t -> t

  val shift_left : Cil.ikind -> t -> t -> t
  val shift_right: Cil.ikind -> t -> t -> t

  val lognot: Cil.ikind -> t -> t
  val logand: Cil.ikind -> t -> t -> t
  val logor : Cil.ikind -> t -> t -> t

end

(* Shared functions between S and Z *)
module type B =
sig
  include Lattice.S
  type int_t
  val bot_of: Cil.ikind -> t
  val top_of: Cil.ikind -> t
  val to_int: t -> int_t option
  val is_int: t -> bool
  val equal_to: int_t -> t -> [`Eq | `Neq | `Top]

  val to_bool: t -> bool option
  val is_bool: t -> bool
  val to_excl_list: t -> int_t list option
  val of_excl_list: Cil.ikind -> int_t list -> t
  val is_excl_list: t -> bool

  val maximal    : t -> int_t option
  val minimal    : t -> int_t option

  val cast_to: ?torg:Cil.typ -> Cil.ikind -> t -> t
end


module type IkindUnawareS =
sig
  include B with type int_t = int64
  include Arith with type t:= t
  val starting   : Cil.ikind -> int_t -> t
  val ending     : Cil.ikind -> int_t -> t
  val of_int: int_t -> t
  val of_bool: bool -> t
  val of_interval: Cil.ikind -> int_t * int_t -> t
end
(** Interface of IntDomain implementations that do not take ikinds for arithmetic operations yet.
   TODO: Should be ported to S in the future. *)

module type S =
sig
  include B
  include ArithIkind with type t:= t
  val join: Cil.ikind -> t -> t -> t
  val meet: Cil.ikind -> t -> t -> t
  val narrow: Cil.ikind -> t -> t -> t
  val widen: Cil.ikind -> t -> t -> t
  val starting : Cil.ikind -> int_t -> t
  val ending : Cil.ikind -> int_t -> t
  val of_int: Cil.ikind -> int_t -> t
  val of_bool: Cil.ikind -> bool -> t
  val of_interval: Cil.ikind -> int_t * int_t -> t
end
(** Interface of IntDomain implementations taking an ikind for arithmetic operations *)

module type Y =
sig
  (* include B *)
  include B
  include Arith with type t:= t
  val of_int: Cil.ikind -> int_t -> t
  val of_bool: Cil.ikind -> bool -> t
  val of_interval: Cil.ikind -> int_t * int_t -> t

  val starting   : Cil.ikind -> int_t -> t
  val ending     : Cil.ikind -> int_t -> t
end

module type Z = Y with type int_t = IntOps.BigIntOps.t

module OldDomainFacade (Old : IkindUnawareS) : S with type int_t = BigIntOps.t and type t = Old.t =
struct
  include Old
  type int_t = IntOps.BigIntOps.t
  let neg _ik = Old.neg
  let add _ik = Old.add
  let sub _ik = Old.sub
  let mul _ik = Old.mul
  let div _ik = Old.div
  let rem _ik = Old.rem

  let lt _ik = Old.lt
  let gt _ik = Old.gt
  let le _ik = Old.le
  let ge _ik = Old.ge
  let eq _ik = Old.eq
  let ne _ik = Old.ne

  let bitnot _ik = bitnot
  let bitand _ik = bitand
  let bitor  _ik = bitor
  let bitxor _ik = bitxor

  let shift_left  _ik = shift_left
  let shift_right _ik = shift_right

  let lognot _ik = lognot
  let logand _ik = logand
  let logor  _ik = logor


  let to_int a = Option.map BigIntOps.of_int64 (Old.to_int a)

  let equal_to (x: int_t) (a: t)=
    try
      Old.equal_to (BigIntOps.to_int64 x) a
    with e -> `Top

  let to_excl_list a = Option.map (List.map BigIntOps.of_int64) (Old.to_excl_list a)
  let of_excl_list ik xs =
    let xs' = List.map BigIntOps.to_int64 xs in
    Old.of_excl_list ik xs'

  let maximal a = Option.map BigIntOps.of_int64 (Old.maximal a)
  let minimal a = Option.map BigIntOps.of_int64 (Old.minimal a)

  let of_int ik x =
    (* If we cannot convert x to int64, we have to represent it with top in the underlying domain*)
    try
      Old.of_int (BigIntOps.to_int64 x)
    with
      Failure _ -> top_of ik

  let of_bool ik b = Old.of_bool b
  let of_interval ik (l, u) =
    try
      Old.of_interval ik (BigIntOps.to_int64 l, BigIntOps.to_int64 u)
    with
      Failure _ -> top_of ik

  let starting ik x =
    try Old.starting ik (BigIntOps.to_int64 x) with Failure _ -> top_of ik
  let ending ik x =
    try Old.ending ik (BigIntOps.to_int64 x) with Failure _ -> top_of ik

  let join _ik = Old.join
  let meet _ik = Old.meet
  let narrow _ik = Old.narrow
  let widen _ik = Old.widen

end


module IntDomLifter (I : S) (*: Z with type int_t = I.int_t and type t =  'a { v : I.t; ikind : ikind } *)=
struct
  open Cil
  type int_t = I.int_t
  type t = { v : I.t; ikind : ikind }

  (* Helper functions *)
  let check_ikinds x y = if x.ikind <> y.ikind then failwith ("ikinds " ^ Prelude.Ana.sprint Cil.d_ikind x.ikind ^ " and " ^ Prelude.Ana.sprint Cil.d_ikind y.ikind ^ " are incompatible. Values: " ^ Prelude.Ana.sprint I.pretty x.v ^ " and " ^ Prelude.Ana.sprint I.pretty y.v ) else ()
  let lift op x = {x with v = op x.ikind x.v }
  (* For logical operations the result is of type int *)
  let lift_logical op x = {v = op x.ikind x.v; ikind = Cil.IInt}
  let lift2 op x y = check_ikinds x y; {x with v = op x.ikind x.v y.v }
  let lift2_cmp op x y = check_ikinds x y; {v = op x.ikind x.v y.v; ikind = Cil.IInt}

  let bot_of ikind = { v = I.bot_of ikind; ikind}
  let bot () = failwith "bot () is not implemented for IntDomLifter."
  let is_bot x = I.is_bot x.v
  let top_of ikind = { v = I.top_of ikind; ikind}
  let top () = failwith "top () is not implemented for IntDomLifter."
  let is_top x = I.is_top x.v

  (* Leq does not check for ikind, because it is used in invariant with arguments of different type.
     TODO: check ikinds here and fix invariant to work with right ikinds *)
  let leq x y = I.leq x.v y.v
  let join = lift2 I.join
  let meet = lift2 I.meet
  let widen = lift2 I.widen
  let narrow = lift2 I.narrow
  let equal x y = if x.ikind <> y.ikind then false else I.equal x.v y.v

  let hash x =
    let ikind_to_int (ikind: ikind) = match ikind with
    | IChar 	-> 0
    | ISChar 	-> 1
    | IUChar 	-> 2
    | IBool 	-> 3
    | IInt 	  -> 4
    | IUInt 	-> 5
    | IShort 	-> 6
    | IUShort -> 7
    | ILong 	-> 8
    | IULong 	-> 9
    | ILongLong -> 10
    | IULongLong -> 11
    in
    3 * (I.hash x.v) + 5 * (ikind_to_int x.ikind)
  let compare x y = let ik_c = compare x.ikind y.ikind in
    if ik_c <> 0
      then ik_c
      else I.compare x.v y.v
  let short l x = I.short l x.v  (* TODO add ikind to output *)
  let isSimple x = I.isSimple x.v
  let pretty () x = I.pretty () x.v (* TODO add ikind to output *)
  let pretty_diff () (x, y) = I.pretty_diff () (x.v, y.v) (* TODO check ikinds, add them to output *)
  let pretty_f f () x = pretty () x (* TODO add ikind to output *)
  let printXml o x = I.printXml o x.v (* TODO add ikind to output *)
  (* This is for debugging *)
  let name () = "IntDomLifter(" ^ (I.name ()) ^ ")"
  let to_yojson x = I.to_yojson x.v
  let invariant c x = I.invariant c x.v
  let tag x = I.tag x.v
  let arbitrary () = failwith @@ "Arbitrary not implement for " ^ (name ()) ^ "."
  let to_int x = I.to_int x.v
  let of_int ikind x = { v = I.of_int ikind x; ikind}
  let is_int x = I.is_int x.v
  let equal_to i x = I.equal_to i x.v
  let to_bool x = I.to_bool x.v
  let of_bool ikind b = { v = I.of_bool ikind b; ikind}
  let is_bool x = I.is_bool x.v
  let to_excl_list x = I.to_excl_list x.v
  let of_excl_list ikind is = {v = I.of_excl_list ikind is; ikind}
  let is_excl_list x = I.is_excl_list x.v
  let of_interval ikind (lb,ub) = {v = I.of_interval ikind (lb,ub); ikind}
  let starting ikind i = {v = I.starting ikind i; ikind}
  let ending ikind i = {v = I.ending ikind i; ikind}
  let maximal x = I.maximal x.v
  let minimal x = I.minimal x.v

  let neg = lift I.neg
  let add = lift2 I.add
  let sub = lift2 I.sub
  let mul = lift2 I.mul
  let div = lift2 I.div
  let rem = lift2 I.rem
  let lt = lift2_cmp I.lt
  let gt = lift2_cmp I.gt
  let le = lift2_cmp I.le
  let ge = lift2_cmp I.ge
  let eq = lift2_cmp I.eq
  let ne = lift2_cmp I.ne
  let bitnot = lift I.bitnot
  let bitand = lift2 I.bitand
  let bitor = lift2 I.bitor
  let bitxor = lift2 I.bitxor
  let shift_left x y = {x with v = I.shift_left x.ikind x.v y.v } (* TODO check ikinds*)
  let shift_right x y = {x with v = I.shift_right x.ikind x.v y.v } (* TODO check ikinds*)
  let lognot = lift_logical I.lognot
  let logand = lift2 I.logand
  let logor = lift2 I.logor

  let cast_to ?torg ikind x = {v = I.cast_to ?torg ikind x.v; ikind}

end

module type Ikind =
sig
  val ikind: unit -> Cil.ikind
end

module PtrDiffIkind : Ikind =
struct
  let ikind = Cilfacade.ptrdiff_ikind
end

module IntDomWithDefaultIkind (I: Y) (Ik: Ikind) : Y with type t = I.t and type int_t = I.int_t =
struct
  include I
  let top () = I.top_of (Ik.ikind ())
  let bot () = I.bot_of (Ik.ikind ())
end

module Size = struct (* size in bits as int, range as int64 *)
  exception Not_in_int64
  open Cil open Int64 open Big_int_Z
  let sign x = if x<0L then `Signed else `Unsigned
  let max = function
    | `Signed -> ILongLong
    | `Unsigned -> IULongLong
  let top_typ = TInt (ILongLong, [])
  let min_for x = intKindForValue (mkCilint (max (sign x)) x) (sign x = `Unsigned)
  let bit = function (* bits needed for representation *)
    | IBool -> 1
    | ik -> bytesSizeOfInt ik * 8
  let is_int64_big_int x = try let _ = int64_of_big_int x in true with _ -> false
  let card ik = (* cardinality *)
    let b = bit ik in
    shift_left_big_int unit_big_int b
  let bits ik = (* highest bits for neg/pos values *)
    let s = bit ik in
    if isSigned ik then s-1, s-1 else 0, s
  let bits_i64 ik = BatTuple.Tuple2.mapn of_int (bits ik)
  let range ik = (* min/max values as int64 (signed), anything bigger is cropped! *)
    let a,b = bits ik in
    if a>63 || b>63 then raise Not_in_int64 else
      let x = if isSigned ik then neg (shift_left 1L a) (* -2^a *) else 0L in
      let y = sub (shift_left 1L b) 1L in (* 2^b - 1 *)
      x,y
  let range_big_int ik =
    let a,b = bits ik in
    let x = if isSigned ik then minus_big_int (shift_left_big_int unit_big_int a) (* -2^a *) else zero_big_int in
    let y = sub_big_int (shift_left_big_int unit_big_int b) unit_big_int in (* 2^b - 1 *)
    x,y
  let cast_big_int t x = (* TODO: overflow is implementation-dependent! *)
    let a,b = range_big_int t in
    let c = card t in
    (* let z = add (rem (sub x a) c) a in (* might lead to overflows itself... *)*)
    let y = mod_big_int x c in
    let y = if gt_big_int y b then sub_big_int y c
      else if lt_big_int y a then add_big_int y c
      else y
    in
    M.tracel "cast_int" "Cast %s to range [%s, %s] (%s) = %s (%s in int64)\n" (string_of_big_int x) (string_of_big_int a) (string_of_big_int b) (string_of_big_int c) (string_of_big_int y) (if is_int64_big_int y then "fits" else "does not fit");
    y
  let cast t x =
    let x' = big_int_of_int64 x in
    try int64_of_big_int (cast_big_int t x') with _ -> raise Not_in_int64

  let min_range_sign_agnostic x =
    let size ik =
      let a,b = bits_i64 ik in
      Int64.neg a,b
    in
    if sign x = `Signed then
      size (min_for x)
    else
      let a, b = size (min_for x) in
      if b <= 64L then
        let upper_bound_less = Int64.sub b 1L in
        let max_one_less = Int64.(pred @@ shift_left 1L (to_int upper_bound_less)) in
        if x < max_one_less then
          a, upper_bound_less
        else
          a,b
      else
        a, b
end

exception Unknown
exception Error
exception ArithmeticOnIntegerBot of string

module StdTop (B: sig type t val top_of: Cil.ikind -> t end) = struct
  open B
  (* these should be overwritten for better precision if possible: *)
  let to_excl_list    x = None
  let of_excl_list ik x = top_of ik
  let is_excl_list    x = false
  let of_interval  ik x = top_of ik
  let starting     ik x = top_of ik
  let ending       ik x = top_of ik
  let maximal         x = None
  let minimal         x = None
end

module Std (B: sig
    type t
    val name: unit -> string
    val top_of: Cil.ikind -> t
    val bot_of: Cil.ikind -> t
    val short: int -> t -> string
    val equal: t -> t -> bool
  end) = struct
  include Printable.Std
  let name = B.name (* overwrite the one from Printable.Std *)
  open B
  let isSimple _ = true
  let hash = Hashtbl.hash
  let is_top x = failwith "is_top not implemented for IntDomain.Std"
  let is_bot x = B.equal x (bot_of Cil.IInt) (* Here we assume that the representation of bottom is independent of the ikind
                                                This may be true for intdomain implementations, but not e.g. for IntDomLifter. *)
  let is_top_of ik x = B.equal x (top_of ik)
  (* let is_bot_of ik x = B.equal x (bot_of ik) *)

  (* all output is based on B.short *)
  let pretty_f sh () x = text (sh Goblintutil.summary_length x)
  let pretty = pretty_f short
  let pretty_diff () (x,y) = dprintf "%s: %a instead of %a" (name ()) pretty x pretty y
  let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (short 800 x)

  include StdTop (B)
end
(* include Std (struct type nonrec t = t let name = name let top = top let bot = bot let short = short end) *)


module IntervalFunctor(Ints_t : IntOps): S with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =
struct
  let name () = "intervals"
  type int_t = Ints_t.t
  type t = (Ints_t.t * Ints_t.t) option
  let to_yojson t = failwith "to yojson unimplemented"

  let min_int ik = Ints_t.of_bigint @@ fst @@ Size.range_big_int ik
  let max_int ik = Ints_t.of_bigint @@ snd @@ Size.range_big_int ik
  let top () = failwith @@ "top () not implemented for " ^ (name ())
  let top_of ik = Some (min_int ik, max_int ik)
  let bot () = None
  let bot_of ik = bot () (* TODO: improve *)

  let is_top x = failwith "is_top not implemented for intervals"

  let is_bot x  = failwith "is_bot not implemented for intervals"

  let short _ = function None -> "bottom" | Some (x,y) -> "["^Ints_t.to_string x^","^Ints_t.to_string y^"]"

  let equal a b = match a, b with
    | None, None -> true
    | Some (a, b), Some (c, d) -> Ints_t.equal a c && Ints_t.equal b d
    | _, _ -> false

  include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let short = short let equal = equal end)

  let equal_to i = function
    | None -> failwith "unsupported: equal_to with bottom"
    | Some (a, b) ->
      if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq

  let norm ik = function None -> None | Some (x,y) ->
    if Ints_t.compare x y > 0 then None
    else if Ints_t.compare (min_int ik) x > 0 || Ints_t.compare (max_int ik) y < 0 then top_of ik
    else Some (x,y)

  let leq (x:t) (y:t) =
    match x, y with
    | None, _ -> true
    | Some _, None -> false
    | Some (x1,x2), Some (y1,y2) -> Ints_t.compare x1 y1 >= 0 && Ints_t.compare x2 y2 <= 0

  let join ik (x:t) y =
    match x, y with
    | None, z | z, None -> z
    | Some (x1,x2), Some (y1,y2) -> norm ik @@ Some (min x1 y1, max x2 y2)

  let meet ik (x:t) y =
    match x, y with
    | None, z | z, None -> None
    | Some (x1,x2), Some (y1,y2) -> norm ik @@ Some (max x1 y1, min x2 y2)

  let is_int = function Some (x,y) when Ints_t.compare x y = 0 -> true | _ -> false

  (* TODO: change to_int signature so it returns a big_int *)
  let to_int = function Some (x,y) when Ints_t.compare x y = 0 -> Some x | _ -> None
  let of_interval ik (x,y) = norm ik @@ Some (x,y)
  let of_int ik (x: int_t) = of_interval ik (x,x)
  let zero = Some (Ints_t.zero, Ints_t.zero)
  let one  = Some (Ints_t.one, Ints_t.one)
  let top_bool = Some (Ints_t.zero, Ints_t.one)

  let of_bool _ik = function true -> one | false -> zero
  let is_bool x = x <> None && not (leq zero x) || equal x zero
  let to_bool (a: t) = match a with
    | None -> None
    | Some (l, u) when Ints_t.compare l Ints_t.zero = 0 && Ints_t.compare u Ints_t.zero = 0 -> Some false
    | x -> if leq zero x then None else Some true
  let to_bool_interval x = match x with
    | None -> x
    | Some (l, u) when Ints_t.compare l Ints_t.zero = 0 && Ints_t.compare u Ints_t.zero = 0 -> x
    | _ -> if leq zero x then top_bool else one

  let range_opt f = function
    | None -> None
    | Some ik -> Some (Ints_t.of_bigint @@ f @@ Size.range_big_int ik)

  let starting ik n =
    (norm ik) @@ Some (n, range_opt snd (Some ik) |? (max_int ik))

  let ending ik n =
    norm ik @@ Some (range_opt fst (Some ik) |? min_int ik, n)

  (* TODO: change signarue of maximal, minimal to return big_int*)
  let maximal = function None -> None | Some (x,y) -> Some y
  let minimal = function None -> None | Some (x,y) -> Some x

  let cast_to ?torg t = function
    | None -> None
    | Some (x,y) ->
      try
        let a = Ints_t.of_bigint @@ Size.cast_big_int t (Ints_t.to_bigint x) in
        let b = Ints_t.of_bigint @@ Size.cast_big_int t (Ints_t.to_bigint y) in
        let a,b = if Ints_t.compare x a <> 0 || Ints_t.compare y b <> 0 then Size.range_big_int t |> (fun (a, b) -> (Ints_t.of_bigint a, Ints_t.of_bigint b)) else a,b in
        norm t @@ Some (a, b)
      with Size.Not_in_int64 -> top_of t

  let widen ik x y =
    match x, y with
    | None, z | z, None -> z
    | Some (l0,u0), Some (l1,u1) ->
      let l2 = if Ints_t.compare l0 l1 = 0 then l0 else min l1 (min_int ik) in
      let u2 = if Ints_t.compare u0 u1 = 0 then u0 else max u1 (max_int ik) in
      norm ik @@ Some (l2,u2)

  let narrow ik x y =
    match x, y with
    | _,None | None, _ -> None
    | Some (x1,x2), Some (y1,y2) ->
      let lr = if Ints_t.compare (min_int ik) x1 = 0 then y1 else x1 in
      let ur = if Ints_t.compare (max_int ik) x2 = 0 then y2 else x2 in
      norm ik @@ Some (lr,ur)

  let log f ik i1 i2 =
    match is_bot i1, is_bot i2 with
    | true, true -> bot_of ik
    | true, _
    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 i1) (short 80 i2)))
    | _ ->
      match to_bool i1, to_bool i2 with
      | Some x, Some y -> of_bool ik (f x y)
      | _              -> top_of ik

  let logor = log (||)
  let logand = log (&&)

  let log1 f ik i1 =
    if is_bot i1 then
      bot_of ik
    else
      match to_bool i1 with
      | Some x -> of_bool ik (f ik x)
      | _      -> top_of ik

  let lognot = log1 (fun _ik -> not)

  let bit f ik i1 i2 =
    match is_bot i1, is_bot i2 with
    | true, true -> bot_of ik
    | true, _
    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 i1) (short 80 i2)))
    | _ ->
      match to_int i1, to_int i2 with
      | Some x, Some y -> (try norm ik (of_int ik (f ik x y)) with Division_by_zero -> top_of ik)
      | _              -> top_of ik

  let bitxor = bit (fun _ik -> Ints_t.logxor)
  let bitand = bit (fun _ik -> Ints_t.logand)
  let bitor  = bit (fun _ik -> Ints_t.logor)

  let bit1 f ik i1 =
    if is_bot i1 then
      bot_of ik
    else
      match to_int i1 with
      | Some x -> of_int ik (f ik x)
      | _      -> top_of ik

  let bitnot = bit1 (fun _ik -> Ints_t.lognot)
  let shift_right = bit (fun _ik x y -> Ints_t.shift_right x (Ints_t.to_int y))
  let shift_left  = bit (fun _ik x y -> Ints_t.shift_left  x (Ints_t.to_int y))

  let neg ik = function None -> None | Some (x,y) -> norm ik @@ Some (Ints_t.neg y, Ints_t.neg x)

  let add ik x y =
    match x, y with
    | None, None -> None
    | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))
    | Some (x1,x2), Some (y1,y2) -> norm ik @@ Some (Ints_t.add x1 y1, Ints_t.add x2 y2)

  let sub ik i1 i2 = add ik i1 (neg ik i2)

  let rem ik x y = match x, y with
    | None, None -> None
    | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))
    | Some (xl, xu), Some (yl, yu) ->
      if is_top_of ik x && is_top_of ik y then
        (* This is needed to preserve soundness also on things bigger than int32 e.g.  *)
        (* x:     3803957176L -> T in Interval32 *)
        (* y:     4209861404L -> T in Interval32 *)
        (* x % y: 3803957176L -> T in Interval32 *)
        (* T in Interval32 is [-2147483648,2147483647] *)
        (* the code below computes [-2147483647,2147483647] for this though which is unsound *)
        top_of ik
      else
        (* If we have definite values, Ints_t.rem will give a definite result.<commit_msg>Interval: Fix sub. Didn't work for unsigned previously<commit_after>open GobConfig
open Pretty
open IntervalOps
open CircularInterval
open CircularIntOps
open IntOps

module GU = Goblintutil
module JB = Json
module M = Messages

let (%) = Batteries.(%)
let (|?) = Batteries.(|?)

module type Arith =
sig
  type t
  val neg: t -> t
  val add: t -> t -> t
  val sub: t -> t -> t
  val mul: t -> t -> t
  val div: t -> t -> t
  val rem: t -> t -> t

  val lt: t -> t -> t
  val gt: t -> t -> t
  val le: t -> t -> t
  val ge: t -> t -> t
  val eq: t -> t -> t
  val ne: t -> t -> t

  val bitnot: t -> t
  val bitand: t -> t -> t
  val bitor : t -> t -> t
  val bitxor: t -> t -> t

  val shift_left : t -> t -> t
  val shift_right: t -> t -> t

  val lognot: t -> t
  val logand: t -> t -> t
  val logor : t -> t -> t

end

module type ArithIkind =
sig
  type t
  val neg: Cil.ikind -> t -> t
  val add: Cil.ikind -> t -> t -> t
  val sub: Cil.ikind -> t -> t -> t
  val mul: Cil.ikind -> t -> t -> t
  val div: Cil.ikind -> t -> t -> t
  val rem: Cil.ikind -> t -> t -> t

  val lt: Cil.ikind -> t -> t -> t
  val gt: Cil.ikind -> t -> t -> t
  val le: Cil.ikind -> t -> t -> t
  val ge: Cil.ikind -> t -> t -> t
  val eq: Cil.ikind -> t -> t -> t
  val ne: Cil.ikind -> t -> t -> t

  val bitnot: Cil.ikind -> t -> t
  val bitand: Cil.ikind -> t -> t -> t
  val bitor : Cil.ikind -> t -> t -> t
  val bitxor: Cil.ikind -> t -> t -> t

  val shift_left : Cil.ikind -> t -> t -> t
  val shift_right: Cil.ikind -> t -> t -> t

  val lognot: Cil.ikind -> t -> t
  val logand: Cil.ikind -> t -> t -> t
  val logor : Cil.ikind -> t -> t -> t

end

(* Shared functions between S and Z *)
module type B =
sig
  include Lattice.S
  type int_t
  val bot_of: Cil.ikind -> t
  val top_of: Cil.ikind -> t
  val to_int: t -> int_t option
  val is_int: t -> bool
  val equal_to: int_t -> t -> [`Eq | `Neq | `Top]

  val to_bool: t -> bool option
  val is_bool: t -> bool
  val to_excl_list: t -> int_t list option
  val of_excl_list: Cil.ikind -> int_t list -> t
  val is_excl_list: t -> bool

  val maximal    : t -> int_t option
  val minimal    : t -> int_t option

  val cast_to: ?torg:Cil.typ -> Cil.ikind -> t -> t
end


module type IkindUnawareS =
sig
  include B with type int_t = int64
  include Arith with type t:= t
  val starting   : Cil.ikind -> int_t -> t
  val ending     : Cil.ikind -> int_t -> t
  val of_int: int_t -> t
  val of_bool: bool -> t
  val of_interval: Cil.ikind -> int_t * int_t -> t
end
(** Interface of IntDomain implementations that do not take ikinds for arithmetic operations yet.
   TODO: Should be ported to S in the future. *)

module type S =
sig
  include B
  include ArithIkind with type t:= t
  val join: Cil.ikind -> t -> t -> t
  val meet: Cil.ikind -> t -> t -> t
  val narrow: Cil.ikind -> t -> t -> t
  val widen: Cil.ikind -> t -> t -> t
  val starting : Cil.ikind -> int_t -> t
  val ending : Cil.ikind -> int_t -> t
  val of_int: Cil.ikind -> int_t -> t
  val of_bool: Cil.ikind -> bool -> t
  val of_interval: Cil.ikind -> int_t * int_t -> t
end
(** Interface of IntDomain implementations taking an ikind for arithmetic operations *)

module type Y =
sig
  (* include B *)
  include B
  include Arith with type t:= t
  val of_int: Cil.ikind -> int_t -> t
  val of_bool: Cil.ikind -> bool -> t
  val of_interval: Cil.ikind -> int_t * int_t -> t

  val starting   : Cil.ikind -> int_t -> t
  val ending     : Cil.ikind -> int_t -> t
end

module type Z = Y with type int_t = IntOps.BigIntOps.t

module OldDomainFacade (Old : IkindUnawareS) : S with type int_t = BigIntOps.t and type t = Old.t =
struct
  include Old
  type int_t = IntOps.BigIntOps.t
  let neg _ik = Old.neg
  let add _ik = Old.add
  let sub _ik = Old.sub
  let mul _ik = Old.mul
  let div _ik = Old.div
  let rem _ik = Old.rem

  let lt _ik = Old.lt
  let gt _ik = Old.gt
  let le _ik = Old.le
  let ge _ik = Old.ge
  let eq _ik = Old.eq
  let ne _ik = Old.ne

  let bitnot _ik = bitnot
  let bitand _ik = bitand
  let bitor  _ik = bitor
  let bitxor _ik = bitxor

  let shift_left  _ik = shift_left
  let shift_right _ik = shift_right

  let lognot _ik = lognot
  let logand _ik = logand
  let logor  _ik = logor


  let to_int a = Option.map BigIntOps.of_int64 (Old.to_int a)

  let equal_to (x: int_t) (a: t)=
    try
      Old.equal_to (BigIntOps.to_int64 x) a
    with e -> `Top

  let to_excl_list a = Option.map (List.map BigIntOps.of_int64) (Old.to_excl_list a)
  let of_excl_list ik xs =
    let xs' = List.map BigIntOps.to_int64 xs in
    Old.of_excl_list ik xs'

  let maximal a = Option.map BigIntOps.of_int64 (Old.maximal a)
  let minimal a = Option.map BigIntOps.of_int64 (Old.minimal a)

  let of_int ik x =
    (* If we cannot convert x to int64, we have to represent it with top in the underlying domain*)
    try
      Old.of_int (BigIntOps.to_int64 x)
    with
      Failure _ -> top_of ik

  let of_bool ik b = Old.of_bool b
  let of_interval ik (l, u) =
    try
      Old.of_interval ik (BigIntOps.to_int64 l, BigIntOps.to_int64 u)
    with
      Failure _ -> top_of ik

  let starting ik x =
    try Old.starting ik (BigIntOps.to_int64 x) with Failure _ -> top_of ik
  let ending ik x =
    try Old.ending ik (BigIntOps.to_int64 x) with Failure _ -> top_of ik

  let join _ik = Old.join
  let meet _ik = Old.meet
  let narrow _ik = Old.narrow
  let widen _ik = Old.widen

end


module IntDomLifter (I : S) (*: Z with type int_t = I.int_t and type t =  'a { v : I.t; ikind : ikind } *)=
struct
  open Cil
  type int_t = I.int_t
  type t = { v : I.t; ikind : ikind }

  (* Helper functions *)
  let check_ikinds x y = if x.ikind <> y.ikind then failwith ("ikinds " ^ Prelude.Ana.sprint Cil.d_ikind x.ikind ^ " and " ^ Prelude.Ana.sprint Cil.d_ikind y.ikind ^ " are incompatible. Values: " ^ Prelude.Ana.sprint I.pretty x.v ^ " and " ^ Prelude.Ana.sprint I.pretty y.v ) else ()
  let lift op x = {x with v = op x.ikind x.v }
  (* For logical operations the result is of type int *)
  let lift_logical op x = {v = op x.ikind x.v; ikind = Cil.IInt}
  let lift2 op x y = check_ikinds x y; {x with v = op x.ikind x.v y.v }
  let lift2_cmp op x y = check_ikinds x y; {v = op x.ikind x.v y.v; ikind = Cil.IInt}

  let bot_of ikind = { v = I.bot_of ikind; ikind}
  let bot () = failwith "bot () is not implemented for IntDomLifter."
  let is_bot x = I.is_bot x.v
  let top_of ikind = { v = I.top_of ikind; ikind}
  let top () = failwith "top () is not implemented for IntDomLifter."
  let is_top x = I.is_top x.v

  (* Leq does not check for ikind, because it is used in invariant with arguments of different type.
     TODO: check ikinds here and fix invariant to work with right ikinds *)
  let leq x y = I.leq x.v y.v
  let join = lift2 I.join
  let meet = lift2 I.meet
  let widen = lift2 I.widen
  let narrow = lift2 I.narrow
  let equal x y = if x.ikind <> y.ikind then false else I.equal x.v y.v

  let hash x =
    let ikind_to_int (ikind: ikind) = match ikind with
    | IChar 	-> 0
    | ISChar 	-> 1
    | IUChar 	-> 2
    | IBool 	-> 3
    | IInt 	  -> 4
    | IUInt 	-> 5
    | IShort 	-> 6
    | IUShort -> 7
    | ILong 	-> 8
    | IULong 	-> 9
    | ILongLong -> 10
    | IULongLong -> 11
    in
    3 * (I.hash x.v) + 5 * (ikind_to_int x.ikind)
  let compare x y = let ik_c = compare x.ikind y.ikind in
    if ik_c <> 0
      then ik_c
      else I.compare x.v y.v
  let short l x = I.short l x.v  (* TODO add ikind to output *)
  let isSimple x = I.isSimple x.v
  let pretty () x = I.pretty () x.v (* TODO add ikind to output *)
  let pretty_diff () (x, y) = I.pretty_diff () (x.v, y.v) (* TODO check ikinds, add them to output *)
  let pretty_f f () x = pretty () x (* TODO add ikind to output *)
  let printXml o x = I.printXml o x.v (* TODO add ikind to output *)
  (* This is for debugging *)
  let name () = "IntDomLifter(" ^ (I.name ()) ^ ")"
  let to_yojson x = I.to_yojson x.v
  let invariant c x = I.invariant c x.v
  let tag x = I.tag x.v
  let arbitrary () = failwith @@ "Arbitrary not implement for " ^ (name ()) ^ "."
  let to_int x = I.to_int x.v
  let of_int ikind x = { v = I.of_int ikind x; ikind}
  let is_int x = I.is_int x.v
  let equal_to i x = I.equal_to i x.v
  let to_bool x = I.to_bool x.v
  let of_bool ikind b = { v = I.of_bool ikind b; ikind}
  let is_bool x = I.is_bool x.v
  let to_excl_list x = I.to_excl_list x.v
  let of_excl_list ikind is = {v = I.of_excl_list ikind is; ikind}
  let is_excl_list x = I.is_excl_list x.v
  let of_interval ikind (lb,ub) = {v = I.of_interval ikind (lb,ub); ikind}
  let starting ikind i = {v = I.starting ikind i; ikind}
  let ending ikind i = {v = I.ending ikind i; ikind}
  let maximal x = I.maximal x.v
  let minimal x = I.minimal x.v

  let neg = lift I.neg
  let add = lift2 I.add
  let sub = lift2 I.sub
  let mul = lift2 I.mul
  let div = lift2 I.div
  let rem = lift2 I.rem
  let lt = lift2_cmp I.lt
  let gt = lift2_cmp I.gt
  let le = lift2_cmp I.le
  let ge = lift2_cmp I.ge
  let eq = lift2_cmp I.eq
  let ne = lift2_cmp I.ne
  let bitnot = lift I.bitnot
  let bitand = lift2 I.bitand
  let bitor = lift2 I.bitor
  let bitxor = lift2 I.bitxor
  let shift_left x y = {x with v = I.shift_left x.ikind x.v y.v } (* TODO check ikinds*)
  let shift_right x y = {x with v = I.shift_right x.ikind x.v y.v } (* TODO check ikinds*)
  let lognot = lift_logical I.lognot
  let logand = lift2 I.logand
  let logor = lift2 I.logor

  let cast_to ?torg ikind x = {v = I.cast_to ?torg ikind x.v; ikind}

end

module type Ikind =
sig
  val ikind: unit -> Cil.ikind
end

module PtrDiffIkind : Ikind =
struct
  let ikind = Cilfacade.ptrdiff_ikind
end

module IntDomWithDefaultIkind (I: Y) (Ik: Ikind) : Y with type t = I.t and type int_t = I.int_t =
struct
  include I
  let top () = I.top_of (Ik.ikind ())
  let bot () = I.bot_of (Ik.ikind ())
end

module Size = struct (* size in bits as int, range as int64 *)
  exception Not_in_int64
  open Cil open Int64 open Big_int_Z
  let sign x = if x<0L then `Signed else `Unsigned
  let max = function
    | `Signed -> ILongLong
    | `Unsigned -> IULongLong
  let top_typ = TInt (ILongLong, [])
  let min_for x = intKindForValue (mkCilint (max (sign x)) x) (sign x = `Unsigned)
  let bit = function (* bits needed for representation *)
    | IBool -> 1
    | ik -> bytesSizeOfInt ik * 8
  let is_int64_big_int x = try let _ = int64_of_big_int x in true with _ -> false
  let card ik = (* cardinality *)
    let b = bit ik in
    shift_left_big_int unit_big_int b
  let bits ik = (* highest bits for neg/pos values *)
    let s = bit ik in
    if isSigned ik then s-1, s-1 else 0, s
  let bits_i64 ik = BatTuple.Tuple2.mapn of_int (bits ik)
  let range ik = (* min/max values as int64 (signed), anything bigger is cropped! *)
    let a,b = bits ik in
    if a>63 || b>63 then raise Not_in_int64 else
      let x = if isSigned ik then neg (shift_left 1L a) (* -2^a *) else 0L in
      let y = sub (shift_left 1L b) 1L in (* 2^b - 1 *)
      x,y
  let range_big_int ik =
    let a,b = bits ik in
    let x = if isSigned ik then minus_big_int (shift_left_big_int unit_big_int a) (* -2^a *) else zero_big_int in
    let y = sub_big_int (shift_left_big_int unit_big_int b) unit_big_int in (* 2^b - 1 *)
    x,y
  let cast_big_int t x = (* TODO: overflow is implementation-dependent! *)
    let a,b = range_big_int t in
    let c = card t in
    (* let z = add (rem (sub x a) c) a in (* might lead to overflows itself... *)*)
    let y = mod_big_int x c in
    let y = if gt_big_int y b then sub_big_int y c
      else if lt_big_int y a then add_big_int y c
      else y
    in
    M.tracel "cast_int" "Cast %s to range [%s, %s] (%s) = %s (%s in int64)\n" (string_of_big_int x) (string_of_big_int a) (string_of_big_int b) (string_of_big_int c) (string_of_big_int y) (if is_int64_big_int y then "fits" else "does not fit");
    y
  let cast t x =
    let x' = big_int_of_int64 x in
    try int64_of_big_int (cast_big_int t x') with _ -> raise Not_in_int64

  let min_range_sign_agnostic x =
    let size ik =
      let a,b = bits_i64 ik in
      Int64.neg a,b
    in
    if sign x = `Signed then
      size (min_for x)
    else
      let a, b = size (min_for x) in
      if b <= 64L then
        let upper_bound_less = Int64.sub b 1L in
        let max_one_less = Int64.(pred @@ shift_left 1L (to_int upper_bound_less)) in
        if x < max_one_less then
          a, upper_bound_less
        else
          a,b
      else
        a, b
end

exception Unknown
exception Error
exception ArithmeticOnIntegerBot of string

module StdTop (B: sig type t val top_of: Cil.ikind -> t end) = struct
  open B
  (* these should be overwritten for better precision if possible: *)
  let to_excl_list    x = None
  let of_excl_list ik x = top_of ik
  let is_excl_list    x = false
  let of_interval  ik x = top_of ik
  let starting     ik x = top_of ik
  let ending       ik x = top_of ik
  let maximal         x = None
  let minimal         x = None
end

module Std (B: sig
    type t
    val name: unit -> string
    val top_of: Cil.ikind -> t
    val bot_of: Cil.ikind -> t
    val short: int -> t -> string
    val equal: t -> t -> bool
  end) = struct
  include Printable.Std
  let name = B.name (* overwrite the one from Printable.Std *)
  open B
  let isSimple _ = true
  let hash = Hashtbl.hash
  let is_top x = failwith "is_top not implemented for IntDomain.Std"
  let is_bot x = B.equal x (bot_of Cil.IInt) (* Here we assume that the representation of bottom is independent of the ikind
                                                This may be true for intdomain implementations, but not e.g. for IntDomLifter. *)
  let is_top_of ik x = B.equal x (top_of ik)
  (* let is_bot_of ik x = B.equal x (bot_of ik) *)

  (* all output is based on B.short *)
  let pretty_f sh () x = text (sh Goblintutil.summary_length x)
  let pretty = pretty_f short
  let pretty_diff () (x,y) = dprintf "%s: %a instead of %a" (name ()) pretty x pretty y
  let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (short 800 x)

  include StdTop (B)
end
(* include Std (struct type nonrec t = t let name = name let top = top let bot = bot let short = short end) *)


module IntervalFunctor(Ints_t : IntOps): S with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =
struct
  let name () = "intervals"
  type int_t = Ints_t.t
  type t = (Ints_t.t * Ints_t.t) option
  let to_yojson t = failwith "to yojson unimplemented"

  let min_int ik = Ints_t.of_bigint @@ fst @@ Size.range_big_int ik
  let max_int ik = Ints_t.of_bigint @@ snd @@ Size.range_big_int ik
  let top () = failwith @@ "top () not implemented for " ^ (name ())
  let top_of ik = Some (min_int ik, max_int ik)
  let bot () = None
  let bot_of ik = bot () (* TODO: improve *)

  let is_top x = failwith "is_top not implemented for intervals"

  let is_bot x  = failwith "is_bot not implemented for intervals"

  let short _ = function None -> "bottom" | Some (x,y) -> "["^Ints_t.to_string x^","^Ints_t.to_string y^"]"

  let equal a b = match a, b with
    | None, None -> true
    | Some (a, b), Some (c, d) -> Ints_t.equal a c && Ints_t.equal b d
    | _, _ -> false

  include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let short = short let equal = equal end)

  let equal_to i = function
    | None -> failwith "unsupported: equal_to with bottom"
    | Some (a, b) ->
      if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq

  let norm ik = function None -> None | Some (x,y) ->
    if Ints_t.compare x y > 0 then None
    else if Ints_t.compare (min_int ik) x > 0 || Ints_t.compare (max_int ik) y < 0 then top_of ik
    else Some (x,y)

  let leq (x:t) (y:t) =
    match x, y with
    | None, _ -> true
    | Some _, None -> false
    | Some (x1,x2), Some (y1,y2) -> Ints_t.compare x1 y1 >= 0 && Ints_t.compare x2 y2 <= 0

  let join ik (x:t) y =
    match x, y with
    | None, z | z, None -> z
    | Some (x1,x2), Some (y1,y2) -> norm ik @@ Some (min x1 y1, max x2 y2)

  let meet ik (x:t) y =
    match x, y with
    | None, z | z, None -> None
    | Some (x1,x2), Some (y1,y2) -> norm ik @@ Some (max x1 y1, min x2 y2)

  let is_int = function Some (x,y) when Ints_t.compare x y = 0 -> true | _ -> false

  (* TODO: change to_int signature so it returns a big_int *)
  let to_int = function Some (x,y) when Ints_t.compare x y = 0 -> Some x | _ -> None
  let of_interval ik (x,y) = norm ik @@ Some (x,y)
  let of_int ik (x: int_t) = of_interval ik (x,x)
  let zero = Some (Ints_t.zero, Ints_t.zero)
  let one  = Some (Ints_t.one, Ints_t.one)
  let top_bool = Some (Ints_t.zero, Ints_t.one)

  let of_bool _ik = function true -> one | false -> zero
  let is_bool x = x <> None && not (leq zero x) || equal x zero
  let to_bool (a: t) = match a with
    | None -> None
    | Some (l, u) when Ints_t.compare l Ints_t.zero = 0 && Ints_t.compare u Ints_t.zero = 0 -> Some false
    | x -> if leq zero x then None else Some true
  let to_bool_interval x = match x with
    | None -> x
    | Some (l, u) when Ints_t.compare l Ints_t.zero = 0 && Ints_t.compare u Ints_t.zero = 0 -> x
    | _ -> if leq zero x then top_bool else one

  let range_opt f = function
    | None -> None
    | Some ik -> Some (Ints_t.of_bigint @@ f @@ Size.range_big_int ik)

  let starting ik n =
    (norm ik) @@ Some (n, range_opt snd (Some ik) |? (max_int ik))

  let ending ik n =
    norm ik @@ Some (range_opt fst (Some ik) |? min_int ik, n)

  (* TODO: change signarue of maximal, minimal to return big_int*)
  let maximal = function None -> None | Some (x,y) -> Some y
  let minimal = function None -> None | Some (x,y) -> Some x

  let cast_to ?torg t = function
    | None -> None
    | Some (x,y) ->
      try
        let a = Ints_t.of_bigint @@ Size.cast_big_int t (Ints_t.to_bigint x) in
        let b = Ints_t.of_bigint @@ Size.cast_big_int t (Ints_t.to_bigint y) in
        let a,b = if Ints_t.compare x a <> 0 || Ints_t.compare y b <> 0 then Size.range_big_int t |> (fun (a, b) -> (Ints_t.of_bigint a, Ints_t.of_bigint b)) else a,b in
        norm t @@ Some (a, b)
      with Size.Not_in_int64 -> top_of t

  let widen ik x y =
    match x, y with
    | None, z | z, None -> z
    | Some (l0,u0), Some (l1,u1) ->
      let l2 = if Ints_t.compare l0 l1 = 0 then l0 else min l1 (min_int ik) in
      let u2 = if Ints_t.compare u0 u1 = 0 then u0 else max u1 (max_int ik) in
      norm ik @@ Some (l2,u2)

  let narrow ik x y =
    match x, y with
    | _,None | None, _ -> None
    | Some (x1,x2), Some (y1,y2) ->
      let lr = if Ints_t.compare (min_int ik) x1 = 0 then y1 else x1 in
      let ur = if Ints_t.compare (max_int ik) x2 = 0 then y2 else x2 in
      norm ik @@ Some (lr,ur)

  let log f ik i1 i2 =
    match is_bot i1, is_bot i2 with
    | true, true -> bot_of ik
    | true, _
    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 i1) (short 80 i2)))
    | _ ->
      match to_bool i1, to_bool i2 with
      | Some x, Some y -> of_bool ik (f x y)
      | _              -> top_of ik

  let logor = log (||)
  let logand = log (&&)

  let log1 f ik i1 =
    if is_bot i1 then
      bot_of ik
    else
      match to_bool i1 with
      | Some x -> of_bool ik (f ik x)
      | _      -> top_of ik

  let lognot = log1 (fun _ik -> not)

  let bit f ik i1 i2 =
    match is_bot i1, is_bot i2 with
    | true, true -> bot_of ik
    | true, _
    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 i1) (short 80 i2)))
    | _ ->
      match to_int i1, to_int i2 with
      | Some x, Some y -> (try norm ik (of_int ik (f ik x y)) with Division_by_zero -> top_of ik)
      | _              -> top_of ik

  let bitxor = bit (fun _ik -> Ints_t.logxor)
  let bitand = bit (fun _ik -> Ints_t.logand)
  let bitor  = bit (fun _ik -> Ints_t.logor)

  let bit1 f ik i1 =
    if is_bot i1 then
      bot_of ik
    else
      match to_int i1 with
      | Some x -> of_int ik (f ik x)
      | _      -> top_of ik

  let bitnot = bit1 (fun _ik -> Ints_t.lognot)
  let shift_right = bit (fun _ik x y -> Ints_t.shift_right x (Ints_t.to_int y))
  let shift_left  = bit (fun _ik x y -> Ints_t.shift_left  x (Ints_t.to_int y))

  let neg ik = function None -> None | Some (x,y) -> norm ik @@ Some (Ints_t.neg y, Ints_t.neg x)

  let add_sub_helper f ik x y =
    match x, y with
    | None, None -> None
    | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))
    | Some (x1,x2), Some (y1,y2) -> norm ik @@ Some (f x1 y1, f x2 y2)

  let add = add_sub_helper Ints_t.add
  let sub = add_sub_helper Ints_t.sub

  let rem ik x y = match x, y with
    | None, None -> None
    | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))
    | Some (xl, xu), Some (yl, yu) ->
      if is_top_of ik x && is_top_of ik y then
        (* This is needed to preserve soundness also on things bigger than int32 e.g.  *)
        (* x:     3803957176L -> T in Interval32 *)
        (* y:     4209861404L -> T in Interval32 *)
        (* x % y: 3803957176L -> T in Interval32 *)
        (* T in Interval32 is [-2147483648,2147483647] *)
        (* the code below computes [-2147483647,2147483647] for this though which is unsound *)
        top_of ik
      else
        (* If we have definite values, Ints_t.rem will give a definite result.
{'fraction_non_alphanumeric': 0.11340374437527687, 'fraction_numerical': 0.015387843603553194, 'mean_word_length': 2.360915217050619, 'pattern_counts': {'":': 0, '<': 37, '<?xml version=': 0, '>': 561, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2234751', 'n_tokens_mistral': 17284, 'n_tokens_neox': 16676, 'n_words': 6160}