Change torg typ param to from_ik ikind param

Author: sim642

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 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
 
@@ -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

@@ -241,10 +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
+  val cast_to : ?suppress_ovwarn:bool -> kind:castkind -> ?from_ik:Cil.ikind -> ?no_ov:bool -> Cil.ikind -> t -> t
   (** Cast to {!Cil.ikind}.
       The function is also called to handle overflow/wraparound after operations.
-      @param torg Only present for actual casts, missing for overflow/wraparound (where the type stays the same).
+      @param from_ik Only present for actual casts, missing for overflow/wraparound (where the type stays the same).
       @param no_ov If true, assume no overflow can occur. *)
 
   val join: Cil.ikind -> t ->  t -> t
@@ -303,10 +303,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 to {!Cil.ikind}.
       The function is also called to handle overflow/wraparound after operations.
-      @param torg Only present for actual casts, missing for overflow/wraparound (where the type stays the same).
+      @param from_ik Only present for actual casts, missing for overflow/wraparound (where the type stays the same).
       @param no_ov If true, assume no overflow can occur. *)
 
   val of_int : Cil.ikind -> int_t -> t * overflow_info