[Ival] Moves cast_int into int_interval.

src/kernel_services/abstract_interp/int_interval.ml

@@ -685,6 +685,46 @@ let div x y =
 
 (* ----------------------------------- Misc --------------------------------- *)
 
+let cast ~size ~signed t =
+  let factor = Int.two_power size
+  and mask = Int.two_power (Int.pred size) in
+  let best_effort () =
+    let modu = Int.pgcd factor t.modu in
+    let rem = Int.e_rem t.rem modu in
+    let min =
+      if signed
+      then Int.round_up_to_r ~min:(Int.neg mask) ~r:rem ~modu
+      else Int.round_up_to_r ~min:Int.zero ~r:rem ~modu
+    and max =
+      if signed
+      then Int.round_down_to_r ~max:(Int.pred mask) ~r:rem ~modu
+      else Int.round_down_to_r ~max:(Int.pred factor) ~r:rem ~modu
+    in
+    make ~min:(Some min) ~max:(Some max) ~rem ~modu
+  in
+  match t.min, t.max with
+  | Some min, Some max ->
+    let not_p_factor = Int.neg factor in
+    let highbits_mn, highbits_mx =
+      if signed then
+        Int.logand (Int.add min mask) not_p_factor,
+        Int.logand (Int.add max mask) not_p_factor
+      else
+        Int.logand min not_p_factor,
+        Int.logand max not_p_factor
+    in
+    if Int.equal highbits_mn highbits_mx
+    then
+      if Int.is_zero highbits_mn
+      then t
+      else
+        let rem_f value = Int.cast ~size ~signed ~value in
+        let min, max = rem_f min, rem_f max in
+        let rem = Int.e_rem min t.modu in
+        make ~min:(Some min) ~max:(Some max) ~rem ~modu:t.modu
+    else best_effort ()
+  | _, _ -> best_effort ()
+
 let subdivide t =
   match t.min, t.max with
   | Some min, Some max ->

src/kernel_services/abstract_interp/int_interval.mli

@@ -63,6 +63,8 @@ val mul: t -> t -> t
 val div: t -> t -> t or_bottom
 val c_rem: t -> t -> t or_bottom
 
+val cast: size:Integer.t -> signed:bool -> t -> t
+
 val subdivide: t -> t * t
 
 val reduce_sign: t -> bool -> t or_bottom

src/kernel_services/abstract_interp/ival.ml

@@ -789,60 +789,18 @@ let cast_int_to_int ~size ~signed value =
   then create_all_values ~size:(Int.to_int size) ~signed
   else
     let result =
-      let factor = Int.two_power size in
-      let mask = Int.two_power (Int.pred size) in
-      let rem_f value = Int.cast ~size ~signed ~value
-      in
-      let not_p_factor = Int.neg factor in
-      let best_effort r m =
-        let modu = Int.pgcd factor m in
-        let rr = Int.e_rem r modu in
-        let min_val = Some (if signed then
-                              Int.round_up_to_r ~min:(Int.neg mask) ~r:rr ~modu
-                            else
-                              Int.round_up_to_r ~min:Int.zero ~r:rr ~modu)
-        in
-        let max_val = Some (if signed then
-                              Int.round_down_to_r ~max:(Int.pred mask) ~r:rr ~modu
-                            else
-                              Int.round_down_to_r ~max:(Int.pred factor)
-                                ~r:rr
-                                ~modu)
-        in
-        inject_top min_val max_val rr modu
-      in
       match value with
-      | Itv i->
-        begin
-          let mn, mx, r, m = Int_interval.min_max_rem_modu i in
-          match mn, mx with
-          | Some mn, Some mx ->
-            let highbits_mn,highbits_mx =
-              if signed then
-                Int.logand (Int.add mn mask) not_p_factor,
-                Int.logand (Int.add mx mask) not_p_factor
-              else
-                Int.logand mn not_p_factor, Int.logand mx not_p_factor
-            in
-            if Int.equal highbits_mn highbits_mx
-            then
-              if Int.is_zero highbits_mn
-              then value
-              else
-                let new_min = rem_f mn in
-                let new_r = Int.e_rem new_min m in
-                inject_top (Some new_min) (Some (rem_f mx)) new_r m
-            else best_effort r m
-          | _, _ -> best_effort r m
-        end
-      | Set s -> begin
-          let all =
-            create_all_values ~size:(Int.to_int size) ~signed
-          in
-          if is_included value all
-          then value
-          else Set (Int_set.map rem_f s)
-        end
+      | Itv i ->
+        inject_itv_or_bottom (`Value (Int_interval.cast ~size ~signed i))
+      | Set s ->
+        let all =
+          create_all_values ~size:(Int.to_int size) ~signed
+        in
+        if is_included value all
+        then value
+        else
+          let rem_f value = Int.cast ~size ~signed ~value in
+          Set (Int_set.map rem_f s)
       | Float _ -> assert false
     in
     (* If sharing is no longer preserved, please change Cvalue.V.cast *)