Use sets for widening thresholds instead of lists

Author: karoliineh

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

@@ -70,7 +70,6 @@ let should_wrap ik = not (Cil.isSigned ik) || get_string "sem.int.signed_overflo
 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;}
 
@@ -94,7 +93,6 @@ let set_overflow_flag ~cast ~underflow ~overflow ik =
 
 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;
@@ -564,22 +562,22 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
     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
+    let t = WideningThresholds.Thresholds.find_first_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
   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 ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds 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
+    let t = WideningThresholds.Thresholds.find_last_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
+    WideningThresholds.Thresholds.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 ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds in
     let l = Ints_t.to_bigint l in
-    List.exists (Z.equal l) ts
+    WideningThresholds.Thresholds.exists (Z.equal l) ts
 end
 
 module IntInvariant =

src/cdomain/value/util/wideningThresholds.ml

@@ -72,7 +72,7 @@ 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
@@ -105,7 +105,7 @@ 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

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

src/cdomains/apron/apronDomain.apron.ml

@@ -19,7 +19,7 @@ module M = Messages
 
 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 r = List.map Scalar.of_z (WideningThresholds.Thresholds.elements t) in
     Array.of_list r
   )