Refactor callbacks for Eradicate and Checkers.

Reviewed By: sblackshear

Differential Revision: D2911784

fb-gh-sync-id: cc01b4a
shipit-source-id: cc01b4a
master
Cristiano Calcagno 9 years ago committed by facebook-github-bot-7
parent c65947439f
commit 047eec5a6f

@ -373,7 +373,7 @@ class Infer:
infer_options += ['-allow_specs_cleanup'] infer_options += ['-allow_specs_cleanup']
if self.args.analyzer == config.ANALYZER_ERADICATE: if self.args.analyzer == config.ANALYZER_ERADICATE:
infer_options += ['-checkers', '-eradicate'] infer_options += ['-eradicate']
elif self.args.analyzer == config.ANALYZER_CHECKERS: elif self.args.analyzer == config.ANALYZER_CHECKERS:
infer_options += ['-checkers'] infer_options += ['-checkers']
else: else:

@ -12,14 +12,16 @@ module L = Logging
(** Module to register and invoke callbacks *) (** Module to register and invoke callbacks *)
type proc_callback_t = type proc_callback_args = {
Procname.t list -> get_proc_desc : Procname.t -> Cfg.Procdesc.t option;
(Procname.t -> Cfg.Procdesc.t option) -> get_procs_in_file : Procname.t -> Procname.t list;
Idenv.t -> idenv : Idenv.t;
Sil.tenv -> tenv : Sil.tenv;
Procname.t -> proc_name : Procname.t;
Cfg.Procdesc.t -> proc_desc : Cfg.Procdesc.t;
unit }
type proc_callback_t = proc_callback_args -> unit
type cluster_callback_t = type cluster_callback_t =
Procname.t list -> Procname.t list ->
@ -55,14 +57,18 @@ let get_procedure_definition exe_env proc_name =
let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.C_CPP let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.C_CPP
(** Invoke all registered procedure callbacks on a set of procedures. *) (** Invoke all registered procedure callbacks on a set of procedures. *)
let iterate_procedure_callbacks all_procs exe_env proc_name = let iterate_procedure_callbacks exe_env proc_name =
let procedure_language = get_language proc_name in let procedure_language = get_language proc_name in
Config.curr_language := procedure_language; Config.curr_language := procedure_language;
let cfg = Exe_env.get_cfg exe_env proc_name in let cfg = Exe_env.get_cfg exe_env proc_name in
let get_procdesc proc_name = let get_proc_desc proc_name =
let cfg = try Exe_env.get_cfg exe_env proc_name with Not_found -> cfg in let cfg = try Exe_env.get_cfg exe_env proc_name with Not_found -> cfg in
Cfg.Procdesc.find_from_name cfg proc_name in Cfg.Procdesc.find_from_name cfg proc_name in
let get_procs_in_file proc_name =
let cfg = try Exe_env.get_cfg exe_env proc_name with Not_found -> cfg in
IList.map Cfg.Procdesc.get_proc_name (Cfg.get_defined_procs cfg) in
let update_time proc_name elapsed = let update_time proc_name elapsed =
match Specs.get_summary proc_name with match Specs.get_summary proc_name with
@ -83,7 +89,15 @@ let iterate_procedure_callbacks all_procs exe_env proc_name =
if language_matches then if language_matches then
begin begin
let init_time = Unix.gettimeofday () in let init_time = Unix.gettimeofday () in
proc_callback all_procs get_procdesc idenv tenv proc_name proc_desc; proc_callback
{
get_proc_desc;
get_procs_in_file;
idenv;
tenv;
proc_name;
proc_desc;
};
let elapsed = Unix.gettimeofday () -. init_time in let elapsed = Unix.gettimeofday () -. init_time in
update_time proc_name elapsed update_time proc_name elapsed
end) end)
@ -160,7 +174,7 @@ let iterate_callbacks store_summary call_graph exe_env =
(* Invoke callbacks. *) (* Invoke callbacks. *)
IList.iter IList.iter
(iterate_procedure_callbacks originally_defined_procs exe_env) (iterate_procedure_callbacks exe_env)
procs_to_analyze; procs_to_analyze;
IList.iter IList.iter

