diff --git a/infer/src/nullsafe/ErrorRenderingUtils.ml b/infer/src/nullsafe/ErrorRenderingUtils.ml index 69f918e28..b973798c0 100644 --- a/infer/src/nullsafe/ErrorRenderingUtils.ml +++ b/infer/src/nullsafe/ErrorRenderingUtils.ml @@ -57,8 +57,7 @@ let is_object_nullability_self_explanatory ~object_expression (object_origin : T | ArrayLengthResult | ArrayAccess | InferredNonnull _ - | OptimisticFallback - | Undef -> + | OptimisticFallback -> false diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 49375b2d9..4f577f08c 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -257,9 +257,6 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc in let is_initialized_in_either_constructor_or_initializer = let is_initialized = function - | TypeOrigin.Undef -> - (* Special case: not really an initialization *) - false | TypeOrigin.Field {object_origin= TypeOrigin.This} -> (* Circular initialization - does not count *) false diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 3c0cd6aac..0e3cd5756 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -226,15 +226,7 @@ let funcall_exp_to_original_pvar_exp tenv curr_pname typestate exp ~is_assignmen exp | Some exp_str -> 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 (_, inferred_nullability) -> - not - (TypeOrigin.equal TypeOrigin.Undef - (InferredNullability.get_origin inferred_nullability)) - | None -> - false - in + let already_defined_in_typestate = Option.is_some (TypeState.lookup_pvar pvar typestate) in if is_assignment && already_defined_in_typestate then exp (* Don't overwrite pvar representing result of function call. *) else Exp.Lvar pvar ) @@ -439,7 +431,7 @@ let typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc tenv node instr_ref typestate1 exp1 loc1 : unit = ignore (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks tenv - node instr_ref typestate1 exp1 Typ.void TypeOrigin.Undef loc1) + node instr_ref typestate1 exp1 Typ.void TypeOrigin.OptimisticFallback loc1) (* Handle Preconditions.checkNotNull. *) @@ -596,7 +588,8 @@ let do_map_put call_params callee_pname tenv loc node curr_pname curr_pdesc call let pvar_map_get = Pvar.mk (Mangled.from_string map_get_str) curr_pname in TypeState.add pvar_map_get (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this - checks tenv node instr_ref typestate' exp_value typ_value TypeOrigin.Undef loc) + checks tenv node instr_ref typestate' exp_value typ_value + TypeOrigin.OptimisticFallback loc) typestate' | None -> typestate' ) @@ -1079,7 +1072,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in TypeState.add_id id (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks - tenv node instr_ref typestate' e' typ TypeOrigin.Undef loc) + tenv node instr_ref typestate' e' typ TypeOrigin.OptimisticFallback loc) typestate' | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Exn _} when is_return pvar -> (* skip assignment to return variable where it is an artifact of a throw instruction *) @@ -1107,7 +1100,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Exp.Lvar pvar -> TypeState.add pvar (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this - checks tenv node instr_ref typestate1 e2 typ TypeOrigin.Undef loc) + checks tenv node instr_ref typestate1 e2 typ TypeOrigin.OptimisticFallback loc) typestate1 | Exp.Lfield _ -> typestate1 diff --git a/infer/src/nullsafe/typeErr.ml b/infer/src/nullsafe/typeErr.ml index b5865d4de..ac548a988 100644 --- a/infer/src/nullsafe/typeErr.ml +++ b/infer/src/nullsafe/typeErr.ml @@ -225,8 +225,7 @@ let get_nonnull_explanation_for_condition_redudant (nonnull_origin : TypeOrigin. | New | ArrayAccess | InferredNonnull _ - | OptimisticFallback - | Undef -> + | OptimisticFallback -> " according to the existing annotations" diff --git a/infer/src/nullsafe/typeOrigin.ml b/infer/src/nullsafe/typeOrigin.ml index 7aab6f47c..5cb3d9c9e 100644 --- a/infer/src/nullsafe/typeOrigin.ml +++ b/infer/src/nullsafe/typeOrigin.ml @@ -10,28 +10,18 @@ open! IStd (** Describe the origin of values propagated by the checker. *) type t = - | NullConst of Location.t (** A null literal in the source *) - | NonnullConst of Location.t (** A constant (not equal to null) in the source. *) - | Field of field_origin (** A field access (result of expression `some_object.some_field`) *) - | MethodParameter of method_parameter_origin (** 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 *) + | NullConst of Location.t + | NonnullConst of Location.t + | Field of field_origin + | MethodParameter of method_parameter_origin + | This + | MethodCall of method_call_origin | 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 *) + | New + | ArrayLengthResult + | ArrayAccess | InferredNonnull of {previous_origin: t} - (** The value is inferred as non-null during flow-sensitive type inference (most commonly from - relevant condition branch or assertion explicitly comparing the value with `null`) *) - (* Below are two special values. *) | OptimisticFallback - (** Something went wrong during typechecking. We fall back to optimistic (not-nullable) type - to reduce potential non-actionable false positives. Ideally we should not see these - instances. They should be either processed gracefully (and a dedicated type constructor - should be added), or fixed. T54687014 tracks unsoundness issues caused by this type. *) - | Undef (** Undefined value before initialization *) [@@deriving compare] and method_parameter_origin = Normal of AnnotatedSignature.param_signature | ObjectEqualsOverride @@ -67,8 +57,7 @@ let get_nullability = function Hence we make potentially dangerous choice in favor of pragmatism. *) | ArrayAccess - | OptimisticFallback (* non-null is the most optimistic type *) - | Undef (* This is a very special case, assigning non-null is a technical trick *) -> + | OptimisticFallback (* non-null is the most optimistic type *) -> Nullability.StrictNonnull | Field {field_type= {nullability}} -> AnnotatedNullability.get_nullability nullability @@ -109,8 +98,6 @@ let rec to_string = function Format.sprintf "InferredNonnull(prev:%s)" (to_string previous_origin) | OptimisticFallback -> "OptimisticFallback" - | Undef -> - "Undef" let atline loc = " at line " ^ string_of_int loc.Location.line @@ -179,18 +166,16 @@ let get_description origin = | InferredNonnull _ | CallToGetKnownToContainsKey -> None - (* Two special cases - should not really occur in normal code *) - | OptimisticFallback | Undef -> + (* A technical origin *) + | OptimisticFallback -> None let join o1 o2 = match (o1, o2) with - (* left priority *) - | Undef, _ | _, Undef -> - Undef | Field _, (NullConst _ | NonnullConst _ | MethodParameter _ | This | MethodCall _ | New) -> (* low priority to Field, to support field initialization patterns *) o2 | _ -> + (* left priority *) o1 diff --git a/infer/src/nullsafe/typeOrigin.mli b/infer/src/nullsafe/typeOrigin.mli index ec72ed666..e8e48e9a4 100644 --- a/infer/src/nullsafe/typeOrigin.mli +++ b/infer/src/nullsafe/typeOrigin.mli @@ -23,13 +23,13 @@ type t = | InferredNonnull of {previous_origin: t} (** The value is inferred as non-null during flow-sensitive type inference (most commonly from relevant condition branch or assertion explicitly comparing the value with `null`) *) - (* Below are two special values. *) | OptimisticFallback - (** Something went wrong during typechecking. We fall back to optimistic (not-nullable) type - to reduce potential non-actionable false positives. Ideally we should not see these - instances. They should be either processed gracefully (and a dedicated type constructor - should be added), or fixed. T54687014 tracks unsoundness issues caused by this type. *) - | Undef (** Undefined value before initialization *) + (** A special case: technical type variant. Indicates either cases when something went wrong + during typechecking, and some cases that should be expressed in a better way than using + this type. We fall back to optimistic (not-nullable) type to reduce potential + non-actionable false positives. Ideally we should not see these instances. They should be + either processed gracefully (and a dedicated type constructor should be added), or fixed. + T54687014 tracks unsoundness issues caused by this type. *) [@@deriving compare] and method_parameter_origin = Normal of AnnotatedSignature.param_signature | ObjectEqualsOverride