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

[nullsafe][BE] Log to html when TypeState is modified

Browse Source 
Summary:
These are important enough operations to be tracked in logs.
This diff also tweaks logs for the main loop processing instuctions, so
that we log instr before processing it, not the reverse

Reviewed By: artempyanykh

Differential Revision: D20282443

fbshipit-source-id: 40b8b6627
master
Mitya Lyubarskiy 5 years ago committed by Facebook Github Bot
parent 7f992bbaa9
commit 16ed8950e9
4 changed files with 63 additions and 31 deletions
Show Stats Download Patch File Download Diff File

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

@ -46,7 +46,9 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
else TypeOrigin.MethodParameter (Normal param_signature) else TypeOrigin.MethodParameter (Normal param_signature)
in in
let inferred_nullability = InferredNullability.create origin in let inferred_nullability = InferredNullability.create origin in
TypeState.add pvar (param_signature.param_annotated_type.typ, inferred_nullability) typestate TypeState.add pvar
(param_signature.param_annotated_type.typ, inferred_nullability)
typestate ~descr:"registering formal param"
in in
let get_initial_typestate () = let get_initial_typestate () =
let typestate_empty = TypeState.empty in let typestate_empty = TypeState.empty in

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

@ -248,7 +248,7 @@ 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 pvar range typestate TypeState.add ~descr:"update_typestate_fld" pvar range typestate
| None -> | None ->
typestate ) typestate )
@ -459,7 +459,9 @@ let do_preconditions_check_not_null instr_ref tenv find_canonical_duplicate node
(Some instr_ref) loc curr_pdesc ) ; (Some instr_ref) loc curr_pdesc ) ;
let previous_origin = InferredNullability.get_origin nullability in let previous_origin = InferredNullability.get_origin nullability in
let new_origin = TypeOrigin.InferredNonnull {previous_origin} in let new_origin = TypeOrigin.InferredNonnull {previous_origin} in
TypeState.add pvar (t, InferredNullability.create new_origin) typestate'' TypeState.add pvar
(t, InferredNullability.create new_origin)
typestate'' ~descr:"check_not_null function argument"
| None -> | None ->
typestate' typestate'
in in
@ -501,7 +503,9 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_
| Some (t, nullability) -> | Some (t, nullability) ->
let previous_origin = InferredNullability.get_origin nullability in let previous_origin = InferredNullability.get_origin nullability in
let new_origin = TypeOrigin.InferredNonnull {previous_origin} in let new_origin = TypeOrigin.InferredNonnull {previous_origin} in
TypeState.add pvar (t, InferredNullability.create new_origin) typestate1 TypeState.add pvar
(t, InferredNullability.create new_origin)
typestate1 ~descr:"check_state argument"
| None -> | None ->
typestate1 typestate1
in in
@ -590,7 +594,7 @@ let do_map_put call_params callee_pname tenv loc node curr_pname curr_pdesc call
(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 typestate' exp_value typ_value checks tenv node instr_ref typestate' exp_value typ_value
TypeOrigin.OptimisticFallback loc) TypeOrigin.OptimisticFallback loc)
typestate' typestate' ~descr:"do_map_put"
| None -> | None ->
typestate' ) typestate' )
| _ -> | _ ->
@ -719,10 +723,11 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
let range = (Typ.void, InferredNullability.create TypeOrigin.CallToGetKnownToContainsKey) in let range = (Typ.void, InferredNullability.create TypeOrigin.CallToGetKnownToContainsKey) in
let typestate_with_new_pvar = TypeState.add pvar range typestate in let typestate_with_new_pvar = TypeState.add pvar range typestate in
typestate_with_new_pvar typestate_with_new_pvar
~descr:"modelling result of Map.get() since containsKey() returned true"
| None -> | None ->
typestate typestate
in in
let set_nonnull e' typestate2 = let set_nonnull e' typestate2 ~descr =
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) -> | Some (t, current_nullability) ->
@ -731,7 +736,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
{previous_origin= InferredNullability.get_origin current_nullability} {previous_origin= InferredNullability.get_origin current_nullability}
in in
let new_nullability = InferredNullability.create new_origin in let new_nullability = InferredNullability.create new_origin in
TypeState.add pvar (t, new_nullability) typestate' TypeState.add pvar (t, new_nullability) typestate' ~descr
| None -> | None ->
typestate' typestate'
in in
@ -746,7 +751,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
Optionally, if this was already non-nullable, emit a corresponding condition redudant issue. Optionally, if this was already non-nullable, emit a corresponding condition redudant issue.
Returns the updated typestate. Returns the updated typestate.
*) *)
let set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check expr typestate = 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, modified_typestate = let pvar_expr, modified_typestate =
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 ~node
@ -765,7 +770,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
EradicateChecks.check_condition_for_redundancy ~is_always_true:true_branch tenv EradicateChecks.check_condition_for_redundancy ~is_always_true:true_branch tenv
find_canonical_duplicate curr_pdesc original_node pvar_expr typ inferred_nullability idenv find_canonical_duplicate curr_pdesc original_node pvar_expr typ inferred_nullability idenv
linereader loc instr_ref ) ; linereader loc instr_ref ) ;
set_nonnull pvar_expr modified_typestate set_nonnull pvar_expr modified_typestate ~descr
in in
(* Assuming [expr] is a boolean, this is the branch where, according to PRUNE semantics, (* Assuming [expr] is a boolean, this is the branch where, according to PRUNE semantics,
We've just ensured that [expr] == false. We've just ensured that [expr] == false.
@ -781,7 +786,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
List.fold ~init:typestate List.fold ~init:typestate
~f:(fun accumulated_typestate argument -> ~f:(fun accumulated_typestate argument ->
set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:false argument set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:false argument
accumulated_typestate ) accumulated_typestate ~descr:"@TrueOnNull-proc argument in false branch" )
arguments arguments
| None -> | None ->
typestate typestate
@ -800,14 +805,14 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
List.fold ~init:typestate List.fold ~init:typestate
~f:(fun accumulated_typestate argument -> ~f:(fun accumulated_typestate argument ->
set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:false argument set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:false argument
accumulated_typestate ) accumulated_typestate ~descr:"@FalseOnNull-proc argument in false branch" )
arguments arguments
| None -> ( | None -> (
match extract_first_argument_from_instanceof expr with match extract_first_argument_from_instanceof expr with
| Some argument -> | Some argument ->
(* ([argument] instanceof <anything> == true) implies (argument != null) *) (* ([argument] instanceof <anything> == true) implies (argument != null) *)
set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:false argument set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:false argument
typestate typestate ~descr:"instanceof argument in true branch"
| None -> | None ->
if is_from_containsKey expr then handle_containsKey_returned_true expr typestate if is_from_containsKey expr then handle_containsKey_returned_true expr typestate
else typestate ) else typestate )
@ -818,6 +823,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
*) *)
let handle_object_not_equal_null expr typestate = let handle_object_not_equal_null expr typestate =
set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:true expr typestate set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:true expr typestate
~descr:"`!= null` branch"
in in
match[@warning "-57"] c with match[@warning "-57"] c with
| Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), expr) | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), expr)
@ -1033,7 +1039,7 @@ let typecheck_sil_call_function find_canonical_duplicate checks tenv instr_ref t
let do_return (ret_ta, ret_typ) typestate' = let do_return (ret_ta, ret_typ) typestate' =
let mk_return_range () = (ret_typ, ret_ta) 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' ~descr:"typecheck_sil_call_function"
in in
let typestate_after_call, finally_resolved_ret = let typestate_after_call, finally_resolved_ret =
calc_typestate_after_call find_canonical_duplicate calls_this checks tenv idenv instr_ref calc_typestate_after_call find_canonical_duplicate calls_this checks tenv idenv instr_ref
@ -1058,7 +1064,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
List.fold_right vars ~init:typestate ~f:(fun var astate -> List.fold_right vars ~init:typestate ~f:(fun var astate ->
match var with match var with
| Var.LogicalVar id -> | Var.LogicalVar id ->
TypeState.remove_id id astate TypeState.remove_id id astate ~descr:"ExitScope"
| Var.ProgramVar _ -> | Var.ProgramVar _ ->
astate ) astate )
| Sil.Metadata (Abstract _ | Nullify _ | Skip | VariableLifetimeBegins _) -> | Sil.Metadata (Abstract _ | Nullify _ | Skip | VariableLifetimeBegins _) ->
@ -1073,7 +1079,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
TypeState.add_id id TypeState.add_id id
(typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv node instr_ref typestate' e' typ TypeOrigin.OptimisticFallback loc) tenv node instr_ref typestate' e' typ TypeOrigin.OptimisticFallback loc)
typestate' ~descr:"Sil.Load" typestate'
| Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Exn _} when is_return pvar -> | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Exn _} when is_return pvar ->
(* skip assignment to return variable where it is an artifact of a throw instruction *) (* skip assignment to return variable where it is an artifact of a throw instruction *)
typestate typestate
@ -1101,7 +1107,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
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 typestate1 e2 typ TypeOrigin.OptimisticFallback loc)
typestate1 typestate1 ~descr:"Sil.Store: Exp.Lvar case"
| Exp.Lfield _ -> | Exp.Lfield _ ->
typestate1 typestate1
| _ -> | _ ->
@ -1112,7 +1118,9 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
| Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], _, _) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], _, _)
when Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array -> when Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array ->
(* new never returns null *) (* new never returns null *)
TypeState.add_id id (typ, InferredNullability.create TypeOrigin.New) typestate TypeState.add_id id
(typ, InferredNullability.create TypeOrigin.New)
typestate ~descr:"new() operator"
(* Type cast *) (* Type cast *)
| Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _)
when Procname.equal pn BuiltinDecl.__cast -> when Procname.equal pn BuiltinDecl.__cast ->
@ -1126,7 +1134,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
TypeState.add_id id TypeState.add_id id
(typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv node instr_ref typestate' e' typ TypeOrigin.OptimisticFallback loc) tenv node instr_ref typestate' e' typ TypeOrigin.OptimisticFallback loc)
typestate' typestate' ~descr:"type cast"
(* myarray.length *) (* myarray.length *)
| 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 Procname.equal pn BuiltinDecl.__get_array_length -> when Procname.equal pn BuiltinDecl.__get_array_length ->
@ -1142,7 +1150,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
curr_pdesc node instr_ref array_exp DereferenceRule.ArrayLengthAccess ta loc ; curr_pdesc node instr_ref array_exp DereferenceRule.ArrayLengthAccess ta loc ;
TypeState.add_id id TypeState.add_id id
(Typ.mk (Tint Typ.IInt), InferredNullability.create TypeOrigin.ArrayLengthResult) (Typ.mk (Tint Typ.IInt), InferredNullability.create TypeOrigin.ArrayLengthResult)
typestate typestate ~descr:"array.length"
(* All other builtins that are not considered above *) (* All other builtins that are not considered above *)
| 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 other builtins *) typestate (* skip other builtins *)
@ -1214,6 +1222,10 @@ let typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc find_canon
let fold_instruction let fold_instruction
( { normal_flow_typestate= normal_typestate_prev_opt ( { normal_flow_typestate= normal_typestate_prev_opt
; exception_flow_typestates= exception_flow_typestates_prev } as prev_result ) instr = ; exception_flow_typestates= exception_flow_typestates_prev } as prev_result ) instr =
if Config.write_html then
L.d_printfln "-----------------------------\nTypecking instr: %a@\n"
(Sil.pp_instr ~print_types:true Pp.text)
instr ;
match normal_typestate_prev_opt with match normal_typestate_prev_opt with
| None -> | None ->
(* no input typestate - abort typechecking and propagate the current result *) (* no input typestate - abort typechecking and propagate the current result *)
@ -1228,17 +1240,19 @@ let typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc find_canon
find_canonical_duplicate annotated_signature instr_ref linereader find_canonical_duplicate annotated_signature instr_ref linereader
normal_flow_typestate_prev instr normal_flow_typestate_prev instr
in in
if is_noreturn_instruction instr then {prev_result with normal_flow_typestate= None} if Config.write_html then
L.d_printfln "New state: @\n%a@\n" TypeState.pp normal_flow_typestate ;
if is_noreturn_instruction instr then (
L.d_strln "Found no return; aborting flow" ;
{prev_result with normal_flow_typestate= None} )
else else
let exception_flow_typestates = let exception_flow_typestates =
if can_instrunction_throw tenv node instr then if can_instrunction_throw tenv node instr then (
(* add the typestate after this instruction to the list of exception typestates *) (* add the typestate after this instruction to the list of exception typestates *)
normal_flow_typestate :: exception_flow_typestates_prev L.d_strln "Throwable instruction: adding the typestate to exception list" ;
normal_flow_typestate :: exception_flow_typestates_prev )
else exception_flow_typestates_prev else exception_flow_typestates_prev
in in
if Config.write_html then (
L.d_printfln "instr: %a@\n" (Sil.pp_instr ~print_types:true Pp.text) instr ;
L.d_printfln "new state:@\n%a@\n" TypeState.pp normal_flow_typestate ) ;
{normal_flow_typestate= Some normal_flow_typestate; exception_flow_typestates} {normal_flow_typestate= Some normal_flow_typestate; exception_flow_typestates}
in in
(* Reset 'always' field for forall errors to false. *) (* Reset 'always' field for forall errors to false. *)

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

