From b46f55d0bca84c65e51f2878055814011e9079cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 19 Dec 2018 07:30:49 -0800 Subject: [PATCH] [purity] Mark functions with empty modified params as pure Reviewed By: mbouaziz, ngorogiannis Differential Revision: D13452909 fbshipit-source-id: f0dc419b1 --- infer/src/checkers/purity.ml | 88 ++++++++++++++----- .../java/hoisting/HoistIndirect.java | 2 +- .../java/hoisting/HoistNoIndirectMod.java | 40 +++++++++ .../codetoanalyze/java/hoisting/issues.exp | 22 ++++- .../hoistingExpensive/HoistExpensive.java | 16 ++++ .../java/hoistingExpensive/issues.exp | 3 +- .../tests/codetoanalyze/java/purity/Test.java | 22 ++++- .../codetoanalyze/java/purity/issues.exp | 5 ++ 8 files changed, 168 insertions(+), 30 deletions(-) diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 49debd2c1..e786d06cc 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -8,6 +8,7 @@ open! IStd module F = Format module L = Logging module ModifiedVarSet = Caml.Set.Make (Var) +module InstrCFG = ProcCfg.NormalOneInstrPerNode let debug fmt = L.(debug Analysis Verbose fmt) @@ -21,11 +22,29 @@ module Payload = SummaryPayload.Make (struct let of_payloads (payloads : Payloads.t) = payloads.purity end) -module TransferFunctions (CFG : ProcCfg.S) = struct - module CFG = CFG +type purity_extras = + {inferbo_invariant_map: BufferOverrunChecker.invariant_map; formals: Var.t list} + +module TransferFunctions = struct + module CFG = ProcCfg.Normal module Domain = PurityDomain - type extras = Var.t list + type extras = purity_extras + + let get_alias_set inferbo_mem var = + let default = ModifiedVarSet.empty in + let alias_v = BufferOverrunDomain.Mem.find (AbsLoc.Loc.of_var var) inferbo_mem in + let pow_locs = BufferOverrunDomain.Val.get_pow_loc alias_v in + AbsLoc.PowLoc.fold + (fun loc modified_acc -> + AbsLoc.Loc.get_path loc + |> Option.value_map ~default:modified_acc ~f:(fun path -> + Symb.SymbolPath.get_pvar path + |> Option.value_map ~default:modified_acc ~f:(fun pvar -> + debug "Add alias of %a -> %a " Var.pp var (Pvar.pp Pp.text) pvar ; + ModifiedVarSet.add (Var.of_pvar pvar) modified_acc ) ) ) + pow_locs default + let get_modified_params formals ~f = List.foldi ~init:Domain.ModifiedParamIndices.empty @@ -36,13 +55,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* given a heap access to ae, find which parameter indices of pdesc it modifies *) - let track_modified_params formals ae = + let track_modified_params inferbo_mem formals ae = let base_var, _ = HilExp.AccessExpression.get_base ae in (* treat writes to global (static) variables separately since they are not considered to be explicit parameters. *) let modified_params = if Var.is_global base_var then Domain.ModifiedParamIndices.singleton Domain.global - else get_modified_params formals ~f:(Var.equal base_var) + else + get_modified_params formals ~f:(fun var -> + Var.equal var base_var || ModifiedVarSet.mem var (get_alias_set inferbo_mem base_var) + ) in Domain.impure modified_params @@ -71,7 +93,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct } } *) - let find_params_matching_modified_args formals callee_args callee_modified_params = + let find_params_matching_modified_args inferbo_mem formals callee_args callee_modified_params = let vars_of_modified_args = List.foldi ~init:ModifiedVarSet.empty ~f:(fun i modified_acc arg_exp -> @@ -79,7 +101,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct debug "Argument %a is modified.\n" HilExp.pp arg_exp ; HilExp.get_access_exprs arg_exp |> List.fold ~init:modified_acc ~f:(fun modified_acc ae -> - ModifiedVarSet.add (HilExp.AccessExpression.get_base ae |> fst) modified_acc ) ) + let base_var, typ = HilExp.AccessExpression.get_base ae in + let modified_acc' = + if Typ.is_pointer typ then ModifiedVarSet.add base_var modified_acc + else modified_acc + in + get_alias_set inferbo_mem base_var |> ModifiedVarSet.union modified_acc' ) ) else modified_acc ) callee_args in @@ -95,23 +122,32 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* if the callee is impure, find the parameters that have been modified by the callee *) - let find_modified_if_impure formals args callee_summary = + let find_modified_if_impure inferbo_mem formals args callee_summary = match Domain.get_modified_params callee_summary with | Some callee_modified_params -> debug "Callee modified params %a \n" Domain.ModifiedParamIndices.pp callee_modified_params ; - Domain.impure (find_params_matching_modified_args formals args callee_modified_params) + Domain.impure + (find_params_matching_modified_args inferbo_mem formals args callee_modified_params) | None -> Domain.pure - let exec_instr (astate : Domain.t) {ProcData.pdesc; tenv; ProcData.extras= formals} _ + let exec_instr (astate : Domain.t) + {ProcData.pdesc; tenv; ProcData.extras= {inferbo_invariant_map; formals}} (node : CFG.Node.t) (instr : HilInstr.t) = + let (node_id : InstrCFG.Node.id) = + CFG.Node.underlying_node node |> InstrCFG.last_of_underlying_node |> InstrCFG.Node.id + in + let inferbo_mem = + Option.value_exn (BufferOverrunChecker.extract_post node_id inferbo_invariant_map) + in match instr with | Assign (ae, _, _) when is_heap_access ae -> - track_modified_params formals ae |> Domain.join astate + track_modified_params inferbo_mem formals ae |> Domain.join astate | Call (_, Direct called_pname, args, _, _) -> let matching_modified = - find_params_matching_modified_args formals args (Domain.all_params_modified args) + find_params_matching_modified_args inferbo_mem formals args + (Domain.all_params_modified args) in Domain.join astate ( match InvariantModels.Call.dispatch tenv called_pname [] with @@ -121,7 +157,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Payload.read pdesc called_pname |> Option.value_map ~default:(Domain.impure matching_modified) ~f:(fun summary -> debug "Reading from %a \n" Typ.Procname.pp called_pname ; - find_modified_if_impure formals args summary ) ) + find_modified_if_impure inferbo_mem formals args summary ) ) | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr @@ -132,7 +168,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "purity checker" end -module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal)) +module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions) let should_report pdesc = (not Config.loop_hoisting) @@ -146,13 +182,16 @@ let should_report pdesc = L.(die InternalError "Not supposed to run on non-Java code.") -let checker {Callbacks.tenv; summary; proc_desc} : Summary.t = +let checker ({Callbacks.tenv; summary; proc_desc} as callback_args) : Summary.t = let proc_name = Procdesc.get_proc_name proc_desc in + let inferbo_invariant_map, _ = + BufferOverrunChecker.compute_invariant_map_and_check callback_args + in let formals = Procdesc.get_formals proc_desc |> List.map ~f:(fun (mname, _) -> Var.of_pvar (Pvar.mk mname proc_name)) in - let proc_data = ProcData.make proc_desc tenv formals in + let proc_data = ProcData.make proc_desc tenv {inferbo_invariant_map; formals} in let report_pure () = let loc = Procdesc.get_loc proc_desc in let exp_desc = F.asprintf "Side-effect free function %a" Typ.Procname.pp proc_name in @@ -161,13 +200,16 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t = in match Analyzer.compute_post proc_data ~initial:PurityDomain.pure with | Some astate -> - ( match PurityDomain.get_modified_params astate with - | Some modified_params -> - debug "Modified parameter indices of %a: %a \n" Typ.Procname.pp proc_name - PurityDomain.ModifiedParamIndices.pp modified_params - | None -> - if should_report proc_desc then report_pure () ) ; - Payload.update_summary astate summary + let astate' = + PurityDomain.get_modified_params astate + |> Option.value_map ~default:astate ~f:(fun modified_params -> + debug "Modified parameter indices of %a: %a \n" Typ.Procname.pp proc_name + PurityDomain.ModifiedParamIndices.pp modified_params ; + if PurityDomain.ModifiedParamIndices.is_empty modified_params then PurityDomain.pure + else astate ) + in + if should_report proc_desc && PurityDomain.is_pure astate' then report_pure () ; + Payload.update_summary astate' summary | None -> L.internal_error "Analyzer failed to compute purity information for %a@." Typ.Procname.pp proc_name ; diff --git a/infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java b/infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java index 7657b5071..318fb8bd4 100644 --- a/infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java +++ b/infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java @@ -230,7 +230,7 @@ class HoistIndirect { new_arr[0] = 4; } - void alias_dont_hoist_FP(int[] arr) { + void alias_dont_hoist(int[] arr) { for (int i = 0; i < 10; i++) { alias(arr); // alias modifies arr get_ith(0, arr); // don't hoist diff --git a/infer/tests/codetoanalyze/java/hoisting/HoistNoIndirectMod.java b/infer/tests/codetoanalyze/java/hoisting/HoistNoIndirectMod.java index e1e490199..e25e0fc83 100644 --- a/infer/tests/codetoanalyze/java/hoisting/HoistNoIndirectMod.java +++ b/infer/tests/codetoanalyze/java/hoisting/HoistNoIndirectMod.java @@ -4,6 +4,7 @@ * 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 HoistNoIndirectMod { @@ -37,4 +38,43 @@ class HoistNoIndirectMod { } return p; } + + // modifies list indirectly via aliasing + public void set_first_to_zero(ArrayList list) { + ArrayList l = list; + if (l != null) { + l.set(0, 0); + } + } + + public void call_set_first_to_zero(ArrayList list) { + set_first_to_zero(list); + } + + public void alias_call_set_first_to_zero(ArrayList list) { + ArrayList l = list; + set_first_to_zero(l); + } + + public void indirect_mod_dont_hoist(Integer[] array, ArrayList list) { + for (Integer element : array) { + set_first_to_zero(list); + call_set_first_to_zero(list); + alias_call_set_first_to_zero(list); + } + } + + int avg(ArrayList list) { + int sum = 0; + for (Integer element : list) { + sum += element; + } + return sum; + } + + public void no_mod_hoist(Integer[] array, ArrayList list) { + for (Integer element : array) { + avg(list); + } + } } diff --git a/infer/tests/codetoanalyze/java/hoisting/issues.exp b/infer/tests/codetoanalyze/java/hoisting/issues.exp index 91e3a5217..56aa200e0 100644 --- a/infer/tests/codetoanalyze/java/hoisting/issues.exp +++ b/infer/tests/codetoanalyze/java/hoisting/issues.exp @@ -1,25 +1,41 @@ codetoanalyze/java/hoisting/Hoist.java, Hoist.array_store_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 117 is loop-invariant] codetoanalyze/java/hoisting/Hoist.java, Hoist.clash_function_calls_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 26 is loop-invariant] codetoanalyze/java/hoisting/Hoist.java, Hoist.legit_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 73 is loop-invariant] +codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 65 is loop-invariant] +codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 127 is loop-invariant] codetoanalyze/java/hoisting/Hoist.java, Hoist.reassigned_temp_hoist(int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 45 is loop-invariant] codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 35 is loop-invariant] codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.bar(int) at line 35 is loop-invariant] codetoanalyze/java/hoisting/Hoist.java, Hoist.used_in_loop_body_before_def_temp_hoist(int,int[]):void, 6, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 57 is loop-invariant] codetoanalyze/java/hoisting/Hoist.java, Hoist.void_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void Hoist.dumb_foo() at line 183 is loop-invariant] +codetoanalyze/java/hoisting/Hoist.java, Hoist.x_not_invariant_dont_hoist(int,int,int):void, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: int Hoist.foo(int,int),Assignment,,Parameter `y`,Binary operation: ([-oo, +oo] + y):signed32] +codetoanalyze/java/hoisting/HoistGlobal.java, HoistGlobal.global_modification_dont_hoist(int):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int HoistGlobal.read_global(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_hoist(int):int, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.foo(int) at line 72 is loop-invariant] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_only_second_call_hoist(int,HoistIndirect$Test,HoistIndirect$Test):int, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.get_test(HoistIndirect$Test) at line 86 is loop-invariant] -codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.alias_dont_hoist_FP(int[]):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get_ith(int,int[]) at line 236 is loop-invariant] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 133 is loop-invariant] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 115 is loop-invariant] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.independent_hoist(int,HoistIndirect$Test):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.foo(int) at line 160 is loop-invariant] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.independent_hoist(int,HoistIndirect$Test):int, 5, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int HoistIndirect.get_ith(int,int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,,Unknown value from: int HoistIndirect.double_me(int),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.double_me(int) at line 210 is loop-invariant] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.modified_array_dont_hoist(int,HoistIndirect$Test):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int HoistIndirect.get_ith(int,int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.modified_inner_array_dont_hoist(int,HoistIndirect$Test):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int HoistIndirect$Test.foo(int),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 125 is loop-invariant] +codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.regionFirst(int[]) at line 220 is loop-invariant] codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate.loop_indirect_hoist(java.util.ArrayList,int,int[]):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistInvalidate.get_length(int[]) at line 52 is loop-invariant] codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.deserialize_hoist(com.fasterxml.jackson.databind.JsonDeserializer,com.fasterxml.jackson.core.JsonParser,com.fasterxml.jackson.databind.DeserializationContext):void, 8, LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to Object JsonDeserializer.deserialize(JsonParser,DeserializationContext) at line 33 is loop-invariant] codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(java.util.List,java.lang.String):int, 3, LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 18 is loop-invariant] codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(java.util.List,java.lang.String):int, 3, LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to boolean List.contains(Object) at line 18 is loop-invariant] -codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.increment_dont_hoist_FP(int):int, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 27 is loop-invariant] -codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 35 is loop-invariant] +codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(java.util.List,java.lang.String):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.avg(java.util.ArrayList):int, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: __cast,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.avg(java.util.ArrayList):int, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int Integer.intValue(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] +codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.increment_dont_hoist_FP(int):int, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 28 is loop-invariant] +codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: int HoistNoIndirectMod.calcNext(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] +codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 36 is loop-invariant] +codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.no_mod_hoist(java.lang.Integer[],java.util.ArrayList):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.avg(ArrayList) at line 77 is loop-invariant] diff --git a/infer/tests/codetoanalyze/java/hoistingExpensive/HoistExpensive.java b/infer/tests/codetoanalyze/java/hoistingExpensive/HoistExpensive.java index 4ef55c1d4..d5f2e844d 100644 --- a/infer/tests/codetoanalyze/java/hoistingExpensive/HoistExpensive.java +++ b/infer/tests/codetoanalyze/java/hoistingExpensive/HoistExpensive.java @@ -4,6 +4,7 @@ * 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 HoistExpensive { @@ -32,4 +33,19 @@ class HoistExpensive { cheap_dont_hoist(1); } } + + // incr will not be hoisted since it is cheap + void cheap_iterator_dont_hoist(ArrayList list) { + int x = 0; + for (Integer elem : list) { + incr(x); + } + } + + // call to cheap_iterator_dont_hoist will be hoisted since it is expensive. + void symbolic_expensive_iterator_hoist(int size, ArrayList list) { + for (int i = 0; i < size; i++) { + cheap_iterator_dont_hoist(list); + } + } } diff --git a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp index 103a13cdd..54fe62c82 100644 --- a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp +++ b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp @@ -1 +1,2 @@ -codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 25 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 26 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList) at line 48 is loop-invariant] diff --git a/infer/tests/codetoanalyze/java/purity/Test.java b/infer/tests/codetoanalyze/java/purity/Test.java index 168606926..7dfd20874 100644 --- a/infer/tests/codetoanalyze/java/purity/Test.java +++ b/infer/tests/codetoanalyze/java/purity/Test.java @@ -42,8 +42,8 @@ class Test { } } - // as soon as we allocate with new, function is marked impure. - int local_alloc_bad_FP(int x, int y) { + // no change to outside state, the local allocation is ok. + int local_alloc_ok(int x, int y) { ArrayList list = new ArrayList(x + y); for (Integer el : list) { call_pure_ok(el); @@ -71,4 +71,22 @@ class Test { array[i] = array[j]; array[j] = tmp; } + + void alias_bad(int[] array, int i, int j) { + int[] a = array; + a[j] = i; + } + + // Currently, we can't distinguish between returning new Objects or + // creating new Objects locally. Ideally, the latter should be fine + // as long as it doesn't leak to the result. + public ArrayList emptyList_bad_FP() { + 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() { + return System.nanoTime(); + } } diff --git a/infer/tests/codetoanalyze/java/purity/issues.exp b/infer/tests/codetoanalyze/java/purity/issues.exp index e1c12e946..07099f483 100644 --- a/infer/tests/codetoanalyze/java/purity/issues.exp +++ b/infer/tests/codetoanalyze/java/purity/issues.exp @@ -1,3 +1,8 @@ codetoanalyze/java/purity/Test.java, Test.call_pure_ok(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Test.call_pure_ok(int)] +codetoanalyze/java/purity/Test.java, Test.emptyList_bad_FP():java.util.ArrayList, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function ArrayList Test.emptyList_bad_FP()] +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_alloc_ok(int,int):int, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/java/purity/Test.java, Test.local_alloc_ok(int,int):int, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] 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()]