add abstraction of access path, use in access path set domain

Reviewed By: dkgi

Differential Revision: D3521054

fbshipit-source-id: 3ff515b

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

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

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

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

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]