diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index cb0e020fa..2d8b72f32 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -23,10 +23,18 @@ type t = | Exact of raw (** precise representation of an access path, e.g. x.f.g *) | Abstracted of raw (** abstraction of heap reachable from an access path, e.g. x.f* *) +val base_compare : base -> base -> int + +val base_equal : base -> base -> bool + val raw_compare : raw -> raw -> int val raw_equal : raw -> raw -> bool +val access_compare : access -> access -> int + +val access_equal : access -> access -> bool + (** create an access path from a pvar *) val of_pvar : Pvar.t -> Typ.t -> raw @@ -36,6 +44,8 @@ val append : raw -> access -> raw (** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *) val is_prefix : raw -> raw -> bool +val pp_access : Format.formatter -> access -> unit + val pp_raw : Format.formatter -> raw -> unit val compare : t -> t -> int @@ -51,4 +61,6 @@ val is_exact : t -> bool (** return true if \gamma(lhs) \subseteq \gamma(rhs) *) val (<=) : lhs:t -> rhs:t -> bool +val pp_base : Format.formatter -> base -> unit + val pp : Format.formatter -> t -> unit diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml new file mode 100644 index 000000000..8762c98c8 --- /dev/null +++ b/infer/src/checkers/accessTree.ml @@ -0,0 +1,104 @@ +(* + * 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. + *) + +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 AccessMap = PrettyPrintable.MakePPMap(struct + type t = AccessPath.access + let compare = AccessPath.access_compare + let pp_key = AccessPath.pp_access + end) + + module BaseMap = PrettyPrintable.MakePPMap(struct + type t = AccessPath.base + let compare = AccessPath.base_compare + let pp_key = AccessPath.pp_base + end) + + 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 *) + type t = node BaseMap.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 make_node trace subtree = + trace, Subtree subtree + + let empty_node = + make_node TraceDomain.initial AccessMap.empty + + let make_normal_leaf trace = + make_node trace AccessMap.empty + + let make_starred_leaf trace = + trace, Star + + 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 [tree] and join them with [orig_trace] *) + let rec join_all_traces orig_trace tree = + let node_join_traces _ (trace, node) trace_acc = + let trace_acc' = TraceDomain.join trace_acc trace in + match node with + | Star -> trace_acc' + | Subtree subtree -> join_all_traces trace_acc' subtree in + AccessMap.fold node_join_traces tree orig_trace + + (** retrieve the trace associated with [ap] from [tree] *) + let get_trace ap tree = + let rec accesses_get_trace access_list trace tree = + match access_list, tree with + | _, Star -> + trace, Star + | [], (Subtree _ as tree) -> + trace, tree + | access :: accesses, Subtree subtree -> + let access_trace, access_subtree = AccessMap.find access subtree in + accesses_get_trace accesses access_trace access_subtree in + let get_trace_ base accesses tree = + let base_trace, base_tree = BaseMap.find base tree in + accesses_get_trace accesses base_trace base_tree in + let base, accesses = AccessPath.extract ap in + match get_trace_ base accesses tree with + | trace, Star -> + Some trace + | trace, Subtree subtree -> + if AccessPath.is_exact ap + then Some trace + else + (* input query was [ap]*, and [trace] is the trace associated with [ap]. get the traces + associated with the children of [ap] in [tree] and join them with [trace] *) + Some (join_all_traces trace subtree) + | exception Not_found -> + None +end diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml new file mode 100644 index 000000000..505989a44 --- /dev/null +++ b/infer/src/unit/accessTreeTests.ml @@ -0,0 +1,134 @@ +(* + * 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. + *) + +open !Utils + +module F = Format + +(* string set domain we use to ensure we're getting the expected traces *) +module MockTraceDomain = + AbstractDomain.FiniteSet + (PrettyPrintable.MakePPSet(struct + include String + let pp_element fmt s = Format.fprintf fmt "%s" s + end)) + +module Domain = AccessTree.Make (MockTraceDomain) + +let make_base base_str = + Pvar.mk (Mangled.from_string base_str) Procname.empty_block, Typ.Tvoid + +let make_field_access access_str = + AccessPath.FieldAccess (Ident.create_fieldname (Mangled.from_string access_str) 0, Typ.Tvoid) + +let make_access_path base_str accesses = + let rec make_accesses accesses_acc = function + | [] -> accesses_acc + | access_str :: l -> make_accesses ((make_field_access access_str) :: accesses_acc) l in + let accesses = make_accesses [] accesses in + make_base base_str, IList.rev accesses + +let tests = + let x_base = make_base "x" in + let y_base = make_base "y" in + let z_base = make_base "z" in + + let f = make_field_access "f" in + let g = make_field_access "g" in + + let xF = AccessPath.Exact (make_access_path "x" ["f"]) in + let xG = AccessPath.Exact (make_access_path "x" ["g"]) in + let xFG = AccessPath.Exact (make_access_path "x" ["f"; "g"]) in + let yF = AccessPath.Exact (make_access_path "y" ["f"]) in + let yG = AccessPath.Exact (make_access_path "y" ["g"]) in + let yFG = AccessPath.Exact (make_access_path "y" ["f"; "g"]) in + let z = AccessPath.Exact (make_access_path "z" []) in + let zF = AccessPath.Exact (make_access_path "z" ["f"]) in + let zFG = AccessPath.Exact (make_access_path "z" ["f"; "g"]) in + + let a_star = AccessPath.Abstracted (make_access_path "a" []) in + let x_star = AccessPath.Abstracted (make_access_path "x" []) in + let xF_star = AccessPath.Abstracted (make_access_path "x" ["f"]) in + let xG_star = AccessPath.Abstracted (make_access_path "x" ["g"]) in + let y_star = AccessPath.Abstracted (make_access_path "y" []) in + let yF_star = AccessPath.Abstracted (make_access_path "y" ["f"]) in + let z_star = AccessPath.Abstracted (make_access_path "z" []) in + + let x_trace = MockTraceDomain.singleton "x" in + let y_trace = MockTraceDomain.singleton "y" in + let z_trace = MockTraceDomain.singleton "z" in + let xF_trace = MockTraceDomain.singleton "xF" in + let yF_trace = MockTraceDomain.singleton "yF" in + let xFG_trace = MockTraceDomain.singleton "xFG" in + + let x_tree = + let g_subtree = Domain.make_access_node xF_trace g xFG_trace in + Domain.AccessMap.singleton f g_subtree + |> Domain.make_node x_trace in + let y_tree = + let yF_subtree = Domain.make_starred_leaf yF_trace in + Domain.AccessMap.singleton f yF_subtree + |> Domain.make_node y_trace in + let z_tree = Domain.make_starred_leaf z_trace in + let tree = + Domain.BaseMap.singleton x_base x_tree + |> Domain.BaseMap.add y_base y_tree + |> Domain.BaseMap.add z_base z_tree in + + (* [tree] is: + x |-> ("x", + f |-> ("Xf", + g |-> ("xFG", {}))) + y |-> ("y", + f |-> ("yF", * )) + z |-> ("z", * ) + *) + + let open OUnit2 in + let no_trace = "NONE" in + + let get_trace_str access_path tree = + match Domain.get_trace access_path tree with + | Some trace -> pp_to_string MockTraceDomain.pp trace + | None -> no_trace in + + let assert_traces_eq access_path tree expected_trace_str = + let actual_trace_str = get_trace_str access_path tree in + let pp_diff fmt (actual, expected) = + F.fprintf fmt "Expected to retrieve trace %s but got %s" expected actual in + assert_equal ~pp_diff actual_trace_str expected_trace_str in + + let assert_trace_not_found access_path tree = + assert_traces_eq access_path tree no_trace in + + let get_trace_test = + let get_trace_test_ _ = + (* exact access path tests *) + assert_traces_eq z tree "{ z }"; + assert_traces_eq xF tree "{ xF }"; + assert_traces_eq yF tree "{ yF }"; + assert_traces_eq xFG tree "{ xFG }"; + assert_trace_not_found xG tree; + + (* starred access path tests *) + assert_traces_eq x_star tree "{ x, xF, xFG }"; + assert_traces_eq xF_star tree "{ xF, xFG }"; + assert_trace_not_found xG_star tree; + assert_trace_not_found a_star tree; + + (* starred tree tests *) + assert_traces_eq zF tree "{ z }"; + assert_traces_eq zFG tree "{ z }"; + assert_traces_eq z_star tree "{ z }"; + assert_traces_eq y_star tree "{ y, yF }"; + assert_traces_eq yF_star tree "{ yF }"; + assert_traces_eq yFG tree "{ yF }"; + assert_trace_not_found yG tree in + "get_trace">::get_trace_test_ in + "access_tree_suite">:::[get_trace_test] diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index db24b77d3..a7a5d6405 100644 --- a/infer/src/unit/inferunit.ml +++ b/infer/src/unit/inferunit.ml @@ -16,6 +16,7 @@ let () = let tests = [ AbstractInterpreterTests.tests; AccessPathTests.tests; + AccessTreeTests.tests; AddressTakenTests.tests; CopyPropagationTests.tests; ProcCfgTests.tests;