From bb3c8cfcc203d6e71af557839342a40f7f30bd9e Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Fri, 8 Mar 2019 10:49:36 -0800
Subject: [PATCH] [pulse][minor] move attributes function around

Summary: imjustmovingshitaround

Reviewed By: mbouaziz

Differential Revision: D14258488

fbshipit-source-id: e32d61b88
---
 infer/src/checkers/PulseDomain.ml     | 28 +++++++++++++++++----------
 infer/src/checkers/PulseDomain.mli    |  3 +--
 infer/src/checkers/PulseOperations.ml |  8 ++++----
 3 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml
index 7b78300f7..91aabdff9 100644
--- a/infer/src/checkers/PulseDomain.ml
+++ b/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
-  (** None denotes a valid location *)
+  val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t) result
 
   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 =
-    (* 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. *)
-    Graph.find_opt address memory |> Option.map ~f:snd
-    |> Option.bind ~f:Attributes.min_elt_opt
-    |> Option.bind ~f:(function Attribute.Invalid invalidation -> Some invalidation | _ -> None)
+  let check_valid address memory =
+    match
+      Graph.find_opt address memory |> Option.map ~f:snd |> Option.bind ~f:Attributes.get_invalid
+    with
+    | Some invalidation ->
+        Error invalidation
+    | None ->
+        Ok ()
 
 
   let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory
diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli
index 62c97d073..9da2c5081 100644
--- a/infer/src/checkers/PulseDomain.mli
+++ b/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
-  (** None denotes a valid location *)
+  val check_valid : AbstractAddress.t -> t -> (unit, PulseInvalidation.t) result
 
   val std_vector_reserve : AbstractAddress.t -> t -> t
 
diff --git a/infer/src/checkers/PulseOperations.ml b/infer/src/checkers/PulseOperations.ml
index ee9af52a7..7d88c816a 100644
--- a/infer/src/checkers/PulseOperations.ml
+++ b/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
-  | Some invalidated_by ->
-      Error (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace})
-  | None ->
+  match Memory.check_valid address astate.heap with
+  | Ok () ->
       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