Merge pull request #1908 from goblint/intdomain-torg

Remove unused `torg` parameters

Author: sim642

src/analyses/base.ml

@@ -946,11 +946,8 @@ struct
         Address (AD.map array_start (eval_lv ~man st lval))
       | CastE (_, t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
       | CastE (kind, t, exp) ->
-        (let v = eval_rv ~man st exp in
-         try
-           VD.cast ~kind ~torg:(Cilfacade.typeOf exp) t v
-         with Cilfacade.TypeOfError _  ->
-           VD.cast ~kind t v)
+        let v = eval_rv ~man st exp in
+        VD.cast ~kind t v
       | SizeOf _
       | Real _
       | Imag _
@@ -2078,7 +2075,7 @@ struct
             if not (ThreadIdDomain.Thread.is_main tid) then ( (* Only non-main return constitutes an implicit pthread_exit according to man page (https://github.com/goblint/analyzer/issues/1767#issuecomment-3642590227). *)
               (* Evaluate exp and cast the resulting value to the void-pointer-type.
                  Casting to the right type here avoids precision loss on joins. *)
-              let rv = VD.cast ~kind:Internal ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in (* TODO: proper castkind *)
+              let rv = VD.cast ~kind:Internal Cil.voidPtrType rv in (* TODO: proper castkind *)
               man.sideg (V.thread tid) (G.create_thread rv)
             );
             Priv.thread_return ask (priv_getg man.global) (priv_sideg man.sideg) tid st'

src/cdomain/value/cdomains/int/bitfieldDomain.ml

@@ -263,25 +263,25 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       else
         top_of ik
 
-  let cast_to ?torg ?(no_ov=false) ik (z,o) =
+  let cast_to ?from_ik ?(no_ov=false) ik (z,o) =
     let (min_ik, max_ik) = Size.range ik in
-    let (underflow, overflow) = match torg with
+    let (underflow, overflow) = match from_ik with
       | None -> (false, false) (* ik does not change *)
-      | Some (GoblintCil.Cil.TInt (old_ik, _) | TEnum ({ekind = old_ik; _}, _)) ->
+      | Some old_ik ->
         let underflow = Z.compare (BArith.min old_ik (z,o)) min_ik < 0 in
         let overflow = Z.compare max_ik (BArith.max old_ik (z,o)) < 0 in
         (underflow, overflow)
-      | _ ->
-        let isPos = z <: Ints_t.zero in
-        let isNeg = o <: Ints_t.zero in
-        let underflow = if GoblintCil.isSigned ik then (((Ints_t.of_bigint min_ik) &: z) <>: Ints_t.zero) && isNeg else isNeg in
-        let overflow = (((!:(Ints_t.of_bigint max_ik)) &: o) <>: Ints_t.zero) && isPos in
-        (underflow, overflow)
+      (* | _ -> (* TODO: what is this case? was it always dead? *)
+           let isPos = z <: Ints_t.zero in
+           let isNeg = o <: Ints_t.zero in
+           let underflow = if GoblintCil.isSigned ik then (((Ints_t.of_bigint min_ik) &: z) <>: Ints_t.zero) && isNeg else isNeg in
+           let overflow = (((!:(Ints_t.of_bigint max_ik)) &: o) <>: Ints_t.zero) && isPos in
+           (underflow, overflow) *)
     in
     let overflow_info = {underflow; overflow} in
     (norm ~ov:(underflow || overflow) ik (z,o), overflow_info)
 
-  let cast_to ~kind ?torg ?(no_ov=false) ik (z,o) =
+  let cast_to ~kind ?from_ik ?(no_ov=false) ik (z,o) =
     if ik = GoblintCil.IBool then (
       let may_zero =
         if Ints_t.equal z BArith.one_mask then (* zero bit may be in every position (one_mask) *)
@@ -298,7 +298,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       (BArith.join may_zero may_one, {underflow=false; overflow=false})
     )
     else
-      cast_to ?torg ~no_ov ik (z,o)
+      cast_to ?from_ik ~no_ov ik (z,o)
 
   let join ik b1 b2 = norm ik @@ (BArith.join b1 b2)
 

src/cdomain/value/cdomains/int/congruenceDomain.ml

@@ -166,7 +166,7 @@ struct
     | _ -> None
 
   (* cast from original type to ikind, set to top if the value doesn't fit into the new type *)
-  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?(no_ov=false) t x =
+  let cast_to ?(suppress_ovwarn=false) ~kind ?from_ik ?(no_ov=false) t x =
     match x with
     | None -> None
     | Some (c, m) when m =: Z.zero ->
@@ -183,16 +183,16 @@ struct
         let (min_ikorg, max_ikorg) = range ikorg in
         ikorg = t || (max_t >=: max_ikorg && min_t <=: min_ikorg)
       in
-      match Option.map Cil.unrollType torg with
-      | Some (Cil.TInt (ikorg, _) | TEnum ({ekind = ikorg; _}, _)) when p ikorg ->
+      match from_ik with
+      | Some ikorg when p ikorg ->
         if M.tracing then M.trace "cong-cast" "some case";
         x
       | _ -> top ()
 
 
-  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?no_ov (t : Cil.ikind) x =
+  let cast_to ?(suppress_ovwarn=false) ~kind ?from_ik ?no_ov (t : Cil.ikind) x =
     let pretty_bool _ x = Pretty.text (string_of_bool x) in
-    let res = cast_to ~kind ?torg ?no_ov t x in
+    let res = cast_to ~kind ?from_ik ?no_ov t x in
     if M.tracing then M.trace "cong-cast" "Cast %a to %a (no_ov: %a) = %a" pretty x Cil.d_ikind t (Pretty.docOpt (pretty_bool ())) no_ov pretty res;
     res
 

src/cdomain/value/cdomains/int/defExcDomain.ml

@@ -132,7 +132,7 @@ struct
     | `Definite x -> if i = x then `Eq else `Neq
     | `Excluded (s,r) -> if S.mem i s then `Neq else `Top
 
-  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?no_ov ik = function
+  let cast_to ?(suppress_ovwarn=false) ~kind ?from_ik ?no_ov ik = function
     | `Excluded (s,r) ->
       let r' = size ik in
       if R.leq r r' then (* upcast -> no change *)

src/cdomain/value/cdomains/int/enumsDomain.ml

@@ -97,7 +97,7 @@ module Enums : S with type int_t = Z.t = struct
       if BISet.mem i x then `Neq
       else `Top
 
-  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?no_ov ik v = norm ik @@ match v with
+  let cast_to ?(suppress_ovwarn=false) ~kind ?from_ik ?no_ov ik v = norm ik @@ match v with
     | Exc (s,r) ->
       let r' = size ik in
       if R.leq r r' then (* upcast -> no change *)

src/cdomain/value/cdomains/int/intDomTuple.ml

@@ -363,8 +363,8 @@ module IntDomTupleImpl = struct
   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 ?(suppress_ovwarn=false) ~kind ?torg ?no_ov t =
-    mapovc ~suppress_ovwarn ~op:(Cast kind) t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ~kind ?torg ?no_ov t)}
+  let cast_to ?(suppress_ovwarn=false) ~kind ?from_ik ?no_ov t =
+    mapovc ~suppress_ovwarn ~op:(Cast kind) t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ~kind ?from_ik ?no_ov t)}
 
   (* fp: projections *)
   let equal_to i x =

src/cdomain/value/cdomains/int/intervalDomain.ml

@@ -138,7 +138,7 @@ struct
   let maximal = function None -> None | Some (x,y) -> Some y
   let minimal = function None -> None | Some (x,y) -> Some x
 
-  let cast_to ~kind ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)
+  let cast_to ~kind ?from_ik ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)
 
   let widen ik x y =
     match x, y with

src/cdomain/value/cdomains/int/intervalSetDomain.ml

@@ -484,7 +484,7 @@ struct
     in
     binop x y interval_rem
 
-  let cast_to ~kind ?torg ?no_ov ik x = norm_intvs ~cast:true ik x
+  let cast_to ~kind ?from_ik ?no_ov ik x = norm_intvs ~cast:true ik x
 
   (*
       narrows down the extremeties of xs if they are equal to boundary values of the ikind with (possibly) narrower values from ys

src/cdomain/value/cdomains/intDomain0.ml

@@ -234,7 +234,7 @@ struct
   let c_logand = lift2 I.c_logand
   let c_logor = lift2 I.c_logor
 
-  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ikind x = {v = I.cast_to  ~suppress_ovwarn ~kind ~torg:(TInt(x.ikind,[])) ikind x.v; ikind}
+  let cast_to ?(suppress_ovwarn=false) ~kind ikind x = {v = I.cast_to  ~suppress_ovwarn ~kind ~from_ik:x.ikind ikind x.v; ikind}
 
   let is_top_of ik x = ik = x.ikind && I.is_top_of ik x.v
 
@@ -537,7 +537,7 @@ module SOverflowUnlifter (D : SOverflow) : S2 with type int_t = D.int_t and type
 
   let neg ?no_ov ik x = fst @@ D.neg ?no_ov ik x
 
-  let cast_to ?suppress_ovwarn ~kind ?torg ?no_ov ik x = fst @@ D.cast_to ~kind ?torg ?no_ov ik x
+  let cast_to ?suppress_ovwarn ~kind ?from_ik ?no_ov ik x = fst @@ D.cast_to ~kind ?from_ik ?no_ov ik x
 
   let of_int ?suppress_ovwarn ik x = fst @@ D.of_int ik x
 
@@ -605,7 +605,7 @@ struct
   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 ?(suppress_ovwarn=false) ~kind ?torg t x =  failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "."
+  let cast_to ?(suppress_ovwarn=false) ~kind 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 *)
 end
@@ -635,7 +635,7 @@ struct
 
 
   let name () = "flat integers"
-  let cast_to ?(suppress_ovwarn=false) ~kind ?torg t = function
+  let cast_to ?(suppress_ovwarn=false) ~kind t = function
     | `Lifted x -> `Lifted (Base.cast_to ~kind t x)
     | x -> x
 
@@ -716,7 +716,7 @@ struct
   include StdTop (struct type nonrec t = t let top_of = top_of end)
 
   let name () = "lifted integers"
-  let cast_to ?(suppress_ovwarn=false) ~kind ?torg t = function
+  let cast_to ?(suppress_ovwarn=false) ~kind t = function
     | `Lifted x -> `Lifted (Base.cast_to ~kind t x)
     | x -> x
 
@@ -789,7 +789,7 @@ module SOverflowLifter (D : S) : SOverflow with type int_t = D.int_t and type t
 
   let neg ?no_ov ik x = lift @@ D.neg ?no_ov ik x
 
-  let cast_to ~kind ?torg ?no_ov ik x = lift @@ D.cast_to ~kind ?torg ?no_ov ik x
+  let cast_to ~kind ?from_ik ?no_ov ik x = lift @@ D.cast_to ~kind ?from_ik ?no_ov ik x
 
   let of_int ik x = lift @@ D.of_int ik x
 

src/cdomain/value/cdomains/intDomain_intf.ml

@@ -199,9 +199,9 @@ sig
 
   (** {b Cast} *)
 
-  val cast_to: ?suppress_ovwarn:bool -> kind:castkind -> ?torg:Cil.typ -> Cil.ikind -> t -> t
-  (** Cast from original type [torg] to integer type [Cil.ikind]. Currently, [torg] is only present for actual casts. The function is also called to handle overflows/wrap around after operations. In these cases (where the type stays the same) [torg] is None. *)
-
+  val cast_to: ?suppress_ovwarn:bool -> kind:castkind -> Cil.ikind -> t -> t
+  (** Cast to {!Cil.ikind}.
+      The function is also called to handle overflow/wraparound after operations. *)
 end
 
 (** The signature of integral value domains. They need to support all integer
@@ -241,8 +241,10 @@ sig
   val mul : ?no_ov:bool -> Cil.ikind ->  t -> t -> t
   val div : ?no_ov:bool -> Cil.ikind ->  t -> t -> t
   val neg : ?no_ov:bool -> Cil.ikind ->  t -> t
-  val cast_to : ?suppress_ovwarn:bool -> kind:castkind -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t
-  (** @param no_ov If true, assume no overflow can occur. *)
+  val cast_to : ?suppress_ovwarn:bool -> kind:castkind -> ?from_ik:Cil.ikind -> ?no_ov:bool -> Cil.ikind -> t -> t
+  (** Cast from [from_ik] (if known) to {!Cil.ikind}.
+      The function is also called to handle overflow/wraparound after operations.
+      @param no_ov If true, assume no overflow can occur. *)
 
   val join: Cil.ikind -> t ->  t -> t
   val meet: Cil.ikind -> t -> t -> t
@@ -300,7 +302,10 @@ sig
 
   val neg : ?no_ov:bool -> Cil.ikind ->  t -> t * overflow_info
 
-  val cast_to : kind:castkind -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info
+  val cast_to : kind:castkind -> ?from_ik:Cil.ikind -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info
+  (** Cast from [from_ik] (if known) to {!Cil.ikind}.
+      The function is also called to handle overflow/wraparound after operations.
+      @param no_ov If true, assume no overflow can occur. *)
 
   val of_int : Cil.ikind -> int_t -> t * overflow_info