diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 99f889d62..cc6543c95 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -26,7 +26,10 @@ module Payload = SummaryPayload.Make (struct let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun_analysis end) -type extras = {oenv: Dom.OndemandEnv.t} +type extras = + { get_proc_summary: + Typ.Procname.t -> (BufferOverrunAnalysisSummary.t * (Pvar.t * Typ.t) list) option + ; oenv: Dom.OndemandEnv.t } module CFG = ProcCfg.NormalOneInstrPerNode @@ -138,7 +141,7 @@ 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= {oenv= {integer_type_widths}}} node instr -> + fun mem {pdesc; tenv; extras= {get_proc_summary; oenv= {integer_type_widths}}} node instr -> match instr with | Load (id, _, _, _) when Ident.is_none id -> mem @@ -146,11 +149,8 @@ module TransferFunctions = struct -> ( match Pvar.get_initializer_pname pvar with | Some callee_pname -> ( - match - Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname - |> Option.bind ~f:Payload.of_summary - with - | Some callee_mem -> + match get_proc_summary 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 | None -> @@ -227,15 +227,7 @@ module TransferFunctions = struct in exec model_env ~ret mem | None -> ( - match - Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname - |> Option.bind ~f:(fun callee_summary -> - Payload.of_summary callee_summary - |> Option.map ~f:(fun payload -> - ( payload - , Summary.get_proc_desc callee_summary |> Procdesc.get_pvar_formals ) ) - ) - with + match get_proc_summary 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 @@ -296,7 +288,14 @@ let cached_compute_invariant_map = let cfg = CFG.from_pdesc pdesc in let pdata = let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in - ProcData.make pdesc tenv {oenv} + 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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 418360823..685619dcc 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -265,8 +265,14 @@ let instantiate_cond : latest_prune +type get_proc_summary = + Typ.Procname.t + -> (BufferOverrunAnalysisSummary.t * BufferOverrunCheckerSummary.t * (Pvar.t * Typ.t) list) + option + let check_instr : - Procdesc.t + get_proc_summary + -> Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.Node.t @@ -274,7 +280,7 @@ let check_instr : -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t = - fun pdesc tenv integer_type_widths node instr mem cond_set -> + fun get_proc_summary pdesc tenv integer_type_widths node instr mem cond_set -> match instr with | Sil.Load (_, exp, _, location) -> cond_set @@ -299,17 +305,7 @@ let check_instr : in check model_env mem cond_set | None -> ( - match - Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname - |> Option.bind ~f:(fun callee_summary -> - let analysis_payload = BufferOverrunAnalysis.Payload.of_summary callee_summary in - let checker_payload = Payload.of_summary callee_summary in - Option.map2 analysis_payload checker_payload - ~f:(fun analysis_payload checker_payload -> - ( analysis_payload - , checker_payload - , Summary.get_proc_desc callee_summary |> Procdesc.get_pvar_formals ) ) ) - with + match get_proc_summary callee_pname with | Some (callee_mem, callee_condset, callee_formals) -> instantiate_cond tenv integer_type_widths callee_pname callee_formals params mem callee_mem callee_condset location @@ -333,7 +329,8 @@ let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> un let check_instrs : - Procdesc.t + get_proc_summary + -> Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t @@ -342,7 +339,7 @@ let check_instrs : -> Dom.Mem.t AbstractInterpreter.State.t -> Checks.t -> Checks.t = - fun pdesc tenv integer_type_widths cfg node instrs state checks -> + fun get_proc_summary pdesc tenv integer_type_widths cfg node instrs state checks -> match state with | _ when Instrs.is_empty instrs -> checks @@ -359,13 +356,16 @@ let check_instrs : | NonBottom _ -> checks in - let cond_set = check_instr pdesc tenv integer_type_widths node instr pre checks.cond_set in + let cond_set = + check_instr get_proc_summary pdesc tenv integer_type_widths node instr pre checks.cond_set + in print_debug_info instr pre cond_set ; {checks with cond_set} let check_node : - Procdesc.t + get_proc_summary + -> Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t @@ -373,11 +373,11 @@ let check_node : -> Checks.t -> CFG.Node.t -> Checks.t = - fun pdesc tenv integer_type_widths cfg inv_map checks node -> + fun get_proc_summary pdesc tenv integer_type_widths cfg inv_map checks node -> match BufferOverrunAnalysis.extract_state (CFG.Node.id node) inv_map with | Some state -> let instrs = CFG.instrs node in - check_instrs pdesc tenv integer_type_widths cfg node instrs state checks + check_instrs get_proc_summary pdesc tenv integer_type_widths cfg node instrs state checks | _ -> checks @@ -385,14 +385,17 @@ let check_node : type checks = Checks.t let compute_checks : - Procdesc.t + get_proc_summary + -> Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> BufferOverrunAnalysis.invariant_map -> checks = - fun pdesc tenv integer_type_widths cfg inv_map -> - CFG.fold_nodes cfg ~f:(check_node pdesc tenv integer_type_widths cfg inv_map) ~init:Checks.empty + fun get_proc_summary pdesc tenv integer_type_widths cfg inv_map -> + CFG.fold_nodes cfg + ~f:(check_node get_proc_summary pdesc tenv integer_type_widths cfg inv_map) + ~init:Checks.empty type checks_summary = PO.ConditionSet.summary_t @@ -432,7 +435,20 @@ let checker : Callbacks.proc_callback_args -> Summary.t = NodePrinter.start_session ~pp_name underlying_exit_node ; let summary = let cfg = CFG.from_pdesc proc_desc in - let checks = compute_checks proc_desc tenv integer_type_widths cfg inv_map in + let checks = + let get_proc_summary callee_pname = + Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname + |> Option.bind ~f:(fun summary -> + let analysis_payload = BufferOverrunAnalysis.Payload.of_summary summary in + let checker_payload = Payload.of_summary summary in + 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 ) ) ) + in + compute_checks get_proc_summary proc_desc tenv integer_type_widths cfg inv_map + in report_errors tenv summary checks ; let locals = BufferOverrunAnalysis.get_local_decls proc_desc in let cond_set = checks_summary locals checks in