Define find_default_delayed helper and replace S.Dom.bot() try/Not_found patterns

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/c0745a92-b9e7-48ca-962c-ee3a8c19c6e7

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

Author: Copilot

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);
@@ -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 =
@@ -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 *)
@@ -102,7 +104,7 @@ module WP =
         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_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 *)
@@ -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 *)
@@ -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;