diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 01ebe076a..373a3d633 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -17,7 +17,11 @@ type access = | FieldAccess of Ident.fieldname * Typ.t | ArrayAccess of Typ.t -type t = base * access list +type raw = base * access list + +type t = + | Exact of raw + | Abstracted of raw let base_compare ((var1, typ1) as base1) ((var2, typ2) as base2) = if base1 == base2 @@ -45,13 +49,21 @@ let access_compare access1 access2 = let access_equal access1 access2 = access_compare access1 access2 = 0 -let compare ((base1, accesses1) as ap1) ((base2, accesses2) as ap2) = +let raw_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 raw_equal ap1 ap2 = + raw_compare ap1 ap2 = 0 + +let compare ap1 ap2 = match ap1, ap2 with + | Exact ap1, Exact ap2 | Abstracted ap1, Abstracted ap2 -> raw_compare ap1 ap2 + | Exact _, Abstracted _ -> 1 + | Abstracted _, Exact _ -> (-1) + let equal ap1 ap2 = compare ap1 ap2 = 0 @@ -76,6 +88,19 @@ let is_prefix ((base1, path1) as ap1) ((base2, path2) as ap2) = else base_equal base1 base2 && is_prefix_path path1 path2 +let extract = function + | Exact ap | Abstracted ap -> ap + +let is_exact = function + | Exact _ -> true + | Abstracted _ -> false + +let (<=) ~lhs ~rhs = + match lhs, rhs with + | Abstracted _, Exact _ -> false + | Exact lhs_ap, Exact rhs_ap -> raw_equal lhs_ap rhs_ap + | (Exact lhs_ap | Abstracted lhs_ap), Abstracted rhs_ap -> is_prefix rhs_ap lhs_ap + let pp_base fmt (pvar, _) = (Pvar.pp pe_text) fmt pvar @@ -83,7 +108,11 @@ 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_raw 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 + +let pp fmt = function + | Exact access_path -> pp_raw fmt access_path + | Abstracted access_path -> F.fprintf fmt "%a*" pp_raw access_path diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index f8d34d59a..cb0e020fa 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -17,19 +17,38 @@ type access = (** 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 +type raw = base * access list -val compare : t -> t -> int +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 equal : t -> t -> bool +val raw_compare : raw -> raw -> int + +val raw_equal : raw -> raw -> bool (** create an access path from a pvar *) -val of_pvar : Pvar.t -> Typ.t -> t +val of_pvar : Pvar.t -> Typ.t -> raw (** 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 +val append : raw -> access -> raw (** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *) -val is_prefix : t -> t -> bool +val is_prefix : raw -> raw -> bool + +val pp_raw : Format.formatter -> raw -> unit + +val compare : t -> t -> int + +val equal : t -> t -> bool + +(** extract a raw access path from its wrapper *) +val extract : t -> raw + +(** return true if [t] is an exact representation of an access path, false if it's an abstraction *) +val is_exact : t -> bool + +(** return true if \gamma(lhs) \subseteq \gamma(rhs) *) +val (<=) : lhs:t -> rhs:t -> bool val pp : Format.formatter -> t -> unit diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml new file mode 100644 index 000000000..3e7ecca3d --- /dev/null +++ b/infer/src/checkers/accessPathDomains.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 + +module Set = struct + module APSet = PrettyPrintable.MakePPSet (struct + type t = AccessPath.t + let compare = AccessPath.compare + let pp_element = AccessPath.pp + end) + + (** TODO (12086310): best-case behavior of some operations can be improved by adding "abstracted" + bool recording whether an abstracted access path has been introduced *) + type astate = APSet.t + + let initial = APSet.empty + + let is_bottom _ = false + + let pp = APSet.pp + + let normalize aps = + APSet.filter + (fun lhs -> not (APSet.exists (fun rhs -> lhs != rhs && AccessPath.(<=) ~lhs ~rhs) aps)) + aps + + let add = APSet.add + + let of_list = APSet.of_list + + let mem ap aps = + APSet.mem ap aps || APSet.exists (fun other_ap -> AccessPath.(<=) ~lhs:ap ~rhs:other_ap) aps + + let mem_fuzzy ap aps = + let has_overlap ap1 ap2 = + AccessPath.(<=) ~lhs:ap1 ~rhs:ap2 || AccessPath.(<=) ~lhs:ap2 ~rhs:ap1 in + APSet.mem ap aps || APSet.exists (has_overlap ap) aps + + let (<=) ~lhs ~rhs = + if lhs == rhs + then true + else + let rhs_contains lhs_ap = + mem lhs_ap rhs in + APSet.subset lhs rhs || APSet.for_all rhs_contains lhs + + let join aps1 aps2 = + if aps1 == aps2 + then aps1 + else APSet.union aps1 aps2 + + let widen ~prev ~next ~num_iters:_ = + if prev == next + then prev + else + let abstract_access_path ap aps = match ap with + | AccessPath.Exact exact_ap -> APSet.add (AccessPath.Abstracted exact_ap) aps + | AccessPath.Abstracted _ -> APSet.add ap aps in + let diff_aps = APSet.diff next prev in + APSet.fold abstract_access_path diff_aps initial + |> join prev +end diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli new file mode 100644 index 000000000..a3ba3a740 --- /dev/null +++ b/infer/src/checkers/accessPathDomains.mli @@ -0,0 +1,36 @@ +(* + * 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. + *) + +(** Generic abstract domains backed by access paths *) + +(** add-only set of access paths. To make common operations efficient (namely, add, join, and + widen), the set is allowed to contain elements whose concretization is redundant (e.g., x* and + x.f). these redundancies can be eliminated by expressing the set in its canonical form via a + call to [normalize]. however, [normalize] is quadratic in the size of the set, so it should be + used sparingly (recommendation: only before computing a summary based on the access path set) *) +module Set : sig + include AbstractDomain.S + + val of_list : AccessPath.t list -> astate + + (** return true if \gamma({ap}) \subseteq \gamma(aps). + note: this is worst-case linear in the size of the set *) + val mem : AccessPath.t -> astate -> bool + + (** more permissive version of [mem]; return true if \gamma({a}) \cap \gamma(aps) != {}. + note: this is worst-case linear in the size of the set *) + val mem_fuzzy : AccessPath.t -> astate -> bool + + val add : AccessPath.t -> astate -> astate + + (** simplify an access path set to its canonical representation by eliminating redundancies + between (1) pairs of abstracted access_paths, and (2) exact access paths and abstracted + access paths. warning: this is quadratic in the size of the set! use sparingly *) + val normalize : astate -> astate +end diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index 319cd636f..109ad288f 100644 --- a/infer/src/unit/accessPathTests.ml +++ b/infer/src/unit/accessPathTests.ml @@ -7,6 +7,8 @@ * of patent rights can be found in the PATENTS file in the same directory. *) +open !Utils + module F = Format let make_base base_str = @@ -22,13 +24,6 @@ let make_access_path base_str accesses = 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 @@ -38,16 +33,34 @@ let tests = let xFG = make_access_path "x" ["f"; "g";] in let yF = make_access_path "y" ["f"] in + let x_exact = AccessPath.Exact x in + let y_exact = AccessPath.Exact y in + let x_abstract = AccessPath.Abstracted x in + let xF_exact = AccessPath.Exact xF in + let xFG_exact = AccessPath.Exact xFG in + let yF_exact = AccessPath.Exact yF in + let yF_abstract = AccessPath.Abstracted yF 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 + assert_bool "equal works for bases" (AccessPath.raw_equal x (make_access_path "x" [])); + assert_bool + "equal works for paths" + (AccessPath.raw_equal xFG (make_access_path "x" ["f"; "g";])); + assert_bool "disequality works for bases" (not (AccessPath.raw_equal x y)); + assert_bool "disequality works for paths" (not (AccessPath.raw_equal xF xFG)) in "equal">::equal_test_ in let append_test = + let pp_diff fmt (actual, expected) = + F.fprintf + fmt + "Expected output %a but got %a" + AccessPath.pp_raw expected + AccessPath.pp_raw actual in + let assert_eq input expected = + assert_equal ~cmp:AccessPath.raw_equal ~pp_diff input expected in let append_test_ _ = assert_eq xF (AccessPath.append x f_access); assert_eq xFG (AccessPath.append xF g_access) in @@ -66,4 +79,71 @@ let tests = 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;] + let abstraction_test = + let abstraction_test_ _ = + assert_bool "extract" (AccessPath.raw_equal (AccessPath.extract xF_exact) xF); + assert_bool "is_exact" (AccessPath.is_exact x_exact); + assert_bool "not is_exact" (not (AccessPath.is_exact x_abstract)); + assert_bool "(<=)1" (AccessPath.(<=) ~lhs:x_exact ~rhs:x_abstract); + assert_bool "(<=)2" (AccessPath.(<=) ~lhs:xF_exact ~rhs:x_abstract); + assert_bool + "not (<=)1" + (not (AccessPath.(<=) ~lhs:x_abstract ~rhs:x_exact)); + assert_bool + "not (<=)2" + (not (AccessPath.(<=) ~lhs:x_abstract ~rhs:xF_exact)) in + "abstraction">::abstraction_test_ in + + let domain_test = + let domain_test_ _ = + let pp_diff fmt (actual, expected) = + F.fprintf fmt "Expected %s but got %s" expected actual in + let assert_eq input_aps expected = + let input = pp_to_string AccessPathDomains.Set.pp input_aps in + assert_equal ~cmp:(=) ~pp_diff input expected in + let aps1 = AccessPathDomains.Set.of_list [x_exact; x_abstract] in (* { x*, x } *) + let aps2 = AccessPathDomains.Set.add xF_exact aps1 in (* x*, x, x.f *) + let aps3 = AccessPathDomains.Set.add yF_exact aps2 in (* x*, x, x.f, y.f *) + + assert_bool "mem_easy" (AccessPathDomains.Set.mem x_exact aps1); + assert_bool "mem_harder1" (AccessPathDomains.Set.mem xFG_exact aps1); + assert_bool "mem_harder2" (AccessPathDomains.Set.mem x_abstract aps1); + assert_bool "mem_negative" (not (AccessPathDomains.Set.mem y_exact aps1)); + assert_bool "mem_not_fully_contained" (not (AccessPathDomains.Set.mem yF_abstract aps3)); + + assert_bool "mem_fuzzy_easy" (AccessPathDomains.Set.mem_fuzzy x_exact aps1); + assert_bool "mem_fuzzy_harder1" (AccessPathDomains.Set.mem_fuzzy xFG_exact aps1); + assert_bool "mem_fuzzy_harder2" (AccessPathDomains.Set.mem_fuzzy x_abstract aps1); + assert_bool "mem_fuzzy_negative" (not (AccessPathDomains.Set.mem_fuzzy y_exact aps1)); + (* [mem_fuzzy] should behave the same as [mem] except in this case *) + assert_bool + "mem_fuzzy_not_fully_contained" + (AccessPathDomains.Set.mem_fuzzy yF_abstract aps3); + + assert_bool "<= on same is true" (AccessPathDomains.Set.(<=) ~lhs:aps1 ~rhs:aps1); + assert_bool "aps1 <= aps2" (AccessPathDomains.Set.(<=) ~lhs:aps1 ~rhs:aps2); + assert_bool "aps2 <= aps1" (AccessPathDomains.Set.(<=) ~lhs:aps2 ~rhs:aps1); + assert_bool "aps1 <= aps3" (AccessPathDomains.Set.(<=) ~lhs:aps1 ~rhs:aps3); + assert_bool "not aps3 <= aps1" (not (AccessPathDomains.Set.(<=) ~lhs:aps3 ~rhs:aps1)); + + assert_eq (AccessPathDomains.Set.join aps1 aps1) "{ &x*, &x }"; + assert_eq (AccessPathDomains.Set.join aps1 aps2) "{ &x*, &x, &x.f }"; + assert_eq (AccessPathDomains.Set.join aps1 aps3) "{ &x*, &x, &x.f, &y.f }"; + + let widen s1 s2 = + AccessPathDomains.Set.widen ~prev:s1 ~next:s2 ~num_iters:10 in + assert_eq (widen aps1 aps1) "{ &x*, &x }"; + assert_eq (widen aps2 aps3) "{ &x*, &y.f*, &x, &x.f }"; + let aps_prev = AccessPathDomains.Set.of_list [x_exact; y_exact] in (* { x, y } *) + let aps_next = AccessPathDomains.Set.of_list [y_exact; yF_exact] in (* { y. y.f } *) + (* { x, y } \/ { y, y.f } = { y.f*, x, y } *) + assert_eq (widen aps_prev aps_next) "{ &y.f*, &x, &y }"; + (* { y, y.f } \/ { x, y } = { x*, y, y.f } *) + assert_eq (widen aps_next aps_prev) "{ &x*, &y, &y.f }"; + + assert_eq (AccessPathDomains.Set.normalize aps1) "{ &x* }"; + assert_eq (AccessPathDomains.Set.normalize aps2) "{ &x* }"; + assert_eq (AccessPathDomains.Set.normalize aps3) "{ &x*, &y.f }" in + "domain">::domain_test_ in + + "all_tests_suite">:::[equal_test; append_test; prefix_test; abstraction_test; domain_test]