[pulse] Remove NoJoin sig from PulseBaseDomain

Summary: `PulseBaseDomain.leq` is never called but was there to satisfy the signature of `NoJoin` which itself was not needed. This diff removes `include NoJoin` and instead just adds signature for `pp` in `PulseBaseDomain`.

Reviewed By: jvillard

Differential Revision: D20280104

fbshipit-source-id: 8e3659280

infer/src/pulse/PulseAbductiveDomain.ml

@@ -34,7 +34,7 @@ module type BaseDomain = sig
   val filter_addr : f:(AbstractValue.t -> bool) -> t -> t
   (**filter both heap and attrs *)
 
-  include AbstractDomain.NoJoin with type t := t
+  val pp : F.formatter -> t -> unit
 end
 
 (* just to expose record field names without having to type
@@ -83,9 +83,6 @@ module InvertedDomain : BaseDomain = struct
   let empty = BaseDomain.empty
 
   let pp = BaseDomain.pp
-
-  (** inverted lattice *)
-  let leq ~lhs ~rhs = BaseDomain.leq ~rhs:lhs ~lhs:rhs
 end
 
 (** biabduction-style pre/post state *)

infer/src/pulse/PulseBaseDomain.ml

@@ -190,10 +190,6 @@ module GraphComparison = struct
     match isograph_map ~lhs ~rhs mapping with IsomorphicUpTo _ -> true | NotIsomorphic -> false
 end
 
-let leq ~lhs ~rhs =
-  phys_equal lhs rhs || GraphComparison.is_isograph ~lhs ~rhs GraphComparison.empty_mapping
-
-
 let pp fmt {heap; stack; skipped_calls; attrs} =
   F.fprintf fmt
     "{@[<v1> roots=@[<hv>%a@];@;mem  =@[<hv>%a@];@;attrs=@[<hv>%a@];@;skipped_calls=@[<hv>%a@];@]}"

infer/src/pulse/PulseBaseDomain.mli

@@ -7,6 +7,7 @@
 
 open! IStd
 open PulseBasicInterface
+module F = Format
 
 module SkippedTrace : sig
   type t = PulseTrace.t
@@ -25,8 +26,6 @@ type cell = PulseBaseMemory.Edges.t * Attributes.t
 
 val empty : t
 
-include AbstractDomain.NoJoin with type t := t
-
 val reachable_addresses : t -> AbstractValue.Set.t
 (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable from
     the stack variables *)
@@ -44,3 +43,5 @@ val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation
 val is_isograph : lhs:t -> rhs:t -> mapping -> bool
 
 val find_cell_opt : AbstractValue.t -> t -> cell option
+
+val pp : F.formatter -> t -> unit