Skip to content

Eliminate exception-based hashtable lookups in solver hot paths #1976

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

Draft
Copilot wants to merge 6 commits into
base: master
Choose a base branch
from
Draft

Eliminate exception-based hashtable lookups in solver hot paths #1976

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
e4a9fa7
Initial plan
Copilot Apr 1, 2026
78f39e1
Replace try/Not_found with find_default in solvers; use List.concat_m…
Copilot Apr 1, 2026
9782831
Also replace try/Not_found with find_default in sLR.ml
Copilot Apr 1, 2026
c001b0f
Revert find_default to try/Not_found where default is S.Dom.bot()
Copilot Apr 1, 2026
15ae6b3
Revert List.concat_map change in vendor/ppx_easy_deriving/pat_exp.ml
Copilot Apr 1, 2026
ca2e46a
Define find_default_delayed helper and replace S.Dom.bot() try/Not_fo…
Copilot Apr 1, 2026
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
4 changes: 2 additions & 2 deletions src/solver/effectWConEq.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ module Make =
and eval x y =
get_var_event y;
if not (HM.mem stable y) then solve y;
HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty));
HM.replace infl y (VS.add x (HM.find_default infl y VS.empty));
HM.find rho y

and set x d =
Expand All @@ -63,7 +63,7 @@ module Make =
update_var_event x old tmp;
if not (S.Dom.equal old tmp) then begin
HM.replace rho x tmp;
let w = try HM.find infl x with Not_found -> VS.empty in
let w = HM.find_default infl x VS.empty in
HM.replace infl x VS.empty;
VS.iter (HM.remove stable) w;
VS.iter solve w
Expand Down
8 changes: 4 additions & 4 deletions src/solver/sLRphased.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ module Make =
(* let old = try HPM.find rho' (x,y) with _ -> S.Dom.bot () in *)
(* let d = S.Dom.join old d in *)
HPM.replace rho' (x,y) d;
HM.replace set y (VS.add x (try HM.find set y with Not_found -> VS.empty));
HM.replace set y (VS.add x (HM.find_default set y VS.empty));
if not (HM.mem rho y) then (
if b then solve1 (HM.find key x - 1) ~side:true y else solve0 ~side:true y
) else (
Expand Down Expand Up @@ -124,7 +124,7 @@ module Make =
update_var_event x old val_new;
if tracing then trace "sol" "New Value:%a" S.Dom.pretty val_new;
HM.replace rho x val_new;
let w = try HM.find infl x with Not_found -> VS.empty in
let w = HM.find_default infl x VS.empty in
(* let w = if wpx then VS.add x w else w in *)
q := VS.fold H.add w !q;
HM.replace infl x VS.empty
Expand Down Expand Up @@ -154,13 +154,13 @@ module Make =
new_var_event x;
let d = HM.find rho0 x in
HM.replace rho1 x d;
let w = VS.add x @@ try HM.find infl x with Not_found -> VS.empty in
let w = VS.add x @@ HM.find_default infl x VS.empty in
HM.replace infl x VS.empty;
q := VS.fold H.add w !q;
iterate true prio
)
and sides x =
let w = try HM.find set x with Not_found -> VS.empty in
let w = HM.find_default set x VS.empty in
let v = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ())
in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pretty_trace x S.Dom.pretty v; v
and eq x get set =
Expand Down
8 changes: 4 additions & 4 deletions src/solver/sLRterm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ module SLR3term =
end
in
let sides x =
let w = try HM.find set x with Not_found -> VS.empty in
let w = HM.find_default set x VS.empty in
let v = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in
if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pretty_trace x S.Dom.pretty v; v
in
Expand Down Expand Up @@ -100,7 +100,7 @@ module SLR3term =
if HM.find key x <= HM.find key y then begin
HM.replace wpoint y ()
end;
HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty));
HM.replace infl y (VS.add x (HM.find_default infl y VS.empty));
HM.find rho y
in
let effects = ref Set.empty in
Expand All @@ -126,7 +126,7 @@ module SLR3term =
effects := Set.add y !effects;
if first then (
HPM.replace rho' (x,y) d;
HM.replace set y (VS.add x (try HM.find set y with Not_found -> VS.empty));
HM.replace set y (VS.add x (HM.find_default set y VS.empty));
if not (HM.mem rho y) then (
init ~side:true y;
ignore @@ do_var false y
Expand Down Expand Up @@ -178,7 +178,7 @@ module SLR3term =
update_var_event x old val_new;
if tracing then trace "sol" "New Value:%a" S.Dom.pretty val_new;
HM.replace rho x val_new;
let w = try HM.find infl x with Not_found -> VS.empty in
let w = HM.find_default infl x VS.empty in
(* let w = if wpx then VS.add x w else w in *)
q := VS.fold H.add w !q;
HM.replace infl x VS.empty
Expand Down
18 changes: 9 additions & 9 deletions src/solver/td3.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -302,10 +302,10 @@ module Base =

let add_infl y x =
if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty));
HM.replace infl y (VS.add x (HM.find_default infl y VS.empty));
HM.replace dep x (VS.add y (HM.find_default dep x VS.empty));
in
let add_sides y x = HM.replace sides y (VS.add x (try HM.find sides y with Not_found -> VS.empty)) in
let add_sides y x = HM.replace sides y (VS.add x (HM.find_default sides y VS.empty)) in

