Skip to content

Commit

Permalink
[hoisting] Hoist only expensive pure functions
Browse files Browse the repository at this point in the history
Reviewed By: mbouaziz

Differential Revision: D10236706

fbshipit-source-id: c51a9ff0c
  • Loading branch information
ezgicicek authored and facebook-github-bot committed Oct 14, 2018
1 parent e71ea9f commit 99c2a6d
Show file tree
Hide file tree
Showing 18 changed files with 210 additions and 37 deletions.
2 changes: 1 addition & 1 deletion Makefile
Expand Up @@ -92,7 +92,7 @@ BUILD_SYSTEMS_TESTS += \

DIRECT_TESTS += \
java_checkers java_eradicate java_infer java_lab java_tracing java_quandary \
java_racerd java_stability java_crashcontext java_hoisting java_starvation java_performance java_purity
java_racerd java_stability java_crashcontext java_hoisting java_hoistingExpensive java_starvation java_performance java_purity
ifneq ($(ANT),no)
BUILD_SYSTEMS_TESTS += ant
endif
Expand Down
5 changes: 5 additions & 0 deletions infer/man/man1/infer-full.txt
Expand Up @@ -412,6 +412,11 @@ OPTIONS
infer-diff(1), infer-events(1), infer-explore(1), infer-report(1),
infer-reportdiff(1), and infer-run(1).

--hoisting-report-only-expensive
Activates: [Hoisting] Report loop-invariant calls only when the
function is expensive, i.e. at least linear (Conversely:
--no-hoisting-report-only-expensive) See also infer-report(1).

--html
Activates: Generate html report. (Conversely: --no-html)
See also infer-explore(1).
Expand Down
5 changes: 5 additions & 0 deletions infer/man/man1/infer-report.txt
Expand Up @@ -161,6 +161,11 @@ OPTIONS
Activates: Whether paths in --skip-analysis-in-path should be
compiled or not (Conversely:
--no-skip-analysis-in-path-skips-compilation)
HOISTING OPTIONS
--hoisting-report-only-expensive
Activates: [Hoisting] Report loop-invariant calls only when the
function is expensive, i.e. at least linear (Conversely:
--no-hoisting-report-only-expensive)


ENVIRONMENT
Expand Down
5 changes: 5 additions & 0 deletions infer/man/man1/infer.txt
Expand Up @@ -412,6 +412,11 @@ OPTIONS
infer-diff(1), infer-events(1), infer-explore(1), infer-report(1),
infer-reportdiff(1), and infer-run(1).

--hoisting-report-only-expensive
Activates: [Hoisting] Report loop-invariant calls only when the
function is expensive, i.e. at least linear (Conversely:
--no-hoisting-report-only-expensive) See also infer-report(1).

--html
Activates: Generate html report. (Conversely: --no-html)
See also infer-explore(1).
Expand Down
11 changes: 11 additions & 0 deletions infer/src/base/Config.ml
Expand Up @@ -208,6 +208,8 @@ let manual_crashcontext = "CRASHCONTEXT OPTIONS"

let manual_generic = Cmdliner.Manpage.s_options

let manual_hoisting = "HOISTING OPTIONS"

let manual_internal = "INTERNAL OPTIONS"

let manual_java = "JAVA OPTIONS"
Expand Down Expand Up @@ -1376,6 +1378,13 @@ and html =
"Generate html report."


and hoisting_report_only_expensive =
CLOpt.mk_bool ~long:"hoisting-report-only-expensive" ~default:false
~in_help:InferCommand.[(Report, manual_hoisting)]
"[Hoisting] Report loop-invariant calls only when the function is expensive, i.e. at least \
linear"


and icfg_dotty_outfile =
CLOpt.mk_path_opt ~long:"icfg-dotty-outfile" ~meta:"path"
"If set, specifies path where .dot file should be written, it overrides the path for all \
Expand Down Expand Up @@ -2612,6 +2621,8 @@ and get_linter_doc_url = process_linters_doc_url !linters_doc_url

and html = !html

and hoisting_report_only_expensive = !hoisting_report_only_expensive

and icfg_dotty_outfile = !icfg_dotty_outfile

and ignore_trivial_traces = !ignore_trivial_traces
Expand Down
2 changes: 2 additions & 0 deletions infer/src/base/Config.mli
Expand Up @@ -380,6 +380,8 @@ val get_linter_doc_url : linter_id:string -> string option

val html : bool

val hoisting_report_only_expensive : bool

