From cf6c78a64a180e48eb12ef50a58c1e45e94bbf6d Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Mon, 21 Oct 2019 04:40:10 -0700 Subject: [PATCH] [nullsafe] Remove calculating locations in typestate `range` Summary: It is unclear what is the purpose of doing so, and it adds complexity to codebase. 1/ The semantics of this is not clear, it more or less corresponds to "where are all original locations that contributed to the type calculation", but many branches in CFG have nothing to do with nullability; also it was used not always consistently. 2/ The only place where this was used is logs, so this is no-ops. It is unclear how seeing all locations can help debugging, given 3/ - see below 3/ We have the right place to store such informatin, namely TypeOrigin, where we store locations associated with types where we merge them in CFG. Currently, we store only "winner" - the most relevant locations that contributed to nullability in the most informative way. We show this to the user when we report an error. 4/ If we want to support more things (e.g. show something more to the user), TypeOrigin seems to be the right place. Or, alternatively, we might still merge locations in `range`, but this will be better to organize in a tree form instead of flat list that is not really informative and helpful. It is all speculative though since need to support things like that seems unclear. Reviewed By: artempyanykh Differential Revision: D17857198 fbshipit-source-id: 6cf6e48a2 --- infer/src/nullsafe/eradicate.ml | 6 +- infer/src/nullsafe/eradicateChecks.ml | 18 +++--- infer/src/nullsafe/typeCheck.ml | 88 ++++++++++++--------------- infer/src/nullsafe/typeState.ml | 25 ++------ infer/src/nullsafe/typeState.mli | 4 +- 5 files changed, 57 insertions(+), 84 deletions(-) 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