Commit f36c3828 authored by David Bühler's avatar David Bühler

[Ival] The small_cardinal limit is only set once in int_set.

Int_val uses the limit provided by int_set.get_small_cardinal to create
sets or intervals.
parent ff44491d
...@@ -25,6 +25,7 @@ open Bottom.Type ...@@ -25,6 +25,7 @@ open Bottom.Type
(* Make sure all this is synchronized with the default value of -ilevel *) (* Make sure all this is synchronized with the default value of -ilevel *)
let small_cardinal = ref 8 let small_cardinal = ref 8
let get_small_cardinal () = !small_cardinal
let set_small_cardinal i = small_cardinal := i let set_small_cardinal i = small_cardinal := i
let debug_cardinal = false let debug_cardinal = false
......
...@@ -87,5 +87,7 @@ val subdivide: t -> t * t ...@@ -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. *) (* This is used by the Value plugin. Do not use. *)
val set_small_cardinal: int -> unit val set_small_cardinal: int -> unit
...@@ -23,29 +23,12 @@ ...@@ -23,29 +23,12 @@
open Abstract_interp open Abstract_interp
open Bottom.Type open Bottom.Type
(* Make sure all this is synchronized with the default value of -ilevel *) let small_cardinal = Int_set.get_small_cardinal
let small_cardinal = ref 8 let small_cardinal_Int () = Int.of_int (small_cardinal ())
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 emitter = Lattice_messages.register "Int_val" let emitter = Lattice_messages.register "Int_val"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s let log_imprecision s = Lattice_messages.emit_imprecision emitter s
module Widen_Hints = Datatype.Integer.Set module Widen_Hints = Datatype.Integer.Set
type size_widen_hint = Integer.t type size_widen_hint = Integer.t
type generic_widen_hint = Widen_Hints.t type generic_widen_hint = Widen_Hints.t
...@@ -144,7 +127,7 @@ let make ~min ~max ~rem ~modu = ...@@ -144,7 +127,7 @@ let make ~min ~max ~rem ~modu =
then inject_singleton mn then inject_singleton mn
else else
let l = Int.succ (Int.e_div (Int.sub mx mn) modu) in 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 then
let l = Int.to_int l in let l = Int.to_int l in
let s = Array.make l Int.zero in let s = Array.make l Int.zero in
...@@ -190,7 +173,7 @@ let inject_itv i = ...@@ -190,7 +173,7 @@ let inject_itv i =
match Int_interval.cardinal i with match Int_interval.cardinal i with
| None -> Itv i | None -> Itv i
| Some card -> | Some card ->
if Int.le card !small_cardinal_Int if Int.le card (small_cardinal_Int ())
then then
let min, max, rem, modu = Int_interval.min_max_rem_modu i in let min, max, rem, modu = Int_interval.min_max_rem_modu i in
make ~min ~max ~rem ~modu make ~min ~max ~rem ~modu
...@@ -365,18 +348,19 @@ let diff_if_one value rem = ...@@ -365,18 +348,19 @@ let diff_if_one value rem =
| _, Some mx when Int.equal v mx -> | _, Some mx when Int.equal v mx ->
check_make_or_bottom ~min ~max:(Some (Int.sub mx modu)) ~rem ~modu check_make_or_bottom ~min ~max:(Some (Int.sub mx modu)) ~rem ~modu
| Some mn, Some mx when | 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 -> && Int_interval.mem v i ->
let r = ref mn in let r = ref mn in
let small_cardinal = small_cardinal () in
let array = let array =
Array.init !small_cardinal Array.init small_cardinal
(fun _ -> (fun _ ->
let c = !r in let c = !r in
let corrected_c = if Int.equal c v then Int.add c modu else c in let corrected_c = if Int.equal c v then Int.add c modu else c in
r := Int.add corrected_c modu; r := Int.add corrected_c modu;
corrected_c) corrected_c)
in in
`Value (Set (Int_set.inject_array array !small_cardinal)) `Value (Set (Int_set.inject_array array small_cardinal))
| _, _ -> `Value value | _, _ -> `Value value
end end
| _ -> `Value value | _ -> `Value value
...@@ -628,7 +612,7 @@ let create_all_values ~signed ~size = ...@@ -628,7 +612,7 @@ let create_all_values ~signed ~size =
in in
let min = Some min let min = Some min
and max = Some max in 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 then make ~min ~max ~rem:Int.zero ~modu:Int.one
else Itv (Int_interval.inject_range min max) else Itv (Int_interval.inject_range min max)
...@@ -977,7 +961,7 @@ struct ...@@ -977,7 +961,7 @@ struct
let acc = ref (set_bit Sign [] (r, v1, v2)) in let acc = ref (set_bit Sign [] (r, v1, v2)) in
for i = size - 1 downto Z.numbits modu - 1 do for i = size - 1 downto Z.numbits modu - 1 do
acc := List.fold_left (set_bit (Bit i)) [] !acc; 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; done;
let o = List.fold_left (fun o (r,_,_) -> O.add r o) O.empty !acc in let o = List.fold_left (fun o (r,_,_) -> O.add r o) O.empty !acc in
let cardinal = O.cardinal o in let cardinal = O.cardinal o in
......
...@@ -116,7 +116,4 @@ val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool ...@@ -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 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 val rehash: t -> t
...@@ -22,9 +22,6 @@ ...@@ -22,9 +22,6 @@
open Abstract_interp 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 emitter = Lattice_messages.register "Ival"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s let log_imprecision s = Lattice_messages.emit_imprecision emitter s
......
...@@ -305,14 +305,8 @@ val complement_int_under: size:int -> signed:bool -> t -> t Bottom.or_bottom ...@@ -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 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 *) val rehash: t -> t (* Low-level operation for demarshalling *)
(**/**) (**/**)
......
...@@ -533,7 +533,7 @@ let memset_typ_offsm_int full_typ i = ...@@ -533,7 +533,7 @@ let memset_typ_offsm_int full_typ i =
let memset_typ_offsm typ v = let memset_typ_offsm typ v =
try try
let i = V.project_ival v in 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 aux_i i offsm =
let offsm_i = memset_typ_offsm_int typ i in let offsm_i = memset_typ_offsm_int typ i in
match offsm with match offsm with
......
...@@ -259,7 +259,7 @@ let search_offsm kind ~validity ~offset offsetmap = ...@@ -259,7 +259,7 @@ let search_offsm kind ~validity ~offset offsetmap =
(* Generic function to fold a search according to a small set of integers. *) (* Generic function to fold a search according to a small set of integers. *)
let search_by_folding ival search = 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 then Ival.fold_enum (fun ival acc -> join acc (search ival)) ival empty
else search ival else search ival
......
...@@ -119,7 +119,7 @@ module Model = struct ...@@ -119,7 +119,7 @@ module Model = struct
let backward_location state _lval typ precise_loc value = let backward_location state _lval typ precise_loc value =
let size = Precise_locs.loc_size precise_loc in 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 loc = Precise_locs.imprecise_location precise_loc in
let eval_one_loc single_loc = let eval_one_loc single_loc =
let v = Cvalue.Model.find state single_loc in let v = Cvalue.Model.find state single_loc in
......
...@@ -898,7 +898,7 @@ module Make ...@@ -898,7 +898,7 @@ module Make
then Bottom.join Value.join (`Value subvalue) acc else acc then Bottom.join Value.join (`Value subvalue) acc else acc
in in
let cvalue = get_cval v 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 -> fold_enumerate upto process cvalue `Bottom >>-: fun value ->
if Value.equal v value if Value.equal v value
then valuation then valuation
......
...@@ -947,7 +947,7 @@ module ILevel = ...@@ -947,7 +947,7 @@ module ILevel =
end) end)
let () = add_precision_dep ILevel.parameter let () = add_precision_dep ILevel.parameter
let () = ILevel.add_aliases ["-val-ilevel"] 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 () = ILevel.set_range 4 256
let () = Parameter_customize.set_group precision_tuning let () = Parameter_customize.set_group precision_tuning
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment