Eliminate exception-based hashtable lookups in solver hot paths

src/solver/effectWConEq.ml

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

src/solver/sLR.ml

@@ -51,8 +51,8 @@ module SLR3 =
       let rho'   = HPM.create 10 in
       let q      = ref H.empty in
 
-      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 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 in
       let make_wpoint x = HM.replace wpoint x () in
       let rec solve x =
         if not (HM.mem stable x) then begin
@@ -74,7 +74,7 @@ module SLR3 =
             update_var_event x old tmp;
             if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp;
             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
             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;
@@ -106,7 +106,7 @@ module SLR3 =
         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
         VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ())
       and side x y d =
         HM.add globals y ();

src/solver/sLRphased.ml

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

src/solver/sLRterm.ml

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

src/solver/td3.ml

@@ -58,6 +58,8 @@ module Base =
 
     let exists_key f hm = HM.exists (fun k _ -> f k) hm
 
+    let find_default_delayed h k f = Option.default_delayed f (HM.find_option h k)
+
     let assert_can_receive_side x =
       if Hooks.system x <> None then (
         failwith ("side-effect to unknown w/ rhs: " ^ GobPretty.sprint S.Var.pretty_trace x);
@@ -302,10 +304,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 *)
@@ -522,10 +524,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;
@@ -666,7 +668,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 -> find_default_delayed rho v S.Dom.bot) in
 
         let old_ret = HM.create 103 in
         if reluctant then (
@@ -861,7 +863,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' = find_default_delayed 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 =
@@ -967,8 +969,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
 
@@ -1049,7 +1051,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 = find_default_delayed 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 ();

src/solver/topDown.ml

@@ -21,6 +21,8 @@ module WP =
 
     module HPM = Hashtbl.Make (P)
 
+    let find_default_delayed h k f = Option.default_delayed f (HPM.find_option h k)
+
     let solve st vs =
       let stable = HM.create  10 in
       let infl   = HM.create  10 in (* y -> xs *)
@@ -33,10 +35,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
@@ -96,13 +98,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 = find_default_delayed 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;

src/solver/topDown_deprecated.ml

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

src/solver/topDown_space_cache_term.ml

@@ -20,6 +20,8 @@ module WP =
 
     type phase = Widen | Narrow
 
+    let find_default_delayed h k f = Option.default_delayed f (HM.find_option h k)
+
     let solve st vs =
       let stable = HM.create  10 in
       let infl   = HM.create  10 in (* y -> xs *)
@@ -30,7 +32,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;
@@ -45,7 +47,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 (find_default_delayed 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;
@@ -94,7 +96,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 = find_default_delayed 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;
@@ -148,7 +150,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' = find_default_delayed 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 =

src/solver/topDown_term.ml

@@ -20,6 +20,8 @@ module WP =
 
     type phase = Widen | Narrow
 
+    let find_default_delayed h k f = Option.default_delayed f (HM.find_option h k)
+
     let solve st vs =
       let stable = HM.create  10 in
       let infl   = HM.create  10 in (* y -> xs *)
@@ -30,7 +32,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;
@@ -49,7 +51,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 (find_default_delayed 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;
@@ -83,7 +85,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 = find_default_delayed 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;

src/solver/worklist.ml

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