Simplify remove_unreachable in uninit and malloc_null

goblint · Sep 12, 2023 · 3ee9af8 · 3ee9af8
1 parent 0568edd
commit 3ee9af8
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 24 deletions.
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
@@ -94,25 +94,25 @@ struct
   (* Remove null values from state that are unreachable from exp.*)
   let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t =
     let reachable =
-      let do_exp e =
+      let do_exp e a =
         match ask.f (Queries.ReachableFrom e) with
         | ad when not (Queries.AD.is_top ad) ->
-          let to_extra addr ad =
-            match addr with
-            | Queries.AD.Addr.Addr _ -> AD.add addr ad
-            | _ -> ad
-          in
-          Queries.AD.fold to_extra ad (AD.empty ())
+          ad
+          |> Queries.AD.filter (function
+              | Queries.AD.Addr.Addr _ -> true
+              | _ -> false)
+          |> Queries.AD.join a
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
         | _ -> AD.empty ()
       in
-      List.map do_exp args
+      List.fold_right do_exp args (AD.empty ())
     in
-    let add_exploded_struct (one: AD.t) (many: AD.t) : AD.t =
-      let vars = AD.to_var_may one in
-      List.fold_right AD.add (List.concat_map to_addrs vars) many
+    let vars =
+      reachable
+      |> AD.to_var_may
+      |> List.concat_map to_addrs
+      |> AD.of_list
     in
-    let vars = List.fold_right add_exploded_struct reachable (AD.empty ()) in
     if D.is_top st
     then D.top ()
     else D.filter (fun x -> AD.mem x vars) st

diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
@@ -193,25 +193,25 @@ struct
 
   let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t =
     let reachable =
-      let do_exp e =
+      let do_exp e a =
         match ask.f (Queries.ReachableFrom e) with
         | ad when not (Queries.AD.is_top ad) ->
-          let to_extra addr ad =
-            match addr with
-            | Queries.AD.Addr.Addr _ -> AD.add addr ad
-            | _ -> ad
-          in
-          Queries.AD.fold to_extra ad (AD.empty ())
+          ad
+          |> Queries.AD.filter (function
+              | Queries.AD.Addr.Addr _ -> true
+              | _ -> false)
+          |> Queries.AD.join a
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
         | _ -> AD.empty ()
       in
-      List.map do_exp args
+      List.fold_right do_exp args (AD.empty ())
     in
-    let add_exploded_struct (one: AD.t) (many: AD.t) : AD.t =
-      let vars = AD.to_var_may one in
-      List.fold_right AD.add (List.concat_map to_addrs vars) many
+    let vars =
+      reachable
+      |> AD.to_var_may
+      |> List.concat_map to_addrs
+      |> AD.of_list
     in
-    let vars = List.fold_right add_exploded_struct reachable (AD.empty ()) in
     if D.is_top st
     then D.top ()
     else D.filter (fun x -> AD.mem x vars) st