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

factoring Node module out of CFG

Browse Source 
Reviewed By: jberdine

Differential Revision: D3273314

fbshipit-source-id: fe32f82
master
Sam Blackshear 9 years ago committed by Facebook Github Bot 5
parent f4335c7c4a
commit 0becc32a88
9 changed files with 152 additions and 123 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/backend/preanal.ml
Unescape View File

@ -473,7 +473,7 @@ module NullifyDomain = AbstractDomain.Pair (VarDomain) (VarDomain)
module NullifyTransferFunctions = struct
type astate = NullifyDomain.astate
type extras = LivenessAnalysis.inv_map
type node_id = BackwardCfg.node_id
type node_id = BackwardCfg.id
let postprocess ((reaching_defs, _) as astate) node_id { ProcData.extras; } =
match LivenessAnalysis.extract_state node_id extras with

34
infer/src/checkers/abstractInterpreter.ml
Unescape View File

@ -12,13 +12,13 @@ open! Utils
module L = Logging
module Make
(C : ProcCfg.Wrapper)
(CFG : ProcCfg.S)
(Sched : Scheduler.S)
(A : AbstractDomain.S)
(T : TransferFunctions.S with type astate = A.astate and type node_id = C.node_id) = struct
(T : TransferFunctions.S with type astate = A.astate and type node_id = CFG.id) = struct
module S = Sched (C)
module M = ProcCfg.NodeIdMap (C)
module S = Sched (CFG)
module M = ProcCfg.NodeIdMap (CFG)
type state = { pre: A.astate; post: A.astate; visit_count: int; }
(* invariant map from node id -> abstract state representing postcondition for node id *)
@ -29,7 +29,7 @@ module Make
try
Some (M.find node_id inv_map)
with Not_found ->
L.err "Warning: No state found for node %a" C.pp_id node_id;
L.err "Warning: No state found for node %a" CFG.pp_id node_id;
None
(** extract the postcondition of node [n] from [inv_map] *)
@ -45,17 +45,17 @@ module Make
| None -> None
let exec_node node astate_pre work_queue inv_map proc_data =
let node_id = C.id node in
L.out "Doing analysis of node %a from pre %a@." C.pp_id node_id A.pp astate_pre;
let node_id = CFG.id node in
L.out "Doing analysis of node %a from pre %a@." CFG.pp_id node_id A.pp astate_pre;
let update_inv_map astate_pre visit_count =
let astate_post =
let exec_instrs astate_acc instr =
if A.is_bottom astate_acc
then astate_acc
else T.exec_instr astate_acc proc_data instr in
let astate_post_instrs = IList.fold_left exec_instrs astate_pre (C.instrs node) in
let astate_post_instrs = IList.fold_left exec_instrs astate_pre (CFG.instrs node) in
T.postprocess astate_post_instrs node_id proc_data in
L.out "Post for node %a is %a@." C.pp_id node_id A.pp astate_post;
L.out "Post for node %a is %a@." CFG.pp_id node_id A.pp astate_post;
let inv_map' = M.add node_id { pre=astate_pre; post=astate_post; visit_count; } inv_map in
inv_map', S.schedule_succs work_queue node in
if M.mem node_id inv_map then
@ -82,11 +82,11 @@ module Make
let rec exec_worklist cfg work_queue inv_map proc_data =
let compute_pre node inv_map =
(* if the [pred] -> [node] transition was normal, use post([pred]) *)
let extract_post_ pred = extract_post (C.id pred) inv_map in
let normal_posts = IList.map extract_post_ (C.normal_preds cfg node) in
let extract_post_ pred = extract_post (CFG.id pred) inv_map in
let normal_posts = IList.map extract_post_ (CFG.normal_preds cfg node) in
(* if the [pred] -> [node] transition was exceptional, use pre([pred]) *)
let extract_pre_f acc pred = extract_pre (C.id pred) inv_map :: acc in
let all_posts = IList.fold_left extract_pre_f normal_posts (C.exceptional_preds cfg node) in
let extract_pre_f acc pred = extract_pre (CFG.id pred) inv_map :: acc in
let all_posts = IList.fold_left extract_pre_f normal_posts (CFG.exceptional_preds cfg node) in
match IList.flatten_options all_posts with
| post :: posts -> Some (IList.fold_left A.join post posts)
| [] -> None in
@ -103,20 +103,20 @@ module Make
(* compute and return an invariant map for [cfg] *)
let exec_cfg cfg proc_data =
let start_node = C.start_node cfg in
let start_node = CFG.start_node cfg in
let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty proc_data in
exec_worklist cfg work_queue' inv_map' proc_data
(* compute and return an invariant map for [pdesc] *)
let exec_pdesc ({ ProcData.pdesc; } as proc_data) =
L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc);
exec_cfg (C.from_pdesc pdesc) proc_data
exec_cfg (CFG.from_pdesc pdesc) proc_data
(* compute and return the postcondition of [pdesc] *)
let compute_post ({ ProcData.pdesc; } as proc_data) =
let cfg = C.from_pdesc pdesc in
let cfg = CFG.from_pdesc pdesc in
let inv_map = exec_cfg cfg proc_data in
extract_post (C.id (C.exit_node cfg)) inv_map
extract_post (CFG.id (CFG.exit_node cfg)) inv_map
module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct

