From 9201ead0b58bcb047f523b8042df8cb9f62069c5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 30 Jan 2019 13:40:53 +0100
Subject: [PATCH] [stdlib] refactor exceptions of Integer
# Conflicts:
# src/libraries/stdlib/integer.ml
---
src/kernel_internals/typing/cabs2cil.ml | 2 +-
src/kernel_services/abstract_interp/ival.ml | 6 +--
src/kernel_services/ast_queries/cil.ml | 2 +-
src/libraries/stdlib/integer.ml | 47 +++++++------------
src/libraries/stdlib/integer.mli | 44 +++++++++--------
src/plugins/loop_analysis/loop_analysis.ml | 2 +-
src/plugins/loop_analysis/slevel_analysis.ml | 9 ++--
.../value/domains/apron/apron_domain.ok.ml | 4 +-
.../value/domains/cvalue/builtins_print_c.ml | 2 +-
.../domains/cvalue/builtins_watchpoint.ml | 2 +-
.../domains/numerors/numerors_domain.ok.ml | 2 +-
src/plugins/value/slevel/split_strategy.ml | 2 +-
src/plugins/value_types/cvalue.ml | 2 +-
src/plugins/wp/Auto.ml | 4 +-
src/plugins/wp/Cint.ml | 2 +-
src/plugins/wp/Filtering.ml | 2 +-
src/plugins/wp/GuiComposer.ml | 2 +-
src/plugins/wp/TacShift.ml | 2 +-
src/plugins/wp/Vlist.ml | 2 +-
19 files changed, 65 insertions(+), 75 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 984fef51c45..00315ab1904 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5365,7 +5365,7 @@ and isIntegerConstant ghost (aexp) : int option =
match doExp (ghost_local_env ghost) true aexp (AExp None) with
| (_, c, e, _) when isEmpty c -> begin
match Cil.constFoldToInt e with
- | Some i64 -> Some (Integer.to_int i64)
+ | Some n -> (try Some (Integer.to_int n) with Z.Overflow -> None)
| _ -> None
end
| _ -> None
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index ce2e6ad7ca7..980c2865415 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -1988,7 +1988,7 @@ let shift_aux scale op (x: t) (y: t) =
let modu = match min_factor with None -> Int.one | Some m -> m in
let factor = inject_top min_factor max_factor Int.zero modu in
op x factor
- with Integer.Too_big ->
+ with Z.Overflow ->
Lattice_messages.emit_imprecision emitter "Ival.shift_aux";
(* We only preserve the sign of the result *)
if is_included x positive_integers then positive_integers
@@ -2199,7 +2199,7 @@ let rec extract_bits ~start ~stop ~size v =
try
let dived = scale_div ~pos:true (Int.two_power start) d in
scale_rem ~pos:true (Int.two_power (Int.length start stop)) dived
- with Integer.Too_big ->
+ with Z.Overflow ->
Lattice_messages.emit_imprecision emitter "Ival.extract_bits";
top
;;
@@ -2428,7 +2428,7 @@ let cast_int_to_float_inverse_not_nan ~single_precision (min, max) =
values on each extremity. *)
let min = ceil min in
let max = floor max in
- let conv f = try Some (Integer.of_float f) with Integer.Too_big -> None in
+ let conv f = try Some (Integer.of_float f) with Z.Overflow -> None in
let r = inject_range (conv min) (conv max) in
(* Kernel.result "Cast I->F inv: %a -> %a@." pretty f pretty r; *)
r
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 86eb8420529..2d351e35a44 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5309,7 +5309,7 @@ and offsetOfFieldAcc_GCC last (fi: fieldinfo) (sofar: offsetAcc) : offsetAcc =
let sz' =
try
Integer.to_int sz
- with Failure _ ->
+ with Z.Overflow ->
raise
(SizeOfError
("Array is so long that its size can't be "
diff --git a/src/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index b8edece5d01..00fe1fc795d 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -22,25 +22,17 @@
type t = Z.t
-exception Too_big
-
let equal = Z.equal
let compare = Z.compare
-
let two_power_of_int k =
- Z.shift_left Z.one k
-
-let two_power y =
- try
- let k = Z.to_int y in
- if k > 1024 then
- (* avoid memory explosion *)
- raise Too_big
- else
- two_power_of_int k
- with Z.Overflow -> raise Too_big
+ if k > 1024 then
+ raise Z.Overflow
+ else
+ Z.shift_left Z.one k
+
+let two_power n = two_power_of_int (Z.to_int n)
let popcount = Z.popcount
@@ -78,7 +70,7 @@ let shift_left x y = Z.shift_left x (Z.to_int y)
let shift_right x y = Z.shift_right x (Z.to_int y)
let shift_right_logical x y = (* no meaning for negative value of x *)
if (Z.lt x Z.zero)
- then failwith "log_shift_right_big_int"
+ then raise (Invalid_argument "Integer.shift_right_logical")
else Z.shift_right x (Z.to_int y)
let logand = Z.logand
@@ -91,32 +83,22 @@ let ge a b = Z.compare a b >= 0
let lt a b = Z.compare a b < 0
let gt a b = Z.compare a b > 0
-
let of_int = Z.of_int
-
let of_int64 = Z.of_int64
let of_int32 = Z.of_int32
-(* Return the same exceptions as [Big_int] *)
let to_int = Big_int_Z.int_of_big_int
let to_int64 = Big_int_Z.int64_of_big_int
let to_int32 = Big_int_Z.int32_of_big_int
-let of_string s =
- try Z.of_string s
- with Invalid_argument _ ->
- (* We intentionally do NOT specify a string in the .mli, as Big_int
- raises multiple [Failure _] exceptions *)
- failwith "Integer.of_string"
+let of_string = Z.of_string
+let to_string = Z.to_string
+let of_float = Z.of_float
+let to_float = Z.to_float
let max_int64 = of_int64 Int64.max_int
let min_int64 = of_int64 Int64.min_int
-let to_string = Z.to_string
-let to_float = Z.to_float
-let of_float z =
- try Z.of_float z
- with Z.Overflow -> raise Too_big
let bdigits = [|
"0000" ; (* 0 *)
@@ -187,7 +169,6 @@ let pp_hex ?(nbits=1) ?(sep="") fmt v =
( Format.pp_print_string fmt "1x" ;
pp_digits { nbits ; sep ; bsize=16 ;
bmask = bmask_hex ; pp = pp_hex_neg } fmt 0 (Z.lognot v) )
-
let pretty ?(hexa=false) fmt v =
let rec aux v =
if gt v two_power_60 then
@@ -205,13 +186,14 @@ let pretty ?(hexa=false) fmt v =
Format.pp_print_string fmt (to_string v)
let is_one v = equal one v
-let pos_div = div
+let pos_div = div
let pos_rem = rem
let native_div = div
let divexact = Z.divexact
let div_rem = Z.div_rem
+(*
let _c_div u v =
let bad_div = div u v in
if (lt u zero) && not (is_zero (rem u v))
@@ -231,9 +213,11 @@ let _c_div u v =
Z.sprint res
Z.sprint res2)
else res2
+*)
let c_div = Z.div
+(*
let _c_rem u v =
sub u (mul v (c_div u v))
@@ -247,6 +231,7 @@ let _c_rem u v =
Z.sprint res
Z.sprint res2)
else res2
+*)
let c_rem = Z.rem
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index e57173cb7e6..3b9e69a8fd2 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -25,9 +25,6 @@
type t = Z.t
-exception Too_big (** Produced by values whose physical representation is too
- costly (e.g. in terms of memory usage). *)
-
val equal : t -> t -> bool
val compare : t -> t -> int
@@ -41,8 +38,14 @@ val sub : t -> t -> t
val mul : t -> t -> t
val shift_left : t -> t -> t
+(** @raise Invalid_argument if second argument (count) is negative *)
+
val shift_right : t -> t -> t
+(** @raise Invalid_argument if second argument (count) is negative *)
+
val shift_right_logical : t -> t -> t
+(** @raise Invalid_argument if any argument is negative *)
+
val logand : t -> t -> t
val logor : t -> t -> t
val logxor : t -> t -> t
@@ -52,24 +55,31 @@ val min : t -> t -> t
val max : t -> t -> t
val native_div : t -> t -> t
+
val div : t -> t -> t
(** Euclidean division (that returns a positive rem) *)
+
val pos_div : t -> t -> t
(** Euclidean division. Equivalent to C division if both operands are positive.
Equivalent to a floored division if b > 0 (rounds downwards),
otherwise rounds upwards.
Note: it is possible that pos_div (-a) b <> pos_div a (-b). *)
+
val divexact: t -> t -> t
(** Faster, but produces correct results only when b evenly divides a. *)
+
val c_div : t -> t -> t
(** Truncated division towards 0 (like in C99) *)
val rem : t -> t -> t
(** Remainder of the Euclidean division (always positive) *)
+
val c_rem : t -> t -> t
(** Remainder of the truncated division towards 0 (like in C99) *)
+
val div_rem: t -> t -> (t * t)
(** [div_rem a b] returns [(pos_div a b, pos_rem a b)] *)
+
val pos_rem : t -> t -> t
(** Remainder of the Euclidean division (always positive) *)
@@ -79,9 +89,6 @@ val pgcd : t -> t -> t
val ppcm : t -> t -> t
(** [ppcm v 0 == ppcm 0 v == 0]. Result is always positive *)
-val power_int_positive_int: int -> int -> t
-(** Exponentiation *)
-
val cast: size:t -> signed:bool -> value:t -> t
val abs : t -> t
@@ -113,16 +120,13 @@ val length : t -> t -> t (** b - a + 1 *)
val of_int : int -> t
val of_int64 : Int64.t -> t
val of_int32 : Int32.t -> t
-val to_int64 : t -> int64
-val to_int32 : t -> int32
-val to_int : t -> int
-(** @raise Failure if the argument does not fit in an OCaml int *)
+val to_int : t -> int (** @raise Z.Overflow if too big *)
+val to_int64 : t -> int64 (** @raise Z.Overflow if too big *)
+val to_int32 : t -> int32 (** @raise Z.Overflow if too big *)
val to_float : t -> float
val of_float : float -> t
-(** Converts from a floating-point value. The value is truncated.
- Raises [Overflow] on infinity and NaN arguments. *)
val round_up_to_r : min:t -> r:t -> modu:t -> t
(** [round_up_to_r m r modu] is the smallest number [n] such that
@@ -133,20 +137,22 @@ val round_down_to_r : max:t -> r:t -> modu:t -> t
[n]<=[m] and [n] = [r] modulo [modu] *)
val two_power : t -> t
-(** [two_power x] computes 2^x. Can raise [Too_big]. *)
+(** [two_power x] computes 2^x.
+ @raise Z.Overflow for exponents greater than 1024 *)
+
val two_power_of_int : int -> t
(** Similar to [two_power x], but x is an OCaml int. *)
-val extract_bits : start:t -> stop:t -> t -> t
+val power_int_positive_int: int -> int -> t
+(** Exponentiation *)
+val extract_bits : start:t -> stop:t -> t -> t
+val popcount: t -> int
val hash : t -> int
-val of_string : string -> t
-(** @raise Failure _ when the string cannot be parsed. *)
-
val to_string : t -> string
-
-val popcount: t -> int
+val of_string : string -> t
+(** @raise Invalid_argument when the string cannot be parsed. *)
val pretty : ?hexa:bool -> t Pretty_utils.formatter
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index de7974e693b..9236b5240a4 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -462,7 +462,7 @@ module Store(* (B:sig *)
success := true;
add_loop_bound stmt adjusted_value
end
- with Failure _ -> (* overflow in Integer.to_int *)
+ with Z.Overflow -> (* overflow in Integer.to_int *)
()
(* TODO: check if this is useful and does not cause false alarms
else
diff --git a/src/plugins/loop_analysis/slevel_analysis.ml b/src/plugins/loop_analysis/slevel_analysis.ml
index 26625cfa02d..898570e1999 100644
--- a/src/plugins/loop_analysis/slevel_analysis.ml
+++ b/src/plugins/loop_analysis/slevel_analysis.ml
@@ -123,9 +123,9 @@ module Specific(KF:sig val kf: Kernel_function.t end) = struct
then Some result
else raise Exit
with
- | Invalid_argument _ (* Possible exponent too big *)
- | Failure _ (* Integer too big *)
- | Exit -> (* Above MaxIterations. *)
+ | Invalid_argument _ (* Possible negative exponent *)
+ | Z.Overflow (* Integer too big *)
+ | Exit -> (* Above MaxIterations. *)
update_max_slevel_encountered
(Some (Integer.mul entry (Integer.mul in_loop
(Integer.of_int max_iteration))));
@@ -197,8 +197,7 @@ module SpecificNoBranches(KF:sig val kf: Kernel_function.t end) = struct
Some Integer.(pred (mul (succ (of_int in_loop_i))
(of_int max_iteration)))
with
- | Invalid_argument _ (* Possible exponent too big *)
- | Failure _ (* Integer too big *)
+ | Z.Overflow (* Integer too big *)
-> update_max_slevel_encountered
(Some (Integer.mul entry (Integer.mul in_loop
(Integer.of_int max_iteration))));
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ok.ml
index 6c7817dff14..27aa29d81c1 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ok.ml
@@ -252,7 +252,7 @@ let translate_lval = function
let translate_constant = function
| CInt64 (i, _, _) -> begin
try Coeff.s_of_int (Integer.to_int i) (* TODO: skip OCaml int type *)
- with Failure _ -> raise (Out_of_Scope "translate_constant big int")
+ with Z.Overflow | Failure _ -> raise (Out_of_Scope "translate_constant big int")
end
| _ -> raise (Out_of_Scope "translate_constant not integer")
@@ -501,7 +501,7 @@ module Make
(* May happen when evaluating an expression in the GUI, while the states
of Apron have not been saved. In this case, we evaluate in the top
apron state, whose environment raises the Failure exception. *)
- | Failure _ -> top
+ | Z.Overflow | Failure _ -> top
let extract_expr _oracle state expr =
compute state expr (Cil.typeOf expr)
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index f3279278605..dc13b3c198b 100644
--- a/src/plugins/value/domains/cvalue/builtins_print_c.ml
+++ b/src/plugins/value/domains/cvalue/builtins_print_c.ml
@@ -280,7 +280,7 @@ let state_pretty cas fmt m =
begin
try offsetmap_pretty cas name print_ampamp fmt offs
with
- | Failure _
+ | Z.Overflow
| Too_large_to_enumerate ->
Value_parameters.warning "base %s too large, \
will not print it" name
diff --git a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index fbebe367bbf..c8a2c01c806 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -89,7 +89,7 @@ let make_watch_cardinal target_value =
let target_value = Cvalue.V.project_ival target_value in
Cardinal (Integer.to_int (Ival.project_int target_value))
with V.Not_based_on_null | Ival.Not_Singleton_Int
- | Failure _ (* from Integer.to_int *) ->
+ | Z.Overflow (* from Integer.to_int *) ->
raise Db.Value.Outside_builtin_possibilities
let () =
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
index daf171d6528..c385ee3a1f3 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ok.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
@@ -110,7 +110,7 @@ let add_numerors_value (module Value: Abstract_value.Internal) =
Numerors_value.of_ints ~prec min max
| _, _ -> num
(* Integer.to_int may fail for too big integers. *)
- with Cvalue.V.Not_based_on_null | Failure _ -> num
+ with Cvalue.V.Not_based_on_null | Z.Overflow -> num
end
| _, _ -> num
in
diff --git a/src/plugins/value/slevel/split_strategy.ml b/src/plugins/value/slevel/split_strategy.ml
index cc8b20271d9..9ab22e48e56 100644
--- a/src/plugins/value/slevel/split_strategy.ml
+++ b/src/plugins/value/slevel/split_strategy.ml
@@ -80,7 +80,7 @@ let of_string s =
let r = Str.regexp ":" in
let conv s =
try Integer.of_string s
- with Failure _ -> raise (ParseFailure s)
+ with Invalid_argument _ -> raise (ParseFailure s)
in SplitEqList (List.map conv (Str.split r s))
let to_string = function
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 86e61503023..0801bc27aea 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -635,7 +635,7 @@ module V = struct
if Integer.is_zero factor
then v
else topify_with_origin_kind topify v
- | Integer.Too_big -> top_int
+ | Z.Overflow -> top_int
let restrict_topint_to_size value size =
if is_topint value
diff --git a/src/plugins/wp/Auto.ml b/src/plugins/wp/Auto.ml
index c06565117db..86d62474d95 100644
--- a/src/plugins/wp/Auto.ml
+++ b/src/plugins/wp/Auto.ml
@@ -162,12 +162,12 @@ struct
Tmap.interf
(fun _ a b ->
try Some(Integer.to_int a,Integer.to_int b)
- with Integer.Too_big -> None
+ with Z.Overflow -> None
) rg.vmin rg.vmax
let small = function
| None -> None
- | Some z -> try Some(Integer.to_int z) with Integer.Too_big -> None
+ | Some z -> try Some(Integer.to_int z) with Z.Overflow -> None
let bounds rg =
Tmap.merge
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 763bd314ff3..462cf49b991 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -621,7 +621,7 @@ let smp_eq_with_lnot a b = (* b1==~e <==> ~b1==e *)
let two_power_k_minus1 k =
try Integer.pred (Integer.two_power k)
- with Integer.Too_big -> raise Not_found
+ with Z.Overflow -> raise Not_found
let smp_eq_with_lsl_cst a0 b0 =
let b1 = match_integer b0 in
diff --git a/src/plugins/wp/Filtering.ml b/src/plugins/wp/Filtering.ml
index a74546d4d09..adf5bbd3177 100644
--- a/src/plugins/wp/Filtering.ml
+++ b/src/plugins/wp/Filtering.ml
@@ -211,7 +211,7 @@ struct
begin match F.repr k with
| Kint z ->
let d =
- try Dindex(Integer.to_int z) with Integer.Too_big -> Darray in
+ try Dindex(Integer.to_int z) with Z.Overflow -> Darray in
X( x , ds @ [ d ] )
| _ ->
let ds = ds @ [ Darray ] in
diff --git a/src/plugins/wp/GuiComposer.ml b/src/plugins/wp/GuiComposer.ml
index a50bd4ab9ef..779d9f467f7 100644
--- a/src/plugins/wp/GuiComposer.ml
+++ b/src/plugins/wp/GuiComposer.ml
@@ -91,7 +91,7 @@ class composer (focused : GuiSequent.focused) =
method private get_int = function
| Tactical.Compose(Tactical.Cint z) ->
- (try Some (Integer.to_int z) with _ -> None)
+ (try Some (Integer.to_int z) with Z.Overflow -> None)
| _ -> None
method private op1 title job args fmt = match args with
diff --git a/src/plugins/wp/TacShift.ml b/src/plugins/wp/TacShift.ml
index 7f5cfe3bc98..f0ac610edab 100644
--- a/src/plugins/wp/TacShift.ml
+++ b/src/plugins/wp/TacShift.ml
@@ -47,7 +47,7 @@ let select_op f =
let select_int n =
match F.repr n with
| Qed.Logic.Kint n ->
- (try Integer.to_int n with Integer.Too_big -> raise Not_found)
+ (try Integer.to_int n with Z.Overflow -> raise Not_found)
| _ -> raise Not_found
class shift =
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 0f41386b7f6..40bdc019497 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -160,7 +160,7 @@ and get_nth_list k = function
let rewrite_nth s k =
match F.repr k with
| L.Kint z ->
- let k = try Integer.to_int z with _ -> raise Not_found in
+ let k = try Integer.to_int z with Z.Overflow -> raise Not_found in
if 0 <= k then get_nth k s else raise Not_found
| _ -> raise Not_found
--
GitLab