diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index f7e10153a..37b640a75 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -23,12 +23,16 @@ let is_defined_outside loop_nodes reaching_defs var = |> Option.value ~default:true +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 callee_pname args = (* Take into account purity behavior of modeled functions *) - let all_params_modified = PurityDomain.all_params_modified args in match Models.ProcName.dispatch tenv callee_pname with | Some inv -> - PurityDomain.with_purity (InvariantModels.is_invariant inv) all_params_modified + PurityDomain.( + if InvariantModels.is_invariant inv then pure else impure_params (all_params_modified args)) | None -> ( debug "No model for %a \n" Typ.Procname.pp callee_pname ; (* If there is no model, invoke purity analysis to see if function is pure *) @@ -36,7 +40,7 @@ let get_purity tenv ~is_inv_by_default callee_pname args = | Some {Summary.payloads= {Payloads.purity= Some purity_summary}} -> purity_summary | _ -> - PurityDomain.with_purity is_inv_by_default all_params_modified ) + if is_inv_by_default then PurityDomain.pure else PurityDomain.impure_global ) let is_non_primitive typ = Typ.is_pointer typ || Typ.is_struct typ @@ -154,13 +158,14 @@ let get_vars_to_invalidate node loop_head args modified_params invalidated_vars args -let all_modified loop_nodes = +let all_unmodeled_modified tenv loop_nodes = LoopNodes.fold (fun node acc -> Procdesc.Node.get_instrs node |> Instrs.fold ~init:acc ~f:(fun acc instr -> match instr with - | Sil.Call ((id, _), _, _, _, _) -> + | Sil.Call ((id, _), Const (Cfun callee_pname), _, _, _) + when is_not_modeled tenv callee_pname -> InvalidatedVars.add (Var.of_id id) acc | _ -> acc ) ) @@ -171,7 +176,7 @@ let all_modified loop_nodes = 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 loop_nodes = - let all_modified = lazy (all_modified loop_nodes) in + let all_unmodeled_modified = lazy (all_unmodeled_modified tenv loop_nodes) in LoopNodes.fold (fun node acc -> Procdesc.Node.get_instrs node @@ -184,10 +189,11 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default loop_nodes = | AbstractDomain.Types.Top -> (* modified global *) (* if one of the callees modifies a global static - variable, invalidate all the function calls *) - InvalidatedVars.union acc (force all_modified) + variable, invalidate all unmodeled function calls *) + InvalidatedVars.union acc (force all_unmodeled_modified) | AbstractDomain.Types.NonTop modified_params -> - if ModifiedParamIndices.is_empty modified_params then (*pure*) acc + if ModifiedParamIndices.is_empty modified_params then (*pure*) + acc else get_vars_to_invalidate node loop_head args modified_params (InvalidatedVars.add (Var.of_id id) acc)) ) diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 710df5618..0e859883e 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -143,22 +143,22 @@ module TransferFunctions = struct | Assign (ae, _, _) when is_heap_access ae -> track_modified_params inferbo_mem formals ae |> Domain.join astate | Call (_, Direct called_pname, args, _, _) -> - let matching_modified = - lazy - (find_params_matching_modified_args inferbo_mem formals args - (Domain.all_params_modified args)) - in Domain.join astate ( match InvariantModels.ProcName.dispatch tenv called_pname with | Some inv -> - Domain.with_purity (InvariantModels.is_invariant inv) (Lazy.force matching_modified) + if InvariantModels.is_invariant inv then Domain.pure + else + find_params_matching_modified_args inferbo_mem formals args + (Domain.all_params_modified args) + |> Domain.impure_params | None -> ( match Payload.read pdesc called_pname with | Some summary -> debug "Reading from %a \n" Typ.Procname.pp called_pname ; find_modified_if_impure inferbo_mem formals args summary | None -> - Domain.impure_params (Lazy.force matching_modified) ) ) + if Typ.Procname.is_constructor called_pname then Domain.pure + else Domain.impure_global ) ) | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr diff --git a/infer/src/checkers/purityDomain.ml b/infer/src/checkers/purityDomain.ml index 55d313310..acb297d0d 100644 --- a/infer/src/checkers/purityDomain.ml +++ b/infer/src/checkers/purityDomain.ml @@ -24,8 +24,6 @@ let is_pure astate = let impure_params modified_params = AbstractDomain.Types.NonTop modified_params -let with_purity is_pure modified_params = if is_pure then pure else impure_params modified_params - let all_params_modified args = List.foldi ~init:ModifiedParamIndices.empty ~f:(fun i acc _ -> ModifiedParamIndices.add i acc) diff --git a/infer/tests/codetoanalyze/java/hoisting/HoistGlobal.java b/infer/tests/codetoanalyze/java/hoisting/HoistGlobal.java index 86176c20c..020cbbecb 100644 --- a/infer/tests/codetoanalyze/java/hoisting/HoistGlobal.java +++ b/infer/tests/codetoanalyze/java/hoisting/HoistGlobal.java @@ -4,6 +4,8 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. */ +import java.util.ArrayList; + class HoistGlobal { public static int svar = 0; @@ -12,6 +14,10 @@ class HoistGlobal { return svar; } + int return_one() { + return 1; + } + class Foo { void set() { svar = 5; @@ -20,6 +26,10 @@ class HoistGlobal { int read_global() { return svar; } + + int return_zero() { + return 0; + } } int global_modification_dont_hoist(int size) { @@ -33,6 +43,17 @@ class HoistGlobal { return d; } + int global_modification_hoist_FN(ArrayList list) { + Foo f = new Foo(); + int d = 0; + for (int i = 0; i < list.size(); i++) { + d += return_one(); // ok to hoist + f.set(); // don't invalidate size() + f.return_zero(); // ok to hoist since doesn't read global + } + return d; + } + void call_global_modification_dont_hoist(int size) { for (int i = 0; i < size; i++) { global_modification_dont_hoist(size); diff --git a/infer/tests/codetoanalyze/java/hoisting/HoistUnmodeled.java b/infer/tests/codetoanalyze/java/hoisting/HoistUnmodeled.java new file mode 100644 index 000000000..a91422962 --- /dev/null +++ b/infer/tests/codetoanalyze/java/hoisting/HoistUnmodeled.java @@ -0,0 +1,29 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +class HoistUnmodeled { + + // Any unmodeled (e.g. timing) call is assumed to be modifying global + // state + void timing_calls_dont_hoist() { + for (int i = 0; i < 10; i++) { + System.nanoTime(); + } + } + + // doesn't read from global state or call any unmodeled function, a + // harmless pure function + void harmless_pure() {} + + // It should be ok to hoist harmless_pure() since it doesn't read + // from global state. + void harmless_hoist_FN() { + for (int i = 0; i < 10; i++) { + timing_calls_dont_hoist(); // don't hoist + harmless_pure(); // ok to hoist + } + } +} diff --git a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java index 639603e60..5d056bfda 100644 --- a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java +++ b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java @@ -55,4 +55,12 @@ class UnknownCallsTest { private static void call_loop_over_charArray(StringBuilder out, String in) { loop_over_charArray(out, in); } + + // hashCode is impure but we don't invalidate all other library + // calls such as size() + void unmodeled_impure_linear(ArrayList list) { + for (int i = 0; i < list.size(); i++) { + list.get(i).hashCode(); + } + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 69162636a..09bdfe754 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -206,3 +206,7 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_ 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] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 17 + 6 ⋅ (Math.min(...).ub + InputStream.read(...).ub), degree = 1] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 6 ⋅ (Math.min(...).ub + InputStream.read(...).ub), degree = 1] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 15 ⋅ list.length + 4 ⋅ (list.length + 1), degree = 1] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ list.length + 4 ⋅ (list.length + 1), degree = 1] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: __cast,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ list.length + 4 ⋅ (list.length + 1), degree = 1] diff --git a/infer/tests/codetoanalyze/java/purity/Test.java b/infer/tests/codetoanalyze/java/purity/Test.java index 7dfd20874..417747bea 100644 --- a/infer/tests/codetoanalyze/java/purity/Test.java +++ b/infer/tests/codetoanalyze/java/purity/Test.java @@ -84,9 +84,8 @@ class Test { return new ArrayList(); } - // All unknown calls that don't have any argument, will be marked as - // pure by default even though they may have side-effects! - static long systemNanoTime_bad_FP() { + // All unmodeled calls will be marked as modifying global state + static long systemNanoTime_bad() { return System.nanoTime(); } } diff --git a/infer/tests/codetoanalyze/java/purity/issues.exp b/infer/tests/codetoanalyze/java/purity/issues.exp index 5664ae6f6..d5345a0f5 100644 --- a/infer/tests/codetoanalyze/java/purity/issues.exp +++ b/infer/tests/codetoanalyze/java/purity/issues.exp @@ -3,4 +3,3 @@ codetoanalyze/java/purity/Test.java, Test.emptyList_bad_FP():java.util.ArrayList codetoanalyze/java/purity/Test.java, Test.local_alloc_ok(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.local_alloc_ok(int,int)] codetoanalyze/java/purity/Test.java, Test.local_write_ok(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.local_write_ok(int,int)] codetoanalyze/java/purity/Test.java, Test.parameter_field_access_ok(Test):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.parameter_field_access_ok(Test)] -codetoanalyze/java/purity/Test.java, Test.systemNanoTime_bad_FP():long, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function long Test.systemNanoTime_bad_FP()]