[pulse] better AbductiveDomain.leq

Summary:
It's a potentially expensive operation given that it does graph
isomorphism twice on equal values so add a fast path for when they are
the same pointer. Also comparing "skipped calls" doesn't need to care
about traces.

Reviewed By: da319

Differential Revision: D26022022

fbshipit-source-id: 8178df37b

infer/src/pulse/PulseAbductiveDomain.ml

@@ -119,20 +119,21 @@ let set_isl_status status astate = {astate with isl_status= status}
 let set_path_condition path_condition astate = {astate with path_condition}
 
 let leq ~lhs ~rhs =
-  SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls
+  phys_equal lhs rhs
-  && equal_isl_status lhs.isl_status rhs.isl_status
+  || SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls
-  &&
+     && ((not Config.pulse_isl) || equal_isl_status lhs.isl_status rhs.isl_status)
-  match
+     &&
-    BaseDomain.isograph_map BaseDomain.empty_mapping
+     match
-      ~lhs:(rhs.pre :> BaseDomain.t)
+       BaseDomain.isograph_map BaseDomain.empty_mapping
-      ~rhs:(lhs.pre :> BaseDomain.t)
+         ~lhs:(rhs.pre :> BaseDomain.t)
-  with
+         ~rhs:(lhs.pre :> BaseDomain.t)
-  | NotIsomorphic ->
+     with
-      false
+     | NotIsomorphic ->
-  | IsomorphicUpTo foot_mapping ->
+         false
-      BaseDomain.is_isograph foot_mapping
+     | IsomorphicUpTo foot_mapping ->
-        ~lhs:(lhs.post :> BaseDomain.t)
+         BaseDomain.is_isograph foot_mapping
-        ~rhs:(rhs.post :> BaseDomain.t)
+           ~lhs:(lhs.post :> BaseDomain.t)
+           ~rhs:(rhs.post :> BaseDomain.t)
 
 
 let initialize address astate = {astate with post= PostDomain.initialize address astate.post}

infer/src/pulse/PulseExecutionDomain.ml

@@ -31,6 +31,8 @@ let continue astate = ContinueProgram astate
 let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc)
 
 let leq ~lhs ~rhs =
+  phys_equal lhs rhs
+  ||
   match (lhs, rhs) with
   | AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 ->
       AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)

infer/src/pulse/PulseSkippedCalls.ml

@@ -23,6 +23,10 @@ module SkippedTrace = struct
   let widen ~prev ~next ~num_iters:_ = join prev next
 end
 
-include AbstractDomain.Map (Procname) (SkippedTrace)
+module M = AbstractDomain.Map (Procname) (SkippedTrace)
+include M
 
 let yojson_of_t = [%yojson_of: _]
+
+(* ignore traces, just compare if the set of skipped procedures is the same *)
+let leq ~lhs ~rhs = M.equal (fun _ _ -> true) lhs rhs