pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[nullsafe] Rename TypeAnnotation to InferredNullability

Browse Source 
Summary:
Now, after series of modifications with TypeAnnotation, we are ready to
rename it to reflect what it means in the code.

See the documentation in the class for details.

Also:
- renamed methods for clarity
- added some documentation
- renamed local variables around the usages

Reviewed By: jvillard

Differential Revision: D17480799

fbshipit-source-id: d4408887a
master
Mitya Lyubarskiy 5 years ago committed by Facebook Github Bot
parent 361e11b3be
commit 74c8629d13
8 changed files with 177 additions and 133 deletions
Show Stats Download Patch File Download Diff File

4
infer/src/nullsafe/typeAnnotation.ml → infer/src/nullsafe/InferredNullability.ml
Unescape View File

@ -7,8 +7,6 @@
open! IStd open! IStd
(** Module to represent annotations on types. *)
type t = {is_nullable: bool; origin: TypeOrigin.t} [@@deriving compare] type t = {is_nullable: bool; origin: TypeOrigin.t} [@@deriving compare]
let equal = [%compare.equal: t] let equal = [%compare.equal: t]
@ -50,7 +48,7 @@ let origin_is_fun_library ta =
false false
let const_nullable is_nullable origin = {origin; is_nullable} let create ~is_nullable origin = {origin; is_nullable}
let with_origin ta o = {ta with origin= o} let with_origin ta o = {ta with origin= o}

60
infer/src/nullsafe/InferredNullability.mli
Unescape View File

@ -0,0 +1,60 @@
(*
* 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
(** 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
(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
expression according to its type inference rules.
*)
type t [@@deriving compare]
val create : is_nullable:bool -> TypeOrigin.t -> t
val descr_origin : t -> TypeErr.origin_descr
(** Human-readable description of the origin of a value.
(How did nullsafe infer the nullability )
*)
val from_nullsafe_type : NullsafeType.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.
*)
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.
{[
if(something) {
a = e1;
} else {
a = e2;
}
// what is nullability of `a` at this point?
]}
*)
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
(** Leave the same nullability, but change the origin *)

8
infer/src/nullsafe/eradicate.ml
Unescape View File

@ -34,11 +34,13 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
annotated_signature linereader proc_loc : bool * TypeState.t option = annotated_signature linereader proc_loc : bool * TypeState.t option =
let add_formal typestate (param_signature : AnnotatedSignature.param_signature) = let add_formal typestate (param_signature : AnnotatedSignature.param_signature) =
let pvar = Pvar.mk param_signature.mangled curr_pname in let pvar = Pvar.mk param_signature.mangled curr_pname in
let ta = let inferred_nullability =
let origin = TypeOrigin.Formal param_signature.mangled in let origin = TypeOrigin.Formal param_signature.mangled in
TypeAnnotation.from_nullsafe_type param_signature.param_nullsafe_type origin InferredNullability.from_nullsafe_type param_signature.param_nullsafe_type origin
in in
TypeState.add pvar (param_signature.param_nullsafe_type.typ, ta, []) typestate TypeState.add pvar
(param_signature.param_nullsafe_type.typ, inferred_nullability, [])
typestate
in in
let get_initial_typestate () = let get_initial_typestate () =
let typestate_empty = TypeState.empty in let typestate_empty = TypeState.empty in

74
infer/src/nullsafe/eradicateChecks.ml
Unescape View File