let destabilize_ref: (S.v -> unit) ref = ref (fun _ -> failwith "no destabilize yet") in
let destabilize x = !destabilize_ref x in (* must be eta-expanded to use changed destabilize_ref *)
Expand Down Expand Up @@ -522,10 +522,10 @@ module Base =
match weak_deps_handling with
| "none" -> ignore (eval l x y)
| "eager" ->
HM.replace weak_dep x (VS.add y (try HM.find weak_dep x with Not_found -> VS.empty));
HM.replace weak_dep x (VS.add y (HM.find_default weak_dep x VS.empty));
solve y Widen
| "lazy" ->
HM.replace weak_dep x (VS.add y (try HM.find weak_dep x with Not_found -> VS.empty))
HM.replace weak_dep x (VS.add y (HM.find_default weak_dep x VS.empty))
| _ -> assert false
and init x =
if tracing then trace "sol2" "init %a" S.Var.pretty_trace x;
Expand Down Expand Up @@ -666,7 +666,7 @@ module Base =
else
destabilize_normal;

let sys_change = S.sys_change (fun v -> try HM.find rho v with Not_found -> S.Dom.bot ()) in
let sys_change = S.sys_change (fun v -> HM.find_default rho v (S.Dom.bot ())) in
Copy link
Copy Markdown
Member

@sim642 sim642 Apr 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's another catch with ones like this: this now always calls bot (), whereas previously it was only called when actually necessary.
There's a reason why Batteries has some *_delayed functions for some things.

Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz Apr 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@copilot See if batteries has something like this and if it does use that.

Copy link
Copy Markdown
Contributor Author

Copilot AI Apr 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Batteries' Hashtbl.S does not have a find_default_delayed (or equivalent lazy) variant. The find_default usages with S.Dom.bot () have been reverted to try HM.find ... with Not_found -> S.Dom.bot () to preserve the lazy evaluation semantics. The VS.empty cases remain as find_default since VS.empty is a constant (commit c001b0f).

Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz Apr 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@copilot: As there are so many of these, define a helper function find_default_delayed from find_opt and BatOption.default_delayed and use that.

Copy link
Copy Markdown
Contributor Author

Copilot AI Apr 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done in commit ca2e46a. Added find_default_delayed h k f = Option.default_delayed f (HM.find_option h k) to each affected solver module and replaced all try HM.find ... with Not_found -> S.Dom.bot () patterns (9 total across td3.ml, topDown.ml, topDown_term.ml, topDown_space_cache_term.ml). In topDown.ml the helper is defined over HPM (the pair hashtable) since the single S.Dom.bot () case there uses that table.

Copy link
Copy Markdown
Member

@sim642 sim642 Apr 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe it should just be in GobHashtbl.
It might require some interface changes, so it might be easier to benchmark this first and then clean up if it turns out to be beneficial.


