[nullsafe] Split NullsafeType into AnnotatedNullability and AnnotatedType

Summary:
As suggested by artempyanykh:
1. Since we recently introduced InferredNullability, AnnotatedNullability deserves its own class which now plays nicely with its counterpart.
2. AnnotatedType is more specific then NullsafeType

Reviewed By: artempyanykh

Differential Revision: D17547988

fbshipit-source-id: 785def23a
master
Mitya Lyubarskiy 5 years ago committed by Facebook Github Bot
parent 71aa4816d6
commit 0a353da6d9

@ -17,7 +17,7 @@ module F = Format
*)
(* TODO(T52947663) add notion of unknown nullability *)
type nullability = Nullable of nullable_origin | Nonnull of nonnull_origin [@@deriving compare]
type t = Nullable of nullable_origin | Nonnull of nonnull_origin [@@deriving compare]
and nullable_origin =
| AnnotatedNullable (** The type is expicitly annotated with @Nullable in the code *)
@ -36,9 +36,7 @@ and nonnull_origin =
| ModelledNonnull (** nullsafe knows it is non-nullable via its internal models *)
[@@deriving compare]
type t = {nullability: nullability; typ: Typ.t} [@@deriving compare]
let pp fmt {nullability; typ} =
let pp fmt t =
let string_of_nullable_origin nullable_origin =
match nullable_origin with
| AnnotatedNullable ->
@ -59,17 +57,14 @@ let pp fmt {nullability; typ} =
| ModelledNonnull ->
"model"
in
let pp_nullability fmt nullability =
match nullability with
| Nullable nullable_origin ->
F.fprintf fmt "Nullable[%s]" (string_of_nullable_origin nullable_origin)
| Nonnull nonnull_origin ->
F.fprintf fmt "Nonnull[%s]" (string_of_nonnull_origin nonnull_origin)
in
F.fprintf fmt "%a %a" pp_nullability nullability (Typ.pp_full Pp.text) typ
match t with
| Nullable nullable_origin ->
F.fprintf fmt "Nullable[%s]" (string_of_nullable_origin nullable_origin)
| Nonnull nonnull_origin ->
F.fprintf fmt "Nonnull[%s]" (string_of_nonnull_origin nonnull_origin)
let nullability_of_annot_item ia =
let of_annot_item ia =
if Annotations.ia_is_nullable ia then
let nullable_origin =
if Annotations.ia_is_propagates_nullable ia then AnnotatedPropagatesNullable

