[absint][pulse] Remove NeverJoin

Summary: There used to be `JoinAfter n` mode where we would try to join `n` states instead of always making disjunctions. It got deleted in D14258485 and Pulse's underlying (pre-disjuncts) domain doesn't even have a join operation.  `NeverJoin` mode is not useful in Pulse anymore: pulse will diverge or OOM if we don't limit the number of disjuncts. It is also not used by any other analyzer.  Let's remove it.

Reviewed By: jvillard

Differential Revision: D22817425

fbshipit-source-id: 1e658f11d

infer/src/absint/AbstractInterpreter.ml

@@ -132,10 +132,7 @@ struct
       fun lhs rhs ->
         if phys_equal lhs rhs then lhs
         else
-          match DConfig.join_policy with
-          | `NeverJoin ->
-              List.rev_append rhs lhs
-          | `UnderApproximateAfter n ->
+          let (`UnderApproximateAfter n) = DConfig.join_policy in
           let lhs_length = List.length lhs in
           if lhs_length >= n then lhs else list_rev_append rhs lhs (n - lhs_length)
 

infer/src/absint/TransferFunctions.ml

@@ -34,7 +34,7 @@ module type MakeHIL = functor (C : ProcCfg.S) -> sig
 end
 
 module type DisjunctiveConfig = sig
-  val join_policy : [`UnderApproximateAfter of int | `NeverJoin]
+  val join_policy : [`UnderApproximateAfter of int]
 
   val widen_policy : [`UnderApproximateAfterNumIterations of int]
 end

infer/src/absint/TransferFunctions.mli

@@ -46,8 +46,7 @@ module type DisjunctiveConfig = sig
     [ `UnderApproximateAfter of int
       (** When the set of disjuncts gets bigger than [n] then just stop adding new states to it,
           drop any further states on the floor. This corresponds to an under-approximation/bounded
-          approach. *)
-    | `NeverJoin  (** keep accumulating states *) ]
+          approach. *) ]
 
   val widen_policy : [`UnderApproximateAfterNumIterations of int]
 end

infer/src/pulse/Pulse.ml

@@ -294,9 +294,7 @@ module DisjunctiveAnalyzer =
   AbstractInterpreter.MakeDisjunctive
     (PulseTransferFunctions)
     (struct
-      let join_policy =
-        match Config.pulse_max_disjuncts with 0 -> `NeverJoin | n -> `UnderApproximateAfter n
-
+      let join_policy = `UnderApproximateAfter Config.pulse_max_disjuncts
 
       let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold
     end)