diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 99a33e8d5..b28d7c024 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -566,6 +566,24 @@ let nullable_annotation_name proc_name = "_Nullable" +let access_desc tags access_opt = + match access_opt with + | None -> + [] + | Some Last_accessed (n, _) -> + let line_str = string_of_int n in + Tags.update tags Tags.accessed_line line_str ; + ["last accessed on line " ^ line_str] + | Some Last_assigned (n, _) -> + let line_str = string_of_int n in + Tags.update tags Tags.assigned_line line_str ; + ["last assigned on line " ^ line_str] + | Some Returned_from_call _ -> + [] + | Some Initialized_automatically -> + ["initialized automatically"] + + let dereference_string proc_name deref_str value_str access_opt loc = let tags = deref_str.tags in Tags.update tags Tags.value value_str ; @@ -577,23 +595,6 @@ let dereference_string proc_name deref_str value_str access_opt loc = ; MF.monospaced_to_string value_str ; (match deref_str.value_post with Some s -> " " ^ MF.monospaced_to_string s | _ -> "") ] in - let access_desc = - match access_opt with - | None -> - [] - | Some Last_accessed (n, _) -> - let line_str = string_of_int n in - Tags.update tags Tags.accessed_line line_str ; - ["last accessed on line " ^ line_str] - | Some Last_assigned (n, _) -> - let line_str = string_of_int n in - Tags.update tags Tags.assigned_line line_str ; - ["last assigned on line " ^ line_str] - | Some Returned_from_call _ -> - [] - | Some Initialized_automatically -> - ["initialized automatically"] - in let problem_desc = let problem_str = let annotation_name = nullable_annotation_name proc_name in @@ -613,6 +614,7 @@ let dereference_string proc_name deref_str value_str access_opt loc = in [problem_str ^ " " ^ at_line tags loc] in + let access_desc = access_desc tags access_opt in {no_desc with descriptions= value_desc :: access_desc @ problem_desc; tags= !tags} @@ -889,37 +891,12 @@ let desc_return_expression_required typ_str loc = {no_desc with descriptions= [description]; tags= !tags} -let desc_retain_cycle cycle loc cycle_dotty = +let desc_retain_cycle cycle_str loc cycle_dotty = Logging.d_strln "Proposition with retain cycle:" ; let tags = Tags.create () in - let desc_retain_cycle (cycle: RetainCyclesType.t) = - let open RetainCyclesType in - let remove_old s = - match Str.split_delim (Str.regexp_string "&old_") s with [_; s'] -> s' | _ -> s - in - let do_edge index_ edge = - let index = index_ + 1 in - let from_exp_str = - match edge.rc_from.rc_node_exp with - | Exp.Lvar pvar when Pvar.equal pvar Sil.block_pvar -> - "a block capturing" - | Exp.Lvar pvar as e -> - let e_str = Exp.to_string e in - if Pvar.is_seed pvar then remove_old e_str else e_str - | _ -> - Format.sprintf "An object of type %s" - (MF.monospaced_to_string (Typ.to_string edge.rc_from.rc_node_typ)) - in - Format.sprintf "(%d) %s retaining another object via instance variable %s, " index - from_exp_str - (MF.monospaced_to_string (Typ.Fieldname.to_string edge.rc_field.rc_field_name)) - in - let cycle_str = List.mapi ~f:do_edge cycle.rc_elements in - String.concat cycle_str ~sep:" " - in let desc = - Format.sprintf "Retain cycle involving the following objects:%s %s" (desc_retain_cycle cycle) - (at_line tags loc) + Format.sprintf "Retain cycle %s involving the following objects:%s" (at_line tags loc) + cycle_str in {no_desc with descriptions= [desc]; tags= !tags; dotty= cycle_dotty} diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index 9b5a6714b..079068ebd 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -201,7 +201,7 @@ val desc_precondition_not_met : pnm_kind option -> Typ.Procname.t -> Location.t val desc_return_expression_required : string -> Location.t -> error_desc -val desc_retain_cycle : RetainCyclesType.t -> Location.t -> string option -> error_desc +val desc_retain_cycle : string -> Location.t -> string option -> error_desc val registered_observer_being_deallocated_str : string -> string @@ -223,3 +223,5 @@ val desc_unary_minus_applied_to_unsigned_expression : val desc_unsafe_guarded_by_access : Typ.Fieldname.t -> string -> Location.t -> error_desc val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Location.t -> error_desc + +val access_desc : (string, string) Base__List.Assoc.t ref -> access option -> string list diff --git a/infer/src/backend/RetainCycles.ml b/infer/src/backend/RetainCycles.ml index a862970ce..0be79ccfa 100644 --- a/infer/src/backend/RetainCycles.ml +++ b/infer/src/backend/RetainCycles.ml @@ -8,6 +8,39 @@ *) module L = Logging module F = Format +module MF = MarkupFormatter + +let desc_retain_cycle tenv (cycle: RetainCyclesType.t) = + let open RetainCyclesType in + Logging.d_strln "Proposition with retain cycle:" ; + let do_edge index_ edge = + let index = index_ + 1 in + let node = State.get_node () in + let from_exp_str = + match edge.rc_from.rc_node_exp with + | Exp.Lvar pvar when Pvar.equal pvar Sil.block_pvar -> + "a block" + | _ -> + match Errdesc.find_outermost_dereference tenv node edge.rc_from.rc_node_exp with + | Some de -> + DecompiledExp.to_string de + | None -> + Format.sprintf "(object of type %s)" (Typ.to_string edge.rc_from.rc_node_typ) + in + let inst_str inst = + let update_str_list = Localise.access_desc (ref []) (Errdesc.access_opt inst) in + if List.is_empty update_str_list then " " else ", " ^ String.concat ~sep:"," update_str_list + in + let cycle_item_str = + Format.sprintf "%s->%s" from_exp_str (Typ.Fieldname.to_string edge.rc_field.rc_field_name) + in + Format.sprintf "(%d) %s%s" index + (MF.monospaced_to_string cycle_item_str) + (inst_str edge.rc_field.rc_field_inst) + in + let cycle_str = List.mapi ~f:do_edge cycle.rc_elements in + List.fold_left cycle_str ~f:(fun acc s -> Format.sprintf "%s\n %s" acc s) ~init:"" + let get_cycle root prop = let open RetainCyclesType in @@ -66,16 +99,6 @@ let get_cycle root prop = [] -let get_retain_cycle_dotty prop_ cycle = - match prop_ with - | None -> - None - | Some Some prop_ -> - Dotty.dotty_retain_cycle_to_str prop_ cycle - | _ -> - None - - let get_var_retain_cycle prop_ = let sigma = prop_.Prop.sigma in (* returns the pvars of the first cycle we find in sigma. @@ -140,9 +163,10 @@ let cycle_has_weak_or_unretained_or_assign_field tenv cycle = do_cycle cycle.rc_elements -let exn_retain_cycle original_prop hpred cycle = - let cycle_dotty = get_retain_cycle_dotty original_prop cycle in - let desc = Errdesc.explain_retain_cycle cycle (State.get_loc ()) cycle_dotty in +let exn_retain_cycle tenv prop hpred cycle = + let retain_cycle = desc_retain_cycle tenv cycle in + let cycle_dotty = Dotty.dotty_retain_cycle_to_str prop cycle in + let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc ()) cycle_dotty in Exceptions.Retain_cycle (hpred, desc, __POS__) @@ -151,10 +175,11 @@ let report_cycle tenv hpred original_prop = only if it's empty or it has weak or unsafe_unretained fields. Otherwise we report a retain cycle. *) let remove_opt prop_ = match prop_ with Some Some p -> p | _ -> Prop.prop_emp in - match get_var_retain_cycle (remove_opt original_prop) with + let prop = remove_opt original_prop in + match get_var_retain_cycle prop with | Some cycle when not (cycle_has_weak_or_unretained_or_assign_field tenv cycle) -> RetainCyclesType.print_cycle cycle ; - Some (exn_retain_cycle original_prop hpred cycle) + Some (exn_retain_cycle tenv prop hpred cycle) | _ -> None diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 52caae24c..e1258f0be 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -786,6 +786,22 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option = res +let access_opt ?(is_nullable= false) inst = + match inst with + | Sil.Iupdate (_, ncf, n, _) -> + Some (Localise.Last_assigned (n, ncf)) + | Sil.Irearrange (_, _, n, _) -> + Some (Localise.Last_accessed (n, is_nullable)) + | Sil.Ireturn_from_call n -> + Some (Localise.Returned_from_call n) + | Sil.Ialloc when Config.curr_language_is Config.Java -> + Some Localise.Initialized_automatically + | inst -> + if verbose then + L.d_strln ("explain_dexp_access: inst is not an update " ^ Sil.inst_to_string inst) ; + None + + (** produce a description of the access from the instrumentation at position [dexp] in [prop] *) let explain_dexp_access prop dexp is_nullable = let sigma = prop.Prop.sigma in @@ -906,26 +922,12 @@ let explain_dexp_access prop dexp is_nullable = if verbose then L.d_strln ("lookup: unknown case not matched " ^ DExp.to_string de) ; None in - let access_opt = - match sexpo_to_inst (lookup dexp) with - | None -> - if verbose then - L.d_strln ("explain_dexp_access: cannot find inst of " ^ DExp.to_string dexp) ; - None - | Some Sil.Iupdate (_, ncf, n, _) -> - Some (Localise.Last_assigned (n, ncf)) - | Some Sil.Irearrange (_, _, n, _) -> - Some (Localise.Last_accessed (n, is_nullable)) - | Some Sil.Ireturn_from_call n -> - Some (Localise.Returned_from_call n) - | Some Sil.Ialloc when Config.curr_language_is Config.Java -> - Some Localise.Initialized_automatically - | Some inst -> - if verbose then - L.d_strln ("explain_dexp_access: inst is not an update " ^ Sil.inst_to_string inst) ; - None - in - access_opt + match sexpo_to_inst (lookup dexp) with + | Some inst -> + access_opt inst ~is_nullable + | None -> + if verbose then L.d_strln ("explain_dexp_access: cannot find inst of " ^ DExp.to_string dexp) ; + None let explain_dereference_access outermost_array is_nullable de_opt_ prop = @@ -1004,6 +1006,59 @@ let create_dereference_desc proc_name tenv ?(use_buckets= false) ?(outermost_arr if use_buckets then Buckets.classify_access desc access_opt' de_opt is_nullable else desc +let rec find_outermost_dereference tenv node e = + match e with + | Exp.Const _ -> + if verbose then ( + L.d_str "find_outermost_dereference: constant " ; + Sil.d_exp e ; + L.d_ln () ) ; + exp_lv_dexp tenv node e + | Exp.Var id when Ident.is_normal id -> + (* look up the normal variable declaration *) + if verbose then ( + L.d_str "find_outermost_dereference: normal var " ; + Sil.d_exp e ; + L.d_ln () ) ; + find_normal_variable_load tenv node id + | Exp.Lfield (e', _, _) -> + if verbose then ( + L.d_str "find_outermost_dereference: Lfield " ; + Sil.d_exp e ; + L.d_ln () ) ; + find_outermost_dereference tenv node e' + | Exp.Lindex (e', _) -> + if verbose then ( + L.d_str "find_outermost_dereference: Lindex " ; + Sil.d_exp e ; + L.d_ln () ) ; + find_outermost_dereference tenv node e' + | Exp.Lvar _ -> + if verbose then ( + L.d_str "find_outermost_dereference: Lvar " ; + Sil.d_exp e ; + L.d_ln () ) ; + exp_lv_dexp tenv node e + | Exp.BinOp (Binop.PlusPI, Exp.Lvar _, _) -> + if verbose then ( + L.d_str "find_outermost_dereference: Lvar+index " ; + Sil.d_exp e ; + L.d_ln () ) ; + exp_lv_dexp tenv node e + | Exp.Cast (_, e') -> + if verbose then ( + L.d_str "find_outermost_dereference: cast " ; + Sil.d_exp e ; + L.d_ln () ) ; + find_outermost_dereference tenv node e' + | _ -> + if verbose then ( + L.d_str "find_outermost_dereference: no match for " ; + Sil.d_exp e ; + L.d_ln () ) ; + None + + (** explain memory access performed by the current instruction if outermost_array is true, the outermost array access is removed if outermost_dereference is true, stop at the outermost dereference @@ -1011,58 +1066,6 @@ let create_dereference_desc proc_name tenv ?(use_buckets= false) ?(outermost_arr let explain_access_ proc_name tenv ?(use_buckets= false) ?(outermost_array= false) ?(outermost_dereference= false) ?(is_nullable= false) ?(is_premature_nil= false) deref_str prop loc = - let rec find_outermost_dereference node e = - match e with - | Exp.Const _ -> - if verbose then ( - L.d_str "find_outermost_dereference: constant " ; - Sil.d_exp e ; - L.d_ln () ) ; - exp_lv_dexp tenv node e - | Exp.Var id when Ident.is_normal id -> - (* look up the normal variable declaration *) - if verbose then ( - L.d_str "find_outermost_dereference: normal var " ; - Sil.d_exp e ; - L.d_ln () ) ; - find_normal_variable_load tenv node id - | Exp.Lfield (e', _, _) -> - if verbose then ( - L.d_str "find_outermost_dereference: Lfield " ; - Sil.d_exp e ; - L.d_ln () ) ; - find_outermost_dereference node e' - | Exp.Lindex (e', _) -> - if verbose then ( - L.d_str "find_outermost_dereference: Lindex " ; - Sil.d_exp e ; - L.d_ln () ) ; - find_outermost_dereference node e' - | Exp.Lvar _ -> - if verbose then ( - L.d_str "find_outermost_dereference: Lvar " ; - Sil.d_exp e ; - L.d_ln () ) ; - exp_lv_dexp tenv node e - | Exp.BinOp (Binop.PlusPI, Exp.Lvar _, _) -> - if verbose then ( - L.d_str "find_outermost_dereference: Lvar+index " ; - Sil.d_exp e ; - L.d_ln () ) ; - exp_lv_dexp tenv node e - | Exp.Cast (_, e') -> - if verbose then ( - L.d_str "find_outermost_dereference: cast " ; - Sil.d_exp e ; - L.d_ln () ) ; - find_outermost_dereference node e' - | _ -> - if verbose then ( - L.d_str "find_outermost_dereference: no match for " ; - Sil.d_exp e ; - L.d_ln () ) ; - None - in let find_exp_dereferenced () = match State.get_instr () with | Some Sil.Store (e, _, _, _) -> @@ -1102,7 +1105,7 @@ let explain_access_ proc_name tenv ?(use_buckets= false) ?(outermost_array= fals | Some e -> L.d_strln "Finding deref'd exp" ; let de_opt = - if outermost_dereference then find_outermost_dereference node e + if outermost_dereference then find_outermost_dereference tenv node e else exp_lv_dexp tenv node e in create_dereference_desc proc_name tenv ~use_buckets ~outermost_array ~is_nullable @@ -1270,9 +1273,6 @@ let explain_return_expression_required loc typ = Localise.desc_return_expression_required typ_str loc -(** Explain retain cycle value error *) -let explain_retain_cycle cycle loc dotty_str = Localise.desc_retain_cycle cycle loc dotty_str - (** explain a return statement missing *) let explain_return_statement_missing loc = Localise.desc_return_statement_missing loc @@ -1331,3 +1331,4 @@ let explain_null_test_after_dereference tenv exp node line loc = let warning_err loc fmt_string = L.(debug Analysis Medium) ("%a: Warning: " ^^ fmt_string) Location.pp loc + diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index 28abafa1d..776b5e897 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -101,9 +101,6 @@ val explain_frontend_warning : string -> string option -> Location.t -> Localise val explain_return_statement_missing : Location.t -> Localise.error_desc (** explain a return statement missing *) -val explain_retain_cycle : RetainCyclesType.t -> Location.t -> string option -> Localise.error_desc -(** explain a retain cycle *) - val explain_unary_minus_applied_to_unsigned_expression : Tenv.t -> Exp.t -> Typ.t -> Procdesc.Node.t -> Location.t -> Localise.error_desc (** explain unary minus applied to unsigned expression *) @@ -136,3 +133,7 @@ type pvar_off = Fpvar (* value of a pvar *) val find_with_exp : 'a Prop.t -> Exp.t -> (Pvar.t * pvar_off) option (** Find a program variable whose value is [exp] or pointing to a struct containing [exp] *) + +val find_outermost_dereference : Tenv.t -> Procdesc.Node.t -> Exp.t -> DecompiledExp.t option + +val access_opt : ?is_nullable:bool -> Sil.inst -> Localise.access option