From 725bf1ea185f17f87326910f194a667e5000f88b Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 4 Mar 2019 06:39:36 -0800 Subject: [PATCH] [Inferbo] Small preparatory changes Reviewed By: skcho Differential Revision: D14258200 fbshipit-source-id: d0822d34c --- .../bufferoverrun/bufferOverrunAnalysis.ml | 58 ++++++++++--------- .../src/bufferoverrun/bufferOverrunChecker.ml | 23 ++++---- 2 files changed, 43 insertions(+), 38 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index cc6543c95..cf4352d0a 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -26,10 +26,11 @@ module Payload = SummaryPayload.Make (struct let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun_analysis end) -type extras = - { get_proc_summary: - Typ.Procname.t -> (BufferOverrunAnalysisSummary.t * (Pvar.t * Typ.t) list) option - ; oenv: Dom.OndemandEnv.t } +type summary_and_formals = BufferOverrunAnalysisSummary.t * (Pvar.t * Typ.t) list + +type get_proc_summary_and_formals = Typ.Procname.t -> summary_and_formals option + +type extras = {get_proc_summary_and_formals: get_proc_summary_and_formals; oenv: Dom.OndemandEnv.t} module CFG = ProcCfg.NormalOneInstrPerNode @@ -141,7 +142,8 @@ module TransferFunctions = struct let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = - fun mem {pdesc; tenv; extras= {get_proc_summary; oenv= {integer_type_widths}}} node instr -> + fun mem {pdesc; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}} node + instr -> match instr with | Load (id, _, _, _) when Ident.is_none id -> mem @@ -149,7 +151,7 @@ module TransferFunctions = struct -> ( match Pvar.get_initializer_pname pvar with | Some callee_pname -> ( - match get_proc_summary callee_pname with + match get_proc_summary_and_formals callee_pname with | Some (callee_mem, _) -> let v = Dom.Mem.find (Loc.of_pvar pvar) callee_mem in Dom.Mem.add_stack (Loc.of_id id) v mem @@ -227,7 +229,7 @@ module TransferFunctions = struct in exec model_env ~ret mem | None -> ( - match get_proc_summary callee_pname with + match get_proc_summary_and_formals callee_pname with | Some (callee_exit_mem, callee_formals) -> instantiate_mem tenv integer_type_widths ret callee_formals callee_pname params mem callee_exit_mem location @@ -281,25 +283,20 @@ let get_local_decls : Procdesc.t -> local_decls = Procdesc.get_locals proc_desc |> List.fold ~init:PowLoc.empty ~f:accum_local_decls -let cached_compute_invariant_map = - let compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map = - fun pdesc tenv integer_type_widths -> - Preanal.do_preanalysis pdesc tenv ; - let cfg = CFG.from_pdesc pdesc in - let pdata = - let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in - let get_proc_summary callee_pname = - Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname - |> Option.bind ~f:(fun summary -> - Payload.of_summary summary - |> Option.map ~f:(fun payload -> - (payload, Summary.get_proc_desc summary |> Procdesc.get_pvar_formals) ) ) - in - ProcData.make pdesc tenv {get_proc_summary; oenv} - in - let initial = Init.initial_state pdata (CFG.start_node cfg) in - Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata +let compute_invariant_map : + Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> get_proc_summary_and_formals -> invariant_map = + fun pdesc tenv integer_type_widths get_proc_summary_and_formals -> + Preanal.do_preanalysis pdesc tenv ; + let cfg = CFG.from_pdesc pdesc in + let pdata = + let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in + ProcData.make pdesc tenv {get_proc_summary_and_formals; oenv} in + let initial = Init.initial_state pdata (CFG.start_node cfg) in + Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata + + +let cached_compute_invariant_map = (* Use a weak Hashtbl to prevent memory leaks (GC unnecessarily keeps invariant maps around) *) let module WeakInvMapHashTbl = Caml.Weak.Make (struct type t = Typ.Procname.t * invariant_map option @@ -318,7 +315,16 @@ let cached_compute_invariant_map = (* this should never happen *) assert false | None -> - let inv_map = compute_invariant_map pdesc tenv integer_type_widths in + let get_proc_summary_and_formals callee_pname = + Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname + |> Option.bind ~f:(fun summary -> + Payload.of_summary summary + |> Option.map ~f:(fun payload -> + (payload, Summary.get_proc_desc summary |> Procdesc.get_pvar_formals) ) ) + in + let inv_map = + compute_invariant_map pdesc tenv integer_type_widths get_proc_summary_and_formals + in WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map) ; inv_map diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 685619dcc..53debbcbd 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -265,10 +265,11 @@ let instantiate_cond : latest_prune +type checks_summary = BufferOverrunCheckerSummary.t + type get_proc_summary = Typ.Procname.t - -> (BufferOverrunAnalysisSummary.t * BufferOverrunCheckerSummary.t * (Pvar.t * Typ.t) list) - option + -> (BufferOverrunAnalysisSummary.t * (Pvar.t * Typ.t) list * checks_summary) option let check_instr : get_proc_summary @@ -306,7 +307,7 @@ let check_instr : check model_env mem cond_set | None -> ( match get_proc_summary callee_pname with - | Some (callee_mem, callee_condset, callee_formals) -> + | Some (callee_mem, callee_formals, callee_condset) -> instantiate_cond tenv integer_type_widths callee_pname callee_formals params mem callee_mem callee_condset location |> PO.ConditionSet.join cond_set @@ -398,10 +399,8 @@ let compute_checks : ~init:Checks.empty -type checks_summary = PO.ConditionSet.summary_t - -let report_errors : Tenv.t -> Summary.t -> checks -> unit = - fun tenv summary {cond_set; unused_branches; unreachable_statements} -> +let report_errors : Tenv.t -> checks -> Summary.t -> unit = + fun tenv {cond_set; unused_branches; unreachable_statements} summary -> UnusedBranches.report tenv summary unused_branches ; UnreachableStatements.report summary unreachable_statements ; let report cond trace issue_type = @@ -417,7 +416,7 @@ let report_errors : Tenv.t -> Summary.t -> checks -> unit = PO.ConditionSet.report_errors ~report cond_set -let checks_summary : BufferOverrunAnalysis.local_decls -> checks -> checks_summary = +let get_checks_summary : BufferOverrunAnalysis.local_decls -> checks -> checks_summary = fun locals Checks.({ cond_set ; unused_branches= _ (* intra-procedural *) @@ -444,14 +443,14 @@ let checker : Callbacks.proc_callback_args -> Summary.t = Option.map2 analysis_payload checker_payload ~f:(fun analysis_payload checker_payload -> ( analysis_payload - , checker_payload - , Summary.get_proc_desc summary |> Procdesc.get_pvar_formals ) ) ) + , Summary.get_proc_desc summary |> Procdesc.get_pvar_formals + , checker_payload ) ) ) in compute_checks get_proc_summary proc_desc tenv integer_type_widths cfg inv_map in - report_errors tenv summary checks ; + report_errors tenv checks summary ; let locals = BufferOverrunAnalysis.get_local_decls proc_desc in - let cond_set = checks_summary locals checks in + let cond_set = get_checks_summary locals checks in Payload.update_summary cond_set summary in NodePrinter.finish_session underlying_exit_node ;