diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 939ba512de44751aea72b1cf9c7dfb6463928b37..e25a29851d9a2d06535cb4c5637ab1a05273bbbe 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -25,6 +25,7 @@ open Bottom.Type
(* Make sure all this is synchronized with the default value of -ilevel *)
let small_cardinal = ref 8
+let get_small_cardinal () = !small_cardinal
let set_small_cardinal i = small_cardinal := i
let debug_cardinal = false
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
index 2d46b7372e848f3d8c7741758519cb542fbfd31e..3e91a938f6dcaa9a27ca313e4bd0ea1e992b7ed2 100644
--- a/src/kernel_services/abstract_interp/int_set.mli
+++ b/src/kernel_services/abstract_interp/int_set.mli
@@ -87,5 +87,7 @@ val subdivide: t -> t * t
(**/**)
+val get_small_cardinal: unit -> int
+
(* This is used by the Value plugin. Do not use. *)
val set_small_cardinal: int -> unit
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 5c0e42071ba5f69fa9c43adf113b2900a41918df..e635e2008e91a387f77af0b0bd3094c91b17c960 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -23,29 +23,12 @@
open Abstract_interp
open Bottom.Type
-(* Make sure all this is synchronized with the default value of -ilevel *)
-let small_cardinal = ref 8
-let small_cardinal_Int = ref (Int.of_int !small_cardinal)
-let small_cardinal_log = ref 3
-
-let set_small_cardinal i =
- assert (2 <= i && i <= 1024);
- let rec log j p =
- if i <= p then j
- else log (j+1) (2*p)
- in
- small_cardinal := i;
- small_cardinal_Int := Int.of_int i;
- small_cardinal_log := log 1 2;
- (* TODO: share this code with Int_set *)
- Int_set.set_small_cardinal i
-
-let get_small_cardinal () = !small_cardinal
+let small_cardinal = Int_set.get_small_cardinal
+let small_cardinal_Int () = Int.of_int (small_cardinal ())
let emitter = Lattice_messages.register "Int_val"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
module Widen_Hints = Datatype.Integer.Set
type size_widen_hint = Integer.t
type generic_widen_hint = Widen_Hints.t
@@ -144,7 +127,7 @@ let make ~min ~max ~rem ~modu =
then inject_singleton mn
else
let l = Int.succ (Int.e_div (Int.sub mx mn) modu) in
- if Int.le l !small_cardinal_Int
+ if Int.le l (small_cardinal_Int ())
then
let l = Int.to_int l in
let s = Array.make l Int.zero in
@@ -190,7 +173,7 @@ let inject_itv i =
match Int_interval.cardinal i with
| None -> Itv i
| Some card ->
- if Int.le card !small_cardinal_Int
+ if Int.le card (small_cardinal_Int ())
then
let min, max, rem, modu = Int_interval.min_max_rem_modu i in
make ~min ~max ~rem ~modu
@@ -365,18 +348,19 @@ let diff_if_one value rem =
| _, Some mx when Int.equal v mx ->
check_make_or_bottom ~min ~max:(Some (Int.sub mx modu)) ~rem ~modu
| Some mn, Some mx when
- Int.equal (Int.sub mx mn) (Int.mul modu !small_cardinal_Int)
+ Int.equal (Int.sub mx mn) (Int.mul modu (small_cardinal_Int ()))
&& Int_interval.mem v i ->
let r = ref mn in
+ let small_cardinal = small_cardinal () in
let array =
- Array.init !small_cardinal
+ Array.init small_cardinal
(fun _ ->
let c = !r in
let corrected_c = if Int.equal c v then Int.add c modu else c in
r := Int.add corrected_c modu;
corrected_c)
in
- `Value (Set (Int_set.inject_array array !small_cardinal))
+ `Value (Set (Int_set.inject_array array small_cardinal))
| _, _ -> `Value value
end
| _ -> `Value value
@@ -628,7 +612,7 @@ let create_all_values ~signed ~size =
in
let min = Some min
and max = Some max in
- if size <= !small_cardinal_log
+ if size < Z.numbits (small_cardinal_Int ())
then make ~min ~max ~rem:Int.zero ~modu:Int.one
else Itv (Int_interval.inject_range min max)
@@ -977,7 +961,7 @@ struct
let acc = ref (set_bit Sign [] (r, v1, v2)) in
for i = size - 1 downto Z.numbits modu - 1 do
acc := List.fold_left (set_bit (Bit i)) [] !acc;
- if List.length !acc > !small_cardinal then raise Do_not_fit_small_sets
+ if List.length !acc > small_cardinal () then raise Do_not_fit_small_sets
done;
let o = List.fold_left (fun o (r,_,_) -> O.add r o) O.empty !acc in
let cardinal = O.cardinal o in
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index b34085584d5b3c95d1dca04a50aeeaa37b6c5d49..45a8be77630079233468c80625f61b0a3c0016f5 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -116,7 +116,4 @@ val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool
val fold_int : (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
-val get_small_cardinal: unit -> int
-val set_small_cardinal: int -> unit
-
val rehash: t -> t
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index dbd3121a495afe922fea93dc511bd49313007816..7437373792e45c16b8a8a63b4f6c4bf15f876142 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -22,9 +22,6 @@
open Abstract_interp
-let set_small_cardinal i = Int_val.set_small_cardinal i
-let get_small_cardinal = Int_val.get_small_cardinal
-
let emitter = Lattice_messages.register "Ival"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index 0d80851635bd9e525e99684884b216d45a94372c..2e179f6f6086965770c256bee127320a8a5de988 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -305,14 +305,8 @@ val complement_int_under: size:int -> signed:bool -> t -> t Bottom.or_bottom
val pretty_debug : Format.formatter -> t -> unit
-val get_small_cardinal: unit -> int
-(** Value of option -ilevel *)
-
(**/**)
-(* This is used by the Value plugin. Do not use. *)
-val set_small_cardinal: int -> unit
-
val rehash: t -> t (* Low-level operation for demarshalling *)
(**/**)
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index 3039c1f9bbe17e922bb3f80b5a507fcba6211900..35c40573b1f98d056f2f86f4f001c3cb4e1d512c 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -533,7 +533,7 @@ let memset_typ_offsm_int full_typ i =
let memset_typ_offsm typ v =
try
let i = V.project_ival v in
- ignore (Ival.cardinal_less_than i (Ival.get_small_cardinal ()));
+ ignore (Ival.cardinal_less_than i (Int_set.get_small_cardinal ()));
let aux_i i offsm =
let offsm_i = memset_typ_offsm_int typ i in
match offsm with
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index e3ed961c845dea79c3c09c708f103da5d218ebb4..2c39d88a1ba0dec4b714b367d2135072004533d3 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -259,7 +259,7 @@ let search_offsm kind ~validity ~offset offsetmap =
(* Generic function to fold a search according to a small set of integers. *)
let search_by_folding ival search =
- if Ival.cardinal_is_less_than ival (Ival.get_small_cardinal ())
+ if Ival.cardinal_is_less_than ival (Int_set.get_small_cardinal ())
then Ival.fold_enum (fun ival acc -> join acc (search ival)) ival empty
else search ival
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 019f87cc0ee61fa5f2fb0ab04a5b43ce16e56256..cf96cb4f36347f7e824a6855347b5cf2db9dde27 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -119,7 +119,7 @@ module Model = struct
let backward_location state _lval typ precise_loc value =
let size = Precise_locs.loc_size precise_loc in
- let upto = succ (Ival.get_small_cardinal()) in
+ let upto = succ (Int_set.get_small_cardinal()) in
let loc = Precise_locs.imprecise_location precise_loc in
let eval_one_loc single_loc =
let v = Cvalue.Model.find state single_loc in
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 965a8ca09342731b082c8da5f775ca3712178641..893c66fae14163fbaeb6028bbd0c5caaabc31150 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -898,7 +898,7 @@ module Make
then Bottom.join Value.join (`Value subvalue) acc else acc
in
let cvalue = get_cval v in
- let upto = succ (Ival.get_small_cardinal ()) in
+ let upto = succ (Int_set.get_small_cardinal ()) in
fold_enumerate upto process cvalue `Bottom >>-: fun value ->
if Value.equal v value
then valuation
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 2c829ea382f7cea3c49c45905f714a1bc22261c3..a45ba4188c1cb01f9b82d9905db9aedc45b08956 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -947,7 +947,7 @@ module ILevel =
end)
let () = add_precision_dep ILevel.parameter
let () = ILevel.add_aliases ["-val-ilevel"]
-let () = ILevel.add_update_hook (fun _ i -> Ival.set_small_cardinal i)
+let () = ILevel.add_update_hook (fun _ i -> Int_set.set_small_cardinal i)
let () = ILevel.set_range 4 256
let () = Parameter_customize.set_group precision_tuning