From 74c8629d13c0df31fedc7a8d41106e0410390a99 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Tue, 24 Sep 2019 03:37:44 -0700 Subject: [PATCH] [nullsafe] Rename TypeAnnotation to InferredNullability Summary: Now, after series of modifications with TypeAnnotation, we are ready to rename it to reflect what it means in the code. See the documentation in the class for details. Also: - renamed methods for clarity - added some documentation - renamed local variables around the usages Reviewed By: jvillard Differential Revision: D17480799 fbshipit-source-id: d4408887a --- ...peAnnotation.ml => InferredNullability.ml} | 4 +- infer/src/nullsafe/InferredNullability.mli | 60 +++++++++ infer/src/nullsafe/eradicate.ml | 8 +- infer/src/nullsafe/eradicateChecks.ml | 74 +++++------ infer/src/nullsafe/typeAnnotation.mli | 33 ----- infer/src/nullsafe/typeCheck.ml | 115 ++++++++++-------- infer/src/nullsafe/typeState.ml | 14 ++- infer/src/nullsafe/typeState.mli | 2 +- 8 files changed, 177 insertions(+), 133 deletions(-) rename infer/src/nullsafe/{typeAnnotation.ml => InferredNullability.ml} (93%) create mode 100644 infer/src/nullsafe/InferredNullability.mli delete mode 100644 infer/src/nullsafe/typeAnnotation.mli diff --git a/infer/src/nullsafe/typeAnnotation.ml b/infer/src/nullsafe/InferredNullability.ml similarity index 93% rename from infer/src/nullsafe/typeAnnotation.ml rename to infer/src/nullsafe/InferredNullability.ml index e015fcea3..0bb0f98a1 100644 --- a/infer/src/nullsafe/typeAnnotation.ml +++ b/infer/src/nullsafe/InferredNullability.ml @@ -7,8 +7,6 @@ open! IStd -(** Module to represent annotations on types. *) - type t = {is_nullable: bool; origin: TypeOrigin.t} [@@deriving compare] let equal = [%compare.equal: t] @@ -50,7 +48,7 @@ let origin_is_fun_library ta = false -let const_nullable is_nullable origin = {origin; is_nullable} +let create ~is_nullable origin = {origin; is_nullable} let with_origin ta o = {ta with origin= o} diff --git a/infer/src/nullsafe/InferredNullability.mli b/infer/src/nullsafe/InferredNullability.mli new file mode 100644 index 000000000..4bc77ef14 --- /dev/null +++ b/infer/src/nullsafe/InferredNullability.mli @@ -0,0 +1,60 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +(** Module to represent nullability of expressions inferred during + flow-sensitive symbolic execution. + NOTE: This module is complementaty to {!NullsafeType.nullability}. + {!NullsafeType} contains info about _formal_ nullability + (what does the code say about nullability of a given type, according to + explicit annotations and implicit agreements (e.g. models)). + In contrast, InferredNullability represents what Nullsafe thinks about such and such + expression according to its type inference rules. + *) + +type t [@@deriving compare] + +val create : is_nullable:bool -> TypeOrigin.t -> t + +val descr_origin : t -> TypeErr.origin_descr +(** Human-readable description of the origin of a value. + (How did nullsafe infer the nullability ) + *) + +val from_nullsafe_type : NullsafeType.t -> TypeOrigin.t -> t +(** Convert formal type to inferred nullability. + (e.g. to infer nullability of `o` in `Object o = someFunction();` + based on `someFunction()` formal return type. + *) + +val get_origin : t -> TypeOrigin.t +(** The simple explanation of how was nullability inferred. *) + +val is_nullable : t -> bool + +val join : t -> t -> t option +(** This is what happens with nullability when we join two flows in CFG, + e.g. + {[ + if(something) { + a = e1; + } else { + a = e2; + } + // what is nullability of `a` at this point? + ]} + *) + +val origin_is_fun_library : t -> bool + +val set_nullable : bool -> t -> t + +val to_string : t -> string + +val with_origin : t -> TypeOrigin.t -> t +(** Leave the same nullability, but change the origin *) diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index 5fc8f7540..c33e5f9aa 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -34,11 +34,13 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct annotated_signature linereader proc_loc : bool * TypeState.t option = let add_formal typestate (param_signature : AnnotatedSignature.param_signature) = let pvar = Pvar.mk param_signature.mangled curr_pname in - let ta = + let inferred_nullability = let origin = TypeOrigin.Formal param_signature.mangled in - TypeAnnotation.from_nullsafe_type param_signature.param_nullsafe_type origin + InferredNullability.from_nullsafe_type param_signature.param_nullsafe_type origin in - TypeState.add pvar (param_signature.param_nullsafe_type.typ, ta, []) typestate + TypeState.add pvar + (param_signature.param_nullsafe_type.typ, inferred_nullability, []) + typestate in let get_initial_typestate () = let typestate_empty = TypeState.empty in diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index aa325ed54..fe792f0e6 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -45,20 +45,20 @@ let is_virtual = function (** Check an access (read or write) to a field. *) -let check_field_access tenv find_canonical_duplicate curr_pname node instr_ref exp fname ta loc : - unit = - if TypeAnnotation.is_nullable ta then - let origin_descr = TypeAnnotation.descr_origin ta in +let check_field_access tenv find_canonical_duplicate curr_pname node instr_ref exp fname + inferred_nullability loc : unit = + if InferredNullability.is_nullable inferred_nullability then + let origin_descr = InferredNullability.descr_origin inferred_nullability in report_error tenv find_canonical_duplicate (TypeErr.Null_field_access (explain_expr tenv node exp, fname, origin_descr, false)) (Some instr_ref) loc curr_pname (** Check an access to an array *) -let check_array_access tenv find_canonical_duplicate curr_pname node instr_ref array_exp fname ta - loc indexed = - if TypeAnnotation.is_nullable ta then - let origin_descr = TypeAnnotation.descr_origin ta in +let check_array_access tenv find_canonical_duplicate curr_pname node instr_ref array_exp fname + inferred_nullability loc indexed = + if InferredNullability.is_nullable inferred_nullability then + let origin_descr = InferredNullability.descr_origin inferred_nullability in report_error tenv find_canonical_duplicate (TypeErr.Null_field_access (explain_expr tenv node array_exp, fname, origin_descr, indexed)) (Some instr_ref) loc curr_pname @@ -76,8 +76,8 @@ type from_call = let equal_from_call = [%compare.equal: from_call] (** Check the normalized "is zero" or "is not zero" condition of a prune instruction. *) -let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e typ ta true_branch - from_call idenv linereader loc instr_ref : unit = +let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e typ + inferred_nullability true_branch from_call idenv linereader loc instr_ref : unit = let contains_instanceof_throwable pdesc node = (* Check if the current procedure has a catch Throwable. *) (* That always happens in the bytecode generated by try-with-resources. *) @@ -115,12 +115,12 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e ty in let is_temp = Idenv.exp_is_temp idenv e in let should_report = - (not (TypeAnnotation.is_nullable ta)) + (not (InferredNullability.is_nullable inferred_nullability)) && Config.eradicate_condition_redundant && true_branch && (not is_temp) && PatternMatch.type_is_class typ && (not (from_try_with_resources ())) && equal_from_call from_call From_condition - && not (TypeAnnotation.origin_is_fun_library ta) + && not (InferredNullability.origin_is_fun_library inferred_nullability) in let is_always_true = not case_zero in if should_report then @@ -142,14 +142,14 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r exp_lhs exp_rhs typ loc fname field_type_opt typecheck_expr : unit = let curr_pname = Procdesc.get_proc_name curr_pdesc in let curr_pattrs = Procdesc.get_attributes curr_pdesc in - let t_lhs, ta_lhs, _ = + let t_lhs, inferred_nullability_lhs, _ = typecheck_expr node instr_ref curr_pdesc typestate exp_lhs - (typ, TypeAnnotation.const_nullable false TypeOrigin.ONone, [loc]) + (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc]) loc in - let _, ta_rhs, _ = + let _, inferred_nullability_rhs, _ = typecheck_expr node instr_ref curr_pdesc typestate exp_rhs - (typ, TypeAnnotation.const_nullable false TypeOrigin.ONone, [loc]) + (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc]) loc in let field_is_injector_readwrite () = @@ -167,14 +167,15 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r in let should_report_nullable = (not (AndroidFramework.is_destroy_method curr_pname)) - && (not (TypeAnnotation.is_nullable ta_lhs)) - && TypeAnnotation.is_nullable ta_rhs && PatternMatch.type_is_class t_lhs + && (not (InferredNullability.is_nullable inferred_nullability_lhs)) + && InferredNullability.is_nullable inferred_nullability_rhs + && PatternMatch.type_is_class t_lhs && (not (Typ.Fieldname.Java.is_outer_instance fname)) && (not (field_is_injector_readwrite ())) && not (field_is_in_cleanup_context ()) in if should_report_nullable then - let origin_descr = TypeAnnotation.descr_origin ta_rhs in + let origin_descr = InferredNullability.descr_origin inferred_nullability_rhs in report_error tenv find_canonical_duplicate (TypeErr.Field_annotation_inconsistent (fname, origin_descr)) (Some instr_ref) loc curr_pdesc @@ -222,12 +223,13 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_pname cu | _ -> true in - final_type_annotation_with false (Lazy.force final_initializer_typestates) (fun ta -> - origin_is_initialized (TypeAnnotation.get_origin ta) ) + final_type_annotation_with false (Lazy.force final_initializer_typestates) + (fun nullability -> + origin_is_initialized (InferredNullability.get_origin nullability) ) in let may_be_nullable_in_final_typestate () = final_type_annotation_with true (Lazy.force final_constructor_typestates) (fun ta -> - TypeAnnotation.is_nullable ta ) + InferredNullability.is_nullable ta ) in let should_check_field_initialization = let in_current_class = @@ -281,9 +283,9 @@ let check_return_annotation tenv find_canonical_duplicate curr_pdesc ret_range | _ -> false -> () - | Some (_, final_ta, _) -> - let is_final_nullable = TypeAnnotation.is_nullable final_ta in - let origin_descr = TypeAnnotation.descr_origin final_ta in + | Some (_, final_inferred_nullability, _) -> + let is_final_nullable = InferredNullability.is_nullable final_inferred_nullability in + let origin_descr = InferredNullability.descr_origin final_inferred_nullability in let return_not_nullable = is_final_nullable && (not ret_annotated_nullable) && not ret_implicitly_nullable in @@ -306,15 +308,15 @@ let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate callee_pname (instr_ref : TypeErr.InstrRef.t) loc typecheck_expr : unit = match call_params with | ((original_this_e, this_e), typ) :: _ -> - let _, this_ta, _ = + let _, this_inferred_nullability, _ = typecheck_expr tenv node instr_ref curr_pdesc typestate this_e - (typ, TypeAnnotation.const_nullable false TypeOrigin.ONone, []) + (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, []) loc in - let null_method_call = TypeAnnotation.is_nullable this_ta in + let null_method_call = InferredNullability.is_nullable this_inferred_nullability in if null_method_call then let descr = explain_expr tenv node original_this_e in - let origin_descr = TypeAnnotation.descr_origin this_ta in + let origin_descr = InferredNullability.descr_origin this_inferred_nullability in report_error tenv find_canonical_duplicate (TypeErr.Call_receiver_annotation_inconsistent (descr, callee_pname, origin_descr)) (Some instr_ref) loc curr_pdesc @@ -324,16 +326,16 @@ let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate type resolved_param = { num: int - ; formal: Mangled.t * TypeAnnotation.t * Typ.t - ; actual: Exp.t * TypeAnnotation.t + ; formal: Mangled.t * InferredNullability.t * Typ.t + ; actual: Exp.t * InferredNullability.t ; is_formal_propagates_nullable: bool } (** Check the parameters of a call. *) let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_attributes resolved_params loc instr_ref : unit = let callee_pname = callee_attributes.ProcAttributes.proc_name in - let check {num= param_num; formal= s1, annotation_formal, t1; actual= orig_e2, annotation_actual} - = + let check + {num= param_num; formal= s1, nullability_formal, t1; actual= orig_e2, nullability_actual} = let report () = let description = match explain_expr tenv node orig_e2 with @@ -342,7 +344,7 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a | None -> "formal parameter " ^ Mangled.to_string s1 in - let origin_descr = TypeAnnotation.descr_origin annotation_actual in + let origin_descr = InferredNullability.descr_origin nullability_actual in let callee_loc = callee_attributes.ProcAttributes.loc in report_error tenv find_canonical_duplicate (TypeErr.Parameter_annotation_inconsistent @@ -350,8 +352,8 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a (Some instr_ref) loc curr_pdesc in if PatternMatch.type_is_class t1 then - let is_nullable_formal = TypeAnnotation.is_nullable annotation_formal in - let is_nullable_actual = TypeAnnotation.is_nullable annotation_actual in + let is_nullable_formal = InferredNullability.is_nullable nullability_formal in + let is_nullable_actual = InferredNullability.is_nullable nullability_actual in if (not is_nullable_formal) && is_nullable_actual then report () in let should_check_parameters = diff --git a/infer/src/nullsafe/typeAnnotation.mli b/infer/src/nullsafe/typeAnnotation.mli deleted file mode 100644 index a53f8e5ff..000000000 --- a/infer/src/nullsafe/typeAnnotation.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -(** Nodule to represent annotations on types. *) - -type t [@@deriving compare] - -val const_nullable : bool -> TypeOrigin.t -> t - -val descr_origin : t -> TypeErr.origin_descr -(** Human-readable description of the origin of a nullable value. *) - -val from_nullsafe_type : NullsafeType.t -> TypeOrigin.t -> t - -val get_origin : t -> TypeOrigin.t - -val is_nullable : t -> bool - -val join : t -> t -> t option - -val origin_is_fun_library : t -> bool - -val set_nullable : bool -> t -> t - -val to_string : t -> string - -val with_origin : t -> TypeOrigin.t -> t diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index a5b5075ce..5e669e2c9 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -113,10 +113,10 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r (curr_pdesc : Procdesc.t) typestate e tr_default loc : TypeState.range = match e with | _ when Exp.is_null_literal e -> - let typ, ta, locs = tr_default in + let typ, inferred_nullability, locs = tr_default in if PatternMatch.type_is_class typ then - (typ, TypeAnnotation.const_nullable true (TypeOrigin.Const loc), locs) - else (typ, TypeAnnotation.with_origin ta (TypeOrigin.Const loc), locs) + (typ, InferredNullability.create ~is_nullable:true (TypeOrigin.Const loc), locs) + else (typ, InferredNullability.with_origin inferred_nullability (TypeOrigin.Const loc), locs) | Exp.Lvar pvar -> ( match TypeState.lookup_pvar pvar typestate with | Some tr -> @@ -134,21 +134,21 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r typestate e1 tr_default loc | Exp.Const _ -> let typ, _, locs = tr_default in - (typ, TypeAnnotation.const_nullable false (TypeOrigin.Const loc), locs) + (typ, InferredNullability.create ~is_nullable:false (TypeOrigin.Const loc), locs) | Exp.Lfield (exp, fn, typ) -> let _, _, locs = tr_default in - let _, ta, locs' = + let _, inferred_nullability, locs' = typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc typestate exp - (typ, TypeAnnotation.const_nullable false TypeOrigin.ONone, locs) + (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, locs) loc in - let exp_origin = TypeAnnotation.get_origin ta in + let exp_origin = InferredNullability.get_origin inferred_nullability in let tr_new = match EradicateChecks.get_field_annotation tenv fn typ with | Some EradicateChecks.{nullsafe_type} -> ( nullsafe_type.typ - , TypeAnnotation.from_nullsafe_type nullsafe_type + , InferredNullability.from_nullsafe_type nullsafe_type (TypeOrigin.Field (exp_origin, fn, loc)) , locs' ) | None -> @@ -156,7 +156,7 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r in if checks.eradicate then EradicateChecks.check_field_access tenv find_canonical_duplicate curr_pdesc node instr_ref - exp fn ta loc ; + exp fn inferred_nullability loc ; tr_new | Exp.Lindex (array_exp, index_exp) -> let _, ta, _ = @@ -188,8 +188,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in let pvar_get_origin pvar = match TypeState.lookup_pvar pvar typestate with - | Some (_, ta, _) -> - Some (TypeAnnotation.get_origin ta) + | Some (_, inferred_nullability, _) -> + Some (InferredNullability.get_origin inferred_nullability) | None -> None in @@ -229,7 +229,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Some EradicateChecks.{nullsafe_type} -> let range = ( nullsafe_type.typ - , TypeAnnotation.from_nullsafe_type nullsafe_type + , InferredNullability.from_nullsafe_type nullsafe_type (TypeOrigin.Field (origin, fn, loc)) , [loc] ) in @@ -249,8 +249,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let pvar = Pvar.mk (Mangled.from_string exp_str) curr_pname in let already_defined_in_typestate = match TypeState.lookup_pvar pvar typestate with - | Some (_, ta, _) -> - not (TypeOrigin.equal TypeOrigin.Undef (TypeAnnotation.get_origin ta)) + | Some (_, inferred_nullability, _) -> + not + (TypeOrigin.equal TypeOrigin.Undef + (InferredNullability.get_origin inferred_nullability)) | None -> false in @@ -282,7 +284,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | _ -> None ) |> Option.value_map - ~f:(fun (_, ta, _) -> TypeAnnotation.get_origin ta) + ~f:(fun (_, nullability, _) -> InferredNullability.get_origin nullability) ~default:TypeOrigin.ONone in let exp' = Idenv.expand_expr_temps idenv node exp_ in @@ -406,7 +408,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let typecheck_expr_simple typestate1 exp1 typ1 origin1 loc1 = typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc typestate1 exp1 - (typ1, TypeAnnotation.const_nullable false origin1, [loc1]) + (typ1, InferredNullability.create ~is_nullable:false origin1, [loc1]) loc1 in (* check if there are errors in exp1 *) @@ -460,7 +462,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p when Typ.Procname.equal pn BuiltinDecl.__new || Typ.Procname.equal pn BuiltinDecl.__new_array -> TypeState.add_id id - (typ, TypeAnnotation.const_nullable false TypeOrigin.New, [loc]) + (typ, InferredNullability.create ~is_nullable:false TypeOrigin.New, [loc]) typestate (* new never returns null *) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _) @@ -474,7 +476,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let _, ta, _ = typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc typestate array_exp - (t, TypeAnnotation.const_nullable false TypeOrigin.ONone, [loc]) + (t, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc]) loc in if checks.eradicate then @@ -483,7 +485,9 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p (Typ.Fieldname.Java.from_string "length") ta loc false ; TypeState.add_id id - (Typ.mk (Tint Typ.IInt), TypeAnnotation.const_nullable false TypeOrigin.New, [loc]) + ( Typ.mk (Tint Typ.IInt) + , InferredNullability.create ~is_nullable:false TypeOrigin.New + , [loc] ) typestate | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn -> typestate (* skip othe builtins *) @@ -544,11 +548,11 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let clear_nullable_flag typestate'' pvar = (* remove the nullable flag for the given pvar *) match TypeState.lookup_pvar pvar typestate'' with - | Some (t, ta, _) -> + | Some (t, nullability, _) -> let should_report = Config.eradicate_condition_redundant - && (not (TypeAnnotation.is_nullable ta)) - && not (TypeAnnotation.origin_is_fun_library ta) + && (not (InferredNullability.is_nullable nullability)) + && not (InferredNullability.origin_is_fun_library nullability) in ( if checks.eradicate && should_report then let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in @@ -556,7 +560,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p (TypeErr.Condition_redundant (true, EradicateChecks.explain_expr tenv node cond)) (Some instr_ref) loc curr_pdesc ) ; TypeState.add pvar - (t, TypeAnnotation.const_nullable false TypeOrigin.ONone, [loc]) + (t, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc]) typestate'' | None -> typestate' @@ -588,12 +592,12 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in (* Handle Preconditions.checkState for &&-separated conditions x!=null. *) let do_preconditions_check_state typestate' = - let handle_pvar b typestate1 pvar = + let handle_pvar is_nullable typestate1 pvar = (* handle the annotation flag for pvar *) match TypeState.lookup_pvar pvar typestate1 with | Some (t, _, _) -> TypeState.add pvar - (t, TypeAnnotation.const_nullable b TypeOrigin.ONone, [loc]) + (t, InferredNullability.create ~is_nullable TypeOrigin.ONone, [loc]) typestate1 | None -> typestate1 @@ -683,22 +687,22 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p typestate' in let typestate_after_call, finally_resolved_ret = - let resolve_param i (sparam, cparam) = + let resolve_param i (formal_param, actual_param) = let AnnotatedSignature.{mangled; param_annotation_deprecated; param_nullsafe_type} = - sparam + formal_param in - let (orig_e2, e2), t2 = cparam in - let ta1 = - TypeAnnotation.from_nullsafe_type param_nullsafe_type (TypeOrigin.Formal mangled) + let (orig_e2, e2), t2 = actual_param in + let inferred_nullability_formal = + InferredNullability.from_nullsafe_type param_nullsafe_type (TypeOrigin.Formal mangled) in - let _, ta2, _ = + let _, inferred_nullability_actual, _ = typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc typestate e2 - (t2, TypeAnnotation.const_nullable false TypeOrigin.ONone, []) + (t2, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, []) loc in - let formal = (mangled, ta1, param_nullsafe_type.typ) in - let actual = (orig_e2, ta2) in + let formal = (mangled, inferred_nullability_formal, param_nullsafe_type.typ) in + let actual = (orig_e2, inferred_nullability_actual) in let num = i + 1 in let is_formal_propagates_nullable = Annotations.ia_is_propagates_nullable param_annotation_deprecated @@ -719,12 +723,12 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p else if List.for_all propagates_nullable_params ~f:(fun EradicateChecks.{actual= _, inferred_nullability_actual} -> - not (TypeAnnotation.is_nullable inferred_nullability_actual) ) + not (InferredNullability.is_nullable inferred_nullability_actual) ) then (* All params' inferred types are non-nullable. Strengten the result to be non-nullable as well! *) let ret_type_annotation, ret_typ = ret in - (TypeAnnotation.set_nullable false ret_type_annotation, ret_typ) + (InferredNullability.set_nullable false ret_type_annotation, ret_typ) else (* At least one param's inferred type is nullable, can not strengthen the result *) ret @@ -740,8 +744,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p ; annotated_signature= callee_annotated_signature ; is_library } in - let ret_ta = TypeAnnotation.from_nullsafe_type ret.ret_nullsafe_type origin in - (ret_ta, ret.ret_nullsafe_type.typ) + let ret_inferred_nullability = + InferredNullability.from_nullsafe_type ret.ret_nullsafe_type origin + in + (ret_inferred_nullability, ret.ret_nullsafe_type.typ) in let sig_len = List.length signature_params in let call_len = List.length call_params in @@ -860,14 +866,16 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | None -> (typestate, e, EradicateChecks.From_condition) in - let set_nullable_flag e' b typestate2 = - (* add constraint on e' for annotation ann *) + let set_nullable_flag e' should_set_nullable typestate2 = + (* add constraint on e' for annotation a given nullability *) let handle_pvar typestate' pvar = match TypeState.lookup_pvar pvar typestate' with - | Some (t, ta1, locs) -> - if TypeAnnotation.is_nullable ta1 <> b then - let ta2 = TypeAnnotation.set_nullable b ta1 in - TypeState.add pvar (t, ta2, locs) typestate' + | Some (t, current_nullability, locs) -> + if InferredNullability.is_nullable current_nullability <> should_set_nullable then + let new_nullability = + InferredNullability.set_nullable should_set_nullable current_nullability + in + TypeState.add pvar (t, new_nullability, locs) typestate' else typestate' | None -> typestate' @@ -891,16 +899,18 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p (typestate, e, EradicateChecks.From_condition) in let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in - let typ, ta, _ = + let typ, inferred_nullability, _ = typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc in if checks.eradicate then - EradicateChecks.check_zero tenv find_canonical_duplicate curr_pdesc node' e' typ ta - true_branch EradicateChecks.From_condition idenv linereader loc instr_ref ; + EradicateChecks.check_zero tenv find_canonical_duplicate curr_pdesc node' e' typ + inferred_nullability true_branch EradicateChecks.From_condition idenv linereader + loc instr_ref ; match from_call with | EradicateChecks.From_is_true_on_null -> (* if f returns true on null, then false branch implies != null *) - if TypeAnnotation.is_nullable ta then set_nullable_flag e' false typestate2 + if InferredNullability.is_nullable inferred_nullability then + set_nullable_flag e' false typestate2 else typestate2 | _ -> typestate2 ) @@ -922,12 +932,12 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p else (typestate, e, EradicateChecks.From_condition) ) in let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in - let typ, ta, _ = + let typ, inferred_nullability, _ = typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc in if checks.eradicate then - EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc node e' typ ta - true_branch from_call idenv linereader loc instr_ref ; + EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc node e' typ + inferred_nullability true_branch from_call idenv linereader loc instr_ref ; match from_call with | EradicateChecks.From_is_true_on_null -> typestate2 @@ -935,7 +945,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | EradicateChecks.From_containsKey | EradicateChecks.From_instanceof | EradicateChecks.From_is_false_on_null -> - if TypeAnnotation.is_nullable ta then set_nullable_flag e' false typestate2 + if InferredNullability.is_nullable inferred_nullability then + set_nullable_flag e' false typestate2 else typestate2 ) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, e1, e2), _) -> check_condition node' (Exp.BinOp (Binop.Ne, e1, e2)) diff --git a/infer/src/nullsafe/typeState.ml b/infer/src/nullsafe/typeState.ml index 02e4a6aa4..44c992be1 100644 --- a/infer/src/nullsafe/typeState.ml +++ b/infer/src/nullsafe/typeState.ml @@ -17,7 +17,7 @@ module M = Caml.Map.Make (struct let compare = Exp.compare end) -type range = Typ.t * TypeAnnotation.t * Location.t list [@@deriving compare] +type range = Typ.t * InferredNullability.t * Location.t list [@@deriving compare] type t = range M.t [@@deriving compare] @@ -30,8 +30,9 @@ let pp fmt typestate = let pp_locs fmt locs = F.fprintf fmt " [%a]" (Pp.seq pp_loc) locs in let pp_one exp (typ, ta, locs) = F.fprintf fmt " %a -> [%s] %s %a%a@\n" Exp.pp exp - (TypeOrigin.to_string (TypeAnnotation.get_origin ta)) - (TypeAnnotation.to_string ta) (Typ.pp_full Pp.text) typ pp_locs locs + (TypeOrigin.to_string (InferredNullability.get_origin ta)) + (InferredNullability.to_string ta) + (Typ.pp_full Pp.text) typ pp_locs locs in let pp_map map = M.iter pp_one map in pp_map typestate @@ -50,8 +51,11 @@ let range_add_locs (typ, ta, locs1) locs2 = let map_join m1 m2 = let range_join _exp range1_opt range2_opt = Option.both range1_opt range2_opt - |> Option.map ~f:(fun (((typ1, ta1, locs1) as range1), (typ2, ta2, locs2)) -> - TypeAnnotation.join ta1 ta2 + |> Option.map + ~f:(fun ( ((typ1, inferred_nullability1, locs1) as range1) + , (typ2, inferred_nullability2, locs2) ) + -> + InferredNullability.join inferred_nullability1 inferred_nullability2 |> Option.value_map ~default:range1 ~f:(fun ta' -> let typ' = type_join typ1 typ2 in let locs' = locs_join locs1 locs2 in diff --git a/infer/src/nullsafe/typeState.mli b/infer/src/nullsafe/typeState.mli index 0c983d9a9..9deaa5904 100644 --- a/infer/src/nullsafe/typeState.mli +++ b/infer/src/nullsafe/typeState.mli @@ -12,7 +12,7 @@ open! IStd (** Typestate *) type t -type range = Typ.t * TypeAnnotation.t * Location.t list +type range = Typ.t * InferredNullability.t * Location.t list val add_id : Ident.t -> range -> t -> t