From 16ed8950e91dc2167ede44a660b75c434d9e2c8c Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Fri, 6 Mar 2020 09:22:56 -0800 Subject: [PATCH] [nullsafe][BE] Log to html when TypeState is modified 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 --- infer/src/nullsafe/eradicate.ml | 4 ++- infer/src/nullsafe/typeCheck.ml | 62 +++++++++++++++++++------------- infer/src/nullsafe/typeState.ml | 19 ++++++++-- infer/src/nullsafe/typeState.mli | 9 +++-- 4 files changed, 63 insertions(+), 31 deletions(-) diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index 0ba544bbf..715d63966 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -46,7 +46,9 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct else TypeOrigin.MethodParameter (Normal param_signature) 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 let get_initial_typestate () = let typestate_empty = TypeState.empty in diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 0e3cd5756..495cb2af2 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -248,7 +248,7 @@ let update_typestate_fld ~is_assignment tenv access_loc typestate pvar object_or , InferredNullability.create (TypeOrigin.Field {object_origin; field_name; field_type; access_loc}) ) in - TypeState.add pvar range typestate + TypeState.add ~descr:"update_typestate_fld" pvar range typestate | None -> typestate ) @@ -459,7 +459,9 @@ let do_preconditions_check_not_null instr_ref tenv find_canonical_duplicate node (Some instr_ref) loc curr_pdesc ) ; let previous_origin = InferredNullability.get_origin nullability 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 -> typestate' in @@ -501,7 +503,9 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_ | Some (t, nullability) -> let previous_origin = InferredNullability.get_origin nullability 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 -> typestate1 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 checks tenv node instr_ref typestate' exp_value typ_value TypeOrigin.OptimisticFallback loc) - typestate' + typestate' ~descr:"do_map_put" | None -> 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 typestate_with_new_pvar = TypeState.add pvar range typestate in typestate_with_new_pvar + ~descr:"modelling result of Map.get() since containsKey() returned true" | None -> typestate in - let set_nonnull e' typestate2 = + let set_nonnull e' typestate2 ~descr = let handle_pvar typestate' pvar = match TypeState.lookup_pvar pvar typestate' with | 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} 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 -> typestate' 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. 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 *) let pvar_expr, modified_typestate = 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 find_canonical_duplicate curr_pdesc original_node pvar_expr typ inferred_nullability idenv linereader loc instr_ref ) ; - set_nonnull pvar_expr modified_typestate + set_nonnull pvar_expr modified_typestate ~descr in (* Assuming [expr] is a boolean, this is the branch where, according to PRUNE semantics, 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 ~f:(fun accumulated_typestate 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 | None -> typestate @@ -800,14 +805,14 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli List.fold ~init:typestate ~f:(fun accumulated_typestate 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 | None -> ( match extract_first_argument_from_instanceof expr with | Some argument -> (* ([argument] instanceof == true) implies (argument != null) *) set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:false argument - typestate + typestate ~descr:"instanceof argument in true branch" | None -> if is_from_containsKey expr then handle_containsKey_returned_true expr 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 = set_original_pvar_to_nonnull_in_typestate ~with_cond_redundant_check:true expr typestate + ~descr:"`!= null` branch" in match[@warning "-57"] c with | 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 mk_return_range () = (ret_typ, ret_ta) 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 let typestate_after_call, finally_resolved_ret = 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 -> match var with | Var.LogicalVar id -> - TypeState.remove_id id astate + TypeState.remove_id id astate ~descr:"ExitScope" | Var.ProgramVar _ -> astate ) | 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 (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks 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 -> (* skip assignment to return variable where it is an artifact of a throw instruction *) typestate @@ -1101,7 +1107,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p TypeState.add pvar (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks tenv node instr_ref typestate1 e2 typ TypeOrigin.OptimisticFallback loc) - typestate1 + typestate1 ~descr:"Sil.Store: Exp.Lvar case" | Exp.Lfield _ -> 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)], _, _) when Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array -> (* 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 *) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _) 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 (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks tenv node instr_ref typestate' e' typ TypeOrigin.OptimisticFallback loc) - typestate' + typestate' ~descr:"type cast" (* myarray.length *) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _) 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 ; TypeState.add_id id (Typ.mk (Tint Typ.IInt), InferredNullability.create TypeOrigin.ArrayLengthResult) - typestate + typestate ~descr:"array.length" (* All other builtins that are not considered above *) | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn -> 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 ( { normal_flow_typestate= normal_typestate_prev_opt ; 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 | None -> (* 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 normal_flow_typestate_prev instr 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 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 *) - 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 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} in (* Reset 'always' field for forall errors to false. *) diff --git a/infer/src/nullsafe/typeState.ml b/infer/src/nullsafe/typeState.ml index e2aea4b50..45d8b477a 100644 --- a/infer/src/nullsafe/typeState.ml +++ b/infer/src/nullsafe/typeState.ml @@ -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 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 diff --git a/infer/src/nullsafe/typeState.mli b/infer/src/nullsafe/typeState.mli index 9f693442d..32ef575ba 100644 --- a/infer/src/nullsafe/typeState.mli +++ b/infer/src/nullsafe/typeState.mli @@ -14,9 +14,11 @@ type 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 @@ -30,4 +32,5 @@ val lookup_pvar : Pvar.t -> t -> range option 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 *)