[ondemand] simplify API by removing need to pass type environment

Summary: Noticed this when I was writing the documentation for the abstract interpretation framework and was curious about why `Ondemand.analyze_proc` needs the type environment. It turns out that the type environment is only used to transform/normalize Infer bi-abduction specs before storing them to disk, but this can be done elsewhere. Doing this normalization elsewhere simplifies the on-demand API, which is a win for all of its clients.

Reviewed By: cristianoc

Differential Revision: D4241279

fbshipit-source-id: 957b243
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent 01136cc326
commit 226791b631

@ -179,10 +179,6 @@ let iterate_callbacks store_summary call_graph exe_env =
(iterate_cluster_callbacks originally_defined_procs exe_env) (iterate_cluster_callbacks originally_defined_procs exe_env)
(cluster procs_to_analyze); (cluster procs_to_analyze);
IList.iter IList.iter store_summary procs_to_analyze;
(fun proc_name ->
let tenv = Exe_env.get_tenv ~create:true exe_env proc_name in
store_summary tenv proc_name)
procs_to_analyze;
Config.curr_language := saved_language Config.curr_language := saved_language

@ -45,4 +45,4 @@ val register_cluster_callback : Config.language option -> cluster_callback_t ->
val unregister_all_callbacks : unit -> unit val unregister_all_callbacks : unit -> unit
(** Invoke all the registered callbacks. *) (** Invoke all the registered callbacks. *)
val iterate_callbacks : (Tenv.t -> Procname.t -> unit) -> Cg.t -> Exe_env.t -> unit val iterate_callbacks : (Procname.t -> unit) -> Cg.t -> Exe_env.t -> unit

@ -1299,10 +1299,11 @@ let update_summary tenv prev_summary specs phase proc_name elapsed res =
symops; symops;
stats_failure; stats_failure;
} in } in
let payload = let preposts =
{ prev_summary.Specs.payload with match phase with
Specs.preposts = Some new_specs; | Specs.FOOTPRINT -> Some new_specs
} in | Specs.RE_EXECUTION -> Some (IList.map (Specs.NormSpec.erase_join_info_pre tenv) new_specs) in
let payload = { prev_summary.Specs.payload with Specs.preposts; } in
{ prev_summary with { prev_summary with
Specs.phase; Specs.phase;
stats; stats;
@ -1424,11 +1425,8 @@ let interprocedural_algorithm exe_env : unit =
None in None in
let process_one_proc proc_name = let process_one_proc proc_name =
match to_analyze proc_name with match to_analyze proc_name with
| Some pdesc -> | Some pdesc -> Ondemand.analyze_proc_name ~propagate_exceptions:false pdesc proc_name
let tenv = Exe_env.get_tenv ~create:true exe_env proc_name in | None -> () in
Ondemand.analyze_proc_name tenv ~propagate_exceptions:false pdesc proc_name
| None ->
() in
IList.iter process_one_proc procs_to_analyze IList.iter process_one_proc procs_to_analyze
(** Perform the analysis of an exe_env *) (** Perform the analysis of an exe_env *)

@ -102,7 +102,7 @@ let restore_global_state st =
Timeout.resume_previous_timeout () Timeout.resume_previous_timeout ()
let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc = let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc =
let curr_pname = Procdesc.get_proc_name curr_pdesc in let curr_pname = Procdesc.get_proc_name curr_pdesc in
let callee_pname = Procdesc.get_proc_name callee_pdesc in let callee_pname = Procdesc.get_proc_name callee_pdesc in
@ -146,7 +146,7 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_
Specs.status = Specs.INACTIVE; Specs.status = Specs.INACTIVE;
timestamp = summary.Specs.timestamp + 1 } in timestamp = summary.Specs.timestamp + 1 } in
Specs.add_summary callee_pname summary'; Specs.add_summary callee_pname summary';
Checkers.ST.store_summary tenv callee_pname; Checkers.ST.store_summary callee_pname;
Printer.write_proc_html source false callee_pdesc in Printer.write_proc_html source false callee_pdesc in
let log_error_and_continue exn kind = let log_error_and_continue exn kind =
@ -187,14 +187,13 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_
log_error_and_continue exn (FKcrash (Printexc.to_string exn)) log_error_and_continue exn (FKcrash (Printexc.to_string exn))
let analyze_proc_desc tenv ~propagate_exceptions curr_pdesc callee_pdesc = let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc =
let callee_pname = Procdesc.get_proc_name callee_pdesc in let callee_pname = Procdesc.get_proc_name callee_pdesc in
let proc_attributes = Procdesc.get_attributes callee_pdesc in let proc_attributes = Procdesc.get_attributes callee_pdesc in
match !callbacks_ref with match !callbacks_ref with
| Some callbacks | Some callbacks
when should_be_analyzed proc_attributes callee_pname -> when should_be_analyzed proc_attributes callee_pname ->
run_proc_analysis tenv run_proc_analysis ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc
~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc
| _ -> () | _ -> ()
@ -202,17 +201,15 @@ let analyze_proc_desc tenv ~propagate_exceptions curr_pdesc callee_pdesc =
(** analyze_proc_name curr_pdesc proc_name (** analyze_proc_name curr_pdesc proc_name
performs an on-demand analysis of proc_name performs an on-demand analysis of proc_name
triggered during the analysis of curr_pname. *) triggered during the analysis of curr_pname. *)
let analyze_proc_name tenv ~propagate_exceptions curr_pdesc callee_pname = let analyze_proc_name ~propagate_exceptions curr_pdesc callee_pname =
match !callbacks_ref with match !callbacks_ref with
| Some callbacks | Some callbacks
when procedure_should_be_analyzed callee_pname -> when procedure_should_be_analyzed callee_pname ->
begin begin
match callbacks.get_proc_desc callee_pname with match callbacks.get_proc_desc callee_pname with
| Some callee_pdesc -> | Some callee_pdesc -> analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc
analyze_proc_desc tenv ~propagate_exceptions curr_pdesc callee_pdesc | None -> ()
| None ->
()
end end
| _ -> | _ ->
() (* skipping *) () (* skipping *)

