[pulse][isl] remove er spec duplicates when code includes conditionals

Reviewed By: skcho

Differential Revision: D27618383

fbshipit-source-id: 05821e019

infer/src/pulse/Pulse.ml

@@ -274,8 +274,15 @@ module PulseTransferFunctions = struct
       ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) _cfg_node
       (instr : Sil.instr) : Domain.t list =
     match astate with
-    | AbortProgram _ | ISLLatentMemoryError _ | LatentAbortProgram _ | LatentInvalidAccess _ ->
+    | AbortProgram _ | LatentAbortProgram _ | LatentInvalidAccess _ ->
         [astate]
+    | ISLLatentMemoryError _ -> (
+      (* Note: This is to avoid duplicated error states at join point of branch *)
+      match instr with
+      | Prune (_, _, is_then_branch, _) when is_then_branch ->
+          []
+      | _ ->
+          [astate] )
     | ExitProgram _ ->
         (* program already exited, simply propagate the exited state upwards  *)
         [astate]

infer/src/pulse/PulseAbductiveDomain.ml

@@ -354,7 +354,6 @@ module AddressAttributes = struct
           (astate.post :> BaseDomain.t).attrs
       with
       | None ->
-          let is_eq_null = PathCondition.is_known_zero astate.path_condition addr in
           let null_astates =
             if PathCondition.is_known_not_equal_zero astate.path_condition addr then []
             else
@@ -365,20 +364,23 @@ module AddressAttributes = struct
               let null_astate = abduce_attribute addr null_attr null_astate in
               if null_noop then [Ok null_astate] else [Error (`ISLError null_astate)]
           in
-          if is_eq_null then null_astates
+          let not_null_astates =
-          else
+            if PathCondition.is_known_zero astate.path_condition addr then []
-            let valid_astate =
+            else
-              let abdalloc = Attribute.ISLAbduced access_trace in
+              let valid_astate =
-              let valid_attr = Attribute.MustBeValid access_trace in
+                let abdalloc = Attribute.ISLAbduced access_trace in
-              add_one addr abdalloc astate |> abduce_attribute addr valid_attr
+                let valid_attr = Attribute.MustBeValid access_trace in
-              |> abduce_attribute addr abdalloc
+                add_one addr abdalloc astate |> abduce_attribute addr valid_attr
-            in
+                |> abduce_attribute addr abdalloc
-            let invalid_free =
+              in
-              (*C or Cpp?*)
+              let invalid_free =
-              let invalid_attr = Attribute.Invalid (CFree, access_trace) in
+                (*C or Cpp?*)
-              abduce_attribute addr invalid_attr astate |> add_one addr invalid_attr
+                let invalid_attr = Attribute.Invalid (CFree, access_trace) in
-            in
+                abduce_attribute addr invalid_attr astate |> add_one addr invalid_attr
-            Ok valid_astate :: Error (`ISLError invalid_free) :: null_astates
+              in
+              [Ok valid_astate; Error (`ISLError invalid_free)]
+          in
+          not_null_astates @ null_astates
       | Some _ ->
           [Ok astate] )
     | Some (invalidation, invalidation_trace) ->