[pulse] use phys_equal on the underlying abstract state instead of the toplevel pair

Summary:
This is more useful for a future where we use the exceptional CFG but
even without it we see some non-trivial changes on OpenSSL (slightly
fewer total disjunts):

Before:
```
Found 57 issues (console output truncated to 5, see '/home/jul/code/openssl-1.0.2d/infer-out/report.txt' for the full list)
                      Issue Type(ISSUED_TYPE_ID): #
                        Memory Leak(MEMORY_LEAK): 48
        Nullptr Dereference(NULLPTR_DEREFERENCE): 6
  Uninitialized Value(PULSE_UNINITIALIZED_VALUE): 3
infer --pulse-only --scheduler restart --pulse-model-malloc-pattern       387.55s user 7.20s system 192% cpu 3:24.60 total

average #disjuncts: 7.695755
total #disjuncts: 64906
min= 0; p10=  0; p20=  1; p25=  1; p30=  1; p40=  1; p50=  2; p60=  4; p70= 18; p75= 20; p80= 20; p90= 20; p95= 20; p96= 20; p97= 20; p98= 20; p99= 20; max= 20
 51253 continue
    67 exit
  1101 abort
  9606 latent abort
  2879 latent invalid
```

After:
```
Found 64 issues (console output truncated to 5, see '/home/jul/code/openssl-1.0.2d/infer-out/report.txt' for the full list)
                      Issue Type(ISSUED_TYPE_ID): #
                        Memory Leak(MEMORY_LEAK): 55
        Nullptr Dereference(NULLPTR_DEREFERENCE): 6
  Uninitialized Value(PULSE_UNINITIALIZED_VALUE): 3
infer --pulse-only --scheduler restart --pulse-model-malloc-pattern       371.63s user 6.62s system 196% cpu 3:12.41 total

average #disjuncts: 7.537230
total #disjuncts: 63569
min= 0; p10=  0; p20=  1; p25=  1; p30=  1; p40=  1; p50=  2; p60=  4; p70= 16; p75= 20; p80= 20; p90= 20; p95= 20; p96= 20; p97= 20; p98= 20; p99= 20; max= 20
 53763 continue
    67 exit
  1022 abort
  6270 latent abort
  2447 latent invalid
```

Reviewed By: ezgicicek

Differential Revision: D29230744

fbshipit-source-id: 5c76c275f

infer/src/absint/AbstractDomain.ml

@@ -18,14 +18,22 @@ end
 
 open! Types
 
-module type NoJoin = sig
+module type Comparable = sig
   include PrettyPrintable.PrintableType
 
   val leq : lhs:t -> rhs:t -> bool
 end
 
+module type Disjunct = sig
+  include Comparable
+
+  val equal_fast : t -> t -> bool
+end
+
 module type S = sig
-  include NoJoin
+  include PrettyPrintable.PrintableType
+
+  val leq : lhs:t -> rhs:t -> bool
 
   val join : t -> t -> t
 
@@ -175,7 +183,7 @@ module TopLifted (Domain : S) = struct
   let pp = TopLiftedUtils.pp ~pp:Domain.pp
 end
 
-module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) = struct
+module PairBase (Domain1 : Comparable) (Domain2 : Comparable) = struct
   type t = Domain1.t * Domain2.t
 
   let leq ~lhs ~rhs =
@@ -186,8 +194,14 @@ module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) = struct
   let pp fmt astate = Pp.pair ~fst:Domain1.pp ~snd:Domain2.pp fmt astate
 end
 
+module PairDisjunct (Domain1 : Disjunct) (Domain2 : Disjunct) = struct
+  include PairBase (Domain1) (Domain2)
+
+  let equal_fast (x1, x2) (y1, y2) = Domain1.equal_fast x1 y1 && Domain2.equal_fast x2 y2
+end
+
 module Pair (Domain1 : S) (Domain2 : S) = struct
-  include PairNoJoin (Domain1) (Domain2)
+  include PairBase (Domain1) (Domain2)
 
   let join astate1 astate2 =
     if phys_equal astate1 astate2 then astate1

infer/src/absint/AbstractDomain.mli

@@ -19,15 +19,23 @@ end
 
 open! Types
 
-module type NoJoin = sig
+module type Comparable = sig
   include PrettyPrintable.PrintableType
 
   val leq : lhs:t -> rhs:t -> bool
   (** the implication relation: [lhs <= rhs] means [lhs |- rhs] *)
 end
 
+module type Disjunct = sig
+  include Comparable
+
+  val equal_fast : t -> t -> bool
+  (** [equal_fast x y] must imply [x <=> y]; it's a good idea for this function to be "fast", e.g.
+      not depend on the size of its input *)
+end
+
 module type S = sig
-  include NoJoin
+  include Comparable
 
   val join : t -> t -> t
 
@@ -83,7 +91,8 @@ end
 (** Cartesian product of two domains. *)
 module Pair (Domain1 : S) (Domain2 : S) : S with type t = Domain1.t * Domain2.t
 
-module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) : NoJoin with type t = Domain1.t * Domain2.t
+module PairDisjunct (Domain1 : Disjunct) (Domain2 : Disjunct) :
+  Disjunct with type t = Domain1.t * Domain2.t
 
 (** Flat abstract domain: Bottom, Top, and non-comparable elements in between *)
 module Flat (V : PrettyPrintable.PrintableEquatableType) : sig

infer/src/absint/AbstractInterpreter.ml

@@ -162,7 +162,7 @@ struct
 
 
     let join_up_to ~limit ~into:lhs rhs =
