diff --git a/infer/src/checkers/invariantModels.ml b/infer/src/checkers/invariantModels.ml deleted file mode 100644 index 02b22baf2..000000000 --- a/infer/src/checkers/invariantModels.ml +++ /dev/null @@ -1,126 +0,0 @@ -(* - * Copyright (c) 2018-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. - *) - -open! IStd -module BuiltinInvariantSet = Caml.Set.Make (String) - -type model = Invariant | Variant - -let is_invariant = function Invariant -> true | Variant -> false - -let invariants = - BuiltinInvariantSet.of_list - [ "__instanceof" - ; "__cast" - ; "__get_array_length" - ; "__get_type_of" - ; "__infer_assume" - ; "__infer_skip" - ; "__infer_fail" ] - - -let invariant_builtins _ s = BuiltinInvariantSet.mem s invariants - -let endsWith suffix _ s = String.is_suffix ~suffix s - -let startsWith prefix _ s = String.is_prefix ~prefix s - -(* matches get*Value *) -let getStarValue tenv s = startsWith "get" tenv s && endsWith "Value" tenv s - -module ProcName = struct - let dispatch : (Tenv.t, model) ProcnameDispatcher.ProcName.dispatcher = - let open ProcnameDispatcher.ProcName in - make_dispatcher - [ +invariant_builtins <>--> Invariant - ; -"__variable_initialization" <>--> Invariant - ; +(fun _ name -> BuiltinDecl.is_declared (Typ.Procname.from_string_c_fun name)) - <>--> Variant - ; +PatternMatch.implements_android "text.TextUtils" &:: "isEmpty" <>--> Invariant - ; +PatternMatch.implements_android "view.ViewGroup" &:: "getChildAt" <>--> Invariant - ; +PatternMatch.implements_android "view.View" &::+ startsWith "get" <>--> Invariant - ; +PatternMatch.implements_android "view.View" &::+ startsWith "findViewById" <>--> Invariant - ; +PatternMatch.implements_android "view.ViewGroup" &:: "getChildCount" <>--> Invariant - ; +PatternMatch.implements_android "content.Context" &::+ startsWith "get" <>--> Invariant - ; +PatternMatch.implements_android "content.res.Resources" - &::+ startsWith "get" <>--> Invariant - ; +PatternMatch.implements_lang "Iterable" &:: "iterator" <>--> Invariant - ; +PatternMatch.implements_collection &:: "iterator" <>--> Invariant - ; +PatternMatch.implements_iterator &:: "hasNext" <>--> Invariant - ; +PatternMatch.implements_iterator &:: "next" <>--> Variant - ; +PatternMatch.implements_iterator &:: "remove" <>--> Variant - ; +PatternMatch.implements_collection &:: "size" <>--> Invariant - ; +PatternMatch.implements_map &:: "size" <>--> Invariant - ; +PatternMatch.implements_collection &:: "add" <>--> Variant - ; +PatternMatch.implements_collection &:: "addAll" <>--> Variant - ; +PatternMatch.implements_collection &:: "remove" <>--> Variant - ; +PatternMatch.implements_collection &:: "isEmpty" <>--> Invariant - ; +PatternMatch.implements_collection &:: "get" <>--> Invariant - ; +PatternMatch.implements_collection &:: "set" <>--> Variant - (* Unlike Set.contains, List.contains is linear *) - ; +PatternMatch.implements_list &:: "contains" <>--> Invariant - ; +PatternMatch.implements_collection &:: "contains" <>--> Invariant - ; +PatternMatch.implements_enumeration &:: "hasMoreElements" <>--> Invariant - ; +PatternMatch.implements_enumeration &:: "nextElement" <>--> Variant - ; +PatternMatch.implements_google "common.base.Preconditions" - &::+ startsWith "check" <>--> Invariant - ; +PatternMatch.implements_inject "Provider" &:: "get" <>--> Invariant - ; +PatternMatch.implements_io "OutputStream" &:: "write" <>--> Variant - ; +PatternMatch.implements_io "InputStream" &:: "read" <>--> Variant - ; +PatternMatch.implements_io "PrintStream" &:: "print" <>--> Variant - ; +PatternMatch.implements_io "PrintStream" &:: "println" <>--> Variant - ; +PatternMatch.implements_io "Reader" &:: "read" <>--> Variant - ; +PatternMatch.implements_io "BufferedReader" &:: "readLine" <>--> Variant - (* deserialization is often expensive *) - ; +PatternMatch.implements_jackson "databind.JsonDeserializer" - &:: "deserialize" <>--> Invariant - ; +PatternMatch.implements_jackson "core.JsonParser" &:: "nextToken" <>--> Variant - ; +PatternMatch.implements_jackson "core.JsonParser" &:: "getCurrentName" <>--> Invariant - ; +PatternMatch.implements_jackson "core.JsonParser" &::+ getStarValue <>--> Invariant - ; +PatternMatch.implements_jackson "core.JsonParser" &::+ startsWith "get" <>--> Invariant - ; +PatternMatch.implements_pseudo_collection &:: "size" <>--> Invariant - ; +PatternMatch.implements_pseudo_collection &:: "get" <>--> Invariant - ; +PatternMatch.implements_lang "Math" &::.*--> Invariant (* for (int|short|byte...)Value*) - ; +PatternMatch.implements_lang "Number" &::+ endsWith "Value" <>--> Invariant - ; +PatternMatch.implements_lang "Boolean" &:: "valueOf" <>--> Invariant - ; +PatternMatch.implements_lang "Boolean" &:: "parseBoolean" <>--> Invariant - ; +PatternMatch.implements_lang "Boolean" &::+ endsWith "Value" <>--> Invariant - ; +PatternMatch.implements_lang "Number" &:: "valueOf" <>--> Invariant - ; +PatternMatch.implements_lang "String" &:: "length" <>--> Invariant - ; +PatternMatch.implements_lang "String" &:: "charAt" <>--> Invariant - (* substring in Java >= 1.7 has linear complexity *) - ; +PatternMatch.implements_lang "String" &:: "substring" <>--> Invariant - ; +PatternMatch.implements_lang "CharSequence" &:: "charAt" <>--> Invariant - ; +PatternMatch.implements_lang "String" &:: "equals" <>--> Invariant - ; +PatternMatch.implements_lang "String" &:: "startsWith" <>--> Invariant - ; +PatternMatch.implements_lang "String" &:: "valueOf" <>--> Invariant - ; +PatternMatch.implements_lang "String" &:: "replace" <>--> Variant - ; +PatternMatch.implements_lang "String" &:: "format" <>--> Invariant - (* String.hashCode is deterministic whereas Object's might not be *) - ; +PatternMatch.implements_lang "String" &:: "hashCode" <>--> Invariant - ; +PatternMatch.implements_lang "StringBuilder" &:: "" <>--> Variant - ; +PatternMatch.implements_lang "StringBuilder" &:: "append" <>--> Variant - ; +PatternMatch.implements_lang "StringBuilder" &:: "length" <>--> Invariant - ; +PatternMatch.implements_lang "Object" &:: "equals" <>--> Invariant - ; +PatternMatch.implements_lang "Object" &:: "toString" <>--> Invariant - ; +PatternMatch.implements_lang "Object" &:: "getClass" <>--> Invariant - ; +PatternMatch.implements_lang "Class" &:: "getSimpleName" <>--> Invariant - ; +PatternMatch.implements_lang "Class" &::+ startsWith "get" <>--> Invariant - ; +PatternMatch.implements_lang "System" &:: "arraycopy" <>--> Variant - ; +PatternMatch.implements_lang "Enum" &:: "valueOf" <>--> Invariant - ; +PatternMatch.implements_lang "Enum" &:: "ordinal" <>--> Invariant - ; +PatternMatch.implements_map &:: "isEmpty" <>--> Invariant - ; +PatternMatch.implements_map &:: "get" <>--> Invariant - ; +PatternMatch.implements_map &:: "put" <>--> Variant - ; +PatternMatch.implements_map &:: "containsKey" <>--> Invariant - ; +PatternMatch.implements_map_entry &:: "getKey" <>--> Invariant - ; +PatternMatch.implements_map_entry &:: "getValue" <>--> Invariant - ; +PatternMatch.implements_queue &:: "poll" <>--> Variant - ; +PatternMatch.implements_queue &:: "add" <>--> Variant - ; +PatternMatch.implements_queue &:: "remove" <>--> Variant - ; +PatternMatch.implements_queue &:: "peek" <>--> Invariant ] -end diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index 88670ec03..568670bd9 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -10,7 +10,6 @@ module InvariantVars = AbstractDomain.FiniteSet (Var) module VarsInLoop = AbstractDomain.FiniteSet (Var) module InvalidatedVars = AbstractDomain.FiniteSet (Var) module LoopNodes = AbstractDomain.FiniteSet (Procdesc.Node) -module Models = InvariantModels module VarSet = AbstractDomain.FiniteSet (Var) let debug fmt = L.(debug Analysis Medium) fmt @@ -25,15 +24,15 @@ let is_defined_outside loop_nodes reaching_defs var = let is_not_modeled tenv callee_pname = - match Models.ProcName.dispatch tenv callee_pname with Some _ -> false | None -> true + match PurityModels.ProcName.dispatch tenv callee_pname with Some _ -> false | None -> true 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 -> + match PurityModels.ProcName.dispatch tenv callee_pname with + | Some callee_purity -> PurityDomain.( - if InvariantModels.is_invariant inv then pure else impure_params (all_params_modified args)) + if is_pure callee_purity 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 *) diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 8ea12c753..232865b61 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -160,17 +160,14 @@ module TransferFunctions = struct track_modified_params inferbo_mem formals ae |> Domain.join astate | Call (_, Direct called_pname, args, _, _) -> Domain.join astate - ( match InvariantModels.ProcName.dispatch tenv called_pname with - | Some inv -> - if InvariantModels.is_invariant inv then Domain.pure - else - find_params_matching_modified_args inferbo_mem formals args - (Domain.all_params_modified args) + ( match PurityModels.ProcName.dispatch tenv called_pname with + | Some callee_summary -> + find_modified_if_impure inferbo_mem formals args callee_summary | None -> ( match get_callee_summary called_pname with - | Some summary -> + | Some callee_summary -> debug "Reading from %a \n" Typ.Procname.pp called_pname ; - find_modified_if_impure inferbo_mem formals args summary + find_modified_if_impure inferbo_mem formals args callee_summary | None -> if Typ.Procname.is_constructor called_pname then Domain.pure else Domain.impure_global ) ) diff --git a/infer/src/checkers/purityModels.ml b/infer/src/checkers/purityModels.ml new file mode 100644 index 000000000..9a3439a8d --- /dev/null +++ b/infer/src/checkers/purityModels.ml @@ -0,0 +1,140 @@ +(* + * Copyright (c) 2018-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. + *) + +open! IStd +module BuiltinPureMethods = Caml.Set.Make (String) + +let pure_builtins = + BuiltinPureMethods.of_list + [ "__instanceof" + ; "__cast" + ; "__get_array_length" + ; "__set_array_length" + ; "__get_type_of" + ; "__infer_assume" + ; "__infer_skip" + ; "__infer_fail" ] + + +let modifies_first = PurityDomain.impure_params (PurityDomain.ModifiedParamIndices.of_list [0]) + +let modifies_third = PurityDomain.impure_params (PurityDomain.ModifiedParamIndices.of_list [2]) + +let pure_builtins _ s = BuiltinPureMethods.mem s pure_builtins + +let endsWith suffix _ s = String.is_suffix ~suffix s + +let startsWith prefix _ s = String.is_prefix ~prefix s + +(* matches get*Value *) +let getStarValue tenv s = startsWith "get" tenv s && endsWith "Value" tenv s + +module ProcName = struct + let dispatch : (Tenv.t, PurityDomain.t) ProcnameDispatcher.ProcName.dispatcher = + let open ProcnameDispatcher.ProcName in + make_dispatcher + [ +pure_builtins <>--> PurityDomain.pure + ; -"__variable_initialization" <>--> PurityDomain.pure + ; -"__new" <>--> PurityDomain.pure + ; -"__new_array" <>--> PurityDomain.pure + ; -"__cast" <>--> PurityDomain.pure + ; -"__variable_initialization" <>--> PurityDomain.pure + ; +(fun _ name -> BuiltinDecl.is_declared (Typ.Procname.from_string_c_fun name)) + <>--> PurityDomain.impure_global + ; +PatternMatch.implements_android "text.TextUtils" &:: "isEmpty" <>--> PurityDomain.pure + ; +PatternMatch.implements_android "view.ViewGroup" &:: "getChildAt" <>--> PurityDomain.pure + ; +PatternMatch.implements_android "view.View" &::+ startsWith "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_android "view.View" + &::+ startsWith "findViewById" <>--> PurityDomain.pure + ; +PatternMatch.implements_android "view.ViewGroup" + &:: "getChildCount" <>--> PurityDomain.pure + ; +PatternMatch.implements_android "content.Context" + &::+ startsWith "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_android "content.res.Resources" + &::+ startsWith "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Iterable" &:: "iterator" <>--> PurityDomain.pure + ; +PatternMatch.implements_collection &:: "iterator" <>--> PurityDomain.pure + ; +PatternMatch.implements_iterator &:: "hasNext" <>--> PurityDomain.pure + ; +PatternMatch.implements_iterator &:: "next" <>--> modifies_first + ; +PatternMatch.implements_iterator &:: "remove" <>--> modifies_first + ; +PatternMatch.implements_collection &:: "size" <>--> PurityDomain.pure + ; +PatternMatch.implements_map &:: "size" <>--> PurityDomain.pure + ; +PatternMatch.implements_collection &:: "add" <>--> modifies_first + ; +PatternMatch.implements_collection &:: "addAll" <>--> modifies_first + ; +PatternMatch.implements_collection &:: "remove" <>--> modifies_first + ; +PatternMatch.implements_collection &:: "isEmpty" <>--> PurityDomain.pure + ; +PatternMatch.implements_collection &:: "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_collection &:: "set" <>--> modifies_first + (* Unlike Set.contains, List.contains is linear *) + ; +PatternMatch.implements_list &:: "contains" <>--> PurityDomain.pure + ; +PatternMatch.implements_collection &:: "contains" <>--> PurityDomain.pure + ; +PatternMatch.implements_enumeration &:: "hasMoreElements" <>--> PurityDomain.pure + ; +PatternMatch.implements_enumeration &:: "nextElement" <>--> modifies_first + ; +PatternMatch.implements_google "common.base.Preconditions" + &::+ startsWith "check" <>--> PurityDomain.pure + ; +PatternMatch.implements_inject "Provider" &:: "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_io "OutputStream" &:: "write" <>--> PurityDomain.impure_global + ; +PatternMatch.implements_io "InputStream" &:: "read" <>--> PurityDomain.impure_global + ; +PatternMatch.implements_io "PrintStream" &:: "print" <>--> PurityDomain.impure_global + ; +PatternMatch.implements_io "PrintStream" &:: "println" <>--> PurityDomain.impure_global + ; +PatternMatch.implements_io "Reader" &:: "read" <>--> PurityDomain.impure_global + ; +PatternMatch.implements_io "BufferedReader" + &:: "readLine" <>--> PurityDomain.impure_global + (* deserialization is often expensive *) + ; +PatternMatch.implements_jackson "databind.JsonDeserializer" + &:: "deserialize" <>--> PurityDomain.pure + ; +PatternMatch.implements_jackson "core.JsonParser" &:: "nextToken" <>--> modifies_first + ; +PatternMatch.implements_jackson "core.JsonParser" + &:: "getCurrentName" <>--> PurityDomain.pure + ; +PatternMatch.implements_jackson "core.JsonParser" + &::+ getStarValue <>--> PurityDomain.pure + ; +PatternMatch.implements_jackson "core.JsonParser" + &::+ startsWith "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_pseudo_collection &:: "size" <>--> PurityDomain.pure + ; +PatternMatch.implements_pseudo_collection &:: "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Math" &:: "random" <>--> PurityDomain.impure_global + ; +PatternMatch.implements_lang "Math" &::.*--> PurityDomain.pure + (* for (int|short|byte...)Value*) + ; +PatternMatch.implements_lang "Number" &::+ endsWith "Value" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Boolean" &:: "valueOf" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Boolean" &:: "parseBoolean" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Boolean" &::+ endsWith "Value" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Number" &:: "valueOf" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "String" &:: "length" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "String" &:: "charAt" <>--> PurityDomain.pure + (* substring in Java >= 1.7 has linear complexity *) + ; +PatternMatch.implements_lang "String" &:: "substring" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "CharSequence" &:: "charAt" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "String" &:: "equals" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "String" &:: "startsWith" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "String" &:: "valueOf" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "String" &:: "replace" <>--> modifies_first + ; +PatternMatch.implements_lang "String" &:: "format" <>--> PurityDomain.pure + (* String.hashCode is deterministic whereas Object's might not be *) + ; +PatternMatch.implements_lang "String" &:: "hashCode" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "StringBuilder" &:: "" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "StringBuilder" &:: "append" <>--> modifies_first + ; +PatternMatch.implements_lang "StringBuilder" &:: "length" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Object" &:: "equals" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Object" &:: "toString" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Object" &:: "getClass" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Class" &:: "getSimpleName" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Class" &::+ startsWith "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "System" &:: "arraycopy" <>--> modifies_third + ; +PatternMatch.implements_lang "Enum" &:: "valueOf" <>--> PurityDomain.pure + ; +PatternMatch.implements_lang "Enum" &:: "ordinal" <>--> PurityDomain.pure + ; +PatternMatch.implements_map &:: "isEmpty" <>--> PurityDomain.pure + ; +PatternMatch.implements_map &:: "get" <>--> PurityDomain.pure + ; +PatternMatch.implements_map &:: "put" <>--> modifies_first + ; +PatternMatch.implements_map &:: "containsKey" <>--> PurityDomain.pure + ; +PatternMatch.implements_map_entry &:: "getKey" <>--> PurityDomain.pure + ; +PatternMatch.implements_map_entry &:: "getValue" <>--> PurityDomain.pure + ; +PatternMatch.implements_queue &:: "poll" <>--> modifies_first + ; +PatternMatch.implements_queue &:: "add" <>--> modifies_first + ; +PatternMatch.implements_queue &:: "remove" <>--> modifies_first + ; +PatternMatch.implements_queue &:: "peek" <>--> PurityDomain.pure ] +end diff --git a/infer/tests/codetoanalyze/java/purity/PurityModeled.java b/infer/tests/codetoanalyze/java/purity/PurityModeled.java new file mode 100644 index 000000000..707acc567 --- /dev/null +++ b/infer/tests/codetoanalyze/java/purity/PurityModeled.java @@ -0,0 +1,18 @@ +/* + * 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 PurityModeled { + + double math_random_impure() { + return Math.random(); + } + + void arraycopy_pure(int[] src) { + int[] dst = {5, 10, 20, 30, 40, 50}; + // copies an array from the specified source array + System.arraycopy(src, 0, dst, 0, 1); + } +} diff --git a/infer/tests/codetoanalyze/java/purity/issues.exp b/infer/tests/codetoanalyze/java/purity/issues.exp index e318d513a..1782a700b 100644 --- a/infer/tests/codetoanalyze/java/purity/issues.exp +++ b/infer/tests/codetoanalyze/java/purity/issues.exp @@ -4,6 +4,7 @@ codetoanalyze/java/purity/Localities.java, Localities.call_impure_with_fresh_arg codetoanalyze/java/purity/Localities.java, Localities.length_pure(java.util.ArrayList):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Localities.length_pure(ArrayList)] codetoanalyze/java/purity/Localities.java, Localities.mkHC_pure(Localities$Counter):Localities$HasCounter, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function Localities$HasCounter Localities.mkHC_pure(Localities$Counter)] codetoanalyze/java/purity/Localities.java, Localities.setFreshArrayEntry_pure(int,int):int[], 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int[] Localities.setFreshArrayEntry_pure(int,int)] +codetoanalyze/java/purity/PurityModeled.java, PurityModeled.arraycopy_pure(int[]):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void PurityModeled.arraycopy_pure(int[])] 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)]