diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 42424550e..7ebff2594 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -34,68 +34,86 @@ 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 - (TransferFunctions : HIL) - (DConfig : DisjunctiveConfig with type domain_t = TransferFunctions.Domain.t) = -struct +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 + +module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : DisjunctiveConfig) = 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 + module Set = TransferFunctions.DisjunctiveDomain + + let join lhs rhs = + if phys_equal lhs rhs then lhs + else + let union = Set.union 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 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 join prev next + + + 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) 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 + 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 diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 99b3eb8dc..41c3cbdc3 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/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 - (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 +module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : DisjunctiveConfig) : sig + include + HIL + with type extras = TransferFunctions.extras + and module CFG = TransferFunctions.CFG + and type Domain.t = TransferFunctions.DisjunctiveDomain.t end diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 4c3af9ab1..a614ab4de 100644 --- a/infer/src/checkers/Pulse.ml +++ b/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 CFG = CFG +module PulseTransferFunctions = struct + 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,17 +157,14 @@ module HilConfig = LowerHil.DefaultConfig module DisjunctiveTransferFunctions = TransferFunctions.MakeHILDisjunctive - (PulseTransferFunctions - (ProcCfg.Exceptional)) - (struct - type domain_t = PulseDomain.t [@@deriving compare] + (PulseTransferFunctions) + (struct + let join_policy = + match Config.pulse_max_disjuncts with 0 -> `NeverJoin | n -> `UnderApproximateAfter n - let join_policy = - match Config.pulse_max_disjuncts with 0 -> `NeverJoin | n -> `UnderApproximateAfter n - - let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold - end) + let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold + end) module DisjunctiveAnalyzer = LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeWTO) (HilConfig) @@ -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