2
infer/src/checkers/addressTaken.ml
Unescape View File

@ -20,7 +20,7 @@ module Domain = AbstractDomain.FiniteSet(PvarSet)
module TransferFunctions = struct
type astate = Domain.astate
type extras = ProcData.no_extras
type node_id = Cfg.Node.id
type node_id = ProcCfg.DefaultNode.id
let postprocess = TransferFunctions.no_postprocessing

2
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -304,7 +304,7 @@ let report_allocations pname loc calls =
module TransferFunctions = struct
type astate = Domain.astate
type extras = ProcData.no_extras
type node_id = Cfg.Node.id
type node_id = ProcCfg.DefaultNode.id
let postprocess = TransferFunctions.no_postprocessing

104
infer/src/checkers/procCfg.ml
Unescape View File

@ -12,25 +12,39 @@ open! Utils
module F = Format
(** Control-flow graph for a single procedure (as opposed to cfg.ml, which represents a cfg for a
file). *)
file). Defines useful wrappers that allows us to do tricks like turn a forward cfg into a
backward one, or view a cfg as having a single instruction per node. *)
module type Base = sig
module type Node = sig
type t
type id
val instrs : t -> Sil.instr list
val kind : t -> Cfg.Node.nodekind
val id : t -> id
val id_compare : id -> id -> int
val pp_id : F.formatter -> id -> unit
end
module DefaultNode = struct
type t = Cfg.Node.t
type id = Cfg.Node.id
let instrs = Cfg.Node.get_instrs
let kind = Cfg.Node.get_kind
let id = Cfg.Node.get_id
let id_compare = Cfg.Node.id_compare
let pp_id = Cfg.Node.pp_id
end
module type S = sig
type t
type node
type node_id
include (Node with type t := node)
val id : node -> node_id
val id_compare : node_id -> node_id -> int
(** all successors (normal and exceptional) *)
val succs : t -> node -> node list
(** all predecessors (normal and exceptional) *)
val preds : t -> node -> node list
end
(** Wrapper that allows us to do tricks like turn a forward cfg to into a backward one *)
module type Wrapper = sig
include Base
(** non-exceptional successors *)
val normal_succs : t -> node -> node list
(** non-exceptional predecessors *)
@ -41,24 +55,17 @@ module type Wrapper = sig
val exceptional_preds : t -> node -> node list
val start_node : t -> node
val exit_node : t -> node
val instrs : node -> Sil.instr list
val kind : node -> Cfg.Node.nodekind
val proc_desc : t -> Cfg.Procdesc.t
val nodes : t -> node list
val from_pdesc : Cfg.Procdesc.t -> t
val pp_node : F.formatter -> node -> unit
val pp_id : F.formatter -> node_id -> unit
end
(** Forward CFG with no exceptional control-flow *)
module Normal = struct
type t = Cfg.Procdesc.t
type node = Cfg.node
type node_id = Cfg.Node.id
type node = DefaultNode.t
include (DefaultNode : module type of DefaultNode with type t := node)
let id = Cfg.Node.get_id
let normal_succs _ n = Cfg.Node.get_succs n
let normal_preds _ n = Cfg.Node.get_preds n
(* prune away exceptional control flow *)
@ -68,25 +75,17 @@ module Normal = struct
let preds = normal_preds
let start_node = Cfg.Procdesc.get_start_node
let exit_node = Cfg.Procdesc.get_exit_node
let instrs = Cfg.Node.get_instrs
let kind = Cfg.Node.get_kind
let proc_desc t = t
let nodes = Cfg.Procdesc.get_nodes
let from_pdesc pdesc = pdesc
let id_compare = Cfg.Node.id_compare
let pp_node = Cfg.Node.pp
let pp_id = Cfg.Node.pp_id
end
(** Forward CFG with exceptional control-flow *)
module Exceptional = struct
type node_id = Cfg.Node.id
type node = Cfg.node
type node = DefaultNode.t
type id_node_map = node list Cfg.IdMap.t
type t = Cfg.Procdesc.t * id_node_map
include (DefaultNode : module type of DefaultNode with type t := node)
let from_pdesc pdesc =
(* map from a node to its exceptional predecessors *)
@ -143,34 +142,29 @@ module Exceptional = struct
let proc_desc (pdesc, _) = pdesc
let start_node (pdesc, _) = Cfg.Procdesc.get_start_node pdesc
let exit_node (pdesc, _) = Cfg.Procdesc.get_exit_node pdesc
let instrs = Cfg.Node.get_instrs
let id = Cfg.Node.get_id
let id_compare = Cfg.Node.id_compare
let pp_node = Cfg.Node.pp
let pp_id = Cfg.Node.pp_id
let kind = Cfg.Node.get_kind
end
module Backward (W : Wrapper) = struct
include W
let succs = W.preds
let preds = W.succs
let start_node = W.exit_node
let exit_node = W.start_node
let instrs t = IList.rev (W.instrs t)
let normal_succs = W.normal_preds
let normal_preds = W.normal_succs
let exceptional_succs = W.exceptional_preds
let exceptional_preds = W.exceptional_succs
(** Wrapper that reverses the direction of the CFG *)
module Backward (Base : S) = struct
include Base
let instrs n = IList.rev (Base.instrs n)
let succs = Base.preds
let preds = Base.succs
let start_node = Base.exit_node
let exit_node = Base.start_node
let normal_succs = Base.normal_preds
let normal_preds = Base.normal_succs
let exceptional_succs = Base.exceptional_preds
let exceptional_preds = Base.exceptional_succs
end
module NodeIdMap (B : Base) = Map.Make(struct
type t = B.node_id
let compare = B.id_compare
module NodeIdMap (CFG : S) = Map.Make(struct
type t = CFG.id
let compare = CFG.id_compare
end)
module NodeIdSet (B : Base) = Set.Make(struct
type t = B.node_id
let compare = B.id_compare
module NodeIdSet (CFG : S) = Set.Make(struct
type t = CFG.id
let compare = CFG.id_compare
end)

54
infer/src/checkers/procCfg.mli
Unescape View File

@ -7,23 +7,29 @@
* of patent rights can be found in the PATENTS file in the same directory.
*)
module type Base = sig
(** Control-flow graph for a single procedure (as opposed to cfg.ml, which represents a cfg for a
file). Defines useful wrappers that allows us to do tricks like turn a forward cfg to into a
backward one, or view a cfg as having a single instruction per block *)
module type Node = sig
type t
type id
val instrs : t -> Sil.instr list
val kind : t -> Cfg.Node.nodekind
val id : t -> id
val id_compare : id -> id -> int
val pp_id : Format.formatter -> id -> unit
end
module type S = sig
type t
type node
type node_id
include (Node with type t := node)
val id : node -> node_id
val id_compare : node_id -> node_id -> int
(** all successors (normal and exceptional) *)
val succs : t -> node -> node list
(** all predecessors (normal and exceptional) *)
val preds : t -> node -> node list
end
(** Wrapper that allows us to do tricks like turn a forward cfg to into a backward one *)
module type Wrapper = sig
include Base
(** non-exceptional successors *)
val normal_succs : t -> node -> node list
(** non-exceptional predecessors *)
@ -34,24 +40,28 @@ module type Wrapper = sig
val exceptional_preds : t -> node -> node list
val start_node : t -> node
val exit_node : t -> node
val instrs : node -> Sil.instr list
val kind : node -> Cfg.Node.nodekind
val proc_desc : t -> Cfg.Procdesc.t
val nodes : t -> node list
val from_pdesc : Cfg.Procdesc.t -> t
val pp_node : Format.formatter -> node -> unit
val pp_id : Format.formatter -> node_id -> unit
end
module Normal : Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id
module DefaultNode : Node with type t = Cfg.Node.t and type id = Cfg.Node.id
module Exceptional : Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id
(** Forward CFG with no exceptional control-flow *)
module Normal : S with type t = Cfg.Procdesc.t
and type node = DefaultNode.t
and type id = DefaultNode.id
module Backward (W : Wrapper) : Wrapper with type node = W.node and type node_id = W.node_id
(** Forward CFG with exceptional control-flow *)
module Exceptional : S with type t = Cfg.Procdesc.t * DefaultNode.t list Cfg.IdMap.t
and type node = DefaultNode.t
and type id = DefaultNode.id
module NodeIdMap (B : Base) : Map.S with type key = B.node_id
(** Wrapper that reverses the direction of the CFG *)
module Backward (Base : S) : S with type t = Base.t
and type node = Base.node
and type id = Base.id
module NodeIdSet (B : Base) : Set.S with type elt = B.node_id
module NodeIdMap (CFG : S) : Map.S with type key = CFG.id
module NodeIdSet (CFG : S) : Set.S with type elt = CFG.id

28
infer/src/checkers/scheduler.ml
Unescape View File

@ -12,28 +12,28 @@ open! Utils
module F = Format
module L = Logging
module type S = functor (C : ProcCfg.Base) -> sig
module type S = functor (CFG : ProcCfg.S) -> sig
type t
(* schedule the successors of [node] *)
val schedule_succs : t -> C.node -> t
val schedule_succs : t -> CFG.node -> t
(* remove and return the node with the highest priority, the ids of its visited
predecessors, and the new schedule *)
val pop : t -> (C.node * C.node_id list * t) option
val empty : C.t -> t
val pop : t -> (CFG.node * CFG.id list * t) option
val empty : CFG.t -> t
end
(* simple scheduler that visits CFG nodes in reverse postorder. fast/precise for straightline code
and conditionals; not as good for loops (may visit nodes after a loop multiple times). *)
module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
module M = ProcCfg.NodeIdMap (C)
module ReversePostorder : S = functor (CFG : ProcCfg.S) -> struct
module M = ProcCfg.NodeIdMap (CFG)
module WorkUnit = struct
module IdSet = ProcCfg.NodeIdSet (C)
module IdSet = ProcCfg.NodeIdSet (CFG)
type t = {
node : C.node; (* node whose instructions will be analyzed *)
node : CFG.node; (* node whose instructions will be analyzed *)
visited_preds : IdSet.t ; (* predecessors of [node] we have already visited in current iter *)
priority : int; (* |preds| - |visited preds|. *)
}
@ -45,7 +45,7 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
let priority t = t.priority
let compute_priority cfg node visited_preds =
IList.length (C.preds cfg node) - IdSet.cardinal visited_preds
IList.length (CFG.preds cfg node) - IdSet.cardinal visited_preds
let make cfg node =
let visited_preds = IdSet.empty in
@ -59,20 +59,20 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
{ t with visited_preds = visited_preds'; priority = priority'; }
end
type t = { worklist : WorkUnit.t M.t; cfg : C.t; }
type t = { worklist : WorkUnit.t M.t; cfg : CFG.t; }
(* schedule the succs of [node] for analysis *)
let schedule_succs t node =
let node_id = C.id node in
let node_id = CFG.id node in
(* mark [node] as a visited pred of [node_to_schedule] and schedule it *)
let schedule_succ worklist_acc node_to_schedule =
let id_to_schedule = C.id node_to_schedule in
let id_to_schedule = CFG.id node_to_schedule in
let old_work =
try M.find id_to_schedule worklist_acc
with Not_found -> WorkUnit.make t.cfg node_to_schedule in
let new_work = WorkUnit.add_visited_pred t.cfg old_work node_id in
M.add id_to_schedule new_work worklist_acc in
let new_worklist = IList.fold_left schedule_succ t.worklist (C.succs t.cfg node) in
let new_worklist = IList.fold_left schedule_succ t.worklist (CFG.succs t.cfg node) in
{ t with worklist = new_worklist; }
(* remove and return the node with the highest priority (note that smaller integers have higher
@ -94,7 +94,7 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
(init_id, init_priority) in
let max_priority_work = M.find max_priority_id t.worklist in
let node = WorkUnit.node max_priority_work in
let t' = { t with worklist = M.remove (C.id node) t.worklist } in
let t' = { t with worklist = M.remove (CFG.id node) t.worklist } in
Some (node, WorkUnit.visited_preds max_priority_work, t')
with Not_found -> None

10
infer/src/unit/analyzerTester.ml
Unescape View File

@ -138,17 +138,17 @@ module StructuredSil = struct
end
module Make
(C : ProcCfg.Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id)
(CFG : ProcCfg.S with type node = Cfg.Node.t)
(S : Scheduler.S)
(A : AbstractDomain.S)
(T : TransferFunctions.S
with type astate = A.astate and type extras = ProcData.no_extras
and type node_id = C.node_id) = struct
and type node_id = CFG.id) = struct
open StructuredSil
module I = AbstractInterpreter.Make (C) (S) (A) (T)
module M = ProcCfg.NodeIdMap (C)
module I = AbstractInterpreter.Make (CFG) (S) (A) (T)
module M = ProcCfg.NodeIdMap (CFG)
type assert_map = string M.t
@ -214,7 +214,7 @@ module Make
let node = create_node (Cfg.Node.Stmt_node "Invariant") [] in
set_succs last_node [node] ~exn_handlers;
(* add the assertion to be checked after analysis converges *)
node, M.add (C.id node) (inv_str, inv_label) assert_map
node, M.add (CFG.id node) (inv_str, inv_label) assert_map
and structured_instrs_to_node last_node assert_map exn_handlers instrs =
IList.fold_left
(fun acc instr -> structured_instr_to_node acc exn_handlers instr)

39
infer/src/unit/schedulerTests.ml
Unescape View File

@ -12,20 +12,33 @@ open! Utils
module F = Format
(* mock for creating CFG's from adjacency lists *)
(** mocks for creating CFG's from adjacency lists *)
module MockNode = struct
type t = int
type id = int
let instrs _ = []
let id n = n
let kind _ = Cfg.Node.Stmt_node ""
let id_compare = int_compare
let pp_id fmt i =
F.fprintf fmt "%i" i
end
module MockProcCfg = struct
type node = int
include (MockNode : module type of MockNode with type t := node)
type t = (node * node list) list
type node_id = int
let id_compare = int_compare
let id n = n
let succs t n =
try
let node_id = id n in
IList.find (fun (node, _) -> id_compare (id node) node_id = 0) t
IList.find
(fun (node, _) -> id_compare (id node) node_id = 0)
t
|> snd
with Not_found -> []
@ -33,12 +46,24 @@ module MockProcCfg = struct
try
let node_id = id n in
IList.filter
(fun (_, succs) -> IList.exists (fun node -> id_compare (id node) node_id = 0) succs) t
(fun (_, succs) ->
IList.exists (fun node -> id_compare (id node) node_id = 0) succs)
t
|> IList.map fst
with Not_found -> []
let from_adjacency_list t = t
let nodes t = IList.map fst t
let normal_succs = succs
let normal_preds = preds
let exceptional_succs _ _ = []
let exceptional_preds _ _ = []
let from_adjacency_list t = t
(* not called by the scheduler *)
let start_node _ = assert false
let exit_node _ = assert false
let proc_desc _ = assert false
let from_pdesc _ = assert false
end
module S = Scheduler.ReversePostorder (MockProcCfg)

Write Preview
Loading…
Cancel
Save