Define and use ResettableLazy.map

Author: karoliineh

src/autoTune.ml

@@ -472,7 +472,7 @@ let apronOctagonOption factors file =
 
 
 let wideningOption factors file =
-  let amountConsts = WideningThresholds.Thresholds.cardinal @@ 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,8 +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
-
 type overflow_info = { overflow: bool; underflow: bool;}
 
 let set_overflow_flag ~cast ~underflow ~overflow ik =
@@ -92,7 +90,6 @@ let set_overflow_flag ~cast ~underflow ~overflow ik =
     | false, false -> assert false
 
 let reset_lazy () =
-  ResettableLazy.reset widening_thresholds;
   ana_int_config.interval_threshold_widening <- None;
   ana_int_config.interval_narrow_by_meet <- None;
   ana_int_config.def_exc_widen_by_join <- None;
@@ -559,25 +556,25 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
     if Ints_t.equal x1 x2 then Some x1 else None
 
   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 ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds else WideningThresholds.thresholds in
     let u = Ints_t.to_bigint u in
     let max_ik' = Ints_t.to_bigint max_ik in
-    let t = WideningThresholds.Thresholds.find_first_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) (ResettableLazy.force 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 in
+    let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds else WideningThresholds.thresholds in
     let l = Ints_t.to_bigint l in
     let min_ik' = Ints_t.to_bigint min_ik in
-    let t = WideningThresholds.Thresholds.find_last_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) (ResettableLazy.force 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 ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds else WideningThresholds.thresholds in
     let u = Ints_t.to_bigint u in
-    WideningThresholds.Thresholds.exists (Z.equal u) ts
+    WideningThresholds.Thresholds.exists (Z.equal u) (ResettableLazy.force ts)
   let is_lower_threshold l =
-    let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds in
+    let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds else WideningThresholds.thresholds in
     let l = Ints_t.to_bigint l in
-    WideningThresholds.Thresholds.exists (Z.equal l) ts
+    WideningThresholds.Thresholds.exists (Z.equal l) (ResettableLazy.force ts)
 end
 
 module IntInvariant =

src/cdomain/value/util/wideningThresholds.ml

@@ -74,14 +74,11 @@ let conditional_widening_thresholds = ResettableLazy.from_fun (fun () ->
     visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file);
     !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
@@ -107,11 +104,9 @@ let widening_thresholds = ResettableLazy.from_fun (fun () ->
     visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file);
     !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

@@ -2,11 +2,11 @@
 
 module Thresholds : Set.S with type elt = Z.t
 
-val thresholds : unit -> Thresholds.t
-val thresholds_incl_mul2 : unit -> Thresholds.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 -> Thresholds.t
-val lower_thresholds : unit -> Thresholds.t
-val octagon_thresholds : unit -> Thresholds.t
+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 (WideningThresholds.Thresholds.elements 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