@ -7,12 +7,19 @@
open! IStd
(** Representation of a type in Java program, but with added information about its nullability.
Nullability information might come either from explicit annotations, or from other sources,
including conventions about defaults.
(** Nullability of a type in Java program (e.g. in a function or field declaration).
It might come from explicit annotations (or lack of annotation), or from other sources,
including conventions about defaults, models, or the mode nullsafe runs in.
NOTE: This is complementary to {!InferredNullability.t}.
{!InferredNullability} contains info about _actual_ nullability
(what did nullsafe infer according to its flow-sensitive rules.).
In contrast, AnnotatedNullability represents _formal_ type as it appears
in the program code.
NOTE: Nullsafe disregards user-provided annotations for local types, so
annotated nullability applies only for types declared at methods and field level.
*)
type nullability = Nullable of nullable_origin | Nonnull of nonnull_origin [@@deriving compare]
type t = Nullable of nullable_origin | Nonnull of nonnull_origin [@@deriving compare]
and nullable_origin =
| AnnotatedNullable (** The type is expicitly annotated with @Nullable in the code *)
@ -31,12 +38,10 @@ and nonnull_origin =
| ModelledNonnull (** nullsafe knows it is non-nullable via its internal models *)
[@@deriving compare]
type t = {nullability: nullability; typ: Typ.t} [@@deriving compare]
val pp : Format.formatter -> t -> unit
val nullability_of_annot_item : Annot.Item.t -> nullability
val of_annot_item : Annot.Item.t -> t
(** Converts the information from the annotation to nullability.
NOTE: it does not take into account models etc., so this is intended to be used
as a helper function for more high-level annotation processing.
*)
val pp : Format.formatter -> t -> unit

@ -9,7 +9,7 @@ module F = Format
module L = Logging
(* TODO(T54088319) remove Annot.Item.t from t:
1. For everything dealing with nullability, use info from NullsafeType instead.
1. For everything dealing with nullability, use info from AnnotatedNullability instead.
2. For other annotations guiding Nullsafe behavior, introduce corresponding datatypes:
a. Known ret value annotations (if any)
b. Known param annotations
@ -18,25 +18,25 @@ module L = Logging
type t = {ret: ret_signature; params: param_signature list} [@@deriving compare]
and ret_signature = {ret_annotation_deprecated: Annot.Item.t; ret_nullsafe_type: NullsafeType.t}
and ret_signature = {ret_annotation_deprecated: Annot.Item.t; ret_annotated_type: AnnotatedType.t}
[@@deriving compare]
and param_signature =
{ param_annotation_deprecated: Annot.Item.t
; mangled: Mangled.t
; param_nullsafe_type: NullsafeType.t }
; param_annotated_type: AnnotatedType.t }
[@@deriving compare]
(* get nullability of method's return type given its annotations and information about its params *)
let nullability_for_return ia ~has_propagates_nullable_in_param =
let nullability = NullsafeType.nullability_of_annot_item ia in
let nullability = AnnotatedNullability.of_annot_item ia in
(* if any param is annotated with propagates nullable, then the result is nullable *)
match nullability with
| NullsafeType.Nullable _ ->
| AnnotatedNullability.Nullable _ ->
nullability (* We already know it is nullable - lets not overwrite the origin *)
| _ when has_propagates_nullable_in_param ->
(* if any params is propagates nullable, the return type can be only nullable *)
NullsafeType.Nullable NullsafeType.HasPropagatesNullableInParam
AnnotatedNullability.Nullable AnnotatedNullability.HasPropagatesNullableInParam
| _ ->
nullability
@ -44,10 +44,10 @@ let nullability_for_return ia ~has_propagates_nullable_in_param =
(* Given annotations for method signature, extract nullability information
for return type and params *)
let extract_nullability return_annotation param_annotations =
let params_nullability = List.map param_annotations ~f:NullsafeType.nullability_of_annot_item in
let params_nullability = List.map param_annotations ~f:AnnotatedNullability.of_annot_item in
let has_propagates_nullable_in_param =
List.exists params_nullability ~f:(function
| NullsafeType.Nullable NullsafeType.AnnotatedPropagatesNullable ->
| AnnotatedNullability.Nullable AnnotatedNullability.AnnotatedPropagatesNullable ->
true
| _ ->
false )
@ -89,13 +89,14 @@ let get proc_attributes : t =
in
let ret =
{ ret_annotation_deprecated= return_annotation
; ret_nullsafe_type= NullsafeType.{nullability= return_nullability; typ= ret_type} }
; ret_annotated_type= AnnotatedType.{nullability= return_nullability; typ= ret_type} }
in
let params =
List.map2_exn params_with_annotations params_nullability
~f:(fun ((mangled, typ), param_annotation_deprecated) nullability ->
{param_annotation_deprecated; mangled; param_nullsafe_type= NullsafeType.{nullability; typ}}
)
{ param_annotation_deprecated
; mangled
; param_annotated_type= AnnotatedType.{nullability; typ} } )
in
{ret; params}
@ -109,12 +110,12 @@ let param_has_annot predicate pvar ann_sig =
let pp proc_name fmt annotated_signature =
let pp_ia fmt ia = if ia <> [] then F.fprintf fmt "%a " Annot.Item.pp ia in
let pp_annotated_param fmt {mangled; param_annotation_deprecated; param_nullsafe_type} =
F.fprintf fmt " %a%a %a" pp_ia param_annotation_deprecated NullsafeType.pp param_nullsafe_type
Mangled.pp mangled
let pp_annotated_param fmt {mangled; param_annotation_deprecated; param_annotated_type} =
F.fprintf fmt " %a%a %a" pp_ia param_annotation_deprecated AnnotatedType.pp
param_annotated_type Mangled.pp mangled
in
let {ret_annotation_deprecated; ret_nullsafe_type} = annotated_signature.ret in
F.fprintf fmt "%a%a %a (%a )" pp_ia ret_annotation_deprecated NullsafeType.pp ret_nullsafe_type
let {ret_annotation_deprecated; ret_annotated_type} = annotated_signature.ret in
F.fprintf fmt "%a%a %a (%a )" pp_ia ret_annotation_deprecated AnnotatedType.pp ret_annotated_type
(Typ.Procname.pp_simplified_string ~withclass:false)
proc_name (Pp.comma_seq pp_annotated_param) annotated_signature.params
@ -129,12 +130,12 @@ let mark_ia_nullability ia x = if x then mk_ia_nullable ia else ia
(* Override existing information about nullability for a given type and
set it to either nullable or nonnull *)
let set_modelled_nullability_for_nullsafe_type nullsafe_type should_set_nullable =
let set_modelled_nullability_for_annotated_type annotated_type should_set_nullable =
let nullability =
if should_set_nullable then NullsafeType.Nullable ModelledNullable
else NullsafeType.Nonnull ModelledNonnull
if should_set_nullable then AnnotatedNullability.Nullable ModelledNullable
else AnnotatedNullability.Nonnull ModelledNonnull
in
NullsafeType.{nullsafe_type with nullability}
AnnotatedType.{annotated_type with nullability}
let set_modelled_nullability proc_name asig (nullability_for_ret, params_nullability) =
@ -142,14 +143,15 @@ let set_modelled_nullability proc_name asig (nullability_for_ret, params_nullabi
{ param with
param_annotation_deprecated=
mark_ia_nullability param.param_annotation_deprecated should_set_nullable
; param_nullsafe_type=
set_modelled_nullability_for_nullsafe_type param.param_nullsafe_type should_set_nullable }
; param_annotated_type=
set_modelled_nullability_for_annotated_type param.param_annotated_type should_set_nullable
}
in
let set_modelled_nullability_for_ret ret should_set_nullable =
{ ret_annotation_deprecated=
mark_ia_nullability ret.ret_annotation_deprecated should_set_nullable
; ret_nullsafe_type=
set_modelled_nullability_for_nullsafe_type ret.ret_nullsafe_type should_set_nullable }
; ret_annotated_type=
set_modelled_nullability_for_annotated_type ret.ret_annotated_type should_set_nullable }
in
let final_params =
let fail () =

