diff --git a/infer/src/nullsafe/InferredNullability.ml b/infer/src/nullsafe/InferredNullability.ml index 2ba4a1367..e79ed4dc7 100644 --- a/infer/src/nullsafe/InferredNullability.ml +++ b/infer/src/nullsafe/InferredNullability.ml @@ -11,12 +11,14 @@ type t = {is_nullable: bool; origin: TypeOrigin.t} [@@deriving compare] let equal = [%compare.equal: t] -let is_nullable ta = ta.is_nullable +let is_nullable t = t.is_nullable -let set_nullable b ta = if Bool.equal (is_nullable ta) b then ta else {ta with is_nullable= b} +let is_nonnull t = not t.is_nullable -let descr_origin ta = - let descr_opt = TypeOrigin.get_description ta.origin in +let set_nonnull t = {t with is_nullable= false} + +let descr_origin t = + let descr_opt = TypeOrigin.get_description t.origin in match descr_opt with | None -> ("", None, None) @@ -24,7 +26,7 @@ let descr_origin ta = ("(Origin: " ^ str ^ ")", loc_opt, sig_opt) -let to_string ta = if is_nullable ta then " @Nullable" else "" +let to_string t = if is_nullable t then " @Nullable" else "" let join ta1 ta2 = let nul1, nul2 = (is_nullable ta1, is_nullable ta2) in @@ -38,19 +40,21 @@ let join ta1 ta2 = if equal ta' ta1 then None else Some ta' -let get_origin ta = ta.origin +let get_origin t = t.origin -let origin_is_fun_library ta = - match get_origin ta with +let origin_is_fun_library t = + match get_origin t with | TypeOrigin.Proc proc_origin -> proc_origin.TypeOrigin.is_library | _ -> false -let create ~is_nullable origin = {origin; is_nullable} +let create_nullable origin = {origin; is_nullable= true} + +let create_nonnull origin = {origin; is_nullable= false} -let with_origin ta o = {ta with origin= o} +let with_origin t o = {t with origin= o} let of_annotated_nullability annotated_nullability origin = match annotated_nullability with diff --git a/infer/src/nullsafe/InferredNullability.mli b/infer/src/nullsafe/InferredNullability.mli index 2146a3066..969be26f3 100644 --- a/infer/src/nullsafe/InferredNullability.mli +++ b/infer/src/nullsafe/InferredNullability.mli @@ -19,7 +19,15 @@ open! IStd type t [@@deriving compare] -val create : is_nullable:bool -> TypeOrigin.t -> t +val create_nullable : TypeOrigin.t -> t + +val create_nonnull : TypeOrigin.t -> t + +val is_nullable : t -> bool + +val is_nonnull : t -> bool + +val set_nonnull : t -> t val descr_origin : t -> TypeErr.origin_descr (** Human-readable description of the origin of a value. @@ -35,8 +43,6 @@ val of_annotated_nullability : AnnotatedNullability.t -> TypeOrigin.t -> t 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. @@ -52,8 +58,6 @@ 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/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 512b33c13..29c675a9d 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -97,7 +97,7 @@ 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 (InferredNullability.is_nullable inferred_nullability)) + InferredNullability.is_nonnull inferred_nullability && Config.eradicate_condition_redundant && true_branch && (not is_temp) && PatternMatch.type_is_class typ && (not (from_try_with_resources ())) @@ -126,12 +126,14 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r let curr_pattrs = Procdesc.get_attributes curr_pdesc in let t_lhs, inferred_nullability_lhs, _ = typecheck_expr node instr_ref curr_pdesc typestate exp_lhs - (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc]) + (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) + (typ, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) loc in let _, inferred_nullability_rhs, _ = typecheck_expr node instr_ref curr_pdesc typestate exp_rhs - (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc]) + (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) + (typ, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) loc in let field_is_injector_readwrite () = @@ -261,8 +263,8 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc let is_field_assigned_to_nonnull_in_all_constructors () = predicate_holds_for_all_typestates (Lazy.force typestates_for_all_constructors_incl_current) field_name - ~predicate:(fun (_, nullability, _) -> - not (InferredNullability.is_nullable nullability) ) + ~predicate:(fun (_, nullability, _) -> InferredNullability.is_nonnull nullability + ) in let should_check_field_initialization = let in_current_class = @@ -317,8 +319,7 @@ let check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_ (* TODO(T54308240) Consolidate return over annotated checks in NullsafeRules *) let check_return_overrannotated tenv find_canonical_duplicate loc curr_pname curr_pdesc (ret_signature : AnnotatedSignature.ret_signature) ret_inferred_nullability = - (* TODO(T54308240) this needs to be changed when we introduce Unknown nullability *) - let is_ret_inferred_nonnull = not (InferredNullability.is_nullable ret_inferred_nullability) in + let is_ret_inferred_nonnull = InferredNullability.is_nonnull ret_inferred_nullability in let is_ret_annotated_nullable = match ret_signature.ret_annotated_type.nullability with | AnnotatedNullability.Nonnull _ -> @@ -363,7 +364,8 @@ let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate | ((original_this_e, this_e), typ) :: _ -> let _, this_inferred_nullability, _ = typecheck_expr tenv node instr_ref curr_pdesc typestate this_e - (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, []) + (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) + (typ, InferredNullability.create_nonnull TypeOrigin.ONone, []) loc in let null_method_call = InferredNullability.is_nullable this_inferred_nullability in diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 0be3ca063..6960bc8c5 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -115,7 +115,7 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r | _ when Exp.is_null_literal e -> let typ, inferred_nullability, locs = tr_default in if PatternMatch.type_is_class typ then - (typ, InferredNullability.create ~is_nullable:true (TypeOrigin.Const loc), locs) + (typ, InferredNullability.create_nullable (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 @@ -134,13 +134,14 @@ 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, InferredNullability.create ~is_nullable:false (TypeOrigin.Const loc), locs) + (typ, InferredNullability.create_nonnull (TypeOrigin.Const loc), locs) | Exp.Lfield (exp, fn, typ) -> let _, _, locs = tr_default in let _, inferred_nullability, locs' = typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc typestate exp - (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, locs) + (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) + (typ, InferredNullability.create_nonnull TypeOrigin.ONone, locs) loc in let exp_origin = InferredNullability.get_origin inferred_nullability in @@ -408,7 +409,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, InferredNullability.create ~is_nullable:false origin1, [loc1]) + (typ1, InferredNullability.create_nonnull origin1, [loc1]) loc1 in (* check if there are errors in exp1 *) @@ -461,9 +462,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], loc, _) when Typ.Procname.equal pn BuiltinDecl.__new || Typ.Procname.equal pn BuiltinDecl.__new_array -> - TypeState.add_id id - (typ, InferredNullability.create ~is_nullable:false TypeOrigin.New, [loc]) - typestate + TypeState.add_id id (typ, InferredNullability.create_nonnull TypeOrigin.New, [loc]) typestate (* new never returns null *) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _) when Typ.Procname.equal pn BuiltinDecl.__cast -> @@ -476,7 +475,8 @@ 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, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc]) + (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) + (t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) loc in if checks.eradicate then @@ -485,9 +485,7 @@ 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) - , InferredNullability.create ~is_nullable:false TypeOrigin.New - , [loc] ) + (Typ.mk (Tint Typ.IInt), InferredNullability.create_nonnull TypeOrigin.New, [loc]) typestate | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn -> typestate (* skip othe builtins *) @@ -551,7 +549,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Some (t, nullability, _) -> let should_report = Config.eradicate_condition_redundant - && (not (InferredNullability.is_nullable nullability)) + && InferredNullability.is_nonnull nullability && not (InferredNullability.origin_is_fun_library nullability) in ( if checks.eradicate && should_report then @@ -560,7 +558,8 @@ 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, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc]) + (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) + (t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) typestate'' | None -> typestate' @@ -592,20 +591,21 @@ 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 is_nullable typestate1 pvar = + let set_nonnull_to_pvar typestate1 pvar = (* handle the annotation flag for pvar *) match TypeState.lookup_pvar pvar typestate1 with | Some (t, _, _) -> TypeState.add pvar - (t, InferredNullability.create ~is_nullable TypeOrigin.ONone, [loc]) + (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) + (t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) typestate1 | None -> typestate1 in let res_typestate = ref typestate' in - let set_nullable_flag pvar b = - (* set the annotation flag for pvar *) - res_typestate := pvar_apply loc (handle_pvar b) !res_typestate pvar + let set_nonnull pvar = + (* set nullability for pvar *) + res_typestate := pvar_apply loc set_nonnull_to_pvar !res_typestate pvar in let handle_negated_condition cond_node = let do_instr instr = @@ -613,7 +613,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let cond_e = Idenv.expand_expr_temps idenv cond_node expression in match convert_complex_exp_to_pvar cond_node false cond_e typestate' loc with | Exp.Lvar pvar', _ -> - set_nullable_flag pvar' false + set_nonnull pvar' | _ -> () in @@ -692,7 +692,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let _, inferred_nullability_actual, _ = typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc typestate e2 - (t2, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, []) + (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) + (t2, InferredNullability.create_nonnull TypeOrigin.ONone, []) loc in let actual = (orig_e2, inferred_nullability_actual) in @@ -717,12 +718,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 (InferredNullability.is_nullable inferred_nullability_actual) ) + InferredNullability.is_nonnull 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 - (InferredNullability.set_nullable false ret_type_annotation, ret_typ) + (InferredNullability.set_nonnull ret_type_annotation, ret_typ) else (* At least one param's inferred type is nullable, can not strengthen the result *) ret @@ -860,15 +861,12 @@ 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' should_set_nullable typestate2 = - (* add constraint on e' for annotation a given nullability *) + let set_nonnull e' typestate2 = let handle_pvar typestate' pvar = match TypeState.lookup_pvar pvar typestate' with | 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 + if not (InferredNullability.is_nonnull current_nullability) then + let new_nullability = InferredNullability.set_nonnull current_nullability in TypeState.add pvar (t, new_nullability, locs) typestate' else typestate' | None -> @@ -903,8 +901,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p match from_call with | EradicateChecks.From_is_true_on_null -> (* if f returns true on null, then false branch implies != null *) - if InferredNullability.is_nullable inferred_nullability then - set_nullable_flag e' false typestate2 + if not (InferredNullability.is_nonnull inferred_nullability) then + set_nonnull e' typestate2 else typestate2 | _ -> typestate2 ) @@ -939,8 +937,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 InferredNullability.is_nullable inferred_nullability then - set_nullable_flag e' false typestate2 + if not (InferredNullability.is_nonnull inferred_nullability) then + set_nonnull e' typestate2 else typestate2 ) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, e1, e2), _) -> check_condition node' (Exp.BinOp (Binop.Ne, e1, e2))