[thread-safety][c++] Do not quotient by may_alias when analyzing non-Java code

Summary: The may alias analysis relation that the thread safety analysis uses is very specific to Java and causes many false alarms for C++ code. This diff disables it when analyzing C++ code. Improving it to avoid false negatives is left for later.

Reviewed By: sblackshear

Differential Revision: D5974182

fbshipit-source-id: 9c7fc65

infer/src/IR/Pvar.ml

@@ -31,7 +31,7 @@ type pvar_kind =
   [@@deriving compare]
 
 (** Names for program variables. *)
-and t = {pv_hash: int; pv_name: Mangled.t; pv_kind: pvar_kind} [@@deriving compare]
+type t = {pv_hash: int; pv_name: Mangled.t; pv_kind: pvar_kind} [@@deriving compare]
 
 let equal = [%compare.equal : t]
 

infer/src/IR/Tenv.ml

@@ -139,3 +139,14 @@ let store_to_file (filename: DB.filename) (tenv: t) =
     let out_channel = Out_channel.create debug_filename in
     let fmt = Format.formatter_of_out_channel out_channel in
     Format.fprintf fmt "%a" pp tenv ; Out_channel.close out_channel
+
+exception Found of Typ.Name.t
+
+let language_is tenv lang =
+  match TypenameHash.iter (fun n -> raise (Found n)) tenv with
+  | ()
+   -> false
+  | exception Found JavaClass _
+   -> Config.equal_language lang Java
+  | exception Found _
+   -> Config.equal_language lang Clang

infer/src/IR/Tenv.mli

@@ -54,3 +54,6 @@ val store_to_file : DB.filename -> t -> unit
 
 val get_overriden_method : t -> Typ.Procname.java -> Typ.Procname.t option
 (** Get method that is being overriden by java_pname (if any) **)
+
+val language_is : t -> Config.language -> bool
+(** Test the language from which the types in the tenv were translated *)

infer/src/checkers/ThreadSafety.ml

@@ -1553,7 +1553,7 @@ let report_unsafe_accesses
 
 let sound = false
 
-let may_alias_container tenv p1 p2 =
+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
@@ -1569,7 +1569,7 @@ let may_alias_container tenv p1 p2 =
     match (fst p1, fst p2) with
     | (Var.ProgramVar pvar1, typ1), (Var.ProgramVar pvar2, typ2)
       when Pvar.is_this pvar1 && Pvar.is_this pvar2
-           && ( Prover.Subtyping_check.check_subtype tenv typ1 typ2
+           && ( 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
@@ -1585,21 +1585,23 @@ let may_alias tenv p1 p2 =
   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
-  (* fields in Java contain the class name /declaring/ them
+  if Tenv.language_is tenv Clang then syntactic_equal_access_path tenv p1 p2
+  else
+    match (List.last_exn (snd p1), List.last_exn (snd p2)) with
+    | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _
+     -> false
+    (* fields in Java contain the class name /declaring/ them
      thus two fields can be aliases *iff* they are equal *)
-  | FieldAccess f1, FieldAccess f2
-   -> Typ.Fieldname.equal f1 f2
-  (* 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 may_alias_container 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 may_alias_container tenv p1 p2
+    | FieldAccess f1, FieldAccess f2
+     -> Typ.Fieldname.equal f1 f2
+    (* 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 *)
 let quotient_access_map acc_map =
@@ -1620,7 +1622,7 @@ let quotient_access_map acc_map =
              -> may_alias tenv ap1 ap2
             | ( (ContainerRead (ap1, _) | ContainerWrite (ap1, _))
               , (ContainerRead (ap2, _) | ContainerWrite (ap2, _)) )
-             -> may_alias_container tenv ap1 ap2
+             -> syntactic_equal_access_path tenv ap1 ap2
             | _
              -> ThreadSafetyDomain.Access.equal k k')
           m