[HIL][pulse] add disjunctive domain

Summary:
Introduce machinery to do disjunctive HIL domains and use it for pulse,
but only in a mode that preserves the existing behaviour.

The disjunctive domain is a functor that turns any (HIL for now)
transfer function module into one operating on sets of elements of the
original domain. The behaviour of joins (and widenings, which are equal
to joins) can be chosen when instantiating the functor among 3
behaviours:

- `` `JoinAfter n`: when the set of disjuncts gets bigger than `n` the
underlying domain's join is called to collapse them into one state

- `` `UnderApproximateAfter n`: when the sest 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`

The widening is always of the form ``
`UnderApproximateAfterNumIterations max_iter` for now since the only
user is pulse and I'm not sure what else would be useful.

Picking `` `JoinAfter 0` gives the same results as the non-disjunctive
domain since the underlying `join` will always be called. Make pulse use
this mode for now, and tune it in a next diff.

Reviewed By: mbouaziz

Differential Revision: D13431375

fbshipit-source-id: b93aa50e7

infer/src/absint/TransferFunctions.ml

@@ -28,3 +28,74 @@ end
 module type HIL = sig
   include S with type instr := HilInstr.t
 end
+
+module type MakeHIL = functor (C : ProcCfg.S) -> sig
+  include HIL with module CFG = C
+end
+
+module type DisjunctiveConfig = sig
+  type domain_t [@@deriving compare]
+
+  val join_policy : [`JoinAfter of int | `UnderApproximateAfter of int | `NeverJoin]
+
+  val widen_policy : [`UnderApproximateAfterNumIterations of int]
+end
+
+module MakeHILDisjunctive
+    (TransferFunctions : HIL)
+    (DConfig : DisjunctiveConfig with type domain_t = TransferFunctions.Domain.t) =
+struct
+  module CFG = TransferFunctions.CFG
+
+  type extras = TransferFunctions.extras
+
+  module Domain = struct
+    module Set = AbstractDomain.FiniteSet (struct
+      include TransferFunctions.Domain
+
+      let compare = DConfig.compare_domain_t
+    end)
+
+    let real_join lhs rhs =
+      let union = Set.join lhs rhs in
+      match DConfig.join_policy with
+      | `NeverJoin ->
+          union
+      | `UnderApproximateAfter n ->
+          if Set.cardinal union <= n then union else lhs
+      | `JoinAfter n ->
+          if Set.cardinal union <= n then union
+          else
+            let joined =
+              Set.fold
+                (fun dom joined ->
+                  match joined with
+                  | None ->
+                      Some dom
+                  | Some joined ->
+                      Some (TransferFunctions.Domain.join dom joined) )
+                union None
+            in
+            Set.singleton (Option.value_exn joined)
+
+
+    let real_widen ~prev ~next ~num_iters =
+      let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in
+      if num_iters > max_iter then prev else real_join prev next
+
+
+    include Set
+
+    let join = real_join
+
+    let widen = real_widen
+  end
+
+  let exec_instr disj_dom extras node instr =
+    Domain.map (fun dom -> TransferFunctions.exec_instr dom extras node instr) disj_dom
+
+
+  let pp_session_name node f = TransferFunctions.pp_session_name node f
+
+  let of_domain x = Domain.singleton x
+end

infer/src/absint/TransferFunctions.mli

@@ -36,3 +36,32 @@ end
 module type HIL = sig
   include S with type instr := HilInstr.t
 end
+
+module type DisjunctiveConfig = sig
+  (** the underlying domain *)
+  type domain_t [@@deriving compare]
+
+  val join_policy :
+    [ `JoinAfter of int
+      (** when the set of disjuncts gets bigger than [n] the underlying domain's join is called to
+       collapse them into one state *)
+    | `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 accumaluting states *) ]
+
+  val widen_policy : [`UnderApproximateAfterNumIterations of int]
+end
+
+(** In the disjunctive interpreter, the domain is a set of abstract states representing a
+   disjunction between these states. The transfer functions are executed on each state in the
+   disjunct independently. The join on the disjunctive state is governed by the policy described in
+   [DConfig]. *)
+module MakeHILDisjunctive
+    (TransferFunctions : HIL)
+    (DConfig : DisjunctiveConfig with type domain_t = TransferFunctions.Domain.t) : sig
+  include HIL with type extras = TransferFunctions.extras and module CFG = TransferFunctions.CFG
+
+  val of_domain : DConfig.domain_t -> Domain.t
+end

infer/src/checkers/Pulse.ml

@@ -24,7 +24,7 @@ let check_error summary = function
       raise_notrace AbstractDomain.Stop_analysis
 
 
-module TransferFunctions (CFG : ProcCfg.S) = struct
+module PulseTransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = PulseDomain
 
@@ -133,13 +133,29 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 end
 
 module HilConfig = LowerHil.DefaultConfig
-module Analyzer =
+
+module DisjunctiveTransferFunctions =
+  TransferFunctions.MakeHILDisjunctive
+    (PulseTransferFunctions
+       (ProcCfg.Exceptional))
+       (struct
+         type domain_t = PulseDomain.t [@@deriving compare]
+
+         let join_policy = `JoinAfter 1
+
+         let widen_policy = `UnderApproximateAfterNumIterations 5
+       end)
+
+module DisjunctiveAnalyzer =
   LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeWTO) (HilConfig)
-    (TransferFunctions (ProcCfg.Exceptional))
+    (DisjunctiveTransferFunctions)
 
 let checker {Callbacks.proc_desc; tenv; summary} =
   let proc_data = ProcData.make proc_desc tenv summary in
   PulseDomain.AbstractAddress.init () ;
-  ( try ignore (Analyzer.compute_post proc_data ~initial:PulseDomain.initial)
+  ( try
+      ignore
+        (DisjunctiveAnalyzer.compute_post proc_data
+           ~initial:(DisjunctiveTransferFunctions.of_domain PulseDomain.initial))
     with AbstractDomain.Stop_analysis -> () ) ;
   summary

infer/src/checkers/PulseDomain.ml

@@ -87,7 +87,7 @@ module Memory : sig
 
   type cell = edges * Attributes.t
 
-  type t
+  type t [@@deriving compare]
 
   val empty : t
 
@@ -124,13 +124,13 @@ end = struct
 
   module Edges = PrettyPrintable.MakePPMap (Access)
 
-  type edges = AbstractAddressSet.t Edges.t
+  type edges = AbstractAddressSet.t Edges.t [@@deriving compare]
 
-  type cell = edges * Attributes.t
+  type cell = edges * Attributes.t [@@deriving compare]
 
   module Graph = PrettyPrintable.MakePPMap (AbstractAddress)
 
-  type t = cell Graph.t
+  type t = cell Graph.t [@@deriving compare]
 
   let pp =
     Graph.pp ~pp_value:(Pp.pair ~fst:(Edges.pp ~pp_value:AbstractAddressSet.pp) ~snd:Attributes.pp)
@@ -238,10 +238,14 @@ end
     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 = AbstractDomain.Map (Var) (AbstractAddressSet)
+module Stack = struct
+  include AbstractDomain.Map (Var) (AbstractAddressSet)
+
+  let compare = compare AbstractAddressSet.compare
+end
 
 (** the domain *)
-type astate = {heap: Memory.t; stack: Stack.t}
+type astate = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
 
 let initial =
   { heap=
@@ -830,4 +834,7 @@ module StdVector = struct
 end
 
 include Domain
+
+let compare = compare_astate
+
 include Operations

infer/src/checkers/PulseDomain.mli

@@ -15,6 +15,8 @@ end
 
 include AbstractDomain.S
 
+val compare : t -> t -> int
+
 module AbstractAddressSet : sig
   type t
 end