@ -11,13 +11,13 @@ open! IStd
type t = {ret: ret_signature; params: param_signature list} [@@deriving compare]
and ret_signature = {ret_annotation_deprecated: Annot.Item.t; ret_nullsafe_type: NullsafeType.t}
and ret_signature = {ret_annotation_deprecated: Annot.Item.t; ret_annotated_type: AnnotatedType.t}
[@@deriving compare]
and param_signature =
{ param_annotation_deprecated: Annot.Item.t
; mangled: Mangled.t
; param_nullsafe_type: NullsafeType.t }
; param_annotated_type: AnnotatedType.t }
[@@deriving compare]
val param_has_annot : (Annot.Item.t -> bool) -> Pvar.t -> t -> bool

@ -0,0 +1,12 @@
(*
* 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
type t = {nullability: AnnotatedNullability.t; typ: Typ.t} [@@deriving compare]
let pp fmt {nullability; typ} =
Format.fprintf fmt "%a %a" AnnotatedNullability.pp nullability (Typ.pp_full Pp.text) typ

@ -0,0 +1,14 @@
(*
* 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
(** Formal type in program together with its nullability information. *)
type t = {nullability: AnnotatedNullability.t; typ: Typ.t} [@@deriving compare]
val pp : Format.formatter -> t -> unit

@ -52,9 +52,9 @@ let create ~is_nullable origin = {origin; is_nullable}
let with_origin ta o = {ta with origin= o}
let from_nullsafe_type NullsafeType.{nullability} origin =
match nullability with
| Nullable _ ->
let of_annotated_nullability annotated_nullability origin =
match annotated_nullability with
| AnnotatedNullability.Nullable _ ->
{origin; is_nullable= true}
| Nonnull _ ->
| AnnotatedNullability.Nonnull _ ->
{origin; is_nullable= false}

@ -9,8 +9,8 @@ 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
NOTE: This is complementaty to {!InferredNullability.t}.
{!InferredNullability} 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
@ -26,10 +26,10 @@ val descr_origin : t -> TypeErr.origin_descr
(How did nullsafe infer the nullability )
*)
val from_nullsafe_type : NullsafeType.t -> TypeOrigin.t -> t
val of_annotated_nullability : AnnotatedNullability.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.
(e.g. to infer nullability of {[o]} in {[Object o = someFunction();]}
based on {[someFunction()]} formal return type.
*)
val get_origin : t -> TypeOrigin.t

@ -7,11 +7,11 @@
open! IStd
let is_nonnull nullsafe_nullability =
match nullsafe_nullability with
| NullsafeType.Nullable _ ->
let is_nonnull annotated_nullability =
match annotated_nullability with
| AnnotatedNullability.Nullable _ ->
false
| NullsafeType.Nonnull _ ->
| AnnotatedNullability.Nonnull _ ->
true

@ -18,7 +18,7 @@ open! IStd
this module instead of doing things on their own.
*)
val passes_assignment_rule : lhs:NullsafeType.nullability -> rhs:InferredNullability.t -> bool
val passes_assignment_rule : lhs:AnnotatedNullability.t -> rhs:InferredNullability.t -> bool
(** Assignment rule: No expression of nullable type is ever assigned to a location
of non-nullable type.
*)