-      join_up_to_with_leq ~limit (fun ~lhs ~rhs -> phys_equal lhs rhs) ~into:lhs rhs
+      join_up_to_with_leq ~limit (fun ~lhs ~rhs -> T.Domain.equal_fast lhs rhs) ~into:lhs rhs
 
 
     let join lhs rhs = join_up_to ~limit:disjunct_limit ~into:lhs rhs |> fst
@@ -173,7 +173,7 @@ struct
       match (disj, of_) with
       | [], _ ->
           true
-      | x :: disj', y :: of' when phys_equal x y ->
+      | x :: disj', y :: of' when T.Domain.equal_fast x y ->
           is_trivial_subset disj' ~of_:of'
       | _, _ :: of' ->
           is_trivial_subset disj ~of_:of'
@@ -229,7 +229,7 @@ struct
       | None ->
           true
       | Some {State.pre= previous_pre; _} ->
-          not (List.mem ~equal:phys_equal previous_pre disjunct)
+          not (List.mem ~equal:T.Domain.equal_fast previous_pre disjunct)
     in
     let current_post_n =
       match old_state_opt with None -> ([], 0) | Some {State.post; _} -> (post, List.length post)

infer/src/absint/TransferFunctions.ml

@@ -43,7 +43,7 @@ end
 module type DisjReady = sig
   module CFG : ProcCfg.S
 
-  module Domain : AbstractDomain.NoJoin
+  module Domain : AbstractDomain.Disjunct
 
   type analysis_data
 

infer/src/absint/TransferFunctions.mli

@@ -55,7 +55,7 @@ end
 module type DisjReady = sig
   module CFG : ProcCfg.S
 
-  module Domain : AbstractDomain.NoJoin
+  module Domain : AbstractDomain.Disjunct
 
   type analysis_data
 

infer/src/pulse/Pulse.ml

@@ -25,7 +25,7 @@ let report_topl_errors proc_desc err_log summary =
 
 module PulseTransferFunctions = struct
   module CFG = ProcCfg.Normal
-  module Domain = AbstractDomain.PairNoJoin (PathContext) (ExecutionDomain)
+  module Domain = AbstractDomain.PairDisjunct (ExecutionDomain) (PathContext)
 
   type analysis_data = PulseSummary.t InterproceduralAnalysis.t
 
@@ -443,13 +443,13 @@ module PulseTransferFunctions = struct
           [ContinueProgram astate] )
 
 
-  let exec_instr (path, astate) analysis_data cfg_node instr : Domain.t list =
+  let exec_instr (astate, path) analysis_data cfg_node instr : Domain.t list =
     (* Sometimes instead of stopping on contradictions a false path condition is recorded
        instead. Prune these early here so they don't spuriously count towards the disjunct limit. *)
     exec_instr_aux path astate analysis_data cfg_node instr
     |> List.filter_map ~f:(fun exec_state ->
            if ExecutionDomain.is_unsat_cheap exec_state then None
-           else Some (PathContext.post_exec_instr path, exec_state) )
+           else Some (exec_state, PathContext.post_exec_instr path) )
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
@@ -474,11 +474,11 @@ let with_debug_exit_node proc_desc ~f =
 let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) =
   AbstractValue.State.reset () ;
   let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in
-  let initial = [(PathContext.initial, initial_astate)] in
+  let initial = [(initial_astate, PathContext.initial)] in
   match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with
   | Some posts ->
       (* forget path contexts, we don't propagate them across functions *)
-      let posts = List.map ~f:snd posts in
+      let posts = List.map ~f:fst posts in
       with_debug_exit_node proc_desc ~f:(fun () ->
           let updated_posts =
             PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts

infer/src/pulse/PulseExecutionDomain.ml

@@ -93,3 +93,16 @@ let get_astate : t -> AbductiveDomain.t = function
 let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_state).path_condition
 
 type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of]
+
+let equal_fast exec_state1 exec_state2 =
+  phys_equal exec_state1 exec_state2
+  ||
+  match (exec_state1, exec_state2) with
+  | AbortProgram astate1, AbortProgram astate2
+  | ExitProgram astate1, ExitProgram astate2
+  | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 ->
+      phys_equal astate1 astate2
+  | ContinueProgram astate1, ContinueProgram astate2 ->
+      phys_equal astate1 astate2
+  | _ ->
+      false

infer/src/pulse/PulseExecutionDomain.mli

@@ -31,7 +31,7 @@ type 'abductive_domain_t base_t =
 
 type t = AbductiveDomain.t base_t
 
-include AbstractDomain.NoJoin with type t := t
+include AbstractDomain.Disjunct with type t := t
 
 val continue : AbductiveDomain.t -> t
 

infer/src/pulse/PulsePathContext.ml

@@ -17,6 +17,9 @@ type t = {timestamp: timestamp}
 (** path contexts is metadata that do not contribute to the semantics *)
 let leq ~lhs:_ ~rhs:_ = true
 
+(** see [leq] *)
+let equal_fast _ _ = true
+
 let pp fmt ({timestamp}[@warning "+9"]) = F.fprintf fmt "timestamp= %d" timestamp
 
 let initial = {timestamp= 0}

infer/src/pulse/PulsePathContext.mli

@@ -16,6 +16,8 @@ type t = {timestamp: timestamp  (** step number *)}
 
 val leq : lhs:t -> rhs:t -> bool
 
+val equal_fast : t -> t -> bool
+
 val initial : t
 
 val post_exec_instr : t -> t