beginnings of access tree domain, tests

Reviewed By: mbouaziz

Differential Revision: D3544575

fbshipit-source-id: 17fa411

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

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

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]

infer/src/unit/inferunit.ml

@@ -16,6 +16,7 @@ let () =
   let tests = [
     AbstractInterpreterTests.tests;
     AccessPathTests.tests;
+    AccessTreeTests.tests;
     AddressTakenTests.tests;
     CopyPropagationTests.tests;
     ProcCfgTests.tests;