@ -36,10 +36,11 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
let pvar = Pvar.mk param_signature.mangled curr_pname in
let inferred_nullability =
let origin = TypeOrigin.Formal param_signature.mangled in
InferredNullability.from_nullsafe_type param_signature.param_nullsafe_type origin
InferredNullability.of_annotated_nullability
param_signature.param_annotated_type.nullability origin
in
TypeState.add pvar
(param_signature.param_nullsafe_type.typ, inferred_nullability, [])
(param_signature.param_annotated_type.typ, inferred_nullability, [])
typestate
in
let get_initial_typestate () =
@ -49,20 +50,20 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
(* Check the nullable flag computed for the return value and report inconsistencies. *)
let check_return find_canonical_duplicate exit_node final_typestate annotated_signature loc :
unit =
let AnnotatedSignature.{ret_nullsafe_type} = annotated_signature.AnnotatedSignature.ret in
let AnnotatedSignature.{ret_annotated_type} = annotated_signature.AnnotatedSignature.ret in
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
in
(* TODO(T54088319): model this in NullsafeType.nullability *)
(* TODO(T54088319): model this in AnnotatedNullability *)
let ret_implicitly_nullable =
String.equal (PatternMatch.get_type_name ret_nullsafe_type.typ) "java.lang.Void"
String.equal (PatternMatch.get_type_name ret_annotated_type.typ) "java.lang.Void"
in
State.set_node exit_node ;
if checks.TypeCheck.check_ret_type <> [] then
List.iter
~f:(fun f -> f curr_pname curr_pdesc ret_nullsafe_type.typ typ_found_opt loc)
~f:(fun f -> f curr_pname curr_pdesc ret_annotated_type.typ typ_found_opt loc)
checks.TypeCheck.check_ret_type ;
if checks.TypeCheck.eradicate then
EradicateChecks.check_return_annotation tenv find_canonical_duplicate curr_pdesc ret_range

