[thread-safety] fix infinite loop in quotient_access_map

Summary:
This was a subtle one. The ranking function of `aux` is the cardinality of `m`..
But if `may_alias` is not reflexive, then `k_part` will be empty, `non_k_part` will be the same size, and we'll diverge.
Sneakily, `may_alias` is actually *not* reflexive because `is_subtype t1 t2` doesn't check for the equality of `t1` and `t2`.
That is confusing and should be fixed separately.

For now, just make sure `may_alias` is always reflexive and add an assertion that `k_part` is never empty.

Reviewed By: jeremydubreil

Differential Revision: D5177427

fbshipit-source-id: 0549d6a

infer/src/checkers/ThreadSafety.ml

@@ -1246,6 +1246,7 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map =
 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
   (* fields in Java contain the class name /declaring/ them
@@ -1275,6 +1276,8 @@ let quotient_access_map acc_map =
       (* assumption: the tenv for k is sufficient for k' too *)
       let (k_part, non_k_part) =
         AccessListMap.partition (fun k' _ -> may_alias tenv k k') m in
+      if AccessListMap.is_empty k_part
+      then failwith "Error: may_alias is not reflexive!";
       let k_accesses =
         AccessListMap.fold
           (fun _ v acc' -> List.append v acc')