From 7544e500bf84a38633e86612d6ff50c4ee899399 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Sat, 2 Jul 2016 13:26:26 -0700 Subject: [PATCH] adding finite access paths, tests, and basic utilities Reviewed By: dkgi Differential Revision: D3502236 fbshipit-source-id: b49bb32 --- infer/src/checkers/accessPath.ml | 89 +++++++++++++++++++++++++++++++ infer/src/checkers/accessPath.mli | 35 ++++++++++++ infer/src/unit/accessPathTests.ml | 69 ++++++++++++++++++++++++ infer/src/unit/inferunit.ml | 1 + 4 files changed, 194 insertions(+) create mode 100644 infer/src/checkers/accessPath.ml create mode 100644 infer/src/checkers/accessPath.mli create mode 100644 infer/src/unit/accessPathTests.ml diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml new file mode 100644 index 000000000..01ebe076a --- /dev/null +++ b/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 diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli new file mode 100644 index 000000000..f8d34d59a --- /dev/null +++ b/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 diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml new file mode 100644 index 000000000..319cd636f --- /dev/null +++ b/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;] diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index 9d5f58cbf..db24b77d3 100644 --- a/infer/src/unit/inferunit.ml +++ b/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;