From 1cbbd2549b367ecc9a223bfc02d9f576554d16c8 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 13:53:40 +0200
Subject: [PATCH 01/52] Use Z module instead of IntOps.BigIntOps in base

---
 src/analyses/base.ml | 31 +++++++++++++++----------------
 1 file changed, 15 insertions(+), 16 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index fb2b5af517..440a1fcd96 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -19,7 +19,6 @@ module Addr = ValueDomain.Addr
 module Offs = ValueDomain.Offs
 module LF = LibraryFunctions
 module CArrays = ValueDomain.CArrays
-module BI = IntOps.BigIntOps
 module PU = PrecisionUtil
 
 module VD     = BaseDomain.VD
@@ -247,7 +246,7 @@ struct
     if M.tracing then M.tracel "eval" "evalbinop %a %a %a\n" d_binop op VD.pretty a1 VD.pretty a2;
     (* We define a conversion function for the easy cases when we can just use
      * the integer domain operations. *)
-    let bool_top ik = ID.(join (of_int ik BI.zero) (of_int ik BI.one)) in
+    let bool_top ik = ID.(join (of_int ik Z.zero) (of_int ik Z.one)) in
     (* An auxiliary function for ptr arithmetic on array values. *)
     let addToAddr n (addr:Addr.t) =
       let typeOffsetOpt o t =
@@ -270,7 +269,7 @@ struct
           begin match t with
             | Some t ->
               let (f_offset_bits, _) = bitsOffset t (Field (f, NoOffset)) in
-              let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (BI.of_int (f_offset_bits / 8)) in
+              let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (f_offset_bits / 8)) in
               begin match IdxDom.(to_bool (eq f_offset (neg n_offset))) with
                 | Some true -> `NoOffset
                 | _ -> `Field (f, `Index (n_offset, `NoOffset))
@@ -286,7 +285,7 @@ struct
         | `NoOffset -> `Index(iDtoIdx n, `NoOffset)
       in
       let default = function
-        | Addr.NullPtr when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> Addr.NullPtr
+        | Addr.NullPtr when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> Addr.NullPtr
         | _ -> Addr.UnknownPtr
       in
       match Addr.to_mval addr with
@@ -388,9 +387,9 @@ struct
               Int (ID.top_of ik)
           end
         | Eq ->
-          Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.zero else match eq p1 p2 with Some x when x -> ID.of_int ik BI.one | _ -> bool_top ik)
+          Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik Z.zero else match eq p1 p2 with Some x when x -> ID.of_int ik Z.one | _ -> bool_top ik)
         | Ne ->
-          Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.one else match eq p1 p2 with Some x when x -> ID.of_int ik BI.zero | _ -> bool_top ik)
+          Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik Z.one else match eq p1 p2 with Some x when x -> ID.of_int ik Z.zero | _ -> bool_top ik)
         | IndexPI when AD.to_string p2 = ["all_index"] ->
           addToAddrOp p1 (ID.top_of (Cilfacade.ptrdiff_ikind ()))
         | IndexPI | PlusPI ->
@@ -871,7 +870,7 @@ struct
       (* CIL's very nice implicit conversion of an array name [a] to a pointer
         * to its first element [&a[0]]. *)
       | StartOf lval ->
-        let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset) in
+        let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
         let array_start = add_offset_varinfo array_ofs in
         Address (AD.map array_start (eval_lv a gs st lval))
       | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv a gs st (Const (CStr (x,e))) (* TODO safe? *)
@@ -974,11 +973,11 @@ struct
         match op with
         | MinusA when must_be_equal () ->
           let ik = Cilfacade.get_ikind t in
-          Int (ID.of_int ik BI.zero)
+          Int (ID.of_int ik Z.zero)
         | MinusPI (* TODO: untested *)
         | MinusPP when must_be_equal () ->
           let ik = Cilfacade.ptrdiff_ikind () in
-          Int (ID.of_int ik BI.zero)
+          Int (ID.of_int ik Z.zero)
         (* Eq case is unnecessary: Q.must_be_equal reconstructs BinOp (Eq, _, _, _) and repeats EvalInt query for that, yielding a top from query cycle and never being must equal *)
         | Le
         | Ge when must_be_equal () ->
@@ -1258,7 +1257,7 @@ struct
             | _ -> None
           in
           let alen = Seq.filter_map (fun v -> lenOf v.vtype) (List.to_seq (AD.to_var_may a)) in
-          let d = Seq.fold_left ID.join (ID.bot_of (Cilfacade.ptrdiff_ikind ())) (Seq.map (ID.of_int (Cilfacade.ptrdiff_ikind ()) %BI.of_int) (Seq.append slen alen)) in
+          let d = Seq.fold_left ID.join (ID.bot_of (Cilfacade.ptrdiff_ikind ())) (Seq.map (ID.of_int (Cilfacade.ptrdiff_ikind ()) %Z.of_int) (Seq.append slen alen)) in
           (* ignore @@ printf "EvalLength %a = %a\n" d_exp e ID.pretty d; *)
           `Lifted d
         | Bot -> Queries.Result.bot q (* TODO: remove *)
@@ -1291,7 +1290,7 @@ struct
             (match r with
              | Array a ->
                (* unroll into array for Calloc calls *)
-               (match ValueDomain.CArrays.get (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) a (None, (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero)) with
+               (match ValueDomain.CArrays.get (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) a (None, (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero)) with
                 | Blob (_,s,_) -> `Lifted s
                 | _ -> Queries.Result.top q
                )
@@ -2457,7 +2456,7 @@ struct
       let st' =
         (* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *)
         match (eval_rv (Analyses.ask_of_ctx ctx) gs st ret_var) with
-        | Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st
+        | Int n when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> st
         | Address ret_a ->
           begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with
             | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
@@ -2517,8 +2516,8 @@ struct
             let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
             (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
             set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
-              (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
-              (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))
+              (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, false))));
+              (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset)))))
             ]
           )
         | _ -> st
@@ -2534,7 +2533,7 @@ struct
             match p_rv with
             | Address a -> a
             (* TODO: don't we already have logic for this? *)
-            | Int i when ID.to_int i = Some BI.zero -> AD.null_ptr
+            | Int i when ID.to_int i = Some Z.zero -> AD.null_ptr
             | Int i -> AD.top_ptr
             | _ -> AD.top_ptr (* TODO: why does this ever happen? *)
           in
@@ -2574,7 +2573,7 @@ struct
       in
       begin match lv with
         | Some lv ->
-          set ~ctx ask gs st' (eval_lv ask ctx.global st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt BI.zero))
+          set ~ctx ask gs st' (eval_lv ask ctx.global st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero))
         | None -> st'
       end
     | Longjmp {env; value}, _ ->

From 5946b03aa50f60fe2a38ed5622e4db37e5c78143 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 13:59:30 +0200
Subject: [PATCH 02/52] Use Z module instead of IntOps.BigIntOps in
 baseInvariant

---
 src/analyses/baseInvariant.ml | 47 +++++++++++++++++------------------
 1 file changed, 23 insertions(+), 24 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index f18eeed24f..7176ea5695 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -7,7 +7,6 @@ module VD = BaseDomain.VD
 module ID = ValueDomain.ID
 module FD = ValueDomain.FD
 module AD = ValueDomain.AD
-module BI = IntOps.BigIntOps
 
 module type Eval =
 sig
@@ -140,7 +139,7 @@ struct
               match ID.to_int n with
               | Some n ->
                 (* When x != n, we can return a singleton exclusion set *)
-                if M.tracing then M.tracec "invariant" "Yes, %a is not %s\n" d_lval x (BI.to_string n);
+                if M.tracing then M.tracec "invariant" "Yes, %a is not %s\n" d_lval x (Z.to_string n);
                 let ikind = Cilfacade.get_ikind_exp (Lval lval) in
                 Some (x, Int (ID.of_excl_list ikind [n]))
               | None -> None
@@ -169,11 +168,11 @@ struct
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
               let n = ID.cast_to ikind n in
-              let range_from x = if tv then ID.ending ikind (BI.sub x BI.one) else ID.starting ikind x in
+              let range_from x = if tv then ID.ending ikind (Z.sub x Z.one) else ID.starting ikind x in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
-                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %s\n\n" d_lval x (BI.to_string n);
+                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %s\n\n" d_lval x (Z.to_string n);
                 Some (x, Int (range_from n))
               | None -> None
             end
@@ -184,11 +183,11 @@ struct
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
               let n = ID.cast_to ikind n in
-              let range_from x = if tv then ID.ending ikind x else ID.starting ikind (BI.add x BI.one) in
+              let range_from x = if tv then ID.ending ikind x else ID.starting ikind (Z.add x Z.one) in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
-                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %s\n\n" d_lval x (BI.to_string n);
+                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %s\n\n" d_lval x (Z.to_string n);
                 Some (x, Int (range_from n))
               | None -> None
             end
@@ -205,7 +204,7 @@ struct
       match Cil.unrollType typ with
       | TPtr _                    -> Address AD.null_ptr
       | TEnum({ekind=_;_},_)
-      | _                         -> Int (ID.of_int (Cilfacade.get_ikind typ) BI.zero)
+      | _                         -> Int (ID.of_int (Cilfacade.get_ikind typ) Z.zero)
     in
     let rec derived_invariant exp tv =
       let switchedOp = function Lt -> Gt | Gt -> Lt | Le -> Ge | Ge -> Le | x -> x in (* a op b <=> b (switchedOp op) b *)
@@ -255,7 +254,7 @@ struct
     (* ikind is the type of a for limiting ranges of the operands a, b. The only binops which can have different types for a, b are Shiftlt, Shiftrt (not handled below; don't use ikind to limit b there). *)
     let inv_bin_int (a, b) ikind c op =
       let warn_and_top_on_zero x =
-        if GobOption.exists (BI.equal BI.zero) (ID.to_int x) then
+        if GobOption.exists (Z.equal Z.zero) (ID.to_int x) then
           (M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
            ID.top_of ikind)
         else
@@ -278,7 +277,7 @@ struct
         (* refine x by information about y, using x * y == c *)
         let refine_by x y = (match ID.to_int y with
             | None -> x
-            | Some v when BI.equal (BI.rem v (BI.of_int 2)) BI.zero (* v % 2 = 0 *) -> x (* A refinement would still be possible here, but has to take non-injectivity into account. *)
+            | Some v when Z.equal (Z.rem v (Z.of_int 2)) Z.zero (* v % 2 = 0 *) -> x (* A refinement would still be possible here, but has to take non-injectivity into account. *)
             | Some v (* when Int64.rem v 2L = 1L *) -> id_meet_down ~old:x ~c:(ID.div c y)) (* Div is ok here, c must be divisible by a and b *)
         in
         (refine_by a b, refine_by b a)
@@ -290,11 +289,11 @@ struct
          * However, a%b will give [-b+1, b-1] for a=top, but we only want the positive/negative side depending on the sign of c*b.
          * If c*b = 0 or it can be positive or negative, we need the full range for the remainder. *)
         let rem =
-          let is_pos = ID.to_bool @@ ID.gt (ID.mul b c) (ID.of_int ikind BI.zero) = Some true in
-          let is_neg = ID.to_bool @@ ID.lt (ID.mul b c) (ID.of_int ikind BI.zero) = Some true in
+          let is_pos = ID.to_bool @@ ID.gt (ID.mul b c) (ID.of_int ikind Z.zero) = Some true in
+          let is_neg = ID.to_bool @@ ID.lt (ID.mul b c) (ID.of_int ikind Z.zero) = Some true in
           let full = ID.rem a b in
-          if is_pos then ID.meet (ID.starting ikind BI.zero) full
-          else if is_neg then ID.meet (ID.ending ikind BI.zero) full
+          if is_pos then ID.meet (ID.starting ikind Z.zero) full
+          else if is_neg then ID.meet (ID.ending ikind Z.zero) full
           else full
         in
         meet_bin (ID.add (ID.mul b c) rem) (ID.div (ID.sub a rem) c)
@@ -310,11 +309,11 @@ struct
          * If b is negative we have to look at the lower bound. *)
         let is_divisible bound =
           match bound a with
-          | Some ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some BI.zero
+          | Some ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some Z.zero
           | None -> false
         in
-        let max_pos = match ID.maximal b with None -> true | Some x -> BI.compare x BI.zero >= 0 in
-        let min_neg = match ID.minimal b with None -> true | Some x -> BI.compare x BI.zero < 0 in
+        let max_pos = match ID.maximal b with None -> true | Some x -> Z.compare x Z.zero >= 0 in
+        let min_neg = match ID.minimal b with None -> true | Some x -> Z.compare x Z.zero < 0 in
         let implies a b = not a || b in
         let a'' =
           if implies max_pos (is_divisible ID.maximal) && implies min_neg (is_divisible ID.minimal) then
@@ -333,10 +332,10 @@ struct
         let a,b = meet_bin a''' b' in
         (* Special handling for case a % 2 != c *)
         let a = if PrecisionUtil.(is_congruence_active (int_precision_from_node_or_config ())) then
-            let two = BI.of_int 2 in
+            let two = Z.of_int 2 in
             match ID.to_int b, ID.to_excl_list c with
-            | Some b, Some ([v], _) when BI.equal b two ->
-              let k = if BI.equal (BI.abs (BI.rem v two)) (BI.zero) then BI.one else BI.zero in
+            | Some b, Some ([v], _) when Z.equal b two ->
+              let k = if Z.equal (Z.abs (Z.rem v two)) Z.zero then Z.one else Z.zero in
               ID.meet (ID.of_congruence ikind (k, b)) a
             | _, _ -> a
           else a
@@ -381,8 +380,8 @@ struct
           | _, _ -> a, b
         end
       | Lt | Le | Ge | Gt as op ->
-        let pred x = BI.sub x BI.one in
-        let succ x = BI.add x BI.one in
+        let pred x = Z.sub x Z.one in
+        let succ x = Z.add x Z.one in
         (match ID.minimal a, ID.maximal a, ID.minimal b, ID.maximal b with
          | Some l1, Some u1, Some l2, Some u2 ->
            (* if M.tracing then M.tracel "inv" "Op: %s, l1: %Ld, u1: %Ld, l2: %Ld, u2: %Ld\n" (show_binop op) l1 u1 l2 u2; *)
@@ -414,7 +413,7 @@ struct
         (* we only attempt to refine a here *)
         let a =
           match ID.to_int b with
-          | Some x when BI.equal x BI.one ->
+          | Some x when Z.equal x Z.one ->
             (match ID.to_bool c with
              | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
              | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
@@ -574,7 +573,7 @@ struct
             | Some true ->
               (* i.e. e should evaluate to [1,1] *)
               (* LNot x is 0 for any x != 0 *)
-              ID.of_excl_list ikind [BI.zero]
+              ID.of_excl_list ikind [Z.zero]
             | Some false -> ID.of_bool ikind false
             | _ -> ID.top_of ikind
           in
@@ -810,7 +809,7 @@ struct
         let itv = if not tv || is_cmp exp then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *)
             ID.of_bool ik tv (* this will give 1 for true which is only ok for comparisons *)
           else
-            ID.of_excl_list ik [BI.zero] (* Lvals, Casts, arithmetic operations etc. should work with true = non_zero *)
+            ID.of_excl_list ik [Z.zero] (* Lvals, Casts, arithmetic operations etc. should work with true = non_zero *)
         in
         inv_exp (Int itv) exp st
       | exception Invalid_argument _ ->

From 2df6d669375a00babbb760a641ab3c39d4154814 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:06:31 +0200
Subject: [PATCH 03/52] Use Z module instead of IntOps.BigIntOps in arrayDomain

---
 src/cdomain/value/cdomains/arrayDomain.ml | 43 +++++++++++------------
 1 file changed, 21 insertions(+), 22 deletions(-)

diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml
index d4d5a46e98..162d782951 100644
--- a/src/cdomain/value/cdomains/arrayDomain.ml
+++ b/src/cdomain/value/cdomains/arrayDomain.ml
@@ -5,7 +5,6 @@ open FlagHelper
 
 module M = Messages
 module A = Array
-module BI = IntOps.BigIntOps
 module VDQ = ValueDomainQueries
 
 type domain = TrivialDomain | PartitionedDomain | UnrolledDomain
@@ -53,9 +52,9 @@ sig
   val get_vars_in_e: t -> Cil.varinfo list
   val map: (value -> value) -> t -> t
   val fold_left: ('a -> value -> 'a) -> 'a -> t -> 'a
-  val smart_join: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t
-  val smart_widen: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t
-  val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool
+  val smart_join: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> t
+  val smart_widen: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> t
+  val smart_leq: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> bool
   val update_length: idx -> t -> t
 
   val project: ?varAttr:attributes -> ?typAttr:attributes -> VDQ.t -> t -> t
@@ -102,9 +101,9 @@ end
 module type LatticeWithSmartOps =
 sig
   include LatticeWithInvalidate
-  val smart_join: (Cil.exp -> BI.t option) -> (Cil.exp -> BI.t option) -> t -> t -> t
-  val smart_widen: (Cil.exp -> BI.t option) -> (Cil.exp -> BI.t option) -> t -> t -> t
-  val smart_leq: (Cil.exp -> BI.t option) -> (Cil.exp -> BI.t option) -> t -> t -> bool
+  val smart_join: (Cil.exp -> Z.t option) -> (Cil.exp -> Z.t option) -> t -> t -> t
+  val smart_widen: (Cil.exp -> Z.t option) -> (Cil.exp -> Z.t option) -> t -> t -> t
+  val smart_leq: (Cil.exp -> Z.t option) -> (Cil.exp -> Z.t option) -> t -> t -> bool
 end
 
 module type Null =
@@ -305,9 +304,9 @@ module type SPartitioned =
 sig
   include S
   val set_with_length: idx option -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value -> t
-  val smart_join_with_length: idx option -> (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t
-  val smart_widen_with_length: idx option -> (exp -> BI.t option) -> (exp -> BI.t option)  -> t -> t-> t
-  val smart_leq_with_length: idx option -> (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool
+  val smart_join_with_length: idx option -> (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> t
+  val smart_widen_with_length: idx option -> (exp -> Z.t option) -> (exp -> Z.t option)  -> t -> t-> t
+  val smart_leq_with_length: idx option -> (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> bool
   val move_if_affected_with_length: ?replace_with_const:bool -> idx option -> VDQ.t -> t -> Cil.varinfo -> (Cil.exp -> int option) -> t
 end
 
@@ -549,15 +548,15 @@ struct
       let use_last = get_string "ana.base.partition-arrays.keep-expr" = "last" in
       let exp_value e =
         let n = ask.eval_int e in
-        Option.map BI.of_bigint (VDQ.ID.to_int n)
+        VDQ.ID.to_int n
       in
-      let equals_zero e = BatOption.map_default (BI.equal BI.zero) false (exp_value e) in
+      let equals_zero e = BatOption.map_default (Z.equal Z.zero) false (exp_value e) in
       let equals_maxIndex e =
         match length with
         | Some l ->
           begin
             match Idx.to_int l with
-            | Some i -> BatOption.map_default (BI.equal (BI.sub i BI.one)) false (exp_value e)
+            | Some i -> BatOption.map_default (Z.equal (Z.sub i Z.one)) false (exp_value e)
             | None -> false
           end
         | _ -> false
@@ -597,10 +596,10 @@ struct
             else if Cil.isConstant e && Cil.isConstant i' then
               match Cil.getInteger e, Cil.getInteger i' with
               | Some (e'': Cilint.cilint), Some i'' ->
-                if BI.equal  i'' (BI.add e'' BI.one) then
+                if Z.equal  i'' (Z.add e'' Z.one) then
                   (* If both are integer constants and they are directly adjacent, we change partitioning to maintain information *)
                   Partitioned (i', (Val.join xl xm, a, xr))
-                else if BI.equal e'' (BI.add i'' BI.one) then
+                else if Z.equal e'' (Z.add i'' Z.one) then
                   Partitioned (i', (xl, a, Val.join xm xr))
                 else
                   default
@@ -658,7 +657,7 @@ struct
 
 
   let make ?(varAttr=[]) ?(typAttr=[]) i v:t =
-    if Idx.to_int i = Some BI.one  then
+    if Idx.to_int i = Some Z.one  then
       Partitioned ((Cil.integer 0), (v, v, v))
     else if Val.is_bot v then
       Joint (Val.bot ())
@@ -674,12 +673,12 @@ struct
         begin
           match Idx.to_int l with
           | Some i ->
-            v = Some (BI.sub i BI.one)
+            v = Some (Z.sub i Z.one)
           | None -> false
         end
       | None -> false
     in
-    let must_be_zero v = v = Some BI.zero in
+    let must_be_zero v = v = Some Z.zero in
     let op_over_all = op (join_of_all_parts x1) (join_of_all_parts x2) in
     match x1, x2 with
     | Partitioned (e1, (xl1, xm1, xr1)), Partitioned (e2, (xl2, xm2, xr2)) when Basetype.CilExp.equal e1 e2 ->
@@ -743,13 +742,13 @@ struct
 
   let smart_leq_with_length length x1_eval_int x2_eval_int x1 x2 =
     let leq' = Val.smart_leq x1_eval_int x2_eval_int in
-    let must_be_zero v = (v = Some BI.zero) in
+    let must_be_zero v = (v = Some Z.zero) in
     let must_be_length_minus_one v =  match length with
       | Some l ->
         begin
           match Idx.to_int l with
           | Some i ->
-            v = Some (BI.sub i BI.one)
+            v = Some (Z.sub i Z.one)
           | None -> false
         end
       | None -> false
@@ -835,7 +834,7 @@ end
 let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) =
   if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
     let idx_before_end = Idx.to_bool (Idx.lt v l) (* check whether index is before the end of the array *)
-    and idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int Cil.ILong BI.zero)) in (* check whether the index is non-negative *)
+    and idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int Cil.ILong Z.zero)) in (* check whether the index is non-negative *)
     (* For an explanation of the warning types check the Pull Request #255 *)
     match(idx_after_start, idx_before_end) with
     | Some true, Some true -> (* Certainly in bounds on both sides.*)
@@ -1739,7 +1738,7 @@ struct
     | UnrolledDomain -> (None, None, Some (U.make i v))
 
   (* convert to another domain *)
-  let index_as_expression i = (Some (Cil.integer i), Idx.of_int IInt (BI.of_int i))
+  let index_as_expression i = (Some (Cil.integer i), Idx.of_int IInt (Z.of_int i))
 
   let partitioned_of_trivial ask t = P.make (Option.value (T.length t) ~default:(Idx.top ())) (T.get ~checkBounds:false ask t (index_as_expression 0))
 

From 643bd414d135b47993de585da94e0e8f0591d53d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:08:31 +0200
Subject: [PATCH 04/52] Use Z module instead of IntOps.BigIntOps in valueDomain

---
 src/cdomain/value/cdomains/valueDomain.ml | 31 +++++++++++------------
 1 file changed, 15 insertions(+), 16 deletions(-)

diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index d1b81dcb08..0fd8fa79fb 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -7,7 +7,6 @@ open PrecisionUtil
 include PreValueDomain
 module Offs = Offset.MakeLattice (IndexDomain)
 module M = Messages
-module BI = IntOps.BigIntOps
 module MutexAttr = MutexAttrDomain
 module VDQ = ValueDomainQueries
 module AD = VDQ.AD
@@ -27,9 +26,9 @@ sig
   val invalidate_abstract_value: t -> t
   val is_safe_cast: typ -> typ -> bool
   val cast: ?torg:typ -> typ -> t -> t
-  val smart_join: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t ->  t
-  val smart_widen: (exp -> BI.t option) -> (exp -> BI.t option) ->  t -> t -> t
-  val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool
+  val smart_join: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t ->  t
+  val smart_widen: (exp -> Z.t option) -> (exp -> Z.t option) ->  t -> t -> t
+  val smart_leq: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> bool
   val is_immediate_type: typ -> bool
   val is_mutex_type: typ -> bool
   val bot_value: ?varAttr:attributes -> typ -> t
@@ -231,7 +230,7 @@ struct
     | _ when is_mutex_type t -> Mutex
     | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.top ())
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ())
-    | TInt (ikind, _) -> Int (ID.of_int ikind BI.zero)
+    | TInt (ikind, _) -> Int (ID.of_int ikind Z.zero)
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_const fkind 0.0)
     | TPtr _ -> Address AD.null_ptr
     | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> zero_init_value ~varAttr:fd.fattr fd.ftype) ci)
@@ -398,7 +397,7 @@ struct
             (* array to its first element *)
             | TArray _, _ ->
               M.tracel "casta" "cast array to its first element\n";
-              adjust_offs v (Addr.Offs.add_offset o (`Index (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset))) (Some false)
+              adjust_offs v (Addr.Offs.add_offset o (`Index (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset))) (Some false)
             | _ -> err @@ Format.sprintf "Cast to neither array index nor struct field. is_zero_offset: %b" (Addr.Offs.cmp_zero_offset o = `MustZero)
           end
     in
@@ -473,7 +472,7 @@ struct
           (* cast to voidPtr are ignored TODO what happens if our value does not fit? *)
         | TPtr (t,_) ->
           Address (match v with
-              | Int x when ID.to_int x = Some BI.zero -> AD.null_ptr
+              | Int x when ID.to_int x = Some Z.zero -> AD.null_ptr
               | Int x -> AD.top_ptr
               (* we ignore casts to void*! TODO report UB! *)
               | Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x)
@@ -532,7 +531,7 @@ struct
     | (_, Bot) -> false
     | (Int x, Int y) -> ID.leq x y
     | (Float x, Float y) -> FD.leq x y
-    | (Int x, Address y) when ID.to_int x = Some BI.zero && not (AD.is_not_null y) -> true
+    | (Int x, Address y) when ID.to_int x = Some Z.zero && not (AD.is_not_null y) -> true
     | (Int _, Address y) when AD.may_be_unknown y -> true
     | (Address _, Int y) when ID.is_top_of (Cilfacade.ptrdiff_ikind ()) y -> true
     | (Address x, Address y) -> AD.leq x y
@@ -560,7 +559,7 @@ struct
     | (Float x, Float y) -> Float (FD.join x y)
     | (Int x, Address y)
     | (Address y, Int x) -> Address (match ID.to_int x with
-        | Some x when BI.equal x BI.zero -> AD.join AD.null_ptr y
+        | Some x when Z.equal x Z.zero -> AD.join AD.null_ptr y
         | Some x -> AD.(join y not_null)
         | None -> AD.join y AD.top_ptr)
     | (Address x, Address y) -> Address (AD.join x y)
@@ -593,7 +592,7 @@ struct
     (* TODO: symmetric widen, wtf? *)
     | (Int x, Address y)
     | (Address y, Int x) -> Address (match ID.to_int x with
-        | Some x when BI.equal x BI.zero -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
+        | Some x when Z.equal x Z.zero -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
         | Some x -> AD.(widen y (join y not_null))
         | None -> AD.widen y (AD.join y AD.top_ptr))
     | (Address x, Address y) -> Address (AD.widen x y)
@@ -916,7 +915,7 @@ struct
               begin
                 do_eval_offset ask f x offs exp l' o' v t (* this used to be `blob `address -> we ignore the index *)
               end
-            | x when GobOption.exists (BI.equal (BI.zero)) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t
+            | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t
             | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()
             | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top ()
           end
@@ -960,7 +959,7 @@ struct
               not @@ ask.is_multiple var
               && not @@ Cil.isVoidType t      (* Size of value is known *)
               && Option.is_some blob_size_opt (* Size of blob is known *)
-              && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.bitsSizeOf (TComp (toptype, []))/8)
+              && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.bitsSizeOf (TComp (toptype, []))/8)
             | _ -> false
           in
           if do_strong_update then
@@ -981,7 +980,7 @@ struct
                 && Option.is_some blob_size_opt (* Size of blob is known *)
                 && ((
                     not @@ Cil.isVoidType t     (* Size of value is known *)
-                    && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.alignOf_int t)
+                    && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.alignOf_int t)
                   ) || blob_destructive)
               | _ -> false
             end
