[Summary] Move payloads to a separate module

Summary:
Preparing for bigger changes...
- Rename `payload` field to `payloads`
- Move `payload` type to `Payloads.t`
- `SummaryPayload`s only have to implement a change on `Payloads.t` rather than `Summary.t`

Reviewed By: sblackshear

Differential Revision: D7987211

fbshipit-source-id: c9d7a74
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 15b77c6a55
commit 1898ef3a7a

@ -12,9 +12,9 @@ open! IStd
module type Payload = sig
type t
val update_summary : t -> Summary.t -> Summary.t
val update_payloads : t -> Payloads.t -> Payloads.t
val of_summary : Summary.t -> t option
val of_payloads : Payloads.t -> t option
end
module type S = sig
@ -22,14 +22,18 @@ module type S = sig
val update_summary : t -> Summary.t -> Summary.t
val read_summary : Procdesc.t -> Typ.Procname.t -> t option
val read : Procdesc.t -> Typ.Procname.t -> t option
end
module Make (P : Payload) : S with type t = P.t = struct
type t = P.t
let update_summary = P.update_summary
let update_summary p (summary: Summary.t) =
{summary with payloads= P.update_payloads p summary.payloads}
let of_summary (summary: Summary.t) = P.of_payloads summary.payloads
let read_summary caller_pdesc callee_pname =
Ondemand.analyze_proc_name ~caller_pdesc callee_pname |> Option.bind ~f:P.of_summary
let read caller_pdesc callee_pname =
Ondemand.analyze_proc_name ~caller_pdesc callee_pname |> Option.bind ~f:of_summary
end

@ -12,11 +12,11 @@ open! IStd
module type Payload = sig
type t
val update_summary : t -> Summary.t -> Summary.t
(** Update the corresponding part of the payload in the procedure summary *)
val update_payloads : t -> Payloads.t -> Payloads.t
(** Update the corresponding part of the payloads *)
val of_summary : Summary.t -> t option
(** Read the corresponding part of the payload from the procedure summary *)
val of_payloads : Payloads.t -> t option
(** Read the corresponding part of the payloads *)
end
module type S = sig
@ -25,7 +25,7 @@ module type S = sig
val update_summary : t -> Summary.t -> Summary.t
(** Update the corresponding part of the payload in the procedure summary *)
val read_summary : Procdesc.t -> Typ.Procname.t -> t option
val read : Procdesc.t -> Typ.Procname.t -> t option
(** Return the payload for the given procedure. Runs the analysis on-demand if necessary. *)
end

@ -535,7 +535,7 @@ end
module StatsLogs = struct
let process _ (summary: Summary.t) _ _ =
let num_preposts =
match summary.payload.biabduction with Some {preposts} -> List.length preposts | None -> 0
match summary.payloads.biabduction with Some {preposts} -> List.length preposts | None -> 0
in
let clang_method_kind =
ProcAttributes.string_of_clang_method_kind (Summary.get_attributes summary).clang_method_kind

@ -0,0 +1,83 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! IStd
module F = Format
type t =
{ annot_map: AnnotReachabilityDomain.astate option
; biabduction: BiabductionSummary.t option
; buffer_overrun: BufferOverrunDomain.Summary.t option
; crashcontext_frame: Stacktree_t.stacktree option
; litho: LithoDomain.astate option
; quandary: QuandarySummary.t option
; racerd: RacerDDomain.summary option
; resources: ResourceLeakDomain.summary option
; siof: SiofDomain.astate option
; typestate: unit TypeState.t option
; uninit: UninitDomain.summary option
; cost: CostDomain.summary option
; starvation: StarvationDomain.summary option }
let pp pe fmt
{ biabduction
; typestate
; crashcontext_frame
; quandary
; siof
; racerd
; litho
; buffer_overrun
; annot_map
; uninit
; cost
; starvation } =
let pp_opt prefix pp fmt = function
| Some x ->
F.fprintf fmt "%s: %a@\n" prefix pp x
| None ->
()
in
F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a@\n"
(pp_opt "Biabduction" (BiabductionSummary.pp pe))
biabduction
(pp_opt "TypeState" (TypeState.pp TypeState.unit_ext))
typestate
(pp_opt "CrashContext" Crashcontext.pp_stacktree)
crashcontext_frame
(pp_opt "Quandary" QuandarySummary.pp)
quandary (pp_opt "Siof" SiofDomain.pp) siof
(pp_opt "RacerD" RacerDDomain.pp_summary)
racerd (pp_opt "Litho" LithoDomain.pp) litho
(pp_opt "BufferOverrun" BufferOverrunDomain.Summary.pp)
buffer_overrun
(pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp)
annot_map
(pp_opt "Uninitialised" UninitDomain.pp_summary)
uninit
(pp_opt "Cost" CostDomain.pp_summary)
cost
(pp_opt "Starvation" StarvationDomain.pp_summary)
starvation
let empty =
{ biabduction= None
; typestate= None
; annot_map= None
; crashcontext_frame= None
; quandary= None
; resources= None
; siof= None
; racerd= None
; litho= None
; buffer_overrun= None
; uninit= None
; cost= None
; starvation= None }

