[Ival] Removes redundant checks between int_interval and int_val.

Shares the implementation of the checks between the two files.

src/kernel_services/abstract_interp/int_interval.ml

@@ -118,16 +118,15 @@ let is_safe_bound bound r modu = match bound with
   | Some m -> Int.equal (Int.e_rem m modu) r
 
 (* Sanity check. *)
-let check t =
-  if not (is_safe_modulo t.rem t.modu
-          && is_safe_bound t.min t.rem t.modu
-          && is_safe_bound t.max t.rem t.modu)
-  then fail t.min t.max t.rem t.modu
+let check ~min ~max ~rem ~modu =
+  if not (is_safe_modulo rem modu
+          && is_safe_bound min rem modu
+          && is_safe_bound max rem modu)
+  then fail min max rem modu
 
 let make ~min ~max ~rem ~modu =
-  let t = { min; max; rem; modu } in
-  check t;
-  t
+  check ~min ~max ~rem ~modu;
+  { min; max; rem; modu }
 
 let inject_singleton e =
   { min = Some e; max = Some e; rem = Int.zero; modu = Int.one }
@@ -220,8 +219,6 @@ let max_max x y =
   | Some x, Some y -> Some (Int.max x y)
 
 let join t1 t2 =
-  check t1;
-  check t2;
   let modu = Int.(pgcd (pgcd t1.modu t2.modu) (abs (sub t1.rem t2.rem))) in
   let rem = Int.e_rem t1.rem modu in
   let min = min_min t1.min t2.min in
@@ -624,8 +621,6 @@ let c_rem t1 t2 =
       `Value (inject_range min max)
 
 let mul t1 t2 =
-  check t1;
-  check t2;
   let min1 = inject_min t1.min in
   let max1 = inject_max t1.max in
   let min2 = inject_min t2.min in
@@ -784,3 +779,7 @@ let reduce_bit i t b =
     | u -> u
   in
   make_or_bottom ~min ~max ~rem:r ~modu
+
+(* No check in the exported [make] function: callers are expected to perform
+   the checks when needed. Thus the function [check] is also exported. *)
+let make ~min ~max ~rem ~modu = { min; max; rem; modu }

src/kernel_services/abstract_interp/int_interval.mli

@@ -34,6 +34,11 @@ include Eva_lattice_type.Full_AI_Lattice_with_cardinality
   with type t := t
    and type widen_hint = Integer.t * Datatype.Integer.Set.t
 
+(** Checks that the interval defined by [min, max, rem, modu] is well formed. *)
+val check:
+  min:Integer.t option -> max:Integer.t option ->
+  rem:Integer.t -> modu:Integer.t -> unit
+
 (** Makes the interval of all integers between [min] and [max] and congruent
     to [rem] modulo [modu]. Fails if these conditions does not hold:
     - min ≤ max

src/kernel_services/abstract_interp/int_val.ml

@@ -90,29 +90,6 @@ let zero_or_one = Set Int_set.zero_or_one
 let positive_integers = Itv (Int_interval.inject_range (Some Int.zero) None)
 let negative_integers = Itv (Int_interval.inject_range None (Some Int.zero))
 
-
-let fail min max r modu =
-  let bound fmt = function
-    | None -> Format.fprintf fmt "--"
-    | Some x -> Int.pretty fmt x
-  in
-  Kernel.fatal "Int_val: broken Itv, min=%a max=%a r=%a modu=%a"
-    bound min bound max Int.pretty r Int.pretty modu
-
-let is_safe_modulo r modu =
-  (Int.ge r Int.zero ) && (Int.ge modu Int.one) && (Int.lt r modu)
-
-let is_safe_bound bound r modu = match bound with
-  | None -> true
-  | Some m -> Int.equal (Int.e_rem m modu) r
-
-(* Sanity check for Itv's arguments *)
-let check ~min ~max ~rem ~modu =
-  if not (is_safe_modulo rem modu
-          && is_safe_bound min rem modu
-          && is_safe_bound max rem modu)
-  then fail min max rem modu
-
 let inject_singleton e = Set (Int_set.inject_singleton e)
 
 let make ~min ~max ~rem ~modu =
@@ -129,11 +106,11 @@ let make ~min ~max ~rem ~modu =
   | _ -> Itv (Int_interval.make ~min ~max ~rem ~modu)
 
 let check_make ~min ~max ~rem ~modu =
-  check ~min ~max ~rem ~modu;
+  Int_interval.check ~min ~max ~rem ~modu;
   make ~min ~max ~rem ~modu
 
 let inject_interval ~min ~max ~rem:r ~modu =
-  assert (is_safe_modulo r modu);
+  assert ((Int.ge r Int.zero ) && (Int.ge modu Int.one) && (Int.lt r modu));
   let fix_bound fix bound = match bound with
     | None -> None
     | Some b -> Some (if Int.equal b (Int.e_rem r modu) then b else fix b)
@@ -374,7 +351,6 @@ let join v1 v2 =
         None -> None
       | Some m -> Some (Int.max m (Int_set.max s))
     in
-    check ~min ~max ~rem ~modu;
     Itv (Int_interval.make ~min ~max ~rem ~modu)
 
 let link v1 v2 =