@@ -1062,10 +1061,10 @@ struct
                       | TArray(_, l, _) ->
                         let len = try Cil.lenOfArray l
                           with Cil.LenOfArray -> 42 (* will not happen, VLA not allowed in union and struct *) in
-                        Array(CArrays.make (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) (BI.of_int len)) Top), offs
+                        Array(CArrays.make (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int len)) Top), offs
                       | _ -> top (), offs (* will not happen*)
                     end
-                  | `Index (idx, _) when IndexDomain.equal idx (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero) ->
+                  | `Index (idx, _) when IndexDomain.equal idx (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) ->
                     (* Why does cil index unions? We'll just pick the first field. *)
                     top (), `Field (List.nth fld.fcomp.cfields 0,`NoOffset)
                   | _ -> M.warn ~category:Analyzer ~tags:[Category Unsound] "Indexing on a union is unusual, and unsupported by the analyzer";
@@ -1102,7 +1101,7 @@ struct
               let new_array_value = CArrays.update_length newl new_array_value in
               Array new_array_value
             | Top -> M.warn ~category:Imprecise "Trying to update an index, but the array is unknown"; top ()
-            | x when GobOption.exists (BI.equal BI.zero) (IndexDomain.to_int idx) -> do_update_offset ask x offs value exp l' o' v t
+            | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset ask x offs value exp l' o' v t
             | _ -> M.warn ~category:Imprecise "Trying to update an index, but was not given an array(%a)" pretty x; top ()
           end
       in mu result

From f16cfca56d4ea287fcc3a457462db56ebb7bfa97 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:10:46 +0200
Subject: [PATCH 05/52] Remove BI module and use Z instead of IntOps.BigIntOps
 in baseDomain

---
 src/cdomains/baseDomain.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml
index ce6cc171fa..ba4b5b073b 100644
--- a/src/cdomains/baseDomain.ml
+++ b/src/cdomains/baseDomain.ml
@@ -2,7 +2,6 @@
 
 open GoblintCil
 module VD = ValueDomain.Compound
-module BI = IntOps.BigIntOps
 
 module CPA =
 struct
@@ -123,7 +122,7 @@ end
 module type ExpEvaluator =
 sig
   type t
-  val eval_exp: t  ->  Cil.exp -> IntOps.BigIntOps.t option
+  val eval_exp: t  ->  Cil.exp -> Z.t option
 end
 
 (* Takes a module for privatization component and a module specifying how expressions can be evaluated inside the domain and returns the domain *)

From 27b267d91ce4dd498cbda2760efd26e774c0968b Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:11:44 +0200
Subject: [PATCH 06/52] Use Z instead of IntOps.BigIntOps in function types in
 vectorMatrix

---
 src/cdomains/vectorMatrix.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/cdomains/vectorMatrix.ml b/src/cdomains/vectorMatrix.ml
index 1dd684a4c0..64d5c5e35d 100644
--- a/src/cdomains/vectorMatrix.ml
+++ b/src/cdomains/vectorMatrix.ml
@@ -24,8 +24,8 @@ sig
   val of_int: int -> t
   val zero: t
   val one: t
-  val get_den: t -> IntOps.BigIntOps.t
-  val get_num: t -> IntOps.BigIntOps.t
+  val get_den: t -> Z.t
+  val get_num: t -> Z.t
 end
 
 (** It provides more readable infix operators for the functions of RatOps.

From ad093889192be3d6d48a06979e46d7c7d03a25df Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:14:44 +0200
Subject: [PATCH 07/52] Remove BI module and use Z instead of IntOps.BigIntOps
 in intDomainProperties

---
 src/domains/intDomainProperties.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml
index 9dcb867efc..fa41ba645e 100644
--- a/src/domains/intDomainProperties.ml
+++ b/src/domains/intDomainProperties.ml
@@ -1,20 +1,19 @@
 (** QCheck properties for {!IntDomain}. *)
 
 open GoblintCil
-module BI = IntOps.BigIntOps
 
 (* TODO: deduplicate with IntDomain *)
 module type OldS =
 sig
   include Lattice.S
   include IntDomain.Arith with type t := t
-  val of_int: BI.t -> t
-  val to_int: t -> BI.t option
+  val of_int: Z.t -> t
+  val to_int: t -> Z.t option
   val of_bool: bool -> t
   val to_bool: t -> bool option
-  val of_excl_list: Cil.ikind -> BI.t list -> t
+  val of_excl_list: Cil.ikind -> Z.t list -> t
   val is_excl_list: t -> bool
-  val to_excl_list: t -> (BI.t list * (int64 * int64)) option
+  val to_excl_list: t -> (Z.t list * (int64 * int64)) option
 end
 
 module type OldSWithIkind =
@@ -23,7 +22,7 @@ sig
   module Ikind: IntDomain.Ikind
 end
 
-module type S = IntDomain.S with type int_t = BI.t
+module type S = IntDomain.S with type int_t = Z.t
 
 (* TODO: deduplicate with IntDomain, extension of IntDomWithDefaultIkind, inverse of OldDomainFacade? *)
 module WithIkind (I: S) (Ik: IntDomain.Ikind): OldSWithIkind =
@@ -140,8 +139,8 @@ struct
   let valid_bitxor = make_valid2 ~name:"bitxor" ~cond:none_bot CD.bitxor AD.bitxor
 
   let defined_shift (a, b) =
-    let max_shift = BI.of_int @@ snd @@ IntDomain.Size.bits (AD.Ikind.ikind ()) in
-    CD.for_all (fun x -> BI.compare BI.zero x <= 0 && BI.compare x max_shift <= 0) b
+    let max_shift = Z.of_int @@ snd @@ IntDomain.Size.bits (AD.Ikind.ikind ()) in
+    CD.for_all (fun x -> Z.compare Z.zero x <= 0 && Z.compare x max_shift <= 0) b
   let shift_cond p = none_bot p && defined_shift p
   let valid_shift_left = make_valid2 ~name:"shift_left" ~cond:shift_cond CD.shift_left AD.shift_left
   let valid_shift_right = make_valid2 ~name:"shift_right" ~cond:shift_cond CD.shift_right AD.shift_right

From 9cf5086b075212bcc4af4a8596f1503b572571b1 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:15:39 +0200
Subject: [PATCH 08/52] Use Z instead of IntOps.BigIntOps in
 expressionEvaluation

---
 src/transform/expressionEvaluation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml
index 815e5742f6..8ebdbb9b58 100644
--- a/src/transform/expressionEvaluation.ml
+++ b/src/transform/expressionEvaluation.ml
@@ -136,7 +136,7 @@ struct
         | Some x ->
           begin match Queries.ID.to_int x with
             (* Evaluable: Definite *)
-            | Some i -> Some (Some (not(IntOps.BigIntOps.equal i IntOps.BigIntOps.zero)))
+            | Some i -> Some (Some (not (Z.equal i Z.zero)))
             (* Evaluable: Inconclusive *)
             | None -> Some None
           end

From b6ed51531678f283a417587ebc666a39803492a1 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:16:54 +0200
Subject: [PATCH 09/52] Use Z instead of IntOps.BigIntOps in transform

---
 src/transform/transform.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/transform/transform.ml b/src/transform/transform.ml
index fe3abb6f08..337f3dfddb 100644
--- a/src/transform/transform.ml
+++ b/src/transform/transform.ml
@@ -55,7 +55,7 @@ module PartialEval = struct
     method! vexpr e =
       let eval e = match Queries.ID.to_int ((ask !loc).Queries.f (Queries.EvalInt e)) with
         | Some i ->
-          let e' = integer @@ IntOps.BigIntOps.to_int i in
+          let e' = integer (Z.to_int i) in
           ignore @@ Pretty.printf "Replacing non-constant expression %a with %a at %a\n" d_exp e d_exp e' CilType.Location.pretty !loc;
           e'
         | None ->

From 0edd272e6d83f4506be8a9f067d504e357b088a9 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:19:47 +0200
Subject: [PATCH 10/52] Use Z instead of IntOps.BigIntOps in
 sharedFunctions.apron

---
 src/cdomains/apron/sharedFunctions.apron.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index e66be00ae4..ff1f14891e 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -3,10 +3,8 @@
 open GoblintCil
 open Batteries
 open Apron
-module M = Messages
-
 
-module BI = IntOps.BigIntOps
+module M = Messages
 
 let int_of_scalar ?round (scalar: Scalar.t) =
   if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)
@@ -19,10 +17,10 @@ let int_of_scalar ?round (scalar: Scalar.t) =
       let+ f = match round with
         | Some `Floor -> Some (Float.floor f)
         | Some `Ceil -> Some (Float.ceil f)
-        | None when Stdlib.Float.is_integer f-> Some f
+        | None when Stdlib.Float.is_integer f -> Some f
         | None -> None
       in
-      BI.of_bigint (Z.of_float f)
+      Z.of_float f
     | Mpqf scalar -> (* octMPQ, boxMPQ, polkaMPQ *)
       let n = Mpqf.get_num scalar in
       let d = Mpqf.get_den scalar in
@@ -129,7 +127,7 @@ struct
             let (type_min, type_max) = IntDomain.Size.range ik in
             let texpr1 = Texpr1.of_expr env expr in
             match Bounds.bound_texpr d texpr1 with
-            | Some min, Some max when BI.compare type_min min <= 0 && BI.compare max type_max <= 0 -> ()
+            | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 -> ()
             | min_opt, max_opt ->
               if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntDomain.BigInt.pretty ())) min_opt (Pretty.docOpt (IntDomain.BigInt.pretty ())) max_opt;
               raise (Unsupported_CilExp Overflow)

From 7ad9d1a084eb94531c651e9470e28477e510130e Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:22:35 +0200
Subject: [PATCH 11/52] Use Z instead of IntOps.BigIntOps in offset

---
 src/cdomain/value/cdomains/offset.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml
index 62bab39eb7..bcca0cf1bc 100644
--- a/src/cdomain/value/cdomains/offset.ml
+++ b/src/cdomain/value/cdomains/offset.ml
@@ -58,7 +58,7 @@ struct
   let rec cmp_zero_offset : t -> [`MustZero | `MustNonzero | `MayZero] = function
     | `NoOffset -> `MustZero
     | `Index (x, o) ->
-      begin match cmp_zero_offset o, Idx.equal_to (IntOps.BigIntOps.zero) x with
+      begin match cmp_zero_offset o, Idx.equal_to Z.zero x with
         | `MustNonzero, _
         | _, `Neq -> `MustNonzero
         | `MustZero, `Eq -> `MustZero

From 028fe9c2dde42a8188276d7c0ba3dea985fa8de8 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:24:54 +0200
Subject: [PATCH 12/52] Use Z instead of IntOps.BigIntOps in
 affineEqualityDomain.apron

---
 src/cdomains/apron/affineEqualityDomain.apron.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 55937a323d..5485dd3f02 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -214,7 +214,7 @@ struct
   let bound_texpr t texpr =
     let texpr = Texpr1.to_expr texpr in
     match Option.bind (get_coeff_vec t texpr) to_constant_opt with
-    | Some c when Mpqf.get_den c = IntOps.BigIntOps.one ->
+    | Some c when Mpqf.get_den c = Z.one ->
       let int_val = Mpqf.get_num c in
       Some int_val, Some int_val
     | _ -> None, None
@@ -224,7 +224,7 @@ struct
     let res = bound_texpr d texpr1 in
     (if M.tracing then
        match res with
-       | Some min, Some max -> M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string min) (IntOps.BigIntOps.to_string max)
+       | Some min, Some max -> M.tracel "bounds" "min: %s max: %s" (Z.to_string min) (Z.to_string max)
        | _ -> ()
     );
     res

From 5da716a6172ca542448cb87179639dcce64493c1 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:25:44 +0200
Subject: [PATCH 13/52] Remove unused BI = IntOps.BigIntOps module from
 apronDomain.apron

---
 src/cdomains/apron/apronDomain.apron.ml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 03b9558621..e78176fc41 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -8,9 +8,6 @@ open GobApron
 open RelationDomain
 open SharedFunctions
 
-
-module BI = IntOps.BigIntOps
-
 module M = Messages
 
 (** Resources for working with Apron:

From c6c7cdfd8eb164b27e010413de9b611e92c2ff3d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:39:44 +0200
Subject: [PATCH 14/52] Replace all BI. calls with Z. in intDomain

---
 src/cdomain/value/cdomains/intDomain.ml | 110 ++++++++++++------------
 1 file changed, 55 insertions(+), 55 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 8a69f7134b..40e2136781 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -280,7 +280,7 @@ sig
   val invariant: Cil.exp -> t -> Invariant.t
 end
 
-module type Z = Y with type int_t = BI.t
+module type Z = Y with type int_t = Z.t
 
 
 module IntDomLifter (I : S) =
@@ -392,7 +392,7 @@ end
 
 module Size = struct (* size in bits as int, range as int64 *)
   open Cil
-  let sign x = if BI.compare x BI.zero < 0 then `Signed else `Unsigned
+  let sign x = if Z.compare x Z.zero < 0 then `Signed else `Unsigned
 
   let top_typ = TInt (ILongLong, [])
   let min_for x = intKindForValue x (sign x = `Unsigned)
@@ -416,8 +416,8 @@ module Size = struct (* size in bits as int, range as int64 *)
   let is_cast_injective ~from_type ~to_type =
     let (from_min, from_max) = range (Cilfacade.get_ikind from_type) in
     let (to_min, to_max) = range (Cilfacade.get_ikind to_type) in
-    if M.tracing then M.trace "int" "is_cast_injective %a (%s, %s) -> %a (%s, %s)\n" CilType.Typ.pretty from_type (BI.to_string from_min) (BI.to_string from_max) CilType.Typ.pretty to_type (BI.to_string to_min) (BI.to_string to_max);
-    BI.compare to_min from_min <= 0 && BI.compare from_max to_max <= 0
+    if M.tracing then M.trace "int" "is_cast_injective %a (%s, %s) -> %a (%s, %s)\n" CilType.Typ.pretty from_type (Z.to_string from_min) (Z.to_string from_max) CilType.Typ.pretty to_type (Z.to_string to_min) (Z.to_string to_max);
+    Z.compare to_min from_min <= 0 && Z.compare from_max to_max <= 0
 
   let cast t x = (* TODO: overflow is implementation-dependent! *)
     if t = IBool then
@@ -445,7 +445,7 @@ module Size = struct (* size in bits as int, range as int64 *)
       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 = BI.(pred @@ shift_left BI.one (Int64.to_int upper_bound_less)) in
+        let max_one_less = Z.(pred @@ shift_left Z.one (Int64.to_int upper_bound_less)) in
         if x <= max_one_less then
           a, upper_bound_less
         else
@@ -454,10 +454,10 @@ module Size = struct (* size in bits as int, range as int64 *)
         a, b
 
   (* From the number of bits used to represent a positive value, determines the maximal representable value *)
-  let max_from_bit_range pos_bits = BI.(pred @@ shift_left BI.one (to_int (BI.of_int64 pos_bits)))
+  let max_from_bit_range pos_bits = Z.(pred @@ shift_left Z.one (to_int (Z.of_int64 pos_bits)))
 
   (* From the number of bits used to represent a non-positive value, determines the minimal representable value *)
-  let min_from_bit_range neg_bits = BI.(if neg_bits = 0L then BI.zero else neg @@ shift_left BI.one (to_int (neg (BI.of_int64 neg_bits))))
+  let min_from_bit_range neg_bits = Z.(if neg_bits = 0L then Z.zero else neg @@ shift_left Z.one (to_int (neg (Z.of_int64 neg_bits))))
 
 end
 
@@ -1783,9 +1783,9 @@ module BigInt = struct
   let top_of ik = top ()
   let bot_of ik = bot ()
   let cast_to ik x = Size.cast ik x
-  let to_bool x = Some (not (BI.equal (BI.zero) x))
+  let to_bool x = Some (not (Z.equal Z.zero x))
 
-  let show x = BI.to_string x
+  let show x = Z.to_string x
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
   let arbitrary () = QCheck.map ~rev:to_int64 of_int64 QCheck.int64
 end
@@ -1805,14 +1805,14 @@ struct
   type inc = Inc of BISet.t [@@unboxed]
   let max_of_range r = Size.max_from_bit_range (Option.get (R.maximal r))
   let min_of_range r = Size.min_from_bit_range (Option.get (R.minimal r))
-  let cardinality_of_range r = BI.add BI.one (BI.add (BI.neg (min_of_range r)) (max_of_range r))
+  let cardinality_of_range r = Z.add Z.one (Z.add (Z.neg (min_of_range r)) (max_of_range r))
 
   let cardinality_BISet s =
-    BI.of_int (BISet.cardinal s)
+    Z.of_int (BISet.cardinal s)
 
   let leq_excl_incl (Exc (xs, r)) (Inc ys) =
     (* For a <= b to hold, the cardinalities must fit, i.e. |a| <= |b|, which implies |min_r, max_r| - |xs| <= |ys|. We check this first. *)
-    let lower_bound_cardinality_a = BI.sub (cardinality_of_range r) (cardinality_BISet xs) in
+    let lower_bound_cardinality_a = Z.sub (cardinality_of_range r) (cardinality_BISet xs) in
     let card_b = cardinality_BISet ys in
     if I.compare lower_bound_cardinality_a card_b > 0 then
       false
@@ -1833,13 +1833,13 @@ struct
           let min_b, max_b = min_of_range s, max_of_range s in
           let leq1 = (* check whether the elements in [r_l; s_l-1] are all in xs, i.e. excluded *)
             if I.compare min_a min_b < 0 then
-              GobZ.for_all_range (fun x -> BISet.mem x xs) (min_a, BI.sub min_b BI.one)
+              GobZ.for_all_range (fun x -> BISet.mem x xs) (min_a, Z.sub min_b Z.one)
             else
               true
           in
           let leq2 () = (* check whether the elements in [s_u+1; r_u] are all in xs, i.e. excluded *)
             if I.compare max_b max_a < 0 then
-              GobZ.for_all_range (fun x -> BISet.mem x xs) (BI.add max_b BI.one, max_a)
+              GobZ.for_all_range (fun x -> BISet.mem x xs) (Z.add max_b Z.one, max_a)
             else
               true
           in
@@ -1900,12 +1900,12 @@ struct
     | `Bot -> None
 
   let in_range r i =
-    let lowerb = Exclusion.min_of_range r in
-    if BI.compare i BI.zero < 0  then BI.compare lowerb i <= 0
-    else (
+    if Z.compare i Z.zero < 0 then
+      let lowerb = Exclusion.min_of_range r in
+      Z.compare lowerb i <= 0
+    else
       let upperb = Exclusion.max_of_range r in
-      BI.compare i upperb <= 0
-    )
+      Z.compare i upperb <= 0
 
   let is_top x = x = top ()
 
@@ -1921,8 +1921,8 @@ struct
         if R.leq r r' then (* upcast -> no change *)
           `Excluded (s, r)
         else if ik = IBool then (* downcast to bool *)
-          if S.mem BI.zero s then
-            `Definite (BI.one)
+          if S.mem Z.zero s then
+            `Definite Z.one
           else
             `Excluded (S.empty(), r')
         else
@@ -2020,7 +2020,7 @@ struct
       else
         let a,b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
         let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
-        `Excluded ((if BI.equal x BI.zero || BI.equal y BI.zero then S.empty () else S.singleton BI.zero), r)
+        `Excluded ((if Z.equal x Z.zero || Z.equal y Z.zero then S.empty () else S.singleton Z.zero), r)
     (* A known value and an exclusion set... the definite value should no
      * longer be excluded: *)
     | `Excluded (s,r), `Definite x
@@ -2071,14 +2071,14 @@ struct
     | _ -> None
 
   let from_excl ikind (s: S.t) = norm ikind @@ `Excluded (s, size ikind)
-  let not_zero ikind = from_excl ikind (S.singleton BI.zero)
+  let not_zero ikind = from_excl ikind (S.singleton Z.zero)
 
-  let of_bool_cmp ik x = of_int ik (if x then BI.one else BI.zero)
+  let of_bool_cmp ik x = of_int ik (if x then Z.one else Z.zero)
   let of_bool = of_bool_cmp
   let to_bool x =
     match x with
     | `Definite x -> BigInt.to_bool x
-    | `Excluded (s,r) when S.mem BI.zero s -> Some true
+    | `Excluded (s,r) when S.mem Z.zero s -> Some true
     | _ -> None
   let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L))
 
@@ -2249,13 +2249,13 @@ struct
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     (* BigInt only accepts int as second argument for shifts; perform conversion here *)
     let shift_op_big_int a (b: int_t) =
-      let (b : int) = BI.to_int b in
+      let (b : int) = Z.to_int b in
       shift_op a b
     in
     (* If one of the parameters of the shift is negative, the result is undefined *)
     let x_min = minimal x in
     let y_min = minimal y in
-    if x_min = None || y_min = None || BI.compare (Option.get x_min) BI.zero < 0 || BI.compare (Option.get y_min) BI.zero < 0 then
+    if x_min = None || y_min = None || Z.compare (Option.get x_min) Z.zero < 0 || Z.compare (Option.get y_min) Z.zero < 0 then
       top_of ik
     else
       norm ik @@ lift2 shift_op_big_int ik x y
@@ -2298,8 +2298,8 @@ struct
         (Exclusion.min_of_range ikr, Exclusion.max_of_range ikr)
       in
       let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
-      let imin = if inexact_type_bounds || BI.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
-      let imax = if inexact_type_bounds || BI.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
+      let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
+      let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
       S.fold (fun x a ->
           let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
           Invariant.(a && i)
@@ -2410,7 +2410,7 @@ module Enums : S with type int_t = BigInt.t = struct
 
   type t = Inc of BISet.t | Exc of BISet.t * R.t [@@deriving eq, ord, hash] (* inclusion/exclusion set *)
 
-  type int_t = BI.t
+  type int_t = Z.t
   let name () = "enums"
   let bot () = failwith "bot () not implemented for Enums"
   let top_of ik = Exc (BISet.empty (), size ik)
@@ -2486,8 +2486,8 @@ module Enums : S with type int_t = BigInt.t = struct
       if R.leq r r' then (* upcast -> no change *)
         Exc (s, r)
       else if ik = IBool then (* downcast to bool *)
-        if BISet.mem BI.zero s then
-          Inc (BISet.singleton BI.one)
+        if BISet.mem Z.zero s then
+          Inc (BISet.singleton Z.one)
         else
           Exc (BISet.empty(), r')
       else (* downcast: may overflow *)
@@ -2571,22 +2571,22 @@ module Enums : S with type int_t = BigInt.t = struct
 
   let neg ?no_ov = lift1 I.neg
   let add ?no_ov ikind = curry @@ function
-    | Inc z,x when BISet.is_singleton z && BISet.choose z = BI.zero -> x
-    | x,Inc z when BISet.is_singleton z && BISet.choose z = BI.zero -> x
+    | Inc z,x when BISet.is_singleton z && BISet.choose z = Z.zero -> x
+    | x,Inc z when BISet.is_singleton z && BISet.choose z = Z.zero -> x
     | x,y -> lift2 I.add ikind x y
   let sub ?no_ov = lift2 I.sub
   let mul ?no_ov ikind a b =
     match a, b with
-    | Inc one,x when BISet.is_singleton one && BISet.choose one = BI.one -> x
-    | x,Inc one when BISet.is_singleton one && BISet.choose one = BI.one -> x
-    | Inc zero,_ when BISet.is_singleton zero && BISet.choose zero = BI.zero -> a
-    | _,Inc zero when BISet.is_singleton zero && BISet.choose zero = BI.zero -> b
+    | Inc one,x when BISet.is_singleton one && BISet.choose one = Z.one -> x
+    | x,Inc one when BISet.is_singleton one && BISet.choose one = Z.one -> x
+    | Inc zero,_ when BISet.is_singleton zero && BISet.choose zero = Z.zero -> a
+    | _,Inc zero when BISet.is_singleton zero && BISet.choose zero = Z.zero -> b
     | x,y -> lift2 I.mul ikind x y
 
   let div ?no_ov ikind a b = match a, b with
-    | x,Inc one when BISet.is_singleton one && BISet.choose one = BI.one -> x
-    | _,Inc zero when BISet.is_singleton zero && BISet.choose zero = BI.zero -> top_of ikind
-    | Inc zero,_ when BISet.is_singleton zero && BISet.choose zero = BI.zero -> a
+    | x,Inc one when BISet.is_singleton one && BISet.choose one = Z.one -> x
+    | _,Inc zero when BISet.is_singleton zero && BISet.choose zero = Z.zero -> top_of ikind
+    | Inc zero,_ when BISet.is_singleton zero && BISet.choose zero = Z.zero -> a
     | x,y -> lift2 I.div ikind x y
 
   let rem = lift2 I.rem
@@ -2600,13 +2600,13 @@ module Enums : S with type int_t = BigInt.t = struct
     handle_bot x y (fun () ->
         (* BigInt only accepts int as second argument for shifts; perform conversion here *)
         let shift_op_big_int a (b: int_t) =
-          let (b : int) = BI.to_int b in
+          let (b : int) = Z.to_int b in
           shift_op a b
         in
         (* If one of the parameters of the shift is negative, the result is undefined *)
         let x_min = minimal x in
         let y_min = minimal y in
-        if x_min = None || y_min = None || BI.compare (Option.get x_min) BI.zero < 0 || BI.compare (Option.get y_min) BI.zero < 0 then
+        if x_min = None || y_min = None || Z.compare (Option.get x_min) Z.zero < 0 || Z.compare (Option.get y_min) Z.zero < 0 then
           top_of ik
         else
           lift2 shift_op_big_int ik x y)
@@ -2617,13 +2617,13 @@ module Enums : S with type int_t = BigInt.t = struct
   let shift_right =
     shift BigInt.shift_right
 
-  let of_bool ikind x = Inc (BISet.singleton (if x then BI.one else BI.zero))
+  let of_bool ikind x = Inc (BISet.singleton (if x then Z.one else Z.zero))
   let to_bool  = function
     | Inc e when BISet.is_empty e -> None
     | Exc (e,_) when BISet.is_empty e -> None
-    | Inc zero when BISet.is_singleton zero && BISet.choose zero = BI.zero -> Some false
-    | Inc xs when BISet.for_all ((<>) BI.zero) xs -> Some true
-    | Exc (xs,_) when BISet.exists ((=) BI.zero) xs -> Some true
+    | Inc zero when BISet.is_singleton zero && BISet.choose zero = Z.zero -> Some false
+    | Inc xs when BISet.for_all ((<>) Z.zero) xs -> Some true
+    | Exc (xs,_) when BISet.exists ((=) Z.zero) xs -> Some true
     | _ -> None
   let to_int = function Inc x when BISet.is_singleton x -> Some (BISet.choose x) | _ -> None
 
@@ -2653,7 +2653,7 @@ module Enums : S with type int_t = BigInt.t = struct
     | Exc (excl,r) ->
       let rec decrement_while_contained v =
         if BISet.mem v excl
-        then decrement_while_contained (BI.sub v (BI.one))
+        then decrement_while_contained (Z.sub v Z.one)
         else v
       in
       let range_max = Exclusion.max_of_range r in
@@ -2665,7 +2665,7 @@ module Enums : S with type int_t = BigInt.t = struct
     | Exc (excl,r) ->
       let rec increment_while_contained v =
         if BISet.mem v excl
-        then increment_while_contained (BI.add v (BI.one))
+        then increment_while_contained (Z.add v Z.one)
         else v
       in
       let range_min = Exclusion.min_of_range r in
@@ -2734,7 +2734,7 @@ module Enums : S with type int_t = BigInt.t = struct
     ] (* S TODO: decide frequencies *)
 
   let refine_with_congruence ik a b =
-    let contains c m x = if BI.equal m BI.zero then BI.equal c x else BI.equal (BI.rem (BI.sub x c) m) BI.zero in
+    let contains c m x = if Z.equal m Z.zero then Z.equal c x else Z.equal (Z.rem (Z.sub x c) m) Z.zero in
     match a, b with
     | Inc e, None -> bot_of ik
     | Inc e, Some (c, m) -> Inc (BISet.filter (contains c m) e)
@@ -2755,7 +2755,7 @@ module Enums : S with type int_t = BigInt.t = struct
   let project ik p t = t
 end
 
-module Congruence : S with type int_t = BI.t and type t = (BI.t * BI.t) option =
+module Congruence : S with type int_t = Z.t and type t = (Z.t * Z.t) option =
 struct
   let name () = "congruences"
   module Ints_t = BI
@@ -3290,7 +3290,7 @@ module IntDomTupleImpl = struct
   include Printable.Std (* for default invariant, tag, ... *)
 
   open Batteries
-  type int_t = BI.t
+  type int_t = Z.t
   module I1 = SOverflowLifter(DefExc)
   module I2 = Interval
   module I3 = SOverflowLifter(Enums)
@@ -3601,10 +3601,10 @@ module IntDomTupleImpl = struct
       if n>1 then Messages.info ~category:Unsound "Inconsistent state! %a" (Pretty.docList ~sep:(Pretty.text ",") (Pretty.text % show)) us; (* do not want to abort *)
       None
     )
-  let to_int = same BI.to_string % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_int }
+  let to_int = same Z.to_string % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_int }
   let to_bool = same string_of_bool % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.to_bool }
