Merge branch 'feature/eva/ival-comparisons' into 'master'

[Eva] Moves integer comparison functions from ival to int_val.

See merge request frama-c/frama-c!4334

src/kernel_services/abstract_interp/int_val.ml

@@ -543,6 +543,57 @@ let shift_right x y =
 
 let shift_left x y = shift_aux scale mul x y
 
+(* -------------------------------- Comparison ------------------------------ *)
+
+let compare_min_max min max =
+  match min, max with
+  | None, _ -> -1
+  | _, None -> -1
+  | Some min, Some max -> Int.compare min max
+
+let compare_max_min max min =
+  match max, min with
+  | None, _ -> 1
+  | _, None -> 1
+  | Some max, Some min -> Int.compare max min
+
+let forward_le_int i1 i2 =
+  if compare_max_min (max_int i1) (min_int i2) <= 0 then Comp.True
+  else if compare_min_max (min_int i1) (max_int i2) > 0 then Comp.False
+  else Comp.Unknown
+
+let forward_lt_int i1 i2 =
+  if compare_max_min (max_int i1) (min_int i2) < 0 then Comp.True
+  else if compare_min_max (min_int i1) (max_int i2) >= 0 then Comp.False
+  else Comp.Unknown
+
+let forward_eq_int i1 i2 =
+  if cardinal_zero_or_one i1 && equal i1 i2 then Comp.True
+  else if intersects i2 i2 then Comp.Unknown
+  else Comp.False
+
+let forward_comp op i1 i2 =
+  match op with
+  | Comp.Le -> forward_le_int i1 i2
+  | Comp.Ge -> forward_le_int i2 i1
+  | Comp.Lt -> forward_lt_int i1 i2
+  | Comp.Gt -> forward_lt_int i2 i1
+  | Comp.Eq -> forward_eq_int i1 i2
+  | Comp.Ne -> inv_truth (forward_eq_int i1 i2)
+
+let backward_le_int max v = narrow v (inject_range None max)
+let backward_ge_int min v = narrow v (inject_range min None)
+let backward_lt_int max v = backward_le_int (Option.map Int.pred max) v
+let backward_gt_int min v = backward_ge_int (Option.map Int.succ min) v
+
+let backward_comp_left op l r =
+  match op with
+  | Comp.Le -> backward_le_int (max_int r) l
+  | Comp.Ge -> backward_ge_int (min_int r) l
+  | Comp.Lt -> backward_lt_int (max_int r) l
+  | Comp.Gt -> backward_gt_int (min_int r) l
+  | Comp.Eq -> narrow l r
+  | Comp.Ne -> diff_if_one l r
 
 (* ----------------------------------- Misc --------------------------------- *)
 

src/kernel_services/abstract_interp/int_val.mli

@@ -163,6 +163,16 @@ val bitwise_xor: t -> t -> t
 val bitwise_signed_not: t -> t
 val bitwise_unsigned_not: size:int -> t -> t
 
+(** {2 Comparisons} *)
+
+(** [forward_comp op l r] returns the result of the comparison [l op r]. *)
+val forward_comp:
+  Abstract_interp.Comp.t -> t -> t -> Abstract_interp.Comp.result
+
+(** [backward_comp_left op l r] reduces [l] by assuming [l op r] holds. *)
+val backward_comp_left: Abstract_interp.Comp.t -> t -> t -> t or_bottom
+
+
 (** {2 Misc} *)
 
 val cast_int_to_int: size:Integer.t -> signed:bool -> t -> t

src/kernel_services/abstract_interp/ival.ml

@@ -664,22 +664,6 @@ let backward_mult_int_left ~right ~result =
                       (backward_mult_pos_left Int.one max result)
                       (backward_mult_neg_left min Int.one result)))
 
-
-let backward_le_int max v =
-  match v with
-  | Bottom -> bottom
-  | Float _ -> v
-  | Int _ -> narrow v (inject_int (Int_val.inject_range None max))
-
-let backward_ge_int min v =
-  match v with
-  | Bottom -> bottom
-  | Float _ -> v
-  | Int _ -> narrow v (inject_int (Int_val.inject_range min None))
-
-let backward_lt_int max v = backward_le_int (Option.map Int.pred max) v
-let backward_gt_int min v = backward_ge_int (Option.map Int.succ min) v
-
 let diff_if_one value rem =
   match value, rem with
   | Int i1, Int i2 -> inject_int_or_bottom (Int_val.diff_if_one i1 i2)
@@ -713,17 +697,10 @@ let fold_int_bounds f v acc =
       if equal v bottom then acc else f v acc
 
 
-let backward_comp_int_left op l r =
-  let open Comp in
-  try
-    match op with
-    | Le -> backward_le_int (max_int r) l
-    | Ge -> backward_ge_int (min_int r) l
-    | Lt -> backward_lt_int (max_int r) l
-    | Gt -> backward_gt_int (min_int r) l
-    | Eq -> narrow l r
-    | Ne -> diff_if_one l r
-  with Error_Bottom (* raised by max_int *) -> bottom
+let backward_comp_int_left op v1 v2 =
+  match v1, v2 with
+  | Int i1, Int i2 -> inject_int_or_bottom (Int_val.backward_comp_left op i1 i2)
+  | _, _ -> v1 (* No reduction *)
 
 let backward_comp_float_left_true op fkind f1 f2  =
   let f1 = project_float f1 in
@@ -770,42 +747,11 @@ let all_values ~size v =
     | Bottom | Float _ -> false
     | Int i -> Int_val.all_values ~size i
 
-let compare_min_max min max =
-  match min, max with
-  | None,_ -> -1
-  | _,None -> -1
-  | Some min, Some max -> Int.compare min max
-
-let compare_max_min max min =
-  match max, min with
-  | None,_ -> 1
-  | _,None -> 1
-  | Some max, Some min -> Int.compare max min
-
-let forward_le_int i1 i2 =
-  if compare_max_min (max_int i1) (min_int i2) <= 0 then Comp.True
-  else if compare_min_max (min_int i1) (max_int i2) > 0 then Comp.False
-  else Comp.Unknown
-
-let forward_lt_int i1 i2 =
-  if compare_max_min (max_int i1) (min_int i2) < 0 then Comp.True
-  else if compare_min_max (min_int i1) (max_int i2) >= 0 then Comp.False
-  else Comp.Unknown
-
-let forward_eq_int i1 i2 =
-  if cardinal_zero_or_one i1 && equal i1 i2 then Comp.True
-  else if intersects i2 i2 then Comp.Unknown
-  else Comp.False
-
-let forward_comp_int op i1 i2 =
-  let open Abstract_interp.Comp in
-  match op with
-  | Le -> forward_le_int i1 i2
-  | Ge -> forward_le_int i2 i1
-  | Lt -> forward_lt_int i1 i2
-  | Gt -> forward_lt_int i2 i1
-  | Eq -> forward_eq_int i1 i2
-  | Ne -> inv_truth (forward_eq_int i1 i2)
+let forward_comp_int op v1 v2 =
+  match v1, v2 with
+  | Bottom, _ | _, Bottom -> raise Error_Bottom
+  | Float _, _ | _, Float _ -> Unknown
+  | Int i1, Int i2 -> Int_val.forward_comp op i1 i2
 
 let rehash = function
   | Bottom -> bottom