@ -30,12 +30,12 @@ val get_proc_desc : get_proc_desc
(** analyze_proc_desc curr_pdesc callee_pdesc (** analyze_proc_desc curr_pdesc callee_pdesc
performs an on-demand analysis of callee_pdesc performs an on-demand analysis of callee_pdesc
triggered during the analysis of curr_pdesc. *) triggered during the analysis of curr_pdesc. *)
val analyze_proc_desc : Tenv.t -> propagate_exceptions:bool -> Procdesc.t -> Procdesc.t -> unit val analyze_proc_desc : propagate_exceptions:bool -> Procdesc.t -> Procdesc.t -> unit
(** analyze_proc_name curr_pdesc proc_name (** analyze_proc_name curr_pdesc proc_name
performs an on-demand analysis of proc_name performs an on-demand analysis of proc_name
triggered during the analysis of curr_pdesc. *) triggered during the analysis of curr_pdesc. *)
val analyze_proc_name : Tenv.t -> propagate_exceptions:bool -> Procdesc.t -> Procname.t -> unit val analyze_proc_name : propagate_exceptions:bool -> Procdesc.t -> Procname.t -> unit
(** Check if the procedure called needs to be analyzed. *) (** Check if the procedure called needs to be analyzed. *)
val procedure_should_be_analyzed : Procname.t -> bool val procedure_should_be_analyzed : Procname.t -> bool

@ -554,14 +554,7 @@ let summary_serializer : summary Serialization.serializer =
Serialization.create_serializer Serialization.summary_key Serialization.create_serializer Serialization.summary_key
(** Save summary for the procedure into the spec database *) (** Save summary for the procedure into the spec database *)
let store_summary tenv pname (summ: summary) = let store_summary pname (summ1: summary) =
let process_payload payload = match payload.preposts with
| Some specs ->
{ payload with
preposts = Some (IList.map (NormSpec.erase_join_info_pre tenv) specs);
}
| None -> payload in
let summ1 = { summ with payload = process_payload summ.payload } in
let summ2 = if Config.save_compact_summaries let summ2 = if Config.save_compact_summaries
then summary_compact (Sil.create_sharing_env ()) summ1 then summary_compact (Sil.create_sharing_env ()) summ1
else summ1 in else summ1 in

