Skip to content

Fix unsoundness bug in interval sets and refactor interval widen thresholds #1476

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 9 commits into from
May 22, 2024
Merged

Fix unsoundness bug in interval sets and refactor interval widen thresholds #1476

Changes from 4 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
716bec9
Check that next thresholds in widening are smaller than max_ik or gre…
karoliineh May 21, 2024
6e2a565
Move upper_threshold and lower_threshold functions out of widen
karoliineh May 21, 2024
b551cd5
Move upper_threshold and lower_threshold functions to IntervalArith
karoliineh May 21, 2024
beb1200
Use upper_threshold and lower_threshold functions from IntervalArith …
karoliineh May 21, 2024
f3a0ab6
Apply suggestions from code review
karoliineh May 21, 2024
c9d7cf7
Calculate lt and ut only when needed
karoliineh May 21, 2024
f3d932d
Remove duplicated check of selecting min (or max) of max_ik (or min_i…
karoliineh May 21, 2024
4c21a79
Remove unnecessary max of u1 or threshold (and min of l1 or threshold)
karoliineh May 21, 2024
a86fb6f
Add unit tests for interval widen
karoliineh May 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 15 additions & 26 deletions src/cdomain/value/cdomains/intDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -559,6 +559,17 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct

let to_int (x1, x2) =
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 u = Ints_t.to_bigint u in
let t = List.find_opt (fun x -> Z.compare u x <= 0 && Z.compare x (Ints_t.to_bigint 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 l = Ints_t.to_bigint l in
let t = List.find_opt (fun x -> Z.compare l x >= 0 && Z.compare x (Ints_t.to_bigint min_ik) >= 0) ts in
BatOption.map_default Ints_t.of_bigint min_ik t
end

module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =
Expand Down Expand Up @@ -668,21 +679,9 @@ struct
| Some (l0,u0), Some (l1,u1) ->
let (min_ik, max_ik) = range ik in
let threshold = get_interval_threshold_widening () in
let 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
let t = List.find_opt (fun x -> Z.compare u x <= 0) ts in
BatOption.map_default Ints_t.of_bigint max_ik t
in
let 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
let t = List.find_opt (fun x -> Z.compare l x >= 0) ts in
BatOption.map_default Ints_t.of_bigint min_ik t
in
let lt = if threshold then lower_threshold l1 else min_ik in
let lt = if threshold then IArith.lower_threshold l1 min_ik else min_ik in
let l2 = if Ints_t.compare l0 l1 = 0 then l0 else Ints_t.min l1 (Ints_t.max lt min_ik) in
let ut = if threshold then upper_threshold u1 else max_ik in
let ut = if threshold then IArith.upper_threshold u1 max_ik else max_ik in
let u2 = if Ints_t.compare u0 u1 = 0 then u0 else Ints_t.max u1 (Ints_t.min ut max_ik) in
norm ik @@ Some (l2,u2) |> fst
let widen ik x y =
Expand Down Expand Up @@ -1394,18 +1393,8 @@ struct
let widen ik xs ys =
let (min_ik,max_ik) = range ik in
let threshold = get_bool "ana.int.interval_threshold_widening" in
let upper_threshold (_,u) =
let ts = if GobConfig.get_string "ana.int.interval_threshold_widening_constants" = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in
let u = Ints_t.to_bigint u in
let t = List.find_opt (fun x -> Z.compare u x <= 0) ts in
BatOption.map_default Ints_t.of_bigint max_ik t
in
let lower_threshold (l,_) =
let ts = if GobConfig.get_string "ana.int.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 t = List.find_opt (fun x -> Z.compare l x >= 0) ts in
BatOption.map_default Ints_t.of_bigint min_ik t
in
let upper_threshold (_,u) = IArith.upper_threshold u max_ik in
let lower_threshold (l,_) = IArith.lower_threshold l min_ik in
(*obtain partitioning of xs intervals according to the ys interval that includes them*)
let rec interval_sets_to_partitions (ik: ikind) (acc : (int_t * int_t) option) (xs: t) (ys: t)=
match xs,ys with
Expand Down