val icfg_dotty_outfile : string option

val ignore_trivial_traces : bool
Expand Down
32 changes: 32 additions & 0 deletions infer/src/bufferoverrun/bufferOverrunChecker.ml
Expand Up @@ -243,6 +243,18 @@ module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (CFG))

type invariant_map = Analyzer.invariant_map

(* Use a weak Hashtbl to prevent memory leaks (GC unnecessarily
keeping invariant maps around) *)
module WeakInvMapHashTbl = Caml.Weak.Make (struct
type t = Typ.Procname.t * invariant_map option

let equal (pname1, _) (pname2, _) = Typ.Procname.equal pname1 pname2

let hash (pname, _) = Hashtbl.hash pname
end)

let inv_map_cache = WeakInvMapHashTbl.create 100

module Init = struct
let declare_symbolic_val :
Typ.Procname.t
Expand Down Expand Up @@ -749,8 +761,28 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
| _ ->
summary
in
if Config.hoisting_report_only_expensive then
let pname = Procdesc.get_proc_name proc_desc in
WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map)
else () ;
(inv_map, summary)


let lookup_inv_map_cache (callback_args : Callbacks.proc_callback_args) (pname : Typ.Procname.t) :
invariant_map =
(* Since we are using a weak Hashtbl, represented as a set of
(Procname) hashed values, we have to lookup with a dummy element
*)
match WeakInvMapHashTbl.find_opt inv_map_cache (pname, None) with
| Some (_, Some inv_map) ->
inv_map
| Some (_, None) ->
(* this should never happen *)
assert false
| None ->
(* if bufferoverrun has not been run yet, run it *)
compute_invariant_map_and_check callback_args |> fst


let checker : Callbacks.proc_callback_args -> Summary.t =
fun args -> compute_invariant_map_and_check args |> snd
2 changes: 2 additions & 0 deletions infer/src/bufferoverrun/bufferOverrunChecker.mli
Expand Up @@ -15,6 +15,8 @@ module CFG = ProcCfg.NormalOneInstrPerNode

type invariant_map

val lookup_inv_map_cache : Callbacks.proc_callback_args -> Typ.Procname.t -> invariant_map

val compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t

val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option
Expand Down
39 changes: 19 additions & 20 deletions infer/src/checkers/cost.ml
Expand Up @@ -33,6 +33,25 @@ module Node = ProcCfg.DefaultNode
set it to 1 and for function call we take it from the spec of the function.
The nodes in the domain of the map are those in the path reaching the current node.
*)

let instantiate_cost ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
match Ondemand.get_proc_desc callee_pname with
| None ->
L.(die InternalError)
"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 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
callee_cost Typ.Procname.pp callee_pname
| Some _ ->
let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in
let eval_sym = BufferOverrunSemantics.mk_eval_sym callee_pdesc params inferbo_caller_mem in
BasicCost.subst callee_cost eval_sym )


module TransferFunctionsNodesBasicCost = struct
module CFG = InstrCFG
module Domain = NodesBasicCostDomain
Expand All @@ -41,26 +60,6 @@ module TransferFunctionsNodesBasicCost = struct

let cost_atomic_instruction = BasicCost.one

let instantiate_cost ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
match Ondemand.get_proc_desc callee_pname with
| None ->
L.(die InternalError)
"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 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
callee_cost Typ.Procname.pp callee_pname
| Some _ ->
let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in
let eval_sym =
BufferOverrunSemantics.mk_eval_sym callee_pdesc params inferbo_caller_mem
in
BasicCost.subst callee_cost eval_sym )


