From eded9141d982d0ff996b6df927d7f0776b3f2e86 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Fri, 7 Feb 2020 02:17:02 -0800 Subject: [PATCH] [nullsafe][refactor] Clean up code responsible for manipulations with `containsKey()` Summary: The whole TypeCheck.ml is exceptionally hard to read and maintain, lets clean up it a bit. Reviewed By: ngorogiannis Differential Revision: D19743632 fbshipit-source-id: c24c21a85 --- infer/src/nullsafe/ErrorRenderingUtils.ml | 27 ++++++++-------- infer/src/nullsafe/typeCheck.ml | 39 +++++++++++++---------- infer/src/nullsafe/typeErr.ml | 1 + infer/src/nullsafe/typeOrigin.ml | 18 +++++++++-- infer/src/nullsafe/typeOrigin.mli | 3 ++ 5 files changed, 55 insertions(+), 33 deletions(-) diff --git a/infer/src/nullsafe/ErrorRenderingUtils.ml b/infer/src/nullsafe/ErrorRenderingUtils.ml index ea4e3f9d2..c8708ffd7 100644 --- a/infer/src/nullsafe/ErrorRenderingUtils.ml +++ b/infer/src/nullsafe/ErrorRenderingUtils.ml @@ -7,7 +7,7 @@ open! IStd -let is_object_nullability_self_explanatory ~object_expression object_origin = +let is_object_nullability_self_explanatory ~object_expression (object_origin : TypeOrigin.t) = (* Fundamentally, object can be of two kinds: 1. Indirect: local variable that was instantiated before. In this case, normally origin is NOT trivial @@ -19,21 +19,21 @@ let is_object_nullability_self_explanatory ~object_expression object_origin = to be 100% precise. *) match object_origin with - | TypeOrigin.NullConst _ -> + | NullConst _ -> (* Expect either a local variable or null literal (latter case is trivial) *) String.equal object_expression "null" - | TypeOrigin.MethodParameter {mangled} -> + | MethodParameter {mangled} -> (* Either local variable or literally parameter. In latter case, its nullability is self-explanatory because the user can quickly see the current method signature. *) let param_name = Mangled.to_string mangled in String.equal object_expression param_name - | TypeOrigin.Field {field_name} -> + | Field {field_name} -> (* Either local variable or expression like `.field_name`. Latter case is trivial: the user can quickly go to field_name definition and see if its annotation. *) let field_name_str = Fieldname.get_field_name field_name in String.is_suffix object_expression ~suffix:field_name_str - | TypeOrigin.MethodCall {pname; annotated_signature= {model_source}} -> + | MethodCall {pname; annotated_signature= {model_source}} -> let is_modelled = Option.is_some model_source in if is_modelled then (* This is non-trivial and should always be explained to the user *) false @@ -47,14 +47,15 @@ let is_object_nullability_self_explanatory ~object_expression object_origin = (* These cases are not yet supported because they normally mean non-nullable case, for which we don't render important messages yet. *) - | TypeOrigin.NonnullConst _ - | TypeOrigin.This - | TypeOrigin.New - | TypeOrigin.ArrayLengthResult - | TypeOrigin.ArrayAccess - | TypeOrigin.InferredNonnull _ - | TypeOrigin.OptimisticFallback - | TypeOrigin.Undef -> + | NonnullConst _ + | This + | New + | CallToGetKnownToContainsKey + | ArrayLengthResult + | ArrayAccess + | InferredNonnull _ + | OptimisticFallback + | Undef -> false diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 8bf53a45e..bb78db8b3 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -677,10 +677,14 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli in (* check if the expression is coming from Map.containsKey *) let from_containsKey e : Exp.t option = from_call ComplexExpressions.procname_containsKey e in - (* Turn x.containsKey(e) into the pvar for x.get(e) *) - (* which is then treated as a normal condition != null. *) - let handle_containsKey e = - let map_dexp = function + (* Call to x.containsKey(e) returned `true`. + It means that subsequent calls to `x.get(e)` should be inferred as non-nullables. + We achieve this behavior by adding the result of a call to `x.get(e)` (in form of corresponding pvar) + to a typestate, with correspnding (non-null) type origin. + *) + let handle_containsKey_returned_true call_to_containsKey_exr = + let replace_contains_key_with_get_in_a_function_call_expression = function + (* This will replace x.containsKey(e) to x.get(e) *) | Some (DExp.Dretcall (DExp.Dconst (Const.Cfun (Procname.Java pname_java)), args, loc, call_flags)) -> @@ -695,19 +699,20 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli | _ -> None in - match ComplexExpressions.exp_to_string_map_dexp tenv map_dexp node e with - | Some e_str -> - let pvar = Pvar.mk (Mangled.from_string e_str) curr_pname in - let e1 = Exp.Lvar pvar in - let typ, ta = - typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks - tenv original_node instr_ref typestate e1 Typ.void TypeOrigin.OptimisticFallback loc - in - let range = (typ, ta) in - let typestate1 = TypeState.add pvar range typestate in - (typestate1, e1, EradicateChecks.From_containsKey) + let string_representing_call_to_get = + ComplexExpressions.exp_to_string_map_dexp tenv + replace_contains_key_with_get_in_a_function_call_expression node call_to_containsKey_exr + in + match string_representing_call_to_get with + | Some expr_str -> + (* Add pvar representing call to `get` to a typestate, indicating that it is a non-nullable *) + let pvar = Pvar.mk (Mangled.from_string expr_str) curr_pname in + let pvar_expr = Exp.Lvar pvar in + let range = (Typ.void, InferredNullability.create TypeOrigin.CallToGetKnownToContainsKey) in + let typestate_with_new_pvar = TypeState.add pvar range typestate in + (typestate_with_new_pvar, pvar_expr, EradicateChecks.From_containsKey) | None -> - (typestate, e, EradicateChecks.From_condition) + (typestate, call_to_containsKey_exr, EradicateChecks.From_condition) in let set_nonnull e' typestate2 = let handle_pvar typestate' pvar = @@ -775,7 +780,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli | Some e1 -> (typestate, e1, EradicateChecks.From_is_false_on_null) | None -> - if Option.is_some (from_containsKey e) then handle_containsKey e + if Option.is_some (from_containsKey e) then handle_containsKey_returned_true e else (typestate, e, EradicateChecks.From_condition) ) in let e', typestate2 = diff --git a/infer/src/nullsafe/typeErr.ml b/infer/src/nullsafe/typeErr.ml index a59606d73..073451840 100644 --- a/infer/src/nullsafe/typeErr.ml +++ b/infer/src/nullsafe/typeErr.ml @@ -250,6 +250,7 @@ let get_nonnull_explanation_for_condition_redudant (nonnull_origin : TypeOrigin. (* TODO: this could be specified more precisely *) | NonnullConst _ | Field _ + | CallToGetKnownToContainsKey | MethodParameter _ | This | New diff --git a/infer/src/nullsafe/typeOrigin.ml b/infer/src/nullsafe/typeOrigin.ml index 0ec1037f2..4f79e921d 100644 --- a/infer/src/nullsafe/typeOrigin.ml +++ b/infer/src/nullsafe/typeOrigin.ml @@ -16,6 +16,9 @@ type t = | MethodParameter of AnnotatedSignature.param_signature (** A method's parameter *) | This (* `this` object. Can not be null, according to Java rules. *) | MethodCall of method_call_origin (** A result of a method call *) + | CallToGetKnownToContainsKey + (** This is a result of accessing a map element that is known to contains this particular key, + normally because it was explicitly checked for presense before *) | New (** A new object creation *) | ArrayLengthResult (** integer value - result of accessing array.length *) | ArrayAccess (** Result of accessing an array by index *) @@ -52,6 +55,7 @@ let get_nullability = function | This (* `this` can not be null according to Java rules *) | New (* In Java `new` always create a non-null object *) | ArrayLengthResult (* integer hence non-nullable *) + | CallToGetKnownToContainsKey (* non-nullable by definition *) | InferredNonnull _ (* WARNING: we trade soundness for usability. In Java, arrays are initialized with null, so accessing array is nullable until it was initialized. @@ -86,14 +90,16 @@ let rec to_string = function "this" | MethodCall {pname} -> Printf.sprintf "Fun %s" (Procname.to_simplified_string pname) + | CallToGetKnownToContainsKey -> + "CallToGetKnownToContainsKey" | New -> "New" | ArrayLengthResult -> "ArrayLength" | ArrayAccess -> "ArrayAccess" - | InferredNonnull _ -> - "InferredNonnull" + | InferredNonnull {previous_origin} -> + Format.sprintf "InferredNonnull(prev:%s)" (to_string previous_origin) | OptimisticFallback -> "OptimisticFallback" | Undef -> @@ -153,7 +159,13 @@ let get_description origin = But for these issues we currently don't print origins in the error string. It is a good idea to change this and start printing origins for these origins as well. *) - | This | New | NonnullConst _ | ArrayLengthResult | ArrayAccess | InferredNonnull _ -> + | This + | New + | NonnullConst _ + | ArrayLengthResult + | ArrayAccess + | InferredNonnull _ + | CallToGetKnownToContainsKey -> None (* Two special cases - should not really occur in normal code *) | OptimisticFallback | Undef -> diff --git a/infer/src/nullsafe/typeOrigin.mli b/infer/src/nullsafe/typeOrigin.mli index 3500730a9..ba14b9481 100644 --- a/infer/src/nullsafe/typeOrigin.mli +++ b/infer/src/nullsafe/typeOrigin.mli @@ -14,6 +14,9 @@ type t = | MethodParameter of AnnotatedSignature.param_signature (** A method's parameter *) | This (* `this` object. Can not be null, according to Java rules. *) | MethodCall of method_call_origin (** A result of a method call *) + | CallToGetKnownToContainsKey + (** This is a result of accessing a map element that is known to contains this particular key, + normally because it was explicitly checked for presense before *) | New (** A new object creation *) | ArrayLengthResult (** integer value - result of accessing array.length *) | ArrayAccess (** Result of accessing an array by index *)