adding finite access paths, tests, and basic utilities

Reviewed By: dkgi

Differential Revision: D3502236

fbshipit-source-id: b49bb32

infer/src/checkers/accessPath.ml

@@ -0,0 +1,89 @@
+(*
+ * 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
+
+type base = Pvar.t * Typ.t
+
+type access =
+  | FieldAccess of Ident.fieldname * Typ.t
+  | ArrayAccess of Typ.t
+
+type t = base * access list
+
+let base_compare ((var1, typ1) as base1) ((var2, typ2) as base2) =
+  if base1 == base2
+  then 0
+  else
+    Pvar.compare var1 var2
+    |> next Typ.compare typ1 typ2
+
+let base_equal base1 base2 =
+  base_compare base1 base2 = 0
+
+let access_compare access1 access2 =
+  if access1 == access2
+  then 0
+  else
+    match access1, access2 with
+    | FieldAccess (f1, typ1), FieldAccess (f2, typ2) ->
+        Ident.fieldname_compare f1 f2
+        |> next Typ.compare typ1 typ2
+    | ArrayAccess typ1, ArrayAccess typ2 ->
+        Typ.compare typ1 typ2
+    | FieldAccess _, _ -> 1
+    | _, FieldAccess _ -> -1
+
+let access_equal access1 access2 =
+  access_compare access1 access2 = 0
+
+let compare ((base1, accesses1) as ap1) ((base2, accesses2) as ap2) =
+  if ap1 == ap2
+  then 0
+  else
+    base_compare base1 base2
+    |> next (IList.compare access_compare) accesses1 accesses2
+
+let equal ap1 ap2 =
+  compare ap1 ap2 = 0
+
+let of_pvar pvar typ =
+  (pvar, typ), []
+
+let append (base, accesses) access =
+  base, accesses @ [access]
+
+let rec is_prefix_path path1 path2 =
+  if path1 == path2
+  then true
+  else
+    match path1, path2 with
+    | [], _ -> true
+    | _, [] -> false
+    | access1 :: p1, access2 :: p2 -> access_equal access1 access2 && is_prefix_path p1 p2
+
+let is_prefix ((base1, path1) as ap1) ((base2, path2) as ap2) =
+  if ap1 == ap2
+  then true
+  else
+    base_equal base1 base2 && is_prefix_path path1 path2
+
+let pp_base fmt (pvar, _) =
+  (Pvar.pp pe_text) fmt pvar
+
+let pp_access fmt = function
+  | FieldAccess (field_name, _) -> F.fprintf fmt ".%a" Ident.pp_fieldname field_name
+  | ArrayAccess _ -> F.fprintf fmt "[_]"
+
+let pp fmt (base, accesses) =
+  let pp_access_list fmt accesses =
+    F.pp_print_list pp_access fmt accesses in
+  F.fprintf fmt "%a%a" pp_base base pp_access_list accesses

infer/src/checkers/accessPath.mli

@@ -0,0 +1,35 @@
+(*
+ * 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.
+ *)
+
+(** Module for naming heap locations via the path used to access them (e.g., x.f.g, y[a].b) *)
+
+type base = Pvar.t * Typ.t
+
+type access =
+  | FieldAccess of Ident.fieldname * Typ.t (* field name * field type *)
+  | ArrayAccess of Typ.t (* array element type. index is unknown *)
+
+(** root var, and a list of accesses. closest to the root var is first that is, x.f.g is represented
+    as (x, [f; g]) *)
+type t = base * access list
+
+val compare : t -> t -> int
+
+val equal : t -> t -> bool
+
+(** create an access path from a pvar *)
+val of_pvar : Pvar.t -> Typ.t -> t
+
+(** append a new access to an existing access path; e.g., `append_access g x.f` produces `x.f.g` *)
+val append : t -> access -> t
+
+(** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *)
+val is_prefix : t -> t -> bool
+
+val pp : Format.formatter -> t -> unit

infer/src/unit/accessPathTests.ml

@@ -0,0 +1,69 @@
+(*
+ * 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.
+ *)
+
+module F = Format
+
+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 pp_diff fmt (actual, expected) =
+  F.fprintf fmt "Expected output %a but got %a" AccessPath.pp expected AccessPath.pp actual
+
+let assert_eq input expected =
+  let open OUnit2 in
+  assert_equal ~cmp:AccessPath.equal ~pp_diff input expected
+
+let tests =
+  let x = make_access_path "x" [] in
+  let y = make_access_path "y" [] in
+  let f_access = make_field_access "f" in
+  let g_access = make_field_access "g" in
+  let xF = make_access_path "x" ["f"] in
+  let xFG = make_access_path "x" ["f"; "g";] in
+  let yF = make_access_path "y" ["f"] in
+
+  let open OUnit2 in
+  let equal_test =
+    let equal_test_ _ =
+      assert_bool "equal works for bases" (AccessPath.equal x (make_access_path "x" []));
+      assert_bool "equal works for paths" (AccessPath.equal xFG (make_access_path "x" ["f"; "g";]));
+      assert_bool "disequality works for bases" (not (AccessPath.equal x y));
+      assert_bool "disequality works for paths" (not (AccessPath.equal xF xFG)) in
+    "equal">::equal_test_ in
+
+  let append_test =
+    let append_test_ _ =
+      assert_eq xF (AccessPath.append x f_access);
+      assert_eq xFG (AccessPath.append xF g_access) in
+    "append">::append_test_ in
+
+  let prefix_test =
+    let prefix_test_ _ =
+      assert_bool "x is prefix of self" (AccessPath.is_prefix x x);
+      assert_bool "x.f is prefix of self" (AccessPath.is_prefix xF xF);
+      assert_bool "x is not prefix of y" (not (AccessPath.is_prefix x y));
+      assert_bool "x is prefix of x.f" (AccessPath.is_prefix x xF);
+      assert_bool "x.f not prefix of x" (not (AccessPath.is_prefix xF x));
+      assert_bool "x.f is prefix of x.f.g" (AccessPath.is_prefix xF xFG);
+      assert_bool "x.f.g is not prefix of x.f" (not (AccessPath.is_prefix xFG xF));
+      assert_bool "y.f is not prefix of x.f" (not (AccessPath.is_prefix yF xF));
+      assert_bool "y.f is not prefix of x.f.g" (not (AccessPath.is_prefix yF xFG)) in
+    "prefix">::prefix_test_ in
+
+  "all_tests_suite">:::[equal_test; append_test; prefix_test;]

infer/src/unit/inferunit.ml

@@ -15,6 +15,7 @@ let () =
   let open OUnit2 in
   let tests = [
     AbstractInterpreterTests.tests;
+    AccessPathTests.tests;
     AddressTakenTests.tests;
     CopyPropagationTests.tests;
     ProcCfgTests.tests;