[pulse] remove last traces of join/widen

Summary:
Instead of defining `let join .. = assert false` introduce simplified
module signatures for domains without join/widen as used in disjunctive
domains.

Reviewed By: mbouaziz, skcho

Differential Revision: D14568271

fbshipit-source-id: 6484335c9

infer/src/absint/AbstractDomain.ml

@@ -20,10 +20,14 @@ open! Types
 
 exception Stop_analysis
 
-module type S = sig
+module type NoJoin = sig
   include PrettyPrintable.PrintableType
 
   val ( <= ) : lhs:t -> rhs:t -> bool
+end
+
+module type S = sig
+  include NoJoin
 
   val join : t -> t -> t
 

infer/src/absint/AbstractDomain.mli

@@ -23,11 +23,15 @@ exception Stop_analysis
 
 (** Abstract domains and domain combinators *)
 
-module type S = sig
+module type NoJoin = sig
   include PrettyPrintable.PrintableType
 
   val ( <= ) : lhs:t -> rhs:t -> bool
-  (** the partial order induced by join *)
+  (** the implication relation: [lhs <= rhs] means [lhs |- rhs] *)
+end
+
+module type S = sig
+  include NoJoin
 
   val join : t -> t -> t
 

infer/src/absint/TransferFunctions.ml

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

infer/src/absint/TransferFunctions.mli

@@ -51,7 +51,7 @@ end
 module type DisjReady = sig
   module CFG : ProcCfg.S
 
-  module Domain : AbstractDomain.S
+  module Domain : AbstractDomain.NoJoin
 
   type extras
 

infer/src/pulse/PulseDomain.ml

@@ -238,12 +238,7 @@ end = struct
     if phys_equal heap (fst memory) && phys_equal attrs (snd memory) then memory else (heap, attrs)
 end
 
-(** Stacks: map addresses of variables to values and initialisation location.
+(** Stacks: map addresses of variables to values and initialisation location. *)
-
-    This is defined as an abstract domain but the domain operations are mostly meaningless on their
-    own. It so happens that the join on abstract states uses the join of stacks provided by this
-    functor followed by normalization wrt the unification found between abstract locations so it's
-    convenient to define stacks as elements of this domain. *)
 module Stack = struct
   module VarAddress = struct
     include Var
@@ -258,28 +253,22 @@ module Stack = struct
       F.fprintf f "%a%a" pp_ampersand var Var.pp var
   end
 
-  module ValueDomain = struct
+  module VarValue = struct
     type t = AbstractAddress.t * Location.t option [@@deriving compare]
 
-    let join ((addr1, _) as v1) ((addr2, _) as v2) = if addr1 <= addr2 then v1 else v2
-
-    let ( <= ) ~lhs:(lhs_addr, _) ~rhs:(rhs_addr, _) = AbstractAddress.equal lhs_addr rhs_addr
-
-    let widen ~prev ~next ~num_iters:_ = join prev next
-
     let pp = Pp.pair ~fst:AbstractAddress.pp ~snd:(Pp.option Location.pp)
   end
 
-  include AbstractDomain.Map (VarAddress) (ValueDomain)
+  include PrettyPrintable.MakePPMonoMap (VarAddress) (VarValue)
 
   let pp fmt m =
     let pp_item fmt (var_address, v) =
-      F.fprintf fmt "%a=%a" VarAddress.pp var_address ValueDomain.pp v
+      F.fprintf fmt "%a=%a" VarAddress.pp var_address VarValue.pp v
     in
     PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
 
 
-  let compare = compare ValueDomain.compare
+  let compare = compare VarValue.compare
 end
 
 type t = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
@@ -442,17 +431,11 @@ module GraphComparison = struct
     match supergraph_map ~lhs ~rhs mapping with Supergraph _ -> true | NotASupergraph -> false
 end
 
-let join _ _ = (* not implemented: use disjunctive domain instead *) assert false
-
 let ( <= ) ~lhs ~rhs =
   (* [lhs] implies [rhs] if it knows more facts than [rhs] *)
   phys_equal lhs rhs || GraphComparison.is_supergraph ~lhs ~rhs GraphComparison.empty_mapping
 
 
-let widen ~prev:_ ~next:_ ~num_iters:_ =
-  (* not implemented: use disjunctive domain instead *) assert false
-
-
 let pp fmt {heap; stack} =
   F.fprintf fmt "{@[<v1> heap=@[<hv>%a@];@;stack=@[<hv>%a@];@]}" Memory.pp heap Stack.pp stack
 

infer/src/pulse/PulseDomain.mli

@@ -31,11 +31,11 @@ end
 
 module Stack : sig
   include
-    AbstractDomain.MapS
+    PrettyPrintable.MonoMap
     with type key = Var.t
      and type value = AbstractAddress.t * Location.t option
 
-  (* need to shadow the declaration in [MapS] even though it is unused since [MapS.compare] has a
+  (* need to shadow the declaration in [MonoMap] even though it is unused since [MapS.compare] has a
      different type *)
   val compare : t -> t -> int [@@warning "-32"]
 end
@@ -83,6 +83,6 @@ type t = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
 
 val initial : t
 
-include AbstractDomain.S with type t := t
+include AbstractDomain.NoJoin with type t := t
 
 val minimize : t -> t