Skip to content
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.

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

Use sets for widening thresholds instead of lists #1591

Open
sim642 opened this issue Oct 3, 2024 · 0 comments
Open

Use sets for widening thresholds instead of lists #1591

sim642 opened this issue Oct 3, 2024 · 0 comments
Labels
cleanup Refactoring, clean-up good first issue performance Analysis time, memory usage

Comments

@sim642
Copy link
Member

sim642 commented Oct 3, 2024

When widening thresholds are collected from the program, we do use a Set to avoid duplicates, but then it's just converted to a list with elements:

let widening_thresholds = ResettableLazy.from_fun (fun () ->
let set = ref Thresholds.empty in
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)

Later, IntDomain uses this list by linearly searching for the next threshold x for u:
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

This linear search is $$O(n)$$ while the same lookup in binary search trees would be $$O(\log n)$$. And actually Set.Make.find_first_opt from the OCaml standard library can be used exactly for this purpose (because that's what Sets are internally).
So we could avoid the intermediate lists and do the more efficient search on sets directly. Although I doubt it will make a notable difference to Goblint performance as a whole.

@sim642 sim642 added cleanup Refactoring, clean-up performance Analysis time, memory usage good first issue labels Oct 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cleanup Refactoring, clean-up good first issue performance Analysis time, memory usage
Projects
None yet
Development

No branches or pull requests

1 participant