pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[cleanup] remove unused dynamic dispatch modes

Browse Source 
Reviewed By: jvillard

Differential Revision: D6592210

fbshipit-source-id: cd55355
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent 5ce859c774
commit ab3da5b1d1
10 changed files with 16 additions and 144 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/absint/LowerHil.ml
Unescape View File

@ -95,7 +95,7 @@ struct
module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig))
let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial =
Preanal.do_preanalysis pdesc None tenv ;
Preanal.do_preanalysis pdesc tenv ;
let initial' = (initial, IdAccessPathMapDomain.empty) in
Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial')

2
infer/src/backend/InferAnalyze.ml
Unescape View File

@ -145,8 +145,6 @@ let main ~changed_files ~makefile =
~f:(fun cl -> DB.string_crc_has_extension ~ext:"java" (DB.source_dir_to_string cl))
all_clusters)
in
L.debug Analysis Quiet "Dynamic dispatch mode: %s@."
Config.(string_of_dynamic_dispatch dynamic_dispatch) ;
print_legend () ;
if Config.per_procedure_parallelism && not (Lazy.force is_java) then (
(* Java uses ZipLib which is incompatible with forking *)

7
infer/src/backend/interproc.ml
Unescape View File

@ -1277,10 +1277,10 @@ let perform_transition proc_cfg tenv proc_name =
()
let analyze_procedure_aux cg_opt tenv proc_desc =
let analyze_procedure_aux tenv proc_desc =
let proc_name = Procdesc.get_proc_name proc_desc in
let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
Preanal.do_preanalysis proc_desc cg_opt tenv ;
Preanal.do_preanalysis proc_desc tenv ;
let summaryfp = Config.run_in_footprint_mode (analyze_proc tenv) proc_cfg in
Specs.add_summary proc_name summaryfp ;
perform_transition proc_cfg tenv proc_name ;
@ -1292,8 +1292,7 @@ let analyze_procedure_aux cg_opt tenv proc_desc =
let analyze_procedure {Callbacks.summary; proc_desc; tenv} : Specs.summary =
let proc_name = Procdesc.get_proc_name proc_desc in
Specs.add_summary proc_name summary ;
( try ignore (analyze_procedure_aux None tenv proc_desc) with exn ->
( try ignore (analyze_procedure_aux tenv proc_desc) with exn ->
reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;
Reporting.log_error_deprecated proc_name exn ) ;
Specs.get_summary_unsafe __FILE__ proc_name

79
infer/src/backend/preanal.ml
Unescape View File

@ -12,67 +12,6 @@ open! IStd
open! PVariant
module L = Logging
(** mutate the cfg/cg to add dynamic dispatch handling *)
let add_dispatch_calls pdesc cg tenv =
let sound_dynamic_dispatch = Config.(equal_dynamic_dispatch dynamic_dispatch Sound) in
let node_add_dispatch_calls caller_pname node =
let call_flags_is_dispatch call_flags =
(* if sound dispatch is turned off, only consider dispatch for interface calls *)
sound_dynamic_dispatch && call_flags.CallFlags.cf_virtual
|| call_flags.CallFlags.cf_interface
in
let instr_is_dispatch_call = function
| Sil.Call (_, _, _, _, call_flags) ->
call_flags_is_dispatch call_flags
| _ ->
false
in
let has_dispatch_call instrs = List.exists ~f:instr_is_dispatch_call instrs in
let replace_dispatch_calls = function
| Sil.Call
( ret_id
, (Exp.Const Const.Cfun callee_pname as call_exp)
, ((_, receiver_typ) :: _ as args)
, loc
, call_flags ) as instr
when call_flags_is_dispatch call_flags
-> (
(* the frontend should not populate the list of targets *)
assert (List.is_empty call_flags.CallFlags.cf_targets) ;
let receiver_typ_no_ptr =
match receiver_typ.Typ.desc with Typ.Tptr (typ', _) -> typ' | _ -> receiver_typ
in
let sorted_overrides =
let overrides = Prover.get_overrides_of tenv receiver_typ_no_ptr callee_pname in
List.sort ~cmp:(fun (_, p1) (_, p2) -> Typ.Procname.compare p1 p2) overrides
in
match sorted_overrides with
| (_, target_pname) :: _ as all_targets ->
let targets_to_add =
if sound_dynamic_dispatch then List.map ~f:snd all_targets
else
(* if sound dispatch is turned off, consider only the first target. we do this
because choosing all targets is too expensive for everyday use *)
[target_pname]
in
List.iter
~f:(fun target_pname -> Cg.add_edge cg caller_pname target_pname)
targets_to_add ;
let call_flags' = {call_flags with CallFlags.cf_targets= targets_to_add} in
Sil.Call (ret_id, call_exp, args, loc, call_flags')
| [] ->
instr )
| instr ->
instr
in
let instrs = Procdesc.Node.get_instrs node in
if has_dispatch_call instrs then List.map ~f:replace_dispatch_calls instrs
|> Procdesc.Node.replace_instrs node
in
let pname = Procdesc.get_proc_name pdesc in
Procdesc.iter_nodes (node_add_dispatch_calls pname) pdesc
(** add instructions to perform abstraction *)
let add_abstraction_instructions pdesc =
let open Procdesc in
@ -258,20 +197,6 @@ let do_abstraction pdesc =
Procdesc.signal_did_preanalysis pdesc
(** add possible dynamic dispatch targets to the call_flags of each call site *)
let do_dynamic_dispatch pdesc cg tenv =
( match Config.dynamic_dispatch with
| Interface | Sound ->
let pname = Procdesc.get_proc_name pdesc in
if Typ.Procname.is_java pname then add_dispatch_calls pdesc cg tenv
| NoDynamicDispatch | Lazy ->
() ) ;
Procdesc.signal_did_preanalysis pdesc
let do_preanalysis pdesc cg_opt tenv =
if not (Procdesc.did_preanalysis pdesc) then (
do_liveness pdesc tenv ;
do_abstraction pdesc ;
Option.iter cg_opt ~f:(fun cg -> do_dynamic_dispatch pdesc cg tenv) )
let do_preanalysis pdesc tenv =
if not (Procdesc.did_preanalysis pdesc) then ( do_liveness pdesc tenv ; do_abstraction pdesc )

2
infer/src/backend/preanal.mli
Unescape View File

@ -10,5 +10,5 @@
open! IStd
val do_preanalysis : Procdesc.t -> Cg.t option -> Tenv.t -> unit
val do_preanalysis : Procdesc.t -> Tenv.t -> unit
(** Various preanalysis passes for transforming the IR in useful ways *)

22
infer/src/backend/symExec.ml
Unescape View File

@ -614,26 +614,6 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Typ.Procna
if !Config.curr_language <> Config.Java then
(* default mode for Obj-C/C++/Java virtual calls: resolution only *)
[do_resolve callee_pname receiver_exp actual_receiver_typ]
else if Config.(equal_dynamic_dispatch dynamic_dispatch Sound) then
let targets =
if call_flags.CallFlags.cf_virtual then
(* virtual call--either [called_pname] or an override in some subtype may be called *)
callee_pname :: call_flags.CallFlags.cf_targets
else
(* interface call--[called_pname] has no implementation), we don't want to consider *)
call_flags.CallFlags.cf_targets
(* interface call, don't want to consider *)
in
(* return true if (receiver typ of [target_pname]) <: [actual_receiver_typ] *)
let may_dispatch_to target_pname =
let target_receiver_typ = get_receiver_typ target_pname actual_receiver_typ in
Prover.Subtyping_check.check_subtype tenv target_receiver_typ actual_receiver_typ
in
let resolved_pname = do_resolve callee_pname receiver_exp actual_receiver_typ in
let feasible_targets = List.filter ~f:may_dispatch_to targets in
(* make sure [resolved_pname] is not a duplicate *)
if List.mem ~equal:Typ.Procname.equal feasible_targets resolved_pname then feasible_targets
else resolved_pname :: feasible_targets
else
let resolved_target = do_resolve callee_pname receiver_exp actual_receiver_typ in
match call_flags.CallFlags.cf_targets with
@ -1193,7 +1173,7 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path
exec_builtin (call_args prop_ callee_pname actual_params ret_id loc)
| None ->
match callee_pname with
| Java callee_pname_java when Config.(equal_dynamic_dispatch dynamic_dispatch Lazy)
| Java callee_pname_java when Config.dynamic_dispatch
-> (
let norm_prop, norm_args' = normalize_params tenv current_pname prop_ actual_params in
let norm_args = call_constructor_url_update_args callee_pname norm_args' in

34
infer/src/base/Config.ml
Unescape View File

@ -399,19 +399,6 @@ let whitelisted_cpp_classes =
; other_whitelisted_cpp_classes ]
type dynamic_dispatch = NoDynamicDispatch | Interface | Sound | Lazy [@@deriving compare]
let equal_dynamic_dispatch = [%compare.equal : dynamic_dispatch]
let string_to_dynamic_dispatch =
[("none", NoDynamicDispatch); ("interface", Interface); ("sound", Sound); ("lazy", Lazy)]
let string_of_dynamic_dispatch ddp =
List.find_exn ~f:(fun (_, ddp') -> equal_dynamic_dispatch ddp ddp') string_to_dynamic_dispatch
|> fst
let pp_version fmt () =
F.fprintf fmt "Infer version %s@\nCopyright 2009 - present Facebook. All Rights Reserved."
Version.versionString
@ -1201,12 +1188,6 @@ and dump_duplicate_symbols =
"Dump all symbols with the same name that are defined in more than one file."
and dynamic_dispatch =
CLOpt.mk_symbol_opt ~long:"dynamic-dispatch"
"Specify treatment of dynamic dispatch in Java code: 'none' treats dynamic dispatch as a call to unknown code, 'lazy' follows the JVM semantics and creates procedure descriptions during symbolic execution using the type information found in the abstract state; 'sound' is significantly more computationally expensive"
~symbols:string_to_dynamic_dispatch
and eradicate_condition_redundant =
CLOpt.mk_bool ~long:"eradicate-condition-redundant" "Condition redundant warnings"
@ -2753,17 +2734,12 @@ let clang_frontend_action_string =
let dynamic_dispatch =
let default_mode =
match analyzer with
| Checkers when biabduction ->
Lazy
| Checkers when quandary ->
Sound
| _ ->
NoDynamicDispatch
in
Option.value ~default:default_mode !dynamic_dispatch
CLOpt.mk_bool ~long:"dynamic-dispatch" ~default:biabduction
"Specify treatment of dynamic dispatch in Java code: false 'none' treats dynamic dispatch as a call to unknown code and true triggers lazy dynamic dispatch. The latter mode follows the JVM semantics and creates procedure descriptions during symbolic execution using the type information found in the abstract state"
~in_help:CLOpt.([(Analyze, manual_java)])
let dynamic_dispatch = !dynamic_dispatch
let specs_library =
match infer_cache with

8
infer/src/base/Config.mli
Unescape View File

@ -70,12 +70,6 @@ type compilation_database_dependencies =
| NoDeps
[@@deriving compare]
type dynamic_dispatch = NoDynamicDispatch | Interface | Sound | Lazy [@@deriving compare]
val equal_dynamic_dispatch : dynamic_dispatch -> dynamic_dispatch -> bool
val string_of_dynamic_dispatch : dynamic_dispatch -> string
type build_system =
| BAnalyze
| BAnt
@ -384,7 +378,7 @@ val dotty_cfg_libs : bool
val dump_duplicate_symbols : bool
val dynamic_dispatch : dynamic_dispatch
val dynamic_dispatch : bool
val eradicate : bool

2
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -546,7 +546,7 @@ let checker : Callbacks.proc_callback_args -> Specs.summary =
fun {proc_desc; tenv; summary; get_proc_desc} ->
let proc_name = Specs.get_proc_name summary in
let proc_data = ProcData.make proc_desc tenv get_proc_desc in
Preanal.do_preanalysis proc_desc None tenv ;
Preanal.do_preanalysis proc_desc tenv ;
match compute_post proc_data with
| Some post ->
if Config.bo_debug >= 1 then print_summary proc_name post ;

2
infer/tests/codetoanalyze/java/checkers/Makefile
Unescape View File

@ -9,7 +9,7 @@ TESTS_DIR = ../../..
ANALYZER = checkers
INFER_OPTIONS = \
--debug-exceptions --dynamic-dispatch none --no-default-checkers \
--debug-exceptions --no-default-checkers \
--annotation-reachability --fragment-retains-view --immutable-cast --printf-args --quandary \
--suggest-nullable --check-nullable --racerd \

Write Preview
Loading…
Cancel
Save