[HIL][disjunctive] allow underlying transfer function to return disjunctions

Summary:
This will allow disjunctive analyzers to return sets of states as a
result instead of always returning one state. More precisely, this will
be needed for pulse when it becomes inter-procedural, if we take
summaries of functions to be disjunctive too (like, e.g., biabduction
does with several specs per function).

Reviewed By: mbouaziz

Differential Revision: D13537601

fbshipit-source-id: f54caf802

infer/src/absint/TransferFunctions.ml

@@ -34,30 +34,43 @@ module type MakeHIL = functor (C : ProcCfg.S) -> sig
 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
+module type DisjReady = sig
-    (TransferFunctions : HIL)
+  module CFG : ProcCfg.S
-    (DConfig : DisjunctiveConfig with type domain_t = TransferFunctions.Domain.t) =
+
-struct
+  module Domain : AbstractDomain.S
+
+  module DisjunctiveDomain : Caml.Set.S with type elt = Domain.t
+
+  type extras
+
+  type instr
+
+  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> DisjunctiveDomain.t
+
+  val pp_session_name : CFG.Node.t -> Format.formatter -> unit
+end
+
+module type HILDisjReady = sig
+  include DisjReady with type instr := HilInstr.t
+end
+
+module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : DisjunctiveConfig) = struct
   module CFG = TransferFunctions.CFG
 
   type extras = TransferFunctions.extras
 
   module Domain = struct
-    module Set = AbstractDomain.FiniteSet (struct
+    module Set = TransferFunctions.DisjunctiveDomain
-      include TransferFunctions.Domain
-
-      let compare = DConfig.compare_domain_t
-    end)
 
-    let real_join lhs rhs =
+    let join lhs rhs =
-      let union = Set.join lhs rhs in
+      if phys_equal lhs rhs then lhs
+      else
+        let union = Set.union lhs rhs in
         match DConfig.join_policy with
         | `NeverJoin ->
             union
@@ -79,23 +92,28 @@ struct
               Set.singleton (Option.value_exn joined)
 
 
-    let real_widen ~prev ~next ~num_iters =
+    let widen ~prev ~next ~num_iters =
+      if phys_equal prev next then prev
+      else
         let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in
-      if num_iters > max_iter then prev else real_join prev next
+        if num_iters > max_iter then prev else join prev next
 
 
-    include Set
+    let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else Set.subset lhs rhs
+
+    let pp f set =
+      PrettyPrintable.pp_collection ~pp_item:TransferFunctions.Domain.pp f (Set.elements set)
 
-    let join = real_join
 
-    let widen = real_widen
+    include Set
   end
 
   let exec_instr disj_dom extras node instr =
-    Domain.map (fun dom -> TransferFunctions.exec_instr dom extras node instr) disj_dom
+    Domain.fold
+      (fun dom result ->
+        TransferFunctions.exec_instr dom extras node instr |> Domain.Set.union result )
+      disj_dom Domain.Set.empty
 
 
   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

@@ -38,9 +38,6 @@ module type HIL = sig
 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
@@ -54,14 +51,34 @@ module type DisjunctiveConfig = sig
   val widen_policy : [`UnderApproximateAfterNumIterations of int]
 end
 
+module type DisjReady = sig
+  module CFG : ProcCfg.S
+
+  module Domain : AbstractDomain.S
+
+  module DisjunctiveDomain : Caml.Set.S with type elt = Domain.t
+
+  type extras
+
+  type instr
+
+  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> DisjunctiveDomain.t
+
+  val pp_session_name : CFG.Node.t -> Format.formatter -> unit
+end
+
+module type HILDisjReady = sig
+  include DisjReady with type instr := HilInstr.t
+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
+module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : DisjunctiveConfig) : sig
-    (TransferFunctions : HIL)
+  include
-    (DConfig : DisjunctiveConfig with type domain_t = TransferFunctions.Domain.t) : sig
+    HIL
-  include HIL with type extras = TransferFunctions.extras and module CFG = TransferFunctions.CFG
+    with type extras = TransferFunctions.extras
-
+     and module CFG = TransferFunctions.CFG
-  val of_domain : DConfig.domain_t -> Domain.t
+     and type Domain.t = TransferFunctions.DisjunctiveDomain.t
 end

infer/src/checkers/Pulse.ml

@@ -24,9 +24,10 @@ let check_error summary = function
       raise_notrace AbstractDomain.Stop_analysis
 
 
-module PulseTransferFunctions (CFG : ProcCfg.S) = struct
+module PulseTransferFunctions = struct
-  module CFG = CFG
+  module CFG = ProcCfg.Exceptional
   module Domain = PulseDomain
+  module DisjunctiveDomain = Caml.Set.Make (Domain)
 
   type extras = Summary.t
 
@@ -137,14 +138,16 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
       =
     match instr with
     | Assign (lhs_access, rhs_exp, loc) ->
-        exec_assign summary lhs_access rhs_exp loc astate |> check_error summary
+        exec_assign summary lhs_access rhs_exp loc astate
+        |> check_error summary |> DisjunctiveDomain.singleton
     | Assume (condition, _, _, loc) ->
         PulseOperations.read_all loc (HilExp.get_access_exprs condition) astate
-        |> check_error summary
+        |> check_error summary |> DisjunctiveDomain.singleton
     | Call (ret, call, actuals, flags, loc) ->
-        dispatch_call summary ret call actuals flags loc astate |> check_error summary
+        dispatch_call summary ret call actuals flags loc astate
+        |> check_error summary |> DisjunctiveDomain.singleton
     | ExitScope (vars, _) ->
-        PulseOperations.remove_vars vars astate
+        PulseOperations.remove_vars vars astate |> DisjunctiveDomain.singleton
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
@@ -154,11 +157,8 @@ module HilConfig = LowerHil.DefaultConfig
 
 module DisjunctiveTransferFunctions =
   TransferFunctions.MakeHILDisjunctive
-    (PulseTransferFunctions
+    (PulseTransferFunctions)
-       (ProcCfg.Exceptional))
     (struct
-         type domain_t = PulseDomain.t [@@deriving compare]
-
       let join_policy =
         match Config.pulse_max_disjuncts with 0 -> `NeverJoin | n -> `UnderApproximateAfter n
 
@@ -176,6 +176,6 @@ let checker {Callbacks.proc_desc; tenv; summary} =
   ( try
       ignore
         (DisjunctiveAnalyzer.compute_post proc_data
-           ~initial:(DisjunctiveTransferFunctions.of_domain PulseDomain.initial))
+           ~initial:(PulseTransferFunctions.DisjunctiveDomain.singleton PulseDomain.initial))
     with AbstractDomain.Stop_analysis -> () ) ;
   summary