@ -0,0 +1,30 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! IStd
(** analysis results *)
type t =
{ annot_map: AnnotReachabilityDomain.astate option
; biabduction: BiabductionSummary.t option
; buffer_overrun: BufferOverrunDomain.Summary.t option
; crashcontext_frame: Stacktree_t.stacktree option
; litho: LithoDomain.astate option
; quandary: QuandarySummary.t option
; racerd: RacerDDomain.summary option
; resources: ResourceLeakDomain.summary option
; siof: SiofDomain.astate option
; typestate: unit TypeState.t option
; uninit: UninitDomain.summary option
; cost: CostDomain.summary option
; starvation: StarvationDomain.summary option }
val pp : Pp.env -> Format.formatter -> t -> unit
val empty : t

@ -74,23 +74,8 @@ module Status = struct
let is_analyzed = function Analyzed -> true | _ -> false
end
type payload =
{ annot_map: AnnotReachabilityDomain.astate option
; biabduction: BiabductionSummary.t option
; buffer_overrun: BufferOverrunDomain.Summary.t option
; crashcontext_frame: Stacktree_t.stacktree option
; litho: LithoDomain.astate option
; quandary: QuandarySummary.t option
; racerd: RacerDDomain.summary option
; resources: ResourceLeakDomain.summary option
; siof: SiofDomain.astate option
; typestate: unit TypeState.t option
; uninit: UninitDomain.summary option
; cost: CostDomain.summary option
; starvation: StarvationDomain.summary option }
type t =
{payload: payload; sessions: int ref; stats: Stats.t; status: Status.t; proc_desc: Procdesc.t}
{payloads: Payloads.t; sessions: int ref; stats: Stats.t; status: Status.t; proc_desc: Procdesc.t}
let get_status summary = summary.status
@ -132,52 +117,10 @@ let pp_no_stats_specs fmt summary =
F.fprintf fmt "%a@\n" Status.pp summary.status
let pp_payload pe fmt
{ biabduction
; typestate
; crashcontext_frame
; quandary
; siof
; racerd
; litho
; buffer_overrun
; annot_map
; uninit
; cost
; starvation } =
let pp_opt prefix pp fmt = function
| Some x ->
F.fprintf fmt "%s: %a@\n" prefix pp x
| None ->
()
in
F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a@\n"
(pp_opt "Biabduction" (BiabductionSummary.pp pe))
biabduction
(pp_opt "TypeState" (TypeState.pp TypeState.unit_ext))
typestate
(pp_opt "CrashContext" Crashcontext.pp_stacktree)
crashcontext_frame
(pp_opt "Quandary" QuandarySummary.pp)
quandary (pp_opt "Siof" SiofDomain.pp) siof
(pp_opt "RacerD" RacerDDomain.pp_summary)
racerd (pp_opt "Litho" LithoDomain.pp) litho
(pp_opt "BufferOverrun" BufferOverrunDomain.Summary.pp)
buffer_overrun
(pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp)
annot_map
(pp_opt "Uninitialised" UninitDomain.pp_summary)
uninit
(pp_opt "Cost" CostDomain.pp_summary)
cost
(pp_opt "Starvation" StarvationDomain.pp_summary)
starvation
let pp_text fmt summary =
pp_no_stats_specs fmt summary ;
F.fprintf fmt "%a@\n%a%a" pp_errlog (get_err_log summary) Stats.pp summary.stats
(pp_payload Pp.text) summary.payload
(Payloads.pp Pp.text) summary.payloads
let pp_html source color fmt summary =
@ -188,7 +131,7 @@ let pp_html source color fmt summary =
Errlog.pp_html source [] fmt (get_err_log summary) ;
Io_infer.Html.pp_hline fmt () ;
F.fprintf fmt "<LISTING>@\n" ;
pp_payload (Pp.html color) fmt summary.payload ;
Payloads.pp (Pp.html color) fmt summary.payloads ;
F.fprintf fmt "</LISTING>@\n"
@ -305,28 +248,16 @@ let store (summ: t) =
~data:final_summary
let empty_payload =
{ biabduction= None
; typestate= None
; annot_map= None
; crashcontext_frame= None
; quandary= None
; resources= None
; siof= None
; racerd= None
; litho= None
; buffer_overrun= None
; uninit= None
; cost= None
; starvation= None }
(** [init_summary (depend_list, nodes,
proc_flags, calls, in_out_calls_opt, proc_attributes)]
initializes the summary for [proc_name] given dependent procs in list [depend_list]. *)
let init_summary proc_desc =
let summary =
{sessions= ref 0; payload= empty_payload; stats= Stats.empty; status= Status.Pending; proc_desc}
{ sessions= ref 0
; payloads= Payloads.empty
; stats= Stats.empty
; status= Status.Pending
; proc_desc }
in
Typ.Procname.Hash.replace cache (Procdesc.get_proc_name proc_desc) summary ;
summary

