diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index c03391b9b..a021121b4 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -1378,54 +1378,33 @@ module MayAliasQuotientedAccessListMap : QuotientedAccessListMap = struct add k (d :: ds) m - let sound = false - let syntactic_equal_access_path tenv p1 p2 = - if sound then - (* this is much too noisy: we'll warn that accesses to *any* Map can race with accesses to any - other Map, etc. Instead, do something simple and unsound: just assume that two accesses can - be to the same container if they are to the same access path *) - match (AccessPath.get_typ p1 tenv, AccessPath.get_typ p2 tenv) with - | Some {desc= Tptr ({desc= Tstruct tn1}, _)}, Some {desc= Tptr ({desc= Tstruct tn2}, _)} -> - PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1 - | _ -> - true - else - (* unsound, but effective: report that the containers alias if their access paths are - syntactically identical *) - match (fst p1, fst p2) with - | (Var.ProgramVar pvar1, typ1), (Var.ProgramVar pvar2, typ2) - when Pvar.is_this pvar1 && Pvar.is_this pvar2 - && ( Typ.equal typ1 typ2 || Prover.Subtyping_check.check_subtype tenv typ1 typ2 - || Prover.Subtyping_check.check_subtype tenv typ2 typ1 ) -> - (* the `this` used in C.foo and C.bar will compare unequal if we're not careful `this` is - represented as a local pvar, and a local pvar contains its parent procedure name. Count - the `this`'s as equal if their types are compatible *) - AccessPath.equal_access_list (snd p1) (snd p2) - | _ -> - AccessPath.equal p1 p2 + (* unsound, but effective: report that the containers alias if their access paths are + syntactically identical *) + match (fst p1, fst p2) with + | (Var.ProgramVar pvar1, typ1), (Var.ProgramVar pvar2, typ2) + when Pvar.is_this pvar1 && Pvar.is_this pvar2 + && ( Typ.equal typ1 typ2 || Prover.Subtyping_check.check_subtype tenv typ1 typ2 + || Prover.Subtyping_check.check_subtype tenv typ2 typ1 ) -> + (* the `this` used in C.foo and C.bar will compare unequal if we're not careful `this` is + represented as a local pvar, and a local pvar contains its parent procedure name. Count + the `this`'s as equal if their types are compatible *) + AccessPath.equal_access_list (snd p1) (snd p2) + | _ -> + AccessPath.equal p1 p2 (* equivalence relation computing whether two access paths may refer to the same heap location. *) let may_alias tenv p1 p2 = - let open Typ in let open AccessPath in phys_equal p1 p2 || match (List.last_exn (snd p1), List.last_exn (snd p2)) with | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _ -> false - | FieldAccess _, FieldAccess _ -> + | _, _ -> syntactic_equal_access_path tenv p1 p2 - (* if arrays of objects that have an inheritance rel then they can alias *) - | ( ArrayAccess ({desc= Tptr ({desc= Tstruct tn1}, _)}, _) - , ArrayAccess ({desc= Tptr ({desc= Tstruct tn2}, _)}, _) ) -> - if sound then PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1 - else syntactic_equal_access_path tenv p1 p2 - (* primitive type arrays can alias if the prim. type is the same *) - | ArrayAccess (t1, _), ArrayAccess (t2, _) -> - if sound then equal_desc t1.desc t2.desc else syntactic_equal_access_path tenv p1 p2 (* take a results table and quotient it by the may_alias relation *)