let exec_instr_cost inferbo_mem (astate : CostDomain.NodeInstructionToCostMap.astate)
{ProcData.pdesc} (node : CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate =
let key = CFG.Node.id node in
Expand Down
8 changes: 8 additions & 0 deletions infer/src/checkers/cost.mli
Expand Up @@ -8,3 +8,11 @@
open! IStd

val checker : Callbacks.proc_callback_t

val instantiate_cost :
caller_pdesc:Procdesc.t
-> inferbo_caller_mem:BufferOverrunDomain.Mem.astate option
-> callee_pname:Typ.Procname.t
-> params:(Exp.t * 'a) list
-> callee_cost:Itv.NonNegativePolynomial.astate
-> Itv.NonNegativePolynomial.astate
38 changes: 33 additions & 5 deletions infer/src/checkers/hoisting.ml
Expand Up @@ -9,7 +9,9 @@ module F = Format
module InstrCFG = ProcCfg.NormalOneInstrPerNode

module Call = struct
type t = {pname: Typ.Procname.t; loc: Location.t} [@@deriving compare]
type t =
{loc: Location.t; pname: Typ.Procname.t; node: Procdesc.Node.t; params: (Exp.t * Typ.t) list}
[@@deriving compare]

let pp fmt {pname; loc} =
F.fprintf fmt "loop-invariant call to %a, at %a " Typ.Procname.pp pname Location.pp loc
Expand All @@ -28,12 +30,12 @@ module LoopHeadToHoistInstrs = Procdesc.NodeMap

let add_if_hoistable inv_vars instr node source_nodes idom hoistable_calls =
match instr with
| Sil.Call ((ret_id, _), Exp.Const (Const.Cfun pname), _, loc, _)
| Sil.Call ((ret_id, _), Exp.Const (Const.Cfun pname), params, loc, _)
when (* Check condition (1); N dominates all loop sources *)
List.for_all ~f:(fun source -> Dominators.dominates idom node source) source_nodes
&& (* Check condition (2); id should be invariant already *)
LoopInvariant.InvariantVars.mem (Var.of_id ret_id) inv_vars ->
HoistCalls.add {pname; loc} hoistable_calls
HoistCalls.add {pname; loc; node; params} hoistable_calls
| _ ->
hoistable_calls

Expand Down Expand Up @@ -73,14 +75,36 @@ let do_report summary Call.({pname; loc}) loop_head_loc =
Reporting.log_error summary ~loc ~ltr IssueType.invariant_call message


let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
let should_report proc_desc Call.({pname; node; params}) inferbo_invariant_map =
(not Config.hoisting_report_only_expensive)
||
(* only report if function call has expensive/symbolic cost *)
match Ondemand.analyze_proc_name pname with
| Some {Summary.payloads= {Payloads.cost= Some {CostDomain.post= cost}}}
when Itv.NonNegativePolynomial.is_symbolic cost ->
let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in
let inferbo_invariant_map = Lazy.force inferbo_invariant_map in
let inferbo_mem = BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map in
(* get the cost of the function call *)
Cost.instantiate_cost ~caller_pdesc:proc_desc ~inferbo_caller_mem:inferbo_mem
~callee_pname:pname ~params ~callee_cost:cost
|> Itv.NonNegativePolynomial.is_symbolic
| _ ->
false


let checker ({Callbacks.tenv; summary; proc_desc} as callback_args) : Summary.t =
let cfg = InstrCFG.from_pdesc proc_desc in
let proc_data = ProcData.make_default proc_desc tenv in
(* computes reaching defs: node -> (var -> node set) *)
let reaching_defs_invariant_map =
ReachingDefs.Analyzer.exec_cfg cfg proc_data
~initial:(ReachingDefs.init_reaching_defs_with_formals proc_desc)
in
let pname = Procdesc.get_proc_name proc_desc in
let inferbo_invariant_map =
lazy (BufferOverrunChecker.lookup_inv_map_cache callback_args pname)
in
(* get dominators *)
let idom = Dominators.get_idoms proc_desc in
let loop_head_to_source_nodes = Loop_control.get_loop_head_to_source_nodes cfg in
Expand All @@ -94,6 +118,10 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
LoopHeadToHoistInstrs.iter
(fun loop_head inv_instrs ->
let loop_head_loc = Procdesc.Node.get_loc loop_head in
HoistCalls.iter (fun call -> do_report summary call loop_head_loc) inv_instrs )
HoistCalls.iter
(fun call ->
if should_report proc_desc call inferbo_invariant_map then
do_report summary call loop_head_loc )
inv_instrs )
loop_head_to_inv_instrs ;
summary
9 changes: 7 additions & 2 deletions infer/src/checkers/loopInvariant.ml
Expand Up @@ -27,8 +27,13 @@ let is_fun_call_invariant tenv ~is_exp_invariant ~is_inv_by_default callee_pname
match Models.Call.dispatch tenv callee_pname params with
| Some inv ->
InvariantModels.is_invariant inv
| None ->
is_inv_by_default
| None -> (
(* If there is no model, invoke purity analysis to see if function is pure *)
match Ondemand.analyze_proc_name callee_pname with
| Some {Summary.payloads= {Payloads.purity= Some is_pure}} ->
is_pure
| _ ->
is_inv_by_default )


(* check if the def of var is unique and invariant *)
Expand Down
12 changes: 6 additions & 6 deletions infer/src/checkers/purity.ml
Expand Up @@ -61,12 +61,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "purity checker"
end

module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions)
module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions)