@ -45,20 +45,20 @@ let is_virtual = function
(** Check an access (read or write) to a field. *) (** Check an access (read or write) to a field. *)
let check_field_access tenv find_canonical_duplicate curr_pname node instr_ref exp fname ta loc : let check_field_access tenv find_canonical_duplicate curr_pname node instr_ref exp fname
unit = inferred_nullability loc : unit =
if TypeAnnotation.is_nullable ta then if InferredNullability.is_nullable inferred_nullability then
let origin_descr = TypeAnnotation.descr_origin ta in let origin_descr = InferredNullability.descr_origin inferred_nullability in
report_error tenv find_canonical_duplicate report_error tenv find_canonical_duplicate
(TypeErr.Null_field_access (explain_expr tenv node exp, fname, origin_descr, false)) (TypeErr.Null_field_access (explain_expr tenv node exp, fname, origin_descr, false))
(Some instr_ref) loc curr_pname (Some instr_ref) loc curr_pname
(** Check an access to an array *) (** Check an access to an array *)
let check_array_access tenv find_canonical_duplicate curr_pname node instr_ref array_exp fname ta let check_array_access tenv find_canonical_duplicate curr_pname node instr_ref array_exp fname
loc indexed = inferred_nullability loc indexed =
if TypeAnnotation.is_nullable ta then if InferredNullability.is_nullable inferred_nullability then
let origin_descr = TypeAnnotation.descr_origin ta in let origin_descr = InferredNullability.descr_origin inferred_nullability in
report_error tenv find_canonical_duplicate report_error tenv find_canonical_duplicate
(TypeErr.Null_field_access (explain_expr tenv node array_exp, fname, origin_descr, indexed)) (TypeErr.Null_field_access (explain_expr tenv node array_exp, fname, origin_descr, indexed))
(Some instr_ref) loc curr_pname (Some instr_ref) loc curr_pname
@ -76,8 +76,8 @@ type from_call =
let equal_from_call = [%compare.equal: from_call] let equal_from_call = [%compare.equal: from_call]
(** Check the normalized "is zero" or "is not zero" condition of a prune instruction. *) (** Check the normalized "is zero" or "is not zero" condition of a prune instruction. *)
let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e typ ta true_branch let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e typ
from_call idenv linereader loc instr_ref : unit = inferred_nullability true_branch from_call idenv linereader loc instr_ref : unit =
let contains_instanceof_throwable pdesc node = let contains_instanceof_throwable pdesc node =
(* Check if the current procedure has a catch Throwable. *) (* Check if the current procedure has a catch Throwable. *)
(* That always happens in the bytecode generated by try-with-resources. *) (* That always happens in the bytecode generated by try-with-resources. *)
@ -115,12 +115,12 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e ty
in in
let is_temp = Idenv.exp_is_temp idenv e in let is_temp = Idenv.exp_is_temp idenv e in
let should_report = let should_report =
(not (TypeAnnotation.is_nullable ta)) (not (InferredNullability.is_nullable inferred_nullability))
&& Config.eradicate_condition_redundant && true_branch && (not is_temp) && Config.eradicate_condition_redundant && true_branch && (not is_temp)
&& PatternMatch.type_is_class typ && PatternMatch.type_is_class typ
&& (not (from_try_with_resources ())) && (not (from_try_with_resources ()))
&& equal_from_call from_call From_condition && equal_from_call from_call From_condition
&& not (TypeAnnotation.origin_is_fun_library ta) && not (InferredNullability.origin_is_fun_library inferred_nullability)
in in
let is_always_true = not case_zero in let is_always_true = not case_zero in
if should_report then if should_report then
@ -142,14 +142,14 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r
exp_lhs exp_rhs typ loc fname field_type_opt typecheck_expr : unit = exp_lhs exp_rhs typ loc fname field_type_opt typecheck_expr : unit =
let curr_pname = Procdesc.get_proc_name curr_pdesc in let curr_pname = Procdesc.get_proc_name curr_pdesc in
let curr_pattrs = Procdesc.get_attributes curr_pdesc in let curr_pattrs = Procdesc.get_attributes curr_pdesc in
let t_lhs, ta_lhs, _ = let t_lhs, inferred_nullability_lhs, _ =
typecheck_expr node instr_ref curr_pdesc typestate exp_lhs typecheck_expr node instr_ref curr_pdesc typestate exp_lhs
(typ, TypeAnnotation.const_nullable false TypeOrigin.ONone, [loc]) (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc])
loc loc
in in
let _, ta_rhs, _ = let _, inferred_nullability_rhs, _ =
typecheck_expr node instr_ref curr_pdesc typestate exp_rhs typecheck_expr node instr_ref curr_pdesc typestate exp_rhs
(typ, TypeAnnotation.const_nullable false TypeOrigin.ONone, [loc]) (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc])
loc loc
in in
let field_is_injector_readwrite () = let field_is_injector_readwrite () =
@ -167,14 +167,15 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r
in in
let should_report_nullable = let should_report_nullable =
(not (AndroidFramework.is_destroy_method curr_pname)) (not (AndroidFramework.is_destroy_method curr_pname))
&& (not (TypeAnnotation.is_nullable ta_lhs)) && (not (InferredNullability.is_nullable inferred_nullability_lhs))
&& TypeAnnotation.is_nullable ta_rhs && PatternMatch.type_is_class t_lhs && InferredNullability.is_nullable inferred_nullability_rhs
&& PatternMatch.type_is_class t_lhs
&& (not (Typ.Fieldname.Java.is_outer_instance fname)) && (not (Typ.Fieldname.Java.is_outer_instance fname))
&& (not (field_is_injector_readwrite ())) && (not (field_is_injector_readwrite ()))
&& not (field_is_in_cleanup_context ()) && not (field_is_in_cleanup_context ())
in in
if should_report_nullable then if should_report_nullable then
let origin_descr = TypeAnnotation.descr_origin ta_rhs in let origin_descr = InferredNullability.descr_origin inferred_nullability_rhs in
report_error tenv find_canonical_duplicate report_error tenv find_canonical_duplicate
(TypeErr.Field_annotation_inconsistent (fname, origin_descr)) (TypeErr.Field_annotation_inconsistent (fname, origin_descr))
(Some instr_ref) loc curr_pdesc (Some instr_ref) loc curr_pdesc
@ -222,12 +223,13 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_pname cu
| _ -> | _ ->
true true
in in
final_type_annotation_with false (Lazy.force final_initializer_typestates) (fun ta -> final_type_annotation_with false (Lazy.force final_initializer_typestates)
origin_is_initialized (TypeAnnotation.get_origin ta) ) (fun nullability ->
origin_is_initialized (InferredNullability.get_origin nullability) )
in in
let may_be_nullable_in_final_typestate () = let may_be_nullable_in_final_typestate () =
final_type_annotation_with true (Lazy.force final_constructor_typestates) (fun ta -> final_type_annotation_with true (Lazy.force final_constructor_typestates) (fun ta ->
TypeAnnotation.is_nullable ta ) InferredNullability.is_nullable ta )
in in
let should_check_field_initialization = let should_check_field_initialization =
let in_current_class = let in_current_class =
@ -281,9 +283,9 @@ let check_return_annotation tenv find_canonical_duplicate curr_pdesc ret_range
| _ -> | _ ->
false -> false ->
() ()
| Some (_, final_ta, _) -> | Some (_, final_inferred_nullability, _) ->
let is_final_nullable = TypeAnnotation.is_nullable final_ta in let is_final_nullable = InferredNullability.is_nullable final_inferred_nullability in
let origin_descr = TypeAnnotation.descr_origin final_ta in let origin_descr = InferredNullability.descr_origin final_inferred_nullability in
let return_not_nullable = let return_not_nullable =
is_final_nullable && (not ret_annotated_nullable) && not ret_implicitly_nullable is_final_nullable && (not ret_annotated_nullable) && not ret_implicitly_nullable
in in
@ -306,15 +308,15 @@ let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate
callee_pname (instr_ref : TypeErr.InstrRef.t) loc typecheck_expr : unit = callee_pname (instr_ref : TypeErr.InstrRef.t) loc typecheck_expr : unit =
match call_params with match call_params with
| ((original_this_e, this_e), typ) :: _ -> | ((original_this_e, this_e), typ) :: _ ->
let _, this_ta, _ = let _, this_inferred_nullability, _ =
typecheck_expr tenv node instr_ref curr_pdesc typestate this_e typecheck_expr tenv node instr_ref curr_pdesc typestate this_e
(typ, TypeAnnotation.const_nullable false TypeOrigin.ONone, []) (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [])
loc loc
in in
let null_method_call = TypeAnnotation.is_nullable this_ta in let null_method_call = InferredNullability.is_nullable this_inferred_nullability in
if null_method_call then if null_method_call then
let descr = explain_expr tenv node original_this_e in let descr = explain_expr tenv node original_this_e in
let origin_descr = TypeAnnotation.descr_origin this_ta in let origin_descr = InferredNullability.descr_origin this_inferred_nullability in
report_error tenv find_canonical_duplicate report_error tenv find_canonical_duplicate
(TypeErr.Call_receiver_annotation_inconsistent (descr, callee_pname, origin_descr)) (TypeErr.Call_receiver_annotation_inconsistent (descr, callee_pname, origin_descr))
(Some instr_ref) loc curr_pdesc (Some instr_ref) loc curr_pdesc
@ -324,16 +326,16 @@ let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate
type resolved_param = type resolved_param =
{ num: int { num: int
; formal: Mangled.t * TypeAnnotation.t * Typ.t ; formal: Mangled.t * InferredNullability.t * Typ.t
; actual: Exp.t * TypeAnnotation.t ; actual: Exp.t * InferredNullability.t
; is_formal_propagates_nullable: bool } ; is_formal_propagates_nullable: bool }
(** Check the parameters of a call. *) (** Check the parameters of a call. *)
let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_attributes let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_attributes
resolved_params loc instr_ref : unit = resolved_params loc instr_ref : unit =
let callee_pname = callee_attributes.ProcAttributes.proc_name in let callee_pname = callee_attributes.ProcAttributes.proc_name in
let check {num= param_num; formal= s1, annotation_formal, t1; actual= orig_e2, annotation_actual} let check
= {num= param_num; formal= s1, nullability_formal, t1; actual= orig_e2, nullability_actual} =
let report () = let report () =
let description = let description =
match explain_expr tenv node orig_e2 with match explain_expr tenv node orig_e2 with
@ -342,7 +344,7 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
| None -> | None ->
"formal parameter " ^ Mangled.to_string s1 "formal parameter " ^ Mangled.to_string s1
in in
let origin_descr = TypeAnnotation.descr_origin annotation_actual in let origin_descr = InferredNullability.descr_origin nullability_actual in
let callee_loc = callee_attributes.ProcAttributes.loc in let callee_loc = callee_attributes.ProcAttributes.loc in
report_error tenv find_canonical_duplicate report_error tenv find_canonical_duplicate
(TypeErr.Parameter_annotation_inconsistent (TypeErr.Parameter_annotation_inconsistent
@ -350,8 +352,8 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
(Some instr_ref) loc curr_pdesc (Some instr_ref) loc curr_pdesc
in in
if PatternMatch.type_is_class t1 then if PatternMatch.type_is_class t1 then
let is_nullable_formal = TypeAnnotation.is_nullable annotation_formal in let is_nullable_formal = InferredNullability.is_nullable nullability_formal in
let is_nullable_actual = TypeAnnotation.is_nullable annotation_actual in let is_nullable_actual = InferredNullability.is_nullable nullability_actual in
if (not is_nullable_formal) && is_nullable_actual then report () if (not is_nullable_formal) && is_nullable_actual then report ()
in in
let should_check_parameters = let should_check_parameters =

33
infer/src/nullsafe/typeAnnotation.mli
Unescape View File

@ -1,33 +0,0 @@
(*
* 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
(** Nodule to represent annotations on types. *)
type t [@@deriving compare]
val const_nullable : bool -> TypeOrigin.t -> t
val descr_origin : t -> TypeErr.origin_descr
(** Human-readable description of the origin of a nullable value. *)
val from_nullsafe_type : NullsafeType.t -> TypeOrigin.t -> t
val get_origin : t -> TypeOrigin.t
val is_nullable : t -> bool
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

115
infer/src/nullsafe/typeCheck.ml
Unescape View File

@ -113,10 +113,10 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r
(curr_pdesc : Procdesc.t) typestate e tr_default loc : TypeState.range = (curr_pdesc : Procdesc.t) typestate e tr_default loc : TypeState.range =
match e with match e with
| _ when Exp.is_null_literal e -> | _ when Exp.is_null_literal e ->
let typ, ta, locs = tr_default in let typ, inferred_nullability, locs = tr_default in
if PatternMatch.type_is_class typ then if PatternMatch.type_is_class typ then
(typ, TypeAnnotation.const_nullable true (TypeOrigin.Const loc), locs) (typ, InferredNullability.create ~is_nullable:true (TypeOrigin.Const loc), locs)
else (typ, TypeAnnotation.with_origin ta (TypeOrigin.Const loc), locs) else (typ, InferredNullability.with_origin inferred_nullability (TypeOrigin.Const loc), locs)
| Exp.Lvar pvar -> ( | Exp.Lvar pvar -> (
match TypeState.lookup_pvar pvar typestate with match TypeState.lookup_pvar pvar typestate with
| Some tr -> | Some tr ->
@ -134,21 +134,21 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r
typestate e1 tr_default loc typestate e1 tr_default loc
| Exp.Const _ -> | Exp.Const _ ->
let typ, _, locs = tr_default in let typ, _, locs = tr_default in
(typ, TypeAnnotation.const_nullable false (TypeOrigin.Const loc), locs) (typ, InferredNullability.create ~is_nullable:false (TypeOrigin.Const loc), locs)
| Exp.Lfield (exp, fn, typ) -> | Exp.Lfield (exp, fn, typ) ->
let _, _, locs = tr_default in let _, _, locs = tr_default in
let _, ta, locs' = let _, inferred_nullability, locs' =
typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc
typestate exp typestate exp
(typ, TypeAnnotation.const_nullable false TypeOrigin.ONone, locs) (typ, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, locs)
loc loc
in in
let exp_origin = TypeAnnotation.get_origin ta in let exp_origin = InferredNullability.get_origin inferred_nullability in
let tr_new = let tr_new =
match EradicateChecks.get_field_annotation tenv fn typ with match EradicateChecks.get_field_annotation tenv fn typ with
| Some EradicateChecks.{nullsafe_type} -> | Some EradicateChecks.{nullsafe_type} ->
( nullsafe_type.typ ( nullsafe_type.typ
, TypeAnnotation.from_nullsafe_type nullsafe_type , InferredNullability.from_nullsafe_type nullsafe_type
(TypeOrigin.Field (exp_origin, fn, loc)) (TypeOrigin.Field (exp_origin, fn, loc))
, locs' ) , locs' )
| None -> | None ->
@ -156,7 +156,7 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r
in in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_field_access tenv find_canonical_duplicate curr_pdesc node instr_ref EradicateChecks.check_field_access tenv find_canonical_duplicate curr_pdesc node instr_ref
exp fn ta loc ; exp fn inferred_nullability loc ;
tr_new tr_new
| Exp.Lindex (array_exp, index_exp) -> | Exp.Lindex (array_exp, index_exp) ->
let _, ta, _ = let _, ta, _ =
@ -188,8 +188,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
in in
let pvar_get_origin pvar = let pvar_get_origin pvar =
match TypeState.lookup_pvar pvar typestate with match TypeState.lookup_pvar pvar typestate with
| Some (_, ta, _) -> | Some (_, inferred_nullability, _) ->
Some (TypeAnnotation.get_origin ta) Some (InferredNullability.get_origin inferred_nullability)
| None -> | None ->
None None
in in
@ -229,7 +229,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
| Some EradicateChecks.{nullsafe_type} -> | Some EradicateChecks.{nullsafe_type} ->
let range = let range =
( nullsafe_type.typ ( nullsafe_type.typ
, TypeAnnotation.from_nullsafe_type nullsafe_type , InferredNullability.from_nullsafe_type nullsafe_type
(TypeOrigin.Field (origin, fn, loc)) (TypeOrigin.Field (origin, fn, loc))
, [loc] ) , [loc] )
in in
@ -249,8 +249,10 @@ 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 pvar = Pvar.mk (Mangled.from_string exp_str) curr_pname in
let already_defined_in_typestate = let already_defined_in_typestate =
match TypeState.lookup_pvar pvar typestate with match TypeState.lookup_pvar pvar typestate with
| Some (_, ta, _) -> | Some (_, inferred_nullability, _) ->
not (TypeOrigin.equal TypeOrigin.Undef (TypeAnnotation.get_origin ta)) not
(TypeOrigin.equal TypeOrigin.Undef
(InferredNullability.get_origin inferred_nullability))
| None -> | None ->
false false
in in
@ -282,7 +284,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
| _ -> | _ ->
None ) None )
|> Option.value_map |> Option.value_map
~f:(fun (_, ta, _) -> TypeAnnotation.get_origin ta) ~f:(fun (_, nullability, _) -> InferredNullability.get_origin nullability)
~default:TypeOrigin.ONone ~default:TypeOrigin.ONone
in in
let exp' = Idenv.expand_expr_temps idenv node exp_ in let exp' = Idenv.expand_expr_temps idenv node exp_ in
@ -406,7 +408,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
let typecheck_expr_simple typestate1 exp1 typ1 origin1 loc1 = let typecheck_expr_simple typestate1 exp1 typ1 origin1 loc1 =
typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc
typestate1 exp1 typestate1 exp1
(typ1, TypeAnnotation.const_nullable false origin1, [loc1]) (typ1, InferredNullability.create ~is_nullable:false origin1, [loc1])
loc1 loc1
in in
(* check if there are errors in exp1 *) (* check if there are errors in exp1 *)
@ -460,7 +462,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
when Typ.Procname.equal pn BuiltinDecl.__new || Typ.Procname.equal pn BuiltinDecl.__new_array when Typ.Procname.equal pn BuiltinDecl.__new || Typ.Procname.equal pn BuiltinDecl.__new_array
-> ->
TypeState.add_id id TypeState.add_id id
(typ, TypeAnnotation.const_nullable false TypeOrigin.New, [loc]) (typ, InferredNullability.create ~is_nullable:false TypeOrigin.New, [loc])
typestate typestate
(* new never returns null *) (* new never returns null *)
| Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _)
@ -474,7 +476,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
let _, ta, _ = let _, ta, _ =
typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc
typestate array_exp typestate array_exp
(t, TypeAnnotation.const_nullable false TypeOrigin.ONone, [loc]) (t, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc])
loc loc
in in
if checks.eradicate then if checks.eradicate then
@ -483,7 +485,9 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
(Typ.Fieldname.Java.from_string "length") (Typ.Fieldname.Java.from_string "length")
ta loc false ; ta loc false ;
TypeState.add_id id TypeState.add_id id
(Typ.mk (Tint Typ.IInt), TypeAnnotation.const_nullable false TypeOrigin.New, [loc]) ( Typ.mk (Tint Typ.IInt)
, InferredNullability.create ~is_nullable:false TypeOrigin.New
, [loc] )
typestate typestate
| Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn -> | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn ->
typestate (* skip othe builtins *) typestate (* skip othe builtins *)
@ -544,11 +548,11 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
let clear_nullable_flag typestate'' pvar = let clear_nullable_flag typestate'' pvar =
(* remove the nullable flag for the given pvar *) (* remove the nullable flag for the given pvar *)
match TypeState.lookup_pvar pvar typestate'' with match TypeState.lookup_pvar pvar typestate'' with
| Some (t, ta, _) -> | Some (t, nullability, _) ->
let should_report = let should_report =
Config.eradicate_condition_redundant Config.eradicate_condition_redundant
&& (not (TypeAnnotation.is_nullable ta)) && (not (InferredNullability.is_nullable nullability))
&& not (TypeAnnotation.origin_is_fun_library ta) && not (InferredNullability.origin_is_fun_library nullability)
in in
( if checks.eradicate && should_report then ( if checks.eradicate && should_report then
let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in
@ -556,7 +560,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
(TypeErr.Condition_redundant (true, EradicateChecks.explain_expr tenv node cond)) (TypeErr.Condition_redundant (true, EradicateChecks.explain_expr tenv node cond))
(Some instr_ref) loc curr_pdesc ) ; (Some instr_ref) loc curr_pdesc ) ;
TypeState.add pvar TypeState.add pvar
(t, TypeAnnotation.const_nullable false TypeOrigin.ONone, [loc]) (t, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [loc])
typestate'' typestate''
| None -> | None ->
typestate' typestate'
@ -588,12 +592,12 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
in in
(* Handle Preconditions.checkState for &&-separated conditions x!=null. *) (* Handle Preconditions.checkState for &&-separated conditions x!=null. *)
let do_preconditions_check_state typestate' = let do_preconditions_check_state typestate' =
let handle_pvar b typestate1 pvar = let handle_pvar is_nullable typestate1 pvar =
(* handle the annotation flag for pvar *) (* handle the annotation flag for pvar *)
match TypeState.lookup_pvar pvar typestate1 with match TypeState.lookup_pvar pvar typestate1 with
| Some (t, _, _) -> | Some (t, _, _) ->
TypeState.add pvar TypeState.add pvar
(t, TypeAnnotation.const_nullable b TypeOrigin.ONone, [loc]) (t, InferredNullability.create ~is_nullable TypeOrigin.ONone, [loc])
typestate1 typestate1
| None -> | None ->
typestate1 typestate1
@ -683,22 +687,22 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
typestate' typestate'
in in
let typestate_after_call, finally_resolved_ret = let typestate_after_call, finally_resolved_ret =
let resolve_param i (sparam, cparam) = let resolve_param i (formal_param, actual_param) =
let AnnotatedSignature.{mangled; param_annotation_deprecated; param_nullsafe_type} = let AnnotatedSignature.{mangled; param_annotation_deprecated; param_nullsafe_type} =
sparam formal_param
in in
let (orig_e2, e2), t2 = cparam in let (orig_e2, e2), t2 = actual_param in
let ta1 = let inferred_nullability_formal =
TypeAnnotation.from_nullsafe_type param_nullsafe_type (TypeOrigin.Formal mangled) InferredNullability.from_nullsafe_type param_nullsafe_type (TypeOrigin.Formal mangled)
in in
let _, ta2, _ = let _, inferred_nullability_actual, _ =
typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref
curr_pdesc typestate e2 curr_pdesc typestate e2
(t2, TypeAnnotation.const_nullable false TypeOrigin.ONone, []) (t2, InferredNullability.create ~is_nullable:false TypeOrigin.ONone, [])
loc loc
in in
let formal = (mangled, ta1, param_nullsafe_type.typ) in let formal = (mangled, inferred_nullability_formal, param_nullsafe_type.typ) in
let actual = (orig_e2, ta2) in let actual = (orig_e2, inferred_nullability_actual) in
let num = i + 1 in let num = i + 1 in
let is_formal_propagates_nullable = let is_formal_propagates_nullable =
Annotations.ia_is_propagates_nullable param_annotation_deprecated Annotations.ia_is_propagates_nullable param_annotation_deprecated
@ -719,12 +723,12 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
else if else if
List.for_all propagates_nullable_params List.for_all propagates_nullable_params
~f:(fun EradicateChecks.{actual= _, inferred_nullability_actual} -> ~f:(fun EradicateChecks.{actual= _, inferred_nullability_actual} ->
not (TypeAnnotation.is_nullable inferred_nullability_actual) ) not (InferredNullability.is_nullable inferred_nullability_actual) )
then then
(* All params' inferred types are non-nullable. (* All params' inferred types are non-nullable.
Strengten the result to be non-nullable as well! *) Strengten the result to be non-nullable as well! *)
let ret_type_annotation, ret_typ = ret in let ret_type_annotation, ret_typ = ret in
(TypeAnnotation.set_nullable false ret_type_annotation, ret_typ) (InferredNullability.set_nullable false ret_type_annotation, ret_typ)
else else
(* At least one param's inferred type is nullable, can not strengthen the result *) (* At least one param's inferred type is nullable, can not strengthen the result *)
ret ret
@ -740,8 +744,10 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
; annotated_signature= callee_annotated_signature ; annotated_signature= callee_annotated_signature
; is_library } ; is_library }
in in
let ret_ta = TypeAnnotation.from_nullsafe_type ret.ret_nullsafe_type origin in let ret_inferred_nullability =
(ret_ta, ret.ret_nullsafe_type.typ) InferredNullability.from_nullsafe_type ret.ret_nullsafe_type origin
in
(ret_inferred_nullability, ret.ret_nullsafe_type.typ)
in in
let sig_len = List.length signature_params in let sig_len = List.length signature_params in
let call_len = List.length call_params in let call_len = List.length call_params in
@ -860,14 +866,16 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
| None -> | None ->
(typestate, e, EradicateChecks.From_condition) (typestate, e, EradicateChecks.From_condition)
in in
let set_nullable_flag e' b typestate2 = let set_nullable_flag e' should_set_nullable typestate2 =
(* add constraint on e' for annotation ann *) (* add constraint on e' for annotation a given nullability *)
let handle_pvar typestate' pvar = let handle_pvar typestate' pvar =
match TypeState.lookup_pvar pvar typestate' with match TypeState.lookup_pvar pvar typestate' with
| Some (t, ta1, locs) -> | Some (t, current_nullability, locs) ->
if TypeAnnotation.is_nullable ta1 <> b then if InferredNullability.is_nullable current_nullability <> should_set_nullable then
let ta2 = TypeAnnotation.set_nullable b ta1 in let new_nullability =
TypeState.add pvar (t, ta2, locs) typestate' InferredNullability.set_nullable should_set_nullable current_nullability
in
TypeState.add pvar (t, new_nullability, locs) typestate'
else typestate' else typestate'
| None -> | None ->
typestate' typestate'
@ -891,16 +899,18 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
(typestate, e, EradicateChecks.From_condition) (typestate, e, EradicateChecks.From_condition)
in in
let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in
let typ, ta, _ = let typ, inferred_nullability, _ =
typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc
in in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_zero tenv find_canonical_duplicate curr_pdesc node' e' typ ta EradicateChecks.check_zero tenv find_canonical_duplicate curr_pdesc node' e' typ
true_branch EradicateChecks.From_condition idenv linereader loc instr_ref ; inferred_nullability true_branch EradicateChecks.From_condition idenv linereader
loc instr_ref ;
match from_call with match from_call with
| EradicateChecks.From_is_true_on_null -> | EradicateChecks.From_is_true_on_null ->
(* if f returns true on null, then false branch implies != null *) (* if f returns true on null, then false branch implies != null *)
if TypeAnnotation.is_nullable ta then set_nullable_flag e' false typestate2 if InferredNullability.is_nullable inferred_nullability then
set_nullable_flag e' false typestate2
else typestate2 else typestate2
| _ -> | _ ->
typestate2 ) typestate2 )
@ -922,12 +932,12 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
else (typestate, e, EradicateChecks.From_condition) ) else (typestate, e, EradicateChecks.From_condition) )
in in
let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in
let typ, ta, _ = let typ, inferred_nullability, _ =
typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc
in in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc node e' typ ta EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc node e' typ
true_branch from_call idenv linereader loc instr_ref ; inferred_nullability true_branch from_call idenv linereader loc instr_ref ;
match from_call with match from_call with
| EradicateChecks.From_is_true_on_null -> | EradicateChecks.From_is_true_on_null ->
typestate2 typestate2
@ -935,7 +945,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
| EradicateChecks.From_containsKey | EradicateChecks.From_containsKey
| EradicateChecks.From_instanceof | EradicateChecks.From_instanceof
| EradicateChecks.From_is_false_on_null -> | EradicateChecks.From_is_false_on_null ->
if TypeAnnotation.is_nullable ta then set_nullable_flag e' false typestate2 if InferredNullability.is_nullable inferred_nullability then
set_nullable_flag e' false typestate2
else typestate2 ) else typestate2 )
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, e1, e2), _) -> | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, e1, e2), _) ->
check_condition node' (Exp.BinOp (Binop.Ne, e1, e2)) check_condition node' (Exp.BinOp (Binop.Ne, e1, e2))

