[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

@@ -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

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

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