From a673a13b444f20e1f226d4dd22f2465a4ed00d02 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Fri, 30 Oct 2020 05:13:10 -0700 Subject: [PATCH] [nullsafe][refactor] Store all joinees' origins in InferredNullability Summary: The fact that we did not preserve all joins (and used only the first one) was a shorcut since the origin is used only for reporting, and reporting the info about left joinee is enough for practical purposes. Hovewer, to support annotation graph, we need all joinees. This diff is a no-op since we use only the first one currently. Reviewed By: artempyanykh Differential Revision: D24621412 fbshipit-source-id: 8fe1174e7 --- infer/src/nullsafe/AssignmentRule.ml | 2 +- infer/src/nullsafe/DereferenceRule.ml | 2 +- infer/src/nullsafe/InferredNullability.ml | 45 +++++++++++++++------- infer/src/nullsafe/InferredNullability.mli | 2 +- infer/src/nullsafe/eradicateChecks.ml | 4 +- infer/src/nullsafe/typeCheck.ml | 14 +++---- infer/src/nullsafe/typeState.ml | 2 +- 7 files changed, 45 insertions(+), 26 deletions(-) diff --git a/infer/src/nullsafe/AssignmentRule.ml b/infer/src/nullsafe/AssignmentRule.ml index fa9ee785c..0103e5106 100644 --- a/infer/src/nullsafe/AssignmentRule.ml +++ b/infer/src/nullsafe/AssignmentRule.ml @@ -218,7 +218,7 @@ module ReportableViolation = struct let make_nullsafe_issue ~assignment_location assignment_type {nullsafe_mode; violation= {rhs}} = - let rhs_origin = InferredNullability.get_origin rhs in + let rhs_origin = InferredNullability.get_simple_origin rhs in let user_friendly_nullable = ErrorRenderingUtils.UserFriendlyNullable.from_nullability (InferredNullability.get_nullability rhs) diff --git a/infer/src/nullsafe/DereferenceRule.ml b/infer/src/nullsafe/DereferenceRule.ml index f82819f64..6d245d132 100644 --- a/infer/src/nullsafe/DereferenceRule.ml +++ b/infer/src/nullsafe/DereferenceRule.ml @@ -114,7 +114,7 @@ module ReportableViolation = struct "get_description:: Dereference violation should not be possible for non-nullable \ values" ) in - let nullable_object_origin = InferredNullability.get_origin nullability in + let nullable_object_origin = InferredNullability.get_simple_origin nullability in match user_friendly_nullable with | ErrorRenderingUtils.UserFriendlyNullable.UntrustedNonnull untrusted_kind -> (* Attempt to dereference a value which is not explictly declared as nullable, diff --git a/infer/src/nullsafe/InferredNullability.ml b/infer/src/nullsafe/InferredNullability.ml index 55a98fbb0..1a566fb51 100644 --- a/infer/src/nullsafe/InferredNullability.ml +++ b/infer/src/nullsafe/InferredNullability.ml @@ -7,9 +7,24 @@ open! IStd -type t = {nullability: Nullability.t; origin: TypeOrigin.t} [@@deriving compare] +type t = + { nullability: Nullability.t + ; origins: TypeOrigin.t list (** Origins responsible for this nullability type *) } +[@@deriving compare] + +let rec sanitize_origin = function + (* Collapse consecutive chains of InferredNonnull to get rid of infinite chains in loops and + hence allowing to reach the fixpoint *) + | TypeOrigin.InferredNonnull + {previous_origin= TypeOrigin.InferredNonnull {previous_origin= underlying}} -> + TypeOrigin.InferredNonnull {previous_origin= underlying} |> sanitize_origin + | other -> + other + + +let create origin = + {nullability= TypeOrigin.get_nullability origin; origins= [sanitize_origin origin]} -let create origin = {nullability= TypeOrigin.get_nullability origin; origin} let get_nullability {nullability} = nullability @@ -17,6 +32,11 @@ let is_nonnullish {nullability} = Nullability.is_nonnullish nullability let pp fmt {nullability} = Nullability.pp fmt nullability +(* Join two lists with removing duplicates and preserving the order of join *) +let join_origins origins1 origins2 = + (IList.append_no_duplicates ~cmp:TypeOrigin.compare |> Staged.unstage) origins1 origins2 + + let join t1 t2 = let joined_nullability = Nullability.join t1.nullability t2.nullability in let is_equal_to_t1 = Nullability.equal t1.nullability joined_nullability in @@ -25,28 +45,27 @@ let join t1 t2 = If nullability is fully determined by one of the arguments, origin should be get from this argument. Otherwise we apply heuristics to choose origin either from t1 or t2. *) - let joined_origin = + let joined_origins = match (is_equal_to_t1, is_equal_to_t2) with | _ when Nullability.equal t1.nullability Nullability.Null -> - t1.origin + t1.origins | _ when Nullability.equal t2.nullability Nullability.Null -> - t2.origin + t2.origins | true, false -> (* Nullability was fully determined by t1. *) - t1.origin + t1.origins | false, true -> (* Nullability was fully determined by t2 *) - t2.origin + t2.origins | false, false | true, true -> - (* Nullability is not fully determined by neither t1 nor t2 - Picking the left one for stability + (* Nullability is not fully determined by neither t1 nor t2 - join both lists *) - t1.origin + join_origins t1.origins t2.origins in - {nullability= joined_nullability; origin= joined_origin} + {nullability= joined_nullability; origins= joined_origins} -let get_origin t = t.origin +let get_simple_origin t = List.nth_exn t.origins 0 let origin_is_fun_defined t = - match get_origin t with TypeOrigin.MethodCall {is_defined; _} -> is_defined | _ -> false + match get_simple_origin t with TypeOrigin.MethodCall {is_defined; _} -> is_defined | _ -> false diff --git a/infer/src/nullsafe/InferredNullability.mli b/infer/src/nullsafe/InferredNullability.mli index 2690ece70..bc314ccb2 100644 --- a/infer/src/nullsafe/InferredNullability.mli +++ b/infer/src/nullsafe/InferredNullability.mli @@ -23,7 +23,7 @@ val create : TypeOrigin.t -> t val is_nonnullish : t -> bool (** Check whether corresponding [Nullability] is [Nullability.is_nonnullish] *) -val get_origin : t -> TypeOrigin.t +val get_simple_origin : t -> TypeOrigin.t (** The simple explanation of how was nullability inferred. *) val join : t -> t -> t diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index ff5c45abe..e0b953e1f 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -104,7 +104,7 @@ let check_condition_for_redundancy So Condition_redundant should either accept expression, or this should pass a condition. *) let condition_descr = explain_expr tenv node expr in - let nonnull_origin = InferredNullability.get_origin inferred_nullability in + let nonnull_origin = InferredNullability.get_simple_origin inferred_nullability in TypeErr.register_error analysis_data find_canonical_duplicate (TypeErr.Condition_redundant {is_always_true; loc; condition_descr; nonnull_origin}) (Some instr_ref) ~nullsafe_mode @@ -256,7 +256,7 @@ let check_constructor_initialization predicate_holds_for_some_typestate (Lazy.force typestates_for_curr_constructor_and_all_initializer_methods) field_name ~predicate:(fun (_, nullability) -> - is_initialized (InferredNullability.get_origin nullability) ) + is_initialized (InferredNullability.get_simple_origin nullability) ) in (* TODO(T54584721) This check is completely independent of the current constuctor we check. This check should be moved out of this function. Until it is done, diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 38b534de5..fc65602a5 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -160,7 +160,7 @@ let rec typecheck_expr ({IntraproceduralAnalysis.tenv; _} as analysis_data) ~nul (typ, InferredNullability.create TypeOrigin.OptimisticFallback) loc in - let object_origin = InferredNullability.get_origin inferred_nullability in + let object_origin = InferredNullability.get_simple_origin inferred_nullability in let tr_new = match AnnotatedField.get tenv field_name typ with | Some AnnotatedField.{annotated_type= field_type} -> @@ -207,7 +207,7 @@ let handle_field_access_via_temporary idenv curr_pname typestate exp = let pvar_get_origin pvar = match TypeState.lookup_pvar pvar typestate with | Some (_, inferred_nullability) -> - Some (InferredNullability.get_origin inferred_nullability) + Some (InferredNullability.get_simple_origin inferred_nullability) | None -> None in @@ -313,7 +313,7 @@ let convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_ | _ -> None ) |> Option.value_map - ~f:(fun (_, nullability) -> InferredNullability.get_origin nullability) + ~f:(fun (_, nullability) -> InferredNullability.get_simple_origin nullability) ~default:TypeOrigin.OptimisticFallback in let exp' = IDEnv.expand_expr_temps idenv original_node exp_ in @@ -526,9 +526,9 @@ let do_preconditions_check_not_null { is_always_true= true ; loc ; condition_descr= EradicateChecks.explain_expr tenv node cond - ; nonnull_origin= InferredNullability.get_origin nullability }) + ; nonnull_origin= InferredNullability.get_simple_origin nullability }) (Some instr_ref) ~nullsafe_mode ) ; - let previous_origin = InferredNullability.get_origin nullability in + let previous_origin = InferredNullability.get_simple_origin nullability in let new_origin = TypeOrigin.InferredNonnull {previous_origin} in TypeState.add pvar (t, InferredNullability.create new_origin) @@ -577,7 +577,7 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_ (* handle the annotation flag for pvar *) match TypeState.lookup_pvar pvar typestate1 with | Some (t, nullability) -> - let previous_origin = InferredNullability.get_origin nullability in + let previous_origin = InferredNullability.get_simple_origin nullability in let new_origin = TypeOrigin.InferredNonnull {previous_origin} in TypeState.add pvar (t, InferredNullability.create new_origin) @@ -851,7 +851,7 @@ let rec check_condition_for_sil_prune | Some (t, current_nullability) -> let new_origin = TypeOrigin.InferredNonnull - {previous_origin= InferredNullability.get_origin current_nullability} + {previous_origin= InferredNullability.get_simple_origin current_nullability} in let new_nullability = InferredNullability.create new_origin in TypeState.add pvar (t, new_nullability) typestate' ~descr diff --git a/infer/src/nullsafe/typeState.ml b/infer/src/nullsafe/typeState.ml index f868e2de0..38317ed66 100644 --- a/infer/src/nullsafe/typeState.ml +++ b/infer/src/nullsafe/typeState.ml @@ -32,7 +32,7 @@ let empty = M.empty let pp fmt typestate = let pp_one exp (typ, ta) = F.fprintf fmt " %a -> [%s] %a %a@\n" Exp.pp exp - (TypeOrigin.to_string (InferredNullability.get_origin ta)) + (TypeOrigin.to_string (InferredNullability.get_simple_origin ta)) InferredNullability.pp ta (Typ.pp_full Pp.text) typ in let pp_map map = M.iter pp_one map in