From bc082da199ad1beae58a30703064de6d9dc22e78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 24 May 2019 01:36:30 -0700 Subject: [PATCH] [cost] Make unmodeled functions pure by default Reviewed By: mbouaziz Differential Revision: D15470254 fbshipit-source-id: ef3833778 --- infer/man/man1/infer-full.txt | 8 +++---- infer/src/base/Config.ml | 14 ++++++------ infer/src/base/Config.mli | 4 ++-- infer/src/checkers/hoisting.ml | 2 +- infer/src/checkers/loopInvariant.ml | 22 ++++++++++--------- infer/src/checkers/loopInvariant.mli | 2 +- .../java/performance/UnknownCallsTest.java | 6 ++--- .../codetoanalyze/java/performance/issues.exp | 4 ++-- 8 files changed, 32 insertions(+), 30 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 8ba336501..5e71cc46d 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1346,10 +1346,6 @@ INTERNAL OPTIONS --icfg-dotty-outfile-reset Cancel the effect of --icfg-dotty-outfile. - --invariant-by-default - Activates: [Cost]Consider functions to be invariant by default - (Conversely: --no-invariant-by-default) - --iphoneos-target-sdk-version-path-regex-reset Set --iphoneos-target-sdk-version-path-regex to the empty list. @@ -1538,6 +1534,10 @@ INTERNAL OPTIONS --pulse-widen-threshold int Under-approximate after int loop iterations (default: 3) + --pure-by-default + Activates: [Purity]Consider unknown functions to be pure by + default (Conversely: --no-pure-by-default) + --reactive-capture Activates: Compile source files only when required by analyzer (clang only) (Conversely: --no-reactive-capture) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 7737692b8..bf625b1f3 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -965,11 +965,6 @@ and continue = a procedure was changed beforehand, keep the changed marking.)" -and cost_invariant_by_default = - CLOpt.mk_bool ~long:"invariant-by-default" ~default:false - "[Cost]Consider functions to be invariant by default" - - and costs_current = CLOpt.mk_path_opt ~long:"costs-current" ~in_help:InferCommand.[(ReportDiff, manual_generic)] @@ -1879,6 +1874,11 @@ and pulse_widen_threshold = "Under-approximate after $(i,int) loop iterations" +and pure_by_default = + CLOpt.mk_bool ~long:"pure-by-default" ~default:false + "[Purity]Consider unknown functions to be pure by default" + + and quandary_endpoints = CLOpt.mk_json ~long:"quandary-endpoints" ~in_help:InferCommand.[(Analyze, manual_quandary)] @@ -2664,8 +2664,6 @@ and continue_capture = !continue and cost = !cost -and cost_invariant_by_default = !cost_invariant_by_default - and costs_current = !costs_current and costs_previous = !costs_previous @@ -2950,6 +2948,8 @@ and pulse_widen_threshold = !pulse_widen_threshold and purity = !purity +and pure_by_default = !pure_by_default + and quandary = !quandary and quandaryBO = !quandaryBO diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 04c1ff6d8..2c46fdf0f 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -294,8 +294,6 @@ val continue_capture : bool val cost : bool -val cost_invariant_by_default : bool - val costs_current : string option val costs_previous : string option @@ -558,6 +556,8 @@ val pulse_widen_threshold : int val purity : bool +val pure_by_default : bool + val quandary : bool val quandary_endpoints : Yojson.Basic.json diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index 92ffb38c9..c17467e54 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -63,7 +63,7 @@ let get_hoist_inv_map tenv ~get_callee_purity reaching_defs_invariant_map loop_h let loop_nodes = Loop_control.get_all_nodes_upwards_until loop_head source_nodes in let inv_vars_in_loop = LoopInvariant.get_inv_vars_in_loop tenv reaching_defs_invariant_map loop_head loop_nodes - ~is_inv_by_default:Config.cost_invariant_by_default ~get_callee_purity + ~is_pure_by_default:Config.pure_by_default ~get_callee_purity in let hoist_instrs = get_hoistable_calls inv_vars_in_loop loop_nodes source_nodes idom in LoopHeadToHoistInstrs.add loop_head hoist_instrs inv_map ) diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index 0e9d652d1..88670ec03 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -28,7 +28,7 @@ let is_not_modeled tenv callee_pname = match Models.ProcName.dispatch tenv callee_pname with Some _ -> false | None -> true -let get_purity tenv ~is_inv_by_default ~get_callee_purity callee_pname args = +let get_purity tenv ~is_pure_by_default ~get_callee_purity callee_pname args = (* Take into account purity behavior of modeled functions *) match Models.ProcName.dispatch tenv callee_pname with | Some inv -> @@ -41,13 +41,13 @@ let get_purity tenv ~is_inv_by_default ~get_callee_purity callee_pname args = | Some purity_summary -> purity_summary | _ -> - if is_inv_by_default then PurityDomain.pure else PurityDomain.impure_global ) + if is_pure_by_default then PurityDomain.pure else PurityDomain.impure_global ) let is_non_primitive typ = Typ.is_pointer typ || Typ.is_struct typ (* check if the def of var is unique and invariant *) -let is_def_unique_and_satisfy tenv var (loop_nodes : LoopNodes.t) ~is_inv_by_default +let is_def_unique_and_satisfy tenv var (loop_nodes : LoopNodes.t) ~is_pure_by_default ~get_callee_purity is_exp_invariant = let equals_var id = Var.equal var (Var.of_id id) in match LoopNodes.is_singleton_or_more loop_nodes with @@ -61,7 +61,7 @@ let is_def_unique_and_satisfy tenv var (loop_nodes : LoopNodes.t) ~is_inv_by_def true | Sil.Call ((id, _), Const (Cfun callee_pname), args, _, _) when equals_var id -> PurityDomain.is_pure - (get_purity tenv ~is_inv_by_default ~get_callee_purity callee_pname args) + (get_purity tenv ~is_pure_by_default ~get_callee_purity callee_pname args) && (* check if all params are invariant *) List.for_all ~f:(fun (exp, _) -> is_exp_invariant exp) args | _ -> @@ -180,7 +180,7 @@ let all_unmodeled_modified tenv loop_nodes = (* If there is a call to an impure function in the loop, invalidate all its non-primitive arguments. Once invalidated, it should be never added again. *) -let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default ~get_callee_purity loop_nodes = +let get_invalidated_vars_in_loop tenv loop_head ~is_pure_by_default ~get_callee_purity loop_nodes = let all_unmodeled_modified = lazy (all_unmodeled_modified tenv loop_nodes) in LoopNodes.fold (fun node acc -> @@ -189,7 +189,7 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default ~get_callee_p match instr with | Sil.Call ((id, _), Const (Cfun callee_pname), args, _, _) -> ( let purity = - get_purity tenv ~is_inv_by_default ~get_callee_purity callee_pname args + get_purity tenv ~is_pure_by_default ~get_callee_purity callee_pname args in PurityDomain.( match purity with @@ -217,7 +217,7 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default ~get_callee_p (* A variable is invariant if - its reaching definition is outside of the loop - o.w. its definition is constant or invariant itself *) -let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_inv_by_default ~get_callee_purity +let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_pure_by_default ~get_callee_purity loop_head loop_nodes = let process_var_once var inv_vars invalidated_vars = (* if a variable is marked invariant once, it can't be invalidated @@ -236,7 +236,7 @@ let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_inv_by_default ~ge if LoopNodes.is_empty in_loop_defs then (InvariantVars.add var inv_vars, true) else if (* its definition is unique and invariant *) - is_def_unique_and_satisfy tenv var def_nodes ~is_inv_by_default + is_def_unique_and_satisfy tenv var def_nodes ~is_pure_by_default ~get_callee_purity (is_exp_invariant inv_vars invalidated_vars loop_nodes reaching_defs) then (InvariantVars.add var inv_vars, true) @@ -249,7 +249,7 @@ let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_inv_by_default ~ge (* until there are no changes to inv_vars, keep repeatedly processing all the variables that occur in the loop nodes *) let invalidated_vars = - get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default ~get_callee_purity loop_nodes + get_invalidated_vars_in_loop tenv loop_head ~is_pure_by_default ~get_callee_purity loop_nodes in let rec find_fixpoint inv_vars = let inv_vars', modified = @@ -270,13 +270,15 @@ module LoopHeadToInvVars = Procdesc.NodeMap type invariant_map = VarSet.t LoopHeadToInvVars.t +(** This is invoked by cost analysis, hence assume that unmodeled + calls are pure by default *) let get_loop_inv_var_map tenv get_callee_purity reaching_defs_invariant_map loop_head_to_loop_nodes : invariant_map = LoopHeadToLoopNodes.fold (fun loop_head loop_nodes inv_map -> let inv_vars_in_loop = get_inv_vars_in_loop tenv reaching_defs_invariant_map loop_head loop_nodes - ~is_inv_by_default:Config.cost_invariant_by_default ~get_callee_purity + ~is_pure_by_default:true ~get_callee_purity in L.(debug Analysis Medium) "@\n>>> loop head: %a --> inv vars: %a @\n" Procdesc.Node.pp loop_head InvariantVars.pp diff --git a/infer/src/checkers/loopInvariant.mli b/infer/src/checkers/loopInvariant.mli index 8e2e2392b..16df0d0d8 100644 --- a/infer/src/checkers/loopInvariant.mli +++ b/infer/src/checkers/loopInvariant.mli @@ -26,7 +26,7 @@ type invariant_map = VarsInLoop.t Procdesc.NodeMap.t val get_inv_vars_in_loop : Tenv.t -> ReachingDefs.invariant_map - -> is_inv_by_default:bool + -> is_pure_by_default:bool -> get_callee_purity:( Typ.Procname.t -> PurityDomain.ModifiedParamIndices.t AbstractDomain.Types.top_lifted sexp_option) diff --git a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java index 5d056bfda..8f9835471 100644 --- a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java +++ b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java @@ -18,9 +18,9 @@ class UnknownCallsTest { for (int i = 0; i < length; ++i) {} } - // call to JSONArray.length is not modeled, hence the result will - // not be invariant. Therefore we get quadratic bound. - public void jsonArray_quadratic(JSONArray jsonArray) { + // call to JSONArray.length is not modeled, but we assume it to be + // invariant for cost analysis. + public void jsonArray(JSONArray jsonArray) { for (int i = 0; i < jsonArray.length(); ++i) {} } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 179aabdcd..2f87d1aac 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -121,7 +121,7 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 33 + 65 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_ALLOCATION_CALL, no_bucket, ERROR, [with estimated cost String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.escape(StringBuilder,String),Loop at line 13] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 24 + 65 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.escape(StringBuilder,String),Loop at line 13] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ seq.length × (min(1, seq.length)) + 3 ⋅ (seq.length + 1), degree = 2,{seq.length + 1},Loop at line 111,{min(1, seq.length)},Loop at line 111,{seq.length},Loop at line 111] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ seq.length + 3 ⋅ (seq.length + 1), degree = 1,{seq.length + 1},Loop at line 111,{seq.length},Loop at line 111] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), degree = 1,{length - 1},Loop at line 40] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 3 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, degree = 2,{length},Loop at line 50,{length - 1},Loop at line 51,{length - 1},Loop at line 50] @@ -144,8 +144,8 @@ codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switc codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 14 + 12 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 52] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray(org.json.JSONArray):void, 0, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ JSONArray.length().ub + 3 ⋅ (1+max(0, JSONArray.length().ub)), degree = 1,{1+max(0, JSONArray.length().ub)},Loop at line 24,{JSONArray.length().ub},Loop at line 24] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ JSONArray.length().ub, degree = 1,{JSONArray.length().ub},Loop at line 18] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_quadratic(org.json.JSONArray):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ JSONArray.length().ub² + 3 ⋅ (1+max(0, JSONArray.length().ub)), degree = 2,{1+max(0, JSONArray.length().ub)},Loop at line 24,{JSONArray.length().ub},Loop at line 24,{JSONArray.length().ub},Loop at line 24] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},Loop at line 52] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 47] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32]