From 9e5307b33902cbd9c7e524376966dcec987f6f1f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 13 Nov 2019 05:14:38 -0800 Subject: [PATCH] [pulse][impurity] Add Pulse Java models for get and cast Summary: We consider Java collections to be like c++ std::vectors and add models for - `Collections.get(..)` - `__cast` Reviewed By: skcho Differential Revision: D18449607 fbshipit-source-id: 448206c84 --- infer/src/backend/Payloads.ml | 3 +++ infer/src/backend/Payloads.mli | 1 + infer/src/checkers/impurity.ml | 17 +++++++++---- infer/src/checkers/impurityDomain.ml | 11 +++++++++ infer/src/checkers/impurityDomain.mli | 2 ++ infer/src/pulse/Pulse.ml | 9 +++---- infer/src/pulse/PulseModels.ml | 24 +++++++++++++------ infer/src/pulse/PulseModels.mli | 2 +- .../java/impurity/Localities.java | 16 +++++++++++++ .../codetoanalyze/java/impurity/issues.exp | 2 ++ 10 files changed, 70 insertions(+), 17 deletions(-) diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 32c5e0e99..c028ea6f1 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -15,6 +15,7 @@ type t = ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option ; class_loads: ClassLoadsDomain.summary option ; cost: CostDomain.summary option + ; impurity: ImpurityDomain.t option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho_graphql_field_access: LithoDomain.t option ; litho_required_props: LithoDomain.t option @@ -44,6 +45,7 @@ let fields = ~buffer_overrun_checker:(fun f -> mk f "BufferOverrunChecker" BufferOverrunCheckerSummary.pp) ~class_loads:(fun f -> mk f "ClassLoads" ClassLoadsDomain.pp_summary) ~cost:(fun f -> mk f "Cost" CostDomain.pp_summary) + ~impurity:(fun f -> mk f "Impurity" ImpurityDomain.pp) ~litho_graphql_field_access:(fun f -> mk f "Litho GraphQL Field Access" LithoDomain.pp) ~litho_required_props:(fun f -> mk f "Litho Required Props" LithoDomain.pp) ~pulse:(fun f -> mk f "Pulse" PulseSummary.pp) @@ -70,6 +72,7 @@ let empty = ; buffer_overrun_checker= None ; class_loads= None ; cost= None + ; impurity= None ; lab_resource_leaks= None ; litho_graphql_field_access= None ; litho_required_props= None diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index e0c19a525..bb22e516b 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -20,6 +20,7 @@ include ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option ; class_loads: ClassLoadsDomain.summary option ; cost: CostDomain.summary option + ; impurity: ImpurityDomain.t option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho_graphql_field_access: LithoDomain.t option ; litho_required_props: LithoDomain.t option diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 65cd89def..856acaa4f 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -15,6 +15,12 @@ let debug fmt = L.(debug Analysis Verbose fmt) (* An impurity analysis that relies on pulse to determine how the state changes *) +module Payload = SummaryPayload.Make (struct + type t = ImpurityDomain.t + + let field = Payloads.Fields.impurity +end) + let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractValue.t list option = match List.fold2 ~init:(Some []) @@ -125,12 +131,13 @@ let report_errors summary modified_opt = let pname_loc = Procdesc.get_loc pdesc in let impure_fun_desc = F.asprintf "Impure function %a" Typ.Procname.pp proc_name in let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in - ( match modified_opt with + match modified_opt with | None -> Reporting.log_error summary ~loc:pname_loc ~ltr:[impure_fun_ltr] IssueType.impure_function - impure_fun_desc + impure_fun_desc ; + summary | Some (ImpurityDomain.{modified_globals; modified_params} as astate) -> - if Purity.should_report pdesc && not (ImpurityDomain.is_pure astate) then + ( if Purity.should_report pdesc && not (ImpurityDomain.is_pure astate) then let modified_ltr param_source set acc = ImpurityDomain.ModifiedVarSet.fold (ImpurityDomain.add_to_errlog ~nesting:1 param_source) @@ -141,8 +148,8 @@ let report_errors summary modified_opt = :: modified_ltr Formal modified_params (modified_ltr Global modified_globals []) in Reporting.log_error summary ~loc:pname_loc ~ltr IssueType.impure_function impure_fun_desc - ) ; - summary + ) ; + Payload.update_summary astate summary let checker ({Callbacks.summary} as callback) : Summary.t = diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 9ade0601c..3c64ef718 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -67,3 +67,14 @@ let add_to_errlog ~nesting param_source ModifiedVar.{var; trace_list} errlog = in let first_trace, rest = trace_list in List.fold_left rest ~init:(aux ~nesting errlog first_trace) ~f:(aux ~nesting) + + +let pp fmt ({modified_globals; modified_params} as astate) = + if is_pure astate then F.fprintf fmt "@\n pure @\n" + else if ModifiedVarSet.is_empty modified_params then + F.fprintf fmt "@\n impure, modified globals :%a @\n" ModifiedVarSet.pp modified_globals + else if ModifiedVarSet.is_empty modified_globals then + F.fprintf fmt "@\n impure, modified params :%a @\n" ModifiedVarSet.pp modified_params + else + F.fprintf fmt "@\n impure, modified params :%a, modified globals :%a @\n" ModifiedVarSet.pp + modified_params ModifiedVarSet.pp modified_globals diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 1cc918ee6..99ae8cc40 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -34,3 +34,5 @@ val add_to_errlog : -> Errlog.loc_trace_elem list val join : t -> t -> t + +val pp : Format.formatter -> t -> unit diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 6d6b87a3b..b0fc0fcf6 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -99,7 +99,7 @@ module PulseTransferFunctions = struct >>= PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base - let dispatch_call summary ret call_exp actuals call_loc flags astate = + let dispatch_call tenv summary ret call_exp actuals call_loc flags astate = (* evaluate all actuals *) List.fold_result actuals ~init:(astate, []) ~f:(fun (astate, rev_actuals_evaled) (actual_exp, actual_typ) -> @@ -111,7 +111,7 @@ module PulseTransferFunctions = struct let model = match proc_name_of_call call_exp with | Some callee_pname -> - PulseModels.dispatch callee_pname flags + PulseModels.dispatch tenv callee_pname flags | None -> (* function pointer, etc.: skip for now *) None @@ -139,7 +139,7 @@ module PulseTransferFunctions = struct posts - let exec_instr (astate : Domain.t) {ProcData.summary} _cfg_node (instr : Sil.instr) = + let exec_instr (astate : Domain.t) {tenv; ProcData.summary} _cfg_node (instr : Sil.instr) = match instr with | Load {id= lhs_id; e= rhs_exp; loc} -> (* [lhs_id := *rhs_exp] *) @@ -178,7 +178,8 @@ module PulseTransferFunctions = struct [post] else (* [condition] is known to be unsatisfiable: prune path *) [] | Call (ret, call_exp, actuals, loc, call_flags) -> - dispatch_call summary ret call_exp actuals loc call_flags astate |> check_error summary + dispatch_call tenv summary ret call_exp actuals loc call_flags astate + |> check_error summary | Metadata (ExitScope (vars, location)) -> [PulseOperations.remove_vars vars location astate] | Metadata (VariableLifetimeBegins (pvar, _, location)) -> diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index c59010cf7..7a2cb9b03 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -39,6 +39,14 @@ module Misc = struct let early_exit : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ _ -> Ok [] let skip : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ astate -> Ok [astate] + + let id_first_arg : model = + fun ~caller_summary:_ _ ~ret ~actuals astate -> + match actuals with + | (arg_access_hist, _) :: _ -> + Ok [PulseOperations.write_id (fst ret) arg_access_hist astate] + | _ -> + Ok [astate] end module C = struct @@ -185,9 +193,9 @@ module StdVector = struct Ok [astate] - let at : model = + let at ~desc : model = fun ~caller_summary:_ location ~ret ~actuals astate -> - let event = ValueHistory.Call {f= Model "std::vector::at()"; location; in_call= []} in + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in match actuals with | [(vector, _); (index, _)] -> element_of_internal_array location vector (fst index) astate @@ -228,7 +236,7 @@ module StdVector = struct end module ProcNameDispatcher = struct - let dispatch : (unit, model) ProcnameDispatcher.ProcName.dispatcher = + let dispatch : (Tenv.t, model) ProcnameDispatcher.ProcName.dispatcher = let open ProcnameDispatcher.ProcName in make_dispatcher [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip @@ -243,10 +251,12 @@ module ProcNameDispatcher = struct ; -"std" &:: "vector" &:: "emplace" &--> StdVector.invalidate_references Emplace ; -"std" &:: "vector" &:: "emplace_back" &--> StdVector.invalidate_references EmplaceBack ; -"std" &:: "vector" &:: "insert" &--> StdVector.invalidate_references Insert - ; -"std" &:: "vector" &:: "operator[]" &--> StdVector.at + ; -"std" &:: "vector" &:: "operator[]" &--> StdVector.at ~desc:"std::vector::at()" ; -"std" &:: "vector" &:: "push_back" &--> StdVector.push_back ; -"std" &:: "vector" &:: "reserve" &--> StdVector.reserve - ; -"std" &:: "vector" &:: "shrink_to_fit" &--> StdVector.invalidate_references ShrinkToFit ] + ; -"std" &:: "vector" &:: "shrink_to_fit" &--> StdVector.invalidate_references ShrinkToFit + ; +PatternMatch.implements_collection &:: "get" <>--> StdVector.at ~desc:"Collection.get()" + ; -"__cast" <>--> Misc.id_first_arg ] end let builtins_dispatcher = @@ -274,12 +284,12 @@ let builtins_dispatcher = fun proc_name -> Hashtbl.find builtins_map proc_name -let dispatch proc_name flags = +let dispatch tenv proc_name flags = match builtins_dispatcher proc_name with | Some _ as result -> result | None -> ( - match ProcNameDispatcher.dispatch () proc_name with + match ProcNameDispatcher.dispatch tenv proc_name with | Some _ as result -> result | None -> diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index 841962d5a..ac0589781 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -17,4 +17,4 @@ type exec_fun = type model = exec_fun -val dispatch : Typ.Procname.t -> CallFlags.t -> model option +val dispatch : Tenv.t -> Typ.Procname.t -> CallFlags.t -> model option diff --git a/infer/tests/codetoanalyze/java/impurity/Localities.java b/infer/tests/codetoanalyze/java/impurity/Localities.java index 7aeaba8e8..6c2d743e5 100644 --- a/infer/tests/codetoanalyze/java/impurity/Localities.java +++ b/infer/tests/codetoanalyze/java/impurity/Localities.java @@ -158,4 +158,20 @@ class Localities { s2 = s1; s1 = temp; } + + // @mod:{list} + void modify_first_el_impure(ArrayList list) { + Foo first = list.get(0); + first.x = 0; + } + + Foo get_first_pure(ArrayList list) { + return list.get(0); + } + + // @mod:{list} + void modify_via_call_impure(ArrayList list) { + Foo first = get_first_pure(list); + first.inc_impure(); + } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 7a807414e..de8630d48 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -9,6 +9,8 @@ codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],in codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here] codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here] codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here,parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list` of void Localities.modify_first_el_impure(ArrayList),passed as argument to `Collection.get()` (modelled),return from call to `Collection.get()` (modelled),assigned,assigned,parameter `list` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),parameter `list` of void Localities.modify_via_call_impure(ArrayList),passed as argument to `Localities$Foo Localities.get_first_pure(ArrayList)`,return from call to `Localities$Foo Localities.get_first_pure(ArrayList)`,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here] codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` accessed here,global variable `Test` modified here] codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` of void Test.alias_impure(int[],int,int),assigned,parameter `array` modified here] codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),parameter `this` of void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` of void Test.set_impure(int,int),parameter `this` modified here]