@ -45,25 +45,9 @@ module Status : sig
val to_string : t -> string
end
(** analysis results *)
type payload =
{ annot_map: AnnotReachabilityDomain.astate option
; biabduction: BiabductionSummary.t option
; buffer_overrun: BufferOverrunDomain.Summary.t option
; crashcontext_frame: Stacktree_t.stacktree option
; litho: LithoDomain.astate option
; quandary: QuandarySummary.t option
; racerd: RacerDDomain.summary option
; resources: ResourceLeakDomain.summary option
; siof: SiofDomain.astate option
; typestate: unit TypeState.t option
; uninit: UninitDomain.summary option
; cost: CostDomain.summary option
; starvation: StarvationDomain.summary option }
(** summary of a procedure name *)
type t =
{ payload: payload
{ payloads: Payloads.t
; sessions: int ref (** Session number: how many nodes went through symbolic execution *)
; stats: Stats.t
; status: Status.t

@ -136,13 +136,14 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc =
let log_error_and_continue exn (summary: Summary.t) kind =
Reporting.log_error summary exn ;
let stats = Summary.Stats.update summary.stats ~failure_kind:kind in
let payload =
let payloads =
let biabduction =
Some BiabductionSummary.{preposts= []; phase= summary.payload.biabduction |> opt_get_phase}
Some
BiabductionSummary.{preposts= []; phase= summary.payloads.biabduction |> opt_get_phase}
in
{summary.payload with biabduction}
{summary.payloads with biabduction}
in
let new_summary = {summary with stats; payload} in
let new_summary = {summary with stats; payloads} in
Summary.store new_summary ; remove_active callee_pname ; log_elapsed_time () ; new_summary
in
let old_state = save_global_state () in

@ -118,7 +118,7 @@ let log_call_trace ~caller_name ~callee_name ?callee_attributes ?reason loc res
(***************)
let get_specs_from_payload summary =
Option.map summary.Summary.payload.biabduction ~f:(fun BiabductionSummary.({preposts}) ->
Option.map summary.Summary.payloads.biabduction ~f:(fun BiabductionSummary.({preposts}) ->
preposts )
|> BiabductionSummary.get_specs_from_preposts

@ -435,7 +435,7 @@ let forward_tabulate exe_env tenv proc_cfg wl =
let log_string proc_name =
let summary = Summary.get_unsafe proc_name in
let phase_string =
BiabductionSummary.(summary.payload.biabduction |> opt_get_phase |> string_of_phase_short)
BiabductionSummary.(summary.payloads.biabduction |> opt_get_phase |> string_of_phase_short)
in
let status = Summary.get_status summary in
F.sprintf "[%s:%s] %s" phase_string (Summary.Status.to_string status)
@ -904,7 +904,7 @@ let perform_analysis_phase exe_env tenv (summary: Summary.t) (proc_cfg: ProcCfg.
in
(go, get_results)
in
match BiabductionSummary.opt_get_phase summary.payload.biabduction with
match BiabductionSummary.opt_get_phase summary.payloads.biabduction with
| FOOTPRINT ->
compute_footprint ()
| RE_EXECUTION ->
@ -1131,11 +1131,11 @@ let update_summary tenv prev_summary specs phase res =
| BiabductionSummary.RE_EXECUTION ->
List.map ~f:(BiabductionSummary.NormSpec.erase_join_info_pre tenv) new_specs
in
let payload =
{ prev_summary.Summary.payload with
Summary.biabduction= Some BiabductionSummary.{preposts; phase} }
let payloads =
{ prev_summary.Summary.payloads with
Payloads.biabduction= Some BiabductionSummary.{preposts; phase} }
in
{prev_summary with Summary.stats; payload}
{prev_summary with Summary.stats; payloads}
(** Analyze the procedure and return the resulting summary. *)
@ -1160,12 +1160,12 @@ let transition_footprint_re_exe tenv proc_name joined_pres =
let summary = Summary.get_unsafe proc_name in
let summary' =
if Config.only_footprint then
match summary.Summary.payload.biabduction with
match summary.Summary.payloads.biabduction with
| Some ({phase= FOOTPRINT} as biabduction) ->
{ summary with
Summary.payload=
{ summary.payload with
Summary.biabduction= Some {biabduction with BiabductionSummary.phase= RE_EXECUTION}
Summary.payloads=
{ summary.payloads with
Payloads.biabduction= Some {biabduction with BiabductionSummary.phase= RE_EXECUTION}
} }
| _ ->
summary
@ -1178,11 +1178,11 @@ let transition_footprint_re_exe tenv proc_name joined_pres =
)
joined_pres
in
let payload =
{ summary.Summary.payload with
let payloads =
{ summary.Summary.payloads with
biabduction= Some BiabductionSummary.{preposts; phase= RE_EXECUTION} }
in
{summary with Summary.payload}
{summary with Summary.payloads}
in
Summary.add proc_name summary'
@ -1220,7 +1220,7 @@ let perform_transition proc_cfg tenv proc_name =
in
match Summary.get proc_name with
| Some summary
when BiabductionSummary.(summary.payload.biabduction |> opt_get_phase |> equal_phase FOOTPRINT) ->
when BiabductionSummary.(summary.payloads.biabduction |> opt_get_phase |> equal_phase FOOTPRINT) ->
transition summary
| _ ->
()
@ -1235,15 +1235,15 @@ let analyze_procedure_aux exe_env tenv proc_desc =
perform_transition proc_cfg tenv proc_name ;
let summaryre = Config.run_in_re_execution_mode (analyze_proc exe_env tenv) proc_cfg in
let summary_compact =
match summaryre.Summary.payload.biabduction with
match summaryre.Summary.payloads.biabduction with
| Some BiabductionSummary.({preposts} as biabduction) when Config.save_compact_summaries ->
let sharing_env = Sil.create_sharing_env () in
let compact_preposts =
List.map ~f:(BiabductionSummary.NormSpec.compact sharing_env) preposts
in
{ summaryre with
payload=
{ summaryre.payload with
payloads=
{ summaryre.payloads with
biabduction= Some {biabduction with BiabductionSummary.preposts= compact_preposts} }
}
| _ ->

@ -24,11 +24,9 @@ module TraceSet = Trace.Set
module Payload = SummaryPayload.Make (struct
type t = Dom.Summary.t
let update_summary astate (summary: Summary.t) =
{summary with payload= {summary.payload with buffer_overrun= Some astate}}
let update_payloads astate (payloads: Payloads.t) = {payloads with buffer_overrun= Some astate}
let of_summary (summary: Summary.t) = summary.payload.buffer_overrun
let of_payloads (payloads: Payloads.t) = payloads.buffer_overrun
end)
module TransferFunctions (CFG : ProcCfg.S) = struct
@ -252,7 +250,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let model_env = Models.mk_model_env callee_pname node_hash location tenv ~ret in
exec model_env mem
| None ->
match Payload.read_summary pdesc callee_pname with
match Payload.read pdesc callee_pname with
| Some summary ->
let callee = Ondemand.get_proc_desc callee_pname in
instantiate_mem tenv ret callee callee_pname params mem summary location
@ -454,7 +452,7 @@ module Report = struct
let node_hash = CFG.hash node in
check (Models.mk_model_env pname node_hash location tenv) mem cond_set
| None ->
match Payload.read_summary pdesc callee_pname with
match Payload.read pdesc callee_pname with
| Some callee_summary ->
let callee = Ondemand.get_proc_desc callee_pname in
instantiate_cond tenv pname callee params mem callee_summary location

@ -22,12 +22,9 @@ module Domain = AbstractDomain.FiniteSet (Typ.Procname)
module SpecPayload = SummaryPayload.Make (struct
type t = Stacktree_j.stacktree
let update_summary frame (summary: Summary.t) =
let payload = {summary.payload with Summary.crashcontext_frame= Some frame} in
{summary with payload}
let update_payloads frame (payloads: Payloads.t) = {payloads with crashcontext_frame= Some frame}
let of_summary (summary: Summary.t) = summary.payload.crashcontext_frame
let of_payloads (payloads: Payloads.t) = payloads.crashcontext_frame
end)
type extras_t = {get_proc_desc: Typ.Procname.t -> Procdesc.t option; stacktraces: Stacktrace.t list}
@ -70,7 +67,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let callees =
List.map
~f:(fun pn ->
match SpecPayload.read_summary pdesc pn with
match SpecPayload.read pdesc pn with
| None -> (
match get_proc_desc pn with
| None ->

@ -14,11 +14,9 @@ module Domain = LithoDomain
module Payload = SummaryPayload.Make (struct
type t = Domain.astate
let update_summary astate (summary: Summary.t) =
{summary with payload= {summary.payload with litho= Some astate}}
let update_payloads astate (payloads: Payloads.t) = {payloads with litho= Some astate}
let of_summary (summary: Summary.t) = summary.payload.litho
let of_payloads (payloads: Payloads.t) = payloads.litho
end)
module LithoFramework = struct
@ -229,7 +227,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
, (HilExp.AccessExpression receiver_ae :: _ as actuals)
, _
, _ ) ->
let summary = Payload.read_summary proc_data.pdesc callee_procname in
let summary = Payload.read proc_data.pdesc callee_procname in
let receiver =
Domain.LocalAccessPath.make (AccessExpression.to_access_path receiver_ae) caller_pname
in
@ -257,7 +255,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(* treat it like a normal call *)
apply_callee_summary summary caller_pname return_base actuals astate
| Call (ret_id_typ, Direct callee_procname, actuals, _, _) ->
let summary = Payload.read_summary proc_data.pdesc callee_procname in
let summary = Payload.read proc_data.pdesc callee_procname in
apply_callee_summary summary caller_pname ret_id_typ actuals astate
| Assign (lhs_ae, HilExp.AccessExpression rhs_ae, _)
-> (

@ -53,11 +53,9 @@ let is_modelled =
module Payload = SummaryPayload.Make (struct
type t = SiofDomain.astate
let update_summary astate (summary: Summary.t) =
{summary with payload= {summary.payload with siof= Some astate}}
let update_payloads astate (payloads: Payloads.t) = {payloads with siof= Some astate}
let of_summary (summary: Summary.t) = summary.payload.siof
let of_payloads (payloads: Payloads.t) = payloads.siof
end)
module TransferFunctions (CFG : ProcCfg.S) = struct
@ -68,7 +66,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let is_compile_time_constructed pdesc pv =
let init_pname = Pvar.get_initializer_pname pv in
match Option.bind init_pname ~f:(Payload.read_summary pdesc) with
match Option.bind init_pname ~f:(Payload.read pdesc) with
| Some (Bottom, _) ->
(* we analyzed the initializer for this global and found that it doesn't require any runtime
initialization so cannot participate in SIOF *)
@ -145,7 +143,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
add_actuals_globals astate pdesc loc actuals_without_self
| Call (_, Const (Cfun callee_pname), actuals, loc, _) ->
let callee_astate =
match Payload.read_summary pdesc callee_pname with
match Payload.read pdesc callee_pname with
| Some (NonBottom trace, initialized_by_callee) ->
let already_initialized = snd astate in
let dangerous_accesses =
@ -194,7 +192,7 @@ let is_foreign tu_opt v =
let report_siof summary trace pdesc gname loc =
let trace_of_pname pname =
match Payload.read_summary pdesc pname with
match Payload.read pdesc pname with
| Some (NonBottom summary, _) ->
summary
| _ ->
@ -223,7 +221,7 @@ let report_siof summary trace pdesc gname loc =
let siof_check pdesc gname (summary: Summary.t) =
match summary.payload.siof with
match summary.payloads.siof with
| Some (NonBottom post, _) ->
let attrs = Procdesc.get_attributes pdesc in
let tu_opt =

@ -63,11 +63,9 @@ end
module Payload = SummaryPayload.Make (struct
type t = AnnotReachabilityDomain.astate
let update_summary annot_map (summary: Summary.t) =
{summary with payload= {summary.payload with annot_map= Some annot_map}}
let update_payloads annot_map (payloads: Payloads.t) = {payloads with annot_map= Some annot_map}
let of_summary (summary: Summary.t) = summary.payload.annot_map
let of_payloads (payloads: Payloads.t) = payloads.annot_map
end)
let is_modeled_expensive tenv = function
@ -119,7 +117,7 @@ let method_overrides_annot annot tenv pname = method_overrides (method_has_annot
let lookup_annotation_calls ~caller_pdesc annot pname =
match Ondemand.analyze_proc_name ~caller_pdesc pname with
| Some {Summary.payload= {Summary.annot_map= Some annot_map}} -> (
| Some {Summary.payloads= {Payloads.annot_map= Some annot_map}} -> (
try AnnotReachabilityDomain.find annot annot_map with Caml.Not_found ->
AnnotReachabilityDomain.SinkMap.empty )
| _ ->
@ -405,7 +403,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let merge_callee_map call_site pdesc callee_pname astate =
match Payload.read_summary pdesc callee_pname with
match Payload.read pdesc callee_pname with
| None ->
astate
| Some callee_call_map ->

@ -16,11 +16,9 @@ module NodesBasicCostDomain = CostDomain.NodeInstructionToCostMap
module Payload = SummaryPayload.Make (struct
type t = CostDomain.summary
let update_summary sum (summary: Summary.t) =
{summary with payload= {summary.payload with cost= Some sum}}
let update_payloads sum (payloads: Payloads.t) = {payloads with cost= Some sum}
let of_summary (summary: Summary.t) = summary.payload.cost
let of_payloads (payloads: Payloads.t) = payloads.cost
end)
(* We use this treshold to give error if the cost is above it.
@ -58,7 +56,7 @@ module TransferFunctionsNodesBasicCost = struct
"Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" BasicCost.pp
callee_cost Typ.Procname.pp callee_pname
| Some callee_pdesc ->
match BufferOverrunChecker.Payload.read_summary caller_pdesc callee_pname with
match BufferOverrunChecker.Payload.read caller_pdesc callee_pname with
| None ->
L.(die InternalError)
"Can't instantiate symbolic cost %a from call to %a (can't get summary)" BasicCost.pp
@ -82,7 +80,7 @@ module TransferFunctionsNodesBasicCost = struct
match instr with
| Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) ->
let callee_cost =
match Payload.read_summary pdesc callee_pname with
match Payload.read pdesc callee_pname with
| Some {post= callee_cost} ->
if BasicCost.is_symbolic callee_cost then
instantiate_cost ~tenv ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem

@ -21,11 +21,9 @@ module RecordDomain = UninitDomain.Record (UninitVars) (AliasedVars) (D)
module Payload = SummaryPayload.Make (struct
type t = UninitDomain.summary
let update_summary sum (summary: Summary.t) =
{summary with payload= {summary.payload with uninit= Some sum}}
let update_payloads sum (payloads: Payloads.t) = {payloads with uninit= Some sum}
let of_summary (summary: Summary.t) = summary.payload.uninit
let of_payloads (payloads: Payloads.t) = payloads.uninit
end)
let blacklisted_functions = [BuiltinDecl.__set_array_length]
@ -181,7 +179,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let remove_initialized_params pdesc call acc idx (base, al) remove_fields =
match Payload.read_summary pdesc call with
match Payload.read pdesc call with
| Some {pre= initialized_formal_params; post= _} -> (
match init_nth_actual_param call idx initialized_formal_params with
| Some nth_formal ->
@ -196,7 +194,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(* true if a function initializes at least a param or a field of a struct param *)
let function_initializes_some_formal_params pdesc call =
match Payload.read_summary pdesc call with
match Payload.read pdesc call with
| Some {pre= initialized_formal_params; post= _} ->
not (D.is_empty initialized_formal_params)
| _ ->

@ -15,11 +15,9 @@ module MF = MarkupFormatter
module Payload = SummaryPayload.Make (struct
type t = RacerDDomain.summary
let update_summary post (summary: Summary.t) =
{summary with payload= {summary.payload with racerd= Some post}}
let update_payloads post (payloads: Payloads.t) = {payloads with racerd= Some post}
let of_summary (summary: Summary.t) = summary.payload.racerd
let of_payloads (payloads: Payloads.t) = payloads.racerd
end)
module TransferFunctions (CFG : ProcCfg.S) = struct
@ -248,7 +246,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
make_container_access callee_pname ~is_write:false (get_receiver_ap actuals) callee_loc
tenv caller_pdesc astate
| None, _ ->
Payload.read_summary caller_pdesc callee_pname
Payload.read caller_pdesc callee_pname
let add_reads exps loc accesses locks threads ownership proc_data =
@ -896,7 +894,7 @@ let desc_of_sink sink =
let trace_of_pname orig_sink orig_pdesc callee_pname =
let open RacerDDomain in
let orig_access = PathDomain.Sink.kind orig_sink in
match Payload.read_summary orig_pdesc callee_pname with
match Payload.read orig_pdesc callee_pname with
| Some {accesses} ->
AccessDomain.fold
(fun snapshot acc ->
@ -1499,7 +1497,7 @@ let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env
accesses acc
in
let aggregate_posts acc (tenv, proc_desc) =
match Payload.read_summary proc_desc (Procdesc.get_proc_name proc_desc) with
match Payload.read proc_desc (Procdesc.get_proc_name proc_desc) with
| Some summary ->
aggregate_post summary tenv proc_desc acc
| None ->

@ -19,11 +19,9 @@ let is_on_main_thread pn =
module Payload = SummaryPayload.Make (struct
type t = StarvationDomain.summary
let update_summary post (summary: Summary.t) =
{summary with payload= {summary.payload with starvation= Some post}}
let update_payloads post (payloads: Payloads.t) = {payloads with starvation= Some post}
let of_summary (summary: Summary.t) = summary.payload.starvation
let of_payloads (payloads: Payloads.t) = payloads.starvation
end)
(* using an indentifier for a class object, create an access path representing that lock;
@ -85,7 +83,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| NoEffect when is_on_main_thread callee ->
Domain.set_on_main_thread astate
| _ ->
Payload.read_summary pdesc callee
Payload.read pdesc callee
|> Option.value_map ~default:astate ~f:(Domain.integrate_summary astate callee loc) )
| _ ->
astate
@ -153,7 +151,7 @@ let get_summaries_of_methods_in_class get_proc_desc tenv current_pdesc clazz =
in
let pdescs = List.rev_filter_map methods ~f:get_proc_desc in
let get_summary callee_pdesc =
Payload.read_summary current_pdesc (Procdesc.get_proc_name callee_pdesc)
Payload.read current_pdesc (Procdesc.get_proc_name callee_pdesc)
|> Option.map ~f:(fun summary -> (callee_pdesc, summary))
in
List.rev_filter_map pdescs ~f:get_summary
@ -316,7 +314,7 @@ let report_blocks_on_main_thread get_proc_desc tenv current_pdesc summary =
let reporting {Callbacks.procedures; get_proc_desc; exe_env} =
let report_procedure (tenv, proc_desc) =
die_if_not_java proc_desc ;
Payload.read_summary proc_desc (Procdesc.get_proc_name proc_desc)
Payload.read proc_desc (Procdesc.get_proc_name proc_desc)
|> Option.iter ~f:(fun ((s, main) as summary) ->
report_deadlocks get_proc_desc tenv proc_desc summary ;
if main then report_blocks_on_main_thread get_proc_desc tenv proc_desc s )

@ -33,7 +33,7 @@ module type ExtensionT = sig
val ext : extension TypeState.ext
val update_payload : extension TypeState.t option -> Summary.payload -> Summary.payload
val update_payloads : extension TypeState.t option -> Payloads.t -> Payloads.t
end
(** Create a module with the toplevel callback. *)
@ -44,8 +44,8 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
| Some old_summ ->
let new_summ =
{ old_summ with
Summary.payload= Extension.update_payload final_typestate_opt old_summ.Summary.payload
}
Summary.payloads=
Extension.update_payloads final_typestate_opt old_summ.Summary.payloads }
in
Summary.add proc_name new_summ
| None ->
@ -379,7 +379,8 @@ module EmptyExtension : ExtensionT = struct
{TypeState.empty; check_instr; join; pp}
let update_payload typestate_opt payload = {payload with Summary.typestate= typestate_opt}
let update_payloads typestate_opt (payloads: Payloads.t) =
{payloads with typestate= typestate_opt}
end
module Main = Build (EmptyExtension)

@ -27,5 +27,5 @@ module type ExtensionT = sig
val ext : extension TypeState.ext
val update_payload : extension TypeState.t option -> Summary.payload -> Summary.payload
val update_payloads : extension TypeState.t option -> Payloads.t -> Payloads.t
end

@ -16,11 +16,11 @@ module Domain = ResourceLeakDomain
module Payload = SummaryPayload.Make (struct
type t = Domain.astate
let update_summary resources_payload (summary: Summary.t) =
{summary with payload= {summary.payload with resources= Some resources_payload}}
let update_payloads resources_payload (payloads: Payloads.t) =
{payloads with resources= Some resources_payload}
let of_summary (summary: Summary.t) = summary.payload.resources
let of_payloads (payloads: Payloads.t) = payloads.resources
end)
type extras = FormalMap.t
@ -70,7 +70,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
else if releases_resource callee_procname tenv then astate - 1 (* 2(a) *)
else astate
in
match Payload.read_summary pdesc callee_procname with
match Payload.read pdesc callee_procname with
| Some _summary ->
(* Looked up the summary for callee_procname... do something with it *)
(* 4(a) *)

@ -19,11 +19,11 @@ module Make (TaintSpecification : TaintSpec.S) = struct
module Payload = SummaryPayload.Make (struct
type t = QuandarySummary.t
let update_summary quandary_payload (summary: Summary.t) =
{summary with payload= {summary.payload with quandary= Some quandary_payload}}
let update_payloads quandary_payload (payloads: Payloads.t) =
{payloads with quandary= Some quandary_payload}
let of_summary (summary: Summary.t) = summary.payload.quandary
let of_payloads (payloads: Payloads.t) = payloads.quandary
end)
module Domain = TaintDomain
@ -137,7 +137,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
(* read_summary will trigger ondemand analysis of the current proc. we don't want that. *)
TaintDomain.empty
else
match Payload.read_summary proc_data.pdesc pname with
match Payload.read proc_data.pdesc pname with
| Some summary ->
TaintSpecification.of_summary_access_tree summary
| None ->
@ -695,7 +695,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
(* don't use a summary for a procedure that is a direct source *)
astate_with_source
else
match Payload.read_summary proc_data.pdesc callee_pname with
match Payload.read proc_data.pdesc callee_pname with
| None ->
handle_unknown_call callee_pname astate_with_source
| Some summary ->

Loading…
Cancel
Save