diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 8bb7169ce..ec015fa43 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -25,11 +25,12 @@ module Payload = SummaryPayload.Make (struct let field = Payloads.Fields.buffer_overrun_analysis end) -type summary_and_formals = BufferOverrunAnalysisSummary.t * (Pvar.t * Typ.t) list +type get_formals = Procname.t -> (Pvar.t * Typ.t) list option -type get_proc_summary_and_formals = Procname.t -> summary_and_formals option - -type extras = {get_proc_summary_and_formals: get_proc_summary_and_formals; oenv: OndemandEnv.t} +type extras = + { get_summary: BufferOverrunAnalysisSummary.get_summary + ; get_formals: get_formals + ; oenv: OndemandEnv.t } module CFG = ProcCfg.NormalOneInstrPerNode @@ -223,7 +224,7 @@ module TransferFunctions = struct let reachable_locs = Dom.Mem.get_reachable_locs_from [] (PowLoc.singleton loc) from_mem in PowLoc.fold copy reachable_locs to_mem in - fun tenv get_proc_summary_and_formals exp mem -> + fun tenv get_summary exp mem -> Option.value_map (Exp.get_java_class_initializer tenv exp) ~default:mem ~f:(fun (clinit_pname, pvar, fn, field_typ) -> match field_typ.Typ.desc with @@ -231,8 +232,7 @@ module TransferFunctions = struct (* It copies all of the reachable values when the contents of the field are commonly used as immutable, e.g., values of enum. Otherwise, it copies only the size of static final array. *) - Option.value_map (get_proc_summary_and_formals clinit_pname) ~default:mem - ~f:(fun (clinit_mem, _) -> + Option.value_map (get_summary clinit_pname) ~default:mem ~f:(fun clinit_mem -> let field_loc = Loc.append_field ~typ:field_typ (Loc.of_pvar pvar) ~fn in if is_known_java_static_field fn then copy_reachable_locs_from field_loc ~from_mem:clinit_mem ~to_mem:mem @@ -266,7 +266,7 @@ module TransferFunctions = struct let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = - fun mem {summary; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}} node + fun mem {summary; tenv; extras= {get_summary; get_formals; oenv= {integer_type_widths}}} node instr -> match instr with | Load {id} when Ident.is_none id -> @@ -275,8 +275,8 @@ module TransferFunctions = struct when Pvar.is_compile_constant pvar || Pvar.is_ice pvar -> ( match Pvar.get_initializer_pname pvar with | Some callee_pname -> ( - match get_proc_summary_and_formals callee_pname with - | Some (callee_mem, _) -> + match get_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 -> @@ -298,8 +298,7 @@ module TransferFunctions = struct mem' | None -> let mem = - if Language.curr_language_is Java then - join_java_static_final tenv get_proc_summary_and_formals exp mem + if Language.curr_language_is Java then join_java_static_final tenv get_summary exp mem else mem in let represents_multiple_values = is_array_access_exp exp in @@ -374,11 +373,11 @@ module TransferFunctions = struct in exec model_env ~ret mem | None -> ( - match get_proc_summary_and_formals callee_pname with - | Some (callee_exit_mem, callee_formals) -> + match (get_summary callee_pname, get_formals callee_pname) with + | Some callee_exit_mem, Some callee_formals -> instantiate_mem integer_type_widths ret callee_formals callee_pname params mem callee_exit_mem location - | None -> + | _, _ -> (* This may happen for procedures with a biabduction model too. *) L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ; if is_external callee_pname then ( @@ -424,13 +423,18 @@ let extract_post = Analyzer.extract_post let extract_state = Analyzer.extract_state let compute_invariant_map : - Summary.t -> Tenv.t -> Typ.IntegerWidths.t -> get_proc_summary_and_formals -> invariant_map = - fun summary tenv integer_type_widths get_proc_summary_and_formals -> + Summary.t + -> Tenv.t + -> Typ.IntegerWidths.t + -> BufferOverrunAnalysisSummary.get_summary + -> get_formals + -> invariant_map = + fun summary tenv integer_type_widths get_summary get_formals -> let pdesc = Summary.get_proc_desc summary in let cfg = CFG.from_pdesc pdesc in let pdata = let oenv = OndemandEnv.mk pdesc tenv integer_type_widths in - ProcData.make summary tenv {get_proc_summary_and_formals; oenv} + ProcData.make summary tenv {get_summary; get_formals; oenv} in let initial = Init.initial_state pdata (CFG.start_node cfg) in Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata @@ -455,15 +459,17 @@ let cached_compute_invariant_map = (* this should never happen *) assert false | None -> - let get_proc_summary_and_formals callee_pname = + let get_summary callee_pname = + Ondemand.analyze_proc_name ~caller_summary:summary callee_pname + |> Option.bind ~f:Payload.of_summary + in + let get_formals callee_pname = Ondemand.analyze_proc_name ~caller_summary:summary 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) ) ) + |> Option.map ~f:Summary.get_proc_desc + |> Option.map ~f:Procdesc.get_pvar_formals in let inv_map = - compute_invariant_map summary tenv integer_type_widths get_proc_summary_and_formals + compute_invariant_map summary tenv integer_type_widths get_summary get_formals in WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map) ; inv_map diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysisSummary.ml b/infer/src/bufferoverrun/bufferOverrunAnalysisSummary.ml index e59aeb5c9..64bc3e51d 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysisSummary.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysisSummary.ml @@ -11,3 +11,5 @@ module DomMem = BufferOverrunDomain.Mem type t = DomMem.no_oenv_t let pp = DomMem.pp + +type get_summary = DomMem.get_summary diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysisSummary.mli b/infer/src/bufferoverrun/bufferOverrunAnalysisSummary.mli index 9a87373da..2a2b92589 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysisSummary.mli +++ b/infer/src/bufferoverrun/bufferOverrunAnalysisSummary.mli @@ -10,3 +10,5 @@ open! IStd type t = BufferOverrunDomain.Mem.no_oenv_t val pp : Format.formatter -> t -> unit + +type get_summary = Procname.t -> t option diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index ab1adc4d1..76d475c2b 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -250,10 +250,10 @@ let instantiate_cond : type checks_summary = BufferOverrunCheckerSummary.t -type get_proc_summary = Procname.t -> ((Pvar.t * Typ.t) list * checks_summary) option +type get_checks_summary = Procname.t -> ((Pvar.t * Typ.t) list * checks_summary) option let check_instr : - get_proc_summary + get_checks_summary -> Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t @@ -262,7 +262,7 @@ let check_instr : -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t = - fun get_proc_summary pdesc tenv integer_type_widths node instr mem cond_set -> + fun get_checks_summary pdesc tenv integer_type_widths node instr mem cond_set -> match instr with | Sil.Load {e= exp; loc= location} -> cond_set @@ -291,7 +291,7 @@ let check_instr : in check model_env mem cond_set | None -> ( - match get_proc_summary callee_pname with + match get_checks_summary callee_pname with | Some (callee_formals, callee_condset) -> instantiate_cond integer_type_widths callee_pname callee_formals params mem callee_condset location @@ -315,7 +315,7 @@ let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> un let check_instrs : - get_proc_summary + get_checks_summary -> Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t @@ -325,7 +325,7 @@ let check_instrs : -> Dom.Mem.t AbstractInterpreter.State.t -> Checks.t -> Checks.t = - fun get_proc_summary pdesc tenv integer_type_widths cfg node instrs state checks -> + fun get_checks_summary pdesc tenv integer_type_widths cfg node instrs state checks -> match state with | _ when Instrs.is_empty instrs -> checks @@ -342,14 +342,14 @@ let check_instrs : checks in let cond_set = - check_instr get_proc_summary pdesc tenv integer_type_widths node instr pre checks.cond_set + check_instr get_checks_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 : - get_proc_summary + get_checks_summary -> Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t @@ -358,11 +358,11 @@ let check_node : -> Checks.t -> CFG.Node.t -> Checks.t = - fun get_proc_summary pdesc tenv integer_type_widths cfg inv_map checks node -> + fun get_checks_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 get_proc_summary pdesc tenv integer_type_widths cfg node instrs state checks + check_instrs get_checks_summary pdesc tenv integer_type_widths cfg node instrs state checks | _ -> checks @@ -370,16 +370,16 @@ let check_node : type checks = Checks.t let compute_checks : - get_proc_summary + get_checks_summary -> Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> BufferOverrunAnalysis.invariant_map -> checks = - fun get_proc_summary pdesc tenv integer_type_widths cfg inv_map -> + fun get_checks_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) + ~f:(check_node get_checks_summary pdesc tenv integer_type_widths cfg inv_map) ~init:Checks.empty @@ -422,7 +422,7 @@ let checker : Callbacks.proc_callback_args -> Summary.t = NodePrinter.with_session ~pp_name underlying_exit_node ~f:(fun () -> let cfg = CFG.from_pdesc proc_desc in let checks = - let get_proc_summary callee_pname = + let get_checks_summary callee_pname = Ondemand.analyze_proc_name ~caller_summary:summary callee_pname |> Option.bind ~f:(fun summary -> let checker_payload = Payload.of_summary summary in @@ -430,7 +430,7 @@ let checker : Callbacks.proc_callback_args -> Summary.t = (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 + compute_checks get_checks_summary proc_desc tenv integer_type_widths cfg inv_map in report_errors tenv checks summary ; let cond_set = get_checks_summary checks in diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index cea7ad454..8a734ec39 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -2229,6 +2229,8 @@ module Mem = struct if phys_equal m' m then x else NonBottom m' + type get_summary = Procname.t -> no_oenv_t option + let init : OndemandEnv.t -> t = fun oenv -> NonBottom (MemReach.init oenv) let f_lift_default : default:'a -> ('h MemReach.t0 -> 'a) -> 'h t0 -> 'a = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index 962f76e5f..f4e6dd4cc 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -455,6 +455,8 @@ module Mem : sig val bot : t + type get_summary = Procname.t -> no_oenv_t option + val init : BufferOverrunOndemandEnv.t -> t val exc_raised : t