@ -63,8 +63,21 @@ let lookup_id id typestate = M.find_opt (Exp.Var id) typestate
let lookup_pvar pvar typestate = M.find_opt (Exp.Lvar pvar) typestate let lookup_pvar pvar typestate = M.find_opt (Exp.Lvar pvar) typestate
let add_id id range typestate = M.add (Exp.Var id) range typestate let add_id id range typestate ~descr =
( if Config.write_html then
let _, nullability = range in
L.d_printfln "Setting %a to Id %a: %s" InferredNullability.pp nullability Ident.pp id descr ) ;
M.add (Exp.Var id) range typestate
let add pvar range typestate = M.add (Exp.Lvar pvar) range typestate
let remove_id id typestate = M.remove (Exp.Var id) typestate let add pvar range typestate ~descr =
( if Config.write_html then
let _, nullability = range in
L.d_printfln "Setting %a to Pvar %a: %s" InferredNullability.pp nullability
Pvar.pp_value_non_verbose pvar descr ) ;
M.add (Exp.Lvar pvar) range typestate
let remove_id id typestate ~descr =
if Config.write_html then L.d_printfln "Removing Id %a from typestate: %s" Ident.pp id descr ;
M.remove (Exp.Var id) typestate

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

@ -14,9 +14,11 @@ type t
type range = Typ.t * InferredNullability.t type range = Typ.t * InferredNullability.t
val add_id : Ident.t -> range -> t -> t val add_id : Ident.t -> range -> t -> descr:string -> t
(** [descr] is for debug logs only *)
val add : Pvar.t -> range -> t -> t val add : Pvar.t -> range -> t -> descr:string -> t
(** [descr] is for debug logs only *)
val empty : t val empty : t
@ -30,4 +32,5 @@ val lookup_pvar : Pvar.t -> t -> range option
val pp : Format.formatter -> t -> unit val pp : Format.formatter -> t -> unit
val remove_id : Ident.t -> t -> t val remove_id : Ident.t -> t -> descr:string -> t
(** [descr] is for debug logs only *)

Write Preview
Loading…
Cancel
Save