From edba7958253bf60913496ff64a6c8728d82bc2e0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 22 Apr 2020 01:48:32 -0700 Subject: [PATCH] [AI] move disjunctive scheduling to AbstractInterpreter Summary: This is a preparatory diff to make the actual change more readable. This just moves the code around, trying to change it as little as possible. Reviewed By: skcho Differential Revision: D21154065 fbshipit-source-id: e086318c1 --- infer/src/absint/AbstractInterpreter.ml | 149 +++++++++++++++++++++-- infer/src/absint/AbstractInterpreter.mli | 22 ++++ infer/src/absint/TransferFunctions.ml | 125 ------------------- infer/src/absint/TransferFunctions.mli | 22 +--- infer/src/pulse/Pulse.ml | 12 +- 5 files changed, 168 insertions(+), 162 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 6dbbcc545..7de5734eb 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -80,6 +80,134 @@ module type S = sig val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option end +module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> + S with module TransferFunctions = TransferFunctions + +module MakeDisjunctiveTransferFunctions + (T : TransferFunctions.DisjReady) + (DConfig : TransferFunctions.DisjunctiveConfig) = +struct + module CFG = T.CFG + + type extras = T.extras + + module Disjuncts = struct + (* The disjunctive domain transformer should really be part of the Abstract Interpreter instead + of the Transfer Functions as the scheduler needs to know which disjuncts have already been + explored. But for now let's emulate that with a disgusting hack in the transfer functions + that try to skip disjuncts we have already explored, using the [visited] flag. *) + type disjunct = {visited: bool; astate: T.Domain.t} + + let pp_disjunct fmt ({visited; astate}[@warning "+9"]) = + F.fprintf fmt "@[visited=%b;@;@[%a@]@]" visited T.Domain.pp astate + + + type t = disjunct list + + let mk_disjunct astate = {visited= false; astate} + + let singleton astate = [mk_disjunct astate] + + let elements disjuncts = List.map disjuncts ~f:(fun {astate} -> astate) + + let pp f disjuncts = + let pp_disjuncts f disjuncts = + List.iteri disjuncts ~f:(fun i disjunct -> + F.fprintf f "#%d: @[%a@]@;" i pp_disjunct disjunct ) + in + F.fprintf f "@[%d disjuncts:@;%a@]" (List.length disjuncts) pp_disjuncts disjuncts + end + + type disjunct_t = Disjuncts.disjunct = {visited: bool; astate: T.Domain.t} + + module Domain = struct + type t = Disjuncts.t + + let rev_filter_not_over_approximated disjuncts ~not_in = + List.rev_filter disjuncts ~f:(fun disjunct -> + List.exists not_in ~f:(fun disj_not_in -> + T.Domain.leq ~lhs:disjunct.astate ~rhs:disj_not_in.astate ) + |> not ) + + + (* Ignore states in [lhs] that are over-approximated in [rhs] and vice-versa. Favors keeping + states in [lhs]. *) + let join_up_to_imply lhs rhs = + let rev_rhs_not_in_lhs = rev_filter_not_over_approximated rhs ~not_in:lhs in + (* cheeky: this is only used in pulse, whose (<=) is actually a symmetric relation so there's + no need to filter out elements of [lhs] *) + List.rev_append rev_rhs_not_in_lhs lhs + + + let join : t -> t -> t = + fun lhs rhs -> + if phys_equal lhs rhs then lhs + else + match DConfig.join_policy with + | `NeverJoin -> + List.rev_append rhs lhs + | `UnderApproximateAfter n -> + let lhs_length = List.length lhs in + if lhs_length >= n then lhs else List.rev_append rhs lhs + + + let set_visited b disjuncts = + if List.for_all disjuncts ~f:(fun {visited} -> Bool.equal visited b) then disjuncts + else List.map disjuncts ~f:(fun disjunct -> {disjunct with visited= b}) + + + (** check if elements of [disj] appear in [of_] in the same order, using pointer equality on + abstract states to compare elements quickly *) + let rec is_trivial_subset disj ~of_ = + match (disj, of_) with + | [], _ -> + true + | x :: disj', y :: of' when phys_equal x.astate y.astate -> + is_trivial_subset disj' ~of_:of' + | _, _ :: of' -> + is_trivial_subset disj ~of_:of' + | _, [] -> + false + + + let leq ~lhs ~rhs = phys_equal lhs rhs || is_trivial_subset lhs ~of_:rhs + + let widen ~prev ~next ~num_iters = + let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in + if phys_equal prev next || num_iters > max_iter then set_visited false prev + else + let visited_prev = set_visited true prev in + let post = join_up_to_imply visited_prev next in + if leq ~lhs:post ~rhs:prev then set_visited false prev else post + + + let pp = Disjuncts.pp + end + + let exec_instr pre_disjuncts extras node instr = + List.foldi pre_disjuncts ~init:[] ~f:(fun i post_disjuncts pre_disjunct -> + if pre_disjunct.visited then + (* SUBTLE/WORST HACK EVER: ignore pres that we know we have gone through already. This + means that the invariant map at that program point will be junk since they are going to + miss some states, but the overall result will still be ok because the loop heads are + ok. + + This should really be implemented in {!AbstractInterpreter}. *) + post_disjuncts + else ( + L.d_printfln "@[Executing from disjunct #%d@;" i ; + let disjuncts' = + T.exec_instr pre_disjunct.astate extras node instr |> List.map ~f:Disjuncts.mk_disjunct + in + ( if Config.write_html then + let n = List.length disjuncts' in + L.d_printfln "@]@\n@[Got %d disjunct%s back@]" n (if Int.equal n 1 then "" else "s") ) ; + Domain.join post_disjuncts disjuncts' ) ) + + + let pp_session_name node f = T.pp_session_name node f +end + module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = struct module CFG = TransferFunctions.CFG module Node = CFG.Node @@ -179,7 +307,7 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s in (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *) let instrs = if Instrs.is_empty instrs then Instrs.singleton Sil.skip_instr else instrs in - Instrs.fold ~f:compute_post ~init:pre instrs + Instrs.fold ~init:pre ~f:compute_post instrs (* Note on narrowing operations: we defines the narrowing operations simply to take a smaller one. @@ -333,7 +461,10 @@ struct let compute_post ?do_narrowing:_ = make_compute_post ~exec_cfg_internal ~do_narrowing:false end -module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct +module MakeRPO (T : TransferFunctions.SIL) = + MakeWithScheduler (Scheduler.ReversePostorder (T.CFG)) (T) + +module MakeWTO (TransferFunctions : TransferFunctions.SIL) = struct include AbstractInterpreterCommon (TransferFunctions) let debug_wto wto node = @@ -453,9 +584,11 @@ module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct let compute_post ?(do_narrowing = false) = make_compute_post ~exec_cfg_internal ~do_narrowing end -module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> - S with module TransferFunctions = TransferFunctions - -module MakeRPO (T : TransferFunctions.SIL) = - MakeWithScheduler (Scheduler.ReversePostorder (T.CFG)) (T) -module MakeWTO (T : TransferFunctions.SIL) = MakeUsingWTO (T) +module MakeDisjunctive + (T : TransferFunctions.DisjReady) + (DConfig : TransferFunctions.DisjunctiveConfig) = +struct + module DisjT = MakeDisjunctiveTransferFunctions (T) (DConfig) + module Disjuncts = DisjT.Disjuncts + include MakeWTO (DisjT) +end diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index 59be50d28..35184ab4f 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/infer/src/absint/AbstractInterpreter.mli @@ -68,3 +68,25 @@ module MakeRPO : Make module MakeWTO : Make (** create an intraprocedural abstract interpreter from transfer functions using Bourdoncle's strongly connected component weak topological order *) + +(** 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 MakeDisjunctive + (T : TransferFunctions.DisjReady) + (DConfig : TransferFunctions.DisjunctiveConfig) : sig + module Disjuncts : sig + type t + + val singleton : T.Domain.t -> t + + val elements : t -> T.Domain.t list + end + + include + S + with type TransferFunctions.extras = T.extras + and module TransferFunctions.CFG = T.CFG + and type TransferFunctions.Domain.t = Disjuncts.t +end diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index f0f0e5bac..b315ca025 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -6,8 +6,6 @@ *) open! IStd -module F = Format -module L = Logging module type S = sig module CFG : ProcCfg.S @@ -52,126 +50,3 @@ module type DisjReady = sig val pp_session_name : CFG.Node.t -> Format.formatter -> unit end - -module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveConfig) = struct - module CFG = TransferFunctions.CFG - - type extras = TransferFunctions.extras - - module Disjuncts = struct - (* The disjunctive domain transformer should really be part of the Abstract Interpreter instead - of the Transfer Functions as the scheduler needs to know which disjuncts have already been - explored. But for now let's emulate that with a disgusting hack in the transfer functions - that try to skip disjuncts we have already explored, using the [visited] flag. *) - type disjunct = {visited: bool; astate: TransferFunctions.Domain.t} - - let pp_disjunct fmt ({visited; astate}[@warning "+9"]) = - F.fprintf fmt "@[visited=%b;@;@[%a@]@]" visited TransferFunctions.Domain.pp astate - - - type t = disjunct list - - let mk_disjunct astate = {visited= false; astate} - - let singleton astate = [mk_disjunct astate] - - let elements disjuncts = List.map disjuncts ~f:(fun {astate} -> astate) - - let pp f disjuncts = - let pp_disjuncts f disjuncts = - List.iteri disjuncts ~f:(fun i disjunct -> - F.fprintf f "#%d: @[%a@]@;" i pp_disjunct disjunct ) - in - F.fprintf f "@[%d disjuncts:@;%a@]" (List.length disjuncts) pp_disjuncts disjuncts - end - - type disjunct_t = Disjuncts.disjunct = {visited: bool; astate: TransferFunctions.Domain.t} - - module Domain = struct - type t = Disjuncts.t - - let rev_filter_not_over_approximated disjuncts ~not_in = - List.rev_filter disjuncts ~f:(fun disjunct -> - List.exists not_in ~f:(fun disj_not_in -> - TransferFunctions.Domain.leq ~lhs:disjunct.astate ~rhs:disj_not_in.astate ) - |> not ) - - - (* Ignore states in [lhs] that are over-approximated in [rhs] and vice-versa. Favors keeping - states in [lhs]. *) - let join_up_to_imply lhs rhs = - let rev_rhs_not_in_lhs = rev_filter_not_over_approximated rhs ~not_in:lhs in - (* cheeky: this is only used in pulse, whose (<=) is actually a symmetric relation so there's - no need to filter out elements of [lhs] *) - List.rev_append rev_rhs_not_in_lhs lhs - - - let join : t -> t -> t = - fun lhs rhs -> - if phys_equal lhs rhs then lhs - else - match DConfig.join_policy with - | `NeverJoin -> - List.rev_append rhs lhs - | `UnderApproximateAfter n -> - let lhs_length = List.length lhs in - if lhs_length >= n then lhs else List.rev_append rhs lhs - - - let set_visited b disjuncts = - if List.for_all disjuncts ~f:(fun {visited} -> Bool.equal visited b) then disjuncts - else List.map disjuncts ~f:(fun disjunct -> {disjunct with visited= b}) - - - (** check if elements of [disj] appear in [of_] in the same order, using pointer equality on - abstract states to compare elements quickly *) - let rec is_trivial_subset disj ~of_ = - match (disj, of_) with - | [], _ -> - true - | x :: disj', y :: of' when phys_equal x.astate y.astate -> - is_trivial_subset disj' ~of_:of' - | _, _ :: of' -> - is_trivial_subset disj ~of_:of' - | _, [] -> - false - - - let leq ~lhs ~rhs = phys_equal lhs rhs || is_trivial_subset lhs ~of_:rhs - - let widen ~prev ~next ~num_iters = - let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in - if phys_equal prev next || num_iters > max_iter then set_visited false prev - else - let visited_prev = set_visited true prev in - let post = join_up_to_imply visited_prev next in - if leq ~lhs:post ~rhs:prev then set_visited false prev else post - - - let pp = Disjuncts.pp - end - - let exec_instr pre_disjuncts extras node instr = - List.foldi pre_disjuncts ~init:[] ~f:(fun i post_disjuncts pre_disjunct -> - if pre_disjunct.visited then - (* SUBTLE/WORST HACK EVER: ignore pres that we know we have gone through already. This - means that the invariant map at that program point will be junk since they are going to - miss some states, but the overall result will still be ok because the loop heads are - ok. - - This should really be implemented in {!AbstractInterpreter}. *) - post_disjuncts - else ( - L.d_printfln "@[Executing from disjunct #%d@;" i ; - let disjuncts' = - TransferFunctions.exec_instr pre_disjunct.astate extras node instr - |> List.map ~f:Disjuncts.mk_disjunct - in - ( if Config.write_html then - let n = List.length disjuncts' in - L.d_printfln "@]@\n@[Got %d disjunct%s back@]" n (if Int.equal n 1 then "" else "s") ) ; - Domain.join post_disjuncts disjuncts' ) ) - - - let pp_session_name node f = TransferFunctions.pp_session_name node f -end diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index f2a7512a6..67da62eb1 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -47,7 +47,7 @@ module type DisjunctiveConfig = sig (** 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 *) ] + | `NeverJoin (** keep accumulating states *) ] val widen_policy : [`UnderApproximateAfterNumIterations of int] end @@ -63,23 +63,3 @@ module type DisjReady = sig val pp_session_name : CFG.Node.t -> Format.formatter -> unit 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 MakeDisjunctive (TransferFunctions : DisjReady) (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 - SIL - with type extras = TransferFunctions.extras - and module CFG = TransferFunctions.CFG - and type Domain.t = Disjuncts.t -end diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 81a1d4c1e..ff08af419 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -200,8 +200,8 @@ module PulseTransferFunctions = struct let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" end -module DisjunctiveTransferFunctions = - TransferFunctions.MakeDisjunctive +module DisjunctiveAnalyzer = + AbstractInterpreter.MakeDisjunctive (PulseTransferFunctions) (struct let join_policy = @@ -211,8 +211,6 @@ module DisjunctiveTransferFunctions = let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold end) -module DisjunctiveAnalyzer = AbstractInterpreter.MakeWTO (DisjunctiveTransferFunctions) - (* Output cases that sledge was unhappy with in files for later replay or inclusion as sledge test cases. We create one file for each PID to avoid all analysis processes racing on writing to the same file. *) @@ -234,9 +232,7 @@ let checker {Callbacks.exe_env; summary} = let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in AbstractValue.State.reset () ; let pdesc = Summary.get_proc_desc summary in - let initial = - DisjunctiveTransferFunctions.Disjuncts.singleton (ExecutionDomain.mk_initial pdesc) - in + let initial = DisjunctiveAnalyzer.Disjuncts.singleton (ExecutionDomain.mk_initial pdesc) in let get_formals callee_pname = Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals in @@ -244,7 +240,7 @@ let checker {Callbacks.exe_env; summary} = match DisjunctiveAnalyzer.compute_post proc_data ~initial with | Some posts -> PulsePayload.update_summary - (PulseSummary.of_posts pdesc (DisjunctiveTransferFunctions.Disjuncts.elements posts)) + (PulseSummary.of_posts pdesc (DisjunctiveAnalyzer.Disjuncts.elements posts)) summary | None -> summary