diff --git a/infer/src/IR/Errlog.ml b/infer/src/IR/Errlog.ml index a83394e84..a60bc019d 100644 --- a/infer/src/IR/Errlog.ml +++ b/infer/src/IR/Errlog.ml @@ -249,7 +249,13 @@ let log_issue procname err_kind err_log loc (node_id, node_key) session ltr ?lin | _ -> false in - let exn_developer = Exceptions.equal_visibility error.visibility Exceptions.Exn_developer in + let report_developer_exn exn = + match exn with Exceptions.Dummy_exception _ -> false | _ -> true + in + let exn_developer = + Exceptions.equal_visibility error.visibility Exceptions.Exn_developer + && report_developer_exn exn + in let should_report = Exceptions.equal_visibility error.visibility Exceptions.Exn_user || Config.developer_mode && exn_developer diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 51c4a66d6..d1919897a 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -67,6 +67,8 @@ exception Condition_always_true_false of Localise.error_desc * bool * L.ocaml_po exception Custom_error of string * Localise.error_desc +exception Dummy_exception of Localise.error_desc + exception Dangling_pointer_dereference of PredSymb.dangling_kind option * Localise.error_desc * L.ocaml_pos @@ -115,7 +117,7 @@ exception Precondition_not_found of Localise.error_desc * L.ocaml_pos exception Precondition_not_met of Localise.error_desc * L.ocaml_pos -exception Retain_cycle of Sil.hpred * Localise.error_desc * L.ocaml_pos +exception Retain_cycle of Localise.error_desc * L.ocaml_pos exception Registered_observer_being_deallocated of Localise.error_desc * L.ocaml_pos @@ -272,6 +274,14 @@ let recognize_exception exn = ; severity= High ; kind= None ; category= Checker } + | Dummy_exception desc -> + { name= IssueType.from_string "Analysis stops" + ; description= desc + ; ocaml_pos= None + ; visibility= Exn_developer + ; severity= Low + ; kind= Some Kinfo + ; category= Checker } | Dangling_pointer_dereference (dko, desc, ocaml_pos) -> let visibility = match dko with @@ -494,7 +504,7 @@ let recognize_exception exn = ; kind= Some Kwarning ; category= Nocat } (* always a warning *) - | Retain_cycle (_, desc, ocaml_pos) -> + | Retain_cycle (desc, ocaml_pos) -> { name= IssueType.retain_cycle ; description= desc ; ocaml_pos= Some ocaml_pos diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 6fae2ee0c..c8a3213d2 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -65,6 +65,8 @@ exception Condition_always_true_false of Localise.error_desc * bool * Logging.oc exception Custom_error of string * Localise.error_desc +exception Dummy_exception of Localise.error_desc + exception Dangling_pointer_dereference of PredSymb.dangling_kind option * Localise.error_desc * Logging.ocaml_pos @@ -118,7 +120,7 @@ exception Precondition_not_found of Localise.error_desc * Logging.ocaml_pos exception Precondition_not_met of Localise.error_desc * Logging.ocaml_pos -exception Retain_cycle of Sil.hpred * Localise.error_desc * Logging.ocaml_pos +exception Retain_cycle of Localise.error_desc * Logging.ocaml_pos exception Registered_observer_being_deallocated of Localise.error_desc * Logging.ocaml_pos diff --git a/infer/src/backend/RetainCycles.ml b/infer/src/backend/RetainCycles.ml index 210898253..87e51a3aa 100644 --- a/infer/src/backend/RetainCycles.ml +++ b/infer/src/backend/RetainCycles.ml @@ -18,11 +18,11 @@ let desc_retain_cycle tenv (cycle: RetainCyclesType.t) = let index = index_ + 1 in let node = State.get_node () in let from_exp_str edge_obj = - match Errdesc.find_outermost_dereference tenv node edge_obj.rc_from.rc_node_exp with - | Some de -> + ignore (Errdesc.find_outermost_dereference tenv node edge_obj.rc_from.rc_node_exp) ; + (* | Some de -> DecompiledExp.to_string de - | None -> - Format.sprintf "(object of type %s)" (Typ.to_string edge_obj.rc_from.rc_node_typ) + | None -> TODO (T26707784): fix issues with DecompiledExp.to_string *) + Format.sprintf "(object of type %s)" (Typ.to_string edge_obj.rc_from.rc_node_typ) in let location_str = match edge with @@ -168,26 +168,24 @@ let get_cycles found_cycles root tenv prop = | _ -> found_cycles in - L.d_strln "Looking for cycle with root expression: " ; - Sil.d_hpred root ; - L.d_strln "" ; match root with - | Sil.Hpointsto (e_root, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) -> + | Sil.Hpointsto (e_root, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) when Sil.is_objc_object root -> let se_root = {rc_node_exp= e_root; rc_node_typ= te} in (* start dfs with empty path and expr pointing to root *) dfs ~found_cycles ~root_node:se_root ~from_node:se_root ~rev_path:[] ~fields:fl ~visited:[] | _ -> - L.d_strln "Root exp is not an allocated object. No cycle found" ; found_cycles -(* Find all the cycles available with root hpred, up to a limit of 10 *) -let get_retain_cycles hpred tenv prop_ = - try get_cycles RetainCyclesType.Set.empty hpred tenv prop_ with Max_retain_cycles cycles -> - cycles +(* Find all the cycles available in prop, up to a limit of 10 *) +let get_retain_cycles tenv prop = + let get_retain_cycles_with_root acc_set root = get_cycles acc_set root tenv prop in + let sigma = prop.Prop.sigma in + try List.fold ~f:get_retain_cycles_with_root sigma ~init:RetainCyclesType.Set.empty + with Max_retain_cycles cycles -> cycles -let exn_retain_cycle tenv hpred cycle = +let exn_retain_cycle tenv cycle = let retain_cycle = desc_retain_cycle tenv cycle in let cycle_dotty = Format.asprintf "%a" RetainCyclesType.pp_dotty cycle in if Config.debug_mode then ( @@ -196,23 +194,24 @@ let exn_retain_cycle tenv hpred cycle = let rc_dotty_file = Filename.temp_file ~in_dir:rc_dotty_dir "rc" ".dot" in RetainCyclesType.write_dotty_to_file rc_dotty_file cycle ) ; let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc ()) (Some cycle_dotty) in - Exceptions.Retain_cycle (hpred, desc, __POS__) + Exceptions.Retain_cycle (desc, __POS__) -let report_cycle tenv pname hpred original_prop = +let report_cycle tenv pname prop = (* When there is a cycle in objc we ignore it 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 - let prop = remove_opt original_prop in - let cycles = get_retain_cycles hpred tenv prop in + let cycles = get_retain_cycles tenv prop in RetainCyclesType.Set.iter RetainCyclesType.print_cycle cycles ; match Specs.get_summary pname with | Some summary -> - RetainCyclesType.Set.iter - (fun cycle -> - let exn = exn_retain_cycle tenv hpred cycle in - Reporting.log_error summary exn ) - cycles + if RetainCyclesType.Set.cardinal cycles > 0 then ( + RetainCyclesType.Set.iter + (fun cycle -> + let exn = exn_retain_cycle tenv cycle in + Reporting.log_error summary exn ) + cycles ; + (* we report the retain cycles above but need to raise an exception as well to stop the analysis *) + raise (Exceptions.Dummy_exception (Localise.verbatim_desc "retain cycle found")) ) | None -> () diff --git a/infer/src/backend/RetainCycles.mli b/infer/src/backend/RetainCycles.mli index 876617d7e..eababcae8 100644 --- a/infer/src/backend/RetainCycles.mli +++ b/infer/src/backend/RetainCycles.mli @@ -9,5 +9,4 @@ open! IStd -val report_cycle : - Tenv.t -> Typ.Procname.t -> Sil.hpred -> Prop.normal Prop.t option option -> unit +val report_cycle : Tenv.t -> Typ.Procname.t -> Prop.normal Prop.t -> unit diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 390b7a131..bf16e41bc 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1003,7 +1003,7 @@ let check_observer_is_unsubscribed_deallocation tenv prop e = () -let check_junk ?original_prop pname tenv prop = +let check_junk pname tenv prop = let leaks_reported = ref [] in let remove_junk_once fp_part fav_root sigma = let id_considered_reachable = @@ -1096,9 +1096,7 @@ let check_junk ?original_prop pname tenv prop = | Some PredSymb.Awont_leak, Rmemory _ -> (true, exn_leak) | Some _, Rmemory Mobjc -> - RetainCycles.report_cycle tenv pname hpred original_prop ; (true, exn_leak) - (* we report now inside RetainCycles, here we ignore the leak *) | (Some _, Rmemory Mnew | Some _, Rmemory Mnew_array) when Language.curr_language_is Clang -> (is_none ml_bucket_opt, exn_leak) @@ -1112,13 +1110,6 @@ let check_junk ?original_prop pname tenv prop = (false, exn_leak) | Some _, Rlock -> (false, exn_leak) - | _ when Sil.is_objc_object hpred -> - (* When it's a cycle and it is an Objective-C object then - we have a retain cycle. Objc object may not have the - Mobjc qualifier when added in footprint doing abduction *) - RetainCycles.report_cycle tenv pname hpred original_prop ; - (true, exn_leak) - (* we report now inside RetainCycles, here we ignore the leak *) | _ -> (Language.curr_language_is Java, exn_leak) in @@ -1173,16 +1164,16 @@ let check_junk ?original_prop pname tenv prop = (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *) -let abstract_junk ?original_prop pname tenv prop = +let abstract_junk pname tenv prop = Absarray.array_abstraction_performed := false ; - check_junk ~original_prop pname tenv prop + check_junk pname tenv prop (** Remove redundant elements in an array, and check for junk afterwards *) let remove_redundant_array_elements pname tenv prop = Absarray.array_abstraction_performed := false ; let prop' = Absarray.remove_redundant_elements tenv prop in - check_junk ~original_prop:(Some prop) pname tenv prop' + check_junk pname tenv prop' let abstract_prop pname tenv ~(rename_primed: bool) ~(from_abstract_footprint: bool) p = @@ -1197,7 +1188,7 @@ let abstract_prop pname tenv ~(rename_primed: bool) ~(from_abstract_footprint: b let abs_p = abs_rules_apply tenv array_abs_p in let abs_p = abstract_gc tenv abs_p in (* abstraction might enable more gc *) - let abs_p = check_junk ~original_prop:(Some p) pname tenv abs_p in + let abs_p = check_junk pname tenv abs_p in let ren_abs_p = if rename_primed then Prop.prop_rename_primed_footprint_vars tenv abs_p else abs_p in diff --git a/infer/src/backend/abs.mli b/infer/src/backend/abs.mli index d0da6a28a..37c2452ac 100644 --- a/infer/src/backend/abs.mli +++ b/infer/src/backend/abs.mli @@ -18,9 +18,7 @@ type rules val abstract : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Abstract a proposition. *) -val abstract_junk : - ?original_prop:Prop.normal Prop.t -> Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t - -> Prop.normal Prop.t +val abstract_junk : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 1a5cb5e34..f18f90656 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1032,7 +1032,11 @@ let execute_store ?(report_deref_errors= true) pname pdesc tenv lhs_exp typ rhs_ let prop = Attribute.replace_objc_null tenv prop n_lhs_exp n_rhs_exp in let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in - List.rev (List.fold ~f:(execute_store_ pdesc tenv n_rhs_exp) ~init:[] iter_list) + let prop_list = + List.rev (List.fold ~f:(execute_store_ pdesc tenv n_rhs_exp) ~init:[] iter_list) + in + if !Config.footprint then List.iter ~f:(RetainCycles.report_cycle tenv pname) prop_list ; + prop_list with Rearrange.ARRAY_ACCESS -> if Int.equal Config.array_level 0 then assert false else [prop_] @@ -1791,7 +1795,7 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), (* but force them into either branch *) p' | _ -> - check_deallocate_static_memory (Abs.abstract_junk ~original_prop:p pname tenv p') + check_deallocate_static_memory (Abs.abstract_junk pname tenv p') in L.d_str "Instruction " ; Sil.d_instr instr ; diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index b2ca5aa34..d3f16196b 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -1236,7 +1236,7 @@ let prop_pure_to_footprint tenv (p: 'a Prop.t) : Prop.normal Prop.t = (** post-process the raw result of a function call *) -let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc results = +let exe_call_postprocess tenv ret_id trace_call caller_pname callee_pname callee_attrs loc results = let filter_valid_res = function Invalid_res _ -> false | Valid_res _ -> true in let valid_res0, invalid_res0 = List.partition_tf ~f:filter_valid_res results in let valid_res = @@ -1366,6 +1366,10 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re List.iter ~f:print_pi (List.map ~f:fst cover) ; List.concat_map ~f:snd cover ) in + if !Config.footprint then + List.iter + ~f:(fun (prop, _) -> RetainCycles.report_cycle tenv caller_pname prop) + res_with_path_idents ; trace_call CR_success ; let res = List.map @@ -1416,4 +1420,5 @@ let exe_function_call callee_summary tenv ret_id_opt caller_pdesc callee_pname l formal_params in let results = List.map ~f:exe_one_spec spec_list in - exe_call_postprocess tenv ret_id_opt trace_call callee_pname callee_attrs loc results + exe_call_postprocess tenv ret_id_opt trace_call caller_pname callee_pname callee_attrs loc + results diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index 8ed66a57e..0f1ea6993 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/infer/tests/codetoanalyze/objc/errors/issues.exp @@ -2,8 +2,8 @@ codetoanalyze/objc/errors/field_superclass/field.c, field_superclass_main, 3, RE codetoanalyze/objc/errors/global_const/global_const.m, SimpleRoot_doSomethingBadWithDict:andString:, 3, NULL_DEREFERENCE, ERROR, [start of procedure doSomethingBadWithDict:andString:,Message stringByAppendingString: with receiver nil returns nil.] codetoanalyze/objc/errors/global_const/global_const.m, SimpleRoot_doSomethingOkWithDict:andString:, 3, NULL_DEREFERENCE, ERROR, [start of procedure doSomethingOkWithDict:andString:,Message stringByAppendingString: with receiver nil returns nil.] codetoanalyze/objc/errors/initialization/compound_literal.c, init_with_compound_literal, 2, DIVIDE_BY_ZERO, ERROR, [start of procedure init_with_compound_literal()] -codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m, testCycle, 3, RETAIN_CYCLE, ERROR, [start of procedure testCycle(),start of procedure init,return from a call to CADisplay_init] -codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleStaticVar.m, RetainCSVycleStaticVar, 2, RETAIN_CYCLE, ERROR, [start of procedure RetainCSVycleStaticVar(),start of procedure init,return from a call to RetainCSV_init,start of procedure foo,return from a call to RetainCSV_foo] +codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m, CADisplay_init, 1, RETAIN_CYCLE, ERROR, [start of procedure init] +codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleStaticVar.m, RetainCSV_foo, 13, RETAIN_CYCLE, ERROR, [start of procedure foo] codetoanalyze/objc/errors/npe/null_returned_by_method.m, NullReturnedByMethodA_test1, 1, NULL_DEREFERENCE, ERROR, [start of procedure test1,start of procedure test,return from a call to NullReturnedByMethodA_test] codetoanalyze/objc/errors/procdescs/main.c, ProcdescMain, 3, MEMORY_LEAK, ERROR, [start of procedure ProcdescMain(),Skipping plusX:andY:: function or method not found] codetoanalyze/objc/errors/procdescs/main.c, call_nslog, 3, MEMORY_LEAK, ERROR, [start of procedure call_nslog(),Skipping NSLog(): function or method not found] @@ -30,12 +30,12 @@ codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, field_set_correc codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, implicit_expr_set_correctly, 3, DIVIDE_BY_ZERO, ERROR, [start of procedure implicit_expr_set_correctly()] codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, point_coords_set_correctly, 2, DIVIDE_BY_ZERO, ERROR, [start of procedure point_coords_set_correctly()] codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlockCapturedVar.m, LinkResolver_test_bad, 3, RETAIN_CYCLE, ERROR, [start of procedure test_bad] -codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, call_retain_self_in_block_cycle, 2, RETAIN_CYCLE, ERROR, [start of procedure call_retain_self_in_block_cycle(),start of procedure retain_self_in_block,return from a call to RCBlock_retain_self_in_block] -codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 5, RETAIN_CYCLE, ERROR, [start of procedure retain_a_in_block_cycle()] -codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 5, RETAIN_CYCLE, ERROR, [start of procedure retain_a_in_block_cycle()] -codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCyclePropertyInProtocol.m, main_bad, 2, RETAIN_CYCLE, ERROR, [start of procedure main_bad(),start of procedure loadViewBad,return from a call to MyCustomViewController_loadViewBad] +codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, RCBlock_retain_self_in_block, 1, RETAIN_CYCLE, ERROR, [start of procedure retain_self_in_block] +codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, objc_blockretain_a_in_block_cycle_3, 1, RETAIN_CYCLE, ERROR, [start of procedure block] +codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 4, RETAIN_CYCLE, ERROR, [start of procedure retain_a_in_block_cycle()] +codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCyclePropertyInProtocol.m, MyCustomViewController_loadViewBad, 3, RETAIN_CYCLE, ERROR, [start of procedure loadViewBad] codetoanalyze/objc/errors/memory_leaks_benchmark/retain_cycle.m, strongcycle, 6, RETAIN_CYCLE, ERROR, [start of procedure strongcycle()] -codetoanalyze/objc/errors/memory_leaks_benchmark/retain_cycle2.m, strongcycle2, 4, RETAIN_CYCLE, ERROR, [start of procedure strongcycle2(),start of procedure init,return from a call to Parent_init,start of procedure init,return from a call to Child_init,start of procedure setChild:,return from a call to Parent_setChild:,start of procedure setParent:,return from a call to Child_setParent:] +codetoanalyze/objc/errors/memory_leaks_benchmark/retain_cycle2.m, strongcycle2, 4, RETAIN_CYCLE, ERROR, [start of procedure strongcycle2(),start of procedure init,return from a call to Parent_init,start of procedure init,return from a call to Child_init,start of procedure setChild:,return from a call to Parent_setChild:] codetoanalyze/objc/errors/npe/UpdateDict.m, add_nil_in_dict, 10, NULL_DEREFERENCE, ERROR, [start of procedure add_nil_in_dict(),Skipping dictionaryWithObjectsAndKeys:: function or method not found] codetoanalyze/objc/errors/npe/UpdateDict.m, add_nil_to_array, 4, NULL_DEREFERENCE, ERROR, [start of procedure add_nil_to_array()] codetoanalyze/objc/errors/npe/UpdateDict.m, insert_nil_in_array, 4, NULL_DEREFERENCE, ERROR, [start of procedure insert_nil_in_array()]