From c59765b95cf5d01e59a7ae2cb1254b0f975e615c Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Wed, 19 May 2021 08:56:06 -0700
Subject: [PATCH] [pulse] refactor an ISL function

Summary:
The returned options were never used or only used in cases when they can
only be `None`, as far as I can tell.

Reviewed By: da319

Differential Revision: D28536428

fbshipit-source-id: c16ed4698
---
 infer/src/pulse/PulseAbductiveDomain.ml        | 16 +++++++---------
 infer/src/pulse/PulseBaseAddressAttributes.ml  | 14 ++++----------
 infer/src/pulse/PulseBaseAddressAttributes.mli |  3 +--
 3 files changed, 12 insertions(+), 21 deletions(-)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 027ad24ea..2dbe98ef3 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -353,12 +353,12 @@ module AddressAttributes = struct
   let check_valid_isl access_trace addr ?(null_noop = false) astate =
     L.d_printfln "*****check_valid_isl: addr*** %a@\n" AbstractValue.pp addr ;
     match BaseAddressAttributes.get_invalid addr (astate.post :> BaseDomain.t).attrs with
-    | None -> (
-      match
-        BaseAddressAttributes.get_must_be_valid_or_allocated_isl addr
-          (astate.post :> BaseDomain.t).attrs
-      with
-      | None, reason ->
+    | None ->
+        if
+          BaseAddressAttributes.is_must_be_valid_or_allocated_isl addr
+            (astate.post :> BaseDomain.t).attrs
+        then [Ok astate]
+        else
           let null_astates =
             if PathCondition.is_known_not_equal_zero astate.path_condition addr then []
             else
@@ -374,7 +374,7 @@ module AddressAttributes = struct
             else
               let valid_astate =
                 let abdalloc = Attribute.ISLAbduced access_trace in
-                let valid_attr = Attribute.MustBeValid (access_trace, reason) in
+                let valid_attr = Attribute.MustBeValid (access_trace, None) in
                 add_one addr abdalloc astate |> abduce_attribute addr valid_attr
                 |> abduce_attribute addr abdalloc
               in
@@ -386,8 +386,6 @@ module AddressAttributes = struct
               [Ok valid_astate; Error (`ISLError invalid_free)]
           in
           not_null_astates @ null_astates
-      | Some _, _ ->
-          [Ok astate] )
     | Some (invalidation, invalidation_trace) ->
         [Error (`InvalidAccess (invalidation, invalidation_trace, astate))]
 end
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml
index 1e8d82447..02948b84b 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.ml
+++ b/infer/src/pulse/PulseBaseAddressAttributes.ml
@@ -136,16 +136,10 @@ let get_invalid = get_attribute Attributes.get_invalid
 
 let get_must_be_valid = get_attribute Attributes.get_must_be_valid
 
-let get_must_be_valid_or_allocated_isl address attrs =
-  match get_must_be_valid address attrs with
-  | Some (trace, reason) ->
-      (Some trace, reason)
-  | None -> (
-    match get_attribute Attributes.get_allocation address attrs with
-    | Some (_, trace) ->
-        (Some trace, None)
-    | None ->
-        (get_attribute Attributes.get_isl_abduced address attrs, None) )
+let is_must_be_valid_or_allocated_isl address attrs =
+  Option.is_some (get_must_be_valid address attrs)
+  || Option.is_some (get_attribute Attributes.get_allocation address attrs)
+  || Option.is_some (get_attribute Attributes.get_isl_abduced address attrs)
 
 
 let get_must_be_initialized = get_attribute Attributes.get_must_be_initialized
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli
index 01eb6cd7e..c13b63a88 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.mli
+++ b/infer/src/pulse/PulseBaseAddressAttributes.mli
@@ -42,8 +42,7 @@ val get_invalid : AbstractValue.t -> t -> (Invalidation.t * Trace.t) option
 val get_must_be_valid :
   AbstractValue.t -> t -> (Trace.t * Invalidation.must_be_valid_reason option) option
 
-val get_must_be_valid_or_allocated_isl :
-  AbstractValue.t -> t -> Trace.t option * Invalidation.must_be_valid_reason option
+val is_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> bool
 
 val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option