let old_ret = HM.create 103 in
if reluctant then (
Expand Down Expand Up @@ -861,7 +861,7 @@ module Base =
let check_side x y d =
HM.replace visited y ();
let mem = HM.mem rho y in
let d' = try HM.find rho y with Not_found -> S.Dom.bot () in
let d' = HM.find_default rho y (S.Dom.bot ()) in
if not (S.Dom.leq d d') then Logs.error "TDFP Fixpoint not reached in restore step at side-effected variable (mem: %b) %a from %a: %a not leq %a" mem S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d S.Dom.pretty d'
in
let rec eq check x =
Expand Down Expand Up @@ -967,8 +967,8 @@ module Base =
(* However, this currently breaks some tests https://github.com/goblint/analyzer/pull/713#issuecomment-1114764937 *)
let one_side ~vh ~x ~y ~d =
(* Also record side-effects caused by post-solver *)
HM.replace side_dep y (VS.add x (try HM.find side_dep y with Not_found -> VS.empty));
HM.replace side_infl x (VS.add y (try HM.find side_infl x with Not_found -> VS.empty));
HM.replace side_dep y (VS.add x (HM.find_default side_dep y VS.empty));
HM.replace side_infl x (VS.add y (HM.find_default side_infl x VS.empty));
end
in

Expand Down Expand Up @@ -1049,7 +1049,7 @@ module Base =
if incr_verify then (
HM.iter (fun x w ->
HM.iter (fun y d ->
let old_d = try HM.find rho y with Not_found -> S.Dom.bot () in
let old_d = HM.find_default rho y (S.Dom.bot ()) in
(* Logs.debug "rho_write retrigger %a %a %a %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty old_d S.Dom.pretty d; *)
HM.replace rho y (S.Dom.join old_d d);
HM.replace init_reachable y ();
Expand Down
8 changes: 4 additions & 4 deletions src/solver/topDown.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,10 @@ module WP =

let add_infl y x =
if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty))
HM.replace infl y (VS.add x (HM.find_default infl y VS.empty))
in
let add_set x y d =
HM.replace set y (VS.add x (try HM.find set y with Not_found -> VS.empty));
HM.replace set y (VS.add x (HM.find_default set y VS.empty));
HPM.add rho' (x,y) d;
HM.replace sidevs y ()
in
Expand Down Expand Up @@ -96,13 +96,13 @@ module WP =
add_infl y x;
HM.find rho y
and sides x =
let w = try HM.find set x with Not_found -> VS.empty in
let w = HM.find_default set x VS.empty in
let d = VS.fold (fun y d -> let r = try S.Dom.join d (HPM.find rho' (y,x)) with Not_found -> d in if tracing then trace "sol2" "sides: side %a from %a: %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty r; r) w (S.Dom.bot ()) in
if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
d
and side x y d =
if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pretty_trace x S.Var.pretty_trace y (HM.mem rho y) S.Dom.pretty d;
let old = try HPM.find rho' (x,y) with Not_found -> S.Dom.bot () in
let old = HPM.find_default rho' (x,y) (S.Dom.bot ()) in
if not (S.Dom.equal old d) then (
add_set x y (S.Dom.join old d);
HM.remove stable y;
Expand Down
6 changes: 3 additions & 3 deletions src/solver/topDown_deprecated.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,8 @@ module TD3 =
let rho = HM.create 10 in
let rho' = HPM.create 10 in (* x,y -> d *)

let add_infl y x = HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty)) in
let add_set x y d = HM.replace set y (VS.add x (try HM.find set y with Not_found -> VS.empty)); HPM.add rho' (x,y) d; HM.add sidevs y () in
let add_infl y x = HM.replace infl y (VS.add x (HM.find_default infl y VS.empty)) in
let add_set x y d = HM.replace set y (VS.add x (HM.find_default set y VS.empty)); HPM.add rho' (x,y) d; HM.add sidevs y () in
let is_side x = HM.mem set x in
let make_wpoint x =
if tracing then trace "sol2" "make_wpoint %a" S.Var.pretty_trace x;
Expand Down Expand Up @@ -90,7 +90,7 @@ module TD3 =
add_infl y x;
HM.find rho y
and sides x =
let w = try HM.find set x with Not_found -> VS.empty in
let w = HM.find_default set x VS.empty in
let d = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in
if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
d
Expand Down
8 changes: 4 additions & 4 deletions src/solver/topDown_space_cache_term.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ module WP =

let add_infl y x =
if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty))
HM.replace infl y (VS.add x (HM.find_default infl y VS.empty))
in
let rec destabilize x =
if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x;
Expand All @@ -45,7 +45,7 @@ module WP =
let old = HM.find rho x in
let l = HM.create 10 in
let tmp = eq x (eval l x) (side l) in
let tmp = S.Dom.join tmp (try HM.find rho' x with Not_found -> S.Dom.bot ()) in
let tmp = S.Dom.join tmp (HM.find_default rho' x (S.Dom.bot ())) in
if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
HM.remove called x;
Expand Down Expand Up @@ -94,7 +94,7 @@ module WP =
tmp
and side l y d =
if tracing then trace "sol2" "side to %a (wpx: %b) ## value: %a" S.Var.pretty_trace y (HM.mem rho y) S.Dom.pretty d;
let old = try HM.find rho' y with Not_found -> S.Dom.bot () in
let old = HM.find_default rho' y (S.Dom.bot ()) in
if not (S.Dom.leq d old) then (
HM.replace rho' y (S.Dom.join old d);
HM.remove l y;
Expand Down Expand Up @@ -148,7 +148,7 @@ module WP =
) else (
HM.replace visited x ();
let check_side y d =
let d' = try HM.find rho y with Not_found -> S.Dom.bot () in
let d' = HM.find_default rho y (S.Dom.bot ()) in
if not (S.Dom.leq d d') then Logs.error "Fixpoint not reached in restore step at side-effected variable %a: %a not leq %a" S.Var.pretty_trace y S.Dom.pretty d S.Dom.pretty d'
in
let eq x =
Expand Down
6 changes: 3 additions & 3 deletions src/solver/topDown_term.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ module WP =

let add_infl y x =
if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty))
HM.replace infl y (VS.add x (HM.find_default infl y VS.empty))
in
let rec destabilize x =
if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x;
Expand All @@ -49,7 +49,7 @@ module WP =
init x;
let old = HM.find rho x in
let tmp = eq x (eval x) side in
let tmp = S.Dom.join tmp (try HM.find rho' x with Not_found -> S.Dom.bot ()) in
let tmp = S.Dom.join tmp (HM.find_default rho' x (S.Dom.bot ())) in
if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ;
if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp;
HM.remove called x;
Expand Down Expand Up @@ -83,7 +83,7 @@ module WP =
add_infl y x;
HM.find rho y
and side y d =
let old = try HM.find rho' y with Not_found -> S.Dom.bot () in
let old = HM.find_default rho' y (S.Dom.bot ()) in
if not (S.Dom.leq d old) then (
HM.replace rho' y (S.Dom.widen old (S.Dom.join old d));
HM.remove stable y;
Expand Down
4 changes: 2 additions & 2 deletions src/solver/worklist.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ module Make =
in
let eval x y =
get_var_event y;
HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty));
HM.replace infl y (VS.add x (HM.find_default infl y VS.empty));
try HM.find rho y
with Not_found ->
new_var_event y;
Expand All @@ -44,7 +44,7 @@ module Make =
if not (leq d old) then begin
update_var_event x old d;
HM.replace rho x (join old d);
let q = try HM.find infl x with Not_found -> VS.empty in
let q = HM.find_default infl x VS.empty in
HM.replace infl x VS.empty;
vs := (VS.fold VS.add q !vs)
end
Expand Down
4 changes: 2 additions & 2 deletions src/vendor/ppx_easy_deriving/pat_exp.ml
View file
Open in desktop
Comment thread
michael-schwarz marked this conversation as resolved.
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,9 @@ let rec to_pat ~loc = function
ppat_var ~loc (Located.mk ~loc s)
let rec to_exps ~loc = function
| Record xs ->
List.flatten (List.map (fun (_, x) -> to_exps ~loc x) xs)
List.concat_map (fun (_, x) -> to_exps ~loc x) xs
| Tuple xs ->
List.flatten (List.map (to_exps ~loc) xs)
List.concat_map (to_exps ~loc) xs
| Unit ->
[]
| Base s ->
Expand Down