From a19db6605c4f962e5284ea7a400ae2f11e5c866d Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 5 Mar 2019 09:34:28 -0800 Subject: [PATCH] [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 | 65 ++++++++++++------- infer/src/absint/TransferFunctions.mli | 14 ++-- infer/src/checkers/Pulse.ml | 23 ++++--- .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 +- 4 files changed, 68 insertions(+), 36 deletions(-) diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index a39e33074..fb2169fcd 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/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 diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index d058b3320..70f2d34ff 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/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 diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index a614ab4de..2e31da946 100644 --- a/infer/src/checkers/Pulse.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 379f2ef66..571a15739 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/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]