-  let minimal = flat (List.max ~cmp:BI.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.minimal }
-  let maximal = flat (List.min ~cmp:BI.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.maximal }
+  let minimal = flat (List.max ~cmp:Z.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.minimal }
+  let maximal = flat (List.min ~cmp:Z.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.maximal }
   (* others *)
   let show = String.concat "; " % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.name () ^ ":" ^ (I.show x) }
   let to_yojson = [%to_yojson: Yojson.Safe.t list] % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.to_yojson x }

From e0cf71acbe5f6097b59fd27c2b5022e0a5aa8692 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:43:15 +0200
Subject: [PATCH 15/52] Remove I = BI module and replace I. calls with Z.

---
 src/cdomain/value/cdomains/intDomain.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 40e2136781..5090383c7d 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1799,7 +1799,6 @@ end
 module Exclusion =
 struct
   module R = Interval32
-  module I = BI
   (* We use these types for the functions in this module to make the intended meaning more explicit *)
   type t = Exc of BISet.t * Interval32.t
   type inc = Inc of BISet.t [@@unboxed]
@@ -1814,7 +1813,7 @@ struct
     (* For a <= b to hold, the cardinalities must fit, i.e. |a| <= |b|, which implies |min_r, max_r| - |xs| <= |ys|. We check this first. *)
     let lower_bound_cardinality_a = Z.sub (cardinality_of_range r) (cardinality_BISet xs) in
     let card_b = cardinality_BISet ys in
-    if I.compare lower_bound_cardinality_a card_b > 0 then
+    if Z.compare lower_bound_cardinality_a card_b > 0 then
       false
     else (* The cardinality did fit, so we check for all elements that are represented by range r, whether they are in (xs union ys) *)
       let min_a = min_of_range r in
@@ -1823,22 +1822,22 @@ struct
 
   let leq (Exc (xs, r)) (Exc (ys, s)) =
     let min_a, max_a = min_of_range r, max_of_range r in
-    let excluded_check = BISet.for_all (fun y -> BISet.mem y xs || I.compare y min_a < 0 || I.compare y max_a > 0) ys in (* if true, then the values ys, that are not in b, also do not occur in a *)
+    let excluded_check = BISet.for_all (fun y -> BISet.mem y xs || Z.compare y min_a < 0 || Z.compare y max_a > 0) ys in (* if true, then the values ys, that are not in b, also do not occur in a *)
     if not excluded_check
     then false
     else begin (* Check whether all elements that are in the range r, but not in s, are in xs, i.e. excluded. *)
       if R.leq r s then true
-      else begin if I.compare (cardinality_BISet xs) (I.sub (cardinality_of_range r) (cardinality_of_range s)) >= 0 (* Check whether the number of excluded elements in a is as least as big as |min_r, max_r| - |min_s, max_s| *)
+      else begin if Z.compare (cardinality_BISet xs) (Z.sub (cardinality_of_range r) (cardinality_of_range s)) >= 0 (* Check whether the number of excluded elements in a is as least as big as |min_r, max_r| - |min_s, max_s| *)
         then
           let min_b, max_b = min_of_range s, max_of_range s in
           let leq1 = (* check whether the elements in [r_l; s_l-1] are all in xs, i.e. excluded *)
-            if I.compare min_a min_b < 0 then
+            if Z.compare min_a min_b < 0 then
               GobZ.for_all_range (fun x -> BISet.mem x xs) (min_a, Z.sub min_b Z.one)
             else
               true
           in
           let leq2 () = (* check whether the elements in [s_u+1; r_u] are all in xs, i.e. excluded *)
-            if I.compare max_b max_a < 0 then
+            if Z.compare max_b max_a < 0 then
               GobZ.for_all_range (fun x -> BISet.mem x xs) (Z.add max_b Z.one, max_a)
             else
               true

From e9afb07a970eef029010afbf768bb88889fb175c Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:48:15 +0200
Subject: [PATCH 16/52] Remove BI module and inline IntOps.BigIntOps where
 needed

---
 src/cdomain/value/cdomains/intDomain.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 5090383c7d..5b92e51fbc 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -4,7 +4,6 @@ open Pretty
 open PrecisionUtil
 
 module M = Messages
-module BI = IntOps.BigIntOps
 
 let (%) = Batteries.(%)
 let (|?) = Batteries.(|?)
@@ -1547,9 +1546,9 @@ module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type
 end
 
 module IntIkind = struct let ikind () = Cil.IInt end
-module Interval =  IntervalFunctor (BI)
+module Interval =  IntervalFunctor (IntOps.BigIntOps)
 module Interval32 = IntDomWithDefaultIkind (IntDomLifter ( SOverflowUnlifter (IntervalFunctor (IntOps.Int64Ops)) ) ) (IntIkind)
-module IntervalSet = IntervalSetFunctor(BI)
+module IntervalSet = IntervalSetFunctor(IntOps.BigIntOps)
 module Integers(Ints_t : IntOps.IntOps): IkindUnawareS with type t = Ints_t.t and type int_t = Ints_t.t = (* no top/bot, order is <= *)
 struct
   include Printable.Std
@@ -1776,7 +1775,7 @@ struct
 end
 
 module BigInt = struct
-  include  BI
+  include IntOps.BigIntOps
   let name () = "BigIntPrintable"
   let top () = raise Unknown
   let bot () = raise Error
@@ -2757,7 +2756,7 @@ end
 module Congruence : S with type int_t = Z.t and type t = (Z.t * Z.t) option =
 struct
   let name () = "congruences"
-  module Ints_t = BI
+  module Ints_t = IntOps.BigIntOps
   type int_t = Ints_t.t
 
   (* represents congruence class of c mod m, None is bot *)
@@ -3294,7 +3293,7 @@ module IntDomTupleImpl = struct
   module I2 = Interval
   module I3 = SOverflowLifter(Enums)
   module I4 = SOverflowLifter(Congruence)
-  module I5 = IntervalSetFunctor (BI)
+  module I5 = IntervalSetFunctor(IntOps.BigIntOps)
 
   type t = I1.t option * I2.t option * I3.t option * I4.t option * I5.t option
   [@@deriving to_yojson, eq, ord]

From 02a1f080c0e8c9d8849e9c560853e28ae38e0b5e Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 14:52:59 +0200
Subject: [PATCH 17/52] Use Z instead IntOps.BigIntOps for Ints_t in Congurence

---
 src/cdomain/value/cdomains/intDomain.ml | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 5b92e51fbc..2371bc702f 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2756,7 +2756,7 @@ end
 module Congruence : S with type int_t = Z.t and type t = (Z.t * Z.t) option =
 struct
   let name () = "congruences"
-  module Ints_t = IntOps.BigIntOps
+  module Ints_t = Z
   type int_t = Ints_t.t
 
   (* represents congruence class of c mod m, None is bot *)
