[infer][scheduler] simplify the callbacks API

Summary:
- changes the `Ondemand` callbacks to take the execution environment instead of a `get_proc_desc` function.
- removes all the cases passing `get_proc_desc` as parameter to use `Ondemand.get_proc_desc` instead.

Reviewed By: jvillard

Differential Revision: D9200583

fbshipit-source-id: d16c218b5
master
Jeremy Dubreil 6 years ago committed by Facebook Github Bot
parent 632cb0e513
commit 3767716c86

@ -11,8 +11,7 @@ module F = Format
(** Module to register and invoke callbacks *)
type proc_callback_args =
{ get_proc_desc: Typ.Procname.t -> Procdesc.t option
; get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
{ get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
; tenv: Tenv.t
; summary: Summary.t
; proc_desc: Procdesc.t
@ -21,10 +20,7 @@ type proc_callback_args =
type proc_callback_t = proc_callback_args -> Summary.t
type cluster_callback_args =
{ procedures: (Tenv.t * Procdesc.t) list
; source_file: SourceFile.t
; get_proc_desc: Typ.Procname.t -> Procdesc.t option
; exe_env: Exe_env.t }
{procedures: (Tenv.t * Procdesc.t) list; source_file: SourceFile.t; exe_env: Exe_env.t}
type cluster_callback_t = cluster_callback_args -> unit
@ -54,7 +50,7 @@ let get_procedure_definition exe_env proc_name =
(** Invoke all registered procedure callbacks on the given procedure. *)
let iterate_procedure_callbacks get_proc_desc exe_env summary proc_desc =
let iterate_procedure_callbacks exe_env summary proc_desc =
let proc_name = Procdesc.get_proc_name proc_desc in
let procedure_language = Typ.Procname.get_language proc_name in
Language.curr_language := procedure_language ;
@ -70,16 +66,16 @@ let iterate_procedure_callbacks get_proc_desc exe_env summary proc_desc =
List.fold ~init:summary
~f:(fun summary {dynamic_dispatch; language; callback} ->
if Language.equal language procedure_language && (dynamic_dispatch || not is_specialized)
then callback {get_proc_desc; get_procs_in_file; tenv; summary; proc_desc; exe_env}
then callback {get_procs_in_file; tenv; summary; proc_desc; exe_env}
else summary )
!procedure_callbacks
(** Invoke all registered cluster callbacks on a cluster of procedures. *)
let iterate_cluster_callbacks all_procs exe_env source_file get_proc_desc =
let iterate_cluster_callbacks all_procs exe_env source_file =
if !cluster_callbacks <> [] then
let procedures = List.filter_map ~f:(get_procedure_definition exe_env) all_procs in
let environment = {procedures; source_file; get_proc_desc; exe_env} in
let environment = {procedures; source_file; exe_env} in
let language_matches language =
match procedures with
| (_, pdesc) :: _ ->
@ -128,18 +124,9 @@ let create_perf_stats_report source_file =
(** Invoke all procedure and cluster callbacks on a given environment. *)
let analyze_file (exe_env: Exe_env.t) source_file =
let saved_language = !Language.curr_language in
let get_proc_desc proc_name =
match Exe_env.get_proc_desc exe_env proc_name with
| Some _ as pdesc_opt ->
pdesc_opt
| None ->
Option.map ~f:Summary.get_proc_desc (Summary.get proc_name)
in
let analyze_ondemand summary proc_desc =
iterate_procedure_callbacks get_proc_desc exe_env summary proc_desc
in
Ondemand.set_callbacks {Ondemand.analyze_ondemand; get_proc_desc} ;
let analyze_ondemand summary proc_desc = iterate_procedure_callbacks exe_env summary proc_desc in
(* Invoke procedure callbacks using on-demand analysis schedulling *)
Ondemand.set_callbacks {Ondemand.exe_env; analyze_ondemand} ;
let procs_to_analyze =
(* analyze all the currently defined procedures *)
SourceFiles.proc_names_of_source source_file
@ -148,7 +135,7 @@ let analyze_file (exe_env: Exe_env.t) source_file =
let analyze_proc_name pname = ignore (Ondemand.analyze_proc_name pname : Summary.t option) in
List.iter ~f:analyze_proc_name procs_to_analyze ;
(* Invoke cluster callbacks. *)
iterate_cluster_callbacks procs_to_analyze exe_env source_file get_proc_desc ;
iterate_cluster_callbacks procs_to_analyze exe_env source_file ;
(* Perf logging needs to remain at the end - after analysis work is complete *)
create_perf_stats_report source_file ;
(* Unregister callbacks *)

@ -10,8 +10,7 @@ open! IStd
(** Module to register and invoke callbacks *)
type proc_callback_args =
{ get_proc_desc: Typ.Procname.t -> Procdesc.t option
; get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
{ get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
; tenv: Tenv.t
; summary: Summary.t
; proc_desc: Procdesc.t
@ -27,7 +26,6 @@ type proc_callback_t = proc_callback_args -> Summary.t
type cluster_callback_args =
{ procedures: (Tenv.t * Procdesc.t) list
; source_file: SourceFile.t
; get_proc_desc: Typ.Procname.t -> Procdesc.t option
; exe_env: Exe_env.t }
type cluster_callback_t = cluster_callback_args -> unit

@ -14,9 +14,7 @@ module F = Format
type analyze_ondemand = Summary.t -> Procdesc.t -> Summary.t
type get_proc_desc = Typ.Procname.t -> Procdesc.t option
type callbacks = {analyze_ondemand: analyze_ondemand; get_proc_desc: get_proc_desc}
type callbacks = {exe_env: Exe_env.t; analyze_ondemand: analyze_ondemand}
let callbacks_ref = ref None
@ -224,6 +222,16 @@ let analyze_proc_desc ~caller_pdesc callee_pdesc =
summary_option
(** Find a proc desc for the procedure, perhaps loading it from disk. *)
let get_proc_desc callee_pname =
let callbacks = Option.value_exn !callbacks_ref in
match Exe_env.get_proc_desc callbacks.exe_env callee_pname with
| Some _ as pdesc_opt ->
pdesc_opt
| None ->
Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname)
(** analyze_proc_name ?caller_pdesc proc_name performs an on-demand analysis of proc_name triggered
during the analysis of caller_pdesc *)
let analyze_proc_name ?caller_pdesc callee_pname =
@ -232,9 +240,8 @@ let analyze_proc_name ?caller_pdesc callee_pname =
let cache = Lazy.force cached_results in
try Typ.Procname.Hash.find cache callee_pname with Caml.Not_found ->
let summary_option =
let callbacks = Option.value_exn !callbacks_ref in
if procedure_should_be_analyzed callee_pname then
match callbacks.get_proc_desc callee_pname with
match get_proc_desc callee_pname with
| Some callee_pdesc ->
analyze_proc ?caller_pdesc callee_pdesc
| None ->
@ -246,8 +253,3 @@ let analyze_proc_name ?caller_pdesc callee_pname =
let clear_cache () = Typ.Procname.Hash.clear (Lazy.force cached_results)
(** Find a proc desc for the procedure, perhaps loading it from disk. *)
let get_proc_desc callee_pname =
let callbacks = Option.value_exn !callbacks_ref in
callbacks.get_proc_desc callee_pname

@ -11,11 +11,9 @@ open! IStd
type analyze_ondemand = Summary.t -> Procdesc.t -> Summary.t
type get_proc_desc = Typ.Procname.t -> Procdesc.t option
type callbacks = {exe_env: Exe_env.t; analyze_ondemand: analyze_ondemand}
type callbacks = {analyze_ondemand: analyze_ondemand; get_proc_desc: get_proc_desc}
val get_proc_desc : get_proc_desc
val get_proc_desc : Typ.Procname.t -> Procdesc.t option
(** Find a proc desc for the procedure, perhaps loading it from disk. *)
val analyze_proc_desc : caller_pdesc:Procdesc.t -> Procdesc.t -> Summary.t option

@ -25,7 +25,7 @@ module SpecPayload = SummaryPayload.Make (struct
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}
type extras_t = {stacktraces: Stacktrace.t list}
let line_range_of_pdesc pdesc =
let ploc = Procdesc.get_loc pdesc in
@ -60,14 +60,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
type extras = extras_t
let stacktree_of_astate pdesc astate loc location_type get_proc_desc =
let stacktree_of_astate pdesc astate loc location_type =
let procs = Domain.elements astate in
let callees =
List.map
~f:(fun pn ->
match SpecPayload.read pdesc pn with
| None -> (
match get_proc_desc pn with
match Ondemand.get_proc_desc pn with
| None ->
stacktree_stub_of_procname pn
(* This can happen when the callee is in the same cluster/ buck
@ -83,9 +83,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
stacktree_of_pdesc pdesc ~loc ~callees location_type
let output_json_summary pdesc astate loc location_type get_proc_desc =
let output_json_summary pdesc astate loc location_type =
let caller = Procdesc.get_proc_name pdesc in
let stacktree = stacktree_of_astate pdesc astate loc location_type get_proc_desc in
let stacktree = stacktree_of_astate pdesc astate loc location_type in
let dir = Filename.concat Config.results_dir "crashcontext" in
let suffix = F.sprintf "%s_%d" location_type loc.Location.line in
let fname = F.sprintf "%s.%s.json" (Typ.Procname.to_filename caller) suffix in
@ -97,7 +97,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let exec_instr astate proc_data _ = function
| Sil.Call (_, Const (Const.Cfun pn), _, loc, _)
-> (
let get_proc_desc = proc_data.ProcData.extras.get_proc_desc in
let traces = proc_data.ProcData.extras.stacktraces in
let caller = Procdesc.get_proc_name proc_data.ProcData.pdesc in
let matches_proc frame =
@ -125,7 +124,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let new_astate = Domain.add pn astate in
( if Stacktrace.frame_matches_location frame loc then
let pdesc = proc_data.ProcData.pdesc in
output_json_summary pdesc new_astate loc "call_site" get_proc_desc ) ;
output_json_summary pdesc new_astate loc "call_site" ) ;
new_astate
| None ->
astate )
@ -169,7 +168,7 @@ let loaded_stacktraces =
Some (List.map ~f:Stacktrace.of_json_file files)
let checker {Callbacks.proc_desc; tenv; get_proc_desc; summary} : Summary.t =
let checker {Callbacks.proc_desc; tenv; summary} : Summary.t =
( match loaded_stacktraces with
| None ->
L.(die UserError)
@ -178,6 +177,6 @@ let checker {Callbacks.proc_desc; tenv; get_proc_desc; summary} : Summary.t =
stack trace or a directory containing multiple such traces, respectively. See \
tests/codetoanalyze/java/crashcontext/*.json for examples of the expected format."
| Some stacktraces ->
let extras = {get_proc_desc; stacktraces} in
let extras = {stacktraces} in
ignore (Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras) ~initial:Domain.empty) ) ;
summary

@ -22,7 +22,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG
module Domain = RacerDDomain
type extras = Typ.Procname.t -> Procdesc.t option
type extras = ProcData.no_extras
(* we don't want to warn on accesses to the field if it is (a) thread-confined, or
(b) volatile *)
@ -315,14 +315,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses
let call_without_summary get_proc_desc callee_pname ret_access_path call_flags actuals astate =
let call_without_summary callee_pname ret_access_path call_flags actuals astate =
let open RacerDConfig in
let open RacerDDomain in
let should_assume_returns_ownership (call_flags: CallFlags.t) actuals =
not call_flags.cf_interface && List.is_empty actuals
in
let is_abstract_getthis_like callee =
get_proc_desc callee
Ondemand.get_proc_desc callee
|> Option.value_map ~default:false ~f:(fun callee_pdesc ->
(Procdesc.get_attributes callee_pdesc).ProcAttributes.is_abstract
&&
@ -363,7 +363,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
else astate
let exec_instr (astate: Domain.astate) ({ProcData.tenv; extras; pdesc} as proc_data) _
let exec_instr (astate: Domain.astate) ({ProcData.tenv; pdesc} as proc_data) _
(instr: HilInstr.t) =
let open Domain in
let open RacerDConfig in
@ -438,7 +438,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate with attribute_map; threads= update_for_lock_use astate.threads}
| NoEffect ->
let summary_opt = get_summary pdesc callee_pname actuals loc tenv astate in
let callee_pdesc = extras callee_pname in
let callee_pdesc = Ondemand.get_proc_desc callee_pname in
match
Option.map summary_opt ~f:(fun summary ->
let rebased_accesses =
@ -479,8 +479,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in
{locks; threads; accesses; ownership; attribute_map; wobbly_paths}
| None ->
call_without_summary extras callee_pname ret_access_path call_flags actuals
astate
call_without_summary callee_pname ret_access_path call_flags actuals astate
in
let add_if_annotated predicate attribute attribute_map =
if PatternMatch.override_exists predicate tenv callee_pname then
@ -632,7 +631,7 @@ let empty_post : RacerDDomain.summary =
; wobbly_paths= RacerDDomain.StabilityDomain.empty }
let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
let open RacerDConfig in
let method_annotation = (Procdesc.get_attributes proc_desc).method_annotation in
let is_initializer tenv proc_name =
@ -641,7 +640,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
let open RacerDDomain in
if Models.should_analyze_proc proc_desc tenv then
let formal_map = FormalMap.make proc_desc in
let proc_data = ProcData.make proc_desc tenv get_proc_desc in
let proc_data = ProcData.make proc_desc tenv ProcData.empty_extras in
let initial =
let threads =
if

@ -289,13 +289,13 @@ let should_report pdesc =
L.(die InternalError "Not supposed to run on non-Java code.")
let fold_reportable_summaries (tenv, current_pdesc) get_proc_desc clazz ~init ~f =
let fold_reportable_summaries (tenv, current_pdesc) clazz ~init ~f =
let methods =
Tenv.lookup tenv clazz
|> Option.value_map ~default:[] ~f:(fun tstruct -> tstruct.Typ.Struct.methods)
in
let f acc mthd =
get_proc_desc mthd
Ondemand.get_proc_desc mthd
|> Option.value_map ~default:acc ~f:(fun other_pdesc ->
if should_report other_pdesc then
Payload.read current_pdesc mthd |> Option.map ~f:(fun payload -> (mthd, payload))
@ -312,7 +312,7 @@ let fold_reportable_summaries (tenv, current_pdesc) get_proc_desc clazz ~init ~f
inner class but this is no longer obvious in the path, because of nested-class path normalisation.
The net effect of the above issues is that we will only see these locks in conflicting pairs
once, as opposed to twice with all other deadlock pairs. *)
let report_deadlocks env get_proc_desc {StarvationDomain.order; ui} report_map' =
let report_deadlocks env {StarvationDomain.order; ui} report_map' =
let open StarvationDomain in
let tenv, current_pdesc = env in
let current_pname = Procdesc.get_proc_name current_pdesc in
@ -371,7 +371,7 @@ let report_deadlocks env get_proc_desc {StarvationDomain.order; ui} report_map'
(* get the class of the root variable of the lock in the endpoint elem
and retrieve all the summaries of the methods of that class *)
(* for each summary related to the endpoint, analyse and report on its pairs *)
fold_reportable_summaries env get_proc_desc endpoint_class ~init:report_map ~f:
fold_reportable_summaries env endpoint_class ~init:report_map ~f:
(fun acc (endp_pname, endpoint_summary) ->
let endp_order = endpoint_summary.order in
let endp_ui = endpoint_summary.ui in
@ -382,7 +382,7 @@ let report_deadlocks env get_proc_desc {StarvationDomain.order; ui} report_map'
OrderDomain.fold report_on_current_elem order report_map'
let report_starvation env get_proc_desc {StarvationDomain.events; ui} report_map' =
let report_starvation env {StarvationDomain.events; ui} report_map' =
let open StarvationDomain in
let tenv, current_pdesc = env in
let current_pname = Procdesc.get_proc_name current_pdesc in
@ -422,7 +422,7 @@ let report_starvation env get_proc_desc {StarvationDomain.events; ui} report_map
(* get the class of the root variable of the lock in the endpoint elem
and retrieve all the summaries of the methods of that class *)
(* for each summary related to the endpoint, analyse and report on its pairs *)
fold_reportable_summaries env get_proc_desc endpoint_class ~init:report_map ~f:
fold_reportable_summaries env endpoint_class ~init:report_map ~f:
(fun acc (endpoint_pname, {order; ui}) ->
(* skip methods known to run on ui thread, as they cannot run in parallel to us *)
if UIThreadDomain.is_empty ui then
@ -438,14 +438,14 @@ let report_starvation env get_proc_desc {StarvationDomain.events; ui} report_map
EventDomain.fold (report_on_current_elem ui_explain) events report_map'
let reporting {Callbacks.procedures; source_file; get_proc_desc} =
let reporting {Callbacks.procedures; source_file} =
let report_procedure ((_, proc_desc) as env) =
die_if_not_java proc_desc ;
if should_report proc_desc then
Payload.read proc_desc (Procdesc.get_proc_name proc_desc)
|> Option.iter ~f:(fun summary ->
report_deadlocks env get_proc_desc summary ReportMap.empty
|> report_starvation env get_proc_desc summary |> ReportMap.log )
report_deadlocks env summary ReportMap.empty |> report_starvation env summary
|> ReportMap.log )
in
List.iter procedures ~f:report_procedure ;
IssueLog.store Config.starvation_issues_dir_name source_file

@ -36,9 +36,8 @@ end
(** Create a module with the toplevel callback. *)
module MkCallback (Extension : ExtensionT) : CallBackT = struct
let callback1 tenv find_canonical_duplicate calls_this checks get_proc_desc idenv curr_pname
curr_pdesc annotated_signature linereader proc_loc
: bool * Extension.extension TypeState.t option =
let callback1 tenv find_canonical_duplicate calls_this checks idenv curr_pname curr_pdesc
annotated_signature linereader proc_loc : bool * Extension.extension TypeState.t option =
let mk s = Pvar.mk s curr_pname in
let add_formal typestate (s, ia, typ) =
let pvar = mk s in
@ -94,9 +93,8 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
NodePrinter.start_session ~pp_name node ;
State.set_node node ;
let typestates_succ, typestates_exn =
TypeCheck.typecheck_node tenv Extension.ext calls_this checks idenv get_proc_desc
curr_pname curr_pdesc find_canonical_duplicate annotated_signature typestate node
linereader
TypeCheck.typecheck_node tenv Extension.ext calls_this checks idenv curr_pname curr_pdesc
find_canonical_duplicate annotated_signature typestate node linereader
in
if Config.write_html then (
let d_typestate ts = L.d_strln (F.asprintf "%a" (TypeState.pp Extension.ext) ts) in
@ -122,8 +120,8 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
let callback2 calls_this checks
{Callbacks.proc_desc= curr_pdesc; summary; get_proc_desc; tenv; get_procs_in_file}
annotated_signature linereader proc_loc : unit =
{Callbacks.proc_desc= curr_pdesc; summary; tenv; get_procs_in_file} annotated_signature
linereader proc_loc : unit =
let idenv = Idenv.create curr_pdesc in
let curr_pname = Summary.get_proc_name summary in
let find_duplicate_nodes = State.mk_find_duplicate_nodes curr_pdesc in
@ -147,8 +145,8 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
if do_checks then (checks, calls_this)
else ({TypeCheck.eradicate= false; check_extension= false; check_ret_type= []}, ref false)
in
callback1 tenv find_canonical_duplicate calls_this' checks' get_proc_desc idenv_pn pname
pdesc ann_sig linereader loc
callback1 tenv find_canonical_duplicate calls_this' checks' idenv_pn pname pdesc ann_sig
linereader loc
in
let module Initializers = struct
type init = Typ.Procname.t * Procdesc.t
@ -180,7 +178,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
PatternMatch.proc_calls Summary.proc_resolve_attributes init_pd filter
in
let do_called (callee_pn, _) =
match get_proc_desc callee_pn with
match Ondemand.get_proc_desc callee_pn with
| Some callee_pd ->
res := (callee_pn, callee_pd) :: !res
| None ->
@ -234,7 +232,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
in
let do_proc pname =
if filter pname then
match get_proc_desc pname with
match Ondemand.get_proc_desc pname with
| Some pdesc ->
res := (pname, pdesc) :: !res
| None ->
@ -357,7 +355,7 @@ module EmptyExtension : ExtensionT = struct
let ext =
let empty = () in
let check_instr _ _ _ _ ext _ _ = ext in
let check_instr _ _ _ ext _ _ = ext in
let join () () = () in
let pp _ () = () in
{TypeState.empty; check_instr; join; pp}

@ -136,8 +136,6 @@ type check_return_type =
type find_canonical_duplicate = Procdesc.Node.t -> Procdesc.Node.t
type get_proc_desc = TypeState.get_proc_desc
type checks = {eradicate: bool; check_extension: bool; check_ret_type: check_return_type list}
(** Typecheck an expression. *)
@ -206,9 +204,8 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r
(** Typecheck an instruction. *)
let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get_proc_desc
curr_pname curr_pdesc find_canonical_duplicate annotated_signature instr_ref linereader
typestate instr =
let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv curr_pname curr_pdesc
find_canonical_duplicate annotated_signature instr_ref linereader typestate instr =
(* let print_current_state () = *)
(* L.stdout "Current Typestate in node %a@\n%a@." *)
(* Procdesc.Node.pp (TypeErr.InstrRef.get_node instr_ref) *)
@ -834,8 +831,7 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get
let etl' = List.map ~f:(fun ((_, e), t) -> (e, t)) call_params in
let extension = TypeState.get_extension typestate1 in
let extension' =
ext.TypeState.check_instr tenv get_proc_desc curr_pname curr_pdesc extension
instr etl'
ext.TypeState.check_instr tenv curr_pname curr_pdesc extension instr etl'
in
TypeState.set_extension typestate1 extension'
else typestate1
@ -1072,8 +1068,8 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get
(** Typecheck the instructions in a cfg node. *)
let typecheck_node tenv ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc
find_canonical_duplicate annotated_signature typestate node linereader =
let typecheck_node tenv ext calls_this checks idenv curr_pname curr_pdesc find_canonical_duplicate
annotated_signature typestate node linereader =
let instrs = Procdesc.Node.get_instrs node in
let instr_ref_gen = TypeErr.InstrRef.create_generator node in
let typestates_exn = ref [] in
@ -1109,7 +1105,7 @@ let typecheck_node tenv ext calls_this checks idenv get_proc_desc curr_pname cur
TypeErr.InstrRef.gen instr_ref_gen
in
let instr' =
typecheck_instr tenv ext calls_this checks node idenv get_proc_desc curr_pname curr_pdesc
typecheck_instr tenv ext calls_this checks node idenv curr_pname curr_pdesc
find_canonical_duplicate annotated_signature instr_ref linereader typestate instr
in
handle_exceptions typestate instr ; instr'

@ -14,11 +14,9 @@ type check_return_type =
type find_canonical_duplicate = Procdesc.Node.t -> Procdesc.Node.t
type get_proc_desc = TypeState.get_proc_desc
type checks = {eradicate: bool; check_extension: bool; check_ret_type: check_return_type list}
val typecheck_node :
Tenv.t -> 'a TypeState.ext -> bool ref -> checks -> Idenv.t -> get_proc_desc -> Typ.Procname.t
-> Procdesc.t -> find_canonical_duplicate -> AnnotatedSignature.t -> 'a TypeState.t
-> Procdesc.Node.t -> Printer.LineReader.t -> 'a TypeState.t list * 'a TypeState.t list
Tenv.t -> 'a TypeState.ext -> bool ref -> checks -> Idenv.t -> Typ.Procname.t -> Procdesc.t
-> find_canonical_duplicate -> AnnotatedSignature.t -> 'a TypeState.t -> Procdesc.Node.t
-> Printer.LineReader.t -> 'a TypeState.t list * 'a TypeState.t list

@ -14,23 +14,16 @@ module F = Format
(** Parameters of a call. *)
type parameters = (Exp.t * Typ.t) list
type get_proc_desc = Typ.Procname.t -> Procdesc.t option
(** Extension to a typestate with values of type 'a. *)
type 'a ext =
{ empty: 'a (** empty extension *)
; check_instr:
Tenv.t -> get_proc_desc -> Typ.Procname.t -> Procdesc.t -> 'a -> Sil.instr -> parameters
-> 'a
; check_instr: Tenv.t -> Typ.Procname.t -> Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a
(** check the extension for an instruction *)
; join: 'a -> 'a -> 'a (** join two extensions *)
; pp: Format.formatter -> 'a -> unit (** pretty print an extension *) }
let unit_ext : unit ext =
{ empty= ()
; check_instr= (fun _ _ _ _ () _ _ -> ())
; join= (fun () () -> ())
; pp= (fun _ () -> ()) }
{empty= (); check_instr= (fun _ _ _ () _ _ -> ()); join= (fun () () -> ()); pp= (fun _ () -> ())}
module M = Caml.Map.Make (struct

@ -12,14 +12,10 @@ open! IStd
(** Parameters of a call. *)
type parameters = (Exp.t * Typ.t) list
type get_proc_desc = Typ.Procname.t -> Procdesc.t option
(** Extension to a typestate with values of type 'a. *)
type 'a ext =
{ empty: 'a (** empty extension *)
; check_instr:
Tenv.t -> get_proc_desc -> Typ.Procname.t -> Procdesc.t -> 'a -> Sil.instr -> parameters
-> 'a
; check_instr: Tenv.t -> Typ.Procname.t -> Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a
(** check the extension for an instruction *)
; join: 'a -> 'a -> 'a (** join two extensions *)
; pp: Format.formatter -> 'a -> unit (** pretty print an extension *) }

@ -9,8 +9,6 @@ open! IStd
module TestInterpreter =
AnalyzerTester.Make (ProcCfg.Exceptional) (BoundedCallTree.TransferFunctions)
let mock_get_proc_desc _ = None
let tests =
let open OUnit2 in
let open AnalyzerTester.StructuredSil in
@ -26,7 +24,7 @@ let tests =
[ Stacktrace.make_frame class_name "foo" file_name (Some 16)
; Stacktrace.make_frame class_name "bar" file_name (Some 20) ]
in
let extras = {BoundedCallTree.get_proc_desc= mock_get_proc_desc; stacktraces= [trace]} in
let extras = {BoundedCallTree.stacktraces= [trace]} in
let multi_trace_1 =
Stacktrace.make "java.lang.NullPointerException"
[Stacktrace.make_frame class_name "foo" file_name (Some 16)]
@ -35,9 +33,7 @@ let tests =
Stacktrace.make "java.lang.NullPointerException"
[Stacktrace.make_frame class_name "bar" file_name (Some 20)]
in
let multi_trace_extras =
{BoundedCallTree.get_proc_desc= mock_get_proc_desc; stacktraces= [multi_trace_1; multi_trace_2]}
in
let multi_trace_extras = {BoundedCallTree.stacktraces= [multi_trace_1; multi_trace_2]} in
let caller_foo_name = Typ.Procname.from_string_c_fun "foo" in
let caller_bar_name = Typ.Procname.from_string_c_fun "bar" in
let caller_baz_name = Typ.Procname.from_string_c_fun "baz" in

@ -118,8 +118,7 @@ let tests =
let assert_empty = invariant "{ }" in
(* hack: register an empty analyze_ondemand to prevent a crash because the callback is unset *)
let analyze_ondemand summary _ = summary in
let get_proc_desc _ = None in
let callbacks = {Ondemand.analyze_ondemand; get_proc_desc} in
let callbacks = {Ondemand.exe_env= Exe_env.mk (); analyze_ondemand} in
Ondemand.set_callbacks callbacks ;
let test_list =
[ ("source recorded", [assign_to_source "ret_id"; invariant "{ ret_id$0* => (SOURCE -> ?) }"])

Loading…
Cancel
Save