Merge pull request #1654 from goblint/issue-1591

Use sets for widening thresholds instead of lists

Author: sim642

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);

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 =

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;

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
+val upper_thresholds : Thresholds.t ResettableLazy.t
+val lower_thresholds : Thresholds.t ResettableLazy.t
+val octagon_thresholds : Thresholds.t ResettableLazy.t

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
   )
 

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))

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