[cost] Make unmodeled functions pure by default

Reviewed By: mbouaziz

Differential Revision: D15470254

fbshipit-source-id: ef3833778

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)

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

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

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 )

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

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)

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) {}
   }
 

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, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]