@ -9,6 +9,14 @@
(** Module to register and invoke callbacks *) (** Module to register and invoke callbacks *)
type proc_callback_args = {
get_proc_desc : Procname.t -> Cfg.Procdesc.t option;
get_procs_in_file : Procname.t -> Procname.t list;
idenv : Idenv.t;
tenv : Sil.tenv;
proc_name : Procname.t;
proc_desc : Cfg.Procdesc.t;
}
(** Type of a procedure callback: (** Type of a procedure callback:
- List of all the procedures the callback will be called on. - List of all the procedures the callback will be called on.
@ -16,14 +24,7 @@
- Idenv to look up the definition of ids in a cfg. - Idenv to look up the definition of ids in a cfg.
- Type environment. - Type environment.
- Procedure for the callback to act on. *) - Procedure for the callback to act on. *)
type proc_callback_t = type proc_callback_t = proc_callback_args -> unit
Procname.t list ->
(Procname.t -> Cfg.Procdesc.t option) ->
Idenv.t ->
Sil.tenv ->
Procname.t ->
Cfg.Procdesc.t ->
unit
type cluster_callback_t = type cluster_callback_t =
Procname.t list -> Procname.t list ->

@ -250,7 +250,10 @@ let arg_desc =
" execute the code query" " execute the code query"
; ;
"-eradicate", "-eradicate",
Arg.Unit (fun () -> Config.eradicate := true; Config.intraprocedural := true), Arg.Unit (fun () ->
Config.eradicate := true;
checkers := true;
Config.intraprocedural := true),
None, None,
" activate the eradicate checker for java annotations" " activate the eradicate checker for java annotations"
; ;

@ -38,8 +38,6 @@ let get_or_create_lifecycle_typs tenv = match !android_lifecycle_typs with
lifecycle_typs lifecycle_typs
| typs -> typs | typs -> typs
let do_eradicate_check all_procs get_procdesc idenv tenv proc_name proc_desc =
Eradicate.callback_eradicate all_procs get_procdesc idenv tenv proc_name proc_desc
let num_methods_checked = ref 0 let num_methods_checked = ref 0
@ -49,21 +47,23 @@ let done_checking num_methods =
(** ask Eradicate to check each of the procs in [registered_callback_procs] (and their transitive (** ask Eradicate to check each of the procs in [registered_callback_procs] (and their transitive
* callees) in a context where each of the fields in [fields_nullifed] is marked as @Nullable *) * callees) in a context where each of the fields in [fields_nullifed] is marked as @Nullable *)
let do_eradicate_check all_procs get_procdesc idenv tenv = let do_eradicate_check ({ Callbacks.get_proc_desc } as callback_args) =
(* tell Eradicate to treat each of the fields nullified in on_destroy as nullable *) (* tell Eradicate to treat each of the fields nullified in on_destroy as nullable *)
FldSet.iter (fun fld -> Models.Inference.field_add_nullable_annotation fld) !fields_nullified; FldSet.iter (fun fld -> Models.Inference.field_add_nullable_annotation fld) !fields_nullified;
Procname.Set.iter Procname.Set.iter
(fun proc_name -> (fun proc_name ->
match get_procdesc proc_name with match get_proc_desc proc_name with
| Some proc_desc -> | Some proc_desc ->
do_eradicate_check all_procs get_procdesc idenv tenv proc_name proc_desc Eradicate.callback_eradicate
{ callback_args with Callbacks.proc_name; proc_desc }
| None -> ()) | None -> ())
!registered_callback_procs !registered_callback_procs
(** if [procname] belongs to an Android lifecycle type, save the set of callbacks registered in (** if [procname] belongs to an Android lifecycle type, save the set of callbacks registered in
* [procname]. in addition, if [procname] is a special "destroy" /"cleanup" method, save the set of * [procname]. in addition, if [procname] is a special "destroy" /"cleanup" method, save the set of
* fields that are nullified *) * fields that are nullified *)
let callback_checker_main all_procs get_procdesc idenv tenv proc_name proc_desc = let callback_checker_main
({ Callbacks.proc_desc; proc_name; tenv } as callback_args) =
let typename = let typename =
Typename.TN_csu Typename.TN_csu
(Csu.Class Csu.Java, Mangled.from_string (Procname.java_get_class proc_name)) in (Csu.Class Csu.Java, Mangled.from_string (Procname.java_get_class proc_name)) in
@ -99,5 +99,5 @@ let callback_checker_main all_procs get_procdesc idenv tenv proc_name proc_desc
fields_nullified := fields_nullified :=
FldSet.union (PatternMatch.get_fields_nullified proc_desc) !fields_nullified in FldSet.union (PatternMatch.get_fields_nullified proc_desc) !fields_nullified in
if done_checking (IList.length def_methods) then if done_checking (IList.length def_methods) then
do_eradicate_check all_procs get_procdesc idenv tenv do_eradicate_check callback_args
| _ -> () | _ -> ()

