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

[nullsafe][refactor] Don't update typestate twice when typechecking Store instruction

Browse Source 
Summary:
The previous diff finally unblocks this important milestone.
Now we have only one place when `convert_complex_exp_to_pvar` needs to
modify the typestate (in Sil.Load typechecking).

Because the only case left is when `~is_assignment: false`, we also can
simplify logic of updating the typestate (remove dependency on
`is_assignment`, and rename the methods so they more clearly say what
they do (instead of vague "update_typestate").

This diff, in turn, unblocks further refactoring. Namely, remove this
remaining usage of
`convert_complex_exp_to_pvar_and_register_field_in_typestate` from
Sil.Load instruction so that there is no tricky field magic left!

We will try doing it in follow up diffs.

Reviewed By: artempyanykh

Differential Revision: D20334924

fbshipit-source-id: 20ce185ed
master
Mitya Lyubarskiy 5 years ago committed by Facebook Github Bot
parent 28db342629
commit 16554689ee
1 changed files with 47 additions and 36 deletions
Show Stats Download Patch File Download Diff File

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

@ -244,13 +244,11 @@ let funcall_exp_to_original_pvar_exp tenv curr_pname typestate exp ~is_assignmen
exp exp
(* If this is an assignment, update the typestate for a field access pvar. *) let add_field_to_typestate_if_absent tenv access_loc typestate pvar object_origin field_name typ =
let update_typestate_fld ~is_assignment tenv access_loc typestate pvar object_origin field_name typ
=
match TypeState.lookup_pvar pvar typestate with match TypeState.lookup_pvar pvar typestate with
| Some _ when not is_assignment -> | Some _ ->
typestate typestate
| _ -> ( | None -> (
match AnnotatedField.get tenv field_name typ with match AnnotatedField.get tenv field_name typ with
| Some AnnotatedField.{annotated_type= field_type} -> | Some AnnotatedField.{annotated_type= field_type} ->
let range = let range =
@ -258,18 +256,20 @@ let update_typestate_fld ~is_assignment tenv access_loc typestate pvar object_or
, InferredNullability.create , InferredNullability.create
(TypeOrigin.Field {object_origin; field_name; field_type; access_loc}) ) (TypeOrigin.Field {object_origin; field_name; field_type; access_loc}) )
in in
TypeState.add ~descr:"update_typestate_fld" pvar range typestate TypeState.add ~descr:"add_field_to_typestate_if_absent" pvar range typestate
| None -> | None ->
typestate ) typestate )
(* When [is_assignment] is true, update the relevant annotations for the pvar. *) (* This does two things:
(* So what is the difference between ~node and ~original_node? I don't know. This is an artifact of refactoring of 1. The same as [convert_complex_exp_to_pvar]
very old code. Sorry, dear future supporter, if names don't make sense. *) 2. On top of this, if expr corresponds to a field access, stores this field in the typestate
let convert_complex_exp_to_pvar_and_update_typestate tenv idenv curr_pname (if not stored yet).
*)
let convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_pname
(curr_annotated_signature : AnnotatedSignature.t) ~node ~(original_node : Procdesc.Node.t) (curr_annotated_signature : AnnotatedSignature.t) ~node ~(original_node : Procdesc.Node.t)
~is_assignment exp_ typestate loc = ~is_assignment exp_ typestate loc =
L.d_with_indent ~name:"convert_complex_exp_to_pvar_and_update_typestate" L.d_with_indent ~name:"convert_complex_exp_to_pvar_and_register_field_in_typestate"
~pp_result:(fun f (exp, typestate) -> ~pp_result:(fun f (exp, typestate) ->
F.fprintf f "Exp: %a;@\nTypestate: @\n%a" Exp.pp exp TypeState.pp typestate ) F.fprintf f "Exp: %a;@\nTypestate: @\n%a" Exp.pp exp TypeState.pp typestate )
(fun () -> (fun () ->
@ -328,7 +328,7 @@ let convert_complex_exp_to_pvar_and_update_typestate tenv idenv curr_pname
let fld_name = pvar_to_str pv ^ Fieldname.to_string fn in let fld_name = pvar_to_str pv ^ Fieldname.to_string fn in
let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in
let typestate' = let typestate' =
update_typestate_fld ~is_assignment tenv loc typestate pvar inner_origin fn typ add_field_to_typestate_if_absent tenv loc typestate pvar inner_origin fn typ
in in
(Exp.Lvar pvar, typestate') (Exp.Lvar pvar, typestate')
| Exp.Lfield (_exp', fn', _) when Fieldname.is_java_outer_instance fn' -> | Exp.Lfield (_exp', fn', _) when Fieldname.is_java_outer_instance fn' ->
@ -336,7 +336,7 @@ let convert_complex_exp_to_pvar_and_update_typestate tenv idenv curr_pname
let fld_name = Fieldname.to_string fn' ^ "_" ^ Fieldname.to_string fn in let fld_name = Fieldname.to_string fn' ^ "_" ^ Fieldname.to_string fn in
let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in
let typestate' = let typestate' =
update_typestate_fld ~is_assignment tenv loc typestate pvar inner_origin fn typ add_field_to_typestate_if_absent tenv loc typestate pvar inner_origin fn typ
in in
(Exp.Lvar pvar, typestate') (Exp.Lvar pvar, typestate')
| Exp.Lvar _ | Exp.Lfield _ -> ( | Exp.Lvar _ | Exp.Lfield _ -> (
@ -345,7 +345,7 @@ let convert_complex_exp_to_pvar_and_update_typestate tenv idenv curr_pname
| Some exp_str -> | Some exp_str ->
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 typestate' = let typestate' =
update_typestate_fld ~is_assignment tenv loc typestate pvar inner_origin fn typ add_field_to_typestate_if_absent tenv loc typestate pvar inner_origin fn typ
in in
(Exp.Lvar pvar, typestate') (Exp.Lvar pvar, typestate')
| None -> | None ->
@ -358,15 +358,26 @@ let convert_complex_exp_to_pvar_and_update_typestate tenv idenv curr_pname
default ) default )
let convert_complex_exp_to_pvar tenv idenv curr_pname (* Tries to find (or create a synthetic) pvar variable name that originated the given expression.
- This can be a "normal" pvar (e.g. a local variable or field parameter).
- Additionally, this can be a "synthetic" pvar corresponding to lookups:
- pvar representing "result of a function call"
- pvar representing field access.
Such synthetic pvars are needed to store once inferred nullability to make nullsafe remember
it in future accesses (so that the next call of the same method or access to the same field
does not require the programmer to write a check.
What is the difference between ~node and ~original_node? I don't know. This is an artifact of refactoring of
very old code. Sorry, dear future supporter, if names don't make sense.
*)
let convert_complex_exp_to_pvar tenv idenv curr_pname ~is_assignment
(curr_annotated_signature : AnnotatedSignature.t) ~node ~(original_node : Procdesc.Node.t) exp (curr_annotated_signature : AnnotatedSignature.t) ~node ~(original_node : Procdesc.Node.t) exp
typestate loc = typestate loc =
L.d_with_indent ~name:"convert_complex_exp_to_pvar" ~pp_result:Exp.pp (fun () -> L.d_with_indent ~name:"convert_complex_exp_to_pvar" ~pp_result:Exp.pp (fun () ->
(* For now, we implement the function via the generic version that modifies the typestate. (* For now, we implement the function via the generic version that modifies the typestate.
*) *)
let exp, _ = let exp, _ =
convert_complex_exp_to_pvar_and_update_typestate tenv idenv curr_pname convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_pname
curr_annotated_signature ~node ~original_node ~is_assignment:false exp typestate loc curr_annotated_signature ~is_assignment ~node ~original_node exp typestate loc
in in
L.d_printfln "Disregarding updated typestate" ; L.d_printfln "Disregarding updated typestate" ;
exp ) exp )
@ -437,8 +448,8 @@ let pvar_apply instr_ref idenv tenv curr_pname curr_annotated_signature loc hand
(* handle the case where pvar is a frontend-generated program variable *) (* handle the case where pvar is a frontend-generated program variable *)
let exp = Idenv.expand_expr idenv (Exp.Var id) in let exp = Idenv.expand_expr idenv (Exp.Var id) in
match match
convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node:node' convert_complex_exp_to_pvar ~is_assignment:false tenv idenv curr_pname
~original_node:node exp typestate' loc curr_annotated_signature ~node:node' ~original_node:node exp typestate' loc
with with
| Exp.Lvar pvar' -> | Exp.Lvar pvar' ->
handle_pvar typestate' pvar' handle_pvar typestate' pvar'
@ -550,8 +561,8 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_
let set_flag expression = let set_flag expression =
let cond_e = Idenv.expand_expr_temps idenv cond_node expression in let cond_e = Idenv.expand_expr_temps idenv cond_node expression in
match match
convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node:cond_node convert_complex_exp_to_pvar ~is_assignment:false tenv idenv curr_pname
~original_node:node cond_e typestate' loc curr_annotated_signature ~node:cond_node ~original_node:node cond_e typestate' loc
with with
| Exp.Lvar pvar' -> | Exp.Lvar pvar' ->
set_nonnull pvar' set_nonnull pvar'
@ -783,8 +794,8 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
let set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check expr typestate ~descr = let set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check expr typestate ~descr =
(* Trace back to original to pvar *) (* Trace back to original to pvar *)
let pvar_expr = let pvar_expr =
convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature
~original_node expr typestate loc ~is_assignment:false ~node ~original_node expr typestate loc
in in
( if with_cond_redundant_check then ( if with_cond_redundant_check then
(* We are about to set [pvar_expr] to nonnull. But what if it already is non-null? (* We are about to set [pvar_expr] to nonnull. But what if it already is non-null?
@ -1041,8 +1052,8 @@ let typecheck_sil_call_function find_canonical_duplicate checks tenv instr_ref t
typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv node instr_ref typestate e1 loc ; tenv node instr_ref typestate e1 loc ;
let e2 = let e2 =
convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature
~original_node:node e1 typestate1 loc ~is_assignment:false ~node ~original_node:node e1 typestate1 loc
in in
(((e1, e2), t1) :: etl1, typestate1) (((e1, e2), t1) :: etl1, typestate1)
in in
@ -1102,7 +1113,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv node instr_ref typestate e loc ; tenv node instr_ref typestate e loc ;
let e', typestate' = let e', typestate' =
convert_complex_exp_to_pvar_and_update_typestate tenv idenv curr_pname convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_pname
curr_annotated_signature ~node ~original_node:node ~is_assignment:false e typestate loc curr_annotated_signature ~node ~original_node:node ~is_assignment:false e typestate loc
in in
TypeState.add_id id TypeState.add_id id
@ -1115,9 +1126,9 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
| Sil.Store {e1; typ; e2; loc} -> | Sil.Store {e1; typ; e2; loc} ->
typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv node instr_ref typestate e1 loc ; tenv node instr_ref typestate e1 loc ;
let e1', typestate1 = let e1' =
convert_complex_exp_to_pvar_and_update_typestate tenv idenv curr_pname convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node
curr_annotated_signature ~node ~original_node:node ~is_assignment:true e1 typestate loc ~original_node:node ~is_assignment:true e1 typestate loc
in in
let check_field_assign () = let check_field_assign () =
match e1 with match e1 with
@ -1126,7 +1137,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
| Some annotated_field -> | Some annotated_field ->
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_field_assignment ~nullsafe_mode tenv find_canonical_duplicate EradicateChecks.check_field_assignment ~nullsafe_mode tenv find_canonical_duplicate
curr_pdesc node instr_ref typestate1 ~expr_rhs:e2 ~field_type:typ loc field_name curr_pdesc node instr_ref typestate ~expr_rhs:e2 ~field_type:typ loc field_name
annotated_field annotated_field
(typecheck_expr ~nullsafe_mode find_canonical_duplicate calls_this checks tenv) (typecheck_expr ~nullsafe_mode find_canonical_duplicate calls_this checks tenv)
| None -> | None ->
@ -1139,12 +1150,12 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
| Exp.Lvar pvar -> | Exp.Lvar pvar ->
TypeState.add pvar TypeState.add pvar
(typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this
checks tenv node instr_ref typestate1 e2 typ TypeOrigin.OptimisticFallback loc) checks tenv node instr_ref typestate e2 typ TypeOrigin.OptimisticFallback loc)
typestate1 ~descr:"Sil.Store: Exp.Lvar case" typestate ~descr:"Sil.Store: Exp.Lvar case"
| Exp.Lfield _ -> | Exp.Lfield _ ->
typestate1 typestate
| _ -> | _ ->
typestate1 typestate
in in
check_field_assign () ; typestate2 check_field_assign () ; typestate2
(* Java `new` operators *) (* Java `new` operators *)
@ -1160,8 +1171,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv node instr_ref typestate e loc ; tenv node instr_ref typestate e loc ;
let e' = let e' =
convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature
~original_node:node e typestate loc ~is_assignment:false ~node ~original_node:node e typestate loc
in in
(* cast copies the type of the first argument *) (* cast copies the type of the first argument *)
TypeState.add_id id TypeState.add_id id

Write Preview
Loading…
Cancel
Save