[AI][pulse] lists of disjuncts instead of sets

Summary:
The disjunctive domain shouldn't really be a set in the first place as
comparing abstract states for equality is expensive to do naively
(walking the whole maps representing the abstract heap). Moreover in
practice these sets have a small max size (currently 50 for pulse, the
only client), so switching them to plain lists makes sense.

Reviewed By: mbouaziz

Differential Revision: D14258489

fbshipit-source-id: c512169eb

infer/src/absint/TransferFunctions.ml

@@ -44,13 +44,11 @@ module type DisjReady = sig
 
   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 exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t list
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
@@ -64,41 +62,64 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct
 
   type extras = TransferFunctions.extras
 
+  module Disjuncts = struct
+    type disjunct = TransferFunctions.Domain.t
+
+    let pp_disjunct fmt astate = TransferFunctions.Domain.pp fmt astate
+
+    type t = disjunct list
+
+    let mk_disjunct astate = astate
+
+    let singleton astate = [mk_disjunct astate]
+
+    let elements disjuncts = disjuncts
+
+    let pp f disjuncts = PrettyPrintable.pp_collection ~pp_item:pp_disjunct f disjuncts
+  end
+
   module Domain = struct
-    module Set = TransferFunctions.DisjunctiveDomain
+    type t = Disjuncts.t
+
+    let join_normalize_into s_froms ~into:s_intos =
+      let s_from_not_in_intos =
+        List.rev_filter s_froms ~f:(fun s_from ->
+            List.exists s_intos ~f:(fun s_into -> phys_equal s_from s_into) |> not )
+      in
+      List.rev_append s_from_not_in_intos s_intos
+
 
-    let join lhs rhs =
+    let join : t -> t -> t =
+     fun lhs rhs ->
       if phys_equal lhs rhs then lhs
       else
-        let union = Set.union lhs rhs in
         match DConfig.join_policy with
         | `NeverJoin ->
-            union
+            rhs @ lhs
         | `UnderApproximateAfter n ->
-            if Set.cardinal union <= n then union else lhs
+            let lhs_length = List.length lhs in
+            if lhs_length >= n then lhs else join_normalize_into rhs ~into:lhs
 
 
-    let widen ~prev ~next ~num_iters =
-      if phys_equal prev next then prev
+    let rec ( <= ) ~lhs ~rhs =
+      if phys_equal lhs rhs then (* also takes care of the case [lhs = rhs = []] *) true
       else
-        let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in
-        if num_iters > max_iter then prev else join prev next
-
+        (* quick check: [lhs <= rhs] if [rhs] is [something @ lhs] *)
+        match rhs with [] -> false | _ :: rhs' -> ( <= ) ~lhs ~rhs:rhs'
 
-    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 widen ~prev ~next ~num_iters =
+      let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in
+      if phys_equal prev next then prev else if num_iters > max_iter then prev else join prev next
 
 
-    include Set
+    let pp = Disjuncts.pp
   end
 
-  let exec_instr disj_dom extras node instr =
-    Domain.fold
-      (fun dom result ->
-        TransferFunctions.exec_instr dom extras node instr |> Domain.Set.union result )
-      disj_dom Domain.Set.empty
+  let exec_instr pre_disjuncts extras node instr =
+    List.fold pre_disjuncts ~init:[] ~f:(fun post_disjuncts pre_disjunct ->
+        let disjuncts' = TransferFunctions.exec_instr pre_disjunct extras node instr in
+        Domain.join post_disjuncts (List.map disjuncts' ~f:Disjuncts.mk_disjunct) )
 
 
   let pp_session_name node f = TransferFunctions.pp_session_name node f

infer/src/absint/TransferFunctions.mli

@@ -53,13 +53,11 @@ module type DisjReady = sig
 
   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 exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t list
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
@@ -73,9 +71,17 @@ end
    disjunct independently. The join on the disjunctive state is governed by the policy described in
    [DConfig]. *)
 module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : DisjunctiveConfig) : sig
+  module Disjuncts : sig
+    type t
+
+    val singleton : TransferFunctions.Domain.t -> t
+
+    val elements : t -> TransferFunctions.Domain.t list [@@warning "-32"]
+  end
+
   include
     HIL
     with type extras = TransferFunctions.extras
      and module CFG = TransferFunctions.CFG
-     and type Domain.t = TransferFunctions.DisjunctiveDomain.t
+     and type Domain.t = Disjuncts.t
 end

infer/src/checkers/Pulse.ml

@@ -27,7 +27,6 @@ let check_error summary = function
 module PulseTransferFunctions = struct
   module CFG = ProcCfg.Exceptional
   module Domain = PulseDomain
-  module DisjunctiveDomain = Caml.Set.Make (Domain)
 
   type extras = Summary.t
 
@@ -138,16 +137,22 @@ module PulseTransferFunctions = struct
       =
     match instr with
     | Assign (lhs_access, rhs_exp, loc) ->
-        exec_assign summary lhs_access rhs_exp loc astate
-        |> check_error summary |> DisjunctiveDomain.singleton
+        let post = exec_assign summary lhs_access rhs_exp loc astate |> check_error summary in
+        [post]
     | Assume (condition, _, _, loc) ->
-        PulseOperations.read_all loc (HilExp.get_access_exprs condition) astate
-        |> check_error summary |> DisjunctiveDomain.singleton
+        let post =
+          PulseOperations.read_all loc (HilExp.get_access_exprs condition) astate
+          |> check_error summary
+        in
+        [post]
     | Call (ret, call, actuals, flags, loc) ->
-        dispatch_call summary ret call actuals flags loc astate
-        |> check_error summary |> DisjunctiveDomain.singleton
+        let post =
+          dispatch_call summary ret call actuals flags loc astate |> check_error summary
+        in
+        [post]
     | ExitScope (vars, _) ->
-        PulseOperations.remove_vars vars astate |> DisjunctiveDomain.singleton
+        let post = PulseOperations.remove_vars vars astate in
+        [post]
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
@@ -176,6 +181,6 @@ let checker {Callbacks.proc_desc; tenv; summary} =
   ( try
       ignore
         (DisjunctiveAnalyzer.compute_post proc_data
-           ~initial:(PulseTransferFunctions.DisjunctiveDomain.singleton PulseDomain.initial))
+           ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseDomain.initial))
     with AbstractDomain.Stop_analysis -> () ) ;
   summary

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -1,5 +1,5 @@
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58 here,accessed `*(ptr)` here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68 here,accessed `ptr` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70 here,accessed `ptr` here]
 codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S_S(&(s),&(0$?%__sil_tmpSIL_materialize_temp__n$12))`,`&(s)` captured as `s`,invalidated by destructor call `S_~S(s)` at line 29 here,accessed `&(f)` here]
 codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S_S(&(s))`,`&(s)` captured as `s`,invalidated by destructor call `S_~S(s)` at line 20 here,accessed `&(f)` here]
 codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 25 here,accessed `*(result)` here]