pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[purity] Enhance purity models with invalidated arguments

Browse Source 
Summary:
- Rename `invariantModels` to `purityModels`
- Track which arguments are modified in purity models. Before we were invalidating all arguments of impure modeled functions. Instead, now we only invalidate modified args given in the model. This should ideally result in more precision in the analysis.
- Add some more purity models for :`cast`, `new`, `new_array` and `Math.random`

Reviewed By: mbouaziz

Differential Revision: D15535332

fbshipit-source-id: 5395800d9
master
Ezgi Çiçek 6 years ago committed by Facebook Github Bot
parent 62a3187f5d
commit a01a4a3658
6 changed files with 168 additions and 139 deletions
Show Stats Download Patch File Download Diff File

126
infer/src/checkers/invariantModels.ml
Unescape View File

@ -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" &:: "<init>" <>--> 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

9
infer/src/checkers/loopInvariant.ml
Unescape View File

@ -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 *)

13
infer/src/checkers/purity.ml
Unescape View File

@ -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 ) )

140
infer/src/checkers/purityModels.ml
Unescape View File

@ -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" &:: "<init>" <>--> 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

18
infer/tests/codetoanalyze/java/purity/PurityModeled.java
Unescape View File

@ -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);
}
}

1
infer/tests/codetoanalyze/java/purity/issues.exp
Unescape View File

@ -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)]

Write Preview
Loading…
Cancel
Save