Revert find_default to try/Not_found where default is S.Dom.bot()

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/549bf1a5-1caf-4b0a-b8e3-fadb8c217dea

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

Author: Copilot

src/solver/td3.ml

@@ -666,7 +666,7 @@ module Base =
           else
             destabilize_normal;
 
-        let sys_change = S.sys_change (fun v -> HM.find_default rho v (S.Dom.bot ())) in
+        let sys_change = S.sys_change (fun v -> try HM.find rho v with Not_found -> S.Dom.bot ()) in
 
         let old_ret = HM.create 103 in
         if reluctant then (
@@ -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' = HM.find_default rho y (S.Dom.bot ()) in
+        let d' = try HM.find rho y with Not_found -> 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 +1049,7 @@ module Base =
           if incr_verify then (
             HM.iter (fun x w ->
                 HM.iter (fun y d ->
-                    let old_d = HM.find_default rho y (S.Dom.bot ()) in
+                    let old_d = try HM.find rho y with Not_found -> 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

@@ -102,7 +102,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 = HPM.find_default rho' (x,y) (S.Dom.bot ()) in
+        let old = try HPM.find rho' (x,y) with Not_found -> 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

@@ -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 (HM.find_default rho' x (S.Dom.bot ())) in
+          let tmp = S.Dom.join tmp (try HM.find rho' x with Not_found -> 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 +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 = HM.find_default rho' y (S.Dom.bot ()) in
+        let old = try HM.find rho' y with Not_found -> 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 +148,7 @@ module WP =
         ) else (
           HM.replace visited x ();
           let check_side y d =
-            let d' = HM.find_default rho y (S.Dom.bot ()) in
+            let d' = try HM.find rho y with Not_found -> 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

@@ -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 (HM.find_default rho' x (S.Dom.bot ())) in
+          let tmp = S.Dom.join tmp (try HM.find rho' x with Not_found -> 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 +83,7 @@ module WP =
         add_infl y x;
         HM.find rho y
       and side y d =
-        let old = HM.find_default rho' y (S.Dom.bot ()) in
+        let old = try HM.find rho' y with Not_found -> 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;