[pulse][minor] move attributes function around

Summary: imjustmovingshitaround

Reviewed By: mbouaziz

Differential Revision: D14258488

fbshipit-source-id: e32d61b88

infer/src/checkers/PulseDomain.ml

@@ -36,7 +36,15 @@ module Attribute = struct
         F.pp_print_string f "std::vector::reserve()"
 end
 
-module Attributes = AbstractDomain.FiniteSet (Attribute)
+module Attributes = struct
+  include AbstractDomain.FiniteSet (Attribute)
+
+  let get_invalid attrs =
+    (* Since we often want to find out whether an address is invalid this case is optimised. Since
+       [Invalid _] attributes are the smallest we can simply look at the first element to decide if
+       an address is invalid or not. *)
+    match min_elt_opt attrs with Some (Invalid invalidation) -> Some invalidation | _ -> None
+end
 
 (** An abstract address in memory. *)
 module AbstractAddress : sig
@@ -112,8 +120,7 @@ module Memory : sig
 
   val invalidate : AbstractAddress.t -> Invalidation.t -> t -> t
 
-  val get_invalidation : AbstractAddress.t -> t -> Invalidation.t option
+  val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t) result
-  (** None denotes a valid location *)
 
   val std_vector_reserve : AbstractAddress.t -> t -> t
 
@@ -198,13 +205,14 @@ end = struct
     add_attribute address (Attribute.Invalid invalidation) memory
 
 
-  let get_invalidation address memory =
+  let check_valid address memory =
-    (* Since we often want to find out whether an address is invalid this case is optimised. Since
+    match
-       [Invalid _] attributes are the smallest we can simply look at the first element to decide if
+      Graph.find_opt address memory |> Option.map ~f:snd |> Option.bind ~f:Attributes.get_invalid
-       an address is invalid or not. *)
+    with
-    Graph.find_opt address memory |> Option.map ~f:snd
+    | Some invalidation ->
-    |> Option.bind ~f:Attributes.min_elt_opt
+        Error invalidation
-    |> Option.bind ~f:(function Attribute.Invalid invalidation -> Some invalidation | _ -> None)
+    | None ->
+        Ok ()
 
 
   let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory

infer/src/checkers/PulseDomain.mli

@@ -72,8 +72,7 @@ module Memory : sig
 
   val invalidate : AbstractAddress.t -> PulseInvalidation.t -> t -> t
 
-  val get_invalidation : AbstractAddress.t -> t -> PulseInvalidation.t option
+  val check_valid : AbstractAddress.t -> t -> (unit, PulseInvalidation.t) result
-  (** None denotes a valid location *)
 
   val std_vector_reserve : AbstractAddress.t -> t -> t
 

infer/src/checkers/PulseOperations.ml

@@ -19,11 +19,11 @@ type 'a access_result = ('a, PulseDiagnostic.t) result
 
 (** Check that the address is not known to be invalid *)
 let check_addr_access actor (address, trace) astate =
-  match Memory.get_invalidation address astate.heap with
+  match Memory.check_valid address astate.heap with
-  | Some invalidated_by ->
+  | Ok () ->
-      Error (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace})
-  | None ->
       Ok astate
+  | Error invalidated_by ->
+      Error (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace})
 
 
 (** Walk the heap starting from [addr] and following [path]. Stop either at the element before last