@ -75,6 +75,8 @@ type 'a spec = { pre: 'a Jprop.t; posts: ('a Prop.t * Paths.Path.t) list; visite
(** encapsulate type for normalized specs *) (** encapsulate type for normalized specs *)
module NormSpec : sig module NormSpec : sig
type t type t
val erase_join_info_pre : Tenv.t -> t -> t (** Erase join info from pre of spec *)
end end
(** module for tracing stats of function calls *) (** module for tracing stats of function calls *)
@ -275,7 +277,7 @@ val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t
val res_dir_specs_filename : Procname.t -> DB.filename val res_dir_specs_filename : Procname.t -> DB.filename
(** Save summary for the procedure into the spec database *) (** Save summary for the procedure into the spec database *)
val store_summary : Tenv.t -> Procname.t -> summary -> unit val store_summary : Procname.t -> summary -> unit
(** Return a compact representation of the summary *) (** Return a compact representation of the summary *)
val summary_compact : Sil.sharing_env -> summary -> summary val summary_compact : Sil.sharing_env -> summary -> summary

@ -641,12 +641,12 @@ let resolve_and_analyze
whether the method is defined or generated by the specialization *) whether the method is defined or generated by the specialization *)
let analyze_ondemand resolved_pname : unit = let analyze_ondemand resolved_pname : unit =
if Procname.equal resolved_pname callee_proc_name then if Procname.equal resolved_pname callee_proc_name then
Ondemand.analyze_proc_name tenv ~propagate_exceptions:true caller_pdesc callee_proc_name Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_proc_name
else else
(* Create the type sprecialized procedure description and analyze it directly *) (* Create the type sprecialized procedure description and analyze it directly *)
Option.may Option.may
(fun specialized_pdesc -> (fun specialized_pdesc ->
Ondemand.analyze_proc_desc tenv ~propagate_exceptions:true caller_pdesc specialized_pdesc) Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc)
(match Ondemand.get_proc_desc resolved_pname with (match Ondemand.get_proc_desc resolved_pname with
| Some resolved_proc_desc -> | Some resolved_proc_desc ->
Some resolved_proc_desc Some resolved_proc_desc
@ -1092,7 +1092,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let resolved_pnames = let resolved_pnames =
resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in
let exec_one_pname pname = let exec_one_pname pname =
Ondemand.analyze_proc_name tenv ~propagate_exceptions:true current_pdesc pname; Ondemand.analyze_proc_name ~propagate_exceptions:true current_pdesc pname;
let exec_skip_call ret_annots ret_type = skip_call norm_prop path pname ret_annots let exec_skip_call ret_annots ret_type = skip_call norm_prop path pname ret_annots
loc ret_id (Some ret_type) url_handled_args in loc ret_id (Some ret_type) url_handled_args in
match Specs.get_summary pname with match Specs.get_summary pname with
@ -1116,7 +1116,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
| resolved_pname :: _ -> resolved_pname | resolved_pname :: _ -> resolved_pname
| [] -> callee_pname in | [] -> callee_pname in
Ondemand.analyze_proc_name Ondemand.analyze_proc_name
tenv ~propagate_exceptions:true current_pdesc resolved_pname; ~propagate_exceptions:true current_pdesc resolved_pname;
let callee_pdesc_opt = Ondemand.get_proc_desc resolved_pname in let callee_pdesc_opt = Ondemand.get_proc_desc resolved_pname in
let ret_typ_opt = Option.map Procdesc.get_ret_type callee_pdesc_opt in let ret_typ_opt = Option.map Procdesc.get_ret_type callee_pdesc_opt in
let sentinel_result = let sentinel_result =

@ -77,11 +77,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
module Domain = Domain module Domain = Domain
type extras = extras_t type extras = extras_t
let stacktree_of_astate tenv pdesc astate loc location_type get_proc_desc = let stacktree_of_astate pdesc astate loc location_type get_proc_desc =
let procs = Domain.elements astate in let procs = Domain.elements astate in
let callees = IList.map let callees = IList.map
(fun pn -> (fun pn ->
match SpecSummary.read_summary tenv pdesc pn with match SpecSummary.read_summary pdesc pn with
| None | Some None -> (match get_proc_desc pn with | None | Some None -> (match get_proc_desc pn with
| None -> stacktree_stub_of_procname pn | None -> stacktree_stub_of_procname pn
(* This can happen when the callee is in the same cluster/ buck (* This can happen when the callee is in the same cluster/ buck
@ -94,10 +94,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
procs in procs in
stacktree_of_pdesc pdesc ~loc ~callees location_type stacktree_of_pdesc pdesc ~loc ~callees location_type
let output_json_summary tenv pdesc astate loc location_type get_proc_desc = let output_json_summary pdesc astate loc location_type get_proc_desc =
let caller = Procdesc.get_proc_name pdesc in let caller = Procdesc.get_proc_name pdesc in
let stacktree = let stacktree = stacktree_of_astate pdesc astate loc location_type get_proc_desc in
stacktree_of_astate tenv pdesc astate loc location_type get_proc_desc in
let dir = Filename.concat Config.results_dir "crashcontext" in let dir = Filename.concat Config.results_dir "crashcontext" in
let suffix = F.sprintf "%s_%d" location_type loc.Location.line in let suffix = F.sprintf "%s_%d" location_type loc.Location.line in
let fname = F.sprintf "%s.%s.json" let fname = F.sprintf "%s.%s.json"
@ -111,7 +110,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Sil.Call (_, Const (Const.Cfun pn), _, loc, _) -> | Sil.Call (_, Const (Const.Cfun pn), _, loc, _) ->
let get_proc_desc = proc_data.ProcData.extras.get_proc_desc in let get_proc_desc = proc_data.ProcData.extras.get_proc_desc in
let traces = proc_data.ProcData.extras.stacktraces in let traces = proc_data.ProcData.extras.stacktraces in
let tenv = proc_data.ProcData.tenv in
let caller = Procdesc.get_proc_name proc_data.ProcData.pdesc in let caller = Procdesc.get_proc_name proc_data.ProcData.pdesc in
let matches_proc frame = let matches_proc frame =
let matches_class pname = match pname with let matches_class pname = match pname with
@ -136,7 +134,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let new_astate = Domain.add pn astate in let new_astate = Domain.add pn astate in
if Stacktrace.frame_matches_location frame loc then begin if Stacktrace.frame_matches_location frame loc then begin
let pdesc = proc_data.ProcData.pdesc in let pdesc = proc_data.ProcData.pdesc in
output_json_summary tenv pdesc new_astate loc "call_site" get_proc_desc output_json_summary pdesc new_astate loc "call_site" get_proc_desc
end; end;
new_astate new_astate
with with

@ -54,7 +54,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let at_least_bottom = let at_least_bottom =
Domain.join (Domain.NonBottom SiofTrace.initial) Domain.join (Domain.NonBottom SiofTrace.initial)
let exec_instr astate { ProcData.pdesc; tenv } _ (instr : Sil.instr) = match instr with let exec_instr astate { ProcData.pdesc; } _ (instr : Sil.instr) = match instr with
| Load (_, exp, _, loc) | Load (_, exp, _, loc)
| Store (_, _, exp, loc) | Store (_, _, exp, loc)
| Prune (exp, loc, _, _) -> | Prune (exp, loc, _, _) ->
@ -62,7 +62,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Call (_, Const (Cfun callee_pname), params, loc, _) -> | Call (_, Const (Cfun callee_pname), params, loc, _) ->
let callsite = CallSite.make callee_pname loc in let callsite = CallSite.make callee_pname loc in
let callee_globals = let callee_globals =
match Summary.read_summary tenv pdesc callee_pname with match Summary.read_summary pdesc callee_pname with
| Some (Domain.NonBottom trace) -> | Some (Domain.NonBottom trace) ->
Domain.NonBottom (SiofTrace.with_callsite trace callsite) Domain.NonBottom (SiofTrace.with_callsite trace callsite)
| _ -> | _ ->
@ -98,12 +98,12 @@ let is_foreign tu_opt v =
| None -> assert false in | None -> assert false in
Option.map_default (fun f -> not (is_orig_file f)) false (Pvar.get_source_file v) Option.map_default (fun f -> not (is_orig_file f)) false (Pvar.get_source_file v)
let report_siof tenv trace pdesc gname loc = let report_siof trace pdesc gname loc =
let tu_opt = let tu_opt =
let attrs = Procdesc.get_attributes pdesc in let attrs = Procdesc.get_attributes pdesc in
attrs.ProcAttributes.translation_unit in attrs.ProcAttributes.translation_unit in
let trace_of_pname pname = let trace_of_pname pname =
match Summary.read_summary tenv pdesc pname with match Summary.read_summary pdesc pname with
| Some (SiofDomain.NonBottom summary) -> summary | Some (SiofDomain.NonBottom summary) -> summary
| _ -> SiofTrace.initial in | _ -> SiofTrace.initial in
@ -147,7 +147,7 @@ let report_siof tenv trace pdesc gname loc =
IList.iter report_one_path (SiofTrace.get_reportable_sink_paths trace ~trace_of_pname) IList.iter report_one_path (SiofTrace.get_reportable_sink_paths trace ~trace_of_pname)
let siof_check tenv pdesc gname = function let siof_check pdesc gname = function
| Some (SiofDomain.NonBottom post) -> | Some (SiofDomain.NonBottom post) ->
let attrs = Procdesc.get_attributes pdesc in let attrs = Procdesc.get_attributes pdesc in
let foreign_global_sinks = let foreign_global_sinks =
@ -155,15 +155,15 @@ let siof_check tenv pdesc gname = function
(fun sink -> is_foreign attrs.ProcAttributes.translation_unit (SiofTrace.Sink.kind sink)) (fun sink -> is_foreign attrs.ProcAttributes.translation_unit (SiofTrace.Sink.kind sink))
(SiofTrace.sinks post) in (SiofTrace.sinks post) in
if not (SiofTrace.Sinks.is_empty foreign_global_sinks) if not (SiofTrace.Sinks.is_empty foreign_global_sinks)
then report_siof tenv post pdesc gname attrs.ProcAttributes.loc; then report_siof post pdesc gname attrs.ProcAttributes.loc;
| Some SiofDomain.Bottom | None -> | Some SiofDomain.Bottom | None ->
() ()
let checker ({ Callbacks.tenv; proc_desc } as callback) = let checker ({ Callbacks.proc_desc; } as callback) =
let post = Interprocedural.checker callback ProcData.empty_extras in let post = Interprocedural.checker callback ProcData.empty_extras in
let pname = Procdesc.get_proc_name proc_desc in let pname = Procdesc.get_proc_name proc_desc in
match Procname.get_global_name_of_initializer pname with match Procname.get_global_name_of_initializer pname with
| Some gname -> | Some gname ->
siof_check tenv proc_desc gname post siof_check proc_desc gname post
| None -> | None ->
() ()

@ -63,7 +63,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
pathdomainstate pathdomainstate
(AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None)) (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None))
let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; tenv } _ = let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ =
let is_unprotected is_locked = let is_unprotected is_locked =
not is_locked && not (Procdesc.is_java_synchronized pdesc) in not is_locked && not (Procdesc.is_java_synchronized pdesc) in
function function
@ -77,7 +77,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
false, snd astate false, snd astate
| None -> | None ->
begin begin
match Summary.read_summary tenv pdesc pn with match Summary.read_summary pdesc pn with
| Some ((callee_lockstate, _) as summary) -> | Some ((callee_lockstate, _) as summary) ->
let lockstate' = callee_lockstate || lockstate in let lockstate' = callee_lockstate || lockstate in
let _, read_writestate' = let _, read_writestate' =

@ -155,7 +155,7 @@ module MakeNoCFG
post_opt post_opt
end end
else else
Summ.read_summary tenv proc_desc proc_name Summ.read_summary proc_desc proc_name
end end
end end

@ -321,7 +321,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let call_site = CallSite.make callee_pname call_loc in let call_site = CallSite.make callee_pname call_loc in
begin begin
(* Runs the analysis of callee_pname if not already analyzed *) (* Runs the analysis of callee_pname if not already analyzed *)
match Summary.read_summary tenv pdesc callee_pname with match Summary.read_summary pdesc callee_pname with
| Some Domain.NonBottom (call_map, _) -> | Some Domain.NonBottom (call_map, _) ->
add_call call_map tenv callee_pname caller_pname call_site astate add_call call_map tenv callee_pname caller_pname call_site astate
| None -> | None ->

@ -55,13 +55,13 @@ module ST = struct
end end
end end
let store_summary tenv proc_name = let store_summary proc_name =
Option.may Option.may
(fun summary -> (fun summary ->
let summary' = let summary' =
{ summary with { summary with
Specs.timestamp = summary.Specs.timestamp + 1 } in Specs.timestamp = summary.Specs.timestamp + 1 } in
try Specs.store_summary tenv proc_name summary' with Sys_error s -> L.err "%s@." s) try Specs.store_summary proc_name summary' with Sys_error s -> L.err "%s@." s)
(Specs.get_summary proc_name) (Specs.get_summary proc_name)
let report_error tenv let report_error tenv

@ -36,7 +36,7 @@ module ST : sig
unit unit
(** Store the summary to a .specs file. *) (** Store the summary to a .specs file. *)
val store_summary : Tenv.t -> Procname.t -> unit val store_summary : Procname.t -> unit
end (* ST *) end (* ST *)

@ -25,7 +25,7 @@ module type S = sig
val write_summary : Procname.t -> summary -> unit val write_summary : Procname.t -> summary -> unit
(* read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis to (* read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis to
create the summary if needed *) create the summary if needed *)
val read_summary : Tenv.t -> Procdesc.t -> Procname.t -> summary option val read_summary : Procdesc.t -> Procname.t -> summary option
end end
module Make (H : Helper) = struct module Make (H : Helper) = struct
@ -40,8 +40,8 @@ module Make (H : Helper) = struct
| None -> | None ->
failwithf "Summary for %a should exist, but does not!@." Procname.pp pname failwithf "Summary for %a should exist, but does not!@." Procname.pp pname
let read_summary tenv caller_pdesc callee_pname = let read_summary caller_pdesc callee_pname =
Ondemand.analyze_proc_name tenv ~propagate_exceptions:false caller_pdesc callee_pname; Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc callee_pname;
match Specs.get_summary callee_pname with match Specs.get_summary callee_pname with
| None -> None | None -> None
| Some summary -> H.read_from_payload summary.Specs.payload | Some summary -> H.read_from_payload summary.Specs.payload

@ -563,7 +563,7 @@ let typecheck_instr
loc, loc,
cflags) cflags)
-> ->
Ondemand.analyze_proc_name tenv ~propagate_exceptions:true curr_pdesc callee_pname; Ondemand.analyze_proc_name ~propagate_exceptions:true curr_pdesc callee_pname;
let callee_attributes = let callee_attributes =
match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with
| Some proc_attributes -> | Some proc_attributes ->

@ -156,7 +156,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
(* log any reportable source-sink flows in [trace] and remove logged sinks from the trace *) (* log any reportable source-sink flows in [trace] and remove logged sinks from the trace *)
let report_and_filter_trace trace callee_site (proc_data : formal_map ProcData.t) = let report_and_filter_trace trace callee_site (proc_data : formal_map ProcData.t) =
let trace_of_pname pname = let trace_of_pname pname =
match Summary.read_summary proc_data.tenv proc_data.pdesc pname with match Summary.read_summary proc_data.pdesc pname with
| Some summary -> | Some summary ->
let join_output_trace acc { QuandarySummary.output_trace; } = let join_output_trace acc { QuandarySummary.output_trace; } =
TraceDomain.join (TaintSpecification.of_summary_trace output_trace) acc in TraceDomain.join (TaintSpecification.of_summary_trace output_trace) acc in
@ -434,7 +434,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
(* don't use a summary for a procedure that is a direct source or sink *) (* don't use a summary for a procedure that is a direct source or sink *)
astate_with_source astate_with_source
else else
match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with match Summary.read_summary proc_data.pdesc callee_pname with
| Some summary -> | Some summary ->
apply_summary ret actuals summary astate_with_source proc_data call_site apply_summary ret actuals summary astate_with_source proc_data call_site
| None -> | None ->

Loading…
Cancel
Save