@ -88,13 +88,7 @@ let check_final_state proc_name proc_desc exit_node final_s =
end end
(** Simple check for dead code. *) (** Simple check for dead code. *)
let callback_check_dead_code let callback_check_dead_code { Callbacks.proc_desc; proc_name } =
(all_procs : Procname.t list)
(get_proc_desc: Procname.t -> Cfg.Procdesc.t option)
(idenv: Idenv.t)
(tenv: Sil.tenv)
(proc_name: Procname.t)
(proc_desc : Cfg.Procdesc.t) : unit =
let module DFDead = MakeDF(struct let module DFDead = MakeDF(struct
type t = State.t type t = State.t

@ -181,7 +181,7 @@ let report_calls_and_accesses callback node instr =
| None -> () | None -> ()
(** Report all field accesses and method calls of a procedure. *) (** Report all field accesses and method calls of a procedure. *)
let callback_check_access all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_check_access { Callbacks.proc_desc } =
Cfg.Procdesc.iter_instrs (report_calls_and_accesses "PROC") proc_desc Cfg.Procdesc.iter_instrs (report_calls_and_accesses "PROC") proc_desc
(** Report all field accesses and method calls of a class. *) (** Report all field accesses and method calls of a class. *)
@ -191,7 +191,7 @@ let callback_check_cluster_access all_procs get_proc_desc proc_definitions =
(IList.map get_proc_desc all_procs) (IList.map get_proc_desc all_procs)
(** Looks for writeToParcel methods and checks whether read is in reverse *) (** Looks for writeToParcel methods and checks whether read is in reverse *)
let callback_check_write_to_parcel all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_check_write_to_parcel { Callbacks.proc_desc; proc_name; idenv; get_proc_desc } =
let verbose = ref false in let verbose = ref false in
let is_write_to_parcel this_expr this_type = let is_write_to_parcel this_expr this_type =
@ -274,7 +274,7 @@ let callback_check_write_to_parcel all_procs get_proc_desc idenv tenv proc_name
Cfg.Procdesc.iter_instrs do_instr proc_desc Cfg.Procdesc.iter_instrs do_instr proc_desc
(** Monitor calls to Preconditions.checkNotNull and detect inconsistent uses. *) (** Monitor calls to Preconditions.checkNotNull and detect inconsistent uses. *)
let callback_monitor_nullcheck all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } =
let verbose = ref false in let verbose = ref false in
let class_formal_names = lazy ( let class_formal_names = lazy (
@ -341,11 +341,11 @@ let callback_monitor_nullcheck all_procs get_proc_desc idenv tenv proc_name proc
summary_checks_of_formals () summary_checks_of_formals ()
(** Test persistent state. *) (** Test persistent state. *)
let callback_test_state all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_test_state { Callbacks.proc_name } =
ST.pname_add proc_name "somekey" "somevalue" ST.pname_add proc_name "somekey" "somevalue"
(** Check the uses of VisibleForTesting *) (** Check the uses of VisibleForTesting *)
let callback_checkVisibleForTesting all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_checkVisibleForTesting { Callbacks.proc_desc } =
let ma = (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in let ma = (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in
if Annotations.ma_contains ma [Annotations.visibleForTesting] then if Annotations.ma_contains ma [Annotations.visibleForTesting] then
begin begin
@ -355,7 +355,7 @@ let callback_checkVisibleForTesting all_procs get_proc_desc idenv tenv proc_name
end end
(** Check for readValue and readValueAs json deserialization *) (** Check for readValue and readValueAs json deserialization *)
let callback_find_deserialization all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; proc_name } =
let verbose = true in let verbose = true in
let ret_const_key = "return_const" in let ret_const_key = "return_const" in
@ -448,7 +448,7 @@ let callback_find_deserialization all_procs get_proc_desc idenv tenv proc_name p
Cfg.Procdesc.iter_instrs do_instr proc_desc Cfg.Procdesc.iter_instrs do_instr proc_desc
(** Check field accesses. *) (** Check field accesses. *)
let callback_check_field_access all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_check_field_access { Callbacks.proc_desc } =
let rec do_exp is_read = function let rec do_exp is_read = function
| Sil.Var _ -> () | Sil.Var _ -> ()
| Sil.UnOp (_, e, _) -> | Sil.UnOp (_, e, _) ->
@ -491,7 +491,7 @@ let callback_check_field_access all_procs get_proc_desc idenv tenv proc_name pro
Cfg.Procdesc.iter_instrs do_instr proc_desc Cfg.Procdesc.iter_instrs do_instr proc_desc
(** Print c method calls. *) (** Print c method calls. *)
let callback_print_c_method_calls all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_print_c_method_calls { Callbacks.proc_desc; proc_name } =
let do_instr node = function let do_instr node = function
| Sil.Call (ret_ids, Sil.Const (Sil.Cfun pn), (e, t):: args, loc, cf) | Sil.Call (ret_ids, Sil.Const (Sil.Cfun pn), (e, t):: args, loc, cf)
when Procname.is_c_method pn -> when Procname.is_c_method pn ->

@ -204,7 +204,7 @@ module Match = struct
end end
let code_query_callback all_procs get_proc_desc idenv tenv proc_name proc_desc = let code_query_callback { Callbacks.proc_desc; idenv; proc_name } =
let do_instr node instr = let do_instr node instr =
let env = Match.init_env () in let env = Match.init_env () in
let _found = Match.match_query true env idenv node proc_name (Lazy.force query_ast) proc_name node instr in let _found = Match.match_query true env idenv node proc_name (Lazy.force query_ast) proc_name node instr in

@ -166,7 +166,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct
end (* MakeDF *) end (* MakeDF *)
(** Example dataflow callback: compute the the distance from a node to the start node. *) (** Example dataflow callback: compute the the distance from a node to the start node. *)
let callback_test_dataflow all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_test_dataflow { Callbacks.proc_desc } =
let verbose = false in let verbose = false in
let module DFCount = MakeDF(struct let module DFCount = MakeDF(struct
type t = int type t = int

@ -26,10 +26,10 @@ let report_error fld fld_typ pname pdesc =
let exn = Exceptions.Checkers (retained_view, Localise.verbatim_desc description) in let exn = Exceptions.Checkers (retained_view, Localise.verbatim_desc description) in
Reporting.log_error pname ~loc:(Some loc) exn Reporting.log_error pname ~loc:(Some loc) exn
let callback_fragment_retains_view all_procs get_procdesc idenv tenv pname pdesc = let callback_fragment_retains_view { Callbacks.proc_desc; proc_name; tenv } =
(* TODO: complain if onDestroyView is not defined, yet the Fragment has View fields *) (* TODO: complain if onDestroyView is not defined, yet the Fragment has View fields *)
(* TODO: handle fields nullified in callees in the same file *) (* TODO: handle fields nullified in callees in the same file *)
let is_on_destroy_view = Procname.java_get_method pname = "onDestroyView" in let is_on_destroy_view = Procname.java_get_method proc_name = "onDestroyView" in
(* this is needlessly complicated because field types are Tvars instead of Tstructs *) (* this is needlessly complicated because field types are Tvars instead of Tstructs *)
let fld_typ_is_view = function let fld_typ_is_view = function
| Sil.Tptr (Sil.Tvar tname, _) -> | Sil.Tptr (Sil.Tvar tname, _) ->
@ -45,18 +45,18 @@ let callback_fragment_retains_view all_procs get_procdesc idenv tenv pname pdesc
Typename.equal fld_classname class_typename && fld_typ_is_view fld_typ in Typename.equal fld_classname class_typename && fld_typ_is_view fld_typ in
if is_on_destroy_view then if is_on_destroy_view then
begin begin
let class_typename = Typename.Java.from_string (Procname.java_get_class pname) in let class_typename = Typename.Java.from_string (Procname.java_get_class proc_name) in
match Sil.tenv_lookup tenv class_typename with match Sil.tenv_lookup tenv class_typename with
| Some (Sil.Tstruct { Sil.csu; struct_name = Some class_name; def_methods; instance_fields } | Some (Sil.Tstruct { Sil.struct_name = Some _; instance_fields }
as typ) when AndroidFramework.is_fragment typ tenv -> as typ) when AndroidFramework.is_fragment typ tenv ->
let declared_view_fields = let declared_view_fields =
IList.filter (is_declared_view_typ class_typename) instance_fields in IList.filter (is_declared_view_typ class_typename) instance_fields in
let fields_nullified = PatternMatch.get_fields_nullified pdesc in let fields_nullified = PatternMatch.get_fields_nullified proc_desc in
(* report if a field is declared by C, but not nulled out in C.onDestroyView *) (* report if a field is declared by C, but not nulled out in C.onDestroyView *)
IList.iter IList.iter
(fun (fname, typ, _) -> (fun (fname, typ, _) ->
if not (Ident.FieldSet.mem fname fields_nullified) then if not (Ident.FieldSet.mem fname fields_nullified) then
report_error fname typ pname pdesc) report_error fname typ proc_name proc_desc)
declared_view_fields declared_view_fields
| _ -> () | _ -> ()
end end

@ -46,5 +46,5 @@ let check_immutable_cast curr_pname curr_pdesc typ_expected typ_found_opt loc :
end end
| None -> () | None -> ()
let callback_check_immutable_cast get_proc_desc idenv proc_name = let callback_check_immutable_cast =
Eradicate.callback_check_return_type check_immutable_cast get_proc_desc idenv proc_name Eradicate.callback_check_return_type check_immutable_cast

@ -227,7 +227,7 @@ let check_one_procedure tenv pname pdesc =
| _ -> () | _ -> ()
let callback_performance_checker _ get_proc_desc _ tenv pname pdesc = let callback_performance_checker { Callbacks.proc_desc; proc_name; get_proc_desc; tenv } =
let callbacks = let callbacks =
let analyze_ondemand pn = let analyze_ondemand pn =
match get_proc_desc pn with match get_proc_desc pn with
@ -235,10 +235,10 @@ let callback_performance_checker _ get_proc_desc _ tenv pname pdesc =
| Some pd -> check_one_procedure tenv pn pd in | Some pd -> check_one_procedure tenv pn pd in
{ Ondemand.analyze_ondemand; get_proc_desc; } in { Ondemand.analyze_ondemand; get_proc_desc; } in
if !Config.ondemand_enabled if !Config.ondemand_enabled
|| Ondemand.procedure_should_be_analyzed pdesc pname || Ondemand.procedure_should_be_analyzed proc_desc proc_name
then then
begin begin
Ondemand.set_callbacks callbacks; Ondemand.set_callbacks callbacks;
check_one_procedure tenv pname pdesc; check_one_procedure tenv proc_name proc_desc;
Ondemand.unset_callbacks () Ondemand.unset_callbacks ()
end end

@ -219,12 +219,6 @@ let check_printf_args_ok
| None -> ()) | None -> ())
| _ -> () | _ -> ()
let callback_printf_args let callback_printf_args { Callbacks.proc_desc; proc_name } : unit =
(all_procs : Procname.t list)
(get_proc_desc: Procname.t -> Cfg.Procdesc.t option)
(idenv: Idenv.t)
(tenv: Sil.tenv)
(proc_name: Procname.t)
(proc_desc : Cfg.Procdesc.t) : unit =
Cfg.Procdesc.iter_instrs (fun n i -> check_printf_args_ok n i proc_name proc_desc) proc_desc Cfg.Procdesc.iter_instrs (fun n i -> check_printf_args_ok n i proc_name proc_desc) proc_desc

@ -165,11 +165,11 @@ end (* CheckRepeatedCalls *)
module MainRepeatedCalls = module MainRepeatedCalls =
Eradicate.Build(RepeatedCallsExtension) Eradicate.Build(RepeatedCallsExtension)
let callback_check_repeated_calls all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_check_repeated_calls callback_args =
let checks = let checks =
{ {
TypeCheck.eradicate = false; TypeCheck.eradicate = false;
check_extension = checkers_repeated_calls; check_extension = checkers_repeated_calls;
check_ret_type = []; check_ret_type = [];
} in } in
MainRepeatedCalls.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc MainRepeatedCalls.callback checks callback_args

@ -13,7 +13,7 @@ module L = Logging
(** Find SQL statements in string concatenations *) (** Find SQL statements in string concatenations *)
let callback_sql all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_sql { Callbacks.proc_desc; proc_name } =
let verbose = false in let verbose = false in
(* Case insensitive SQL statement patterns *) (* Case insensitive SQL statement patterns *)

@ -31,10 +31,7 @@ type parameters = TypeState.parameters
(** Type for a module that provides a main callback function *) (** Type for a module that provides a main callback function *)
module type CallBackT = module type CallBackT =
sig sig
val callback : val callback : TypeCheck.checks -> Callbacks.proc_callback_args -> unit
TypeCheck.checks -> Procname.t list -> TypeCheck.get_proc_desc ->
Idenv.t -> Sil.tenv -> Procname.t ->
Cfg.Procdesc.t -> unit
end (* CallBackT *) end (* CallBackT *)
(** Extension to the type checker. *) (** Extension to the type checker. *)
@ -149,8 +146,16 @@ struct
!calls_this, None !calls_this, None
let callback2 let callback2
calls_this checks all_procs get_proc_desc idenv tenv curr_pname calls_this checks
curr_pdesc annotated_signature linereader proc_loc : unit = {
Callbacks.proc_desc = curr_pdesc;
proc_name = curr_pname;
get_proc_desc;
idenv;
tenv;
get_procs_in_file;
}
annotated_signature linereader proc_loc : unit =
let find_duplicate_nodes = State.mk_find_duplicate_nodes curr_pdesc in let find_duplicate_nodes = State.mk_find_duplicate_nodes curr_pdesc in
let find_canonical_duplicate node = let find_canonical_duplicate node =
@ -251,7 +256,7 @@ struct
| Some pdesc -> | Some pdesc ->
res := (pname, pdesc) :: !res res := (pname, pdesc) :: !res
| None -> () in | None -> () in
IList.iter do_proc all_procs; IList.iter do_proc (get_procs_in_file curr_pname);
IList.rev !res IList.rev !res
(** Typestates after the current procedure and all initializer procedures. *) (** Typestates after the current procedure and all initializer procedures. *)
@ -322,7 +327,7 @@ struct
update_summary curr_pname curr_pdesc final_typestate_opt update_summary curr_pname curr_pdesc final_typestate_opt
(** Entry point for the eradicate-based checker infrastructure. *) (** Entry point for the eradicate-based checker infrastructure. *)
let callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback checks ({ Callbacks.proc_desc; proc_name } as callback_args) =
let calls_this = ref false in let calls_this = ref false in
let filter_special_cases () = let filter_special_cases () =
@ -346,8 +351,7 @@ struct
annotated_signature; annotated_signature;
callback2 callback2
calls_this checks all_procs get_proc_desc idenv tenv calls_this checks callback_args annotated_signature linereader loc
proc_name proc_desc annotated_signature linereader loc
end (* MkCallback *) end (* MkCallback *)
@ -383,7 +387,7 @@ module Main =
Build(EmptyExtension) Build(EmptyExtension)
(** Eradicate checker for Java @Nullable annotations. *) (** Eradicate checker for Java @Nullable annotations. *)
let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc = let callback_eradicate ({ Callbacks.get_proc_desc; idenv; proc_desc; proc_name } as callback_args) =
let checks = let checks =
{ {
TypeCheck.eradicate = true; TypeCheck.eradicate = true;
@ -396,7 +400,11 @@ let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc =
| None -> () | None -> ()
| Some pdesc -> | Some pdesc ->
let idenv_pname = Idenv.create_from_idenv idenv pdesc in let idenv_pname = Idenv.create_from_idenv idenv pdesc in
Main.callback checks all_procs get_proc_desc idenv_pname tenv pname pdesc in Main.callback checks
{ callback_args with
Callbacks.idenv = idenv_pname;
proc_name = pname;
proc_desc = pdesc; } in
{ Ondemand.analyze_ondemand; get_proc_desc; } in { Ondemand.analyze_ondemand; get_proc_desc; } in
if not !Config.ondemand_enabled || if not !Config.ondemand_enabled ||
@ -404,17 +412,16 @@ let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc =
then then
begin begin
Ondemand.set_callbacks callbacks; Ondemand.set_callbacks callbacks;
Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc; Main.callback checks callback_args;
Ondemand.unset_callbacks () Ondemand.unset_callbacks ()
end end
(** Call the given check_return_type at the end of every procedure. *) (** Call the given check_return_type at the end of every procedure. *)
let callback_check_return_type check_return_type all_procs let callback_check_return_type check_return_type callback_args =
get_proc_desc idenv tenv proc_name proc_desc =
let checks = let checks =
{ {
TypeCheck.eradicate = false; TypeCheck.eradicate = false;
check_extension = false; check_extension = false;
check_ret_type = [check_return_type]; check_ret_type = [check_return_type];
} in } in
Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc Main.callback checks callback_args

@ -21,10 +21,7 @@ type parameters = (Sil.exp * Sil.typ) list
(** Type for a module that provides a main callback function *) (** Type for a module that provides a main callback function *)
module type CallBackT = module type CallBackT =
sig sig
val callback : val callback : TypeCheck.checks -> Callbacks.proc_callback_args -> unit
TypeCheck.checks -> Procname.t list -> TypeCheck.get_proc_desc ->
Idenv.t -> Sil.tenv -> Procname.t ->
Cfg.Procdesc.t -> unit
end (* CallBackT *) end (* CallBackT *)

Loading…
Cancel
Save