pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[AI] move disjunctive scheduling to AbstractInterpreter

Browse Source 
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
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent 60184a5e73
commit edba795825
5 changed files with 168 additions and 162 deletions
Show Stats Download Patch File Download Diff File

149
infer/src/absint/AbstractInterpreter.ml
Unescape View File

@ -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 "@[<hv>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 "@[<v>%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 "@[<v2>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

22
infer/src/absint/AbstractInterpreter.mli
Unescape View File

@ -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

125
infer/src/absint/TransferFunctions.ml
Unescape View File

@ -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 "@[<hv>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 "@[<v>%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 "@[<v2>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

22
infer/src/absint/TransferFunctions.mli
Unescape View File

@ -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

12
infer/src/pulse/Pulse.ml
Unescape View File

@ -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

Write Preview
Loading…
Cancel
Save