let should_report pure pdesc =
let should_report is_pure pdesc =
match Procdesc.get_proc_name pdesc with
| Typ.Procname.Java java_pname as proc_name ->
pure
is_pure
&& (not (Typ.Procname.is_constructor proc_name))
&& (not (Typ.Procname.Java.is_class_initializer java_pname))
&& not (Typ.Procname.Java.is_access_method java_pname)
Expand All @@ -85,9 +85,9 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
Reporting.log_error summary ~loc ~ltr IssueType.pure_function exp_desc
in
match Analyzer.compute_post proc_data ~initial with
| Some pure ->
if should_report pure proc_desc then report_pure () ;
Payload.update_summary pure summary
| Some is_pure ->
if should_report is_pure proc_desc then report_pure () ;
Payload.update_summary is_pure summary
| None ->
L.internal_error "Analyzer failed to compute purity information for %a@." Typ.Procname.pp
proc_name ;
Expand Down
8 changes: 6 additions & 2 deletions infer/src/checkers/registerCheckers.ml
Expand Up @@ -109,8 +109,12 @@ let all_checkers =
; { name= "loop hoisting"
; active= Config.loop_hoisting
; callbacks=
[(Procedure Hoisting.checker, Language.Clang); (Procedure Hoisting.checker, Language.Java)]
}
[ (Procedure Hoisting.checker, Language.Clang)
; (Procedure Hoisting.checker, Language.Java)
; (Procedure Cost.checker, Language.Clang)
; (Procedure Cost.checker, Language.Java)
; (Procedure Purity.checker, Language.Clang)
; (Procedure Purity.checker, Language.Java) ] }
; { name= "Starvation analysis"
; active= Config.starvation
; callbacks=
Expand Down
17 changes: 16 additions & 1 deletion infer/tests/codetoanalyze/java/hoisting/issues.exp
@@ -1,12 +1,27 @@
codetoanalyze/java/hoisting/Hoist.java, Hoist.array_store_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 117]
codetoanalyze/java/hoisting/Hoist.java, Hoist.bar(int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Hoist.bar(int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.clash_function_calls_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.clash_function_calls_hoist(int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.clash_function_calls_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 26]
codetoanalyze/java/hoisting/Hoist.java, Hoist.dep_not_invariant_dont_hoist(int,int[]):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.dep_not_invariant_dont_hoist(int,int[])]
codetoanalyze/java/hoisting/Hoist.java, Hoist.dumb_foo():void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.dumb_foo()]
codetoanalyze/java/hoisting/Hoist.java, Hoist.foo(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Hoist.foo(int,int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.legit_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 73]
codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.loop_guard_hoist(int,int[])]
codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 65]
codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_dont_hoist(int,int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_dont_hoist(int,int,int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.nested_loop_dont_hoist(int,int,int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.nested_loop_hoist(int,int,int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 127]
codetoanalyze/java/hoisting/Hoist.java, Hoist.not_guaranteed_to_execute_dont_hoist(int,int,int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.not_guaranteed_to_execute_dont_hoist(int,int,int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.reassigned_temp_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.reassigned_temp_hoist(int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.reassigned_temp_hoist(int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 45]
codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.two_function_call_hoist(int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 35]
codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.bar(int) at line 35]
codetoanalyze/java/hoisting/Hoist.java, Hoist.used_in_loop_body_before_def_temp_hoist(int,int[]):void, 6, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 57]
codetoanalyze/java/hoisting/Hoist.java, Hoist.void_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.void_hoist(int)]
codetoanalyze/java/hoisting/Hoist.java, Hoist.void_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to void Hoist.dumb_foo() at line 183]
codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_dont_hoist_FP(int):int, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to void HoistIndirect$Test.set_test(HoistIndirect$Test) at line 27]
codetoanalyze/java/hoisting/Hoist.java, Hoist.x_not_invariant_dont_hoist(int,int,int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.x_not_invariant_dont_hoist(int,int,int)]
codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.get_test(HoistIndirect$Test):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect$Test.get_test(HoistIndirect$Test)]
codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_dont_hoist_FP(int):int, 6, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect$Test.get_test(HoistIndirect$Test) at line 28]

0 comments on commit 99c2a6d

Please sign in to comment.