14
infer/src/nullsafe/typeState.ml
Unescape View File

@ -17,7 +17,7 @@ module M = Caml.Map.Make (struct
let compare = Exp.compare let compare = Exp.compare
end) end)
type range = Typ.t * TypeAnnotation.t * Location.t list [@@deriving compare] type range = Typ.t * InferredNullability.t * Location.t list [@@deriving compare]
type t = range M.t [@@deriving compare] type t = range M.t [@@deriving compare]
@ -30,8 +30,9 @@ let pp fmt typestate =
let pp_locs fmt locs = F.fprintf fmt " [%a]" (Pp.seq pp_loc) locs in let pp_locs fmt locs = F.fprintf fmt " [%a]" (Pp.seq pp_loc) locs in
let pp_one exp (typ, ta, locs) = let pp_one exp (typ, ta, locs) =
F.fprintf fmt " %a -> [%s] %s %a%a@\n" Exp.pp exp F.fprintf fmt " %a -> [%s] %s %a%a@\n" Exp.pp exp
(TypeOrigin.to_string (TypeAnnotation.get_origin ta)) (TypeOrigin.to_string (InferredNullability.get_origin ta))
(TypeAnnotation.to_string ta) (Typ.pp_full Pp.text) typ pp_locs locs (InferredNullability.to_string ta)
(Typ.pp_full Pp.text) typ pp_locs locs
in in
let pp_map map = M.iter pp_one map in let pp_map map = M.iter pp_one map in
pp_map typestate pp_map typestate
@ -50,8 +51,11 @@ let range_add_locs (typ, ta, locs1) locs2 =
let map_join m1 m2 = let map_join m1 m2 =
let range_join _exp range1_opt range2_opt = let range_join _exp range1_opt range2_opt =
Option.both range1_opt range2_opt Option.both range1_opt range2_opt
|> Option.map ~f:(fun (((typ1, ta1, locs1) as range1), (typ2, ta2, locs2)) -> |> Option.map
TypeAnnotation.join ta1 ta2 ~f:(fun ( ((typ1, inferred_nullability1, locs1) as range1)
, (typ2, inferred_nullability2, locs2) )
->
InferredNullability.join inferred_nullability1 inferred_nullability2
|> Option.value_map ~default:range1 ~f:(fun ta' -> |> Option.value_map ~default:range1 ~f:(fun ta' ->
let typ' = type_join typ1 typ2 in let typ' = type_join typ1 typ2 in
let locs' = locs_join locs1 locs2 in let locs' = locs_join locs1 locs2 in

2
infer/src/nullsafe/typeState.mli
Unescape View File

@ -12,7 +12,7 @@ open! IStd
(** Typestate *) (** Typestate *)
type t type t
type range = Typ.t * TypeAnnotation.t * Location.t list type range = Typ.t * InferredNullability.t * Location.t list
val add_id : Ident.t -> range -> t -> t val add_id : Ident.t -> range -> t -> t

Write Preview
Loading…
Cancel
Save