@@ -2793,7 +2793,7 @@ struct
         else
           Some (c' %: m', m')
 
-  let range ik = BatTuple.Tuple2.mapn Ints_t.of_bigint (Size.range ik)
+  let range ik = Size.range ik
 
   let top () = Some (Ints_t.zero, Ints_t.one)
   let top_of ik = Some (Ints_t.zero, Ints_t.one)
@@ -2904,7 +2904,7 @@ struct
     match x with
     | None -> None
     | Some (c, m) when m =: Ints_t.zero ->
-      let c' = Ints_t.of_bigint @@ BigInt.cast_to t (Ints_t.to_bigint c) in
+      let c' = BigInt.cast_to t c in
       (* When casting into a signed type and the result does not fit, the behavior is implementation-defined. (C90 6.2.1.2, C99 and C11 6.3.1.3) *)
       (* We go with GCC behavior here: *)
       (*  For conversion to a type of width N, the value is reduced modulo 2^N to be within range of the type; no signal is raised. *)
@@ -2985,10 +2985,10 @@ struct
     | Some (c, m), Some (c', m') when (Cil.isSigned ik) || c <: Ints_t.zero || c' <: Ints_t.zero -> top_of ik
     | Some (c, m), Some (c', m') ->
       let (_, max_ik) = range ik in
-      if (m =: Ints_t.zero && m' =: Ints_t.zero) then
-        normalize ik @@ Some (Ints_t.bitand max_ik (Ints_t.shift_left c (Ints_t.to_int c')), Ints_t.zero)
+      if m =: Ints_t.zero && m' =: Ints_t.zero then
+        normalize ik @@ Some (Z.logand max_ik (Ints_t.shift_left c (Ints_t.to_int c')), Ints_t.zero)
       else
-        let x = (Ints_t.bitand max_ik (Ints_t.shift_left Ints_t.one (Ints_t.to_int c'))) in   (* 2^c' *)
+        let x = Z.logand max_ik (Ints_t.shift_left Ints_t.one (Ints_t.to_int c')) in (* 2^c' *)
         (* TODO: commented out because fails test with _Bool *)
         (* if is_prime (m' +: Ints_t.one) then
              normalize ik @@ Some (x *: c, Ints_t.gcd (x *: m) ((c *: x) *: (m' +: Ints_t.one)))
@@ -3100,7 +3100,7 @@ struct
       if (m =: Ints_t.zero && m' =: Ints_t.zero) then Some (f c c', Ints_t.zero)
       else top ()
 
-  let bitor ik x y = bit2 Ints_t.bitor ik x y
+  let bitor ik x y = bit2 Z.logor ik x y
 
   let bitand ik x y =  match x, y with
     | None, None -> None
@@ -3108,15 +3108,15 @@ struct
     | Some (c, m), Some (c', m') ->
       if (m =: Ints_t.zero && m' =: Ints_t.zero) then
         (* both arguments constant *)
-        Some (Ints_t.bitand c c', Ints_t.zero)
+        Some (Z.logand c c', Ints_t.zero)
       else if m' =: Ints_t.zero && c' =: Ints_t.one && Ints_t.rem m (Ints_t.of_int 2) =: Ints_t.zero then
         (* x & 1  and  x == c (mod 2*z) *)
         (* Value is equal to LSB of c *)
-        Some (Ints_t.bitand c c', Ints_t.zero)
+        Some (Z.logand c c', Ints_t.zero)
       else
         top ()
 
-  let bitxor ik x y = bit2 Ints_t.bitxor ik x y
+  let bitxor ik x y = bit2 Z.logxor ik x y
 
   let rem ik x y =
     match x, y with
@@ -3202,13 +3202,12 @@ struct
     | x when is_top x -> Invariant.top ()
     | Some (c, m) when m =: Ints_t.zero ->
       if get_bool "witness.invariant.exact" then
-        let c = Ints_t.to_bigint c in
         Invariant.of_exp Cil.(BinOp (Eq, e, Cil.kintegerCilint ik c, intType))
       else
         Invariant.top ()
     | Some (c, m) ->
       let open Cil in
-      let (c, m) = BatTuple.Tuple2.mapn (fun a -> kintegerCilint ik @@ Ints_t.to_bigint a) (c, m) in
+      let (c, m) = BatTuple.Tuple2.mapn (fun a -> kintegerCilint ik a) (c, m) in
       Invariant.of_exp (BinOp (Eq, (BinOp (Mod, e, m, TInt(ik,[]))), c, intType))
     | None -> Invariant.none
 

From f6e991cfeb1fc8bc625a427f03360398e8a85afb Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 15:08:00 +0200
Subject: [PATCH 18/52] Remove Ints_t from Congurence and use Z directly

---
 src/cdomain/value/cdomains/intDomain.ml | 181 ++++++++++++------------
 1 file changed, 91 insertions(+), 90 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 2371bc702f..2d7dd1d024 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2756,56 +2756,55 @@ end
 module Congruence : S with type int_t = Z.t and type t = (Z.t * Z.t) option =
 struct
   let name () = "congruences"
-  module Ints_t = Z
-  type int_t = Ints_t.t
+  type int_t = Z.t
 
   (* represents congruence class of c mod m, None is bot *)
-  type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord, hash]
-
-  let ( *: ) = Ints_t.mul
-  let (+:) = Ints_t.add
-  let (-:) = Ints_t.sub
-  let (%:) = Ints_t.rem
-  let (/:) = Ints_t.div
-  let (=:) = Ints_t.equal
-  let (<:) x y = Ints_t.compare x y < 0
-  let (>:) x y = Ints_t.compare x y > 0
-  let (<=:) x y = Ints_t.compare x y <= 0
-  let (>=:) x y = Ints_t.compare x y >= 0
+  type t = (Z.t * Z.t) option [@@deriving eq, ord, hash]
+
+  let ( *: ) = Z.mul
+  let (+:) = Z.add
+  let (-:) = Z.sub
+  let (%:) = Z.rem
+  let (/:) = Z.div
+  let (=:) = Z.equal
+  let (<:) x y = Z.compare x y < 0
+  let (>:) x y = Z.compare x y > 0
+  let (<=:) x y = Z.compare x y <= 0
+  let (>=:) x y = Z.compare x y >= 0
   (* a divides b *)
   let ( |: ) a b =
-    if a =: Ints_t.zero then false else (b %: a) =: Ints_t.zero
+    if a =: Z.zero then false else (b %: a) =: Z.zero
 
   let normalize ik x =
     match x with
     | None -> None
     | Some (c, m) ->
-      if m =: Ints_t.zero then
+      if m =: Z.zero then
         if should_wrap ik then
           Some (BigInt.cast_to ik c, m)
         else
           Some (c, m)
       else
-        let m' = Ints_t.abs m in
+        let m' = Z.abs m in
         let c' = c %: m' in
-        if c' <: Ints_t.zero then
+        if c' <: Z.zero then
           Some (c' +: m', m')
         else
           Some (c' %: m', m')
 
   let range ik = Size.range ik
 
-  let top () = Some (Ints_t.zero, Ints_t.one)
-  let top_of ik = Some (Ints_t.zero, Ints_t.one)
+  let top () = Some (Z.zero, Z.one)
+  let top_of ik = Some (Z.zero, Z.one)
   let bot () = None
   let bot_of ik = bot ()
 
   let show = function ik -> match ik with
     | None -> "⟂"
-    | Some (c, m) when (c, m) = (Ints_t.zero, Ints_t.zero) -> Ints_t.to_string c
+    | Some (c, m) when (c, m) = (Z.zero, Z.zero) -> Z.to_string c
     | Some (c, m) ->
-      let a = if c =: Ints_t.zero then "" else Ints_t.to_string c in
-      let b = if m =: Ints_t.zero then "" else if m = Ints_t.one then "ℤ" else Ints_t.to_string m^"ℤ" in
+      let a = if c =: Z.zero then "" else Z.to_string c in
+      let b = if m =: Z.zero then "" else if m = Z.one then "ℤ" else Z.to_string m^"ℤ" in
       let c = if a = "" || b = "" then "" else "+" in
       a^c^b
 
@@ -2815,29 +2814,29 @@ struct
 
   let equal_to i = function
     | None -> failwith "unsupported: equal_to with bottom"
-    | Some (a, b) when b =: Ints_t.zero -> if a =: i then `Eq else `Neq
+    | Some (a, b) when b =: Z.zero -> if a =: i then `Eq else `Neq
     | Some (a, b) ->  if i %: b =: a then `Top else `Neq
 
   let leq (x:t) (y:t) =
     match x, y with
     | None, _ -> true
     | Some _, None -> false
-    | Some (c1,m1), Some (c2,m2) when m2 =: Ints_t.zero && m1 =: Ints_t.zero -> c1 =: c2
-    | Some (c1,m1), Some (c2,m2) when m2 =: Ints_t.zero -> c1 =: c2 && m1 =: Ints_t.zero
-    | Some (c1,m1), Some (c2,m2) -> m2 |: (Ints_t.gcd (c1 -: c2) m1)
+    | Some (c1,m1), Some (c2,m2) when m2 =: Z.zero && m1 =: Z.zero -> c1 =: c2
+    | Some (c1,m1), Some (c2,m2) when m2 =: Z.zero -> c1 =: c2 && m1 =: Z.zero
+    | Some (c1,m1), Some (c2,m2) -> m2 |: Z.gcd (c1 -: c2) m1
   (* Typo in original equation of P. Granger (m2 instead of m1): gcd (c1 -: c2) m2
      Reference: https://doi.org/10.1080/00207168908803778 Page 171 corollary 3.3*)
 
   let leq x y =
     let res = leq x y in
-    if M.tracing then M.trace "congruence" "leq %a %a -> %a \n" pretty x pretty y pretty (Some(Ints_t.of_int (Bool.to_int res), Ints_t.zero)) ;
+    if M.tracing then M.trace "congruence" "leq %a %a -> %a \n" pretty x pretty y pretty (Some (Z.of_int (Bool.to_int res), Z.zero)) ;
     res
 
   let join ik (x:t) y =
     match x, y with
     | None, z | z, None -> z
     | Some (c1,m1), Some (c2,m2) ->
-      let m3 = Ints_t.gcd m1 (Ints_t.gcd m2 (c1 -: c2)) in
+      let m3 = Z.gcd m1 (Z.gcd m2 (c1 -: c2)) in
       normalize ik (Some (c1, m3))
 
   let join ik (x:t) y =
@@ -2852,17 +2851,17 @@ struct
       let rec next a1 c1 a2 c2 =
         if a2 |: a1 then (a2, c2)
         else next a2 c2 (a1 %: a2) (c1 -: (c2 *: (a1 /: a2)))
-      in next m Ints_t.zero a c
+      in next m Z.zero a c
     in
     let simple_case i c m =
       if m |: (i -: c)
-      then Some (i, Ints_t.zero) else None
+      then Some (i, Z.zero) else None
     in
     match x, y with
-    | Some (c1, m1), Some (c2, m2) when m1 =: Ints_t.zero && m2 =: Ints_t.zero -> if c1 =: c2 then Some (c1, Ints_t.zero) else None
-    | Some (c1, m1), Some (c2, m2) when m1 =: Ints_t.zero -> simple_case c1 c2 m2
-    | Some (c1, m1), Some (c2, m2) when m2 =: Ints_t.zero -> simple_case c2 c1 m1
-    | Some (c1, m1), Some (c2, m2) when (Ints_t.gcd m1 m2) |: (c1 -: c2) ->
+    | Some (c1, m1), Some (c2, m2) when m1 =: Z.zero && m2 =: Z.zero -> if c1 =: c2 then Some (c1, Z.zero) else None
+    | Some (c1, m1), Some (c2, m2) when m1 =: Z.zero -> simple_case c1 c2 m2
+    | Some (c1, m1), Some (c2, m2) when m2 =: Z.zero -> simple_case c2 c1 m1
+    | Some (c1, m1), Some (c2, m2) when (Z.gcd m1 m2) |: (c1 -: c2) ->
       let (c, m) = congruence_series m1 (c2 -: c1 ) m2 in
       normalize ik (Some(c1 +: (m1 *: (m /: c)), m1 *: (m2 /: c)))
     | _  -> None
@@ -2872,10 +2871,10 @@ struct
     if M.tracing then M.trace "congruence" "meet %a %a -> %a\n" pretty x pretty y pretty res;
     res
 
-  let to_int = function Some (c, m) when m =: Ints_t.zero -> Some c | _ -> None
-  let of_int ik (x: int_t) = normalize ik @@ Some (x, Ints_t.zero)
-  let zero = Some (Ints_t.zero, Ints_t.zero)
-  let one  = Some (Ints_t.one, Ints_t.zero)
+  let to_int = function Some (c, m) when m =: Z.zero -> Some c | _ -> None
+  let of_int ik (x: int_t) = normalize ik @@ Some (x, Z.zero)
+  let zero = Some (Z.zero, Z.zero)
+  let one  = Some (Z.one, Z.zero)
   let top_bool = top()
 
   let of_bool _ik = function true -> one | false -> zero
@@ -2892,18 +2891,18 @@ struct
   let of_congruence ik (c,m) = normalize ik @@ Some(c,m)
 
   let maximal t = match t with
-    | Some (x, y) when y =: Ints_t.zero -> Some x
+    | Some (x, y) when y =: Z.zero -> Some x
     | _ -> None
 
   let minimal t = match t with
-    | Some (x,y) when y =: Ints_t.zero -> Some x
+    | Some (x,y) when y =: Z.zero -> Some x
     | _ -> None
 
   (* cast from original type to ikind, set to top if the value doesn't fit into the new type *)
   let cast_to ?torg ?(no_ov=false) t x =
     match x with
     | None -> None
-    | Some (c, m) when m =: Ints_t.zero ->
+    | Some (c, m) when m =: Z.zero ->
       let c' = BigInt.cast_to t c in
       (* When casting into a signed type and the result does not fit, the behavior is implementation-defined. (C90 6.2.1.2, C99 and C11 6.3.1.3) *)
       (* We go with GCC behavior here: *)
@@ -2972,28 +2971,28 @@ struct
   let shift_left ik x y =
     (* Naive primality test *)
     (* let is_prime n =
-         let n = Ints_t.abs n in
+         let n = Z.abs n in
          let rec is_prime' d =
-           (d *: d >: n) || ((not ((n %: d) =: Ints_t.zero)) && (is_prime' [@tailcall]) (d +: Ints_t.one))
+           (d *: d >: n) || ((not ((n %: d) =: Z.zero)) && (is_prime' [@tailcall]) (d +: Z.one))
          in
-         not (n =: Ints_t.one) && is_prime' (Ints_t.of_int 2)
+         not (n =: Z.one) && is_prime' (Z.of_int 2)
        in *)
     match x, y with
     | None, None -> None
     | None, _
     | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
-    | Some (c, m), Some (c', m') when (Cil.isSigned ik) || c <: Ints_t.zero || c' <: Ints_t.zero -> top_of ik
+    | Some (c, m), Some (c', m') when Cil.isSigned ik || c <: Z.zero || c' <: Z.zero -> top_of ik
     | Some (c, m), Some (c', m') ->
       let (_, max_ik) = range ik in
-      if m =: Ints_t.zero && m' =: Ints_t.zero then
-        normalize ik @@ Some (Z.logand max_ik (Ints_t.shift_left c (Ints_t.to_int c')), Ints_t.zero)
+      if m =: Z.zero && m' =: Z.zero then
+        normalize ik @@ Some (Z.logand max_ik (Z.shift_left c (Z.to_int c')), Z.zero)
       else
-        let x = Z.logand max_ik (Ints_t.shift_left Ints_t.one (Ints_t.to_int c')) in (* 2^c' *)
+        let x = Z.logand max_ik (Z.shift_left Z.one (Z.to_int c')) in (* 2^c' *)
         (* TODO: commented out because fails test with _Bool *)
-        (* if is_prime (m' +: Ints_t.one) then
-             normalize ik @@ Some (x *: c, Ints_t.gcd (x *: m) ((c *: x) *: (m' +: Ints_t.one)))
+        (* if is_prime (m' +: Z.one) then
+             normalize ik @@ Some (x *: c, Z.gcd (x *: m) ((c *: x) *: (m' +: Z.one)))
            else *)
-        normalize ik @@ Some (x *: c, Ints_t.gcd (x *: m) (c *: x))
+        normalize ik @@ Some (x *: c, Z.gcd (x *: m) (c *: x))
 
   let shift_left ik x y =
     let res = shift_left ik x y in
@@ -3004,24 +3003,24 @@ struct
      From n === k mod (2^a * b), we conclude n === k mod 2^a, for a <= bitwidth.
      The congruence modulo b may not persist on an overflow. *)
   let handle_overflow ik (c, m) =
-    if m =: Ints_t.zero then
+    if m =: Z.zero then
       normalize ik (Some (c, m))
     else
       (* Find largest m'=2^k (for some k) such that m is divisible by m' *)
-      let tz = Ints_t.trailing_zeros m in
-      let m' = Ints_t.shift_left (Ints_t.of_int 1) tz in
+      let tz = Z.trailing_zeros m in
+      let m' = Z.shift_left (Z.of_int 1) tz in
 
-      let max = (snd (Size.range ik)) +: Ints_t.one in
+      let max = (snd (Size.range ik)) +: Z.one in
       if m' >=: max then
         (* if m' >= 2 ^ {bitlength}, there is only one value in range *)
         let c' = c %: max in
-        Some (c', Ints_t.zero)
+        Some (c', Z.zero)
       else
         normalize ik (Some (c, m'))
 
   let mul ?(no_ov=false) ik x y =
     let no_ov_case (c1, m1) (c2, m2) =
-      (c1 *: c2, Ints_t.gcd (c1 *: m2) (Ints_t.gcd (m1 *: c2) (m1 *: m2)))
+      c1 *: c2, Z.gcd (c1 *: m2) (Z.gcd (m1 *: c2) (m1 *: m2))
     in
     match x, y with
     | None, None -> bot ()
@@ -3029,9 +3028,9 @@ struct
       raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c1, m1), Some (c2, m2) when no_ov ->
       Some (no_ov_case (c1, m1) (c2, m2))
-    | Some (c1, m1), Some (c2, m2) when m1 =: Ints_t.zero && m2 =: Ints_t.zero && not (Cil.isSigned ik) ->
+    | Some (c1, m1), Some (c2, m2) when m1 =: Z.zero && m2 =: Z.zero && not (Cil.isSigned ik) ->
       let (_, max_ik) = range ik in
-      Some((c1 *: c2) %: (max_ik +: Ints_t.one), Ints_t.zero)
+      Some ((c1 *: c2) %: (max_ik +: Z.one), Z.zero)
     | Some a, Some b when not (Cil.isSigned ik) ->
       handle_overflow ik (no_ov_case a b )
     | _ -> top ()
@@ -3044,11 +3043,11 @@ struct
   let neg ?(no_ov=false) ik x =
     match x with
     | None -> bot()
-    | Some _ ->  mul ~no_ov ik (of_int ik (Ints_t.of_int (-1))) x
+    | Some _ -> mul ~no_ov ik (of_int ik (Z.of_int (-1))) x
 
   let add ?(no_ov=false) ik x y =
     let no_ov_case (c1, m1) (c2, m2) =
-      c1 +: c2, Ints_t.gcd m1 m2
+      c1 +: c2, Z.gcd m1 m2
     in
     match (x, y) with
     | None, None -> bot ()
@@ -3056,9 +3055,9 @@ struct
       raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some a, Some b when no_ov ->
       normalize ik (Some (no_ov_case a b))
-    | Some (c1, m1), Some (c2, m2) when m1 =: Ints_t.zero && m2 =: Ints_t.zero && not (Cil.isSigned ik) ->
+    | Some (c1, m1), Some (c2, m2) when m1 =: Z.zero && m2 =: Z.zero && not (Cil.isSigned ik) ->
       let (_, max_ik) = range ik in
-      Some((c1 +: c2) %: (max_ik +: Ints_t.one), Ints_t.zero)
+      Some((c1 +: c2) %: (max_ik +: Z.one), Z.zero)
     | Some a, Some b when not (Cil.isSigned ik) ->
       handle_overflow ik (no_ov_case a b)
     | _ -> top ()
@@ -3088,7 +3087,7 @@ struct
         sub ik (neg ik x) one
       else
         let (_, max_ik) = range ik in
-        Some (Ints_t.sub max_ik c, m)
+        Some (Z.sub max_ik c, m)
 
   (** The implementation of the bit operations could be improved based on the master’s thesis
       'Abstract Interpretation and Abstract Domains' written by Stefan Bygde.
@@ -3097,7 +3096,7 @@ struct
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c, m), Some (c', m') ->
-      if (m =: Ints_t.zero && m' =: Ints_t.zero) then Some (f c c', Ints_t.zero)
+      if m =: Z.zero && m' =: Z.zero then Some (f c c', Z.zero)
       else top ()
 
   let bitor ik x y = bit2 Z.logor ik x y
@@ -3106,13 +3105,13 @@ struct
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c, m), Some (c', m') ->
-      if (m =: Ints_t.zero && m' =: Ints_t.zero) then
+      if m =: Z.zero && m' =: Z.zero then
         (* both arguments constant *)
-        Some (Z.logand c c', Ints_t.zero)
-      else if m' =: Ints_t.zero && c' =: Ints_t.one && Ints_t.rem m (Ints_t.of_int 2) =: Ints_t.zero then
+        Some (Z.logand c c', Z.zero)
+      else if m' =: Z.zero && c' =: Z.one && Z.rem m (Z.of_int 2) =: Z.zero then
         (* x & 1  and  x == c (mod 2*z) *)
         (* Value is equal to LSB of c *)
-        Some (Z.logand c c', Ints_t.zero)
+        Some (Z.logand c c', Z.zero)
       else
         top ()
 
@@ -3123,13 +3122,13 @@ struct
     | None, None -> bot()
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c1, m1), Some(c2, m2) ->
-      if m2 =: Ints_t.zero then
-        if (c2 |: m1) && (c1 %: c2 =: Ints_t.zero || m1 =: Ints_t.zero || not (Cil.isSigned ik)) then
-          Some(c1 %: c2, Ints_t.zero)
+      if m2 =: Z.zero then
+        if (c2 |: m1) && (c1 %: c2 =: Z.zero || m1 =: Z.zero || not (Cil.isSigned ik)) then
+          Some (c1 %: c2, Z.zero)
         else
-          normalize ik (Some(c1, (Ints_t.gcd m1 c2)))
+          normalize ik (Some (c1, (Z.gcd m1 c2)))
       else
-        normalize ik (Some(c1, Ints_t.gcd m1 (Ints_t.gcd c2 m2)))
+        normalize ik (Some (c1, Z.gcd m1 (Z.gcd c2 m2)))
 
   let rem ik x y = let res = rem ik x y in
     if M.tracing then  M.trace "congruence" "rem : %a %a -> %a \n" pretty x pretty y pretty res;
@@ -3140,9 +3139,9 @@ struct
     | None, None -> bot ()
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | _, x when leq zero x -> top ()
-    | Some(c1, m1), Some(c2, m2) when not no_ov && m2 =: Ints_t.zero && c2 =: Ints_t.neg Ints_t.one -> top ()
-    | Some(c1, m1), Some(c2, m2) when m1 =: Ints_t.zero && m2 =: Ints_t.zero -> Some(c1 /: c2, Ints_t.zero)
-    | Some(c1, m1), Some(c2, m2) when m2 =: Ints_t.zero ->  if (c2 |: m1) && (c2 |: c1) then Some(c1 /: c2, m1 /: c2) else top ()
+    | Some(c1, m1), Some(c2, m2) when not no_ov && m2 =: Z.zero && c2 =: Z.neg Z.one -> top ()
+    | Some(c1, m1), Some(c2, m2) when m1 =: Z.zero && m2 =: Z.zero -> Some (c1 /: c2, Z.zero)
+    | Some(c1, m1), Some(c2, m2) when m2 =: Z.zero && c2 |: m1 && c2 |: c1 -> Some (c1 /: c2, m1 /: c2)
     | _, _ -> top ()
 
 
@@ -3154,19 +3153,21 @@ struct
     res
 
   let ne ik (x: t) (y: t) = match x, y with
-    | Some (c1, m1), Some (c2, m2) when (m1 =: Ints_t.zero) && (m2 =: Ints_t.zero) -> of_bool ik (not (c1 =: c2 ))
+    | Some (c1, m1), Some (c2, m2) when (m1 =: Z.zero) && (m2 =: Z.zero) -> of_bool ik (not (c1 =: c2 ))
     | x, y -> if meet ik x y = None then of_bool ik true else top_bool
 
   let eq ik (x: t) (y: t) = match x, y with
-    | Some (c1, m1), Some (c2, m2) when (m1 =: Ints_t.zero) && (m2 =: Ints_t.zero) -> of_bool ik (c1 =: c2)
+    | Some (c1, m1), Some (c2, m2) when (m1 =: Z.zero) && (m2 =: Z.zero) -> of_bool ik (c1 =: c2)
     | x, y -> if meet ik x y <> None then top_bool else of_bool ik false
 
   let comparison ik op x y = match x, y with
     | None, None -> bot_of ik
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
-    | Some (c1, m1), Some(c2, m2) -> if (m1 =: Ints_t.zero) && (m2 =: Ints_t.zero) then
+    | Some (c1, m1), Some (c2, m2) ->
+      if m1 =: Z.zero && m2 =: Z.zero then
         if op c1 c2 then of_bool ik true else of_bool ik false
-      else top_bool
+      else
+        top_bool
 
   let ge ik x y = comparison ik (>=:) x y
 
@@ -3200,7 +3201,7 @@ struct
   let invariant_ikind e ik x =
     match x with
     | x when is_top x -> Invariant.top ()
-    | Some (c, m) when m =: Ints_t.zero ->
+    | Some (c, m) when m =: Z.zero ->
       if get_bool "witness.invariant.exact" then
         Invariant.of_exp Cil.(BinOp (Eq, e, Cil.kintegerCilint ik c, intType))
       else
@@ -3213,7 +3214,7 @@ struct
 
   let arbitrary ik =
     let open QCheck in
-    let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
+    let int_arb = map ~rev:Z.to_int64 Z.of_int64 GobQCheck.Arbitrary.int64 in
     let cong_arb = pair int_arb int_arb in
     let of_pair ik p = normalize ik (Some p) in
     let to_pair = Option.get in
@@ -3222,19 +3223,19 @@ struct
   let refine_with_interval ik (cong : t) (intv : (int_t * int_t ) option) : t =
     match intv, cong with
     | Some (x, y), Some (c, m) ->
-      if m =: Ints_t.zero then
-        if (c <: x || c >: y) then None else Some (c, Ints_t.zero)
+      if m =: Z.zero then
+        if c <: x || c >: y then None else Some (c, Z.zero)
       else
-        let rcx = x +: ((c -: x) %: Ints_t.abs m) in
-        let lcy = y -: ((y -: c) %: Ints_t.abs m) in
+        let rcx = x +: ((c -: x) %: Z.abs m) in
+        let lcy = y -: ((y -: c) %: Z.abs m) in
         if rcx >: lcy then None
-        else if rcx =: lcy then Some (rcx, Ints_t.zero)
+        else if rcx =: lcy then Some (rcx, Z.zero)
         else cong
     | _ -> None
 
   let refine_with_interval ik (cong : t) (intv : (int_t * int_t) option) : t =
     let pretty_intv _ i = (match i with
-        | Some(l, u) -> let s = "["^Ints_t.to_string l^","^Ints_t.to_string u^"]" in Pretty.text s
+        | Some(l, u) -> let s = "["^Z.to_string l^","^Z.to_string u^"]" in Pretty.text s
         | _ -> Pretty.text ("Display Error")) in
     let refn = refine_with_interval ik cong intv in
     if M.tracing then M.trace "refine" "cong_refine_with_interval %a %a -> %a\n" pretty cong pretty_intv intv pretty refn;

From d627cdc0346a747d33391b58978e177eff62c908 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 15:22:42 +0200
Subject: [PATCH 19/52] Address semgrep findings

---
 src/analyses/baseInvariant.ml             |  8 ++++----
 src/cdomain/value/cdomains/arrayDomain.ml | 10 +++++-----
 src/cdomain/value/cdomains/intDomain.ml   | 12 ++++++------
 3 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 7176ea5695..366615a1b5 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -168,7 +168,7 @@ struct
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
               let n = ID.cast_to ikind n in
-              let range_from x = if tv then ID.ending ikind (Z.sub x Z.one) else ID.starting ikind x in
+              let range_from x = if tv then ID.ending ikind (Z.pred x) else ID.starting ikind x in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
@@ -183,7 +183,7 @@ struct
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
               let n = ID.cast_to ikind n in
-              let range_from x = if tv then ID.ending ikind x else ID.starting ikind (Z.add x Z.one) in
+              let range_from x = if tv then ID.ending ikind x else ID.starting ikind (Z.succ x) in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
@@ -380,8 +380,8 @@ struct
           | _, _ -> a, b
         end
       | Lt | Le | Ge | Gt as op ->
-        let pred x = Z.sub x Z.one in
-        let succ x = Z.add x Z.one in
+        let pred x = Z.pred x in
+        let succ x = Z.succ x in
         (match ID.minimal a, ID.maximal a, ID.minimal b, ID.maximal b with
          | Some l1, Some u1, Some l2, Some u2 ->
            (* if M.tracing then M.tracel "inv" "Op: %s, l1: %Ld, u1: %Ld, l2: %Ld, u2: %Ld\n" (show_binop op) l1 u1 l2 u2; *)
diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml
index 162d782951..ac9af3c5a4 100644
--- a/src/cdomain/value/cdomains/arrayDomain.ml
+++ b/src/cdomain/value/cdomains/arrayDomain.ml
@@ -556,7 +556,7 @@ struct
         | Some l ->
           begin
             match Idx.to_int l with
-            | Some i -> BatOption.map_default (Z.equal (Z.sub i Z.one)) false (exp_value e)
+            | Some i -> BatOption.map_default (Z.equal (Z.pred i)) false (exp_value e)
             | None -> false
           end
         | _ -> false
@@ -596,10 +596,10 @@ struct
             else if Cil.isConstant e && Cil.isConstant i' then
               match Cil.getInteger e, Cil.getInteger i' with
               | Some (e'': Cilint.cilint), Some i'' ->
-                if Z.equal  i'' (Z.add e'' Z.one) then
+                if Z.equal  i'' (Z.succ e'') then
                   (* If both are integer constants and they are directly adjacent, we change partitioning to maintain information *)
                   Partitioned (i', (Val.join xl xm, a, xr))
-                else if Z.equal e'' (Z.add i'' Z.one) then
+                else if Z.equal e'' (Z.succ i'') then
                   Partitioned (i', (xl, a, Val.join xm xr))
                 else
                   default
@@ -673,7 +673,7 @@ struct
         begin
           match Idx.to_int l with
           | Some i ->
-            v = Some (Z.sub i Z.one)
+            v = Some (Z.pred i)
           | None -> false
         end
       | None -> false
@@ -748,7 +748,7 @@ struct
         begin
           match Idx.to_int l with
           | Some i ->
-            v = Some (Z.sub i Z.one)
+            v = Some (Z.pred i)
           | None -> false
         end
       | None -> false
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 2d7dd1d024..7415444c2c 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1803,7 +1803,7 @@ struct
   type inc = Inc of BISet.t [@@unboxed]
   let max_of_range r = Size.max_from_bit_range (Option.get (R.maximal r))
   let min_of_range r = Size.min_from_bit_range (Option.get (R.minimal r))
-  let cardinality_of_range r = Z.add Z.one (Z.add (Z.neg (min_of_range r)) (max_of_range r))
+  let cardinality_of_range r = Z.succ (Z.add (Z.neg (min_of_range r)) (max_of_range r))
 
   let cardinality_BISet s =
     Z.of_int (BISet.cardinal s)
@@ -1831,13 +1831,13 @@ struct
           let min_b, max_b = min_of_range s, max_of_range s in
           let leq1 = (* check whether the elements in [r_l; s_l-1] are all in xs, i.e. excluded *)
             if Z.compare min_a min_b < 0 then
-              GobZ.for_all_range (fun x -> BISet.mem x xs) (min_a, Z.sub min_b Z.one)
+              GobZ.for_all_range (fun x -> BISet.mem x xs) (min_a, Z.pred min_b)
             else
               true
           in
           let leq2 () = (* check whether the elements in [s_u+1; r_u] are all in xs, i.e. excluded *)
             if Z.compare max_b max_a < 0 then
-              GobZ.for_all_range (fun x -> BISet.mem x xs) (Z.add max_b Z.one, max_a)
+              GobZ.for_all_range (fun x -> BISet.mem x xs) (Z.succ max_b, max_a)
             else
               true
           in
@@ -2651,7 +2651,7 @@ module Enums : S with type int_t = BigInt.t = struct
     | Exc (excl,r) ->
       let rec decrement_while_contained v =
         if BISet.mem v excl
-        then decrement_while_contained (Z.sub v Z.one)
+        then decrement_while_contained (Z.pred v)
         else v
       in
       let range_max = Exclusion.max_of_range r in
@@ -2663,7 +2663,7 @@ module Enums : S with type int_t = BigInt.t = struct
     | Exc (excl,r) ->
       let rec increment_while_contained v =
         if BISet.mem v excl
-        then increment_while_contained (Z.add v Z.one)
+        then increment_while_contained (Z.succ v)
         else v
       in
       let range_min = Exclusion.min_of_range r in
@@ -3008,7 +3008,7 @@ struct
     else
       (* Find largest m'=2^k (for some k) such that m is divisible by m' *)
       let tz = Z.trailing_zeros m in
-      let m' = Z.shift_left (Z.of_int 1) tz in
+      let m' = Z.shift_left Z.one tz in
 
       let max = (snd (Size.range ik)) +: Z.one in
       if m' >=: max then

From 4f8e9569286ef715329997a0864f4e8408bc5c01 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 18:03:14 +0200
Subject: [PATCH 20/52] Fix spacing in module definitions

---
 src/cdomain/value/cdomains/intDomain.ml | 36 ++++++++++++-------------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 7415444c2c..3ed8a86c59 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -505,7 +505,7 @@ module Std (B: sig
 end
 
 (* Textbook interval arithmetic, without any overflow handling etc. *)
-module IntervalArith(Ints_t : IntOps.IntOps) = struct
+module IntervalArith (Ints_t : IntOps.IntOps) = struct
   let min4 a b c d = Ints_t.min (Ints_t.min a b) (Ints_t.min c d)
   let max4 a b c d = Ints_t.max (Ints_t.max a b) (Ints_t.max c d)
 
@@ -545,12 +545,12 @@ module IntervalArith(Ints_t : IntOps.IntOps) = struct
     if Ints_t.equal x1 x2 then Some x1 else None
 end
 
-module IntervalFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =
+module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow 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 [@@deriving eq, ord, hash]
-  module IArith = IntervalArith(Ints_t)
+  module IArith = IntervalArith (Ints_t)
 
   let range ik = BatTuple.Tuple2.mapn Ints_t.of_bigint (Size.range ik)
 
@@ -974,11 +974,11 @@ struct
 end
 
 (** IntervalSetFunctor that is not just disjunctive completion of intervals, but attempts to be precise for wraparound arithmetic for unsigned types *)
-module IntervalSetFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) list =
+module IntervalSetFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) list =
 struct
 
-  module Interval = IntervalFunctor(Ints_t)
-  module IArith = IntervalArith(Ints_t)
+  module Interval = IntervalFunctor (Ints_t)
+  module IArith = IntervalArith (Ints_t)
 
 
   let name () = "interval_sets"
@@ -1546,10 +1546,10 @@ module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type
 end
 
 module IntIkind = struct let ikind () = Cil.IInt end
-module Interval =  IntervalFunctor (IntOps.BigIntOps)
-module Interval32 = IntDomWithDefaultIkind (IntDomLifter ( SOverflowUnlifter (IntervalFunctor (IntOps.Int64Ops)) ) ) (IntIkind)
-module IntervalSet = IntervalSetFunctor(IntOps.BigIntOps)
-module Integers(Ints_t : IntOps.IntOps): IkindUnawareS with type t = Ints_t.t and type int_t = Ints_t.t = (* no top/bot, order is <= *)
+module Interval = IntervalFunctor (IntOps.BigIntOps)
+module Interval32 = IntDomWithDefaultIkind (IntDomLifter (SOverflowUnlifter (IntervalFunctor (IntOps.Int64Ops)))) (IntIkind)
+module IntervalSet = IntervalSetFunctor (IntOps.BigIntOps)
+module Integers (Ints_t : IntOps.IntOps): IkindUnawareS with type t = Ints_t.t and type int_t = Ints_t.t = (* no top/bot, order is <= *)
 struct
   include Printable.Std
   let name () = "integers"
@@ -1764,9 +1764,9 @@ struct
     | `Top | `Bot -> Invariant.none
 end
 
-module Flattened = Flat (Integers(IntOps.Int64Ops))
-module FlattenedBI = Flat (Integers(IntOps.BigIntOps))
-module Lifted    = Lift (Integers(IntOps.Int64Ops))
+module Flattened = Flat (Integers (IntOps.Int64Ops))
+module FlattenedBI = Flat (Integers (IntOps.BigIntOps))
+module Lifted = Lift (Integers (IntOps.Int64Ops))
 
 module Reverse (Base: IkindUnawareS) =
 struct
@@ -1790,7 +1790,7 @@ module BigInt = struct
 end
 
 module BISet = struct
-  include SetDomain.Make(BigInt)
+  include SetDomain.Make (BigInt)
   let is_singleton s = cardinal s = 1
 end
 
@@ -3289,11 +3289,11 @@ module IntDomTupleImpl = struct
 
   open Batteries
   type int_t = Z.t
-  module I1 = SOverflowLifter(DefExc)
+  module I1 = SOverflowLifter (DefExc)
   module I2 = Interval
-  module I3 = SOverflowLifter(Enums)
-  module I4 = SOverflowLifter(Congruence)
-  module I5 = IntervalSetFunctor(IntOps.BigIntOps)
+  module I3 = SOverflowLifter (Enums)
+  module I4 = SOverflowLifter (Congruence)
+  module I5 = IntervalSetFunctor (IntOps.BigIntOps)
 
   type t = I1.t option * I2.t option * I3.t option * I4.t option * I5.t option
   [@@deriving to_yojson, eq, ord]

From 944b531737e89e78b5bfef781af2c2717469a690 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 18:18:48 +0200
Subject: [PATCH 21/52] Include Z instead of IntOps.BigIntOps in BigInt

---
 src/cdomain/value/cdomains/intDomain.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 3ed8a86c59..c55a13a975 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1775,7 +1775,7 @@ struct
 end
 
 module BigInt = struct
-  include IntOps.BigIntOps
+  include Z
   let name () = "BigIntPrintable"
   let top () = raise Unknown
   let bot () = raise Error
@@ -2218,7 +2218,7 @@ struct
 
   let ge ik x y = le ik y x
 
-  let bitnot = lift1 BigInt.bitnot
+  let bitnot = lift1 Z.lognot
 
   let bitand ik x y = norm ik (match x,y with
       (* We don't bother with exclusion sets: *)
@@ -2234,15 +2234,15 @@ struct
       | `Excluded _, `Excluded _ -> top ()
       (* The good case: *)
       | `Definite x, `Definite y ->
-        (try `Definite (BigInt.bitand x y) with | Division_by_zero -> top ())
+        (try `Definite (Z.logand x y) with | Division_by_zero -> top ())
       | `Bot, `Bot -> `Bot
       | _ ->
         (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
         raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
 
 
-  let bitor  = lift2 BigInt.bitor
-  let bitxor = lift2 BigInt.bitxor
+  let bitor  = lift2 Z.logor
+  let bitxor = lift2 Z.logxor
 
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     (* BigInt only accepts int as second argument for shifts; perform conversion here *)
@@ -2416,7 +2416,7 @@ module Enums : S with type int_t = BigInt.t = struct
   let bot_of ik = Inc (BISet.empty ())
   let top_bool = Inc (BISet.of_list [I.zero; I.one])
 
-  let range ik = BatTuple.Tuple2.mapn I.of_bigint (Size.range ik)
+  let range ik = Size.range ik
 
 (*
   let max_of_range r = Size.max_from_bit_range (Option.get (R.maximal r))
@@ -2589,10 +2589,10 @@ module Enums : S with type int_t = BigInt.t = struct
 
   let rem = lift2 I.rem
 
-  let bitnot = lift1 BigInt.bitnot
-  let bitand = lift2 BigInt.bitand
-  let bitor  = lift2 BigInt.bitor
-  let bitxor = lift2 BigInt.bitxor
+  let bitnot = lift1 Z.lognot
+  let bitand = lift2 Z.logand
+  let bitor  = lift2 Z.logor
+  let bitxor = lift2 Z.logxor
 
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     handle_bot x y (fun () ->

From 35d8cd749efbd7cd794195358ef033e0d87ec7a2 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 18:19:51 +0200
Subject: [PATCH 22/52] Define bitnot as Z.lognot in BigIntOpsBase

---
 src/common/util/intOps.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/common/util/intOps.ml b/src/common/util/intOps.ml
index 7c8e5d31e1..24aa4e3f66 100644
--- a/src/common/util/intOps.ml
+++ b/src/common/util/intOps.ml
@@ -241,7 +241,7 @@ struct
 
   let shift_left = Z.shift_left
   let shift_right = Z.shift_right
-  let bitnot x = sub (neg x) one
+  let bitnot = Z.lognot
   let bitand = Z.logand
   let bitor = Z.logor
   let bitxor = Z.logxor

From d929216777885ac1545250b848dd4c7f640768de Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 21:04:36 +0200
Subject: [PATCH 23/52] Revert "Include Z instead of IntOps.BigIntOps in
 BigInt"

This reverts commit 944b531737e89e78b5bfef781af2c2717469a690.
---
 src/cdomain/value/cdomains/intDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index c55a13a975..1ba13da47b 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1775,7 +1775,7 @@ struct
 end
 
 module BigInt = struct
-  include Z
+  include IntOps.BigIntOps
   let name () = "BigIntPrintable"
   let top () = raise Unknown
   let bot () = raise Error

From 4e95cff843ae0315081517beb47b97677670feb6 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 21:11:48 +0200
Subject: [PATCH 24/52] Remove unused FlattenedBI module

---
 src/cdomain/value/cdomains/intDomain.ml  | 1 -
 src/cdomain/value/cdomains/intDomain.mli | 4 ----
 unittest/cdomains/intDomainTest.ml       | 4 +---
 3 files changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 1ba13da47b..34fba4104d 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1765,7 +1765,6 @@ struct
 end
 
 module Flattened = Flat (Integers (IntOps.Int64Ops))
-module FlattenedBI = Flat (Integers (IntOps.BigIntOps))
 module Lifted = Lift (Integers (IntOps.Int64Ops))
 
 module Reverse (Base: IkindUnawareS) =
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index 4b14aeec72..27a766e7aa 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -396,10 +396,6 @@ module Flattened : IkindUnawareS with type t = [`Top | `Lifted of IntOps.Int64Op
 (** This is the typical flattened integer domain used in Kildall's constant
   * propagation. *)
 
-module FlattenedBI : IkindUnawareS with type t = [`Top | `Lifted of IntOps.BigIntOps.t | `Bot] and type int_t = IntOps.BigIntOps.t
-(** This is the typical flattened integer domain used in Kildall's constant
-  * propagation, using Big_int instead of int64. *)
-
 module Lifted : IkindUnawareS with type t = [`Top | `Lifted of int64 | `Bot] and type int_t = int64
 (** Artificially bounded integers in their natural ordering. *)
 
diff --git a/unittest/cdomains/intDomainTest.ml b/unittest/cdomains/intDomainTest.ml
index f803ef1c35..763c3e7e93 100644
--- a/unittest/cdomains/intDomainTest.ml
+++ b/unittest/cdomains/intDomainTest.ml
@@ -110,7 +110,6 @@ end
 
 module Ikind = struct let ikind () = Cil.ILong end
 module A = IntTest (IntDomain.Integers (IntOps.BigIntOps))
-module B = IntTest (IntDomain.FlattenedBI)
 module C = IntTest (IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind))
 module T = struct
   include IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind)
@@ -283,8 +282,7 @@ end
 
 let test () = "intDomainTest" >:::
               [ "int_Integers"  >::: A.test ();
-                "int_Flattened" >::: B.test ();
-                "int_DefExc"     >::: C.test ();
+                "int_DefExc"    >::: C.test ();
                 "test_bot"      >::  test_bot;
                 "test_join"     >::  test_join;
                 "test_meet"     >::  test_meet;

From 89b13d4038a1b39a9ce1d97eb11088afba7ca389 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 21:29:51 +0200
Subject: [PATCH 25/52] Replace BigInt.zero with Z.zero

---
 src/cdomain/value/cdomains/intDomain.ml | 26 ++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 34fba4104d..6f1228237e 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1962,10 +1962,10 @@ struct
         let mapped_excl = S.map (fun excl -> BigInt.cast_to ik excl) s in
         match ik with
         | IBool ->
-          begin match S.mem BigInt.zero mapped_excl, S.mem BigInt.one mapped_excl with
+          begin match S.mem Z.zero mapped_excl, S.mem BigInt.one mapped_excl with
             | false, false -> `Excluded (mapped_excl, r) (* Not {} -> Not {} *)
             | true, false -> `Definite BigInt.one (* Not {0} -> 1 *)
-            | false, true -> `Definite BigInt.zero (* Not {1} -> 0 *)
+            | false, true -> `Definite Z.zero (* Not {1} -> 0 *)
             | true, true -> `Bot (* Not {0, 1} -> bot *)
           end
         | ik ->
@@ -2081,8 +2081,8 @@ struct
 
   let of_interval ?(suppress_ovwarn=false) ik (x,y) = if BigInt.compare x y = 0 then of_int ik x else top_of ik
 
-  let starting ?(suppress_ovwarn=false) ikind x = if BigInt.compare x BigInt.zero > 0 then not_zero ikind else top_of ikind
-  let ending ?(suppress_ovwarn=false) ikind x = if BigInt.compare x BigInt.zero < 0 then not_zero ikind else top_of ikind
+  let starting ?(suppress_ovwarn=false) ikind x = if BigInt.compare x Z.zero > 0 then not_zero ikind else top_of ikind
+  let ending ?(suppress_ovwarn=false) ikind x = if BigInt.compare x Z.zero < 0 then not_zero ikind else top_of ikind
 
   let of_excl_list t l =
     let r = size t in (* elements in l are excluded from the full range of t! *)
@@ -2182,12 +2182,12 @@ struct
 
   let sub ?no_ov ik x y = norm ik @@ lift2_inj BigInt.sub ik x y
   let mul ?no_ov ik x y = norm ik @@ match x, y with
-    | `Definite z, (`Excluded _ | `Definite _) when BigInt.equal z BigInt.zero -> x
-    | (`Excluded _ | `Definite _), `Definite z when BigInt.equal z BigInt.zero -> y
+    | `Definite z, (`Excluded _ | `Definite _) when BigInt.equal z Z.zero -> x
+    | (`Excluded _ | `Definite _), `Definite z when BigInt.equal z Z.zero -> y
     | `Definite a, `Excluded (s,r)
     (* Integer multiplication with even numbers is not injective. *)
     (* Thus we cannot exclude the values to which the exclusion set would be mapped to. *)
-    | `Excluded (s,r),`Definite a when BigInt.equal (BigInt.rem a (BigInt.of_int 2)) BigInt.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
+    | `Excluded (s,r),`Definite a when BigInt.equal (BigInt.rem a (BigInt.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
     | _ -> lift2_inj BigInt.mul ik x y
   let div ?no_ov ik x y = lift2 BigInt.div ik x y
   let rem ik x y = lift2 BigInt.rem ik x y
@@ -2223,10 +2223,10 @@ struct
       (* We don't bother with exclusion sets: *)
       | `Excluded _, `Definite i ->
         (* Except in two special cases *)
-        if BigInt.equal i BigInt.zero then
-          `Definite BigInt.zero
+        if BigInt.equal i Z.zero then
+          `Definite Z.zero
         else if BigInt.equal i BigInt.one then
-          of_interval IBool (BigInt.zero, BigInt.one)
+          of_interval IBool (Z.zero, BigInt.one)
         else
           top ()
       | `Definite _, `Excluded _
@@ -2277,7 +2277,7 @@ struct
       of_bool ik true
     | _, _ ->
       lift2 BigInt.logor ik x y
-  let lognot ik = eq ik (of_int ik BigInt.zero)
+  let lognot ik = eq ik (of_int ik Z.zero)
 
   let invariant_ikind e ik (x:t) =
     match x with
@@ -2456,10 +2456,10 @@ module Enums : S with type int_t = BigInt.t = struct
          assert (range_in_ikind r && BISet.for_all (value_in_range (r_min, r_max)) xs); *)
       begin match ikind with
         | IBool ->
-          begin match BISet.mem BigInt.zero xs, BISet.mem BigInt.one xs with
+          begin match BISet.mem Z.zero xs, BISet.mem BigInt.one xs with
             | false, false -> top_bool  (* Not {} -> {0, 1} *)
             | true, false -> Inc (BISet.singleton BigInt.one) (* Not {0} -> {1} *)
-            | false, true -> Inc (BISet.singleton BigInt.zero) (* Not {1} -> {0} *)
+            | false, true -> Inc (BISet.singleton Z.zero) (* Not {1} -> {0} *)
             | true, true -> bot_of ikind (* Not {0, 1} -> bot *)
           end
         | _ ->

From c2c4d7e15769f1e59784e9a2db0be461ff25fe1c Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 15 Jan 2024 21:35:07 +0200
Subject: [PATCH 26/52] Replace BigInt.one with Z.one

---
 src/cdomain/value/cdomains/intDomain.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 6f1228237e..4eb1f88a97 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1962,9 +1962,9 @@ struct
         let mapped_excl = S.map (fun excl -> BigInt.cast_to ik excl) s in
         match ik with
         | IBool ->
-          begin match S.mem Z.zero mapped_excl, S.mem BigInt.one mapped_excl with
+          begin match S.mem Z.zero mapped_excl, S.mem Z.one mapped_excl with
             | false, false -> `Excluded (mapped_excl, r) (* Not {} -> Not {} *)
-            | true, false -> `Definite BigInt.one (* Not {0} -> 1 *)
+            | true, false -> `Definite Z.one (* Not {0} -> 1 *)
             | false, true -> `Definite Z.zero (* Not {1} -> 0 *)
             | true, true -> `Bot (* Not {0, 1} -> bot *)
           end
@@ -2225,8 +2225,8 @@ struct
         (* Except in two special cases *)
         if BigInt.equal i Z.zero then
           `Definite Z.zero
-        else if BigInt.equal i BigInt.one then
-          of_interval IBool (Z.zero, BigInt.one)
+        else if BigInt.equal i Z.one then
+          of_interval IBool (Z.zero, Z.one)
         else
           top ()
       | `Definite _, `Excluded _
@@ -2456,9 +2456,9 @@ module Enums : S with type int_t = BigInt.t = struct
          assert (range_in_ikind r && BISet.for_all (value_in_range (r_min, r_max)) xs); *)
       begin match ikind with
         | IBool ->
-          begin match BISet.mem Z.zero xs, BISet.mem BigInt.one xs with
+          begin match BISet.mem Z.zero xs, BISet.mem Z.one xs with
             | false, false -> top_bool  (* Not {} -> {0, 1} *)
-            | true, false -> Inc (BISet.singleton BigInt.one) (* Not {0} -> {1} *)
+            | true, false -> Inc (BISet.singleton Z.one) (* Not {0} -> {1} *)
             | false, true -> Inc (BISet.singleton Z.zero) (* Not {1} -> {0} *)
             | true, true -> bot_of ikind (* Not {0, 1} -> bot *)
           end

From 57d9201cf5cccbf22a1eece793c8acd8f9bee7fc Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:18:40 +0200
Subject: [PATCH 27/52] Replace BigInt.equal with Z.equal

---
 src/cdomain/value/cdomains/intDomain.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 4eb1f88a97..a8aade6b19 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2182,12 +2182,12 @@ struct
 
   let sub ?no_ov ik x y = norm ik @@ lift2_inj BigInt.sub ik x y
   let mul ?no_ov ik x y = norm ik @@ match x, y with
-    | `Definite z, (`Excluded _ | `Definite _) when BigInt.equal z Z.zero -> x
-    | (`Excluded _ | `Definite _), `Definite z when BigInt.equal z Z.zero -> y
+    | `Definite z, (`Excluded _ | `Definite _) when Z.equal z Z.zero -> x
+    | (`Excluded _ | `Definite _), `Definite z when Z.equal z Z.zero -> y
     | `Definite a, `Excluded (s,r)
     (* Integer multiplication with even numbers is not injective. *)
     (* Thus we cannot exclude the values to which the exclusion set would be mapped to. *)
-    | `Excluded (s,r),`Definite a when BigInt.equal (BigInt.rem a (BigInt.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
+    | `Excluded (s,r),`Definite a when Z.equal (BigInt.rem a (BigInt.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
     | _ -> lift2_inj BigInt.mul ik x y
   let div ?no_ov ik x y = lift2 BigInt.div ik x y
   let rem ik x y = lift2 BigInt.rem ik x y
@@ -2223,9 +2223,9 @@ struct
       (* We don't bother with exclusion sets: *)
       | `Excluded _, `Definite i ->
         (* Except in two special cases *)
-        if BigInt.equal i Z.zero then
+        if Z.equal i Z.zero then
           `Definite Z.zero
-        else if BigInt.equal i Z.one then
+        else if Z.equal i Z.one then
           of_interval IBool (Z.zero, Z.one)
         else
           top ()

From 12045ea3d1e9c4a023c9f9b042ee9d4d2740ff68 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:19:32 +0200
Subject: [PATCH 28/52] Replace BigInt.add with Z.add

---
 src/cdomain/value/cdomains/intDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index a8aade6b19..35743546f8 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2178,7 +2178,7 @@ struct
       raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
 
   let neg ?no_ov ik (x :t) = norm ik @@ lift1 BigInt.neg ik x
-  let add ?no_ov ik x y = norm ik @@ lift2_inj BigInt.add ik x y
+  let add ?no_ov ik x y = norm ik @@ lift2_inj Z.add ik x y
 
   let sub ?no_ov ik x y = norm ik @@ lift2_inj BigInt.sub ik x y
   let mul ?no_ov ik x y = norm ik @@ match x, y with

From ace1963a7ccd13b9b174719af9ea239475bfe7be Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:20:08 +0200
Subject: [PATCH 29/52] Replace BigInt.sub with Z.sub

---
 src/cdomain/value/cdomains/intDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 35743546f8..0dc2c0f114 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2180,7 +2180,7 @@ struct
   let neg ?no_ov ik (x :t) = norm ik @@ lift1 BigInt.neg ik x
   let add ?no_ov ik x y = norm ik @@ lift2_inj Z.add ik x y
 
-  let sub ?no_ov ik x y = norm ik @@ lift2_inj BigInt.sub ik x y
+  let sub ?no_ov ik x y = norm ik @@ lift2_inj Z.sub ik x y
   let mul ?no_ov ik x y = norm ik @@ match x, y with
     | `Definite z, (`Excluded _ | `Definite _) when Z.equal z Z.zero -> x
     | (`Excluded _ | `Definite _), `Definite z when Z.equal z Z.zero -> y

From b8c9b4b86a34ca9a11a30fd23b1f2382870b48ed Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:20:43 +0200
Subject: [PATCH 30/52] Replace BigInt.neg with Z.neg

---
 src/cdomain/value/cdomains/intDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 0dc2c0f114..c1de32ff18 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2177,7 +2177,7 @@ struct
       (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
       raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
 
-  let neg ?no_ov ik (x :t) = norm ik @@ lift1 BigInt.neg ik x
+  let neg ?no_ov ik (x :t) = norm ik @@ lift1 Z.neg ik x
   let add ?no_ov ik x y = norm ik @@ lift2_inj Z.add ik x y
 
   let sub ?no_ov ik x y = norm ik @@ lift2_inj Z.sub ik x y

From dfe104fd3400278eb5b3f18650b3a309f681f1a2 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:21:33 +0200
Subject: [PATCH 31/52] Replace BigInt.of_int with Z.of_int

---
 src/cdomain/value/cdomains/intDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index c1de32ff18..66e57c2417 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2187,7 +2187,7 @@ struct
     | `Definite a, `Excluded (s,r)
     (* Integer multiplication with even numbers is not injective. *)
     (* Thus we cannot exclude the values to which the exclusion set would be mapped to. *)
-    | `Excluded (s,r),`Definite a when Z.equal (BigInt.rem a (BigInt.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
+    | `Excluded (s,r),`Definite a when Z.equal (BigInt.rem a (Z.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
     | _ -> lift2_inj BigInt.mul ik x y
   let div ?no_ov ik x y = lift2 BigInt.div ik x y
   let rem ik x y = lift2 BigInt.rem ik x y

From 8b181cf77f30e77993ea13af6f249a1c0b997de8 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:22:07 +0200
Subject: [PATCH 32/52] Replace BigInt.rem with Z.rem

---
 src/cdomain/value/cdomains/intDomain.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 66e57c2417..d0fa91b1fc 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2187,10 +2187,10 @@ struct
     | `Definite a, `Excluded (s,r)
     (* Integer multiplication with even numbers is not injective. *)
     (* Thus we cannot exclude the values to which the exclusion set would be mapped to. *)
-    | `Excluded (s,r),`Definite a when Z.equal (BigInt.rem a (Z.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
+    | `Excluded (s,r),`Definite a when Z.equal (Z.rem a (Z.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
     | _ -> lift2_inj BigInt.mul ik x y
   let div ?no_ov ik x y = lift2 BigInt.div ik x y
-  let rem ik x y = lift2 BigInt.rem ik x y
+  let rem ik x y = lift2 Z.rem ik x y
 
   (* Comparison handling copied from Enums. *)
   let handle_bot x y f = match x, y with

From 1d18891dd0d737794cc40a728e11e3db7e27847d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:25:59 +0200
Subject: [PATCH 33/52] Replace BigInt.compare with Z.compare

---
 src/cdomain/value/cdomains/intDomain.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index d0fa91b1fc..338f4508e8 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1977,7 +1977,7 @@ struct
       if should_wrap ik then (
         cast_to ik v
       )
-      else if BigInt.compare min x <= 0 && BigInt.compare x max <= 0 then (
+      else if Z.compare min x <= 0 && Z.compare x max <= 0 then (
         v
       )
       else if should_ignore_overflow ik then (
@@ -2079,10 +2079,10 @@ struct
     | _ -> None
   let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L))
 
-  let of_interval ?(suppress_ovwarn=false) ik (x,y) = if BigInt.compare x y = 0 then of_int ik x else top_of ik
+  let of_interval ?(suppress_ovwarn=false) ik (x,y) = if Z.compare x y = 0 then of_int ik x else top_of ik
 
-  let starting ?(suppress_ovwarn=false) ikind x = if BigInt.compare x Z.zero > 0 then not_zero ikind else top_of ikind
-  let ending ?(suppress_ovwarn=false) ikind x = if BigInt.compare x Z.zero < 0 then not_zero ikind else top_of ikind
+  let starting ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero > 0 then not_zero ikind else top_of ikind
+  let ending ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero < 0 then not_zero ikind else top_of ikind
 
   let of_excl_list t l =
     let r = size t in (* elements in l are excluded from the full range of t! *)
@@ -2187,9 +2187,9 @@ struct
     | `Definite a, `Excluded (s,r)
     (* Integer multiplication with even numbers is not injective. *)
     (* Thus we cannot exclude the values to which the exclusion set would be mapped to. *)
-    | `Excluded (s,r),`Definite a when Z.equal (Z.rem a (Z.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (BigInt.mul a) r)
-    | _ -> lift2_inj BigInt.mul ik x y
-  let div ?no_ov ik x y = lift2 BigInt.div ik x y
+    | `Excluded (s,r),`Definite a when Z.equal (Z.rem a (Z.of_int 2)) Z.zero -> `Excluded (S.empty (), apply_range (Z.mul a) r)
+    | _ -> lift2_inj Z.mul ik x y
+  let div ?no_ov ik x y = lift2 Z.div ik x y
   let rem ik x y = lift2 Z.rem ik x y
 
   (* Comparison handling copied from Enums. *)
@@ -2202,8 +2202,8 @@ struct
   let lt ik x y =
     handle_bot x y (fun () ->
         match minimal x, maximal x, minimal y, maximal y with
-        | _, Some x2, Some y1, _ when BigInt.compare x2 y1 < 0 -> of_bool ik true
-        | Some x1, _, _, Some y2 when BigInt.compare x1 y2 >= 0 -> of_bool ik false
+        | _, Some x2, Some y1, _ when Z.compare x2 y1 < 0 -> of_bool ik true
+        | Some x1, _, _, Some y2 when Z.compare x1 y2 >= 0 -> of_bool ik false
         | _, _, _, _ -> top_bool)
 
   let gt ik x y = lt ik y x
@@ -2211,8 +2211,8 @@ struct
   let le ik x y =
     handle_bot x y (fun () ->
         match minimal x, maximal x, minimal y, maximal y with
-        | _, Some x2, Some y1, _ when BigInt.compare x2 y1 <= 0 -> of_bool ik true
-        | Some x1, _, _, Some y2 when BigInt.compare x1 y2 > 0 -> of_bool ik false
+        | _, Some x2, Some y1, _ when Z.compare x2 y1 <= 0 -> of_bool ik true
+        | Some x1, _, _, Some y2 when Z.compare x1 y2 > 0 -> of_bool ik false
         | _, _, _, _ -> top_bool)
 
   let ge ik x y = le ik y x

From 1b1320781df33e9655fb3c91f19fa54dec76a202 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:26:30 +0200
Subject: [PATCH 34/52] Replace BigInt.shift_left with Z.shift_left

---
 src/cdomain/value/cdomains/intDomain.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 338f4508e8..8082195dee 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2258,7 +2258,7 @@ struct
       norm ik @@ lift2 shift_op_big_int ik x y
 
   let shift_left =
-    shift BigInt.shift_left
+    shift Z.shift_left
 
   let shift_right =
     shift BigInt.shift_right
@@ -2609,7 +2609,7 @@ module Enums : S with type int_t = BigInt.t = struct
           lift2 shift_op_big_int ik x y)
 
   let shift_left =
-    shift BigInt.shift_left
+    shift Z.shift_left
 
   let shift_right =
     shift BigInt.shift_right

From b5e883b74a6b7ecfd5562ae838a76f7c0cb7b18a Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:26:55 +0200
Subject: [PATCH 35/52] Replace BigInt.shift_right with Z.shift_right

---
 tests/regression/40-threadid/12-threads.c | 50 +++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 tests/regression/40-threadid/12-threads.c

diff --git a/tests/regression/40-threadid/12-threads.c b/tests/regression/40-threadid/12-threads.c
new file mode 100644
index 0000000000..636d0da50d
--- /dev/null
+++ b/tests/regression/40-threadid/12-threads.c
@@ -0,0 +1,50 @@
+
+#include <goblint.h>
+#include <pthread.h>
+
+/* Slab sizing definitions. */
+#define POWER_SMALLEST 1
+#define POWER_LARGEST 16 /* actual cap is 255 */
+#define LARGEST_ID POWER_LARGEST
+/* Locks for cache LRU operations */
+pthread_mutex_t lru_locks[POWER_LARGEST];
+static pthread_t item_crawler_tid;
+
+int myglobal;
+
+void memcached_thread_init(int nthreads, void *arg) {
+    int i;
+    for (i = 0; i < POWER_LARGEST; i++) {
+        pthread_mutex_init(&lru_locks[i], NULL);
+    }
+}
+
+void *item_crawler_thread(void *arg) {
+    int i, r1, r2;
+    for (i = POWER_SMALLEST; i < LARGEST_ID; i++) {
+        pthread_mutex_lock(&lru_locks[i]);
+        myglobal = myglobal + 1; // RACE!
+        if (r1) {
+            pthread_mutex_unlock(&lru_locks[i]);
+            continue;
+        }
+        // if (r2) {
+        //     int x = 0;
+        // }
+    }
+    return NULL;
+}
+
+int main(void) {
+    int i;
+    int num_threads = rand();
+    memcached_thread_init(num_threads, NULL);
+    pthread_create(&item_crawler_tid, NULL, item_crawler_thread, NULL);
+    for (i = POWER_SMALLEST; i < LARGEST_ID; i++) {
+        pthread_mutex_lock(&lru_locks[i]);
+        myglobal = myglobal + 1; // RACE!
+        pthread_mutex_unlock(&lru_locks[i]);
+    }
+    pthread_join(&item_crawler_tid, NULL);
+    return 0;
+}
\ No newline at end of file

From 68dc1891ef9d39fe1cf5298f7267ae8b3185315b Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:29:57 +0200
Subject: [PATCH 36/52] Replace BigInt.shift_right with Z.shift_right

---
 src/cdomain/value/cdomains/intDomain.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 8082195dee..43d301e9fa 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2261,7 +2261,7 @@ struct
     shift Z.shift_left
 
   let shift_right =
-    shift BigInt.shift_right
+    shift Z.shift_right
   (* TODO: lift does not treat Not {0} as true. *)
   let logand ik x y =
     match to_bool x, to_bool y with
@@ -2612,7 +2612,7 @@ module Enums : S with type int_t = BigInt.t = struct
     shift Z.shift_left
 
   let shift_right =
-    shift BigInt.shift_right
+    shift Z.shift_right
 
   let of_bool ikind x = Inc (BISet.singleton (if x then Z.one else Z.zero))
   let to_bool  = function

From 70871ef3401bc8d5317b23d1edbcd2105eaf1670 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 00:30:51 +0200
Subject: [PATCH 37/52] Revert "Replace BigInt.shift_right with Z.shift_right"

This reverts commit b5e883b74a6b7ecfd5562ae838a76f7c0cb7b18a.
---
 tests/regression/40-threadid/12-threads.c | 50 -----------------------
 1 file changed, 50 deletions(-)
 delete mode 100644 tests/regression/40-threadid/12-threads.c

diff --git a/tests/regression/40-threadid/12-threads.c b/tests/regression/40-threadid/12-threads.c
deleted file mode 100644
index 636d0da50d..0000000000
--- a/tests/regression/40-threadid/12-threads.c
+++ /dev/null
@@ -1,50 +0,0 @@
-
-#include <goblint.h>
-#include <pthread.h>
-
-/* Slab sizing definitions. */
-#define POWER_SMALLEST 1
-#define POWER_LARGEST 16 /* actual cap is 255 */
-#define LARGEST_ID POWER_LARGEST
-/* Locks for cache LRU operations */
-pthread_mutex_t lru_locks[POWER_LARGEST];
-static pthread_t item_crawler_tid;
-
-int myglobal;
-
-void memcached_thread_init(int nthreads, void *arg) {
-    int i;
-    for (i = 0; i < POWER_LARGEST; i++) {
-        pthread_mutex_init(&lru_locks[i], NULL);
-    }
-}
-
-void *item_crawler_thread(void *arg) {
-    int i, r1, r2;
-    for (i = POWER_SMALLEST; i < LARGEST_ID; i++) {
-        pthread_mutex_lock(&lru_locks[i]);
-        myglobal = myglobal + 1; // RACE!
-        if (r1) {
-            pthread_mutex_unlock(&lru_locks[i]);
-            continue;
-        }
-        // if (r2) {
-        //     int x = 0;
-        // }
-    }
-    return NULL;
-}
-
-int main(void) {
-    int i;
-    int num_threads = rand();
-    memcached_thread_init(num_threads, NULL);
-    pthread_create(&item_crawler_tid, NULL, item_crawler_thread, NULL);
-    for (i = POWER_SMALLEST; i < LARGEST_ID; i++) {
-        pthread_mutex_lock(&lru_locks[i]);
-        myglobal = myglobal + 1; // RACE!
-        pthread_mutex_unlock(&lru_locks[i]);
-    }
-    pthread_join(&item_crawler_tid, NULL);
-    return 0;
-}
\ No newline at end of file

From aad0a09b051f446313e07106e29764150e7ab526 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 12:34:57 +0200
Subject: [PATCH 38/52] Replace IntOps.BigIntOps with Z where possible in
 intDomain.mli

---
 src/cdomain/value/cdomains/intDomain.mli | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index 27a766e7aa..cc43c32ace 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -335,7 +335,7 @@ sig
 end
 (** The signature of integral value domains keeping track of ikind information *)
 
-module type Z = Y with type int_t = IntOps.BigIntOps.t
+module type Z = Y with type int_t = Z.t
 
 module IntDomLifter (I: S): Y with type int_t = I.int_t
 
@@ -407,17 +407,17 @@ module Interval32 :Y with (* type t = (IntOps.Int64Ops.t * IntOps.Int64Ops.t) op
 
 module BigInt:
   sig
-    include Printable.S with type t = Z.t (* TODO: why doesn't this have a more useful signature like IntOps.BigIntOps? *)
+    include Printable.S with type t = Z.t
     val cast_to: Cil.ikind -> Z.t -> Z.t
   end
 
-module Interval : SOverflow with type int_t = IntOps.BigIntOps.t
+module Interval : SOverflow with type int_t = Z.t
 
-module IntervalSet : SOverflow with type int_t = IntOps.BigIntOps.t
+module IntervalSet : SOverflow with type int_t = Z.t
 
-module Congruence : S with type int_t = IntOps.BigIntOps.t
+module Congruence : S with type int_t = Z.t
 
-module DefExc : S with type int_t = IntOps.BigIntOps.t
+module DefExc : S with type int_t = Z.t
 (** The DefExc domain. The Flattened integer domain is topped by exclusion sets.
   * Good for analysing branches. *)
 
@@ -440,7 +440,7 @@ module Reverse (Base: IkindUnawareS): IkindUnawareS with type t = Base.t and typ
 
 (* module IncExcInterval : S with type t = [ | `Excluded of Interval.t| `Included of Interval.t ] *)
 (** Inclusive and exclusive intervals. Warning: NOT A LATTICE *)
-module Enums : S with type int_t = IntOps.BigIntOps.t
+module Enums : S with type int_t = Z.t
 
 (** {b Boolean domains} *)
 

From 444290d9dd099444d3c93970aebd9bedbce8c1e6 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 16 Jan 2024 16:05:17 +0200
Subject: [PATCH 39/52] Simplify BigInt and replace with Z where possible

---
 src/cdomain/value/cdomains/intDomain.ml | 61 ++++++++++++-------------
 1 file changed, 28 insertions(+), 33 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 43d301e9fa..873aebb8a9 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1781,11 +1781,9 @@ module BigInt = struct
   let top_of ik = top ()
   let bot_of ik = bot ()
   let cast_to ik x = Size.cast ik x
-  let to_bool x = Some (not (Z.equal Z.zero x))
-
   let show x = Z.to_string x
-  include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
-  let arbitrary () = QCheck.map ~rev:to_int64 of_int64 QCheck.int64
+  include Std (struct type nonrec t = Z.t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
+  let arbitrary () = QCheck.map ~rev:Z.to_int64 Z.of_int64 QCheck.int64
 end
 
 module BISet = struct
@@ -1847,7 +1845,7 @@ struct
     end
 end
 
-module DefExc : S with type int_t = BigInt.t = (* definite or set of excluded values *)
+module DefExc : S with type int_t = Z.t = (* definite or set of excluded values *)
 struct
   module S = BISet
   module R = Interval32 (* range for exclusion *)
@@ -1859,10 +1857,10 @@ struct
 
   type t = [
     | `Excluded of S.t * R.t
-    | `Definite of BigInt.t
+    | `Definite of Z.t
     | `Bot
   ] [@@deriving eq, ord, hash]
-  type int_t = BigInt.t
+  type int_t = Z.t
   let name () = "def_exc"
 
 
@@ -1872,13 +1870,11 @@ struct
   let top_of ik = `Excluded (S.empty (), size ik)
   let bot_of ik = bot ()
 
-
-
   let show x =
     let short_size x = "("^R.show x^")" in
     match x with
     | `Bot -> "Error int"
-    | `Definite x -> BigInt.show x
+    | `Definite x -> Z.to_string x
     (* Print the empty exclusion as if it was a distinct top element: *)
     | `Excluded (s,l) when S.is_empty s -> "Unknown int" ^ short_size l
     (* Prepend the exclusion sets with something: *)
@@ -2074,7 +2070,7 @@ struct
   let of_bool = of_bool_cmp
   let to_bool x =
     match x with
-    | `Definite x -> BigInt.to_bool x
+    | `Definite x -> Some (BigInt.to_bool x)
     | `Excluded (s,r) when S.mem Z.zero s -> Some true
     | _ -> None
   let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L))
@@ -2397,9 +2393,8 @@ module Booleans = MakeBooleans (
   end)
 
 (* Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions. *)
-module Enums : S with type int_t = BigInt.t = struct
+module Enums : S with type int_t = Z.t = struct
   open Batteries
-  module I = BigInt
   module R = Interval32 (* range for exclusion *)
 
   let range_ikind = Cil.IInt
@@ -2413,20 +2408,20 @@ module Enums : S with type int_t = BigInt.t = struct
   let top_of ik = Exc (BISet.empty (), size ik)
   let top () = failwith "top () not implemented for Enums"
   let bot_of ik = Inc (BISet.empty ())
-  let top_bool = Inc (BISet.of_list [I.zero; I.one])
+  let top_bool = Inc (BISet.of_list [Z.zero; Z.one])
 
   let range ik = Size.range ik
 
 (*
   let max_of_range r = Size.max_from_bit_range (Option.get (R.maximal r))
   let min_of_range r = Size.min_from_bit_range (Option.get (R.minimal r))
-  let cardinality_of_range r = I.add (I.neg (min_of_range r)) (max_of_range r) *)
-  let value_in_range (min, max) v = I.compare min v <= 0 && I.compare v max <= 0
+  let cardinality_of_range r = Z.add (Z.neg (min_of_range r)) (max_of_range r) *)
+  let value_in_range (min, max) v = Z.compare min v <= 0 && Z.compare v max <= 0
 
   let show = function
     | Inc xs when BISet.is_empty xs -> "bot"
-    | Inc xs -> "{" ^ (String.concat ", " (List.map I.show (BISet.elements  xs))) ^ "}"
-    | Exc (xs,r) -> "not {" ^ (String.concat ", " (List.map I.show (BISet.elements xs))) ^ "} " ^ "("^R.show r^")"
+    | Inc xs -> "{" ^ (String.concat ", " (List.map Z.to_string (BISet.elements  xs))) ^ "}"
+    | Exc (xs,r) -> "not {" ^ (String.concat ", " (List.map Z.to_string (BISet.elements xs))) ^ "} " ^ "("^R.show r^")"
 
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
 
@@ -2436,7 +2431,7 @@ module Enums : S with type int_t = BigInt.t = struct
     let min, max = range ikind in
     (* Whether the value v lies within the values of the specified ikind. *)
     let value_in_ikind v =
-      I.compare min v <= 0 && I.compare v max <= 0
+      Z.compare min v <= 0 && Z.compare v max <= 0
     in
     match v with
     | Inc xs when BISet.for_all value_in_ikind xs -> v
@@ -2536,7 +2531,7 @@ module Enums : S with type int_t = BigInt.t = struct
         let min_b, max_b = Exclusion.min_of_range r, Exclusion.max_of_range r in
         let min_a, max_a = BISet.min_elt xs, BISet.max_elt xs in
         (* Check that the xs fit into the range r  *)
-        I.compare min_b min_a <= 0 && I.compare max_a max_b <= 0 &&
+        Z.compare min_b min_a <= 0 && Z.compare max_a max_b <= 0 &&
         (* && check that none of the values contained in xs is excluded, i.e. contained in ys. *)
         BISet.for_all (fun x -> not (BISet.mem x ys)) xs
     | Inc xs, Inc ys ->
@@ -2566,27 +2561,27 @@ module Enums : S with type int_t = BigInt.t = struct
   let lift2 f ikind a b =
     try lift2 f ikind a b with Division_by_zero -> top_of ikind
 
-  let neg ?no_ov = lift1 I.neg
+  let neg ?no_ov = lift1 Z.neg
   let add ?no_ov ikind = curry @@ function
     | Inc z,x when BISet.is_singleton z && BISet.choose z = Z.zero -> x
     | x,Inc z when BISet.is_singleton z && BISet.choose z = Z.zero -> x
-    | x,y -> lift2 I.add ikind x y
-  let sub ?no_ov = lift2 I.sub
+    | x,y -> lift2 Z.add ikind x y
+  let sub ?no_ov = lift2 Z.sub
   let mul ?no_ov ikind a b =
     match a, b with
     | Inc one,x when BISet.is_singleton one && BISet.choose one = Z.one -> x
     | x,Inc one when BISet.is_singleton one && BISet.choose one = Z.one -> x
     | Inc zero,_ when BISet.is_singleton zero && BISet.choose zero = Z.zero -> a
     | _,Inc zero when BISet.is_singleton zero && BISet.choose zero = Z.zero -> b
-    | x,y -> lift2 I.mul ikind x y
+    | x,y -> lift2 Z.mul ikind x y
 
   let div ?no_ov ikind a b = match a, b with
     | x,Inc one when BISet.is_singleton one && BISet.choose one = Z.one -> x
     | _,Inc zero when BISet.is_singleton zero && BISet.choose zero = Z.zero -> top_of ikind
     | Inc zero,_ when BISet.is_singleton zero && BISet.choose zero = Z.zero -> a
-    | x,y -> lift2 I.div ikind x y
+    | x,y -> lift2 Z.div ikind x y
 
-  let rem = lift2 I.rem
+  let rem = lift2 Z.rem
 
   let bitnot = lift1 Z.lognot
   let bitand = lift2 Z.logand
@@ -2643,8 +2638,8 @@ module Enums : S with type int_t = BigInt.t = struct
       | Some b -> of_bool ik (not b)
       | None -> top_bool
 
-  let logand = lift2 I.logand
-  let logor  = lift2 I.logor
+  let logand = lift2 BigInt.logand
+  let logor  = lift2 BigInt.logor
   let maximal = function
     | Inc xs when not (BISet.is_empty xs) -> Some (BISet.max_elt xs)
     | Exc (excl,r) ->
@@ -2672,8 +2667,8 @@ module Enums : S with type int_t = BigInt.t = struct
   let lt ik x y =
     handle_bot x y (fun () ->
         match minimal x, maximal x, minimal y, maximal y with
-        | _, Some x2, Some y1, _ when I.compare x2 y1 < 0 -> of_bool ik true
-        | Some x1, _, _, Some y2 when I.compare x1 y2 >= 0 -> of_bool ik false
+        | _, Some x2, Some y1, _ when Z.compare x2 y1 < 0 -> of_bool ik true
+        | Some x1, _, _, Some y2 when Z.compare x1 y2 >= 0 -> of_bool ik false
         | _, _, _, _ -> top_bool)
 
   let gt ik x y = lt ik y x
@@ -2681,8 +2676,8 @@ module Enums : S with type int_t = BigInt.t = struct
   let le ik x y =
     handle_bot x y (fun () ->
         match minimal x, maximal x, minimal y, maximal y with
-        | _, Some x2, Some y1, _ when I.compare x2 y1 <= 0 -> of_bool ik true
-        | Some x1, _, _, Some y2 when I.compare x1 y2 > 0 -> of_bool ik false
+        | _, Some x2, Some y1, _ when Z.compare x2 y1 <= 0 -> of_bool ik true
+        | Some x1, _, _, Some y2 when Z.compare x1 y2 > 0 -> of_bool ik false
         | _, _, _, _ -> top_bool)
 
   let ge ik x y = le ik y x
@@ -2690,7 +2685,7 @@ module Enums : S with type int_t = BigInt.t = struct
   let eq ik x y =
     handle_bot x y (fun () ->
         match x, y with
-        | Inc xs, Inc ys when BISet.is_singleton xs && BISet.is_singleton ys -> of_bool ik (I.equal (BISet.choose xs) (BISet.choose ys))
+        | Inc xs, Inc ys when BISet.is_singleton xs && BISet.is_singleton ys -> of_bool ik (Z.equal (BISet.choose xs) (BISet.choose ys))
         | _, _ ->
           if is_bot (meet ik x y) then
             (* If the meet is empty, there is no chance that concrete values are equal *)

From f8ea135e0074ab507166a6ffd4164deddbf9dfdc Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 22 Jan 2024 15:16:28 +0200
Subject: [PATCH 40/52] Inline Z.pred and Z.succ

---
 src/analyses/baseInvariant.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 366615a1b5..f6cd11afa9 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -380,8 +380,6 @@ struct
           | _, _ -> a, b
         end
       | Lt | Le | Ge | Gt as op ->
-        let pred x = Z.pred x in
-        let succ x = Z.succ x in
         (match ID.minimal a, ID.maximal a, ID.minimal b, ID.maximal b with
          | Some l1, Some u1, Some l2, Some u2 ->
            (* if M.tracing then M.tracel "inv" "Op: %s, l1: %Ld, u1: %Ld, l2: %Ld, u2: %Ld\n" (show_binop op) l1 u1 l2 u2; *)
@@ -395,9 +393,9 @@ struct
             | Ge, Some true
             | Lt, Some false -> meet_bin (ID.starting ikind l2) (ID.ending ikind u1)
             | Lt, Some true
-            | Ge, Some false -> meet_bin (ID.ending ikind (pred u2)) (ID.starting ikind (succ l1))
+            | Ge, Some false -> meet_bin (ID.ending ikind (Z.pred u2)) (ID.starting ikind (Z.succ l1))
             | Gt, Some true
-            | Le, Some false -> meet_bin (ID.starting ikind (succ l2)) (ID.ending ikind (pred u1))
+            | Le, Some false -> meet_bin (ID.starting ikind (Z.succ l2)) (ID.ending ikind (Z.pred u1))
             | _, _ -> a, b)
          | _ -> a, b)
       | BOr | BXor as op->

From 7f80113b2adc89dc9aaeda3f6583879f7b8f5bb2 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 22 Jan 2024 15:20:14 +0200
Subject: [PATCH 41/52] Revert part of "Remove unused FlattenedBI module": keep
 the test

This reverts part of the commit 4e95cff843ae0315081517beb47b97677670feb6.
---
 unittest/cdomains/intDomainTest.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/unittest/cdomains/intDomainTest.ml b/unittest/cdomains/intDomainTest.ml
index 763c3e7e93..7caf98a861 100644
--- a/unittest/cdomains/intDomainTest.ml
+++ b/unittest/cdomains/intDomainTest.ml
@@ -110,6 +110,7 @@ end
 
 module Ikind = struct let ikind () = Cil.ILong end
 module A = IntTest (IntDomain.Integers (IntOps.BigIntOps))
+module B = IntTest (IntDomain.Flat (IntDomain.Integers (IntOps.BigIntOps)))
 module C = IntTest (IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind))
 module T = struct
   include IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind)
@@ -282,7 +283,8 @@ end
 
 let test () = "intDomainTest" >:::
               [ "int_Integers"  >::: A.test ();
-                "int_DefExc"    >::: C.test ();
+                "int_Flattened" >::: B.test ();
+                "int_DefExc"     >::: C.test ();
                 "test_bot"      >::  test_bot;
                 "test_join"     >::  test_join;
                 "test_meet"     >::  test_meet;

From 5c773ed06e6f6d3b354d32132c71b59aba084010 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 22 Jan 2024 16:27:06 +0200
Subject: [PATCH 42/52] Remove unused functions from BigInt

---
 src/cdomain/value/cdomains/intDomain.ml  | 27 ++++++++++++------------
 src/cdomain/value/cdomains/intDomain.mli |  2 +-
 src/domains/intDomainProperties.ml       |  2 +-
 3 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 873aebb8a9..085d0f584a 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1774,15 +1774,16 @@ struct
 end
 
 module BigInt = struct
+  include Printable.StdLeaf
   include IntOps.BigIntOps
   let name () = "BigIntPrintable"
-  let top () = raise Unknown
-  let bot () = raise Error
-  let top_of ik = top ()
-  let bot_of ik = bot ()
-  let cast_to ik x = Size.cast ik x
   let show x = Z.to_string x
-  include Std (struct type nonrec t = Z.t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
+  include Printable.SimpleShow (
+    struct
+      type nonrec t = t
+      let show = show
+    end
+    )
   let arbitrary () = QCheck.map ~rev:Z.to_int64 Z.of_int64 QCheck.int64
 end
 
@@ -1920,13 +1921,13 @@ struct
             `Excluded (S.empty(), r')
         else
           (* downcast: may overflow *)
-          (* let s' = S.map (BigInt.cast_to ik) s in *)
+          (* let s' = S.map (Size.cast ik) s in *)
           (* We want to filter out all i in s' where (t)x with x in r could be i. *)
           (* Since this is hard to compute, we just keep all i in s' which overflowed, since those are safe - all i which did not overflow may now be possible due to overflow of r. *)
           (* S.diff s' s, r' *)
           (* The above is needed for test 21/03, but not sound! See example https://github.com/goblint/analyzer/pull/95#discussion_r483023140 *)
           `Excluded (S.empty (), r')
-    | `Definite x -> `Definite (BigInt.cast_to ik x)
+    | `Definite x -> `Definite (Size.cast ik x)
     | `Bot -> `Bot
 
   (* Wraps definite values and excluded values according to the ikind.
@@ -1955,7 +1956,7 @@ struct
         (* Else an overflow occurred that we should treat with wrap-around *)
         let r = size ik in
         (* Perform a wrap-around for unsigned values and for signed values (if configured). *)
-        let mapped_excl = S.map (fun excl -> BigInt.cast_to ik excl) s in
+        let mapped_excl = S.map (fun excl -> Size.cast ik excl) s in
         match ik with
         | IBool ->
           begin match S.mem Z.zero mapped_excl, S.mem Z.one mapped_excl with
@@ -2437,7 +2438,7 @@ module Enums : S with type int_t = Z.t = struct
     | Inc xs when BISet.for_all value_in_ikind xs -> v
     | Inc xs ->
       if should_wrap ikind then
-        Inc (BISet.map (BigInt.cast_to ikind) xs)
+        Inc (BISet.map (Size.cast ikind) xs)
       else if should_ignore_overflow ikind then
         Inc (BISet.filter value_in_ikind xs)
       else
@@ -2485,7 +2486,7 @@ module Enums : S with type int_t = Z.t = struct
       else (* downcast: may overflow *)
         Exc ((BISet.empty ()), r')
     | Inc xs ->
-      let casted_xs = BISet.map (BigInt.cast_to ik) xs in
+      let casted_xs = BISet.map (Size.cast ik) xs in
       if Cil.isSigned ik && not (BISet.equal xs casted_xs)
       then top_of ik (* When casting into a signed type and the result does not fit, the behavior is implementation-defined *)
       else Inc casted_xs
@@ -2775,7 +2776,7 @@ struct
     | Some (c, m) ->
       if m =: Z.zero then
         if should_wrap ik then
-          Some (BigInt.cast_to ik c, m)
+          Some (Size.cast ik c, m)
         else
           Some (c, m)
       else
@@ -2897,7 +2898,7 @@ struct
     match x with
     | None -> None
     | Some (c, m) when m =: Z.zero ->
-      let c' = BigInt.cast_to t c in
+      let c' = Size.cast t c in
       (* When casting into a signed type and the result does not fit, the behavior is implementation-defined. (C90 6.2.1.2, C99 and C11 6.3.1.3) *)
       (* We go with GCC behavior here: *)
       (*  For conversion to a type of width N, the value is reduced modulo 2^N to be within range of the type; no signal is raised. *)
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index cc43c32ace..724c0776b5 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -366,6 +366,7 @@ module Size : sig
   val range           : Cil.ikind -> Z.t * Z.t
   val is_cast_injective : from_type:Cil.typ -> to_type:Cil.typ -> bool
   val bits            : Cil.ikind -> int * int
+  val cast            : Cil.ikind -> Z.t -> Z.t
 end
 
 module BISet: SetDomain.S with type elt = Z.t
@@ -408,7 +409,6 @@ module Interval32 :Y with (* type t = (IntOps.Int64Ops.t * IntOps.Int64Ops.t) op
 module BigInt:
   sig
     include Printable.S with type t = Z.t
-    val cast_to: Cil.ikind -> Z.t -> Z.t
   end
 
 module Interval : SOverflow with type int_t = Z.t
diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml
index fa41ba645e..e18ce65554 100644
--- a/src/domains/intDomainProperties.ml
+++ b/src/domains/intDomainProperties.ml
@@ -73,7 +73,7 @@ struct
   module Base =
   struct
     include IntDomain.Integers(IntOps.BigIntOps)
-    let arbitrary () = QCheck.map_same_type (IntDomain.BigInt.cast_to (Ikind.ikind ())) (arbitrary ())
+    let arbitrary () = QCheck.map_same_type (IntDomain.Size.cast (Ikind.ikind ())) (arbitrary ())
   end
 
   include SetDomain.Make(Base)

From a8d74cd2b991c33368991cfaf32b0d1a806f2379 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 22 Jan 2024 16:48:09 +0200
Subject: [PATCH 43/52] Include Printable to IntOpsDecorator and make IntOps
 printable

---
 src/cdomain/value/cdomains/intDomain.ml     |  9 ---------
 src/cdomain/value/cdomains/intDomain.mli    |  5 -----
 src/cdomain/value/cdomains/nullByteSet.ml   |  6 +++---
 src/cdomains/apron/sharedFunctions.apron.ml |  2 +-
 src/common/util/intOps.ml                   | 14 ++++++++++++++
 5 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 085d0f584a..1fc6a49143 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1774,16 +1774,7 @@ struct
 end
 
 module BigInt = struct
-  include Printable.StdLeaf
   include IntOps.BigIntOps
-  let name () = "BigIntPrintable"
-  let show x = Z.to_string x
-  include Printable.SimpleShow (
-    struct
-      type nonrec t = t
-      let show = show
-    end
-    )
   let arbitrary () = QCheck.map ~rev:Z.to_int64 Z.of_int64 QCheck.int64
 end
 
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index 724c0776b5..35ebc03794 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -406,11 +406,6 @@ module IntervalSetFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = I
 
 module Interval32 :Y with (* type t = (IntOps.Int64Ops.t * IntOps.Int64Ops.t) option and *) type int_t = IntOps.Int64Ops.t
 
-module BigInt:
-  sig
-    include Printable.S with type t = Z.t
-  end
-
 module Interval : SOverflow with type int_t = Z.t
 
 module IntervalSet : SOverflow with type int_t = Z.t
diff --git a/src/cdomain/value/cdomains/nullByteSet.ml b/src/cdomain/value/cdomains/nullByteSet.ml
index ff5d0270e0..ae382b6118 100644
--- a/src/cdomain/value/cdomains/nullByteSet.ml
+++ b/src/cdomain/value/cdomains/nullByteSet.ml
@@ -1,7 +1,7 @@
 (** Abstract domains for tracking [NULL] bytes in C arrays. *)
 
 module MustSet = struct
-  module M = SetDomain.Reverse (SetDomain.ToppedSet (IntDomain.BigInt) (struct let topname = "All Null" end))
+  module M = SetDomain.Reverse (SetDomain.ToppedSet (IntOps.BigIntOps) (struct let topname = "All Null" end))
   include M
 
   let compute_set len =
@@ -45,7 +45,7 @@ module MustSet = struct
 end
 
 module MaySet = struct
-  module M = SetDomain.ToppedSet (IntDomain.BigInt) (struct let topname = "All Null" end)
+  module M = SetDomain.ToppedSet (IntOps.BigIntOps) (struct let topname = "All Null" end)
   include M
 
   let elements ?max_size may_nulls_set =
@@ -80,7 +80,7 @@ end
 module MustMaySet = struct
   include Lattice.Prod (MustSet) (MaySet)
 
-  module Set = SetDomain.Make (IntDomain.BigInt)
+  module Set = SetDomain.Make (IntOps.BigIntOps)
 
   type mode = Definitely | Possibly
 
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index ff1f14891e..f7b800a404 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -129,7 +129,7 @@ struct
             match Bounds.bound_texpr d texpr1 with
             | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 -> ()
             | min_opt, max_opt ->
-              if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntDomain.BigInt.pretty ())) min_opt (Pretty.docOpt (IntDomain.BigInt.pretty ())) max_opt;
+              if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt;
               raise (Unsupported_CilExp Overflow)
           );
           expr
diff --git a/src/common/util/intOps.ml b/src/common/util/intOps.ml
index 24aa4e3f66..0f0da6fa7b 100644
--- a/src/common/util/intOps.ml
+++ b/src/common/util/intOps.ml
@@ -9,6 +9,8 @@ module type IntOpsBase =
 sig
   type t
 
+  val name : unit -> string
+
   (* Constants *)
   val zero : t
   val one : t
@@ -74,6 +76,7 @@ end
 module NIntOpsBase : IntOpsBase with type t = int =
 struct
   type t = int [@@deriving hash]
+  let name () = "int"
   let zero = 0
   let one = 1
   let lower_bound = Some min_int
@@ -117,6 +120,7 @@ end
 module Int32OpsBase : IntOpsBase with type t = int32 =
 struct
   type t = int32 [@@deriving hash]
+  let name () = "int32"
   let zero = 0l
   let one = 1l
   let lower_bound = Some Int32.min_int
@@ -162,6 +166,7 @@ end
 module Int64OpsBase : IntOpsBase with type t = int64 =
 struct
   type t = int64 [@@deriving hash]
+  let name () = "int64"
   let zero = 0L
   let one = 1L
   let lower_bound = Some Int64.min_int
@@ -207,6 +212,7 @@ end
 module BigIntOpsBase : IntOpsBase with type t = Z.t =
 struct
   type t = Z.t
+  let name () = "Z"
   let zero = Z.zero
   let one = Z.one
   let upper_bound = None
@@ -251,7 +257,15 @@ end
 
 module IntOpsDecorator(B: IntOpsBase) =
 struct
+  include Printable.StdLeaf
   include B
+  let show = to_string
+  include Printable.SimpleShow (
+    struct
+      type nonrec t = t
+      let show = to_string
+    end
+    )
   let pred x = sub x one
   let of_bool x = if x then one else zero
   let to_bool x = x <> zero

From bc267c80c0f4c4a007f5a9222d3474fe1f6847d7 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 22 Jan 2024 16:54:59 +0200
Subject: [PATCH 44/52] Remove IntDomain.BigInt

---
 src/cdomain/value/cdomains/intDomain.ml | 21 ++++++++-------------
 src/common/util/intOps.ml               |  9 +++++++++
 2 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 1fc6a49143..e32cf098c1 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1773,13 +1773,8 @@ struct
   include (Lattice.Reverse (Base) : Lattice.S with type t := Base.t)
 end
 
-module BigInt = struct
-  include IntOps.BigIntOps
-  let arbitrary () = QCheck.map ~rev:Z.to_int64 Z.of_int64 QCheck.int64
-end
-
 module BISet = struct
-  include SetDomain.Make (BigInt)
+  include SetDomain.Make (IntOps.BigIntOps)
   let is_singleton s = cardinal s = 1
 end
 
@@ -2062,7 +2057,7 @@ struct
   let of_bool = of_bool_cmp
   let to_bool x =
     match x with
-    | `Definite x -> Some (BigInt.to_bool x)
+    | `Definite x -> Some (IntOps.BigIntOps.to_bool x)
     | `Excluded (s,r) when S.mem Z.zero s -> Some true
     | _ -> None
   let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L))
@@ -2257,14 +2252,14 @@ struct
     | _, Some false ->
       of_bool ik false
     | _, _ ->
-      lift2 BigInt.logand ik x y
+      lift2 IntOps.BigIntOps.logand ik x y
   let logor ik x y =
     match to_bool x, to_bool y with
     | Some true, _
     | _, Some true ->
       of_bool ik true
     | _, _ ->
-      lift2 BigInt.logor ik x y
+      lift2 IntOps.BigIntOps.logor ik x y
   let lognot ik = eq ik (of_int ik Z.zero)
 
   let invariant_ikind e ik (x:t) =
@@ -2297,12 +2292,12 @@ struct
     let definite x = of_int ik x in
     let shrink = function
       | `Excluded (s, _) -> GobQCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *)
-      | `Definite x -> (return `Bot) <+> (GobQCheck.shrink (BigInt.arbitrary ()) x >|= definite)
+      | `Definite x -> (return `Bot) <+> (GobQCheck.shrink (IntOps.BigIntOps.arbitrary ()) x >|= definite)
       | `Bot -> empty
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map excluded (S.arbitrary ());
-      10, QCheck.map definite (BigInt.arbitrary ());
+      10, QCheck.map definite (IntOps.BigIntOps.arbitrary ());
       1, QCheck.always `Bot
     ] (* S TODO: decide frequencies *)
 
@@ -2630,8 +2625,8 @@ module Enums : S with type int_t = Z.t = struct
       | Some b -> of_bool ik (not b)
       | None -> top_bool
 
-  let logand = lift2 BigInt.logand
-  let logor  = lift2 BigInt.logor
+  let logand = lift2 IntOps.BigIntOps.logand
+  let logor  = lift2 IntOps.BigIntOps.logor
   let maximal = function
     | Inc xs when not (BISet.is_empty xs) -> Some (BISet.max_elt xs)
     | Exc (excl,r) ->
diff --git a/src/common/util/intOps.ml b/src/common/util/intOps.ml
index 0f0da6fa7b..a14305b0c2 100644
--- a/src/common/util/intOps.ml
+++ b/src/common/util/intOps.ml
@@ -55,6 +55,8 @@ sig
   val to_string : t -> string
   val of_bigint : Z.t -> t
   val to_bigint : t -> Z.t
+
+  val arbitrary : unit -> t QCheck.arbitrary
 end
 
 module type IntOps =
@@ -115,6 +117,8 @@ struct
   let to_string = string_of_int
   let of_bigint = Z.to_int
   let to_bigint = Z.of_int
+
+  let arbitrary () = QCheck.int
 end
 
 module Int32OpsBase : IntOpsBase with type t = int32 =
@@ -161,6 +165,8 @@ struct
   let to_string = Int32.to_string
   let of_bigint = Z.to_int32
   let to_bigint = Z.of_int32
+
+  let arbitrary () = QCheck.int32
 end
 
 module Int64OpsBase : IntOpsBase with type t = int64 =
@@ -207,6 +213,8 @@ struct
   let to_string = Int64.to_string
   let of_bigint = Z.to_int64
   let to_bigint = Z.of_int64
+
+  let arbitrary () = QCheck.int64
 end
 
 module BigIntOpsBase : IntOpsBase with type t = Z.t =
@@ -252,6 +260,7 @@ struct
   let bitor = Z.logor
   let bitxor = Z.logxor
 
+  let arbitrary () = QCheck.map ~rev:Z.to_int64 Z.of_int64 QCheck.int64
 end
 
 

From 0e1b389f56e419d792c5032ce7d8dc1e74609930 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 23 Jan 2024 12:50:06 +0200
Subject: [PATCH 45/52] Implement GobZ.pretty and use it where possible

---
 src/analyses/baseInvariant.ml                    |  6 +++---
 src/cdomain/value/cdomains/intDomain.ml          | 11 ++++++-----
 src/cdomains/apron/affineEqualityDomain.apron.ml |  2 +-
 src/common/util/cilfacade.ml                     |  2 +-
 src/util/std/gobZ.ml                             |  2 ++
 5 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index f6cd11afa9..efd098d994 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -139,7 +139,7 @@ struct
               match ID.to_int n with
               | Some n ->
                 (* When x != n, we can return a singleton exclusion set *)
-                if M.tracing then M.tracec "invariant" "Yes, %a is not %s\n" d_lval x (Z.to_string n);
+                if M.tracing then M.tracec "invariant" "Yes, %a is not %a\n" d_lval x GobZ.pretty n;
                 let ikind = Cilfacade.get_ikind_exp (Lval lval) in
                 Some (x, Int (ID.of_excl_list ikind [n]))
               | None -> None
@@ -172,7 +172,7 @@ struct
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
-                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %s\n\n" d_lval x (Z.to_string n);
+                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a\n\n" d_lval x GobZ.pretty n;
                 Some (x, Int (range_from n))
               | None -> None
             end
@@ -187,7 +187,7 @@ struct
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
               | Some n ->
-                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %s\n\n" d_lval x (Z.to_string n);
+                if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a\n\n" d_lval x GobZ.pretty n;
                 Some (x, Int (range_from n))
               | None -> None
             end
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index e32cf098c1..75224084e1 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -415,7 +415,7 @@ module Size = struct (* size in bits as int, range as int64 *)
   let is_cast_injective ~from_type ~to_type =
     let (from_min, from_max) = range (Cilfacade.get_ikind from_type) in
     let (to_min, to_max) = range (Cilfacade.get_ikind to_type) in
-    if M.tracing then M.trace "int" "is_cast_injective %a (%s, %s) -> %a (%s, %s)\n" CilType.Typ.pretty from_type (Z.to_string from_min) (Z.to_string from_max) CilType.Typ.pretty to_type (Z.to_string to_min) (Z.to_string to_max);
+    if M.tracing then M.trace "int" "is_cast_injective %a (%a, %a) -> %a (%a, %a)\n" CilType.Typ.pretty from_type GobZ.pretty from_min GobZ.pretty from_max CilType.Typ.pretty to_type GobZ.pretty to_min GobZ.pretty to_max;
     Z.compare to_min from_min <= 0 && Z.compare from_max to_max <= 0
 
   let cast t x = (* TODO: overflow is implementation-dependent! *)
@@ -430,7 +430,7 @@ module Size = struct (* size in bits as int, range as int64 *)
         else if Z.lt y a then Z.add y c
         else y
       in
-      if M.tracing then M.tracel "cast" "Cast %s to range [%s, %s] (%s) = %s (%s in int64)\n" (Z.to_string x) (Z.to_string a) (Z.to_string b) (Z.to_string c) (Z.to_string y) (if is_int64_big_int y then "fits" else "does not fit");
+      if M.tracing then M.tracel "cast" "Cast %a to range [%a, %a] (%a) = %a (%s in int64)\n" GobZ.pretty x GobZ.pretty a GobZ.pretty b GobZ.pretty c GobZ.pretty y (if is_int64_big_int y then "fits" else "does not fit");
       y
 
   let min_range_sign_agnostic x =
@@ -3215,9 +3215,10 @@ struct
     | _ -> None
 
   let refine_with_interval ik (cong : t) (intv : (int_t * int_t) option) : t =
-    let pretty_intv _ i = (match i with
-        | Some(l, u) -> let s = "["^Z.to_string l^","^Z.to_string u^"]" in Pretty.text s
-        | _ -> Pretty.text ("Display Error")) in
+    let pretty_intv _ i =
+      match i with
+      | Some (l, u) -> Pretty.dprintf "[%a,%a]" GobZ.pretty l GobZ.pretty u
+      | _ -> Pretty.text ("Display Error") in
     let refn = refine_with_interval ik cong intv in
     if M.tracing then M.trace "refine" "cong_refine_with_interval %a %a -> %a\n" pretty cong pretty_intv intv pretty refn;
     refn
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 5485dd3f02..661e220d69 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -224,7 +224,7 @@ struct
     let res = bound_texpr d texpr1 in
     (if M.tracing then
        match res with
-       | Some min, Some max -> M.tracel "bounds" "min: %s max: %s" (Z.to_string min) (Z.to_string max)
+       | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pretty min GobZ.pretty max
        | _ -> ()
     );
     res
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index eff97da404..749ede4fc2 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -427,7 +427,7 @@ let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts =
     pretty_typsig_like_typ
       (Some (name'
              ++ text "["
-             ++ (match lo with None -> nil | Some e -> text (Z.to_string e))
+             ++ (match lo with None -> nil | Some e -> GobZ.pretty () e)
              ++ text "]"))
       ()
       elemt
diff --git a/src/util/std/gobZ.ml b/src/util/std/gobZ.ml
index 598b8448dc..02110ac8bb 100644
--- a/src/util/std/gobZ.ml
+++ b/src/util/std/gobZ.ml
@@ -8,3 +8,5 @@ let rec for_all_range f (a, b) =
     true
   else
     f a && for_all_range f (Z.succ a, b)
+
+let pretty () x = GoblintCil.Pretty.text (Z.to_string x)

From 0417cf723bf1a989b037c2ad21dea50203ac75b3 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 23 Jan 2024 12:51:24 +0200
Subject: [PATCH 46/52] Simplify same

---
 src/cdomain/value/cdomains/intDomain.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 75224084e1..c3ab114afc 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -3575,12 +3575,14 @@ module IntDomTupleImpl = struct
     if List.mem `Eq xs then `Eq else
     if List.mem `Neq xs then `Neq else
       `Top
-  let same show x = let xs = to_list_some x in let us = List.unique xs in let n = List.length us in
-    if n = 1 then Some (List.hd xs)
-    else (
-      if n>1 then Messages.info ~category:Unsound "Inconsistent state! %a" (Pretty.docList ~sep:(Pretty.text ",") (Pretty.text % show)) us; (* do not want to abort *)
+  let same show x =
+    let us = List.unique (to_list_some x) in
+    match us with
+    | [x] -> Some (List.hd us)
+    | [] -> None
+    | _ ->
+      Messages.info ~category:Unsound "Inconsistent state! %a" (Pretty.docList ~sep:(Pretty.text ",") (Pretty.text % show)) us; (* do not want to abort *)
       None
-    )
   let to_int = same Z.to_string % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_int }
   let to_bool = same string_of_bool % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.to_bool }
   let minimal = flat (List.max ~cmp:Z.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.minimal }

From 3991fbd1a6b358539abf469237e214050f1a22e6 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com>
Date: Tue, 23 Jan 2024 12:54:56 +0200
Subject: [PATCH 47/52] Remove redundant List.hd call

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 src/cdomain/value/cdomains/intDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index c3ab114afc..46c43f44dd 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -3578,7 +3578,7 @@ module IntDomTupleImpl = struct
   let same show x =
     let us = List.unique (to_list_some x) in
     match us with
-    | [x] -> Some (List.hd us)
+    | [x] -> Some x
     | [] -> None
     | _ ->
       Messages.info ~category:Unsound "Inconsistent state! %a" (Pretty.docList ~sep:(Pretty.text ",") (Pretty.text % show)) us; (* do not want to abort *)

From 190dd1fac2ac20551271bd4d212c1c38b542a121 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 26 Jan 2024 13:29:34 +0200
Subject: [PATCH 48/52] Rename log.* functions to c_log.*

---
 src/analyses/base.ml                     |  8 +--
 src/analyses/baseInvariant.ml            |  2 +-
 src/cdomain/value/cdomains/intDomain.ml  | 90 ++++++++++++------------
 src/cdomain/value/cdomains/intDomain.mli | 12 ++--
 src/common/util/intOps.ml                | 20 +++---
 src/domains/intDomainProperties.ml       | 18 ++---
 6 files changed, 75 insertions(+), 75 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 440a1fcd96..caa718a616 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -174,7 +174,7 @@ struct
   let unop_ID = function
     | Neg  -> ID.neg
     | BNot -> ID.bitnot
-    | LNot -> ID.lognot
+    | LNot -> ID.c_lognot
 
   let unop_FD = function
     | Neg  -> FD.neg
@@ -217,8 +217,8 @@ struct
     | BXor -> ID.bitxor
     | Shiftlt -> ID.shift_left
     | Shiftrt -> ID.shift_right
-    | LAnd -> ID.logand
-    | LOr -> ID.logor
+    | LAnd -> ID.c_logand
+    | LOr -> ID.c_logor
     | b -> (fun x y -> (ID.top_of result_ik))
 
   let binop_FD (result_fk: Cil.fkind) = function
@@ -2436,7 +2436,7 @@ struct
           | Isgreaterequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.ge x y))
           | Isless (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.lt x y))
           | Islessequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.le x y))
-          | Islessgreater (x,y) -> Int(ID.logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y)))
+          | Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y)))
           | Isunordered (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.unordered x y))
           | Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
           | Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index efd098d994..6634b3f21c 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -44,7 +44,7 @@ struct
   let unop_ID = function
     | Neg  -> ID.neg
     | BNot -> ID.bitnot
-    | LNot -> ID.lognot
+    | LNot -> ID.c_lognot
 
   let unop_FD = function
     | Neg  -> FD.neg
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 46c43f44dd..e192e1341a 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -122,9 +122,9 @@ sig
   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
+  val c_lognot: t -> t
+  val c_logand: t -> t -> t
+  val c_logor : t -> t -> t
 
 end
 
@@ -153,9 +153,9 @@ sig
   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
+  val c_lognot: Cil.ikind -> t -> t
+  val c_logand: Cil.ikind -> t -> t -> t
+  val c_logor : Cil.ikind -> t -> t -> t
 
 end
 
@@ -359,9 +359,9 @@ struct
   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 c_lognot = lift_logical I.c_lognot
+  let c_logand = lift2 I.c_logand
+  let c_logor = lift2 I.c_logor
 
   let cast_to ?torg ikind x = {v = I.cast_to ~torg:(TInt(x.ikind,[])) ikind x.v; ikind}
 
@@ -703,8 +703,8 @@ struct
       | Some x, Some y -> of_bool ik (f x y)
       | _              -> top_of ik
 
-  let logor = log (||) ~annihilator:true
-  let logand = log (&&) ~annihilator:false
+  let c_logor = log (||) ~annihilator:true
+  let c_logand = log (&&) ~annihilator:false
 
   let log1 f ik i1 =
     if is_bot i1 then
@@ -714,7 +714,7 @@ struct
       | Some x -> of_bool ik (f ik x)
       | _      -> top_of ik
 
-  let lognot = log1 (fun _ik -> not)
+  let c_lognot = log1 (fun _ik -> not)
 
   let bit f ik i1 i2 =
     match is_bot i1, is_bot i2 with
@@ -1298,7 +1298,7 @@ struct
     let interval_shiftright = bitcomp (fun x y -> Ints_t.shift_right x (Ints_t.to_int y)) ik in
     binary_op_with_ovc x y interval_shiftright
 
-  let lognot ik x =
+  let c_lognot ik x =
     let log1 f ik i1 =
       match interval_to_bool i1 with
       | Some x -> of_bool ik (f x)
@@ -1307,11 +1307,11 @@ struct
     let interval_lognot = log1 not ik in
     unop x interval_lognot
 
-  let logand ik x y =
+  let c_logand ik x y =
     let interval_logand = log (&&) ik in
     binop x y interval_logand
 
-  let logor ik x y =
+  let c_logor ik x y =
     let interval_logor = log (||) ik in
     binop x y interval_logor
 
@@ -1597,9 +1597,9 @@ struct
   let bitxor = Ints_t.bitxor
   let shift_left  n1 n2 = Ints_t.shift_left n1 (Ints_t.to_int n2)
   let shift_right n1 n2 = Ints_t.shift_right n1 (Ints_t.to_int n2)
-  let lognot n1    = of_bool (not (to_bool' n1))
-  let logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2))
-  let logor  n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2))
+  let c_lognot n1    = of_bool (not (to_bool' n1))
+  let c_logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2))
+  let c_logor  n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2))
   let cast_to ?torg t x =  failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "."
   let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 (* TODO: use ikind *)
   let invariant _ _ = Invariant.none (* TODO *)
@@ -1688,9 +1688,9 @@ struct
   let bitxor = lift2 Base.bitxor
   let shift_left  = lift2 Base.shift_left
   let shift_right = lift2 Base.shift_right
-  let lognot = lift1 Base.lognot
-  let logand = lift2 Base.logand
-  let logor  = lift2 Base.logor
+  let c_lognot = lift1 Base.c_lognot
+  let c_logand = lift2 Base.c_logand
+  let c_logor  = lift2 Base.c_logor
 
   let invariant e = function
     | `Lifted x -> Base.invariant e x
@@ -1755,9 +1755,9 @@ struct
   let bitxor = lift2 Base.bitxor
   let shift_left  = lift2 Base.shift_left
   let shift_right = lift2 Base.shift_right
-  let lognot = lift1 Base.lognot
-  let logand = lift2 Base.logand
-  let logor  = lift2 Base.logor
+  let c_lognot = lift1 Base.c_lognot
+  let c_logand = lift2 Base.c_logand
+  let c_logor  = lift2 Base.c_logor
 
   let invariant e = function
     | `Lifted x -> Base.invariant e x
@@ -2246,21 +2246,21 @@ struct
   let shift_right =
     shift Z.shift_right
   (* TODO: lift does not treat Not {0} as true. *)
-  let logand ik x y =
+  let c_logand ik x y =
     match to_bool x, to_bool y with
     | Some false, _
     | _, Some false ->
       of_bool ik false
     | _, _ ->
-      lift2 IntOps.BigIntOps.logand ik x y
-  let logor ik x y =
+      lift2 IntOps.BigIntOps.c_logand ik x y
+  let c_logor ik x y =
     match to_bool x, to_bool y with
     | Some true, _
     | _, Some true ->
       of_bool ik true
     | _, _ ->
-      lift2 IntOps.BigIntOps.logor ik x y
-  let lognot ik = eq ik (of_int ik Z.zero)
+      lift2 IntOps.BigIntOps.c_logor ik x y
+  let c_lognot ik = eq ik (of_int ik Z.zero)
 
   let invariant_ikind e ik (x:t) =
     match x with
@@ -2366,9 +2366,9 @@ struct
   let bitxor x y = x && not y || not x && y
   let shift_left  n1 n2 = n1
   let shift_right n1 n2 = n1
-  let lognot = (not)
-  let logand = (&&)
-  let logor  = (||)
+  let c_lognot = (not)
+  let c_logand = (&&)
+  let c_logor  = (||)
   let arbitrary () = QCheck.bool
   let invariant _ _ = Invariant.none (* TODO *)
 end
@@ -2617,7 +2617,7 @@ module Enums : S with type int_t = Z.t = struct
   let starting ?(suppress_ovwarn=false) ikind x = top_of ikind
   let ending ?(suppress_ovwarn=false) ikind x = top_of ikind
 
-  let lognot ik x =
+  let c_lognot ik x =
     if is_bot x
     then x
     else
@@ -2625,8 +2625,8 @@ module Enums : S with type int_t = Z.t = struct
       | Some b -> of_bool ik (not b)
       | None -> top_bool
 
-  let logand = lift2 IntOps.BigIntOps.logand
-  let logor  = lift2 IntOps.BigIntOps.logor
+  let c_logand = lift2 IntOps.BigIntOps.c_logand
+  let c_logor  = lift2 IntOps.BigIntOps.c_logor
   let maximal = function
     | Inc xs when not (BISet.is_empty xs) -> Some (BISet.max_elt xs)
     | Exc (excl,r) ->
@@ -2680,7 +2680,7 @@ module Enums : S with type int_t = Z.t = struct
           else
             top_bool)
 
-  let ne ik x y = lognot ik (eq ik x y)
+  let ne ik x y = c_lognot ik (eq ik x y)
 
   let invariant_ikind e ik x =
     match x with
@@ -2929,8 +2929,8 @@ struct
       | Some x, Some y -> of_bool ik (f x y)
       | _              -> top_of ik
 
-  let logor = log (||)
-  let logand = log (&&)
+  let c_logor = log (||)
+  let c_logand = log (&&)
 
   let log1 f ik i1 =
     if is_bot i1 then
@@ -2940,7 +2940,7 @@ struct
       | Some x -> of_bool ik (f ik x)
       | _      -> top_of ik
 
-  let lognot = log1 (fun _ik -> not)
+  let c_lognot = log1 (fun _ik -> not)
 
   let shift_right _ _ _ = top()
 
@@ -3563,8 +3563,8 @@ module IntDomTupleImpl = struct
   let bitnot ik =
     map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.bitnot ik)}
 
-  let lognot ik =
-    map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.lognot ik)}
+  let c_lognot ik =
+    map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_lognot ik)}
 
   let cast_to ?torg ?no_ov t =
     mapovc ~cast:true t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ?torg ?no_ov t)}
@@ -3689,11 +3689,11 @@ module IntDomTupleImpl = struct
   let shift_right ik =
     map2ovc ik {f2_ovc= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.shift_right ik)}
 
-  let logand ik =
-    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.logand ik)}
+  let c_logand ik =
+    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_logand ik)}
 
-  let logor ik =
-    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.logor ik)}
+  let c_logor ik =
+    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_logor ik)}
 
 
   (* printing boilerplate *)
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index 35ebc03794..ebbf8ceaf3 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -77,13 +77,13 @@ sig
 
   (** {b Logical operators} *)
 
-  val lognot: t -> t
+  val c_lognot: t -> t
   (** Logical not: [!x] *)
 
-  val logand: t -> t -> t
+  val c_logand: t -> t -> t
   (** Logical and: [x && y] *)
 
-  val logor : t -> t -> t
+  val c_logor : t -> t -> t
   (** Logical or: [x || y] *)
 
 end
@@ -156,13 +156,13 @@ sig
 
   (** {b Logical operators} *)
 
-  val lognot: Cil.ikind -> t -> t
+  val c_lognot: Cil.ikind -> t -> t
   (** Logical not: [!x] *)
 
-  val logand: Cil.ikind -> t -> t -> t
+  val c_logand: Cil.ikind -> t -> t -> t
   (** Logical and: [x && y] *)
 
-  val logor : Cil.ikind -> t -> t -> t
+  val c_logor : Cil.ikind -> t -> t -> t
   (** Logical or: [x || y] *)
 
 end
diff --git a/src/common/util/intOps.ml b/src/common/util/intOps.ml
index a14305b0c2..17df714a82 100644
--- a/src/common/util/intOps.ml
+++ b/src/common/util/intOps.ml
@@ -62,12 +62,12 @@ end
 module type IntOps =
 sig
   include IntOpsBase
-  (* Logical: These are intended to be the logical operations in the C sense!   *)
-  (* Int64 calls its bit-wise operations e.g. logand, we call those e.g. bitand *)
-  val logand : t -> t -> t
-  val logor : t -> t -> t
-  val logxor : t -> t -> t
-  val lognot : t -> t
+  (* Logical: These are intended to be the logical operations in the C sense! *)
+  (* Int64 calls its bit-wise operations e.g. logand, without the c_ prefix *)
+  val c_logand : t -> t -> t
+  val c_logor : t -> t -> t
+  val c_logxor : t -> t -> t
+  val c_lognot : t -> t
   val to_bool : t -> bool
   val of_bool : bool -> t
 end
@@ -281,10 +281,10 @@ struct
 
   (* These are logical operations in the C sense! *)
   let log_op op a b = of_bool @@ op (to_bool a) (to_bool b)
-  let lognot x = of_bool (x = zero)
-  let logand = log_op (&&)
-  let logor = log_op (||)
-  let logxor = log_op (<>)
+  let c_lognot x = of_bool (x = zero)
+  let c_logand = log_op (&&)
+  let c_logor = log_op (||)
+  let c_logxor = log_op (<>)
 
   let lt x y = of_bool (compare x y < 0)
   let gt x y = of_bool (compare x y > 0)
diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml
index e18ce65554..fcff746936 100644
--- a/src/domains/intDomainProperties.ml
+++ b/src/domains/intDomainProperties.ml
@@ -51,9 +51,9 @@ struct
   let bitxor = bitxor (Ik.ikind ())
   let shift_left = shift_left (Ik.ikind ())
   let shift_right = shift_right (Ik.ikind ())
-  let lognot = lognot (Ik.ikind ())
-  let logand = logand (Ik.ikind ())
-  let logor = logor (Ik.ikind ())
+  let c_lognot = c_lognot (Ik.ikind ())
+  let c_logand = c_logand (Ik.ikind ())
+  let c_logor = c_logor (Ik.ikind ())
 
   let of_int = of_int (Ik.ikind ())
   let of_bool = of_bool (Ik.ikind ())
@@ -104,9 +104,9 @@ struct
   let shift_left  = lift2 Base.shift_left
   let shift_right = lift2 Base.shift_right
 
-  let lognot = lift1 Base.lognot
-  let logand = lift2 Base.logand
-  let logor  = lift2 Base.logor
+  let c_lognot = lift1 Base.c_lognot
+  let c_logand = lift2 Base.c_logand
+  let c_logor  = lift2 Base.c_logor
 end
 
 
@@ -145,9 +145,9 @@ struct
   let valid_shift_left = make_valid2 ~name:"shift_left" ~cond:shift_cond CD.shift_left AD.shift_left
   let valid_shift_right = make_valid2 ~name:"shift_right" ~cond:shift_cond CD.shift_right AD.shift_right
 
-  let valid_lognot = make_valid1 ~name:"lognot" ~cond:not_bot CD.lognot AD.lognot
-  let valid_logand = make_valid2 ~name:"logand" ~cond:none_bot CD.logand AD.logand
-  let valid_logor = make_valid2 ~name:"logor" ~cond:none_bot CD.logor AD.logor
+  let valid_lognot = make_valid1 ~name:"lognot" ~cond:not_bot CD.c_lognot AD.c_lognot
+  let valid_logand = make_valid2 ~name:"logand" ~cond:none_bot CD.c_logand AD.c_logand
+  let valid_logor = make_valid2 ~name:"logor" ~cond:none_bot CD.c_logor AD.c_logor
 
   let tests = [
     valid_neg;

From bdd61d1a2a2ef9c290e682a14db9109d71fa3419 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 26 Jan 2024 13:48:30 +0200
Subject: [PATCH 49/52] Rename bit.* functions to log.*

---
 src/analyses/base.ml                     |   8 +-
 src/analyses/baseInvariant.ml            |   2 +-
 src/cdomain/value/cdomains/intDomain.ml  | 132 +++++++++++------------
 src/cdomain/value/cdomains/intDomain.mli |  16 +--
 src/common/util/intOps.ml                |  40 +++----
 src/domains/intDomainProperties.ml       |  32 +++---
 unittest/cdomains/intDomainTest.ml       |  12 +--
 7 files changed, 121 insertions(+), 121 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index caa718a616..b945f34f9d 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -173,7 +173,7 @@ struct
 
   let unop_ID = function
     | Neg  -> ID.neg
-    | BNot -> ID.bitnot
+    | BNot -> ID.lognot
     | LNot -> ID.c_lognot
 
   let unop_FD = function
@@ -212,9 +212,9 @@ struct
          evalint: base eval_rv 1 -> (1,[1,1])
          evalint: base query_evalint m == 1 -> (0,[1,1]) *)
     | Ne -> ID.ne
-    | BAnd -> ID.bitand
-    | BOr -> ID.bitor
-    | BXor -> ID.bitxor
+    | BAnd -> ID.logand
+    | BOr -> ID.logor
+    | BXor -> ID.logxor
     | Shiftlt -> ID.shift_left
     | Shiftrt -> ID.shift_right
     | LAnd -> ID.c_logand
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 6634b3f21c..003ac06b92 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -43,7 +43,7 @@ struct
 
   let unop_ID = function
     | Neg  -> ID.neg
-    | BNot -> ID.bitnot
+    | BNot -> ID.lognot
     | LNot -> ID.c_lognot
 
   let unop_FD = function
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index e192e1341a..4372df13fe 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -114,10 +114,10 @@ sig
   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 lognot: t -> t
+  val logand: t -> t -> t
+  val logor : t -> t -> t
+  val logxor: t -> t -> t
 
   val shift_left : t -> t -> t
   val shift_right: t -> t -> t
@@ -145,10 +145,10 @@ sig
   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 lognot: Cil.ikind -> t -> t
+  val logand: Cil.ikind -> t -> t -> t
+  val logor : Cil.ikind -> t -> t -> t
+  val logxor: Cil.ikind -> t -> t -> t
 
   val shift_left : Cil.ikind -> t -> t -> t
   val shift_right: Cil.ikind -> t -> t -> t
@@ -353,10 +353,10 @@ struct
   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 lognot = lift I.lognot
+  let logand = lift2 I.logand
+  let logor = lift2 I.logor
+  let logxor = lift2 I.logxor
   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 c_lognot = lift_logical I.c_lognot
@@ -736,21 +736,21 @@ struct
       | Some x, Some y -> (try of_int ik (f ik x y) with Division_by_zero | Invalid_argument _ -> (top_of ik,{underflow=false; overflow=false}))
       | _              -> (top_of ik,{underflow=true; overflow=true})
 
-  let bitxor = bit (fun _ik -> Ints_t.bitxor)
+  let logxor = bit (fun _ik -> Ints_t.logxor)
 
-  let bitand ik i1 i2 =
+  let logand 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" (show i1) (show i2)))
     | _ ->
       match to_int i1, to_int i2 with
-      | Some x, Some y -> (try of_int ik (Ints_t.bitand x y) |> fst with Division_by_zero -> top_of ik)
+      | Some x, Some y -> (try of_int ik (Ints_t.logand x y) |> fst with Division_by_zero -> top_of ik)
       | _, Some y when Ints_t.equal y Ints_t.zero -> of_int ik Ints_t.zero |> fst
       | _, Some y when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
       | _ -> top_of ik
 
-  let bitor  = bit (fun _ik -> Ints_t.bitor)
+  let logor  = bit (fun _ik -> Ints_t.logor)
 
   let bit1 f ik i1 =
     if is_bot i1 then
@@ -760,7 +760,7 @@ struct
       | Some x -> of_int ik (f ik x) |> fst
       | _      -> top_of ik
 
-  let bitnot = bit1 (fun _ik -> Ints_t.bitnot)
+  let lognot = bit1 (fun _ik -> Ints_t.lognot)
   let shift_right = bitcomp (fun _ik x y -> Ints_t.shift_right x (Ints_t.to_int y))
 
   let neg ?no_ov ik = function None -> (None,{underflow=false; overflow=false}) | Some x -> norm ik @@ Some (IArith.neg x)
@@ -1270,25 +1270,25 @@ struct
     | Some x, Some y -> (try of_int ik (f x y) with Division_by_zero | Invalid_argument _ -> (top_of ik,{overflow=false; underflow=false}))
     | _, _ -> (top_of ik,{overflow=false; underflow=false})
 
-  let bitand ik x y =
-    let interval_bitand = bit Ints_t.bitand ik in
-    binop x y interval_bitand
+  let logand ik x y =
+    let interval_logand = bit Ints_t.logand ik in
+    binop x y interval_logand
 
-  let bitor ik x y =
-    let interval_bitor = bit Ints_t.bitor ik in
-    binop x y interval_bitor
+  let logor ik x y =
+    let interval_logor = bit Ints_t.logor ik in
+    binop x y interval_logor
 
-  let bitxor ik x y =
-    let interval_bitxor = bit Ints_t.bitxor ik in
-    binop x y interval_bitxor
+  let logxor ik x y =
+    let interval_logxor = bit Ints_t.logxor ik in
+    binop x y interval_logxor
 
-  let bitnot ik x =
-    let interval_bitnot i =
+  let lognot ik x =
+    let interval_lognot i =
       match interval_to_int i with
-      | Some x -> of_int ik (Ints_t.bitnot x) |> fst
+      | Some x -> of_int ik (Ints_t.lognot x) |> fst
       | _ -> top_of ik
     in
-    unop x interval_bitnot
+    unop x interval_lognot
 
   let shift_left ik x y =
     let interval_shiftleft = bitcomp (fun x y -> Ints_t.shift_left x (Ints_t.to_int y)) ik in
@@ -1591,10 +1591,10 @@ struct
   let ge n1 n2 = of_bool (n1 >= n2)
   let eq n1 n2 = of_bool (n1 =  n2)
   let ne n1 n2 = of_bool (n1 <> n2)
-  let bitnot = Ints_t.bitnot
-  let bitand = Ints_t.bitand
-  let bitor  = Ints_t.bitor
-  let bitxor = Ints_t.bitxor
+  let lognot = Ints_t.lognot
+  let logand = Ints_t.logand
+  let logor  = Ints_t.logor
+  let logxor = Ints_t.logxor
   let shift_left  n1 n2 = Ints_t.shift_left n1 (Ints_t.to_int n2)
   let shift_right n1 n2 = Ints_t.shift_right n1 (Ints_t.to_int n2)
   let c_lognot n1    = of_bool (not (to_bool' n1))
@@ -1682,10 +1682,10 @@ struct
   let ge = lift2 Base.ge
   let eq = lift2 Base.eq
   let ne = lift2 Base.ne
-  let bitnot = lift1 Base.bitnot
-  let bitand = lift2 Base.bitand
-  let bitor  = lift2 Base.bitor
-  let bitxor = lift2 Base.bitxor
+  let lognot = lift1 Base.lognot
+  let logand = lift2 Base.logand
+  let logor  = lift2 Base.logor
+  let logxor = lift2 Base.logxor
   let shift_left  = lift2 Base.shift_left
   let shift_right = lift2 Base.shift_right
   let c_lognot = lift1 Base.c_lognot
@@ -1749,10 +1749,10 @@ struct
   let ge = lift2 Base.ge
   let eq = lift2 Base.eq
   let ne = lift2 Base.ne
-  let bitnot = lift1 Base.bitnot
-  let bitand = lift2 Base.bitand
-  let bitor  = lift2 Base.bitor
-  let bitxor = lift2 Base.bitxor
+  let lognot = lift1 Base.lognot
+  let logand = lift2 Base.logand
+  let logor  = lift2 Base.logor
+  let logxor = lift2 Base.logxor
   let shift_left  = lift2 Base.shift_left
   let shift_right = lift2 Base.shift_right
   let c_lognot = lift1 Base.c_lognot
@@ -2200,9 +2200,9 @@ struct
 
   let ge ik x y = le ik y x
 
-  let bitnot = lift1 Z.lognot
+  let lognot = lift1 Z.lognot
 
-  let bitand ik x y = norm ik (match x,y with
+  let logand ik x y = norm ik (match x,y with
       (* We don't bother with exclusion sets: *)
       | `Excluded _, `Definite i ->
         (* Except in two special cases *)
@@ -2223,8 +2223,8 @@ struct
         raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
 
 
-  let bitor  = lift2 Z.logor
-  let bitxor = lift2 Z.logxor
+  let logor  = lift2 Z.logor
+  let logxor = lift2 Z.logxor
 
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     (* BigInt only accepts int as second argument for shifts; perform conversion here *)
@@ -2360,10 +2360,10 @@ struct
   let ge n1 n2 = true
   let eq n1 n2 = true
   let ne n1 n2 = true
-  let bitnot x = true
-  let bitand x y = x && y
-  let bitor  x y = x || y
-  let bitxor x y = x && not y || not x && y
+  let lognot x = true
+  let logand x y = x && y
+  let logor  x y = x || y
+  let logxor x y = x && not y || not x && y
   let shift_left  n1 n2 = n1
   let shift_right n1 n2 = n1
   let c_lognot = (not)
@@ -2570,10 +2570,10 @@ module Enums : S with type int_t = Z.t = struct
 
   let rem = lift2 Z.rem
 
-  let bitnot = lift1 Z.lognot
-  let bitand = lift2 Z.logand
-  let bitor  = lift2 Z.logor
-  let bitxor = lift2 Z.logxor
+  let lognot = lift1 Z.lognot
+  let logand = lift2 Z.logand
+  let logor  = lift2 Z.logor
+  let logxor = lift2 Z.logxor
 
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     handle_bot x y (fun () ->
@@ -3061,7 +3061,7 @@ struct
         pretty res ;
     res
 
-  let bitnot ik x = match x with
+  let lognot ik x = match x with
     | None -> None
     | Some (c, m) ->
       if (Cil.isSigned ik) then
@@ -3080,9 +3080,9 @@ struct
       if m =: Z.zero && m' =: Z.zero then Some (f c c', Z.zero)
       else top ()
 
-  let bitor ik x y = bit2 Z.logor ik x y
+  let logor ik x y = bit2 Z.logor ik x y
 
-  let bitand ik x y =  match x, y with
+  let logand ik x y =  match x, y with
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c, m), Some (c', m') ->
@@ -3096,7 +3096,7 @@ struct
       else
         top ()
 
-  let bitxor ik x y = bit2 Z.logxor ik x y
+  let logxor ik x y = bit2 Z.logxor ik x y
 
   let rem ik x y =
     match x, y with
@@ -3560,8 +3560,8 @@ module IntDomTupleImpl = struct
   let neg ?no_ov ik =
     mapovc ik {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.neg ?no_ov ik)}
 
-  let bitnot ik =
-    map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.bitnot ik)}
+  let lognot ik =
+    map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.lognot ik)}
 
   let c_lognot ik =
     map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_lognot ik)}
@@ -3674,14 +3674,14 @@ module IntDomTupleImpl = struct
   let ne ik =
     map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.ne ik)}
 
-  let bitand ik =
-    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.bitand ik)}
+  let logand ik =
+    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.logand ik)}
 
-  let bitor ik =
-    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.bitor ik)}
+  let logor ik =
+    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.logor ik)}
 
-  let bitxor ik =
-    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.bitxor ik)}
+  let logxor ik =
+    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.logxor ik)}
 
   let shift_left ik =
     map2ovc ik {f2_ovc= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.shift_left ik)}
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index ebbf8ceaf3..64295bd440 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -56,16 +56,16 @@ sig
 
   (** {b Bit operators} *)
 
-  val bitnot: t -> t
+  val lognot: t -> t
   (** Bitwise not (one's complement): [~x] *)
 
-  val bitand: t -> t -> t
+  val logand: t -> t -> t
   (** Bitwise and: [x & y] *)
 
-  val bitor : t -> t -> t
+  val logor : t -> t -> t
   (** Bitwise or: [x | y] *)
 
-  val bitxor: t -> t -> t
+  val logxor: t -> t -> t
   (** Bitwise exclusive or: [x ^ y] *)
 
   val shift_left : t -> t -> t
@@ -135,16 +135,16 @@ sig
 
   (** {b Bit operators} *)
 
-  val bitnot: Cil.ikind -> t -> t
+  val lognot: Cil.ikind -> t -> t
   (** Bitwise not (one's complement): [~x] *)
 
-  val bitand: Cil.ikind -> t -> t -> t
+  val logand: Cil.ikind -> t -> t -> t
   (** Bitwise and: [x & y] *)
 
-  val bitor : Cil.ikind -> t -> t -> t
+  val logor : Cil.ikind -> t -> t -> t
   (** Bitwise or: [x | y] *)
 
-  val bitxor: Cil.ikind -> t -> t -> t
+  val logxor: Cil.ikind -> t -> t -> t
   (** Bitwise exclusive or: [x ^ y] *)
 
   val shift_left : Cil.ikind -> t -> t -> t
diff --git a/src/common/util/intOps.ml b/src/common/util/intOps.ml
index 17df714a82..5b33751d96 100644
--- a/src/common/util/intOps.ml
+++ b/src/common/util/intOps.ml
@@ -33,10 +33,10 @@ sig
   (* Bitwise *)
   val shift_left : t -> int -> t
   val shift_right : t -> int -> t
-  val bitand : t -> t -> t
-  val bitor : t -> t -> t
-  val bitxor : t -> t -> t
-  val bitnot : t -> t
+  val logand : t -> t -> t
+  val logor : t -> t -> t
+  val logxor : t -> t -> t
+  val lognot : t -> t
 
   (* Comparison *)
   val compare : t -> t -> int
@@ -97,10 +97,10 @@ struct
 
   let shift_left = (lsl)
   let shift_right = (lsr)
-  let bitand = (land)
-  let bitor = (lor)
-  let bitxor = (lxor)
-  let bitnot = (lnot)
+  let logand = (land)
+  let logor = (lor)
+  let logxor = (lxor)
+  let lognot = (lnot)
 
 
   let compare = compare
@@ -143,11 +143,11 @@ struct
 
   let shift_left = Int32.shift_left
   let shift_right = Int32.shift_right_logical
-  let bitand = Int32.logand (* Int32 calls bitwise operations 'log' *)
-  let bitor = Int32.logor (* Int32 calls bitwise operations 'log' *)
-  let bitxor = Int32.logxor (* Int32 calls bitwise operations 'log' *)
+  let logand = Int32.logand (* Int32 calls bitwise operations 'log' *)
+  let logor = Int32.logor (* Int32 calls bitwise operations 'log' *)
+  let logxor = Int32.logxor (* Int32 calls bitwise operations 'log' *)
 
-  let bitnot = Int32.lognot (* Int32 calls bitwise operations 'log' *)
+  let lognot = Int32.lognot (* Int32 calls bitwise operations 'log' *)
 
   let compare = Int32.compare
   let equal = Int32.equal
@@ -191,11 +191,11 @@ struct
 
   let shift_left = Int64.shift_left
   let shift_right = Int64.shift_right_logical
-  let bitand = Int64.logand (* Int64 calls bitwise operations 'log' *)
-  let bitor = Int64.logor (* Int64 calls bitwise operations 'log' *)
-  let bitxor = Int64.logxor (* Int64 calls bitwise operations 'log' *)
+  let logand = Int64.logand (* Int64 calls bitwise operations 'log' *)
+  let logor = Int64.logor (* Int64 calls bitwise operations 'log' *)
+  let logxor = Int64.logxor (* Int64 calls bitwise operations 'log' *)
 
-  let bitnot = Int64.lognot (* Int64 calls bitwise operations 'log' *)
+  let lognot = Int64.lognot (* Int64 calls bitwise operations 'log' *)
 
   let compare = Int64.compare
   let equal = Int64.equal
@@ -255,10 +255,10 @@ struct
 
   let shift_left = Z.shift_left
   let shift_right = Z.shift_right
-  let bitnot = Z.lognot
-  let bitand = Z.logand
-  let bitor = Z.logor
-  let bitxor = Z.logxor
+  let lognot = Z.lognot
+  let logand = Z.logand
+  let logor = Z.logor
+  let logxor = Z.logxor
 
   let arbitrary () = QCheck.map ~rev:Z.to_int64 Z.of_int64 QCheck.int64
 end
diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml
index fcff746936..8757a16c0d 100644
--- a/src/domains/intDomainProperties.ml
+++ b/src/domains/intDomainProperties.ml
@@ -45,10 +45,10 @@ struct
   let ge = ge (Ik.ikind ())
   let eq = eq (Ik.ikind ())
   let ne = ne (Ik.ikind ())
-  let bitnot = bitnot (Ik.ikind ())
-  let bitand = bitand (Ik.ikind ())
-  let bitor = bitor (Ik.ikind ())
-  let bitxor = bitxor (Ik.ikind ())
+  let lognot = lognot (Ik.ikind ())
+  let logand = logand (Ik.ikind ())
+  let logor = logor (Ik.ikind ())
+  let logxor = logxor (Ik.ikind ())
   let shift_left = shift_left (Ik.ikind ())
   let shift_right = shift_right (Ik.ikind ())
   let c_lognot = c_lognot (Ik.ikind ())
@@ -97,10 +97,10 @@ struct
   let eq = lift2 Base.eq
   let ne = lift2 Base.ne
 
-  let bitnot = lift1 Base.bitnot
-  let bitand = lift2 Base.bitand
-  let bitor  = lift2 Base.bitor
-  let bitxor = lift2 Base.bitxor
+  let lognot = lift1 Base.lognot
+  let logand = lift2 Base.logand
+  let logor  = lift2 Base.logor
+  let logxor = lift2 Base.logxor
   let shift_left  = lift2 Base.shift_left
   let shift_right = lift2 Base.shift_right
 
@@ -133,10 +133,10 @@ struct
   let valid_eq = make_valid2 ~name:"eq" ~cond:none_bot CD.eq AD.eq
   let valid_ne = make_valid2 ~name:"ne" ~cond:none_bot CD.ne AD.ne
 
-  let valid_bitnot = make_valid1 ~name:"bitnot" ~cond:not_bot CD.bitnot AD.bitnot
-  let valid_bitand = make_valid2 ~name:"bitand" ~cond:none_bot CD.bitand AD.bitand
-  let valid_bitor = make_valid2 ~name:"bitor" ~cond:none_bot CD.bitor AD.bitor
-  let valid_bitxor = make_valid2 ~name:"bitxor" ~cond:none_bot CD.bitxor AD.bitxor
+  let valid_lognot = make_valid1 ~name:"lognot" ~cond:not_bot CD.lognot AD.lognot
+  let valid_logand = make_valid2 ~name:"logand" ~cond:none_bot CD.logand AD.logand
+  let valid_logor = make_valid2 ~name:"logor" ~cond:none_bot CD.logor AD.logor
+  let valid_logxor = make_valid2 ~name:"logxor" ~cond:none_bot CD.logxor AD.logxor
 
   let defined_shift (a, b) =
     let max_shift = Z.of_int @@ snd @@ IntDomain.Size.bits (AD.Ikind.ikind ()) in
@@ -164,10 +164,10 @@ struct
     valid_eq;
     valid_ne;
 
-    valid_bitnot;
-    valid_bitand;
-    valid_bitor;
-    valid_bitxor;
+    valid_lognot;
+    valid_logand;
+    valid_logor;
+    valid_logxor;
     valid_shift_left;
     valid_shift_right;
 
diff --git a/unittest/cdomains/intDomainTest.ml b/unittest/cdomains/intDomainTest.ml
index 7caf98a861..dfa8f88d63 100644
--- a/unittest/cdomains/intDomainTest.ml
+++ b/unittest/cdomains/intDomainTest.ml
@@ -82,12 +82,12 @@ struct
 
 
   let test_bit _ =
-    assert_equal ~printer:I.show iminus_one (I.bitnot izero);
-    assert_equal ~printer:I.show iminus_two (I.bitnot ione);
-    assert_equal ~printer:I.show i5   (I.bitand i5 i5);
-    assert_equal ~printer:I.show i4   (I.bitand i5 i4);
-    assert_equal ~printer:I.show i5   (I.bitor  i4 ione);
-    assert_equal ~printer:I.show ione (I.bitxor i4 i5);
+    assert_equal ~printer:I.show iminus_one (I.lognot izero);
+    assert_equal ~printer:I.show iminus_two (I.lognot ione);
+    assert_equal ~printer:I.show i5   (I.logand i5 i5);
+    assert_equal ~printer:I.show i4   (I.logand i5 i4);
+    assert_equal ~printer:I.show i5   (I.logor  i4 ione);
+    assert_equal ~printer:I.show ione (I.logxor i4 i5);
     assert_equal ~printer:I.show itwo (I.shift_left  ione ione );
     assert_equal ~printer:I.show ione (I.shift_left  ione izero);
     assert_equal ~printer:I.show ione (I.shift_right itwo ione);

From 018166e8f3678b9cd136a6db48483de6c9bd7251 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com>
Date: Mon, 29 Jan 2024 12:43:20 +0200
Subject: [PATCH 50/52] rename log* -> c_log*

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 src/domains/intDomainProperties.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml
index 8757a16c0d..2de416ff26 100644
--- a/src/domains/intDomainProperties.ml
+++ b/src/domains/intDomainProperties.ml
@@ -145,9 +145,9 @@ struct
   let valid_shift_left = make_valid2 ~name:"shift_left" ~cond:shift_cond CD.shift_left AD.shift_left
   let valid_shift_right = make_valid2 ~name:"shift_right" ~cond:shift_cond CD.shift_right AD.shift_right
 
-  let valid_lognot = make_valid1 ~name:"lognot" ~cond:not_bot CD.c_lognot AD.c_lognot
-  let valid_logand = make_valid2 ~name:"logand" ~cond:none_bot CD.c_logand AD.c_logand
-  let valid_logor = make_valid2 ~name:"logor" ~cond:none_bot CD.c_logor AD.c_logor
+  let valid_c_lognot = make_valid1 ~name:"c_lognot" ~cond:not_bot CD.c_lognot AD.c_lognot
+  let valid_c_logand = make_valid2 ~name:"c_logand" ~cond:none_bot CD.c_logand AD.c_logand
+  let valid_c_logor = make_valid2 ~name:"c_logor" ~cond:none_bot CD.c_logor AD.c_logor
 
   let tests = [
     valid_neg;

From 3d9997891633a710895868b5fa27ec41de0e72c2 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 29 Jan 2024 12:49:04 +0200
Subject: [PATCH 51/52] Rename valid_log* -> valid_c_log* in tests

---
 src/domains/intDomainProperties.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml
index 2de416ff26..155be6f90a 100644
--- a/src/domains/intDomainProperties.ml
+++ b/src/domains/intDomainProperties.ml
@@ -171,9 +171,9 @@ struct
     valid_shift_left;
     valid_shift_right;
 
-    valid_lognot;
-    valid_logand;
-    valid_logor
+    valid_c_lognot;
+    valid_c_logand;
+    valid_c_logor
   ]
 end
 

From 67320d479c521f27e27541997e01863985aa4e37 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 29 Jan 2024 13:00:05 +0200
Subject: [PATCH 52/52] Update and add comments about log* functions

---
 src/cdomain/value/cdomains/intDomain.mli | 10 +++++-----
 src/common/util/intOps.ml                |  6 ++++++
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index 64295bd440..632128ff72 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -54,19 +54,19 @@ sig
   (** Not equal to: [x != y] *)
 
 
-  (** {b Bit operators} *)
+  (** {b Bitwise logical operators} *)
 
   val lognot: t -> t
-  (** Bitwise not (one's complement): [~x] *)
+  (** Bitwise logical not (one's complement): [~x] *)
 
   val logand: t -> t -> t
-  (** Bitwise and: [x & y] *)
+  (** Bitwise logical and: [x & y] *)
 
   val logor : t -> t -> t
-  (** Bitwise or: [x | y] *)
+  (** Bitwise logical or: [x | y] *)
 
   val logxor: t -> t -> t
-  (** Bitwise exclusive or: [x ^ y] *)
+  (** Bitwise logical exclusive or: [x ^ y] *)
 
   val shift_left : t -> t -> t
   (** Shifting bits left: [x << y] *)
diff --git a/src/common/util/intOps.ml b/src/common/util/intOps.ml
index 5b33751d96..fa9a96f465 100644
--- a/src/common/util/intOps.ml
+++ b/src/common/util/intOps.ml
@@ -32,11 +32,17 @@ sig
 
   (* Bitwise *)
   val shift_left : t -> int -> t
+  (* shift_left x y shifts x to the left by y bits. *)
   val shift_right : t -> int -> t
+  (* shift_right x y shifts x to the right by y bits. *)
   val logand : t -> t -> t
+  (* Bitwise logical and. *)
   val logor : t -> t -> t
+  (* Bitwise logical or. *)
   val logxor : t -> t -> t
+  (* Bitwise logical exclusive or. *)
   val lognot : t -> t
+  (* Bitwise logical negation. *)
 
   (* Comparison *)
   val compare : t -> t -> int