diff --git a/src/autoTune.ml b/src/autoTune.ml index 05f651ee62..7313d95881 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -472,7 +472,7 @@ let apronOctagonOption factors file = let wideningOption factors file = - let amountConsts = List.length @@ WideningThresholds.upper_thresholds () in + let amountConsts = WideningThresholds.Thresholds.cardinal @@ ResettableLazy.force WideningThresholds.upper_thresholds in let cost = amountConsts * (factors.loops * 5 + factors.controlFlowStatements) in { value = amountConsts * (factors.loops * 5 + factors.controlFlowStatements); diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml index 61a5f2c19b..e88ddaa8ee 100644 --- a/src/cdomain/value/cdomains/intDomain0.ml +++ b/src/cdomain/value/cdomains/intDomain0.ml @@ -69,9 +69,6 @@ let should_wrap ik = not (Cil.isSigned ik) || get_string "sem.int.signed_overflo * Always false for unsigned types, true for signed types if 'sem.int.signed_overflow' is 'assume_none' *) let should_ignore_overflow ik = Cil.isSigned ik && get_string "sem.int.signed_overflow" = "assume_none" -let widening_thresholds = ResettableLazy.from_fun WideningThresholds.thresholds -let widening_thresholds_desc = ResettableLazy.from_fun (List.rev % WideningThresholds.thresholds) - type overflow_info = { overflow: bool; underflow: bool;} let set_overflow_flag ~cast ~underflow ~overflow ik = @@ -93,8 +90,6 @@ let set_overflow_flag ~cast ~underflow ~overflow ik = | false, false -> assert false let reset_lazy () = - ResettableLazy.reset widening_thresholds; - ResettableLazy.reset widening_thresholds_desc; ana_int_config.interval_threshold_widening <- None; ana_int_config.interval_narrow_by_meet <- None; ana_int_config.def_exc_widen_by_join <- None; @@ -560,26 +555,32 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct let to_int (x1, x2) = if Ints_t.equal x1 x2 then Some x1 else None + let find_thresholds lower_or_upper = + let ts = if get_interval_threshold_widening_constants () = "comparisons" then lower_or_upper else WideningThresholds.thresholds in + ResettableLazy.force ts + let upper_threshold u max_ik = - let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in let u = Ints_t.to_bigint u in let max_ik' = Ints_t.to_bigint max_ik in - let t = List.find_opt (fun x -> Z.compare u x <= 0 && Z.compare x max_ik' <= 0) ts in - BatOption.map_default Ints_t.of_bigint max_ik t + find_thresholds WideningThresholds.upper_thresholds + |> WideningThresholds.Thresholds.find_first_opt (fun x -> Z.compare u x <= 0) + |> BatOption.filter (fun x -> Z.compare x max_ik' <= 0) + |> BatOption.map_default Ints_t.of_bigint max_ik let lower_threshold l min_ik = - let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in let l = Ints_t.to_bigint l in let min_ik' = Ints_t.to_bigint min_ik in - let t = List.find_opt (fun x -> Z.compare l x >= 0 && Z.compare x min_ik' >= 0) ts in - BatOption.map_default Ints_t.of_bigint min_ik t - let is_upper_threshold u = - let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in - let u = Ints_t.to_bigint u in - List.exists (Z.equal u) ts - let is_lower_threshold l = - let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in - let l = Ints_t.to_bigint l in - List.exists (Z.equal l) ts + find_thresholds WideningThresholds.lower_thresholds + |> WideningThresholds.Thresholds.find_last_opt (fun x -> Z.compare l x >= 0) + |> BatOption.filter (fun x -> Z.compare x min_ik' >= 0) + |> BatOption.map_default Ints_t.of_bigint min_ik + + let is_threshold t ts = + let ts = find_thresholds ts in + let t = Ints_t.to_bigint t in + WideningThresholds.Thresholds.mem t ts + + let is_upper_threshold u = is_threshold u WideningThresholds.upper_thresholds + let is_lower_threshold l = is_threshold l WideningThresholds.lower_thresholds end module IntInvariant = diff --git a/src/cdomain/value/util/wideningThresholds.ml b/src/cdomain/value/util/wideningThresholds.ml index 939ed9482f..df89728a40 100644 --- a/src/cdomain/value/util/wideningThresholds.ml +++ b/src/cdomain/value/util/wideningThresholds.ml @@ -72,16 +72,13 @@ let conditional_widening_thresholds = ResettableLazy.from_fun (fun () -> let octagon = ref default_thresholds in let thisVisitor = new extractThresholdsFromConditionsVisitor(upper,lower,octagon) in visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); - Thresholds.elements !upper, List.rev (Thresholds.elements !lower), Thresholds.elements !octagon ) + !upper, !lower, !octagon) -let upper_thresholds () = - let (u,_,_) = ResettableLazy.force conditional_widening_thresholds in u +let upper_thresholds = ResettableLazy.map Tuple3.first conditional_widening_thresholds -let lower_thresholds () = - let (_,l,_) = ResettableLazy.force conditional_widening_thresholds in l +let lower_thresholds = ResettableLazy.map Tuple3.second conditional_widening_thresholds -let octagon_thresholds () = - let (_,_,o) = ResettableLazy.force conditional_widening_thresholds in o +let octagon_thresholds = ResettableLazy.map Tuple3.third conditional_widening_thresholds class extractConstantsVisitor(widening_thresholds,widening_thresholds_incl_mul2) = object @@ -105,13 +102,11 @@ let widening_thresholds = ResettableLazy.from_fun (fun () -> let set_incl_mul2 = ref Thresholds.empty in let thisVisitor = new extractConstantsVisitor(set,set_incl_mul2) in visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); - Thresholds.elements !set, Thresholds.elements !set_incl_mul2) + !set, !set_incl_mul2) -let thresholds () = - fst @@ ResettableLazy.force widening_thresholds +let thresholds = ResettableLazy.map fst widening_thresholds -let thresholds_incl_mul2 () = - snd @@ ResettableLazy.force widening_thresholds +let thresholds_incl_mul2 = ResettableLazy.map snd widening_thresholds module EH = BatHashtbl.Make (CilType.Exp) @@ -153,4 +148,9 @@ let exps = ResettableLazy.from_fun (fun () -> let reset_lazy () = ResettableLazy.reset widening_thresholds; ResettableLazy.reset conditional_widening_thresholds; - ResettableLazy.reset exps + ResettableLazy.reset exps; + ResettableLazy.reset thresholds; + ResettableLazy.reset thresholds_incl_mul2; + ResettableLazy.reset upper_thresholds; + ResettableLazy.reset lower_thresholds; + ResettableLazy.reset octagon_thresholds; diff --git a/src/cdomain/value/util/wideningThresholds.mli b/src/cdomain/value/util/wideningThresholds.mli index 69e48695dd..5ebe664f13 100644 --- a/src/cdomain/value/util/wideningThresholds.mli +++ b/src/cdomain/value/util/wideningThresholds.mli @@ -1,10 +1,12 @@ (** Widening threshold utilities. *) -val thresholds : unit -> Z.t list -val thresholds_incl_mul2 : unit -> Z.t list +module Thresholds : Set.S with type elt = Z.t + +val thresholds : Thresholds.t ResettableLazy.t +val thresholds_incl_mul2 : Thresholds.t ResettableLazy.t val exps: GoblintCil.exp list ResettableLazy.t val reset_lazy : unit -> unit -val upper_thresholds : unit -> Z.t list -val lower_thresholds : unit -> Z.t list -val octagon_thresholds : unit -> Z.t list \ No newline at end of file +val upper_thresholds : Thresholds.t ResettableLazy.t +val lower_thresholds : Thresholds.t ResettableLazy.t +val octagon_thresholds : Thresholds.t ResettableLazy.t \ No newline at end of file diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 043b728799..04d4a2eaa9 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -18,8 +18,8 @@ module M = Messages - heterogeneous environments: https://link.springer.com/chapter/10.1007%2F978-3-030-17184-1_26 (Section 4.1) *) let widening_thresholds_apron = ResettableLazy.from_fun (fun () -> - let t = if GobConfig.get_string "ana.apron.threshold_widening_constants" = "comparisons" then WideningThresholds.octagon_thresholds () else WideningThresholds.thresholds_incl_mul2 () in - let r = List.map Scalar.of_z t in + let t = if GobConfig.get_string "ana.apron.threshold_widening_constants" = "comparisons" then WideningThresholds.octagon_thresholds else WideningThresholds.thresholds_incl_mul2 in + let r = List.map Scalar.of_z (WideningThresholds.Thresholds.elements (ResettableLazy.force t)) in Array.of_list r ) diff --git a/src/common/util/resettableLazy.ml b/src/common/util/resettableLazy.ml index 0ca2575f68..acd3c44a47 100644 --- a/src/common/util/resettableLazy.ml +++ b/src/common/util/resettableLazy.ml @@ -7,3 +7,5 @@ let from_fun f = make_map ~gen:f let force cache = cache.get () let reset cache = cache.del () + +let map f cache = from_fun (fun () -> f (force cache)) diff --git a/src/common/util/resettableLazy.mli b/src/common/util/resettableLazy.mli index 5b0db478bb..a222dd376d 100644 --- a/src/common/util/resettableLazy.mli +++ b/src/common/util/resettableLazy.mli @@ -5,3 +5,4 @@ type 'a t val from_fun: (unit -> 'a) -> 'a t val force: 'a t -> 'a val reset: 'a t -> unit +val map: ('a -> 'b) -> 'a t -> 'b t