From b8c5192ea1b19a4a0a379a0b37c90f9a6a7d3307 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 11 May 2020 04:37:36 -0700 Subject: [PATCH] remove unused accessPathDomains Summary: The only thing keeping this module alive were unit tests, proving once and for all that unit tests are bad. Reviewed By: ngorogiannis Differential Revision: D21451855 fbshipit-source-id: e63995732 --- infer/src/IR/AccessPath.ml | 83 ----------- infer/src/IR/AccessPath.mli | 17 --- infer/src/checkers/accessPathDomains.ml | 68 --------- infer/src/checkers/accessPathDomains.mli | 36 ----- infer/src/inferunit.ml | 1 - infer/src/unit/accessPathTestUtils.mli | 2 - infer/src/unit/accessPathTests.ml | 177 ----------------------- 7 files changed, 384 deletions(-) delete mode 100644 infer/src/checkers/accessPathDomains.ml delete mode 100644 infer/src/checkers/accessPathDomains.mli delete mode 100644 infer/src/unit/accessPathTests.ml diff --git a/infer/src/IR/AccessPath.ml b/infer/src/IR/AccessPath.ml index cdf273158..85668405d 100644 --- a/infer/src/IR/AccessPath.ml +++ b/infer/src/IR/AccessPath.ml @@ -113,80 +113,7 @@ module Raw = struct match var with Var.LogicalVar id -> of_id id typ | Var.ProgramVar pvar -> of_pvar pvar typ - let of_exp ~include_array_indexes exp0 typ0 ~(f_resolve_id : Var.t -> t option) = - (* [typ] is the type of the last element of the access path (e.g., typeof(g) for x.f.g) *) - let rec of_exp_ exp typ accesses acc = - match exp with - | Exp.Var id -> ( - match f_resolve_id (Var.of_id id) with - | Some (base, base_accesses) -> - (base, base_accesses @ accesses) :: acc - | None -> - (base_of_id id typ, accesses) :: acc ) - | Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> ( - match f_resolve_id (Var.of_pvar pvar) with - | Some (base, base_accesses) -> - (base, base_accesses @ accesses) :: acc - | None -> - (base_of_pvar pvar typ, accesses) :: acc ) - | Exp.Lvar pvar -> - (base_of_pvar pvar typ, accesses) :: acc - | Exp.Lfield (root_exp, fld, root_exp_typ) -> - let field_access = FieldAccess fld in - of_exp_ root_exp root_exp_typ (field_access :: accesses) acc - | Exp.Lindex (root_exp, index_exp) -> - let index_access_paths = - if include_array_indexes then of_exp_ index_exp typ [] [] else [] - in - let array_access = ArrayAccess (typ, index_access_paths) in - let array_typ = Typ.mk_array typ in - of_exp_ root_exp array_typ (array_access :: accesses) acc - | Exp.Cast (cast_typ, cast_exp) -> - of_exp_ cast_exp cast_typ [] acc - | Exp.UnOp (_, unop_exp, _) -> - of_exp_ unop_exp typ [] acc - | Exp.Exn exn_exp -> - of_exp_ exn_exp typ [] acc - | Exp.BinOp (_, exp1, exp2) -> - of_exp_ exp1 typ [] acc |> of_exp_ exp2 typ [] - | Exp.Const _ | Closure _ | Sizeof _ -> - (* trying to make access path from an invalid expression *) - acc - in - of_exp_ exp0 typ0 [] [] - - - let of_lhs_exp ~include_array_indexes lhs_exp typ ~(f_resolve_id : Var.t -> t option) = - match of_exp ~include_array_indexes lhs_exp typ ~f_resolve_id with - | [lhs_ap] -> - Some lhs_ap - | _ -> - None - - let append (base, old_accesses) new_accesses = (base, old_accesses @ new_accesses) - - let rec chop_prefix_path ~prefix:path1 path2 = - if phys_equal path1 path2 then Some [] - else - match (path1, path2) with - | [], remaining -> - Some remaining - | _, [] -> - None - | access1 :: prefix, access2 :: rest when equal_access access1 access2 -> - chop_prefix_path ~prefix rest - | _ -> - None - - - let chop_prefix ~prefix:((base1, path1) as ap1) ((base2, path2) as ap2) = - if phys_equal ap1 ap2 then Some [] - else if equal_base base1 base2 then chop_prefix_path ~prefix:path1 path2 - else None - - - let is_prefix ap1 ap2 = chop_prefix ~prefix:ap1 ap2 |> Option.is_some end module Abs = struct @@ -220,16 +147,6 @@ module Abs = struct let is_exact = function Exact _ -> true | Abstracted _ -> false - let leq ~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 -> - Raw.is_prefix rhs_ap lhs_ap - - let pp fmt = function | Exact access_path -> Raw.pp fmt access_path diff --git a/infer/src/IR/AccessPath.mli b/infer/src/IR/AccessPath.mli index 0116ebd9f..f4ee5e8a4 100644 --- a/infer/src/IR/AccessPath.mli +++ b/infer/src/IR/AccessPath.mli @@ -36,24 +36,10 @@ val of_id : Ident.t -> Typ.t -> t val of_var : Var.t -> Typ.t -> t (** create an access path from a var *) -val of_exp : - include_array_indexes:bool -> Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t list -(** extract the access paths that occur in [exp], resolving identifiers using [f_resolve_id]. don't - include index expressions in array accesses if [include_array_indexes] is false *) - -val of_lhs_exp : - include_array_indexes:bool -> Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t option -(** convert [lhs_exp] to an access path, resolving identifiers using [f_resolve_id] *) - val append : t -> access list -> t (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces `x.f.g.h` *) -val is_prefix : t -> t -> bool -(** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *) - -val equal : t -> t -> bool - val equal_base : base -> base -> bool val pp : Format.formatter -> t -> unit @@ -89,9 +75,6 @@ module Abs : sig val is_exact : t -> bool (** return true if [t] is an exact representation of an access path, false if it's an abstraction *) - val leq : lhs:t -> rhs:t -> bool - (** return true if \gamma(lhs) \subseteq \gamma(rhs) *) - val pp : Format.formatter -> t -> unit end diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml deleted file mode 100644 index dc1d658a2..000000000 --- a/infer/src/checkers/accessPathDomains.ml +++ /dev/null @@ -1,68 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -module Set = struct - module APSet = PrettyPrintable.MakePPSet (AccessPath.Abs) - - (** 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 t = APSet.t - - let pp = APSet.pp - - let bottom = APSet.empty - - let is_bottom = APSet.is_empty - - let normalize aps = - APSet.filter - (fun lhs -> - not - (APSet.exists (fun rhs -> (not (phys_equal lhs rhs)) && AccessPath.Abs.leq ~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.Abs.leq ~lhs:ap ~rhs:other_ap) aps - - - let mem_fuzzy ap aps = - let has_overlap ap1 ap2 = - AccessPath.Abs.leq ~lhs:ap1 ~rhs:ap2 || AccessPath.Abs.leq ~lhs:ap2 ~rhs:ap1 - in - APSet.mem ap aps || APSet.exists (has_overlap ap) aps - - - let leq ~lhs ~rhs = - if phys_equal 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 phys_equal aps1 aps2 then aps1 else APSet.union aps1 aps2 - - let widen ~prev ~next ~num_iters:_ = - if phys_equal prev next then prev - else - let abstract_access_path ap aps = - match ap with - | AccessPath.Abs.Exact exact_ap -> - APSet.add (AccessPath.Abs.Abstracted exact_ap) aps - | AccessPath.Abs.Abstracted _ -> - APSet.add ap aps - in - let diff_aps = APSet.diff next prev in - APSet.fold abstract_access_path diff_aps APSet.empty |> join prev -end diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli deleted file mode 100644 index b9305c0bf..000000000 --- a/infer/src/checkers/accessPathDomains.mli +++ /dev/null @@ -1,36 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -(** 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.WithBottom - - val of_list : AccessPath.Abs.t list -> t - - val mem : AccessPath.Abs.t -> t -> bool - (** return true if [\gamma(\{ap\}) \subseteq \gamma(aps)]. note: this is worst-case linear in the - size of the set *) - - val mem_fuzzy : AccessPath.Abs.t -> t -> 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 add : AccessPath.Abs.t -> t -> t - - val normalize : t -> t - (** 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 *) -end diff --git a/infer/src/inferunit.ml b/infer/src/inferunit.ml index 15de370a8..c50670e01 100644 --- a/infer/src/inferunit.ml +++ b/infer/src/inferunit.ml @@ -27,7 +27,6 @@ let () = (* OUnit runs tests in parallel using fork(2) *) List.map ~f:mk_test_fork_proof ( [ AbstractInterpreterTests.tests - ; AccessPathTests.tests ; AccessTreeTests.tests ; AddressTakenTests.tests ; CStubsTests.tests diff --git a/infer/src/unit/accessPathTestUtils.mli b/infer/src/unit/accessPathTestUtils.mli index 4d40618af..4f21b81e1 100644 --- a/infer/src/unit/accessPathTestUtils.mli +++ b/infer/src/unit/accessPathTestUtils.mli @@ -7,8 +7,6 @@ open! IStd -val make_var : string -> Pvar.t - val make_fieldname : string -> Fieldname.t val make_base : ?typ:Typ.t -> string -> AccessPath.base diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml deleted file mode 100644 index 70ebff44d..000000000 --- a/infer/src/unit/accessPathTests.ml +++ /dev/null @@ -1,177 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd -module F = Format - -let tests = - let open AccessPathTestUtils in - 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 xArr = - let dummy_typ = Typ.void in - let dummy_arr_typ = Typ.mk_array dummy_typ in - let base = make_base "x" ~typ:dummy_arr_typ in - (base, [make_array_access dummy_typ]) - in - let x_exact = AccessPath.Abs.Exact x in - let y_exact = AccessPath.Abs.Exact y in - let x_abstract = AccessPath.Abs.Abstracted x in - let xF_exact = AccessPath.Abs.Exact xF in - let xFG_exact = AccessPath.Abs.Exact xFG in - let yF_exact = AccessPath.Abs.Exact yF in - let yF_abstract = AccessPath.Abs.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 - "equal" >:: equal_test_ - in - let append_test = - let pp_diff fmt (actual, expected) = - F.fprintf fmt "Expected output %a but got %a" AccessPath.pp expected AccessPath.pp actual - in - let assert_eq input expected = assert_equal ~cmp:AccessPath.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 - "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 - let of_exp_test = - let f_resolve_id _ = None in - let dummy_typ = Typ.void in - let check_make_ap exp expected_ap ~f_resolve_id = - let make_ap exp = - match AccessPath.of_lhs_exp ~include_array_indexes:true exp dummy_typ ~f_resolve_id with - | Some ap -> - ap - | None -> - assert false - in - let actual_ap = make_ap exp in - let pp_diff fmt (actual_ap, expected_ap) = - F.fprintf fmt "Expected to make access path %a from expression %a, but got %a" AccessPath.pp - expected_ap Exp.pp exp AccessPath.pp actual_ap - in - assert_equal ~cmp:AccessPath.equal ~pp_diff actual_ap expected_ap - in - let of_exp_test_ _ = - let f_fieldname = make_fieldname "f" in - let g_fieldname = make_fieldname "g" in - let x_exp = Exp.Lvar (make_var "x") in - check_make_ap x_exp x ~f_resolve_id ; - let xF_exp = Exp.Lfield (x_exp, f_fieldname, dummy_typ) in - check_make_ap xF_exp xF ~f_resolve_id ; - let xFG_exp = Exp.Lfield (xF_exp, g_fieldname, dummy_typ) in - check_make_ap xFG_exp xFG ~f_resolve_id ; - let xArr_exp = Exp.Lindex (x_exp, Exp.zero) in - check_make_ap xArr_exp xArr ~f_resolve_id ; - (* make sure [f_resolve_id] works *) - let f_resolve_id_to_xF _ = Some xF in - let xFG_exp_with_id = - let id_exp = Exp.Var (Ident.create_normal (Ident.string_to_name "") 0) in - Exp.Lfield (id_exp, g_fieldname, dummy_typ) - in - check_make_ap xFG_exp_with_id xFG ~f_resolve_id:f_resolve_id_to_xF ; - (* make sure we can grab access paths from compound expressions *) - let binop_exp = Exp.le xF_exp xFG_exp in - match AccessPath.of_exp ~include_array_indexes:true binop_exp dummy_typ ~f_resolve_id with - | [ap1; ap2] -> - assert_equal ~cmp:AccessPath.equal ap1 xFG ; - assert_equal ~cmp:AccessPath.equal ap2 xF - | _ -> - assert false - in - "of_exp" >:: of_exp_test_ - in - let abstraction_test = - let abstraction_test_ _ = - assert_bool "extract" (AccessPath.equal (AccessPath.Abs.extract xF_exact) xF) ; - assert_bool "is_exact" (AccessPath.Abs.is_exact x_exact) ; - assert_bool "not is_exact" (not (AccessPath.Abs.is_exact x_abstract)) ; - assert_bool "(<=)1" (AccessPath.Abs.leq ~lhs:x_exact ~rhs:x_abstract) ; - assert_bool "(<=)2" (AccessPath.Abs.leq ~lhs:xF_exact ~rhs:x_abstract) ; - assert_bool "not (<=)1" (not (AccessPath.Abs.leq ~lhs:x_abstract ~rhs:x_exact)) ; - assert_bool "not (<=)2" (not (AccessPath.Abs.leq ~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 = F.asprintf "%a" AccessPathDomains.Set.pp input_aps in - assert_equal ~cmp:String.equal ~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.leq ~lhs:aps1 ~rhs:aps1) ; - assert_bool "aps1 <= aps2" (AccessPathDomains.Set.leq ~lhs:aps1 ~rhs:aps2) ; - assert_bool "aps2 <= aps1" (AccessPathDomains.Set.leq ~lhs:aps2 ~rhs:aps1) ; - assert_bool "aps1 <= aps3" (AccessPathDomains.Set.leq ~lhs:aps1 ~rhs:aps3) ; - assert_bool "not aps3 <= aps1" (not (AccessPathDomains.Set.leq ~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; of_exp_test; abstraction_test; domain_test]