[Eva] Ival: implements the absolute value of integers.

src/kernel_services/abstract_interp/int_interval.ml

@@ -482,6 +482,20 @@ let neg t =
     ~rem:(Int.e_rem (Int.neg t.rem) t.modu)
     ~modu:t.modu
 
+let abs t =
+  match t.min, t.max with
+  | Some mn, _ when Int.(ge mn zero) -> t
+  | _, Some mx when Int.(le mx zero) -> neg t
+  | _, _ ->
+    let max =
+      match t.min, t.max with
+      | Some mn, Some mx -> Some (Int.(max (neg mn) mx))
+      | _, _ -> None
+    in
+    let modu = Int.(pgcd t.modu (add t.rem t.rem)) in
+    let rem = Int.e_rem t.rem modu in
+    build_interval ~min:(Some Int.zero) ~max ~rem ~modu
+
 type ext_value = Ninf | Pinf | Val of Int.t
 let inject_min = function None -> Ninf | Some m -> Val m
 let inject_max = function None -> Pinf | Some m -> Val m

src/kernel_services/abstract_interp/int_interval.mli

@@ -77,6 +77,7 @@ val add_singleton_int: Integer.t -> t -> t
 val add: t -> t -> t
 val add_under: t -> t -> t or_bottom
 val neg: t -> t
+val abs: t -> t
 
 val scale: Integer.t -> t -> t
 val scale_div: pos:bool -> Integer.t -> t -> t

src/kernel_services/abstract_interp/int_set.ml

@@ -604,6 +604,13 @@ let add_under s1 s2 =
 
 let neg s = map_set_strict_decr Int.neg s
 
+let abs s =
+  if Int.(ge s.(0) zero)
+  then s
+  else if Int.(le s.(Array.length s - 1) zero)
+  then neg s
+  else map Int.abs s
+
 let scale f s =
   if Int.ge f Int.zero
   then apply_bin_1_strict_incr Int.mul f s

src/kernel_services/abstract_interp/int_set.mli

@@ -117,6 +117,7 @@ val add_singleton: Integer.t -> t -> t
 val add: t -> t -> set_or_top
 val add_under: t -> t -> set_or_top
 val neg: t -> t
+val abs: t -> t
 
 val mul: t -> t -> set_or_top
 val c_rem: t -> t -> set_or_top_or_bottom

src/kernel_services/abstract_interp/int_val.ml

@@ -436,6 +436,10 @@ let neg = function
   | Set s -> Set (Int_set.neg s)
   | Itv i -> Itv (Int_interval.neg i)
 
+let abs = function
+  | Set s -> Set (Int_set.abs s)
+  | Itv i -> inject_itv (Int_interval.abs i)
+
 
 let scale f v =
   if Int.is_zero f

src/kernel_services/abstract_interp/int_val.mli

@@ -126,6 +126,9 @@ val add_singleton: Integer.t -> t -> t
 val neg: t -> t
 (** Negation of an integer abstraction. *)
 
+val abs: t -> t
+(** Absolute value of an integer abstraction. *)
+
 val scale: Integer.t -> t -> t
 (** [scale f v] returns an abstraction of the integers [f * x]
     for all [x] in [v]. This operation is exact. *)

src/kernel_services/abstract_interp/ival.ml

@@ -445,6 +445,11 @@ let neg_int = function
   | Float _ -> assert false
   | Int i -> inject_int (Int_val.neg i)
 
+let abs_int = function
+  | Bottom -> bottom
+  | Float _ -> assert false
+  | Int i -> inject_int (Int_val.abs i)
+
 let sub_int v1 v2 = add_int v1 (neg_int v2)
 let sub_int_under v1 v2 = add_int_under v1 (neg_int v2)
 

src/kernel_services/abstract_interp/ival.mli

@@ -63,6 +63,8 @@ val add_singleton_int: Integer.t -> t -> t
 
 val neg_int : t -> t
 (** Negation of an integer ival. Exact operation. *)
+val abs_int: t -> t
+(** Absolute value of an integer. *)
 val sub_int : t -> t -> t
 val sub_int_under: t -> t -> t