From 3e45a249d505239487257da78823b2a33533dd90 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 2 Jun 2017 16:28:25 -0700 Subject: [PATCH] [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 | 3 +++ 1 file changed, 3 insertions(+) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index f96d3bc8b..7dd83b0c3 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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')