diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index f0caad220..f535cd01d 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -39,9 +39,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct InferredNullability.of_annotated_nullability param_signature.param_annotated_type.nullability origin in - TypeState.add pvar - (param_signature.param_annotated_type.typ, inferred_nullability, []) - typestate + TypeState.add pvar (param_signature.param_annotated_type.typ, inferred_nullability) typestate in let get_initial_typestate () = let typestate_empty = TypeState.empty in @@ -54,7 +52,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct let ret_pvar = Procdesc.get_ret_var curr_pdesc in let ret_range = TypeState.lookup_pvar ret_pvar final_typestate in let typ_found_opt = - match ret_range with Some (typ_found, _, _) -> Some typ_found | None -> None + match ret_range with Some (typ_found, _) -> Some typ_found | None -> None in (* TODO(T54088319): model this in AnnotatedNullability *) let ret_implicitly_nullable = diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 60461a7df..b8e0e6536 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -119,16 +119,16 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r exp_lhs exp_rhs typ loc fname annotated_field_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, inferred_nullability_lhs, _ = + let t_lhs, inferred_nullability_lhs = typecheck_expr node instr_ref curr_pdesc typestate exp_lhs (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (typ, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) + (typ, InferredNullability.create_nonnull TypeOrigin.ONone) loc in - let _, inferred_nullability_rhs, _ = + let _, inferred_nullability_rhs = typecheck_expr node instr_ref curr_pdesc typestate exp_rhs (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (typ, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) + (typ, InferredNullability.create_nonnull TypeOrigin.ONone) loc in let field_is_injector_readwrite () = @@ -206,7 +206,7 @@ let get_nullability_upper_bound_for_typestate proc_name field_name typestate = *) Nullability.top (* We were able to lookup the field. Its nullability gives precise upper bound. *) - | Some (_, inferred_nullability, _) -> + | Some (_, inferred_nullability) -> InferredNullability.get_nullability inferred_nullability @@ -254,7 +254,7 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc in predicate_holds_for_some_typestate (Lazy.force typestates_for_curr_constructor_and_all_initializer_methods) field_name - ~predicate:(fun (_, nullability, _) -> + ~predicate:(fun (_, nullability) -> is_initialized (InferredNullability.get_origin nullability) ) in (* TODO(T54584721) This check is completely independent of the current constuctor we check. @@ -347,7 +347,7 @@ let check_return_annotation tenv find_canonical_duplicate curr_pdesc ret_range | _ -> false -> () - | Some (_, ret_inferred_nullability, _) -> + | Some (_, ret_inferred_nullability) -> (* TODO(T54308240) Model ret_implicitly_nullable in AnnotatedNullability *) if not ret_implicitly_nullable then check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_pdesc @@ -364,10 +364,10 @@ 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_inferred_nullability, _ = + let _, this_inferred_nullability = typecheck_expr tenv node instr_ref curr_pdesc typestate this_e (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (typ, InferredNullability.create_nonnull TypeOrigin.ONone, []) + (typ, InferredNullability.create_nonnull TypeOrigin.ONone) loc in check_object_dereference tenv find_canonical_duplicate curr_pdesc node instr_ref diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 5ecb2dc47..48ff44044 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -113,35 +113,27 @@ 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, inferred_nullability, locs = tr_default in + let typ, inferred_nullability = tr_default in if PatternMatch.type_is_class typ then - (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 - | Some tr -> - TypeState.range_add_locs tr [loc] - | None -> - tr_default ) - | Exp.Var id -> ( - match TypeState.lookup_id id typestate with - | Some tr -> - TypeState.range_add_locs tr [loc] - | None -> - tr_default ) + (typ, InferredNullability.create_nullable (TypeOrigin.Const loc)) + else (typ, InferredNullability.with_origin inferred_nullability (TypeOrigin.Const loc)) + | Exp.Lvar pvar -> + Option.value (TypeState.lookup_pvar pvar typestate) ~default:tr_default + | Exp.Var id -> + Option.value (TypeState.lookup_id id typestate) ~default:tr_default | Exp.Exn e1 -> typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc typestate e1 tr_default loc | Exp.Const _ -> - let typ, _, locs = tr_default in - (typ, InferredNullability.create_nonnull (TypeOrigin.Const loc), locs) + let typ, _ = tr_default in + (typ, InferredNullability.create_nonnull (TypeOrigin.Const loc)) | Exp.Lfield (exp, field_name, typ) -> - let _, _, locs = tr_default in - let _, inferred_nullability, locs' = + let _, _ = tr_default in + let _, inferred_nullability = typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc typestate exp (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (typ, InferredNullability.create_nonnull TypeOrigin.ONone, locs) + (typ, InferredNullability.create_nonnull TypeOrigin.ONone) loc in let exp_origin = InferredNullability.get_origin inferred_nullability in @@ -150,8 +142,7 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r | Some AnnotatedField.{annotated_type} -> ( annotated_type.typ , InferredNullability.of_annotated_nullability annotated_type.nullability - (TypeOrigin.Field (exp_origin, field_name, loc)) - , locs' ) + (TypeOrigin.Field (exp_origin, field_name, loc)) ) | None -> tr_default in @@ -160,7 +151,7 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r instr_ref exp (TypeErr.AccessToField field_name) inferred_nullability loc ; tr_new | Exp.Lindex (array_exp, index_exp) -> - let _, inferred_nullability, _ = + let _, inferred_nullability = typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc typestate array_exp tr_default loc in @@ -190,7 +181,7 @@ 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 (_, inferred_nullability, _) -> + | Some (_, inferred_nullability) -> Some (InferredNullability.get_origin inferred_nullability) | None -> None @@ -232,8 +223,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let range = ( annotated_type.typ , InferredNullability.of_annotated_nullability annotated_type.nullability - (TypeOrigin.Field (origin, fn, loc)) - , [loc] ) + (TypeOrigin.Field (origin, fn, loc)) ) in TypeState.add pvar range typestate | None -> @@ -251,7 +241,7 @@ 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 (_, inferred_nullability, _) -> + | Some (_, inferred_nullability) -> not (TypeOrigin.equal TypeOrigin.Undef (InferredNullability.get_origin inferred_nullability)) @@ -286,7 +276,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | _ -> None ) |> Option.value_map - ~f:(fun (_, nullability, _) -> InferredNullability.get_origin nullability) + ~f:(fun (_, nullability) -> InferredNullability.get_origin nullability) ~default:TypeOrigin.ONone in let exp' = Idenv.expand_expr_temps idenv node exp_ in @@ -410,7 +400,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_nonnull origin1, [loc1]) + (typ1, InferredNullability.create_nonnull origin1) loc1 in (* check if there are errors in exp1 *) @@ -460,10 +450,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p typestate1 in check_field_assign () ; typestate2 - | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], loc, _) + | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], _, _) when Typ.Procname.equal pn BuiltinDecl.__new || Typ.Procname.equal pn BuiltinDecl.__new_array -> - TypeState.add_id id (typ, InferredNullability.create_nonnull TypeOrigin.New, [loc]) typestate + TypeState.add_id id (typ, InferredNullability.create_nonnull TypeOrigin.New) typestate (* new never returns null *) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _) when Typ.Procname.equal pn BuiltinDecl.__cast -> @@ -473,18 +463,18 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p TypeState.add_id id (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc) typestate' | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _) when Typ.Procname.equal pn BuiltinDecl.__get_array_length -> - let _, ta, _ = + let _, ta = typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc typestate array_exp (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) + (t, InferredNullability.create_nonnull TypeOrigin.ONone) loc in if checks.eradicate then EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node instr_ref array_exp TypeErr.ArrayLengthAccess ta loc ; TypeState.add_id id - (Typ.mk (Tint Typ.IInt), InferredNullability.create_nonnull TypeOrigin.New, [loc]) + (Typ.mk (Tint Typ.IInt), InferredNullability.create_nonnull TypeOrigin.New) typestate | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn -> typestate (* skip othe builtins *) @@ -534,8 +524,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let is_anonymous_inner_class_constructor = Typ.Procname.Java.is_anonymous_inner_class_constructor callee_pname_java in - let do_return (ret_ta, ret_typ) loc' typestate' = - let mk_return_range () = (ret_typ, ret_ta, [loc']) in + let do_return (ret_ta, ret_typ) typestate' = + let mk_return_range () = (ret_typ, ret_ta) in let id = fst ret_id_typ in TypeState.add_id id (mk_return_range ()) typestate' in @@ -545,7 +535,7 @@ 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, nullability, _) -> + | Some (t, nullability) -> let should_report = Config.eradicate_condition_redundant && InferredNullability.is_nonnull nullability @@ -558,7 +548,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p (Some instr_ref) loc curr_pdesc ) ; TypeState.add pvar (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) + (t, InferredNullability.create_nonnull TypeOrigin.ONone) typestate'' | None -> typestate' @@ -593,10 +583,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let set_nonnull_to_pvar typestate1 pvar = (* handle the annotation flag for pvar *) match TypeState.lookup_pvar pvar typestate1 with - | Some (t, _, _) -> + | Some (t, _) -> TypeState.add pvar (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) + (t, InferredNullability.create_nonnull TypeOrigin.ONone) typestate1 | None -> typestate1 @@ -688,11 +678,11 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let typestate_after_call, finally_resolved_ret = let resolve_param i (formal_param, actual_param) = let (orig_e2, e2), t2 = actual_param in - let _, inferred_nullability_actual, _ = + let _, inferred_nullability_actual = typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc typestate e2 (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) - (t2, InferredNullability.create_nonnull TypeOrigin.ONone, []) + (t2, InferredNullability.create_nonnull TypeOrigin.ONone) loc in let actual = (orig_e2, inferred_nullability_actual) in @@ -795,7 +785,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in (typestate_after_call, ret_respecting_propagates_nullable) in - do_return finally_resolved_ret loc typestate_after_call + do_return finally_resolved_ret typestate_after_call | Sil.Call _ -> typestate | Sil.Prune (cond, loc, true_branch, _) -> @@ -851,10 +841,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Some e_str -> let pvar = Pvar.mk (Mangled.from_string e_str) curr_pname in let e1 = Exp.Lvar pvar in - let typ, ta, _ = + let typ, ta = typecheck_expr_simple typestate e1 (Typ.mk Tvoid) TypeOrigin.ONone loc in - let range = (typ, ta, [loc]) in + let range = (typ, ta) in let typestate1 = TypeState.add pvar range typestate in (typestate1, e1, EradicateChecks.From_containsKey) | None -> @@ -863,10 +853,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let set_nonnull e' typestate2 = let handle_pvar typestate' pvar = match TypeState.lookup_pvar pvar typestate' with - | Some (t, current_nullability, locs) -> + | Some (t, current_nullability) -> 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' + TypeState.add pvar (t, new_nullability) typestate' else typestate' | None -> typestate' @@ -890,7 +880,7 @@ 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, inferred_nullability, _ = + let typ, inferred_nullability = typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc in if checks.eradicate then @@ -923,7 +913,7 @@ 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, inferred_nullability, _ = + let typ, inferred_nullability = typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc in if checks.eradicate then diff --git a/infer/src/nullsafe/typeState.ml b/infer/src/nullsafe/typeState.ml index 44c992be1..7647e2db5 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 * InferredNullability.t * Location.t list [@@deriving compare] +type range = Typ.t * InferredNullability.t [@@deriving compare] type t = range M.t [@@deriving compare] @@ -26,13 +26,11 @@ let equal = [%compare.equal: t] let empty = M.empty let pp fmt typestate = - let pp_loc fmt loc = F.pp_print_int fmt loc.Location.line in - 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 + let pp_one exp (typ, ta) = + F.fprintf fmt " %a -> [%s] %s %a@\n" Exp.pp exp (TypeOrigin.to_string (InferredNullability.get_origin ta)) (InferredNullability.to_string ta) - (Typ.pp_full Pp.text) typ pp_locs locs + (Typ.pp_full Pp.text) typ in let pp_map map = M.iter pp_one map in pp_map typestate @@ -40,26 +38,15 @@ let pp fmt typestate = let type_join typ1 typ2 = if PatternMatch.type_is_object typ1 then typ2 else typ1 -let locs_join locs1 locs2 = IList.merge_sorted_nodup ~cmp:Location.compare ~res:[] locs1 locs2 - -(** Add a list of locations to a range. *) -let range_add_locs (typ, ta, locs1) locs2 = - let locs' = locs_join locs1 locs2 in - (typ, ta, locs') - - let map_join m1 m2 = let range_join _exp range1_opt range2_opt = Option.both range1_opt range2_opt |> Option.map - ~f:(fun ( ((typ1, inferred_nullability1, locs1) as range1) - , (typ2, inferred_nullability2, locs2) ) - -> + ~f:(fun (((typ1, inferred_nullability1) as range1), (typ2, inferred_nullability2)) -> 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 - (typ', ta', locs') ) ) + (typ', ta') ) ) in if phys_equal m1 m2 then m1 else M.merge range_join m1 m2 diff --git a/infer/src/nullsafe/typeState.mli b/infer/src/nullsafe/typeState.mli index 9deaa5904..9f693442d 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 * InferredNullability.t * Location.t list +type range = Typ.t * InferredNullability.t val add_id : Ident.t -> range -> t -> t @@ -30,6 +30,4 @@ val lookup_pvar : Pvar.t -> t -> range option val pp : Format.formatter -> t -> unit -val range_add_locs : range -> Location.t list -> range - val remove_id : Ident.t -> t -> t