From b9747bdc0860dcf38fbf4c0fc5371a994d1ff869 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 28 Jan 2021 06:47:20 -0800
Subject: [PATCH] [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 | 29 +++++++++++++------------
 infer/src/pulse/PulseExecutionDomain.ml |  2 ++
 infer/src/pulse/PulseSkippedCalls.ml    |  6 ++++-
 3 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 0730e55d2..60689067f 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/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
-  && equal_isl_status lhs.isl_status rhs.isl_status
-  &&
-  match
-    BaseDomain.isograph_map BaseDomain.empty_mapping
-      ~lhs:(rhs.pre :> BaseDomain.t)
-      ~rhs:(lhs.pre :> BaseDomain.t)
-  with
-  | NotIsomorphic ->
-      false
-  | IsomorphicUpTo foot_mapping ->
-      BaseDomain.is_isograph foot_mapping
-        ~lhs:(lhs.post :> BaseDomain.t)
-        ~rhs:(rhs.post :> BaseDomain.t)
+  phys_equal lhs rhs
+  || 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
+         ~lhs:(rhs.pre :> BaseDomain.t)
+         ~rhs:(lhs.pre :> BaseDomain.t)
+     with
+     | NotIsomorphic ->
+         false
+     | IsomorphicUpTo foot_mapping ->
+         BaseDomain.is_isograph foot_mapping
+           ~lhs:(lhs.post :> BaseDomain.t)
+           ~rhs:(rhs.post :> BaseDomain.t)
 
 
 let initialize address astate = {astate with post= PostDomain.initialize address astate.post}
diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
index d2433988f..579da13ad 100644
--- a/infer/src/pulse/PulseExecutionDomain.ml
+++ b/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)
diff --git a/infer/src/pulse/PulseSkippedCalls.ml b/infer/src/pulse/PulseSkippedCalls.ml
index 2450fa5e3..8c2d9c478 100644
--- a/infer/src/pulse/PulseSkippedCalls.ml
+++ b/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