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

[nullsafe] Remove calculating locations in typestate `range`

Browse Source 
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
master
Mitya Lyubarskiy 5 years ago committed by Facebook Github Bot
parent cf6f107b88
commit cf6c78a64a
5 changed files with 57 additions and 84 deletions
Show Stats Download Patch File Download Diff File

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

@ -39,9 +39,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
InferredNullability.of_annotated_nullability InferredNullability.of_annotated_nullability
param_signature.param_annotated_type.nullability origin param_signature.param_annotated_type.nullability origin
in in
TypeState.add pvar TypeState.add pvar (param_signature.param_annotated_type.typ, inferred_nullability) typestate
(param_signature.param_annotated_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
@ -54,7 +52,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
let ret_pvar = Procdesc.get_ret_var curr_pdesc in let ret_pvar = Procdesc.get_ret_var curr_pdesc in
let ret_range = TypeState.lookup_pvar ret_pvar final_typestate in let ret_range = TypeState.lookup_pvar ret_pvar final_typestate in
let typ_found_opt = 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 in
(* TODO(T54088319): model this in AnnotatedNullability *) (* TODO(T54088319): model this in AnnotatedNullability *)
let ret_implicitly_nullable = let ret_implicitly_nullable =

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

@ -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 = 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_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, inferred_nullability_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
(* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
(typ, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) (typ, InferredNullability.create_nonnull TypeOrigin.ONone)
loc loc
in in
let _, inferred_nullability_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
(* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
(typ, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) (typ, InferredNullability.create_nonnull TypeOrigin.ONone)
loc loc
in in
let field_is_injector_readwrite () = let field_is_injector_readwrite () =
@ -206,7 +206,7 @@ let get_nullability_upper_bound_for_typestate proc_name field_name typestate =
*) *)
Nullability.top Nullability.top
(* We were able to lookup the field. Its nullability gives precise upper bound. *) (* We were able to lookup the field. Its nullability gives precise upper bound. *)
| Some (_, inferred_nullability, _) -> | Some (_, inferred_nullability) ->
InferredNullability.get_nullability inferred_nullability InferredNullability.get_nullability inferred_nullability
@ -254,7 +254,7 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc
in in
predicate_holds_for_some_typestate predicate_holds_for_some_typestate
(Lazy.force typestates_for_curr_constructor_and_all_initializer_methods) field_name (Lazy.force typestates_for_curr_constructor_and_all_initializer_methods) field_name
~predicate:(fun (_, nullability, _) -> ~predicate:(fun (_, nullability) ->
is_initialized (InferredNullability.get_origin nullability) ) is_initialized (InferredNullability.get_origin nullability) )
in in
(* TODO(T54584721) This check is completely independent of the current constuctor we check. (* 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 -> false ->
() ()
| Some (_, ret_inferred_nullability, _) -> | Some (_, ret_inferred_nullability) ->
(* TODO(T54308240) Model ret_implicitly_nullable in AnnotatedNullability *) (* TODO(T54308240) Model ret_implicitly_nullable in AnnotatedNullability *)
if not ret_implicitly_nullable then if not ret_implicitly_nullable then
check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_pdesc 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 = 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_inferred_nullability, _ = 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
(* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
(typ, InferredNullability.create_nonnull TypeOrigin.ONone, []) (typ, InferredNullability.create_nonnull TypeOrigin.ONone)
loc loc
in in
check_object_dereference tenv find_canonical_duplicate curr_pdesc node instr_ref check_object_dereference tenv find_canonical_duplicate curr_pdesc node instr_ref

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

@ -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 = (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, inferred_nullability, locs = tr_default in let typ, inferred_nullability = tr_default in
if PatternMatch.type_is_class typ then if PatternMatch.type_is_class typ then
(typ, InferredNullability.create_nullable (TypeOrigin.Const loc), locs) (typ, InferredNullability.create_nullable (TypeOrigin.Const loc))
else (typ, InferredNullability.with_origin inferred_nullability (TypeOrigin.Const loc), locs) else (typ, InferredNullability.with_origin inferred_nullability (TypeOrigin.Const loc))
| Exp.Lvar pvar -> ( | Exp.Lvar pvar ->
match TypeState.lookup_pvar pvar typestate with Option.value (TypeState.lookup_pvar pvar typestate) ~default:tr_default
| Some tr -> | Exp.Var id ->
TypeState.range_add_locs tr [loc] Option.value (TypeState.lookup_id id typestate) ~default:tr_default
| None ->
tr_default )
| Exp.Var id -> (
match TypeState.lookup_id id typestate with
| Some tr ->
TypeState.range_add_locs tr [loc]
| None ->
tr_default )
| Exp.Exn e1 -> | Exp.Exn e1 ->
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 e1 tr_default loc typestate e1 tr_default loc
| Exp.Const _ -> | Exp.Const _ ->
let typ, _, locs = tr_default in let typ, _ = tr_default in
(typ, InferredNullability.create_nonnull (TypeOrigin.Const loc), locs) (typ, InferredNullability.create_nonnull (TypeOrigin.Const loc))
| Exp.Lfield (exp, field_name, typ) -> | Exp.Lfield (exp, field_name, typ) ->
let _, _, locs = tr_default in let _, _ = tr_default in
let _, inferred_nullability, locs' = let _, inferred_nullability =
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
(* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
(typ, InferredNullability.create_nonnull TypeOrigin.ONone, locs) (typ, InferredNullability.create_nonnull TypeOrigin.ONone)
loc loc
in in
let exp_origin = InferredNullability.get_origin inferred_nullability 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} -> | Some AnnotatedField.{annotated_type} ->
( annotated_type.typ ( annotated_type.typ
, InferredNullability.of_annotated_nullability annotated_type.nullability , InferredNullability.of_annotated_nullability annotated_type.nullability
(TypeOrigin.Field (exp_origin, field_name, loc)) (TypeOrigin.Field (exp_origin, field_name, loc)) )
, locs' )
| None -> | None ->
tr_default tr_default
in 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 ; instr_ref exp (TypeErr.AccessToField field_name) inferred_nullability loc ;
tr_new tr_new
| Exp.Lindex (array_exp, index_exp) -> | 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 typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc
typestate array_exp tr_default loc typestate array_exp tr_default loc
in in
@ -190,7 +181,7 @@ 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 (_, inferred_nullability, _) -> | Some (_, inferred_nullability) ->
Some (InferredNullability.get_origin inferred_nullability) Some (InferredNullability.get_origin inferred_nullability)
| None -> | None ->
None None
@ -232,8 +223,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
let range = let range =
( annotated_type.typ ( annotated_type.typ
, InferredNullability.of_annotated_nullability annotated_type.nullability , InferredNullability.of_annotated_nullability annotated_type.nullability
(TypeOrigin.Field (origin, fn, loc)) (TypeOrigin.Field (origin, fn, loc)) )
, [loc] )
in in
TypeState.add pvar range typestate TypeState.add pvar range typestate
| None -> | 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 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 (_, inferred_nullability, _) -> | Some (_, inferred_nullability) ->
not not
(TypeOrigin.equal TypeOrigin.Undef (TypeOrigin.equal TypeOrigin.Undef
(InferredNullability.get_origin inferred_nullability)) (InferredNullability.get_origin inferred_nullability))
@ -286,7 +276,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 (_, nullability, _) -> InferredNullability.get_origin nullability) ~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
@ -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 = 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, InferredNullability.create_nonnull origin1, [loc1]) (typ1, InferredNullability.create_nonnull origin1)
loc1 loc1
in in
(* check if there are errors in exp1 *) (* 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 typestate1
in in
check_field_assign () ; typestate2 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 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 *) (* 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, _)
when Typ.Procname.equal pn BuiltinDecl.__cast -> 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' 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, _) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _)
when Typ.Procname.equal pn BuiltinDecl.__get_array_length -> 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 typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc
typestate array_exp typestate array_exp
(* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
(t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) (t, InferredNullability.create_nonnull TypeOrigin.ONone)
loc loc
in in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node
instr_ref array_exp TypeErr.ArrayLengthAccess ta loc ; instr_ref array_exp TypeErr.ArrayLengthAccess ta loc ;
TypeState.add_id id 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 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 *)
@ -534,8 +524,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
let is_anonymous_inner_class_constructor = let is_anonymous_inner_class_constructor =
Typ.Procname.Java.is_anonymous_inner_class_constructor callee_pname_java Typ.Procname.Java.is_anonymous_inner_class_constructor callee_pname_java
in in
let do_return (ret_ta, ret_typ) loc' typestate' = let do_return (ret_ta, ret_typ) typestate' =
let mk_return_range () = (ret_typ, ret_ta, [loc']) in let mk_return_range () = (ret_typ, ret_ta) in
let id = fst ret_id_typ in let id = fst ret_id_typ in
TypeState.add_id id (mk_return_range ()) typestate' TypeState.add_id id (mk_return_range ()) typestate'
in 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 = 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, nullability, _) -> | Some (t, nullability) ->
let should_report = let should_report =
Config.eradicate_condition_redundant Config.eradicate_condition_redundant
&& InferredNullability.is_nonnull nullability && 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 ) ; (Some instr_ref) loc curr_pdesc ) ;
TypeState.add pvar TypeState.add pvar
(* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
(t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) (t, InferredNullability.create_nonnull TypeOrigin.ONone)
typestate'' typestate''
| None -> | None ->
typestate' 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 = let set_nonnull_to_pvar 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
(* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
(t, InferredNullability.create_nonnull TypeOrigin.ONone, [loc]) (t, InferredNullability.create_nonnull TypeOrigin.ONone)
typestate1 typestate1
| None -> | None ->
typestate1 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 typestate_after_call, finally_resolved_ret =
let resolve_param i (formal_param, actual_param) = let resolve_param i (formal_param, actual_param) =
let (orig_e2, e2), t2 = actual_param in 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 typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref
curr_pdesc typestate e2 curr_pdesc typestate e2
(* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
(t2, InferredNullability.create_nonnull TypeOrigin.ONone, []) (t2, InferredNullability.create_nonnull TypeOrigin.ONone)
loc loc
in in
let actual = (orig_e2, inferred_nullability_actual) 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 in
(typestate_after_call, ret_respecting_propagates_nullable) (typestate_after_call, ret_respecting_propagates_nullable)
in in
do_return finally_resolved_ret loc typestate_after_call do_return finally_resolved_ret typestate_after_call
| Sil.Call _ -> | Sil.Call _ ->
typestate typestate
| Sil.Prune (cond, loc, true_branch, _) -> | 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 -> | Some e_str ->
let pvar = Pvar.mk (Mangled.from_string e_str) curr_pname in let pvar = Pvar.mk (Mangled.from_string e_str) curr_pname in
let e1 = Exp.Lvar pvar in let e1 = Exp.Lvar pvar in
let typ, ta, _ = let typ, ta =
typecheck_expr_simple typestate e1 (Typ.mk Tvoid) TypeOrigin.ONone loc typecheck_expr_simple typestate e1 (Typ.mk Tvoid) TypeOrigin.ONone loc
in in
let range = (typ, ta, [loc]) in let range = (typ, ta) in
let typestate1 = TypeState.add pvar range typestate in let typestate1 = TypeState.add pvar range typestate in
(typestate1, e1, EradicateChecks.From_containsKey) (typestate1, e1, EradicateChecks.From_containsKey)
| None -> | 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 set_nonnull e' typestate2 =
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, current_nullability, locs) -> | Some (t, current_nullability) ->
if not (InferredNullability.is_nonnull current_nullability) then if not (InferredNullability.is_nonnull current_nullability) then
let new_nullability = InferredNullability.set_nonnull current_nullability in 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' else typestate'
| None -> | None ->
typestate' typestate'
@ -890,7 +880,7 @@ 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, inferred_nullability, _ = 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
@ -923,7 +913,7 @@ 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, inferred_nullability, _ = 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

25
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 * InferredNullability.t * Location.t list [@@deriving compare] type range = Typ.t * InferredNullability.t [@@deriving compare]
type t = range M.t [@@deriving compare] type t = range M.t [@@deriving compare]
@ -26,13 +26,11 @@ let equal = [%compare.equal: t]
let empty = M.empty let empty = M.empty
let pp fmt typestate = let pp fmt typestate =
let pp_loc fmt loc = F.pp_print_int fmt loc.Location.line in let pp_one exp (typ, ta) =
let pp_locs fmt locs = F.fprintf fmt " [%a]" (Pp.seq pp_loc) locs in F.fprintf fmt " %a -> [%s] %s %a@\n" Exp.pp exp
let pp_one exp (typ, ta, locs) =
F.fprintf fmt " %a -> [%s] %s %a%a@\n" Exp.pp exp
(TypeOrigin.to_string (InferredNullability.get_origin ta)) (TypeOrigin.to_string (InferredNullability.get_origin ta))
(InferredNullability.to_string ta) (InferredNullability.to_string ta)
(Typ.pp_full Pp.text) typ pp_locs locs (Typ.pp_full Pp.text) typ
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
@ -40,26 +38,15 @@ let pp fmt typestate =
let type_join typ1 typ2 = if PatternMatch.type_is_object typ1 then typ2 else typ1 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 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 |> Option.map
~f:(fun ( ((typ1, inferred_nullability1, locs1) as range1) ~f:(fun (((typ1, inferred_nullability1) as range1), (typ2, inferred_nullability2)) ->
, (typ2, inferred_nullability2, locs2) )
->
InferredNullability.join inferred_nullability1 inferred_nullability2 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 (typ', ta') ) )
(typ', ta', locs') ) )
in in
if phys_equal m1 m2 then m1 else M.merge range_join m1 m2 if phys_equal m1 m2 then m1 else M.merge range_join m1 m2

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

@ -12,7 +12,7 @@ open! IStd
(** Typestate *) (** Typestate *)
type t 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 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 pp : Format.formatter -> t -> unit
val range_add_locs : range -> Location.t list -> range
val remove_id : Ident.t -> t -> t val remove_id : Ident.t -> t -> t

Write Preview
Loading…
Cancel
Save