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

[checkers] add mli for AccessTree

Browse Source 
Reviewed By: jberdine

Differential Revision: D4271772

fbshipit-source-id: 3f9681d
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent 4b98543d35
commit ff3b6a10db
2 changed files with 114 additions and 30 deletions
Show Stats Download Patch File Download Diff File

72
infer/src/checkers/accessTree.ml
Unescape View File

@ -12,31 +12,58 @@ open! Utils
module F = Format
module L = Logging
(** tree of (trace, access path) associations organized by structure of access paths *)
module Make (TraceDomain : AbstractDomain.S) = struct
module type S = sig
module TraceDomain : AbstractDomain.S
module AccessMap = AccessPath.AccessMap
module BaseMap = AccessPath.BaseMap
type node = TraceDomain.astate * tree
and tree =
| Subtree of node AccessMap.t
| Star
type t = node BaseMap.t
include AbstractDomain.S with type astate = t
val empty : t
val empty_node : node
val make_node : TraceDomain.astate -> node AccessMap.t -> node
val make_access_node : TraceDomain.astate -> AccessPath.access -> TraceDomain.astate -> node
val make_normal_leaf : TraceDomain.astate -> node
val make_starred_leaf : TraceDomain.astate -> node
val get_node : AccessPath.t -> t -> node option
val get_trace : AccessPath.t -> t -> TraceDomain.astate option
val add_node : AccessPath.t -> node -> t -> t
val add_trace : AccessPath.t -> TraceDomain.astate -> t -> t
val fold : ('a -> AccessPath.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a
val pp_node : F.formatter -> node -> unit
end
module Make (TraceDomain : AbstractDomain.S) = struct
module TraceDomain = TraceDomain
module AccessMap = AccessPath.AccessMap
module BaseMap = AccessPath.BaseMap
type node = TraceDomain.astate * tree
and tree =
| Subtree of node AccessMap.t (* map from access -> nodes. a leaf is encoded as an empty map *)
| Star (* special leaf for starred access paths *)
| Subtree of node AccessMap.t
| Star
(* map from base var -> access subtree *)
type t = node BaseMap.t
type astate = t
(** Here's how to represent a few different kinds of trace * access path associations:
(x, T) := { x |-> (T, Subtree {}) }
(x.f, T) := { x |-> (empty, Subtree { f |-> (T, Subtree {}) }) }
(x*, T) := { x |-> (T, Star) }
(x.f*, T) := { x |-> (empty, Subtree { f |-> (T, Star) }) }
(x, T1), (y, T2) := { x |-> (T1, Subtree {}), y |-> (T2, Subtree {}) }
(x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}),
g |-> (T2, Subtree {}) }) }
*)
let empty = BaseMap.empty
let initial = empty
@ -56,9 +83,6 @@ module Make (TraceDomain : AbstractDomain.S) = struct
let make_access_node base_trace access trace =
make_node base_trace (AccessMap.singleton access (make_normal_leaf trace))
let make_empty_trace_access_node trace access =
make_access_node TraceDomain.initial access trace
(** find all of the traces in the subtree and join them with [orig_trace] *)
let rec join_all_traces orig_trace = function
| Subtree subtree ->
@ -70,7 +94,6 @@ module Make (TraceDomain : AbstractDomain.S) = struct
| Star ->
orig_trace
(** retrieve the trace and subtree associated with [ap] from [tree] *)
let get_node ap tree =
let rec accesses_get_node access_list trace tree =
match access_list, tree with
@ -96,7 +119,6 @@ module Make (TraceDomain : AbstractDomain.S) = struct
| exception Not_found ->
None
(** retrieve the trace associated with [ap] from [tree] *)
let get_trace ap tree =
Option.map fst (get_node ap tree)
@ -207,7 +229,6 @@ module Make (TraceDomain : AbstractDomain.S) = struct
trace, Subtree (AccessMap.add access access_node' subtree) in
access_tree_add_trace_ ~seen_array_access accesses node
(** add ([ap], [node]) to [tree]. *)
let add_node ap node_to_add tree =
let base, accesses = AccessPath.extract ap in
let is_exact = AccessPath.is_exact ap in
@ -218,12 +239,6 @@ module Make (TraceDomain : AbstractDomain.S) = struct
access_tree_add_trace ~node_to_add ~seen_array_access:false ~is_exact accesses base_node in
BaseMap.add base base_node' tree
(** add [ap] to [tree] and associate its leaf node with [trace].
if [ap] or a suffix of [ap] is not already present in the tree, it will be added with empty
traces associated with each of the inner nodes.
if [ap] is already present in the tree and contains no array accesses, this overwrites the
existing trace. if [ap] does contain array accesses, it joins the existing trace with [trace].
*)
let add_trace ap trace tree =
add_node ap (make_normal_leaf trace) tree
@ -246,9 +261,6 @@ module Make (TraceDomain : AbstractDomain.S) = struct
let node_fold (f : 'a -> AccessPath.t -> TraceDomain.astate -> 'a) base node acc =
node_fold_ f base [] node acc
let access_map_fold (f : 'a -> AccessPath.t -> TraceDomain.astate -> 'a) base m acc =
access_map_fold_ f base [] m acc
let fold (f : 'a -> AccessPath.t -> TraceDomain.astate -> 'a) tree acc_ =
BaseMap.fold (fun base node acc -> node_fold f base node acc) tree acc_

72
infer/src/checkers/accessTree.mli
Unescape View File

@ -0,0 +1,72 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
(** tree of (trace, access path) associations organized by structure of access paths *)
module type S = sig
module TraceDomain : AbstractDomain.S
module AccessMap = AccessPath.AccessMap
module BaseMap = AccessPath.BaseMap
type node = TraceDomain.astate * tree
and tree =
| Subtree of node AccessMap.t (** map from access -> nodes. a leaf is encoded as an empty map *)
| Star (** special leaf for starred access paths *)
(** map from base var -> access subtree. Here's how to represent a few different kinds of
trace * access path associations:
(x, T) := { x |-> (T, Subtree {}) }
(x.f, T) := { x |-> (empty, Subtree { f |-> (T, Subtree {}) }) }
(x*, T) := { x |-> (T, Star) }
(x.f*, T) := { x |-> (empty, Subtree { f |-> (T, Star) }) }
(x, T1), (y, T2) := { x |-> (T1, Subtree {}), y |-> (T2, Subtree {}) }
(x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}),
g |-> (T2, Subtree {}) }) }
*)
type t = node BaseMap.t
include AbstractDomain.S with type astate = t
val empty : t
val empty_node : node
val make_node : TraceDomain.astate -> node AccessMap.t -> node
(** for testing only *)
val make_access_node : TraceDomain.astate -> AccessPath.access -> TraceDomain.astate -> node
(** create a leaf node with no successors *)
val make_normal_leaf : TraceDomain.astate -> node
(** create a leaf node with a wildcard successor *)
val make_starred_leaf : TraceDomain.astate -> node
(** retrieve the node associated with the given access path *)
val get_node : AccessPath.t -> t -> node option
(** retrieve the trace associated with the given access path *)
val get_trace : AccessPath.t -> t -> TraceDomain.astate option
(** add the given access path to the tree and associate its last access with with the given node.
if any of the accesses in the path are not already present in the tree, they will be added
with with empty traces associated with each of the inner nodes. *)
val add_node : AccessPath.t -> node -> t -> t
(** add the given access path to the tree and associate its last access with with the given trace.
if any of the accesses in the path are not already present in the tree, they will be added
with with empty traces associated with each of the inner nodes. *)
val add_trace : AccessPath.t -> TraceDomain.astate -> t -> t
(** apply a function to each (access path, node) pair in the tree. *)
val fold : ('a -> AccessPath.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a
val pp_node : Format.formatter -> node -> unit
end
module Make (TraceDomain : AbstractDomain.S) : S with module TraceDomain = TraceDomain
Write Preview
Loading…
Cancel
Save