diff --git a/infer/src/biabduction/RetainCycles.ml b/infer/src/biabduction/RetainCycles.ml index 99bf16993..20c5da86a 100644 --- a/infer/src/biabduction/RetainCycles.ml +++ b/infer/src/biabduction/RetainCycles.ml @@ -213,7 +213,7 @@ let get_cycles found_cycles root tenv prop = found_cycles -(* Find all the cycles available in prop, up to a limit of 10 *) +(** 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 @@ -233,21 +233,16 @@ let exn_retain_cycle tenv cycle = Exceptions.Retain_cycle (desc, __POS__) -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 report_cycle tenv summary 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 cycles = get_retain_cycles tenv prop in RetainCyclesType.Set.iter RetainCyclesType.print_cycle cycles ; - match Summary.get pname with - | Some summary -> - 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 -> - () + 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")) ) diff --git a/infer/src/biabduction/RetainCycles.mli b/infer/src/biabduction/RetainCycles.mli index 0ae60e197..a527b7797 100644 --- a/infer/src/biabduction/RetainCycles.mli +++ b/infer/src/biabduction/RetainCycles.mli @@ -7,4 +7,4 @@ open! IStd -val report_cycle : Tenv.t -> Typ.Procname.t -> Prop.normal Prop.t -> unit +val report_cycle : Tenv.t -> Summary.t -> Prop.normal Prop.t -> unit diff --git a/infer/src/biabduction/RetainCyclesType.ml b/infer/src/biabduction/RetainCyclesType.ml index 8f19f220c..45cb9680e 100644 --- a/infer/src/biabduction/RetainCyclesType.ml +++ b/infer/src/biabduction/RetainCyclesType.ml @@ -94,7 +94,7 @@ let is_exp_null node = match node with Object obj -> Exp.is_null_literal obj.rc_from.rc_node_exp | Block _ -> false -let _retain_cycle_node_to_string (node: retain_cycle_node) = +let retain_cycle_node_to_string (node: retain_cycle_node) = Format.sprintf "%s : %s" (Exp.to_string node.rc_node_exp) (Typ.to_string node.rc_node_typ) @@ -104,22 +104,22 @@ let retain_cycle_field_to_string (field: retain_cycle_field) = (Sil.inst_to_string field.rc_field_inst) -let _retain_cycle_edge_to_string (edge: retain_cycle_edge) = +let retain_cycle_edge_to_string (edge: retain_cycle_edge) = match edge with | Object obj -> Format.sprintf "%s ->{%s}" - (_retain_cycle_node_to_string obj.rc_from) + (retain_cycle_node_to_string obj.rc_from) (retain_cycle_field_to_string obj.rc_field) | Block _ -> Format.sprintf "a block" -let _retain_cycle_to_string cycle = +let retain_cycle_to_string cycle = "Cycle= \n\t" - ^ String.concat ~sep:"->" (List.map ~f:_retain_cycle_edge_to_string cycle.rc_elements) + ^ String.concat ~sep:"->" (List.map ~f:retain_cycle_edge_to_string cycle.rc_elements) -let print_cycle cycle = Logging.d_strln (_retain_cycle_to_string cycle) +let print_cycle cycle = Logging.d_strln (retain_cycle_to_string cycle) let find_minimum_element cycle = List.reduce_exn cycle.rc_elements ~f:(fun el1 el2 -> diff --git a/infer/src/biabduction/RetainCyclesType.mli b/infer/src/biabduction/RetainCyclesType.mli index 90334a872..c6c41dfdb 100644 --- a/infer/src/biabduction/RetainCyclesType.mli +++ b/infer/src/biabduction/RetainCyclesType.mli @@ -30,9 +30,3 @@ val create_cycle : retain_cycle_edge list -> t option val pp_dotty : Format.formatter -> t -> unit val write_dotty_to_file : string -> t -> unit - -val _retain_cycle_edge_to_string : retain_cycle_edge -> string - -val _retain_cycle_node_to_string : retain_cycle_node -> string - -val _retain_cycle_to_string : t -> string diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 83d60ff23..78a11ecfe 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1908,8 +1908,8 @@ and proc_call ?dynamic_dispatch exe_env callee_summary (** perform symbolic execution for a single prop, and check for junk *) -and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), path) - : Paths.PathSet.t = +and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr + ((prop: Prop.normal Prop.t), path) : Paths.PathSet.t = let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let prop_primed_to_normal p = (* Rename primed vars with fresh normal vars, and return them *) @@ -1950,7 +1950,7 @@ and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal (* Check for retain cycles after assignments and method calls *) ( match instr with | (Sil.Store _ | Sil.Call _) when !Config.footprint -> - List.iter ~f:(RetainCycles.report_cycle tenv pname) [p] + List.iter ~f:(RetainCycles.report_cycle tenv summary) [p] | _ -> () ) ; let node_has_abstraction node = @@ -2000,7 +2000,7 @@ and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal (** {2 Lifted Abstract Transfer Functions} *) -let node handle_exn exe_env tenv proc_cfg (node: ProcCfg.Exceptional.Node.t) +let node handle_exn exe_env tenv summary proc_cfg (node: ProcCfg.Exceptional.Node.t) (pset: Paths.PathSet.t) : Paths.PathSet.t = let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) = @@ -2015,7 +2015,7 @@ let node handle_exn exe_env tenv proc_cfg (node: ProcCfg.Exceptional.Node.t) Sil.d_instr instr ; L.d_strln " due to exception" ; Paths.PathSet.from_renamed_list [(p, tr)] ) - else sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr (p, tr) + else sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr (p, tr) in Paths.PathSet.union pset2 pset1 in diff --git a/infer/src/biabduction/SymExec.mli b/infer/src/biabduction/SymExec.mli index 80eab1f0b..5d88f8a50 100644 --- a/infer/src/biabduction/SymExec.mli +++ b/infer/src/biabduction/SymExec.mli @@ -11,8 +11,8 @@ open! IStd (** Symbolic Execution *) val node : - (exn -> unit) -> Exe_env.t -> Tenv.t -> ProcCfg.Exceptional.t -> ProcCfg.Exceptional.Node.t - -> Paths.PathSet.t -> Paths.PathSet.t + (exn -> unit) -> Exe_env.t -> Tenv.t -> Summary.t -> ProcCfg.Exceptional.t + -> ProcCfg.Exceptional.Node.t -> Paths.PathSet.t -> Paths.PathSet.t (** Symbolic execution of the instructions of a node, lifted to sets of propositions. *) val instrs : diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 305f8a0e6..f6997467e 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -376,14 +376,14 @@ let instrs_get_normal_vars instrs = (** Perform symbolic execution for a node starting from an initial prop *) -let do_symbolic_execution exe_env proc_cfg handle_exn tenv (node: ProcCfg.Exceptional.Node.t) - (prop: Prop.normal Prop.t) (path: Paths.Path.t) = +let do_symbolic_execution exe_env summary proc_cfg handle_exn tenv + (node: ProcCfg.Exceptional.Node.t) (prop: Prop.normal Prop.t) (path: Paths.Path.t) = State.mark_execution_start node ; let instrs = ProcCfg.Exceptional.instrs node in (* fresh normal vars must be fresh w.r.t. instructions *) Ident.update_name_generator (instrs_get_normal_vars instrs) ; let pset = - SymExec.node handle_exn exe_env tenv proc_cfg node + SymExec.node handle_exn exe_env tenv summary proc_cfg node (Paths.PathSet.from_renamed_list [(prop, path)]) in L.d_strln ".... After Symbolic Execution ...." ; @@ -457,7 +457,9 @@ let forward_tabulate summary exe_env tenv proc_cfg wl = L.d_increase_indent 1 ; try State.reset_diverging_states_node () ; - let pset = do_symbolic_execution exe_env proc_cfg handle_exn tenv curr_node prop path in + let pset = + do_symbolic_execution exe_env summary proc_cfg handle_exn tenv curr_node prop path + in propagate_nodes_divergence tenv proc_cfg pset curr_node wl ; L.d_decrease_indent 1 ; L.d_ln ()