@ -10,17 +10,17 @@ open! IStd
(** Module for the checks called by Eradicate. *)
(* TODO(T54088319) get rid of annotation_deprecated:
- move all usages related to nullability to nullsafe_type
- move all usages related to nullability to AnnotatedNullability.
- introduce "field flags" and move all other usages to this dedicated datatype
*)
type field_type = {annotation_deprecated: Annot.Item.t; nullsafe_type: NullsafeType.t}
type field_type = {annotation_deprecated: Annot.Item.t; annotated_type: AnnotatedType.t}
let get_field_annotation tenv fn typ =
let lookup = Tenv.lookup tenv in
let type_and_annotation_to_field_type (typ, annotation) =
{ annotation_deprecated= annotation
; nullsafe_type=
NullsafeType.{nullability= NullsafeType.nullability_of_annot_item annotation; typ} }
; annotated_type=
AnnotatedType.{nullability= AnnotatedNullability.of_annot_item annotation; typ} }
in
Option.map
(Typ.Struct.get_field_type_and_annotation ~lookup fn typ)
@ -266,7 +266,7 @@ let check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_
(ret_signature : AnnotatedSignature.ret_signature) ret_inferred_nullability =
if
not
(NullsafeRules.passes_assignment_rule ~lhs:ret_signature.ret_nullsafe_type.nullability
(NullsafeRules.passes_assignment_rule ~lhs:ret_signature.ret_annotated_type.nullability
~rhs:ret_inferred_nullability)
then
report_error tenv find_canonical_duplicate
@ -281,10 +281,10 @@ let check_return_overrannotated tenv find_canonical_duplicate loc curr_pname cur
(* 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_annotated_nullable =
match ret_signature.ret_nullsafe_type.nullability with
| NullsafeType.Nonnull _ ->
match ret_signature.ret_annotated_type.nullability with
| AnnotatedNullability.Nonnull _ ->
false
| NullsafeType.Nullable _ ->
| AnnotatedNullability.Nullable _ ->
true
in
if is_ret_inferred_nonnull && is_ret_annotated_nullable then
@ -306,7 +306,7 @@ let check_return_annotation tenv find_canonical_duplicate curr_pdesc ret_range
false ->
()
| Some (_, ret_inferred_nullability, _) ->
(* TODO(T54308240) Model ret_implicitly_nullable in NullsafeType.t *)
(* 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
annotated_signature.ret ret_inferred_nullability ;
@ -364,10 +364,10 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
(description, param_num, callee_pname, callee_loc, origin_descr))
(Some instr_ref) loc curr_pdesc
in
if PatternMatch.type_is_class formal.param_nullsafe_type.typ then
if PatternMatch.type_is_class formal.param_annotated_type.typ then
if
not
(NullsafeRules.passes_assignment_rule ~lhs:formal.param_nullsafe_type.nullability
(NullsafeRules.passes_assignment_rule ~lhs:formal.param_annotated_type.nullability
~rhs:nullability_actual)
then report ()
in

@ -146,9 +146,9 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r
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
, InferredNullability.from_nullsafe_type nullsafe_type
| Some EradicateChecks.{annotated_type} ->
( annotated_type.typ
, InferredNullability.of_annotated_nullability annotated_type.nullability
(TypeOrigin.Field (exp_origin, fn, loc))
, locs' )
| None ->
@ -226,10 +226,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
typestate
| _ -> (
match EradicateChecks.get_field_annotation tenv fn typ with
| Some EradicateChecks.{nullsafe_type} ->
| Some EradicateChecks.{annotated_type} ->
let range =
( nullsafe_type.typ
, InferredNullability.from_nullsafe_type nullsafe_type
( annotated_type.typ
, InferredNullability.of_annotated_nullability annotated_type.nullability
(TypeOrigin.Field (origin, fn, loc))
, [loc] )
in
@ -739,9 +739,9 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
; is_library }
in
let ret_inferred_nullability =
InferredNullability.from_nullsafe_type ret.ret_nullsafe_type origin
InferredNullability.of_annotated_nullability ret.ret_annotated_type.nullability origin
in
(ret_inferred_nullability, ret.ret_nullsafe_type.typ)
(ret_inferred_nullability, ret.ret_annotated_type.typ)
in
let sig_len = List.length signature_params in
let call_len = List.length call_params in

@ -178,9 +178,10 @@ module Severity = struct
let this_type_get_severity tenv (signature : AnnotatedSignature.t) =
match signature.params with
| AnnotatedSignature.{mangled; param_nullsafe_type} :: _ when Mangled.is_this mangled ->
| AnnotatedSignature.{mangled; param_annotated_type} :: _ when Mangled.is_this mangled ->
(* TODO(T54088319) get rid of direct access to annotation *)
Option.bind ~f:get_severity (PatternMatch.type_get_annotation tenv param_nullsafe_type.typ)
Option.bind ~f:get_severity
(PatternMatch.type_get_annotation tenv param_annotated_type.typ)
| _ ->
None

@ -56,7 +56,7 @@ let get_description origin =
Some ("method parameter " ^ Mangled.to_string s, None, None)
| Proc po ->
let modelled_in =
(* TODO(T54088319) don't calculate this info and propagate it from NullsafeType instead *)
(* TODO(T54088319) don't calculate this info and propagate it from AnnotatedNullability instead *)
if Models.is_modelled_for_nullability po.pname then " modelled in " ^ ModelTables.this_file
else ""
in

Loading…
Cancel
Save