From 156f5946c201c6e8d51cdb84f1714e48c82d3488 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 13 Dec 2018 03:00:09 -0800 Subject: [PATCH] [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 | 71 ++++++++++++++++++++++++++ infer/src/absint/TransferFunctions.mli | 29 +++++++++++ infer/src/checkers/Pulse.ml | 24 +++++++-- infer/src/checkers/PulseDomain.ml | 19 ++++--- infer/src/checkers/PulseDomain.mli | 2 + 5 files changed, 135 insertions(+), 10 deletions(-) diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index b18cc0d0d..42424550e 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/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 diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index a09092183..99b3eb8dc 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/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 diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 97f6377d3..fd673afc0 100644 --- a/infer/src/checkers/Pulse.ml +++ b/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 diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index c936fbb65..e6542e46e 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/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 diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 9ed2e7f57..82345f91d 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -15,6 +15,8 @@ end include AbstractDomain.S +val compare : t -> t -> int + module AbstractAddressSet : sig type t end