From f0f4fc1f34a3ef8bddeaa25af0d842fe11cb1f42 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=3D=3FUTF-8=3Fq=3FEzgi=3D20=3DC3=3D87i=3DC3=3DA7ek=3F=3D?= Date: Mon, 20 Feb 2023 05:50:46 -0800 Subject: [PATCH 01/25] [report][unnecessary copy] Include point of instantiation in traces Summary: Issues in templated functions were reported at the template definition with a specialized procname that includes the specialized type. However, it is not clear where these functions are instantiated first, making it difficult to understand some issues like unnecessary copies. This diff alleviates this problem by including the point of instantiation in the first step of the trace. Reviewed By: skcho Differential Revision: D43395985 fbshipit-source-id: 3eda9a9c1db64d235ea5897a39db6bd836a19a91 --- infer/src/IR/ProcAttributes.ml | 2 ++ infer/src/IR/ProcAttributes.mli | 3 +++ infer/src/absint/Reporting.ml | 18 +++++++++++++++-- infer/src/absint/Reporting.mli | 8 +++++++- infer/src/pulse/Pulse.ml | 8 +++++++- infer/src/pulse/PulseDiagnostic.ml | 20 ++++++++++++++++--- infer/src/pulse/PulseDiagnostic.mli | 3 +++ infer/src/pulse/PulseReport.ml | 3 ++- infer/tests/codetoanalyze/cpp/pulse/header.h | 12 +++++++++++ .../tests/codetoanalyze/cpp/pulse/issues.exp | 6 ++++-- .../codetoanalyze/cpp/pulse/issues.exp-11 | 8 +++++--- .../cpp/pulse/unnecessary_copy.cpp | 10 ++++++++++ 12 files changed, 88 insertions(+), 13 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/header.h diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml index 7492d334f21..7d4190e7707 100644 --- a/infer/src/IR/ProcAttributes.ml +++ b/infer/src/IR/ProcAttributes.ml @@ -130,6 +130,8 @@ let get_proc_name attributes = attributes.proc_name let get_loc attributes = attributes.loc +let get_loc_instantiated attributes = attributes.loc_instantiated + let to_return_type attributes = if attributes.has_added_return_param then match List.last attributes.formals with diff --git a/infer/src/IR/ProcAttributes.mli b/infer/src/IR/ProcAttributes.mli index a49b05a71b1..10a87f15387 100644 --- a/infer/src/IR/ProcAttributes.mli +++ b/infer/src/IR/ProcAttributes.mli @@ -109,6 +109,9 @@ val get_formals : t -> (Mangled.t * Typ.t * Annot.Item.t) list val get_loc : t -> Location.t (** Return loc information for the procedure *) +val get_loc_instantiated : t -> Location.t option +(** Return instantiated loc information for the procedure *) + val get_proc_name : t -> Procname.t val get_pvar_formals : t -> (Pvar.t * Typ.t) list diff --git a/infer/src/absint/Reporting.ml b/infer/src/absint/Reporting.ml index 245564fdcae..1412a03b490 100644 --- a/infer/src/absint/Reporting.ml +++ b/infer/src/absint/Reporting.ml @@ -8,7 +8,13 @@ open! IStd type log_t = - ?ltr:Errlog.loc_trace -> ?extras:Jsonbug_t.extra -> Checker.t -> IssueType.t -> string -> unit + ?loc_instantiated:Location.t + -> ?ltr:Errlog.loc_trace + -> ?extras:Jsonbug_t.extra + -> Checker.t + -> IssueType.t + -> string + -> unit module Suppression = struct let does_annotation_suppress_issue (kind : IssueType.t) (annot : Annot.t) = @@ -138,7 +144,15 @@ let log_issue_from_summary_simplified ?severity_override proc_desc err_log ~loc ~loc ~ltr ?extras checker issue_to_report -let log_issue proc_desc err_log ~loc ?ltr ?extras checker issue_type error_message = +let log_issue proc_desc err_log ~loc ?loc_instantiated ?ltr ?extras checker issue_type error_message + = + let ltr = + Option.map ltr ~f:(fun default -> + Option.value_map ~default loc_instantiated ~f:(fun loc_instantiated -> + let depth = 0 in + let tags = [] in + Errlog.make_trace_element depth loc_instantiated "first instantiated at" tags :: default ) ) + in log_issue_from_summary_simplified proc_desc err_log ~loc ?ltr ?extras checker issue_type error_message diff --git a/infer/src/absint/Reporting.mli b/infer/src/absint/Reporting.mli index 000f145ae42..b4ce2b50ff7 100644 --- a/infer/src/absint/Reporting.mli +++ b/infer/src/absint/Reporting.mli @@ -10,7 +10,13 @@ open! IStd (** Type of functions to report issues to the error_log in a spec. *) type log_t = - ?ltr:Errlog.loc_trace -> ?extras:Jsonbug_t.extra -> Checker.t -> IssueType.t -> string -> unit + ?loc_instantiated:Location.t + -> ?ltr:Errlog.loc_trace + -> ?extras:Jsonbug_t.extra + -> Checker.t + -> IssueType.t + -> string + -> unit val log_issue_from_summary : ?severity_override:IssueType.severity diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 7a1b54ee180..b834e5a8547 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -52,6 +52,10 @@ let is_type_copiable tenv typ = true +let get_loc_instantiated pname = + IRAttributes.load pname |> Option.bind ~f:ProcAttributes.get_loc_instantiated + + let report_unnecessary_copies proc_desc err_log non_disj_astate = let pname = Procdesc.get_proc_name proc_desc in if is_not_implicit_or_copy_ctor_assignment pname then @@ -59,8 +63,10 @@ let report_unnecessary_copies proc_desc err_log non_disj_astate = |> List.iter ~f:(fun (copied_into, source_typ, location, copied_location, from) -> let copy_name = Format.asprintf "%a" Attribute.CopiedInto.pp copied_into in let is_suppressed = PulseNonDisjunctiveOperations.has_copy_in copy_name in + let location_instantiated = get_loc_instantiated pname in let diagnostic = - Diagnostic.UnnecessaryCopy {copied_into; source_typ; location; copied_location; from} + Diagnostic.UnnecessaryCopy + {copied_into; source_typ; location; copied_location; location_instantiated; from} in PulseReport.report ~is_suppressed ~latent:false proc_desc err_log diagnostic ) diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index d275a8efeeb..29df3e47dd0 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -153,6 +153,7 @@ type t = ; source_typ: Typ.t option ; location: Location.t ; copied_location: (Procname.t * Location.t) option + ; location_instantiated: Location.t option ; from: PulseAttribute.CopyOrigin.t } [@@deriving equal] @@ -211,9 +212,14 @@ let pp fmt diagnostic = ; source_typ: Typ.t option ; location: Location.t ; copied_location: (Procname.t * Location.t) option - ; from: PulseAttribute.CopyOrigin.t } -> + ; from: PulseAttribute.CopyOrigin.t + ; location_instantiated: Location.t option } -> F.fprintf fmt - "UnnecessaryCopy {@[copied_into=%a;@;typ=%a;@;location:%a;@;copied_location:%a@;from=%a@]}" + "UnnecessaryCopy {@[copied_into=%a;@;\ + typ=%a;@;\ + location:%a;@;\ + copied_location:%a@;\ + from=%a;loc_instantiated=%a@]}" PulseAttribute.CopiedInto.pp copied_into (Pp.option (Typ.pp_full Pp.text)) source_typ Location.pp location @@ -222,7 +228,8 @@ let pp fmt diagnostic = F.pp_print_string fmt "none" | Some (callee, location) -> F.fprintf fmt "%a,%a" Procname.pp callee Location.pp location ) - copied_location PulseAttribute.CopyOrigin.pp from + copied_location PulseAttribute.CopyOrigin.pp from (Pp.option Location.pp) + location_instantiated let get_location = function @@ -266,6 +273,13 @@ let get_location = function location +let get_location_instantiated = function + | UnnecessaryCopy {location_instantiated} -> + location_instantiated + | _ -> + None + + let get_copy_type = function | UnnecessaryCopy {source_typ} -> source_typ diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 15b43d3ecee..be1514dea41 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -100,6 +100,7 @@ type t = ; copied_location: (Procname.t * Location.t) option (* [copied_location] has a value when the copied location is different to where to report: e.g. this is the case for returning copied values. *) + ; location_instantiated: Location.t option ; from: PulseAttribute.CopyOrigin.t } [@@deriving equal] @@ -112,6 +113,8 @@ val get_message : t -> string val get_location : t -> Location.t +val get_location_instantiated : t -> Location.t option + val get_copy_type : t -> Typ.t option val get_issue_type : latent:bool -> t -> IssueType.t diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 9bbf6fb066e..3a030d7ffc3 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -17,6 +17,7 @@ let report ~is_suppressed ~latent proc_desc err_log diagnostic = else (* Report suppressed issues with a message to distinguish them from non-suppressed issues. Useful for infer's tests. *) + let loc_instantiated = Diagnostic.get_location_instantiated diagnostic in let extra_trace = if is_suppressed && Config.pulse_report_issues_for_tests then let depth = 0 in @@ -72,7 +73,7 @@ let report ~is_suppressed ~latent proc_desc err_log diagnostic = ; config_usage_extra ; taint_extra } in - Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic) + Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic) ?loc_instantiated ~ltr:(extra_trace @ get_trace diagnostic) ~extras Pulse (get_issue_type ~latent diagnostic) diff --git a/infer/tests/codetoanalyze/cpp/pulse/header.h b/infer/tests/codetoanalyze/cpp/pulse/header.h new file mode 100644 index 00000000000..8ebaffed0c0 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/header.h @@ -0,0 +1,12 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +template +void copy_in_header_bad(const std::vector& arg) { + auto c = arg; // creates a copy +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index cb8662091b7..b48910189a8 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -95,6 +95,8 @@ codetoanalyze/cpp/pulse/funptr.cpp, funptr_conditionnaly_apply_funptr_with_intpt codetoanalyze/cpp/pulse/funptr.cpp, funptr_conditionnaly_apply_funptr_with_intptrptr_specialized_bad, 11, NULLPTR_DEREFERENCE, no_bucket, ERROR, [variable `ptr` declared here,in call to `conditionnaly_apply_funptr_with_intptrptr[specialized with functions]`,is assigned to the null pointer,assigned,return from call to `conditionnaly_apply_funptr_with_intptrptr[specialized with functions]`,invalid access occurs here] codetoanalyze/cpp/pulse/funptr.cpp, test_assign_nullptr_callback_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [parameter `ptr` of test_assign_nullptr_callback_bad,in call to `apply_callback[specialized with functions]`,parameter `ptr` of apply_callback[specialized with functions],in call to `FunPtrCallback::apply[specialized with functions]`,parameter `ptr` of FunPtrCallback::apply[specialized with functions],in call to `assign_nullptr`,is assigned to the null pointer,assigned,return from call to `assign_nullptr`,return from call to `FunPtrCallback::apply[specialized with functions]`,return from call to `apply_callback[specialized with functions]`,invalid access occurs here] codetoanalyze/cpp/pulse/funptr.cpp, test_update_callback_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [parameter `ptr` of test_update_callback_bad,in call to `apply_callback[specialized with functions]`,parameter `ptr` of apply_callback[specialized with functions],in call to `FunPtrCallback::apply[specialized with functions]`,parameter `ptr` of FunPtrCallback::apply[specialized with functions],in call to `assign_nullptr`,is assigned to the null pointer,assigned,return from call to `assign_nullptr`,return from call to `FunPtrCallback::apply[specialized with functions]`,return from call to `apply_callback[specialized with functions]`,invalid access occurs here] +codetoanalyze/cpp/pulse/header.h, copy_in_header_bad, 1, PULSE_UNNECESSARY_COPY, no_bucket, ERROR, [first instantiated at,copied here] +codetoanalyze/cpp/pulse/header.h, copy_in_header_bad, 1, PULSE_UNNECESSARY_COPY, no_bucket, ERROR, [first instantiated at,copied here] codetoanalyze/cpp/pulse/instantiate_pre_addresses.cpp, set_inner_pointer_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `new` (modelled),in call to `mutate_deep_pointers`,is assigned to the constant 24,assigned,return from call to `mutate_deep_pointers`,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] @@ -322,9 +324,9 @@ codetoanalyze/cpp/pulse/taint/strings.cpp, strings::replace2_bad, 3, PULSE_UNNEC codetoanalyze/cpp/pulse/taint/strings.cpp, strings::swap_bad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from __infer_taint_source with kind SimpleSource,in call to function `std::basic_string,std::allocator>::swap` with no summary,in call to function `std::basic_string,std::allocator>::basic_string` with no summary,passed as argument #0 to __infer_taint_sink with kind SimpleSink] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::swap_bad, 4, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1, 0, PULSE_CONST_REFABLE, no_bucket, ERROR, [Parameter fmt] -codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] +codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [first instantiated at,copied here] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format2, 0, PULSE_CONST_REFABLE, no_bucket, ERROR, [Parameter fmt] -codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format2, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] +codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format2, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [first instantiated at,copied here] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1_bad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from __infer_taint_source with kind SimpleSource,passed as argument #0 to __infer_taint_sink with kind SimpleSink] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1_bad, 3, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format2_bad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from __infer_taint_source with kind SimpleSource,passed as argument #0 to __infer_taint_sink with kind SimpleSink] diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp-11 b/infer/tests/codetoanalyze/cpp/pulse/issues.exp-11 index 60851a35360..05236edca34 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp-11 +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp-11 @@ -106,6 +106,8 @@ codetoanalyze/cpp/pulse/funptr.cpp, funptr_conditionnaly_apply_funptr_with_intpt codetoanalyze/cpp/pulse/funptr.cpp, funptr_conditionnaly_apply_funptr_with_intptrptr_specialized_bad, 11, NULLPTR_DEREFERENCE, no_bucket, ERROR, [variable `ptr` declared here,in call to `conditionnaly_apply_funptr_with_intptrptr[specialized with functions]`,is assigned to the null pointer,assigned,return from call to `conditionnaly_apply_funptr_with_intptrptr[specialized with functions]`,invalid access occurs here] codetoanalyze/cpp/pulse/funptr.cpp, test_assign_nullptr_callback_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [parameter `ptr` of test_assign_nullptr_callback_bad,in call to `apply_callback[specialized with functions]`,parameter `ptr` of apply_callback[specialized with functions],in call to `FunPtrCallback::apply[specialized with functions]`,parameter `ptr` of FunPtrCallback::apply[specialized with functions],in call to `assign_nullptr`,is assigned to the null pointer,assigned,return from call to `assign_nullptr`,return from call to `FunPtrCallback::apply[specialized with functions]`,return from call to `apply_callback[specialized with functions]`,invalid access occurs here] codetoanalyze/cpp/pulse/funptr.cpp, test_update_callback_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [parameter `ptr` of test_update_callback_bad,in call to `apply_callback[specialized with functions]`,parameter `ptr` of apply_callback[specialized with functions],in call to `FunPtrCallback::apply[specialized with functions]`,parameter `ptr` of FunPtrCallback::apply[specialized with functions],in call to `assign_nullptr`,is assigned to the null pointer,assigned,return from call to `assign_nullptr`,return from call to `FunPtrCallback::apply[specialized with functions]`,return from call to `apply_callback[specialized with functions]`,invalid access occurs here] +codetoanalyze/cpp/pulse/header.h, copy_in_header_bad, 1, PULSE_UNNECESSARY_COPY, no_bucket, ERROR, [first instantiated at,copied here] +codetoanalyze/cpp/pulse/header.h, copy_in_header_bad, 1, PULSE_UNNECESSARY_COPY, no_bucket, ERROR, [first instantiated at,copied here] codetoanalyze/cpp/pulse/instantiate_pre_addresses.cpp, set_inner_pointer_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `new` (modelled),in call to `mutate_deep_pointers`,is assigned to the constant 24,assigned,return from call to `mutate_deep_pointers`,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] @@ -335,9 +337,9 @@ codetoanalyze/cpp/pulse/taint/strings.cpp, strings::replace2_bad, 3, PULSE_UNNEC codetoanalyze/cpp/pulse/taint/strings.cpp, strings::swap_bad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from __infer_taint_source with kind SimpleSource,in call to function `std::basic_string,std::allocator>::basic_string` with no summary,in call to function `std::basic_string,std::allocator>::swap` with no summary,in call to function `std::basic_string,std::allocator>::basic_string` with no summary,passed as argument #0 to __infer_taint_sink with kind SimpleSink] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::swap_bad, 4, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1, 0, PULSE_CONST_REFABLE, no_bucket, ERROR, [Parameter fmt] -codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] +codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [first instantiated at,copied here] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format2, 0, PULSE_CONST_REFABLE, no_bucket, ERROR, [Parameter fmt] -codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format2, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] +codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format2, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [first instantiated at,copied here] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1_bad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from __infer_taint_source with kind SimpleSource,in call to function `std::basic_string,std::allocator>::basic_string` with no summary,passed as argument #0 to __infer_taint_sink with kind SimpleSink] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format1_bad, 3, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] codetoanalyze/cpp/pulse/taint/strings.cpp, strings::format2_bad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from __infer_taint_source with kind SimpleSource,in call to function `std::basic_string,std::allocator>::basic_string` with no summary,passed as argument #0 to __infer_taint_sink with kind SimpleSink] @@ -442,7 +444,7 @@ codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_in_both_cases_bad, 3, PULSE_U codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_in_both_cases_branch_bad, 3, PULSE_UNNECESSARY_COPY, no_bucket, ERROR, [copied here] codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_modified_after_abort_ok, 5, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,in call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/unnecessary_copy.cpp, ns::creates_copy, 0, PULSE_CONST_REFABLE, no_bucket, ERROR, [Parameter a] -codetoanalyze/cpp/pulse/unnecessary_copy.cpp, ns::creates_copy, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] +codetoanalyze/cpp/pulse/unnecessary_copy.cpp, ns::creates_copy, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [first instantiated at,copied here] codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_via_model_bad, 0, PULSE_CONST_REFABLE, no_bucket, ERROR, [Parameter arr] codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_via_model_bad, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] codetoanalyze/cpp/pulse/unnecessary_copy.cpp, copy_via_model_bad, 1, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/unnecessary_copy.cpp b/infer/tests/codetoanalyze/cpp/pulse/unnecessary_copy.cpp index fafece3af63..cc2d32e7243 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/unnecessary_copy.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/unnecessary_copy.cpp @@ -8,6 +8,7 @@ #include #include #include +#include "header.h" struct Arr { int arr[2]; @@ -668,3 +669,12 @@ class FVector { protected: std::vector table_; }; + +void call_templated_func_specialized_int(const std::vector& arg) { + copy_in_header_bad(arg); +} + +void call_templated_func_specialized_string( + const std::vector& arg) { + copy_in_header_bad(arg); +} From 5aa8f9e1a458de2b0cee6cf6e6a3168aeb10d450 Mon Sep 17 00:00:00 2001 From: Artem Pianykh Date: Mon, 20 Feb 2023 06:39:52 -0800 Subject: [PATCH 02/25] [textual] Register undefined types used in decls as part of tenv Summary: Textual doesn't require that types used inside a module are defined in the module. This leads to undefined types not being a part of the file's tenv which in turn causes problems down the line (e.g. PatternMatch not picking up types when checking againts taint sources/sinks). This diff adds undefined types used in the module's declarations to the tenv. NOTE: the diff doesn't cover types used in alloc and cast expressions. This will be done separately. Reviewed By: davidpichardie, ngorogiannis Differential Revision: D43246895 fbshipit-source-id: f97b4d2e9972ef4e6b7235787fb3a6b61c6e8e7d --- infer/src/istd/HashSet.ml | 12 ++++++++ infer/src/istd/HashSet.mli | 6 ++++ infer/src/textual/TextualDecls.ml | 42 +++++++++++++++++++++++++++ infer/src/textual/TextualDecls.mli | 2 ++ infer/src/textual/TextualSil.ml | 9 +++++- infer/src/textual/unit/TextualTest.ml | 34 ++++++++++++++++++++++ 6 files changed, 104 insertions(+), 1 deletion(-) diff --git a/infer/src/istd/HashSet.ml b/infer/src/istd/HashSet.ml index 6b074ae54d6..96dbd5c91cb 100644 --- a/infer/src/istd/HashSet.ml +++ b/infer/src/istd/HashSet.ml @@ -19,8 +19,14 @@ module type S = sig val add : elt -> t -> unit + val remove : elt -> t -> unit + + val remove_all : elt Iter.t -> t -> unit + val iter : t -> elt Iter.t + val seq : t -> elt Seq.t + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a val length : t -> int @@ -43,8 +49,14 @@ module Make (Key : Hashtbl.HashedType) : S with type elt = Key.t = struct let add x xs = replace xs x () + let remove x xs = remove xs x + let iter xs f = iter (fun x _ -> f x) xs + let seq xs = to_seq_keys xs + + let remove_all it xs = Iter.iter (fun y -> remove y xs) it + let fold f = fold (fun x _ acc -> f x acc) let length = length diff --git a/infer/src/istd/HashSet.mli b/infer/src/istd/HashSet.mli index 0e20be47fae..830bfcffb09 100644 --- a/infer/src/istd/HashSet.mli +++ b/infer/src/istd/HashSet.mli @@ -20,8 +20,14 @@ module type S = sig val add : elt -> t -> unit + val remove : elt -> t -> unit + + val remove_all : elt Iter.t -> t -> unit + val iter : t -> elt Iter.t + val seq : t -> elt Seq.t + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a val length : t -> int diff --git a/infer/src/textual/TextualDecls.ml b/infer/src/textual/TextualDecls.ml index 2fe40140632..42f6850c141 100644 --- a/infer/src/textual/TextualDecls.ml +++ b/infer/src/textual/TextualDecls.ml @@ -7,6 +7,7 @@ open! IStd open Textual +module StringSet = HashSet.Make (String) module QualifiedNameHashtbl = Hashtbl.Make (struct type t = qualified_procname @@ -169,6 +170,47 @@ let check_proc_not_implemented_twice decls errors procdecl = else errors +let get_undefined_types decls = + let referenced_tnames, defined_tnames = (StringSet.create 17, StringSet.create 17) in + (* Helpers *) + let register_tname tname set = StringSet.add tname.TypeName.value set in + let register_tnames tnames set = List.iter tnames ~f:(fun x -> register_tname x set) in + let rec register_typ (typ : Typ.t) set = + match typ with + | Struct tname -> + register_tname tname set + | Ptr typ | Array typ -> + register_typ typ set + | _ -> + () + in + let register_annotated_typ ({typ} : Typ.annotated) set = register_typ typ set in + let register_annotated_typs typs set = + List.iter typs ~f:(fun annotated_typ -> register_annotated_typ annotated_typ set) + in + (* Collect type names from Globals *) + VarName.Hashtbl.to_seq_values decls.globals + |> Seq.iter (fun ({typ} : Global.t) -> register_typ typ referenced_tnames) ; + (* Collect type names from Procdecls *) + QualifiedNameHashtbl.to_seq_values decls.procnames + |> Seq.iter (fun ((procdecl : ProcDecl.t), _) -> + register_annotated_typ procdecl.result_type referenced_tnames ; + register_annotated_typs procdecl.formals_types referenced_tnames ) ; + (* Collect type names from Structs *) + TypeName.Hashtbl.to_seq_values decls.structs + |> Seq.iter (fun (s : Struct.t) -> + register_tname s.name referenced_tnames ; + register_tname s.name defined_tnames ; + register_tnames s.supers referenced_tnames ; + List.iter s.fields ~f:(fun (field : FieldDecl.t) -> + register_tname field.qualified_name.enclosing_class referenced_tnames ; + register_typ field.typ referenced_tnames ) ) ; + (* TODO(arr): collect types from expressions such as alloc and cast. We'll need to extend the + decls with ProcDescs to have access to expressions. *) + StringSet.remove_all (StringSet.iter defined_tnames) referenced_tnames ; + StringSet.seq referenced_tnames + + let make_decls ({decls; sourcefile} : Module.t) : error list * t = let decls_env = init sourcefile in let register errors decl = diff --git a/infer/src/textual/TextualDecls.mli b/infer/src/textual/TextualDecls.mli index f48c359629b..b9072c9400a 100644 --- a/infer/src/textual/TextualDecls.mli +++ b/infer/src/textual/TextualDecls.mli @@ -35,6 +35,8 @@ val is_field_declared : t -> Textual.qualified_fieldname -> bool val source_file : t -> Textual.SourceFile.t +val get_undefined_types : t -> string Seq.t + type error val pp_error : Textual.SourceFile.t -> Format.formatter -> error -> unit diff --git a/infer/src/textual/TextualSil.ml b/infer/src/textual/TextualSil.ml index 57b2f8d3f19..a9f8c822145 100644 --- a/infer/src/textual/TextualSil.ml +++ b/infer/src/textual/TextualSil.ml @@ -82,7 +82,7 @@ module TypeNameBridge = struct JavaClass (replace_2colons_with_dot string |> JavaClassName.from_string) - let to_sil (lang : Lang.t) {value} : SilTyp.Name.t = + let value_to_sil (lang : Lang.t) value : SilTyp.Name.t = match lang with | Java -> string_to_java_sil value @@ -90,6 +90,8 @@ module TypeNameBridge = struct HackClass (HackClassName.make value) + let to_sil (lang : Lang.t) {value} = value_to_sil lang value + let java_lang_object = of_java_name "java.lang.Object" let hack_mixed = SilTyp.HackClass (HackClassName.make "Mixed") @@ -883,6 +885,11 @@ module ModuleBridge = struct Java examples are not in SSA *) SsaVerification.run pdesc ; ProcDescBridge.to_sil lang decls_env cfgs pdesc ) ; + (* Register undefined types in tenv *) + TextualDecls.get_undefined_types decls_env + |> Seq.iter (fun tname -> + let sil_tname = TypeNameBridge.value_to_sil lang tname in + Tenv.mk_struct ~dummy:true tenv sil_tname |> ignore ) ; (cfgs, tenv) diff --git a/infer/src/textual/unit/TextualTest.ml b/infer/src/textual/unit/TextualTest.ml index fdffdfacfa3..4752c525c03 100644 --- a/infer/src/textual/unit/TextualTest.ml +++ b/infer/src/textual/unit/TextualTest.ml @@ -214,6 +214,40 @@ let%test_module "to_sil" = List.iter errs ~f:(Textual.pp_transform_error sourcefile F.std_formatter) ; [%expect {| dummy.sil, : transformation error: Missing or unsupported source_language attribute |}] + + let%expect_test "undefined types are included in tenv" = + let source = + {| + .source_language = "hack" + type Foo {} + define f(arg1: Foo, arg2: Bar) : void { #n: ret null } + |} + in + let m = parse_module source in + let _, tenv = TextualSil.module_to_sil m in + F.printf "%a@\n" Tenv.pp tenv ; + [%expect + {| + hack Bar + fields: {} + statics: {} + supers: {} + objc_protocols: {} + methods: {} + exported_obj_methods: {} + annots: {<>} + java_class_info: {[None]} + dummy: true + hack Foo + fields: {} + statics: {} + supers: {} + objc_protocols: {} + methods: {} + exported_obj_methods: {} + annots: {<>} + java_class_info: {[None]} + dummy: false |}] end ) let%test_module "remove_internal_calls transformation" = From ac03fddb3e37296b153e505a0638f27a3ac16c1f Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 20 Feb 2023 06:51:57 -0800 Subject: [PATCH 03/25] [unnecessary copy][refactoring] Set suggestion message in on place Reviewed By: ezgicicek Differential Revision: D43398457 fbshipit-source-id: 80997473252ff45a7b6244363273138278740ef5 --- infer/src/pulse/PulseDiagnostic.ml | 33 +++++++++++++++--------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 29df3e47dd0..a1ed05701a6 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -617,20 +617,24 @@ let get_message diagnostic = hence suppress the warning" in let suggestion_msg = - match (from : CopyOrigin.t) with - | CopyCtor -> + match (from, copied_into) with + | _, IntoIntermediate _ -> + suggestion_msg_move + | _, IntoField _ -> + "Rather than copying into the field, consider moving into it instead" + | CopyCtor, IntoVar _ -> "To avoid the copy, try using a reference `&`" - | CopyAssignment -> + | CopyAssignment, IntoVar _ -> suggestion_msg_move in match copied_into with | IntoIntermediate {source_opt= None} -> F.asprintf "An intermediate%a is %a on %a. %s." pp_typ source_typ CopyOrigin.pp from - Location.pp_line location suggestion_msg_move + Location.pp_line location suggestion_msg | IntoIntermediate {source_opt= Some source_expr} -> F.asprintf "variable `%a`%a is %a unnecessarily into an intermediate on %a. %s." DecompilerExpr.pp_source_expr source_expr pp_typ source_typ CopyOrigin.pp from - Location.pp_line location suggestion_msg_move + Location.pp_line location suggestion_msg | IntoVar {source_opt= None} -> F.asprintf "%a variable `%a` is not modified after it is copied from a source%a on %a. %s. %s." @@ -641,17 +645,14 @@ let get_message diagnostic = "%a variable `%a` is not modified after it is copied from `%a`%a on %a. %s. %s." CopyOrigin.pp from CopiedInto.pp copied_into DecompilerExpr.pp_source_expr source_expr pp_typ source_typ Location.pp_line location suggestion_msg suppression_msg - | IntoField {field; source_opt} -> ( - let advice = "Rather than copying into the field, consider moving into it instead." in - match source_opt with - | Some source_expr -> - F.asprintf "`%a`%a is %a into field `%a` but is not modified afterwards. %s" - DecompilerExpr.pp source_expr pp_typ source_typ CopyOrigin.pp from Fieldname.pp - field advice - | None -> - F.asprintf - "Field `%a` is %a into from an rvalue-ref%a but is not modified afterwards. %s" - Fieldname.pp field CopyOrigin.pp from pp_typ source_typ advice ) ) + | IntoField {field; source_opt= None} -> + F.asprintf + "Field `%a` is %a into from an rvalue-ref%a but is not modified afterwards. %s." + Fieldname.pp field CopyOrigin.pp from pp_typ source_typ suggestion_msg + | IntoField {field; source_opt= Some source_expr} -> + F.asprintf "`%a`%a is %a into field `%a` but is not modified afterwards. %s." + DecompilerExpr.pp source_expr pp_typ source_typ CopyOrigin.pp from Fieldname.pp field + suggestion_msg ) let add_errlog_header ~nesting ~title location errlog = From baddbd71c2748cbb06f564f33729ca5b64b0bdb3 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 20 Feb 2023 10:54:20 -0800 Subject: [PATCH 04/25] [unnecessary copy] Introduce separate issue types (copy to Optional) Summary: This diff introduces separate issue types: copy to optional value. Reviewed By: ezgicicek Differential Revision: D43392227 fbshipit-source-id: 8d954346c280115490cd89a0f1db5d1a736df693 --- .../issues/PULSE_UNNECESSARY_COPY_OPTIONAL.md | 15 +++++++++++ infer/man/man1/infer-full.txt | 2 ++ infer/man/man1/infer-report.txt | 2 ++ infer/man/man1/infer.txt | 2 ++ infer/src/base/IssueType.ml | 12 +++++++++ infer/src/base/IssueType.mli | 4 +++ infer/src/pulse/PulseAttribute.ml | 4 ++- infer/src/pulse/PulseAttribute.mli | 2 +- infer/src/pulse/PulseDiagnostic.ml | 7 +++++ .../pulse/PulseNonDisjunctiveOperations.ml | 2 +- .../build_systems/pulse_messages/issues.exp | 27 ++++++++++--------- .../pulse_messages/unnecessary_copy.cpp | 8 ++++++ .../codetoanalyze/cpp/pulse-17/issues.exp | 4 +-- 13 files changed, 73 insertions(+), 18 deletions(-) create mode 100644 infer/documentation/issues/PULSE_UNNECESSARY_COPY_OPTIONAL.md diff --git a/infer/documentation/issues/PULSE_UNNECESSARY_COPY_OPTIONAL.md b/infer/documentation/issues/PULSE_UNNECESSARY_COPY_OPTIONAL.md new file mode 100644 index 00000000000..744babbfdab --- /dev/null +++ b/infer/documentation/issues/PULSE_UNNECESSARY_COPY_OPTIONAL.md @@ -0,0 +1,15 @@ +This is reported when Infer detects an unnecessary copy of an object via `optional` value +construction where the source is not modified before it goes out of scope. To avoid the copy, we +can move the source object or change the callee's type. + +For example, + +```cpp +void get_optional_value(std::optional x) {} + +void pass_non_optional_value(A x) { + get_optional_value(x); + // fix is to move as follows + // get_optional_value(std::move(x)); +} +``` diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index b6a44034416..c4bbbe84f1e 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -628,6 +628,8 @@ OPTIONS PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by default), PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default), + PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default), + PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default), PULSE_UNNECESSARY_COPY_RETURN (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index a7e3ac44cd8..887e384db4b 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -278,6 +278,8 @@ OPTIONS PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by default), PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default), + PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default), + PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default), PULSE_UNNECESSARY_COPY_RETURN (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 73da822377a..da0f2129c70 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -628,6 +628,8 @@ OPTIONS PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by default), PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default), + PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default), + PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default), PULSE_UNNECESSARY_COPY_RETURN (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 809f8d45d47..515339b0b27 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -1115,6 +1115,18 @@ let unnecessary_copy_movable_pulse = ~user_documentation:[%blob "./documentation/issues/PULSE_UNNECESSARY_COPY_MOVABLE.md"] +let unnecessary_copy_optional_pulse = + register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY_OPTIONAL" Error Pulse + ~hum:"Unnecessary Copy to Optional" + ~user_documentation:[%blob "./documentation/issues/PULSE_UNNECESSARY_COPY_OPTIONAL.md"] + + +let unnecessary_copy_optional_const_pulse = + register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY_OPTIONAL_CONST" Error Pulse + ~hum:"Unnecessary Copy to Optional from Const" + ~user_documentation:"See [PULSE_UNNECESSARY_COPY_OPTIONAL](#pulse_unnecessary_copy_optional)." + + let unnecessary_copy_return_pulse = register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY_RETURN" Error Pulse ~hum:"Unnecessary Copy Return" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 42aa655de79..fe33f1580cf 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -388,6 +388,10 @@ val unnecessary_copy_intermediate_const_pulse : t val unnecessary_copy_movable_pulse : t +val unnecessary_copy_optional_pulse : t + +val unnecessary_copy_optional_const_pulse : t + val unnecessary_copy_return_pulse : t val unreachable_code_after : t diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 7ec02cd23f1..5bca3ac9a99 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -95,13 +95,15 @@ module Attribute = struct module TaintSanitizedSet = PrettyPrintable.MakePPSet (TaintSanitized) module CopyOrigin = struct - type t = CopyCtor | CopyAssignment [@@deriving compare, equal] + type t = CopyCtor | CopyAssignment | CopyToOptional [@@deriving compare, equal] let pp fmt = function | CopyCtor -> F.fprintf fmt "copied" | CopyAssignment -> F.fprintf fmt "copy assigned" + | CopyToOptional -> + F.fprintf fmt "copied by Optional value construction" end module CopiedInto = struct diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 06c4ec9aa38..0f894370830 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -54,7 +54,7 @@ end module TaintSanitizedSet : PrettyPrintable.PPSet with type elt = TaintSanitized.t module CopyOrigin : sig - type t = CopyCtor | CopyAssignment [@@deriving compare, equal] + type t = CopyCtor | CopyAssignment | CopyToOptional [@@deriving compare, equal] val pp : Formatter.t -> t -> unit end diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index a1ed05701a6..411ffaf491c 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -618,6 +618,9 @@ let get_message diagnostic = in let suggestion_msg = match (from, copied_into) with + | CopyToOptional, _ -> + if is_from_const then suggestion_msg_move + else suggestion_msg_move ^ " or changing the callee's type" | _, IntoIntermediate _ -> suggestion_msg_move | _, IntoField _ -> @@ -918,6 +921,10 @@ let get_issue_type ~latent issue_type = if Option.exists ~f:Typ.is_const_reference source_typ then IssueType.unnecessary_copy_assignment_const_pulse else IssueType.unnecessary_copy_assignment_pulse + | UnnecessaryCopy {source_typ; from= CopyToOptional}, false -> + if Option.exists ~f:Typ.is_const_reference source_typ then + IssueType.unnecessary_copy_optional_const_pulse + else IssueType.unnecessary_copy_optional_pulse | ( ( ConfigUsage _ | ConstRefableParameter _ | CSharpResourceLeak _ diff --git a/infer/src/pulse/PulseNonDisjunctiveOperations.ml b/infer/src/pulse/PulseNonDisjunctiveOperations.ml index 4cc6d4a099d..331ffeb3f80 100644 --- a/infer/src/pulse/PulseNonDisjunctiveOperations.ml +++ b/infer/src/pulse/PulseNonDisjunctiveOperations.ml @@ -83,7 +83,7 @@ let get_element_copy_by_optional = if is_optional_copy_constructor_with_arg_payloads pname arg_payloads then None else dispatch () pname arg_payloads - |> Option.bind ~f:(fun matched -> Option.some_if matched Attribute.CopyOrigin.CopyCtor) + |> Option.bind ~f:(fun matched -> Option.some_if matched Attribute.CopyOrigin.CopyToOptional) let try_eval path location e astate = diff --git a/infer/tests/build_systems/pulse_messages/issues.exp b/infer/tests/build_systems/pulse_messages/issues.exp index 85e1937f50d..e8bb36a817b 100644 --- a/infer/tests/build_systems/pulse_messages/issues.exp +++ b/infer/tests/build_systems/pulse_messages/issues.exp @@ -31,19 +31,20 @@ build_systems/pulse_messages/optional.cpp, optional_empty_access::latent, 38, 13 build_systems/pulse_messages/optional.cpp, optional_empty_access::make_latent_manifest, 48, 31, ERROR, OPTIONAL_EMPTY_ACCESS, The call to `optional_empty_access::propagate_latent_3_latent` ends up calling `optional_empty_access::latent` (after 2 more calls) and may trigger the following issue: call to `optional_empty_access::propagate_latent_3_latent()` eventually accesses memory that is assigned an empty value during the call to `optional_empty_access::propagate_latent_3_latent()` on line 37. build_systems/pulse_messages/readonly_shared_ptr_param.cpp, read_shared_ptr_param, 11, 1, ERROR, PULSE_READONLY_SHARED_PTR_PARAM, Function parameter `x` with type `std::shared_ptr` is passed by-value but its lifetime is not extended inside the function on line 11. This might result in an unnecessary copy at the callsite of this function. Consider passing a raw pointer instead and changing its usages if necessary at line 14. build_systems/pulse_messages/readonly_shared_ptr_param.cpp, multiple_read_shared_ptr_param, 17, 1, ERROR, PULSE_READONLY_SHARED_PTR_PARAM, Function parameter `x` with type `std::shared_ptr` is passed by-value but its lifetime is not extended inside the function on line 17. This might result in an unnecessary copy at the callsite of this function. Consider passing a raw pointer instead and changing its usages if necessary at line 19, line 21. -build_systems/pulse_messages/unnecessary_copy.cpp, copy_decl_bad, 20, 14, ERROR, PULSE_UNNECESSARY_COPY, copied variable `cpy` is not modified after it is copied from `get_a_ref()` with type `A&` on line 20. To avoid the copy, try using a reference `&`. If this copy was intentional, consider calling `folly::copy` to make it explicit and hence suppress the warning. -build_systems/pulse_messages/unnecessary_copy.cpp, copy_assignment_bad, 25, 1, ERROR, PULSE_CONST_REFABLE, Function parameter `source` with type `A` is passed by-value but not modified inside the function on line 25. This might result in an unnecessary copy at the callsite of this function. Consider changing the type of this function parameter to `const &`. -build_systems/pulse_messages/unnecessary_copy.cpp, copy_assignment_bad, 27, 3, ERROR, PULSE_UNNECESSARY_COPY_ASSIGNMENT, copy assigned variable `c` is not modified after it is copied from `source` with type `A&` on line 27. To avoid the copy, try moving it by calling `std::move` instead. If this copy was intentional, consider calling `folly::copy` to make it explicit and hence suppress the warning. -build_systems/pulse_messages/unnecessary_copy.cpp, Test::unnecessary_copy_moveable_bad, 33, 47, ERROR, PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE, `a` with type `A&&` is copy assigned into field `mem_a` but is not modified afterwards. Rather than copying into the field, consider moving into it instead. -build_systems/pulse_messages/unnecessary_copy.cpp, Test::intermediate_member_field_copy_bad, 37, 33, ERROR, PULSE_UNNECESSARY_COPY_INTERMEDIATE, variable `&a` with type `A&` is copied unnecessarily into an intermediate on line 37. To avoid the copy, try moving it by calling `std::move` instead. -build_systems/pulse_messages/unnecessary_copy.cpp, get_size, 41, 1, ERROR, PULSE_CONST_REFABLE, Function parameter `a` with type `A` is passed by-value but not modified inside the function on line 41. This might result in an unnecessary copy at the callsite of this function. Consider changing the type of this function parameter to `const &`. -build_systems/pulse_messages/unnecessary_copy.cpp, unnecessary_intermediate_copy, 46, 12, ERROR, PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST, variable `my_a` with type `A const &` is copied unnecessarily into an intermediate on line 46. To avoid the copy, try 1) removing the `const &` from the source and 2) moving it by calling `std::move` instead. -build_systems/pulse_messages/unnecessary_copy.cpp, call_value_or_bad, 65, 9, ERROR, PULSE_UNNECESSARY_COPY_RETURN, the return value `g` is not modified after it is copied in the callee `MyValueOr::value_or` with type `A` at `build_systems/pulse_messages/unnecessary_copy.cpp:56`. Please check if we can avoid the copy, e.g. by changing the return type of `MyValueOr::value_or` or by revising the function body of it. -build_systems/pulse_messages/unnecessary_copy.cpp, call_value_or_bad, 65, 9, ERROR, PULSE_UNNECESSARY_COPY_RETURN, the return value `g` is not modified after it is copied in the callee `MyValueOr::value_or` with type `A` at `build_systems/pulse_messages/unnecessary_copy.cpp:58`. Please check if we can avoid the copy, e.g. by changing the return type of `MyValueOr::value_or` or by revising the function body of it. -build_systems/pulse_messages/unnecessary_copy.cpp, ns::creates_copy, 71, 1, ERROR, PULSE_CONST_REFABLE, Function parameter `a` with type `A` is passed by-value but not modified inside the function on line 71. This might result in an unnecessary copy at the callsite of this function. Consider changing the type of this function parameter to `const &`. -build_systems/pulse_messages/unnecessary_copy.cpp, intermediate_copy_via_model_bad, 76, 1, ERROR, PULSE_CONST_REFABLE, Function parameter `arr` with type `A` is passed by-value but not modified inside the function on line 76. This might result in an unnecessary copy at the callsite of this function. Consider changing the type of this function parameter to `const &`. -build_systems/pulse_messages/unnecessary_copy.cpp, intermediate_copy_via_model_bad, 77, 12, ERROR, PULSE_UNNECESSARY_COPY_INTERMEDIATE, An intermediate with type `A` is copied on line 77. To avoid the copy, try moving it by calling `std::move` instead. -build_systems/pulse_messages/unnecessary_copy.cpp, intermediate_copy_via_model_bad, 78, 7, ERROR, PULSE_UNNECESSARY_COPY_INTERMEDIATE, variable `arr` with type `A&` is copied unnecessarily into an intermediate on line 78. To avoid the copy, try moving it by calling `std::move` instead. +build_systems/pulse_messages/unnecessary_copy.cpp, copy_decl_bad, 21, 14, ERROR, PULSE_UNNECESSARY_COPY, copied variable `cpy` is not modified after it is copied from `get_a_ref()` with type `A&` on line 21. To avoid the copy, try using a reference `&`. If this copy was intentional, consider calling `folly::copy` to make it explicit and hence suppress the warning. +build_systems/pulse_messages/unnecessary_copy.cpp, copy_assignment_bad, 26, 1, ERROR, PULSE_CONST_REFABLE, Function parameter `source` with type `A` is passed by-value but not modified inside the function on line 26. This might result in an unnecessary copy at the callsite of this function. Consider changing the type of this function parameter to `const &`. +build_systems/pulse_messages/unnecessary_copy.cpp, copy_assignment_bad, 28, 3, ERROR, PULSE_UNNECESSARY_COPY_ASSIGNMENT, copy assigned variable `c` is not modified after it is copied from `source` with type `A&` on line 28. To avoid the copy, try moving it by calling `std::move` instead. If this copy was intentional, consider calling `folly::copy` to make it explicit and hence suppress the warning. +build_systems/pulse_messages/unnecessary_copy.cpp, Test::unnecessary_copy_moveable_bad, 34, 47, ERROR, PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE, `a` with type `A&&` is copy assigned into field `mem_a` but is not modified afterwards. Rather than copying into the field, consider moving into it instead. +build_systems/pulse_messages/unnecessary_copy.cpp, Test::intermediate_member_field_copy_bad, 38, 33, ERROR, PULSE_UNNECESSARY_COPY_INTERMEDIATE, variable `&a` with type `A&` is copied unnecessarily into an intermediate on line 38. To avoid the copy, try moving it by calling `std::move` instead. +build_systems/pulse_messages/unnecessary_copy.cpp, get_size, 42, 1, ERROR, PULSE_CONST_REFABLE, Function parameter `a` with type `A` is passed by-value but not modified inside the function on line 42. This might result in an unnecessary copy at the callsite of this function. Consider changing the type of this function parameter to `const &`. +build_systems/pulse_messages/unnecessary_copy.cpp, unnecessary_intermediate_copy, 47, 12, ERROR, PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST, variable `my_a` with type `A const &` is copied unnecessarily into an intermediate on line 47. To avoid the copy, try 1) removing the `const &` from the source and 2) moving it by calling `std::move` instead. +build_systems/pulse_messages/unnecessary_copy.cpp, call_value_or_bad, 66, 9, ERROR, PULSE_UNNECESSARY_COPY_RETURN, the return value `g` is not modified after it is copied in the callee `MyValueOr::value_or` with type `A` at `build_systems/pulse_messages/unnecessary_copy.cpp:57`. Please check if we can avoid the copy, e.g. by changing the return type of `MyValueOr::value_or` or by revising the function body of it. +build_systems/pulse_messages/unnecessary_copy.cpp, call_value_or_bad, 66, 9, ERROR, PULSE_UNNECESSARY_COPY_RETURN, the return value `g` is not modified after it is copied in the callee `MyValueOr::value_or` with type `A` at `build_systems/pulse_messages/unnecessary_copy.cpp:59`. Please check if we can avoid the copy, e.g. by changing the return type of `MyValueOr::value_or` or by revising the function body of it. +build_systems/pulse_messages/unnecessary_copy.cpp, ns::creates_copy, 72, 1, ERROR, PULSE_CONST_REFABLE, Function parameter `a` with type `A` is passed by-value but not modified inside the function on line 72. This might result in an unnecessary copy at the callsite of this function. Consider changing the type of this function parameter to `const &`. +build_systems/pulse_messages/unnecessary_copy.cpp, intermediate_copy_via_model_bad, 77, 1, ERROR, PULSE_CONST_REFABLE, Function parameter `arr` with type `A` is passed by-value but not modified inside the function on line 77. This might result in an unnecessary copy at the callsite of this function. Consider changing the type of this function parameter to `const &`. +build_systems/pulse_messages/unnecessary_copy.cpp, intermediate_copy_via_model_bad, 78, 12, ERROR, PULSE_UNNECESSARY_COPY_INTERMEDIATE, An intermediate with type `A` is copied on line 78. To avoid the copy, try moving it by calling `std::move` instead. +build_systems/pulse_messages/unnecessary_copy.cpp, intermediate_copy_via_model_bad, 79, 7, ERROR, PULSE_UNNECESSARY_COPY_INTERMEDIATE, variable `arr` with type `A&` is copied unnecessarily into an intermediate on line 79. To avoid the copy, try moving it by calling `std::move` instead. +build_systems/pulse_messages/unnecessary_copy.cpp, call_get_optional_value_bad, 86, 22, ERROR, PULSE_UNNECESSARY_COPY_OPTIONAL, variable `x` with type `A&` is copied by Optional value construction unnecessarily into an intermediate on line 86. To avoid the copy, try moving it by calling `std::move` instead or changing the callee's type. build_systems/pulse_messages/use_after_free.c, uaf_intraprocedural_bad, 12, 11, ERROR, USE_AFTER_FREE, accessing memory that was invalidated by call to `free()` on line 11. build_systems/pulse_messages/use_after_free.c, free_wrapper_uaf_bad, 19, 11, ERROR, USE_AFTER_FREE, accessing memory that was invalidated by call to `free()` during the call to `free_wrapper()` on line 18. build_systems/pulse_messages/use_after_free.c, uaf_via_deref_bad, 26, 3, ERROR, USE_AFTER_FREE, call to `deref_int()` eventually accesses memory that was invalidated by call to `free()` on line 25. diff --git a/infer/tests/build_systems/pulse_messages/unnecessary_copy.cpp b/infer/tests/build_systems/pulse_messages/unnecessary_copy.cpp index bb8eabb9f9c..fe660b95b2f 100644 --- a/infer/tests/build_systems/pulse_messages/unnecessary_copy.cpp +++ b/infer/tests/build_systems/pulse_messages/unnecessary_copy.cpp @@ -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. */ +#include #include #include @@ -77,3 +78,10 @@ void intermediate_copy_via_model_bad(A arr) { get_size(ns::creates_copy( arr)); // creates an intermediate copy (via model/unknown) } + +void get_optional_value(std::optional x) {} + +void call_get_optional_value_bad(A x) { + x.vec[0] = 42; + get_optional_value(x); +} diff --git a/infer/tests/codetoanalyze/cpp/pulse-17/issues.exp b/infer/tests/codetoanalyze/cpp/pulse-17/issues.exp index 86394272668..d21c2414bf5 100644 --- a/infer/tests/codetoanalyze/cpp/pulse-17/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse-17/issues.exp @@ -32,5 +32,5 @@ codetoanalyze/cpp/pulse-17/std_optional.cpp, std_operator_arrow_bad, 0, OPTIONAL codetoanalyze/cpp/pulse-17/std_optional.cpp, might_return_none, 0, PULSE_CONST_REFABLE, no_bucket, ERROR, [Parameter x] codetoanalyze/cpp/pulse-17/std_optional.cpp, FP_cannot_be_empty, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `getEnum`,in call to function `getenv` with no summary,assigned,taking "then" branch,is assigned to the null pointer,returned,return from call to `getEnum`,taking "then" branch,variable `C++ temporary` declared here,in call to `getOptionalValue`,in call to `std::optional::optional(=nullopt)` (modelled),is assigned an empty value,return from call to `getOptionalValue`,invalid access occurs here] codetoanalyze/cpp/pulse-17/std_optional.cpp, inside_try_catch_FP, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [variable `foo` accessed here,in call to `might_return_none`,parameter `b` of might_return_none,taking "then" branch,in call to `std::optional::optional(=nullopt)` (modelled),is assigned an empty value,return from call to `might_return_none`,invalid access occurs here] -codetoanalyze/cpp/pulse-17/unnecessary_copy.cpp, unnecessary_copy::call_get_optional_const_ref_bad, 2, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] -codetoanalyze/cpp/pulse-17/unnecessary_copy.cpp, unnecessary_copy::call_get_optional_value_bad, 2, PULSE_UNNECESSARY_COPY_INTERMEDIATE, no_bucket, ERROR, [copied here] +codetoanalyze/cpp/pulse-17/unnecessary_copy.cpp, unnecessary_copy::call_get_optional_const_ref_bad, 2, PULSE_UNNECESSARY_COPY_OPTIONAL, no_bucket, ERROR, [copied by Optional value construction here] +codetoanalyze/cpp/pulse-17/unnecessary_copy.cpp, unnecessary_copy::call_get_optional_value_bad, 2, PULSE_UNNECESSARY_COPY_OPTIONAL, no_bucket, ERROR, [copied by Optional value construction here] From b84a5f8449d21154a073ad5b3866351411c43e46 Mon Sep 17 00:00:00 2001 From: Artem Pianykh Date: Tue, 21 Feb 2023 08:10:44 -0800 Subject: [PATCH 05/25] [misc] Flush formatters in the parent to avoid double printing Summary: In ForkUtils.protect we already do Logging.reset_formatters which flushes formatters, but this happens in children. We need to flush *in the parent* before we fork to avoid carrying over stale buffers. This diff adds a call to Logging.flush_formatters to ProcessPool before it forks children. This is not a bullet proof fix (ideally, we should flush in the parent before *every* call to fork), but it works fine and gets rid of some double printing I saw. Reviewed By: rumster Differential Revision: D43452027 fbshipit-source-id: 4e303110ee88a3bdd758feb0840c9485bbf33459 --- infer/src/base/Logging.ml | 12 ++++++++---- infer/src/base/Logging.mli | 5 ++++- infer/src/base/ProcessPool.ml | 2 ++ infer/src/integration/Hack.ml | 3 +-- 4 files changed, 15 insertions(+), 7 deletions(-) diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml index 7fdf5e5349f..cd078df07c3 100644 --- a/infer/src/base/Logging.ml +++ b/infer/src/base/Logging.ml @@ -143,14 +143,18 @@ let register_formatter = formatters_ref ) -let flush_formatters {file; console_file} = +let flush_formatter {file; console_file} = Option.iter file ~f:(fun file -> F.pp_print_flush file ()) ; F.pp_print_flush console_file () +let flush_formatters () = + let flush (formatters, _) = flush_formatter !formatters in + List.iter ~f:flush !logging_formatters + + let close_logs () = - let close_fmt (formatters, _) = flush_formatters !formatters in - List.iter ~f:close_fmt !logging_formatters ; + flush_formatters () ; Option.iter !log_file ~f:(function file_fmt, chan -> F.pp_print_flush file_fmt () ; Out_channel.close chan ) @@ -163,7 +167,7 @@ let register_epilogue () = let reset_formatters () = let refresh_formatter (formatters, mk_formatters) = (* flush to be nice *) - flush_formatters !formatters ; + flush_formatter !formatters ; (* recreate formatters, in particular update PID info *) formatters := mk_formatters () in diff --git a/infer/src/base/Logging.mli b/infer/src/base/Logging.mli index 0c400555b90..ea0fe1748e8 100644 --- a/infer/src/base/Logging.mli +++ b/infer/src/base/Logging.mli @@ -80,8 +80,11 @@ val pp_ocaml_pos_opt : F.formatter -> ocaml_pos option -> unit val setup_log_file : unit -> unit (** Set up logging to go to the log file. Call this once the results directory has been set up. *) +val flush_formatters : unit -> unit +(** Flushes the formatters used for logging. Call this in the parent before you fork(2). *) + val reset_formatters : unit -> unit -(** Reset the formatters used for logging. Call this when you fork(2). *) +(** Reset the formatters used for logging. Call this in the child after you fork(2). *) (** Delayed printing (HTML debug, ...) *) diff --git a/infer/src/base/ProcessPool.ml b/infer/src/base/ProcessPool.ml index 96d51a2e118..5cef77236a1 100644 --- a/infer/src/base/ProcessPool.ml +++ b/infer/src/base/ProcessPool.ml @@ -456,6 +456,8 @@ let create : fun ~jobs ~child_prologue ~f ~child_epilogue ~tasks -> let task_bar = TaskBar.create ~jobs in let children_pipes = create_pipes jobs in + (* Flush formatters in the parent before we start forking children. *) + L.flush_formatters () ; let slots = Array.init jobs ~f:(fun slot -> let child_pipe = List.nth_exn children_pipes slot in diff --git a/infer/src/integration/Hack.ml b/infer/src/integration/Hack.ml index c470ffc5834..874894bdc5f 100644 --- a/infer/src/integration/Hack.ml +++ b/infer/src/integration/Hack.ml @@ -250,8 +250,7 @@ end When the whole compilation unit has been accumulated, [Unit.capture_unit] is called. *) let process_output ic = let unit_count, units = Unit.extract_units ic in - (* Use @. to flush the format buffer and avoid double printing in child processes. *) - Option.iter unit_count ~f:(L.progress "Expecting to capture %d files@.") ; + Option.iter unit_count ~f:(L.progress "Expecting to capture %d files@\n") ; let n_captured, n_error = (ref 0, ref 0) in (* action's output and on_finish's input are connected and consistent with ProcessPool.TaskGenerator's contract *) From ba8c1aa653155d59739f40188e791ecf94281acf Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Wed, 22 Feb 2023 01:59:43 -0800 Subject: [PATCH 06/25] [buck2][clang] use a bxl script for query&capture Summary: Buck2 Extension Language (BXL) allows writing scripts in Starlark that directly interact with buck2 internals. For Infer, this means that the two buck invocations typically used (query and build) can be combined into a single invocation, which avoids constructing or traversing the build graph twice. The script is provided externally through a configuration option. Reviewed By: rumster Differential Revision: D43347630 fbshipit-source-id: ef2a4159567a5ee83fa07b8a170ffd7e3dc1fca5 --- infer/man/man1/infer-capture.txt | 8 +++++ infer/man/man1/infer-full.txt | 11 ++++++ infer/man/man1/infer.txt | 8 +++++ infer/src/base/Config.ml | 16 +++++++++ infer/src/base/Config.mli | 4 +++ infer/src/integration/Buck.ml | 2 ++ infer/src/integration/BxlClang.ml | 57 ++++++++++++++++++++++++++++++ infer/src/integration/BxlClang.mli | 11 ++++++ infer/src/integration/Driver.ml | 8 +++++ infer/src/integration/Driver.mli | 1 + 10 files changed, 126 insertions(+) create mode 100644 infer/src/integration/BxlClang.ml create mode 100644 infer/src/integration/BxlClang.mli diff --git a/infer/man/man1/infer-capture.txt b/infer/man/man1/infer-capture.txt index 51ca5253209..770f7f1e966 100644 --- a/infer/man/man1/infer-capture.txt +++ b/infer/man/man1/infer-capture.txt @@ -202,9 +202,17 @@ BUCK OPTIONS Skip capture of buck targets matched by the specified regular expression. + --buck2-bxl-target string + Buck2 BXL script (as a buck target) to run when capturing with + buck2/clang integration. + --buck2-root dir Specify the parent directory of buck-out (used only for buck2). + --buck2-use-bxl + Activates: Use BXL script when capturing with buck2. (Conversely: + --no-buck2-use-bxl) + --Xbuck +string Pass values as command-line arguments to invocations of `buck build`. Only valid for --buck-clang. diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index c4bbbe84f1e..f010d745210 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -223,10 +223,18 @@ OPTIONS Skip capture of buck targets matched by the specified regular expression. See also infer-capture(1) and infer-run(1). + --buck2-bxl-target string + Buck2 BXL script (as a buck target) to run when capturing with + buck2/clang integration. See also infer-capture(1). + --buck2-root dir Specify the parent directory of buck-out (used only for buck2). See also infer-capture(1) and infer-run(1). + --buck2-use-bxl + Activates: Use BXL script when capturing with buck2. (Conversely: + --no-buck2-use-bxl) See also infer-capture(1). + --bufferoverrun Activates: checker bufferoverrun: InferBO is a detector for out-of-bounds array accesses. (Conversely: --no-bufferoverrun) @@ -1920,6 +1928,9 @@ INTERNAL OPTIONS --buck-targets-block-list-reset Set --buck-targets-block-list to the empty list. + --buck2-bxl-target-reset + Cancel the effect of --buck2-bxl-target. + --buck2-root-reset Cancel the effect of --buck2-root. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index da0f2129c70..340ad0325d0 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -223,10 +223,18 @@ OPTIONS Skip capture of buck targets matched by the specified regular expression. See also infer-capture(1) and infer-run(1). + --buck2-bxl-target string + Buck2 BXL script (as a buck target) to run when capturing with + buck2/clang integration. See also infer-capture(1). + --buck2-root dir Specify the parent directory of buck-out (used only for buck2). See also infer-capture(1) and infer-run(1). + --buck2-use-bxl + Activates: Use BXL script when capturing with buck2. (Conversely: + --no-buck2-use-bxl) See also infer-capture(1). + --bufferoverrun Activates: checker bufferoverrun: InferBO is a detector for out-of-bounds array accesses. (Conversely: --no-bufferoverrun) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index d66cd1d4b7e..bb339ce250e 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -814,6 +814,18 @@ and buck2_build_args_no_inline_rev = args starting with '@'. Only valid for $(b,--buck-clang)." +and buck2_bxl_target = + CLOpt.mk_string_opt ~long:"buck2-bxl-target" + ~in_help:InferCommand.[(Capture, manual_buck)] + "Buck2 BXL script (as a buck target) to run when capturing with buck2/clang integration." + + +and buck2_use_bxl = + CLOpt.mk_bool ~long:"buck2-use-bxl" ~default:false + ~in_help:InferCommand.[(Capture, manual_buck)] + "Use BXL script when capturing with buck2." + + and buck_block_list = CLOpt.mk_string_list ~deprecated:["-blacklist-regex"; "-blacklist"; "-buck-blacklist"] @@ -3444,6 +3456,10 @@ and buck2_build_args = RevList.to_list !buck2_build_args and buck2_build_args_no_inline = RevList.to_list !buck2_build_args_no_inline_rev +and buck2_bxl_target = !buck2_bxl_target + +and buck2_use_bxl = !buck2_use_bxl + and buck_block_list = RevList.to_list !buck_block_list and buck_build_args = RevList.to_list !buck_build_args diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 1fa8858525f..78cefaf5b80 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -185,6 +185,10 @@ val buck2_build_args : string list val buck2_build_args_no_inline : string list +val buck2_bxl_target : string option + +val buck2_use_bxl : bool + val buck_block_list : string list val buck_build_args : string list diff --git a/infer/src/integration/Buck.ml b/infer/src/integration/Buck.ml index efe04731ceb..01a95f345a5 100644 --- a/infer/src/integration/Buck.ml +++ b/infer/src/integration/Buck.ml @@ -450,6 +450,8 @@ let parse_command_and_targets (buck_mode : BuckMode.t) (version : version) origi match (buck_mode, version, parsed_args) with | Clang, V1, {pattern_targets= []; alias_targets= []; normal_targets} -> normal_targets + | Clang, V2, {pattern_targets; alias_targets; normal_targets} -> + pattern_targets |> List.rev_append alias_targets |> List.rev_append normal_targets | _, _, {pattern_targets; alias_targets; normal_targets} -> pattern_targets |> List.rev_append alias_targets |> List.rev_append normal_targets |> resolve_pattern_targets buck_mode version diff --git a/infer/src/integration/BxlClang.ml b/infer/src/integration/BxlClang.ml new file mode 100644 index 00000000000..5929d0f89db --- /dev/null +++ b/infer/src/integration/BxlClang.ml @@ -0,0 +1,57 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * 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 L = Logging +module F = Format + +let rec traverse ~root acc target_path = + let target_path = if Filename.is_absolute target_path then target_path else root ^/ target_path in + match Sys.is_directory target_path with + | `Yes when ISys.file_exists (ResultsDirEntryName.get_path ~results_dir:target_path CaptureDB) -> + (* we found a capture DB so add this as a target line *) + Printf.sprintf "dummy\t-\t%s" target_path :: acc + | `Yes -> + (* recurse into non-infer-out directory *) + Sys.readdir target_path + |> Array.fold ~init:acc ~f:(fun acc entry -> + traverse ~root acc (Filename.concat target_path entry) ) + | _ -> + acc + + +let capture build_cmd = + let bxl_target = + match Config.buck2_bxl_target with + | None -> + L.die UserError "A BXL script must be provided when capturing with buck2/clang.@\n" + | Some target -> + target + in + let prog, buck2_args = (List.hd_exn build_cmd, List.tl_exn build_cmd) in + let _command, rev_not_targets, targets = Buck.parse_command_and_targets Clang V2 buck2_args in + if List.is_empty targets then L.user_warning "No targets found to capture.@\n" + else + let targets_with_arg = + List.fold targets ~init:[] ~f:(fun acc target -> "--target" :: target :: acc) + in + let buck2_build_cmd = + ["bxl"; bxl_target] @ List.rev rev_not_targets @ Config.buck2_build_args_no_inline @ ["--"] + @ Option.value_map Config.buck_dependency_depth ~default:[] ~f:(fun depth -> + ["--depth"; Int.to_string depth] ) + @ Buck.store_args_in_file ~identifier:"clang_buck2_bxl" targets_with_arg + in + L.debug Capture Quiet "Processed buck2 bxl command '%a'@\n" (Pp.seq F.pp_print_string) + buck2_build_cmd ; + ResultsDir.RunState.set_merge_capture true ; + let infer_deps_lines = + Buck.wrap_buck_call ~extend_env:[] V2 ~label:"build" (prog :: buck2_build_cmd) + |> List.fold ~init:[] ~f:(traverse ~root:Config.buck2_root) + |> List.dedup_and_sort ~compare:String.compare + in + let infer_deps = ResultsDir.get_path CaptureDependencies in + Utils.with_file_out infer_deps ~f:(fun out_channel -> + Out_channel.output_lines out_channel infer_deps_lines ) diff --git a/infer/src/integration/BxlClang.mli b/infer/src/integration/BxlClang.mli new file mode 100644 index 00000000000..900ff40e038 --- /dev/null +++ b/infer/src/integration/BxlClang.mli @@ -0,0 +1,11 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +val capture : string list -> unit +(** do a buck2/clang capture given the prog and build command (buck args) *) diff --git a/infer/src/integration/Driver.ml b/infer/src/integration/Driver.ml index 379d11c5e66..ea23b174b0f 100644 --- a/infer/src/integration/Driver.ml +++ b/infer/src/integration/Driver.ml @@ -22,6 +22,7 @@ type mode = | BuckErlang of {prog: string; args: string list} | BuckGenrule of {prog: string} | BuckJavaFlavor of {build_cmd: string list} + | BxlClang of {build_cmd: string list} | Clang of {compiler: Clang.compiler; prog: string; args: string list} | ClangCompilationDB of {db_files: [`Escaped of string | `Raw of string] list} | Gradle of {prog: string; args: string list} @@ -60,6 +61,8 @@ let pp_mode fmt = function F.fprintf fmt "BuckGenRule driver mode:@\nprog = '%s'" prog | BuckJavaFlavor {build_cmd} -> F.fprintf fmt "BuckJavaFlavor driver mode:@\nbuild command = %a" Pp.cli_args build_cmd + | BxlClang {build_cmd} -> + F.fprintf fmt "BxlClang driver mode:@\nbuild command = %a" Pp.cli_args build_cmd | Clang {prog; args} -> F.fprintf fmt "Clang driver mode:@\nprog = '%s'@\nargs = %a" prog Pp.cli_args args | ClangCompilationDB _ -> @@ -167,6 +170,9 @@ let capture ~changed_files mode = | BuckJavaFlavor {build_cmd} -> L.progress "Capturing for BuckJavaFlavor integration...@." ; BuckJavaFlavor.capture build_cmd + | BxlClang {build_cmd} -> + L.progress "Capturing in bxl/clang mode...@." ; + BxlClang.capture build_cmd | Clang {compiler; prog; args} -> if Config.is_originator then L.progress "Capturing in make/cc mode...@." ; Clang.capture compiler ~prog ~args @@ -487,6 +493,8 @@ let mode_of_build_command build_cmd (buck_mode : BuckMode.t option) = error_no_buck_mode_specified () | Some Erlang -> BuckErlang {prog; args} + | Some Clang when Config.buck2_use_bxl -> + BxlClang {build_cmd} | Some Clang -> Buck2Clang {build_cmd} | Some Java -> diff --git a/infer/src/integration/Driver.mli b/infer/src/integration/Driver.mli index 403b82eefef..30824673514 100644 --- a/infer/src/integration/Driver.mli +++ b/infer/src/integration/Driver.mli @@ -21,6 +21,7 @@ type mode = | BuckErlang of {prog: string; args: string list} | BuckGenrule of {prog: string} | BuckJavaFlavor of {build_cmd: string list} + | BxlClang of {build_cmd: string list} | Clang of {compiler: Clang.compiler; prog: string; args: string list} | ClangCompilationDB of {db_files: [`Escaped of string | `Raw of string] list} | Gradle of {prog: string; args: string list} From c34789413a9990506977bdf6b6992d598d17f910 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 22 Feb 2023 06:05:37 -0800 Subject: [PATCH 07/25] Add procdescs for models to models.sql dump Summary: This is in preparation to remove procdescs from summaries in a subsequent diff. Reviewed By: ngorogiannis Differential Revision: D43313290 fbshipit-source-id: f4a31b97a439f52ed29b58373bf883f0d2886610 --- infer/models/Makefile | 8 +++++++- infer/src/biabduction/Paths.ml | 8 +++++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/infer/models/Makefile b/infer/models/Makefile index bd302b1e114..9281de38637 100644 --- a/infer/models/Makefile +++ b/infer/models/Makefile @@ -13,6 +13,8 @@ OBJC_MODELS_DIR = objc/src RESULTS_DIR = infer-out RESULTS_DB = $(RESULTS_DIR)/results.db +CAPTURE_DB = $(RESULTS_DIR)/capture.db + INFER_OPTIONS = --jobs 1 --biabduction-only --results-dir $(RESULTS_DIR) --biabduction-models-mode JAVA_MODELS_OUT = java/models @@ -28,6 +30,10 @@ SQL_DUMP_MODEL_SPECS = \ -cmd ".output $(MODELS_RESULTS_FILE)" \ -cmd "select * from specs order by proc_uid ;" +SQL_DUMP_MODEL_PROCS = \ + -cmd ".mode insert procedures" \ + -cmd "select * from procedures order by proc_uid ;" + .PHONY: all all: $(MODELS_RESULTS_FILE) @@ -66,7 +72,7 @@ $(MODELS_RESULTS_FILE): $(MAKEFILE_LIST) $(MAKE) capture $(QUIET)$(call silent_on_success,Analyzing models,$(INFER_BIN) analyze $(INFER_OPTIONS)) sqlite3 $(RESULTS_DB) $(SQL_DUMP_MODEL_SPECS) > $(MODELS_RESULTS_FILE) ifeq ($(BUILD_C_ANALYZERS),yes) $(MODELS_RESULTS_FILE): $(CLANG_DEPS_NO_MODELS) diff --git a/infer/src/biabduction/Paths.ml b/infer/src/biabduction/Paths.ml index 0c6ee078293..a387bc468b1 100644 --- a/infer/src/biabduction/Paths.ml +++ b/infer/src/biabduction/Paths.ml @@ -466,7 +466,13 @@ end = struct trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace ; Option.iter ~f:(fun loc -> - if Procname.is_java pname && not (SourceFile.is_invalid loc.Location.file) then + if + Procname.is_java pname + && (not (SourceFile.is_invalid loc.Location.file)) + && not + ( Attributes.load pname + |> Option.exists ~f:(fun attrs -> attrs.ProcAttributes.is_biabduction_model) ) + then let definition_descr = Format.asprintf "Definition of %a" (Procname.pp_simplified_string ~withclass:false) From afaf51a48a4f3a6cf01ac58e7ea2210e6e7f6c5f Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 22 Feb 2023 06:05:40 -0800 Subject: [PATCH 08/25] Write structured-SIL test programs to capture DB during unit tests Summary: Move the `already_started` logic for the DBWriter server from `infer.ml` to DBWriter, then start the server and store CFGs during tests. Reviewed By: skcho Differential Revision: D43313291 fbshipit-source-id: d7531bb8107a52d00b0b11d7d3937db028ea9eef --- infer/src/base/DBWriter.ml | 13 +++++++++-- infer/src/base/DBWriter.mli | 9 -------- infer/src/infer.ml | 14 ++---------- infer/src/inferunit.ml | 3 +-- infer/src/unit/analyzerTester.ml | 39 +++++++++++++++++++++----------- 5 files changed, 40 insertions(+), 38 deletions(-) diff --git a/infer/src/base/DBWriter.ml b/infer/src/base/DBWriter.ml index 39cbcfdce3f..a2cf3bae199 100644 --- a/infer/src/base/DBWriter.ml +++ b/infer/src/base/DBWriter.ml @@ -585,10 +585,19 @@ let replace_attributes ~proc_uid ~proc_attributes ~cfg ~callees ~analysis = let shrink_analysis_db () = perform ShrinkAnalysisDB -let start () = Server.start () - let stop () = try Server.send Command.Terminate with Unix.Unix_error _ -> () +let start = + let already_started = ref false in + fun () -> + if (not !already_started) && Config.is_originator then ( + remove_socket_file () ; + if Lazy.force use_daemon then ( + Server.start () ; + Epilogues.register ~f:stop ~description:"Stop Sqlite write daemon" ; + already_started := true ) ) + + let store_issue_log ~checker ~source_file ~issue_log = perform (StoreIssueLog {checker; source_file; issue_log}) diff --git a/infer/src/base/DBWriter.mli b/infer/src/base/DBWriter.mli index cd7e25eb908..9e45cbf4dd9 100644 --- a/infer/src/base/DBWriter.mli +++ b/infer/src/base/DBWriter.mli @@ -8,13 +8,6 @@ open! IStd -val remove_socket_file : unit -> unit -(** deletes (unlinks) the file corresponding to the socket in the results dir if it exists; useful - to clean up stale state at the start of an infer execution *) - -val use_daemon : bool Lazy.t -(** indicates that there should be a daemon running *) - val add_source_file : source_file:Sqlite3.Data.t -> tenv:Sqlite3.Data.t @@ -52,8 +45,6 @@ val shrink_analysis_db : unit -> unit val start : unit -> unit -val stop : unit -> unit - val store_issue_log : checker:string -> source_file:Sqlite3.Data.t -> issue_log:Sqlite3.Data.t -> unit diff --git a/infer/src/infer.ml b/infer/src/infer.ml index 0199639ccb3..6ed86816330 100644 --- a/infer/src/infer.ml +++ b/infer/src/infer.ml @@ -27,16 +27,6 @@ let run driver_mode = let run driver_mode = ScubaLogging.execute_with_time_logging "run" (fun () -> run driver_mode) let setup () = - let db_start = - let already_started = ref false in - fun () -> - if (not !already_started) && Config.is_originator then ( - DBWriter.remove_socket_file () ; - if Lazy.force DBWriter.use_daemon then ( - DBWriter.start () ; - Epilogues.register ~f:DBWriter.stop ~description:"Stop Sqlite write daemon" ; - already_started := true ) ) - in ( match Config.command with | Analyze -> ResultsDir.assert_results_dir "have you run capture before?" @@ -61,7 +51,7 @@ let setup () = Config.is_originator && (not Config.continue_capture) && not (Driver.is_analyze_mode driver_mode) then ( - db_start () ; + DBWriter.start () ; SourceFiles.mark_all_stale () ) | Explore -> ResultsDir.assert_results_dir "please run an infer analysis first" @@ -77,7 +67,7 @@ let setup () = false in if has_result_dir then ( - db_start () ; + DBWriter.start () ; if Config.is_originator then ResultsDir.RunState.add_run_to_sequence () ) ; has_result_dir diff --git a/infer/src/inferunit.ml b/infer/src/inferunit.ml index c9985c6d49c..a01f1052612 100644 --- a/infer/src/inferunit.ml +++ b/infer/src/inferunit.ml @@ -21,7 +21,6 @@ let rec mk_test_fork_proof test = let () = - ResultsDir.create_results_dir () ; let open OUnit2 in let tests = (* OUnit runs tests in parallel using fork(2) *) @@ -50,4 +49,4 @@ let () = @ ClangTests.tests @ AllNullsafeTests.tests ) in let test_suite = "all" >::: tests in - OUnit2.run_test_tt_main test_suite + run_test_tt_main test_suite diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index e7c58154097..252a36c2987 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -10,6 +10,12 @@ module F = Format (** utilities for writing abstract domains/transfer function tests *) +(** set up results dir and database for StructuredSil test programs *) +let () = + ResultsDir.create_results_dir () ; + DBWriter.start () + + (** structured language that makes it easy to write small test programs in OCaml *) module StructuredSil = struct type assertion = string @@ -179,11 +185,19 @@ struct module T = I.TransferFunctions module M = I.InvariantMap - let structured_program_to_cfg program test_pname = + let gen_pname = + let id = ref (-1) in + fun () -> + Int.incr id ; + Procname.from_string_c_fun ("structured_sil_test_" ^ Int.to_string !id) + + + let structured_program_to_cfg program = let cfg = Cfg.create () in - let pdesc = - Cfg.create_proc_desc cfg (ProcAttributes.default (SourceFile.invalid __FILE__) test_pname) - in + let src_file = SourceFile.invalid __FILE__ in + let pname = gen_pname () in + let attrs = ProcAttributes.{(default src_file pname) with is_defined= true} in + let pdesc = Cfg.create_proc_desc cfg attrs in let create_node kind cmds = Procdesc.create_node pdesc dummy_loc kind cmds in let set_succs cur_node succs ~exn_handlers = Procdesc.node_set_succs pdesc cur_node ~normal:succs ~exn:exn_handlers @@ -278,15 +292,14 @@ struct let exit_node = create_node Procdesc.Node.Exit_node [] in set_succs last_node [exit_node] ~exn_handlers:no_exn_handlers ; Procdesc.set_exit_node pdesc exit_node ; - (Summary.OnDisk.reset pdesc, assert_map) + Cfg.store src_file cfg ; + (Summary.OnDisk.reset pdesc, assert_map, pdesc) - let create_test test_program make_analysis_data ~initial pp_opt test_pname _ = + let create_test test_program make_analysis_data ~initial pp_opt _ = let pp_state = Option.value ~default:I.TransferFunctions.Domain.pp pp_opt in - let summary, assert_map = structured_program_to_cfg test_program test_pname in - let inv_map = - I.exec_pdesc (make_analysis_data summary) ~initial (Summary.get_proc_desc summary) - in + let summary, assert_map, pdesc = structured_program_to_cfg test_program in + let inv_map = I.exec_pdesc (make_analysis_data summary) ~initial pdesc in let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc = let post_str = try @@ -328,7 +341,7 @@ struct let ai_list = [("ai_rpo", AI_RPO.create_test); ("ai_wto", AI_WTO.create_test)] - let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt make_analysis_data tests = + let create_tests ~initial ?pp_opt make_analysis_data tests = AnalysisCallbacks.set_callbacks { html_debug_new_node_session_f= NodePrinter.with_session ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc } ; @@ -336,8 +349,8 @@ struct List.concat_map ~f:(fun (name, test_program) -> List.map ai_list ~f:(fun (ai_name, create_test) -> - name ^ "_" ^ ai_name - >:: create_test test_program make_analysis_data ~initial pp_opt test_pname ) ) + name ^ "_" ^ ai_name >:: create_test test_program make_analysis_data ~initial pp_opt ) + ) tests end From 2a434399ec50db493398fbee6c7bbf6c6aabb1a2 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 22 Feb 2023 06:05:43 -0800 Subject: [PATCH 09/25] Remove get_model_proc_desc_f from AnalysisCallbacks Summary: Instead of storing a callback to avoid module dependency cycles, we can just call Procdesc.load now that model procdescs are in the DB. Reviewed By: ngorogiannis Differential Revision: D43313292 fbshipit-source-id: bb98538c7bdbb8f98729a2079bf7ecb6fd7c4946 --- infer/src/absint/AnalysisCallbacks.ml | 6 +----- infer/src/absint/AnalysisCallbacks.mli | 6 +----- infer/src/backend/CallbackOfChecker.ml | 6 +----- infer/src/biabduction/SymExec.ml | 25 +++++++------------------ infer/src/biabduction/Tabulation.ml | 8 +------- infer/src/unit/analyzerTester.ml | 4 +--- 6 files changed, 12 insertions(+), 43 deletions(-) diff --git a/infer/src/absint/AnalysisCallbacks.ml b/infer/src/absint/AnalysisCallbacks.ml index 3d4de72b937..a5d41cbd6b3 100644 --- a/infer/src/absint/AnalysisCallbacks.ml +++ b/infer/src/absint/AnalysisCallbacks.ml @@ -15,8 +15,7 @@ type callbacks = -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) - -> 'a - ; get_model_proc_desc_f: Procname.t -> Procdesc.t option } + -> 'a } let callbacks_ref : callbacks option ref = ref None @@ -32,6 +31,3 @@ let get_callbacks () = let html_debug_new_node_session ?kind ~pp_name node ~f = (get_callbacks ()).html_debug_new_node_session_f ?kind ~pp_name node ~f - - -let get_model_proc_desc proc_name = (get_callbacks ()).get_model_proc_desc_f proc_name diff --git a/infer/src/absint/AnalysisCallbacks.mli b/infer/src/absint/AnalysisCallbacks.mli index a31b69db768..c4119c18353 100644 --- a/infer/src/absint/AnalysisCallbacks.mli +++ b/infer/src/absint/AnalysisCallbacks.mli @@ -9,9 +9,6 @@ open! IStd (** {2 Analysis API} *) -val get_model_proc_desc : Procname.t -> Procdesc.t option -(** get the preanalysed procdesc of a model; raises if procname given is not a biabduction model *) - val html_debug_new_node_session : ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO] -> pp_name:(Format.formatter -> unit) @@ -32,8 +29,7 @@ type callbacks = -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) - -> 'a - ; get_model_proc_desc_f: Procname.t -> Procdesc.t option } + -> 'a } val set_callbacks : callbacks -> unit (** make sure this is called before starting any actual analysis *) diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index 013e487bce9..1230ee1e39f 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -9,11 +9,7 @@ open! IStd (* make sure callbacks are set or the checkers will not be able to call into them (and get a nice crash) *) -let () = - AnalysisCallbacks.set_callbacks - { html_debug_new_node_session_f= NodePrinter.with_session - ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc } - +let () = AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session} let mk_interprocedural_t ~f_analyze_dep ~get_payload exe_env summary ?(tenv = Exe_env.get_proc_tenv exe_env (Summary.get_proc_name summary)) () = diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 584f02ef333..b7e2287e412 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -590,17 +590,6 @@ type resolve_and_analyze_result = ; resolved_procdesc_opt: Procdesc.t option ; resolved_summary_opt: (Procdesc.t * BiabductionSummary.t) option } -let get_proc_desc proc_name = - if BiabductionModels.mem proc_name then AnalysisCallbacks.get_model_proc_desc proc_name - else Procdesc.load proc_name - - -let get_attributes proc_name = - if BiabductionModels.mem proc_name then - AnalysisCallbacks.get_model_proc_desc proc_name |> Option.map ~f:Procdesc.get_attributes - else Attributes.load proc_name - - (** Resolve the procedure name and run the analysis of the resolved procedure if not already analyzed *) let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv} @@ -612,15 +601,15 @@ let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc; whether the method is defined or generated by the specialization *) let analyze_ondemand resolved_pname = if Procname.equal resolved_pname callee_proc_name then - (get_proc_desc callee_proc_name, analyze_dependency callee_proc_name) + (Procdesc.load callee_proc_name, analyze_dependency callee_proc_name) else (* Create the type specialized procedure description and analyze it directly *) let resolved_proc_desc_option = - match get_proc_desc resolved_pname with + match Procdesc.load resolved_pname with | Some _ as resolved_proc_desc -> resolved_proc_desc | None -> - let procdesc_opt = get_proc_desc callee_proc_name in + let procdesc_opt = Procdesc.load callee_proc_name in Option.map procdesc_opt ~f:(fun callee_proc_desc -> (* It is possible that the types of the arguments are not as precise as the type of the objects in the heap, so we should update them to get the best results. *) @@ -996,7 +985,7 @@ let execute_store ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv; let is_variadic_procname callee_pname = - Option.exists (get_attributes callee_pname) ~f:(fun proc_attrs -> + Option.exists (Attributes.load callee_pname) ~f:(fun proc_attrs -> proc_attrs.ProcAttributes.is_variadic ) @@ -1010,7 +999,7 @@ let resolve_and_analyze_no_dynamic_dispatch {InterproceduralAnalysis.analyze_dep callee_pname in let resolved_summary_opt = analyze_dependency resolved_pname in - {resolved_pname; resolved_procdesc_opt= get_proc_desc resolved_pname; resolved_summary_opt} + {resolved_pname; resolved_procdesc_opt= Procdesc.load resolved_pname; resolved_summary_opt} let resolve_and_analyze_clang analysis_data prop_r n_actual_params callee_pname call_flags = @@ -1539,7 +1528,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots callee_pname ret_annots loc path_pos in let callee_loc_opt = - Option.map ~f:(fun attributes -> attributes.ProcAttributes.loc) (get_attributes callee_pname) + Option.map ~f:(fun attributes -> attributes.ProcAttributes.loc) (Attributes.load callee_pname) in let skip_path = Paths.Path.add_skipped_call path callee_pname reason callee_loc_opt in [(prop_with_undef_attr, skip_path)] @@ -1581,7 +1570,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as builtin_args) = - match get_attributes proc_name with + match Attributes.load proc_name with | Some callee_attributes -> ( match callee_attributes.ProcAttributes.sentinel_attr with | Some sentinel -> diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 19fa1698a3f..fa3b2246346 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -745,15 +745,9 @@ let prop_set_exn tenv pname prop se_exn = Prop.normalize tenv (Prop.set prop ~sigma:sigma') -let get_attributes proc_name = - if BiabductionModels.mem proc_name then - AnalysisCallbacks.get_model_proc_desc proc_name |> Option.map ~f:Procdesc.get_attributes - else Attributes.load proc_name - - (** Include a subtrace for a procedure call if the callee is not a model. *) let include_subtrace callee_pname = - match get_attributes callee_pname with + match Attributes.load callee_pname with | Some attrs -> (not attrs.ProcAttributes.is_biabduction_model) && SourceFile.is_under_project_root attrs.ProcAttributes.loc.Location.file diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 252a36c2987..5e83f3f1b5a 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -342,9 +342,7 @@ struct let ai_list = [("ai_rpo", AI_RPO.create_test); ("ai_wto", AI_WTO.create_test)] let create_tests ~initial ?pp_opt make_analysis_data tests = - AnalysisCallbacks.set_callbacks - { html_debug_new_node_session_f= NodePrinter.with_session - ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc } ; + AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session} ; let open OUnit2 in List.concat_map ~f:(fun (name, test_program) -> From 684e43b68d2cd70ed5f3752af93c3c4b452f55c1 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 22 Feb 2023 06:05:45 -0800 Subject: [PATCH 10/25] [frontend][objc] Construct correct procnames for pre-defined methods Summary: This diff constructs correct procnames for the pre-defined methods, i.e. `stringWithUTF8String` and `isKindOfClass`, which should have one parameter. Reviewed By: skcho Differential Revision: D43390612 fbshipit-source-id: ae44ebbe2a5d6d03351e3d99d5ea37434608b450 --- infer/src/IR/Procname.mli | 1 + infer/src/clang/CType_decl.ml | 10 +++++----- infer/src/clang/CType_decl.mli | 7 ++++++- infer/src/clang/cTrans.ml | 3 ++- infer/src/clang/cTrans_models.ml | 10 +++++----- infer/src/clang/cTrans_models.mli | 6 +++++- infer/src/clang/cTrans_utils.ml | 2 +- infer/tests/build_systems/objc_missing_fld/issues.exp | 2 +- 8 files changed, 26 insertions(+), 15 deletions(-) diff --git a/infer/src/IR/Procname.mli b/infer/src/IR/Procname.mli index e98047fa665..adfd4686ae9 100644 --- a/infer/src/IR/Procname.mli +++ b/infer/src/IR/Procname.mli @@ -156,6 +156,7 @@ module ObjC_Cpp : sig ; kind: kind ; method_name: string ; parameters: Parameter.clang_parameter list + (** NOTE: [parameters] should NOT include additional [this/self] or [__return_param]. *) ; template_args: Typ.template_spec_info } [@@deriving compare] diff --git a/infer/src/clang/CType_decl.ml b/infer/src/clang/CType_decl.ml index 6b465722092..f0edf3abff0 100644 --- a/infer/src/clang/CType_decl.ml +++ b/infer/src/clang/CType_decl.ml @@ -660,11 +660,11 @@ and get_class_typename ?tenv method_decl_info = "Expecting class declaration when getting the class typename" -and objc_method_procname ?tenv decl_info method_name mdi = +and objc_method_procname ?tenv decl_info method_name parameters mdi = let class_typename = get_class_typename ?tenv decl_info in let is_instance = mdi.Clang_ast_t.omdi_is_instance_method in let method_kind = Procname.ObjC_Cpp.objc_method_kind_of_bool is_instance in - mk_objc_method class_typename method_name method_kind + mk_objc_method class_typename method_name method_kind parameters and objc_block_procname outer_proc_opt parameters = @@ -721,7 +721,7 @@ and procname_from_decl ?tenv ?block_return_type ?outer_proc meth_decl = | CXXDestructorDecl (decl_info, name_info, _, fdi, mdi) -> mk_cpp_method decl_info name_info fdi mdi | ObjCMethodDecl (decl_info, name_info, mdi) -> - objc_method_procname ?tenv decl_info name_info.Clang_ast_t.ni_name mdi parameters + objc_method_procname ?tenv decl_info name_info.Clang_ast_t.ni_name parameters mdi | BlockDecl _ -> objc_block_procname outer_proc parameters | _ -> @@ -821,8 +821,8 @@ module CProcname = struct mk_cpp_method ~tenv class_name method_name None [] - let objc_method_of_string_kind class_name method_name method_kind = - mk_objc_method class_name method_name method_kind [] + let objc_method_of_string_kind class_name method_name method_kind parameters = + mk_objc_method class_name method_name method_kind parameters end end diff --git a/infer/src/clang/CType_decl.mli b/infer/src/clang/CType_decl.mli index a2071d10e8e..e9a240b7772 100644 --- a/infer/src/clang/CType_decl.mli +++ b/infer/src/clang/CType_decl.mli @@ -23,7 +23,12 @@ module CProcname : sig val cpp_method_of_string : Tenv.t -> Typ.Name.t -> string -> Procname.t - val objc_method_of_string_kind : Typ.Name.t -> string -> Procname.ObjC_Cpp.kind -> Procname.t + val objc_method_of_string_kind : + Typ.Name.t + -> string + -> Procname.ObjC_Cpp.kind + -> Procname.Parameter.clang_parameter list + -> Procname.t end end diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index ef1f3855019..f5cbccf098c 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -36,8 +36,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s CMethod_trans.get_class_name_method_call_from_receiver_kind context obj_c_message_expr_info act_params in + let parameters = List.map act_params ~f:(fun (_, typ) -> Procname.Parameter.of_typ typ) in CType_decl.CProcname.NoAstDecl.objc_method_of_string_kind class_name selector - objc_method_kind + objc_method_kind parameters in let predefined_ms_opt = match proc_name with diff --git a/infer/src/clang/cTrans_models.ml b/infer/src/clang/cTrans_models.ml index e9882930366..954dbfd3893 100644 --- a/infer/src/clang/cTrans_models.ml +++ b/infer/src/clang/cTrans_models.ml @@ -63,15 +63,15 @@ let is_assert_log pname = false -let get_predefined_ms_method condition class_name method_name method_kind mk_procname arguments - return_type attributes builtin = +let get_predefined_ms_method condition class_name method_name method_kind clang_params mk_procname + arguments return_type attributes builtin = if condition then let procname = match builtin with | Some procname -> procname | None -> - mk_procname class_name method_name method_kind + mk_procname class_name method_name method_kind clang_params in let ms = CMethodSignature.mk procname None arguments return_type ~is_ret_constexpr:false attributes @@ -94,7 +94,7 @@ let get_predefined_ms_stringWithUTF8String class_name method_name mk_procname = in let param_name = Mangled.from_string "x" in let params = [CMethodSignature.mk_param_type param_name char_star_type] in - get_predefined_ms_method condition class_name method_name Procname.ObjC_Cpp.ObjCClassMethod + get_predefined_ms_method condition class_name method_name Procname.ObjC_Cpp.ObjCClassMethod [None] mk_procname params (id_type, Annot.Item.empty) [] None @@ -105,7 +105,7 @@ let get_predefined_ms_is_kind_of_class class_name method_name mk_procname = let params = [CMethodSignature.mk_param_type name class_type] in let bool_type = CType_to_sil_type.type_of_builtin_type_kind `Bool in get_predefined_ms_method condition class_name method_name Procname.ObjC_Cpp.ObjCInstanceMethod - mk_procname params (bool_type, Annot.Item.empty) [] (Some BuiltinDecl.__instanceof) + [None] mk_procname params (bool_type, Annot.Item.empty) [] (Some BuiltinDecl.__instanceof) let get_predefined_model_method_signature class_name method_name mk_procname = diff --git a/infer/src/clang/cTrans_models.mli b/infer/src/clang/cTrans_models.mli index 1a5bf67971e..d659c6df94f 100644 --- a/infer/src/clang/cTrans_models.mli +++ b/infer/src/clang/cTrans_models.mli @@ -28,5 +28,9 @@ val is_modeled_attribute : string -> bool val get_predefined_model_method_signature : Typ.Name.t -> string - -> (Typ.Name.t -> string -> Procname.ObjC_Cpp.kind -> Procname.t) + -> ( Typ.Name.t + -> string + -> Procname.ObjC_Cpp.kind + -> Procname.Parameter.clang_parameter list + -> Procname.t ) -> CMethodSignature.t option diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index b13d98280d0..fb0619619c6 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -461,7 +461,7 @@ let objc_new_trans trans_state ~alloc_builtin loc stmt_info cls_name function_ty let method_kind = ClangMethodKind.OBJC_INSTANCE in let pname = CType_decl.CProcname.NoAstDecl.objc_method_of_string_kind cls_name CFrontend_config.init - Procname.ObjC_Cpp.ObjCInstanceMethod + Procname.ObjC_Cpp.ObjCInstanceMethod [] in CMethod_trans.create_external_procdesc trans_state.context.CContext.translation_unit_context trans_state.context.CContext.cfg pname method_kind None ; diff --git a/infer/tests/build_systems/objc_missing_fld/issues.exp b/infer/tests/build_systems/objc_missing_fld/issues.exp index ad6e0e7efc0..13df168f2d8 100644 --- a/infer/tests/build_systems/objc_missing_fld/issues.exp +++ b/infer/tests/build_systems/objc_missing_fld/issues.exp @@ -1,2 +1,2 @@ build_systems/codetoanalyze/objc_missing_fld/A.m, badOnlyOneNDA, 5, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure badOnlyOneNDA(),macro expanded here,start of procedure predA(),start of procedure implOnlyFn:,return from a call to A.implOnlyFn:,start of procedure delegate,return from a call to A.delegate,Condition is true,return from a call to predA,Taking false branch] -build_systems/codetoanalyze/objc_missing_fld/B.m, badOnlyOneNDB, 5, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure badOnlyOneNDB(),macro expanded here,start of procedure predB(),start of procedure implOnlyFn:,return from a call to A.implOnlyFn:,start of procedure delegate,return from a call to A.delegate,Condition is true,return from a call to predB,Taking false branch] +build_systems/codetoanalyze/objc_missing_fld/B.m, badOnlyOneNDB, 5, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure badOnlyOneNDB(),macro expanded here,start of procedure predB(),Skipping implOnlyFn:: method has no implementation,start of procedure delegate,return from a call to A.delegate,Condition is true,return from a call to predB,Taking false branch] From 3209490d1497f038763f643001defd31a325a7b6 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 22 Feb 2023 06:05:48 -0800 Subject: [PATCH 11/25] Stop passing procdescs with payloads in interprocedural analysis Summary: This diff changes the return type of the `analyze_dependency` callback in `InterproceduralAnalysis.t` from `(Procdesc.t * 'payload) option` to just `'payload option`. The procdesc was previously just passed for convenience, but can be removed now (as we are removing procdescs from summaries). This also involves changes to all of the uses of that callback throughout checkers and analyzers. Reviewed By: skcho Differential Revision: D43313294 fbshipit-source-id: d24ccfefd3f4219e7fd8f047a55d4520139cc10a --- infer/src/IR/Attributes.ml | 2 + infer/src/IR/Attributes.mli | 3 ++ infer/src/absint/FormalMap.ml | 5 +- infer/src/absint/FormalMap.mli | 2 +- infer/src/absint/InterproceduralAnalysis.ml | 7 +-- infer/src/absint/InterproceduralAnalysis.mli | 2 +- infer/src/backend/CallbackOfChecker.ml | 39 ++++++-------- infer/src/backend/CallbackOfChecker.mli | 5 +- infer/src/backend/StarvationGlobalAnalysis.ml | 3 +- infer/src/backend/registerCheckers.ml | 6 +-- infer/src/biabduction/BuiltinDefn.ml | 4 +- infer/src/biabduction/SymExec.ml | 53 ++++++++----------- infer/src/biabduction/SymExec.mli | 2 +- .../bufferoverrun/bufferOverrunAnalysis.ml | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 14 +---- infer/src/checkers/DisjunctiveDemo.ml | 2 +- infer/src/checkers/PurityAnalysis.ml | 4 +- infer/src/checkers/RequiredProps.ml | 7 +-- infer/src/checkers/SimpleLineage.ml | 7 ++- infer/src/checkers/SimpleShape.ml | 11 ++-- infer/src/checkers/Siof.ml | 8 +-- infer/src/checkers/annotationReachability.ml | 4 +- infer/src/checkers/scopeLeakage.ml | 8 +-- infer/src/checkers/uninit.ml | 6 +-- infer/src/concurrency/ConcurrencyUtils.ml | 4 +- infer/src/concurrency/RacerDDomain.ml | 4 +- infer/src/concurrency/RacerDDomain.mli | 2 +- infer/src/concurrency/RacerDProcAnalysis.ml | 13 ++--- infer/src/concurrency/starvation.ml | 4 +- infer/src/cost/ConfigImpactAnalysis.ml | 4 +- infer/src/cost/cost.ml | 10 ++-- infer/src/cost/costInstantiate.ml | 9 ++-- infer/src/cost/hoisting.ml | 4 +- .../labs/04_interprocedural/ResourceLeaks.ml | 2 +- .../ResourceLeaks.ml | 4 +- infer/src/labs/README.md | 2 +- infer/src/pulse/PulseCallOperations.ml | 8 +-- infer/src/pulse/PulseCallOperations.mli | 2 +- infer/src/pulse/PulseClosureSpecialization.ml | 7 ++- infer/src/quandary/TaintAnalysis.ml | 6 +-- infer/src/unit/TaintTests.ml | 5 +- 41 files changed, 129 insertions(+), 167 deletions(-) diff --git a/infer/src/IR/Attributes.ml b/infer/src/IR/Attributes.ml index 33524a94824..cd4d310c6ac 100644 --- a/infer/src/IR/Attributes.ml +++ b/infer/src/IR/Attributes.ml @@ -68,6 +68,8 @@ let load_from_uid, load, clear_cache, store = (load_from_uid, load, clear_cache, store) +let load_exn pname = Option.value_exn (load pname) + let load_formal_types pname = match load pname with Some {formals} -> List.map formals ~f:snd3 | None -> [] diff --git a/infer/src/IR/Attributes.mli b/infer/src/IR/Attributes.mli index 9d2cf9b7873..c9c19431692 100644 --- a/infer/src/IR/Attributes.mli +++ b/infer/src/IR/Attributes.mli @@ -18,6 +18,9 @@ val load_from_uid : string -> ProcAttributes.t option val load : Procname.t -> ProcAttributes.t option (** Load the attributes for the procedure from the attributes database. *) +val load_exn : Procname.t -> ProcAttributes.t +(** like [load], but raises an exception if no attributes are found. *) + val is_no_return : Procname.t -> bool val load_formal_types : Procname.t -> Typ.t list diff --git a/infer/src/absint/FormalMap.ml b/infer/src/absint/FormalMap.ml index d87f7fa6e99..b18e0511e18 100644 --- a/infer/src/absint/FormalMap.ml +++ b/infer/src/absint/FormalMap.ml @@ -10,9 +10,8 @@ module F = Format type t = int AccessPath.BaseMap.t -let make pdesc = - let pname = Procdesc.get_proc_name pdesc in - let attrs = Procdesc.get_attributes pdesc in +let make attrs = + let pname = attrs.ProcAttributes.proc_name in let formals_with_nums = List.mapi ~f:(fun index (name, typ, _) -> diff --git a/infer/src/absint/FormalMap.mli b/infer/src/absint/FormalMap.mli index 15b2c8fc024..5b7357f4988 100644 --- a/infer/src/absint/FormalMap.mli +++ b/infer/src/absint/FormalMap.mli @@ -11,7 +11,7 @@ module F = Format (** a map from a formal to its positional index *) type t -val make : Procdesc.t -> t +val make : ProcAttributes.t -> t (** create a formal map for the given procdesc *) val empty : t diff --git a/infer/src/absint/InterproceduralAnalysis.ml b/infer/src/absint/InterproceduralAnalysis.ml index 9b2855cac4f..71ec00b7bd9 100644 --- a/infer/src/absint/InterproceduralAnalysis.ml +++ b/infer/src/absint/InterproceduralAnalysis.ml @@ -12,7 +12,7 @@ type 'payload t = ; tenv: Tenv.t ; err_log: Errlog.t ; exe_env: Exe_env.t - ; analyze_dependency: Procname.t -> (Procdesc.t * 'payload) option + ; analyze_dependency: Procname.t -> 'payload option ; update_stats: ?add_symops:int -> ?failure_kind:Exception.failure_kind -> unit -> unit } type 'payload file_t = @@ -24,7 +24,4 @@ type 'payload file_t = let bind_payload ~f analysis_data = { analysis_data with analyze_dependency= - (fun proc_name -> - analysis_data.analyze_dependency proc_name - |> Option.bind ~f:(fun (proc_desc, payloads) -> - Option.map (f payloads) ~f:(fun payloads' -> (proc_desc, payloads')) ) ) } + (fun proc_name -> Option.bind ~f (analysis_data.analyze_dependency proc_name)) } diff --git a/infer/src/absint/InterproceduralAnalysis.mli b/infer/src/absint/InterproceduralAnalysis.mli index 98bce8ebfd9..f3ff9b42c12 100644 --- a/infer/src/absint/InterproceduralAnalysis.mli +++ b/infer/src/absint/InterproceduralAnalysis.mli @@ -17,7 +17,7 @@ type 'payload t = ; err_log: Errlog.t (** the issue log for the current procedure (internally a mutable data structure) *) ; exe_env: Exe_env.t (** {!Exe_env.t} for the current analysis *) - ; analyze_dependency: Procname.t -> (Procdesc.t * 'payload) option + ; analyze_dependency: Procname.t -> 'payload option (** On-demand analysis of callees or other dependencies of the analysis of the current procedure. Uses [Ondemand.analyze_procedure]. *) ; update_stats: ?add_symops:int -> ?failure_kind:Exception.failure_kind -> unit -> unit diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index 1230ee1e39f..5d002ba6073 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -11,44 +11,35 @@ open! IStd crash) *) let () = AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session} -let mk_interprocedural_t ~f_analyze_dep ~get_payload exe_env summary - ?(tenv = Exe_env.get_proc_tenv exe_env (Summary.get_proc_name summary)) () = +let mk_interprocedural_t ~f_analyze_dep ~get_payload + {Callbacks.exe_env; summary= {Summary.stats; proc_desc; err_log} as caller_summary} + ?(tenv = Exe_env.get_proc_tenv exe_env (Procdesc.get_proc_name proc_desc)) () = let analyze_dependency proc_name = - let summary = Ondemand.analyze_proc_name exe_env ~caller_summary:summary proc_name in - Option.bind summary ~f:(fun {Summary.payloads; proc_desc; _} -> - f_analyze_dep proc_desc (get_payload payloads) ) + let open IOption.Let_syntax in + let* {Summary.payloads} = Ondemand.analyze_proc_name exe_env ~caller_summary proc_name in + f_analyze_dep (get_payload payloads) in - let stats = ref summary.Summary.stats in + let stats = ref stats in let update_stats ?add_symops ?failure_kind () = stats := Summary.Stats.update ?add_symops ?failure_kind !stats in - ( { InterproceduralAnalysis.proc_desc= Summary.get_proc_desc summary - ; tenv - ; err_log= Summary.get_err_log summary - ; exe_env - ; analyze_dependency - ; update_stats } + ( {InterproceduralAnalysis.proc_desc; tenv; err_log; exe_env; analyze_dependency; update_stats} , stats ) -let mk_interprocedural_field_t payload_field exe_env summary = - mk_interprocedural_t - ~f_analyze_dep:(fun pdesc payload_opt -> - Option.map payload_opt ~f:(fun payload -> (pdesc, payload)) ) - ~get_payload:(fun payloads -> Field.get payload_field payloads |> Lazy.force) - exe_env summary +let mk_interprocedural_field_t payload_field = + mk_interprocedural_t ~f_analyze_dep:Fn.id ~get_payload:(fun payloads -> + Field.get payload_field payloads |> Lazy.force ) -let interprocedural ~f_analyze_dep ~get_payload ~set_payload checker {Callbacks.summary; exe_env} = - let analysis_data, stats_ref = - mk_interprocedural_t ~f_analyze_dep ~get_payload exe_env summary () - in +let interprocedural ~f_analyze_dep ~get_payload ~set_payload checker ({Callbacks.summary} as args) = + let analysis_data, stats_ref = mk_interprocedural_t ~f_analyze_dep ~get_payload args () in let result = checker analysis_data |> Lazy.from_val in {summary with payloads= set_payload summary.payloads result; stats= !stats_ref} -let interprocedural_with_field payload_field checker {Callbacks.summary; exe_env} = - let analysis_data, stats_ref = mk_interprocedural_field_t payload_field exe_env summary () in +let interprocedural_with_field payload_field checker ({Callbacks.summary} as args) = + let analysis_data, stats_ref = mk_interprocedural_field_t payload_field args () in let result = checker analysis_data |> Lazy.from_val in {summary with payloads= Field.fset payload_field summary.payloads result; stats= !stats_ref} diff --git a/infer/src/backend/CallbackOfChecker.mli b/infer/src/backend/CallbackOfChecker.mli index a0e9a4c3bbb..9bbf4a8ad62 100644 --- a/infer/src/backend/CallbackOfChecker.mli +++ b/infer/src/backend/CallbackOfChecker.mli @@ -12,14 +12,13 @@ open! IStd val mk_interprocedural_field_t : (Payloads.t, 'payload option Lazy.t) Field.t - -> Exe_env.t - -> Summary.t + -> Callbacks.proc_callback_args -> ?tenv:Tenv.t -> unit -> 'payload InterproceduralAnalysis.t * Summary.Stats.t ref val interprocedural : - f_analyze_dep:(Procdesc.t -> 'payloads_orig -> (Procdesc.t * 'payloads) option) + f_analyze_dep:('payloads_orig -> 'payloads option) -> get_payload:(Payloads.t -> 'payloads_orig) -> set_payload:(Payloads.t -> 'payload_checker Lazy.t -> Payloads.t) -> ('payloads InterproceduralAnalysis.t -> 'payload_checker) diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index ae1272ac740..9cafc5be261 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -66,8 +66,7 @@ let report exe_env work_set = let wrap_report (procname, (pair : CriticalPair.t)) init = Summary.OnDisk.get ~lazy_payloads:true procname |> Option.fold ~init ~f:(fun acc summary -> - let pdesc = Summary.get_proc_desc summary in - let pattrs = Procdesc.get_attributes pdesc in + let pattrs = Attributes.load_exn procname in let tenv = Exe_env.get_proc_tenv exe_env procname in let acc = Starvation.report_on_pair diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index bc5d00dc41e..eb796771f8f 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -33,8 +33,7 @@ let interprocedural_with_field_dependency ~dep_field payload_field checker = [payload_field1] *) let interprocedural2 payload_field1 payload_field2 checker = Procedure - (CallbackOfChecker.interprocedural - ~f_analyze_dep:(fun proc_desc payloads -> Some (proc_desc, payloads)) + (CallbackOfChecker.interprocedural ~f_analyze_dep:Option.some ~get_payload:(fun payloads -> ( Field.get payload_field1 payloads |> Lazy.force , Field.get payload_field2 payloads |> Lazy.force ) ) @@ -45,8 +44,7 @@ let interprocedural2 payload_field1 payload_field2 checker = (** For checkers that read three separate payloads. *) let interprocedural3 payload_field1 payload_field2 payload_field3 ~set_payload checker = Procedure - (CallbackOfChecker.interprocedural - ~f_analyze_dep:(fun proc_desc payloads -> Some (proc_desc, payloads)) + (CallbackOfChecker.interprocedural ~f_analyze_dep:Option.some ~get_payload:(fun payloads -> ( Field.get payload_field1 payloads |> Lazy.force , Field.get payload_field2 payloads |> Lazy.force diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index d3c75684527..fea98d2822b 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -646,8 +646,8 @@ let execute_pthread_create (* no precondition to check, skip *) [(prop_, path)] | Some callee_summary -> - SymExec.proc_call callee_summary {builtin_args with args= [(routine_arg, snd arg)]} ) - ) + SymExec.proc_call pname callee_summary + {builtin_args with args= [(routine_arg, snd arg)]} ) ) | _ -> raise (Exceptions.Wrong_argument_number __POS__) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index b7e2287e412..e6024c11c95 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -360,8 +360,8 @@ let reason_to_skip ~callee_desc : string option = else None in match callee_desc with - | `Summary (callee_pdesc, callee_summary) -> - let attr_reason = Procdesc.get_attributes callee_pdesc |> reason_from_attributes in + | `Summary (callee_pname, callee_summary) -> + let attr_reason = Attributes.load_exn callee_pname |> reason_from_attributes in if Option.is_some attr_reason then attr_reason else if List.is_empty (BiabductionSummary.get_specs callee_summary) then Some "empty list of specs" @@ -588,7 +588,7 @@ let resolve_args prop args = type resolve_and_analyze_result = { resolved_pname: Procname.t ; resolved_procdesc_opt: Procdesc.t option - ; resolved_summary_opt: (Procdesc.t * BiabductionSummary.t) option } + ; resolved_summary_opt: BiabductionSummary.t option } (** Resolve the procedure name and run the analysis of the resolved procedure if not already analyzed *) @@ -1019,7 +1019,7 @@ let resolve_and_analyze_clang analysis_data prop_r n_actual_params callee_pname In that case, default to the non-specialized spec for the model. *) let clang_model_specialized_failure = match resolve_and_analyze_result.resolved_summary_opt with - | Some (_, summary) when has_clang_model -> + | Some summary when has_clang_model -> List.is_empty (BiabductionSummary.get_specs summary) | None -> true @@ -1174,15 +1174,14 @@ let rec sym_exec let ret_typ = Procname.Java.get_return_typ callee_pname_java in let ret_annots = load_ret_annots callee_pname in exec_skip_call ~reason:"unknown method" resolved_pname ret_annots ret_typ - | Some ((callee_proc_desc, _) as resolved_summary) -> ( - match reason_to_skip ~callee_desc:(`Summary resolved_summary) with + | Some resolved_summary -> ( + match reason_to_skip ~callee_desc:(`Summary (resolved_pname, resolved_summary)) with | None -> - proc_call resolved_summary (call_args prop_ callee_pname norm_args ret_id_typ loc) + proc_call resolved_pname resolved_summary + (call_args prop_ callee_pname norm_args ret_id_typ loc) | Some reason -> - let proc_attrs = Procdesc.get_attributes callee_proc_desc in - let ret_annots = proc_attrs.ProcAttributes.ret_annots in - exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type - ) ) + let {ProcAttributes.ret_annots; ret_type} = Attributes.load_exn callee_pname in + exec_skip_call ~reason resolved_pname ret_annots ret_type ) ) | CSharp callee_pname_csharp -> let norm_prop, norm_args = normalize_params analysis_data prop_ actual_params in let url_handled_args = call_constructor_url_update_args callee_pname norm_args in @@ -1199,15 +1198,14 @@ let rec sym_exec let ret_typ = Procname.CSharp.get_return_typ callee_pname_csharp in let ret_annots = load_ret_annots callee_pname in exec_skip_call ~reason:"unknown method" ret_annots ret_typ - | Some ((callee_proc_desc, _) as callee_summary) -> ( - match reason_to_skip ~callee_desc:(`Summary callee_summary) with + | Some callee_summary -> ( + match reason_to_skip ~callee_desc:(`Summary (callee_pname, callee_summary)) with | None -> let handled_args = call_args norm_prop pname url_handled_args ret_id_typ loc in - proc_call callee_summary handled_args + proc_call callee_pname callee_summary handled_args | Some reason -> - let proc_attrs = Procdesc.get_attributes callee_proc_desc in - let ret_annots = proc_attrs.ProcAttributes.ret_annots in - exec_skip_call ~reason ret_annots proc_attrs.ProcAttributes.ret_type ) + let {ProcAttributes.ret_annots; ret_type} = Attributes.load_exn callee_pname in + exec_skip_call ~reason ret_annots ret_type ) in List.fold ~f:(fun acc pname -> exec_one_pname pname @ acc) ~init:[] resolved_pnames | _ -> @@ -1231,7 +1229,7 @@ let rec sym_exec let callee_desc = match (resolved_summary_opt, resolved_pdesc_opt) with | Some summary, _ -> - `Summary summary + `Summary (resolved_pname, summary) | None, Some pdesc -> `ProcDesc pdesc | None, None -> @@ -1239,13 +1237,7 @@ let rec sym_exec in match reason_to_skip ~callee_desc with | Some reason -> ( - let ret_annots = - match resolved_summary_opt with - | Some (proc_desc, _) -> - (Procdesc.get_attributes proc_desc).ProcAttributes.ret_annots - | None -> - load_ret_annots resolved_pname - in + let ret_annots = load_ret_annots resolved_pname in match resolved_pdesc_opt with | Some resolved_pdesc -> let attrs = Procdesc.get_attributes resolved_pdesc in @@ -1260,7 +1252,7 @@ let rec sym_exec skip_call ~reason prop path resolved_pname ret_annots loc ret_id_typ (snd ret_id_typ) n_actual_params ) | None -> - proc_call + proc_call resolved_pname (Option.value_exn resolved_summary_opt) (call_args prop resolved_pname n_actual_params ret_id_typ loc) in @@ -1527,9 +1519,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots Attribute.mark_vars_as_undefined tenv pre_final ~ret_exp ~undefined_actuals_by_ref callee_pname ret_annots loc path_pos in - let callee_loc_opt = - Option.map ~f:(fun attributes -> attributes.ProcAttributes.loc) (Attributes.load callee_pname) - in + let callee_loc_opt = Attributes.load callee_pname |> Option.map ~f:ProcAttributes.get_loc in let skip_path = Paths.Path.add_skipped_call path callee_pname reason callee_loc_opt in [(prop_with_undef_attr, skip_path)] @@ -1583,15 +1573,14 @@ and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as buil (** Perform symbolic execution for a function call *) -and proc_call (callee_pdesc, callee_summary) +and proc_call callee_pname callee_summary { Builtin.analysis_data= {tenv; proc_desc= caller_pdesc; _} as analysis_data ; prop_= pre ; path ; ret_id_typ ; args= actual_pars ; loc } = - let callee_pname = Procdesc.get_proc_name callee_pdesc in - let callee_attributes = Procdesc.get_attributes callee_pdesc in + let callee_attributes = Attributes.load_exn callee_pname in check_inherently_dangerous_function analysis_data callee_pname ; let formal_types = List.map ~f:snd3 callee_attributes.ProcAttributes.formals in let rec comb actual_pars formal_types = diff --git a/infer/src/biabduction/SymExec.mli b/infer/src/biabduction/SymExec.mli index 58b5150a2af..d4395a7c28a 100644 --- a/infer/src/biabduction/SymExec.mli +++ b/infer/src/biabduction/SymExec.mli @@ -34,7 +34,7 @@ val instrs : val diverge : Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list (** Symbolic execution of the divergent pure computation. *) -val proc_call : Procdesc.t * BiabductionSummary.t -> Builtin.t +val proc_call : Procname.t -> BiabductionSummary.t -> Builtin.t val unknown_or_scan_call : is_scan:bool -> reason:string -> Typ.t -> Annot.Item.t -> Builtin.t diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 9b1dc45dede..00e35cb1a93 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -516,7 +516,7 @@ let compute_invariant_map : let analysis_data = let proc_name = Procdesc.get_proc_name proc_desc in let open IOption.Let_syntax in - let get_summary proc_name = analyze_dependency proc_name >>| snd in + let get_summary = analyze_dependency in let get_formals callee_pname = Attributes.load callee_pname >>| ProcAttributes.get_pvar_formals in diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 3b5c76e8ab1..fa9db60d881 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -457,18 +457,8 @@ let checker ({InterproceduralAnalysis.proc_desc; tenv; exe_env; analyze_dependen let cfg = CFG.from_pdesc proc_desc in let checks = let open IOption.Let_syntax in - let get_summary_common callee_pname = - let+ _, summaries = analyze_dependency callee_pname in - summaries - in - let get_checks_summary callee_pname = - let* checker_summary, _analysis_summary = get_summary_common callee_pname in - checker_summary - in - let get_summary callee_pname = - let* _checker_summary, analysis_summary = get_summary_common callee_pname in - analysis_summary - in + let get_checks_summary callee_pname = analyze_dependency callee_pname >>= fst in + let get_summary callee_pname = analyze_dependency callee_pname >>= snd in let get_formals callee_pname = Attributes.load callee_pname >>| ProcAttributes.get_pvar_formals in diff --git a/infer/src/checkers/DisjunctiveDemo.ml b/infer/src/checkers/DisjunctiveDemo.ml index 7f548e67f31..44c9148f5d5 100644 --- a/infer/src/checkers/DisjunctiveDemo.ml +++ b/infer/src/checkers/DisjunctiveDemo.ml @@ -54,7 +54,7 @@ module TransferFunctions = struct match analysis_data.InterproceduralAnalysis.analyze_dependency proc_name with | None -> [astate] - | Some (_, (callee_summary, _)) -> + | Some (callee_summary, _) -> incr node_id ; List.map callee_summary ~f:(fun xs -> xs @ (F.asprintf "%a%d" Procname.pp proc_name !node_id :: astate) ) ) diff --git a/infer/src/checkers/PurityAnalysis.ml b/infer/src/checkers/PurityAnalysis.ml index 19373f677d3..4f513b1e136 100644 --- a/infer/src/checkers/PurityAnalysis.ml +++ b/infer/src/checkers/PurityAnalysis.ml @@ -185,9 +185,7 @@ let compute_summary {InterproceduralAnalysis.proc_desc; tenv; analyze_dependency Procdesc.get_formals proc_desc |> List.map ~f:(fun (mname, _, _) -> Var.of_pvar (Pvar.mk mname proc_name)) in - let get_callee_summary callee_pname = - analyze_dependency callee_pname |> Option.bind ~f:(fun (_, (purity_opt, _)) -> purity_opt) - in + let get_callee_summary callee_pname = analyze_dependency callee_pname |> Option.bind ~f:fst in let analysis_data = {tenv; inferbo_invariant_map; formals; get_callee_summary} in Analyzer.compute_post analysis_data ~initial:PurityDomain.pure proc_desc diff --git a/infer/src/checkers/RequiredProps.ml b/infer/src/checkers/RequiredProps.ml index b05d9a1d72a..48ae17a6fab 100644 --- a/infer/src/checkers/RequiredProps.ml +++ b/infer/src/checkers/RequiredProps.ml @@ -301,9 +301,10 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions) let init_analysis_data ({InterproceduralAnalysis.analyze_dependency} as interproc) = let get_proc_summary_and_formals callee_pname = - analyze_dependency callee_pname - |> Option.map ~f:(fun (callee_pdesc, callee_summary) -> - (callee_summary, Procdesc.get_pvar_formals callee_pdesc) ) + let open IOption.Let_syntax in + let* callee_summary = analyze_dependency callee_pname in + let+ callee_attrs = Attributes.load callee_pname in + (callee_summary, ProcAttributes.get_pvar_formals callee_attrs) in {interproc; get_proc_summary_and_formals} diff --git a/infer/src/checkers/SimpleLineage.ml b/infer/src/checkers/SimpleLineage.ml index f4caae3eb81..e460809fdd4 100644 --- a/infer/src/checkers/SimpleLineage.ml +++ b/infer/src/checkers/SimpleLineage.ml @@ -1198,13 +1198,12 @@ module TransferFunctions = struct (* Add the relevant Summary/Direct call edges from concrete arguments to the destination, depending on the presence of a summary. *) - let add_summary_flows shapes node (kind : LineageGraph.FlowKind.t) - (callee : (Procdesc.t * Summary.t) option) (argument_list : Exp.t list) (ret_id : Ident.t) - (astate : Domain.t) : Domain.t = + let add_summary_flows shapes node (kind : LineageGraph.FlowKind.t) (callee : Summary.t option) + (argument_list : Exp.t list) (ret_id : Ident.t) (astate : Domain.t) : Domain.t = match callee with | None -> add_tito_all shapes node kind argument_list ret_id astate - | Some (_callee_pdesc, {Summary.tito_arguments}) -> + | Some {Summary.tito_arguments} -> add_tito shapes node kind tito_arguments argument_list ret_id astate diff --git a/infer/src/checkers/SimpleShape.ml b/infer/src/checkers/SimpleShape.ml index 2fdbe1fe0df..455559c8e0b 100644 --- a/infer/src/checkers/SimpleShape.ml +++ b/infer/src/checkers/SimpleShape.ml @@ -710,7 +710,7 @@ struct () - let standard_model proc_desc summary ret_var args = + let standard_model procname summary ret_var args = (* Standard call of a known function: 1. We get the shape of the actual args and ret_id 2. We introduce into the environment the shapes of the formal args and return value of @@ -721,9 +721,10 @@ struct *) let ret_id_shape = Shape.Env.var_shape env ret_var in let actual_args_shapes = List.map ~f:shape_expr args in - let return = Var.of_pvar (Procdesc.get_ret_var proc_desc) in + let return = Var.of_pvar (Pvar.get_ret_pvar procname) in let formals = - List.map ~f:(fun (pvar, _typ) -> Var.of_pvar pvar) (Procdesc.get_pvar_formals proc_desc) + Attributes.load_exn procname |> ProcAttributes.get_pvar_formals + |> List.map ~f:(fun (pvar, _typ) -> Var.of_pvar pvar) in let formal_shapes, returned_shape = Shape.Summary.introduce ~return ~formals summary env in List.iter2_exn ~f:(fun s1 s2 -> Shape.Env.unify env s1 s2) actual_args_shapes formal_shapes ; @@ -736,8 +737,8 @@ struct model ret_var args | None -> ( match analyze_dependency procname with - | Some (proc_desc, summary) -> - standard_model proc_desc summary ret_var args + | Some summary -> + standard_model procname summary ret_var args | None -> unknown_model procname ret_var args ) end diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 42856f2e433..99b9bf96214 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -66,7 +66,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let is_compile_time_constructed {InterproceduralAnalysis.analyze_dependency} pv = let init_pname = Pvar.get_initializer_pname pv in match Option.bind init_pname ~f:(fun callee_pname -> analyze_dependency callee_pname) with - | Some (_, (Bottom, _)) -> + | Some (Bottom, _) -> (* we analyzed the initializer for this global and found that it doesn't require any runtime initialization so cannot participate in SIOF *) true @@ -172,7 +172,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Const (Cfun callee_pname), actuals, loc, _) -> let callee_astate = match analyze_dependency callee_pname with - | Some (_, (NonBottom trace, initialized_by_callee)) -> + | Some (NonBottom trace, initialized_by_callee) -> let already_initialized = snd astate in let dangerous_accesses = SiofTrace.sinks trace @@ -187,7 +187,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct dangerous_accesses in (NonBottom (SiofTrace.update_sinks trace sinks), initialized_by_callee) - | Some (_, ((Bottom, _) as callee_astate)) -> + | Some ((Bottom, _) as callee_astate) -> callee_astate | None -> L.d_printfln "Unknown call" ; @@ -222,7 +222,7 @@ let report_siof {InterproceduralAnalysis.proc_desc; err_log; analyze_dependency; = let trace_of_pname pname = match analyze_dependency pname with - | Some (_, (NonBottom summary, _)) -> + | Some (NonBottom summary, _) -> summary | _ -> SiofTrace.bottom diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 3f3ed6c3e27..ecab417c968 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -63,7 +63,7 @@ let method_overrides_annot annot tenv pname = method_overrides (method_has_annot let lookup_annotation_calls {InterproceduralAnalysis.analyze_dependency} annot pname = analyze_dependency pname - |> Option.bind ~f:(fun (_, astate) -> Domain.find_opt annot astate) + |> Option.bind ~f:(Domain.find_opt annot) |> Option.value ~default:Domain.SinkMap.empty @@ -501,7 +501,7 @@ module MakeTransferFunctions (CFG : ProcCfg.S) = struct match analyze_dependency callee_pname with | None -> astate - | Some (_, callee_call_map) -> + | Some callee_call_map -> L.d_printf "Applying summary for `%a`@\n" Procname.pp callee_pname ; let add_call_site annot sink calls astate = if Domain.CallSites.is_empty calls then astate diff --git a/infer/src/checkers/scopeLeakage.ml b/infer/src/checkers/scopeLeakage.ml index 46c21ef5a4a..4019d82747f 100644 --- a/infer/src/checkers/scopeLeakage.ml +++ b/infer/src/checkers/scopeLeakage.ml @@ -513,10 +513,12 @@ let apply_to_expr (e : Exp.t) scope = let apply_summary procname analyze_dependency ret_exp args = match analyze_dependency procname with - | Some (proc_desc, summary) -> + | Some summary -> let all_formals = - (Procdesc.get_ret_var proc_desc, Procdesc.get_ret_type proc_desc) - :: Procdesc.get_pvar_formals proc_desc + let attrs = Attributes.load_exn procname in + let ret_var = Pvar.get_ret_pvar procname in + let ret_type = attrs.ProcAttributes.ret_type in + (ret_var, ret_type) :: ProcAttributes.get_pvar_formals attrs in let all_actuals = ret_exp :: args in if equal_int (List.length all_formals) (List.length all_actuals) then diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index c794be14779..4603872c445 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -182,7 +182,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let remove_initialized_params {InterproceduralAnalysis.analyze_dependency} call maybe_uninit_vars idx access_expr remove_fields = match analyze_dependency call with - | Some (_, {UninitDomain.pre= init_formals; post= _}) -> ( + | Some {UninitDomain.pre= init_formals; post= _} -> ( match init_nth_actual_param call idx init_formals with | Some var_formal -> let maybe_uninit_vars = MaybeUninitVars.remove access_expr maybe_uninit_vars in @@ -200,7 +200,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* true if a function initializes at least a param or a field of a struct param *) let function_initializes_some_formal_params {InterproceduralAnalysis.analyze_dependency} call = match analyze_dependency call with - | Some (_, {UninitDomain.pre= initialized_formal_params; post= _}) -> + | Some {UninitDomain.pre= initialized_formal_params; post= _} -> not (D.is_empty initialized_formal_params) | _ -> false @@ -348,7 +348,7 @@ let checker ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) = ; prepost= {UninitDomain.pre= D.empty; post= D.empty} } in let proc_data = - let formals = FormalMap.make proc_desc in + let formals = FormalMap.make (Procdesc.get_attributes proc_desc) in {analysis_data; formals} in Analyzer.compute_post proc_data ~initial proc_desc diff --git a/infer/src/concurrency/ConcurrencyUtils.ml b/infer/src/concurrency/ConcurrencyUtils.ml index 674bfeb4db5..e977a19aa23 100644 --- a/infer/src/concurrency/ConcurrencyUtils.ml +++ b/infer/src/concurrency/ConcurrencyUtils.ml @@ -12,7 +12,7 @@ let get_java_class_initializer_summary_of {InterproceduralAnalysis.proc_desc; an | Procname.Java _ -> Procname.get_class_type_name procname |> Option.map ~f:(fun tname -> Procname.(Java (Java.get_class_initializer tname))) - |> Option.bind ~f:analyze_dependency |> Option.map ~f:snd + |> Option.bind ~f:analyze_dependency | _ -> None @@ -28,4 +28,4 @@ let get_java_constructor_summaries_of {InterproceduralAnalysis.proc_desc; tenv; (* keep only the constructors *) |> List.filter ~f:Procname.(function Java jname -> Java.is_constructor jname | _ -> false) (* get the summaries of the constructors *) - |> List.filter_map ~f:(fun pname -> analyze_dependency pname |> Option.map ~f:snd) + |> List.filter_map ~f:analyze_dependency diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 735142d462d..65d6e95662c 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -725,12 +725,12 @@ let branch_never_returns () = AttributeMapDomain.empty } -let integrate_summary formals ~callee_proc_desc summary ret_access_exp callee_pname actuals loc +let integrate_summary formals ~callee_proc_attrs summary ret_access_exp callee_pname actuals loc astate = let {threads; locks; never_returns; return_ownership; return_attribute} = summary in if never_returns then branch_never_returns () else - let callee_formals = FormalMap.make callee_proc_desc in + let callee_formals = FormalMap.make callee_proc_attrs in let astate = add_callee_accesses ~caller_formals:formals ~callee_formals ~callee_accesses:summary.accesses callee_pname actuals loc astate diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 0ce805e35bb..a614dfbb17a 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -185,7 +185,7 @@ val add_reads_of_hilexps : Tenv.t -> FormalMap.t -> HilExp.t list -> Location.t val integrate_summary : FormalMap.t - -> callee_proc_desc:Procdesc.t + -> callee_proc_attrs:ProcAttributes.t -> summary -> HilExp.access_expression -> Procname.t diff --git a/infer/src/concurrency/RacerDProcAnalysis.ml b/infer/src/concurrency/RacerDProcAnalysis.ml index 07cca81c8d1..5978516abfc 100644 --- a/infer/src/concurrency/RacerDProcAnalysis.ml +++ b/infer/src/concurrency/RacerDProcAnalysis.ml @@ -74,8 +74,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let process_call_summary analyze_dependency tenv formals ret_access_exp callee_pname actuals loc astate = match analyze_dependency callee_pname with - | Some (callee_proc_desc, summary) -> - Domain.integrate_summary formals ~callee_proc_desc summary ret_access_exp callee_pname + | Some summary -> + let callee_proc_attrs = Attributes.load_exn callee_pname in + Domain.integrate_summary formals ~callee_proc_attrs summary ret_access_exp callee_pname actuals loc astate | None -> process_call_without_summary tenv ret_access_exp callee_pname actuals astate @@ -225,7 +226,8 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.N let analyze ({InterproceduralAnalysis.proc_desc; tenv} as interproc) = let open RacerDDomain in - let proc_name = Procdesc.get_proc_name proc_desc in + let proc_attrs = Procdesc.get_attributes proc_desc in + let proc_name = proc_attrs.proc_name in let open ConcurrencyModels in let add_owned_formal acc base = OwnershipDomain.add base OwnershipAbstractValue.owned acc in let add_conditionally_owned_formal = @@ -233,9 +235,8 @@ let analyze ({InterproceduralAnalysis.proc_desc; tenv} as interproc) = (* [@InjectProp] allocates a fresh object to bind to the parameter *) String.is_suffix ~suffix:Annotations.inject_prop class_name in - let ret_annots = (Procdesc.get_attributes proc_desc).ret_annots in let is_inject_prop = - Annotations.method_has_annotation_with ret_annots + Annotations.method_has_annotation_with proc_attrs.ret_annots (List.map (Procdesc.get_formals proc_desc) ~f:trd3) is_owned_formal in @@ -283,7 +284,7 @@ let analyze ({InterproceduralAnalysis.proc_desc; tenv} as interproc) = else add_conditionally_owned_formal acc base index ) in let initial = {initial with ownership; threads; locks} in - let formals = FormalMap.make proc_desc in + let formals = FormalMap.make proc_attrs in let analysis_data = {interproc; formals} in Analyzer.compute_post analysis_data ~initial proc_desc |> Option.map ~f:(astate_to_summary proc_desc formals) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index dbe9d9ff1ad..aa5ff2e2be7 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -174,7 +174,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Some (make_ret_attr (Looper ForUIThread)) else None in - let get_callee_summary () = analyze_dependency callee |> Option.map ~f:snd in + let get_callee_summary () = analyze_dependency callee in let treat_handler_constructor () = if StarvationModels.is_handler_constructor tenv callee actuals then match actuals_acc_exps with @@ -429,7 +429,7 @@ let analyze_procedure ({InterproceduralAnalysis.proc_desc; tenv} as interproc) = let procname = Procdesc.get_proc_name proc_desc in if StarvationModels.should_skip_analysis tenv procname [] then None else - let formals = FormalMap.make proc_desc in + let formals = FormalMap.make (Procdesc.get_attributes proc_desc) in let proc_data = {interproc; formals} in let loc = Procdesc.get_loc proc_desc in let set_lock_state_for_synchronized_proc astate = diff --git a/infer/src/cost/ConfigImpactAnalysis.ml b/infer/src/cost/ConfigImpactAnalysis.ml index c0460fefa86..dc841bb2443 100644 --- a/infer/src/cost/ConfigImpactAnalysis.ml +++ b/infer/src/cost/ConfigImpactAnalysis.ml @@ -947,7 +947,7 @@ module Dom = struct match analyze_dependency callee with | None -> None - | Some (_, (_, analysis_data, _)) -> + | Some (_, analysis_data, _) -> analysis_data in let expensiveness_model = get_expensiveness_model tenv callee args in @@ -1111,7 +1111,7 @@ module TransferFunctions = struct let add_ret analyze_dependency id callee astate = match analyze_dependency callee with - | Some (_, (_, Some {Summary.ret= ret_val}, _)) -> + | Some (_, Some {Summary.ret= ret_val}, _) -> Dom.add_mem (Loc.of_id id) ret_val astate | _ -> astate diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 1842dc4df3e..36fe202d985 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -374,7 +374,7 @@ let compute_bound_map tenv proc_desc node_cfg inferbo_invariant_map analyze_depe in let loop_inv_map = let get_callee_purity callee_pname = - match analyze_dependency callee_pname with Some (_, (_, _, purity)) -> purity | _ -> None + match analyze_dependency callee_pname with Some (_, _, purity) -> purity | _ -> None in LoopInvariant.get_loop_inv_var_map tenv get_callee_purity reaching_defs_invariant_map loop_head_to_loop_nodes @@ -428,16 +428,12 @@ let checker ({InterproceduralAnalysis.proc_desc; exe_env; analyze_dependency} as in let get_node_nb_exec = compute_get_node_nb_exec node_cfg bound_map in let astate = - let get_summary_common callee_pname = - let+ _, summaries = analyze_dependency callee_pname in - summaries - in let get_summary callee_pname = - let* cost_summary, _inferbo_summary, _ = get_summary_common callee_pname in + let* cost_summary, _inferbo_summary, _ = analyze_dependency callee_pname in cost_summary in let inferbo_get_summary callee_pname = - let* _cost_summary, inferbo_summary, _ = get_summary_common callee_pname in + let* _cost_summary, inferbo_summary, _ = analyze_dependency callee_pname in inferbo_summary in let get_formals callee_pname = diff --git a/infer/src/cost/costInstantiate.ml b/infer/src/cost/costInstantiate.ml index a72475092e1..ea796b786ab 100644 --- a/infer/src/cost/costInstantiate.ml +++ b/infer/src/cost/costInstantiate.ml @@ -84,14 +84,13 @@ let prepare_call_args (InterproceduralAnalysis.bind_payload ~f:fst3 analysis_data) in let get_callee_cost_summary_and_formals callee_pname = - let* callee_pdesc, (_inferbo, _, callee_costs_summary) = analyze_dependency callee_pname in + let* _inferbo, _, callee_costs_summary = analyze_dependency callee_pname in + let* callee_attrs = Attributes.load callee_pname in let+ callee_costs_summary in - (callee_costs_summary, Procdesc.get_pvar_formals callee_pdesc) + (callee_costs_summary, ProcAttributes.get_pvar_formals callee_attrs) in let inferbo_get_summary callee_pname = - let* _callee_pdesc, (inferbo, _purity, _callee_costs_summary) = - analyze_dependency callee_pname - in + let* inferbo, _purity, _callee_costs_summary = analyze_dependency callee_pname in inferbo in { tenv diff --git a/infer/src/cost/hoisting.ml b/infer/src/cost/hoisting.ml index 218673608c5..1fee2a831de 100644 --- a/infer/src/cost/hoisting.ml +++ b/infer/src/cost/hoisting.ml @@ -130,9 +130,7 @@ let checker CostInstantiate.get_cost_if_expensive analysis_data else fun _ -> None in - let get_callee_purity callee_pname = - match analyze_dependency callee_pname with Some (_, (_, purity, _)) -> purity | _ -> None - in + let get_callee_purity callee_pname = Option.bind ~f:snd3 (analyze_dependency callee_pname) in report_errors proc_desc tenv err_log get_callee_purity reaching_defs_invariant_map loop_head_to_source_nodes extract_cost_if_expensive ; () diff --git a/infer/src/labs/04_interprocedural/ResourceLeaks.ml b/infer/src/labs/04_interprocedural/ResourceLeaks.ml index 0bbb70e30e8..a652bab1c2a 100644 --- a/infer/src/labs/04_interprocedural/ResourceLeaks.ml +++ b/infer/src/labs/04_interprocedural/ResourceLeaks.ml @@ -57,7 +57,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ResourceLeakDomain.release_resource astate else match analyze_dependency callee_procname with - | Some (_callee_proc_desc, callee_summary) -> + | Some callee_summary -> (* interprocedural analysis produced a summary: use it *) ResourceLeakDomain.apply_summary ~summary:callee_summary astate | None -> diff --git a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml index 99c32062697..255a0d29542 100644 --- a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml +++ b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml @@ -64,7 +64,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate ) | Call (return, Direct callee_procname, actuals, _, _loc) -> ( match analyze_dependency callee_procname with - | Some (_callee_proc_desc, callee_summary) -> + | Some callee_summary -> (* interprocedural analysis produced a summary: use it *) ResourceLeakDomain.Summary.apply ~callee:callee_summary ~return ~actuals astate | None -> @@ -111,6 +111,6 @@ let report_if_leak {InterproceduralAnalysis.proc_desc; err_log; _} formal_map po let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = let result = Analyzer.compute_post analysis_data ~initial:ResourceLeakDomain.initial proc_desc in Option.map result ~f:(fun post -> - let formal_map = FormalMap.make proc_desc in + let formal_map = FormalMap.make (Procdesc.get_attributes proc_desc) in report_if_leak analysis_data formal_map post ; ResourceLeakDomain.Summary.make formal_map post ) diff --git a/infer/src/labs/README.md b/infer/src/labs/README.md index 2c47e46cca4..04a10b0230c 100644 --- a/infer/src/labs/README.md +++ b/infer/src/labs/README.md @@ -125,7 +125,7 @@ Augment the summary type with state to indicate whether the current procedure re ```OCaml match analyze_dependency callee_procname with - | Some (callee_proc_desc, callee_summary) -> + | Some callee_summary -> (* interprocedural analysis produced a summary: use it *) () | None -> diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index e843bf32e2c..b7022a73307 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -410,8 +410,8 @@ let call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals call_k (post :: posts, merge_contradictions contradiction new_contradiction) ) -let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc - callee_pname ~ret ~actuals ~formals_opt ~call_kind (astate : AbductiveDomain.t) = +let call tenv path ~caller_proc_desc ~(callee_data : PulseSummary.t option) call_loc callee_pname + ~ret ~actuals ~formals_opt ~call_kind (astate : AbductiveDomain.t) = (* a special case for objc nil messaging *) let unknown_objc_nil_messaging astate_unknown proc_name proc_attrs = let result_unknown = @@ -430,9 +430,9 @@ let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary. (result_unknown @ result_unknown_nil, contradiction) in match callee_data with - | Some (callee_proc_desc, exec_states) -> + | Some exec_states -> call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals call_kind - (Procdesc.get_attributes callee_proc_desc) + (IRAttributes.load_exn callee_pname) exec_states astate | None -> (* no spec found for some reason (unknown function, ...) *) diff --git a/infer/src/pulse/PulseCallOperations.mli b/infer/src/pulse/PulseCallOperations.mli index 42e2fe712a1..b4a29482673 100644 --- a/infer/src/pulse/PulseCallOperations.mli +++ b/infer/src/pulse/PulseCallOperations.mli @@ -15,7 +15,7 @@ val call : Tenv.t -> PathContext.t -> caller_proc_desc:Procdesc.t - -> callee_data:(Procdesc.t * PulseSummary.t) option + -> callee_data:PulseSummary.t option -> Location.t -> Procname.t -> ret:Ident.t * Typ.t diff --git a/infer/src/pulse/PulseClosureSpecialization.ml b/infer/src/pulse/PulseClosureSpecialization.ml index 8886f1c1ff1..f430e89cc0b 100644 --- a/infer/src/pulse/PulseClosureSpecialization.ml +++ b/infer/src/pulse/PulseClosureSpecialization.ml @@ -26,12 +26,11 @@ let specialize_captured_vars {InterproceduralAnalysis.proc_desc} captured_vars = {captured_var with pvar= Pvar.specialize_pvar pvar caller_pname} ) -let get_procname_and_captured value ({InterproceduralAnalysis.analyze_dependency} as analysis_data) - astate = +let get_procname_and_captured value analysis_data astate = let open IOption.Let_syntax in let* procname = AddressAttributes.get_closure_proc_name value astate in - let+ pdesc, _ = analyze_dependency procname in - let captured_vars = Procdesc.get_captured pdesc |> specialize_captured_vars analysis_data in + let+ {ProcAttributes.captured} = IRAttributes.load procname in + let captured_vars = specialize_captured_vars analysis_data captured in (procname, captured_vars) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 1db815f4b1e..212776e73de 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -123,7 +123,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct TaintDomain.bottom else match analyze_dependency pname with - | Some (_, summary) -> + | Some summary -> TaintSpecification.of_summary_access_tree summary | None -> TaintDomain.bottom @@ -638,7 +638,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct match analyze_dependency callee_pname with | None -> handle_unknown_call callee_pname astate_with_direct_sources - | Some (_, summary) -> ( + | Some summary -> ( let ret_typ = snd ret_ap in let access_tree = TaintSpecification.of_summary_access_tree summary in match TaintSpecification.get_model callee_pname ret_typ actuals tenv access_tree with @@ -842,7 +842,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct (TraceDomain.Source.get_tainted_formals pdesc tenv) in let initial = make_initial proc_desc in - let formal_map = FormalMap.make proc_desc in + let formal_map = FormalMap.make (Procdesc.get_attributes proc_desc) in let proc_data = {analysis_data; formal_map} in match Analyzer.compute_post proc_data ~initial proc_desc with | Some access_tree -> diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 9e5b5332cd3..d559bc6f2cc 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -153,8 +153,9 @@ let tests = |> TestInterpreter.create_tests ~pp_opt:pp_sparse (fun summary -> { analysis_data= - CallbackOfChecker.mk_interprocedural_field_t Payloads.Fields.quandary (Exe_env.mk ()) - summary ~tenv:(Tenv.create ()) () + CallbackOfChecker.mk_interprocedural_field_t Payloads.Fields.quandary + {exe_env= Exe_env.mk (); summary} + ~tenv:(Tenv.create ()) () |> fst ; formal_map= FormalMap.empty } ) ~initial:(MockTaintAnalysis.Domain.bottom, Bindings.empty) From b44a87c88093f833a97838a4358d35a048d375c3 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 22 Feb 2023 06:05:50 -0800 Subject: [PATCH 12/25] Add procdescs to proc_callback_args Summary: Previously, procdescs (i.e. procedure CFGs) were stored in summaries; since previous diffs removed that field, this diff adds an additional `Procdesc.t` argument to procedure-analysis callbacks, simplifying some unit testing logic and avoiding multiple `Procdesc.load`s of the same procedure. Reviewed By: ngorogiannis Differential Revision: D43047928 fbshipit-source-id: 55ff653e1505a860ccec31741f430b530eb60d43 --- infer/src/backend/CallbackOfChecker.ml | 6 +++--- infer/src/backend/callbacks.ml | 7 +++---- infer/src/backend/callbacks.mli | 4 ++-- infer/src/backend/ondemand.ml | 7 ++++--- infer/src/unit/TaintTests.ml | 2 +- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index 5d002ba6073..5b0fe27b67d 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -12,7 +12,7 @@ open! IStd let () = AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session} let mk_interprocedural_t ~f_analyze_dep ~get_payload - {Callbacks.exe_env; summary= {Summary.stats; proc_desc; err_log} as caller_summary} + {Callbacks.exe_env; proc_desc; summary= {Summary.stats; err_log} as caller_summary} ?(tenv = Exe_env.get_proc_tenv exe_env (Procdesc.get_proc_name proc_desc)) () = let analyze_dependency proc_name = let open IOption.Let_syntax in @@ -61,8 +61,8 @@ let interprocedural_file payload_field checker {Callbacks.procedures; exe_env; s {InterproceduralAnalysis.procedures; source_file; file_exe_env= exe_env; analyze_file_dependency} -let to_intraprocedural_t {Callbacks.summary; exe_env} = - { IntraproceduralAnalysis.proc_desc= Summary.get_proc_desc summary +let to_intraprocedural_t {Callbacks.summary; exe_env; proc_desc} = + { IntraproceduralAnalysis.proc_desc ; tenv= Exe_env.get_proc_tenv exe_env (Summary.get_proc_name summary) ; err_log= Summary.get_err_log summary } diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 9a3a9b9b281..e35d3d33b86 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -8,7 +8,7 @@ open! IStd module L = Logging -type proc_callback_args = {summary: Summary.t; exe_env: Exe_env.t} +type proc_callback_args = {summary: Summary.t; exe_env: Exe_env.t; proc_desc: Procdesc.t} type proc_callback_t = proc_callback_args -> Summary.t @@ -36,8 +36,7 @@ let register_file_callback checker language (callback : file_callback_t) = file_callbacks_rev := {checker; language; callback} :: !file_callbacks_rev -let iterate_procedure_callbacks exe_env summary = - let proc_desc = Summary.get_proc_desc summary in +let iterate_procedure_callbacks exe_env summary proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in let procedure_language = Procname.get_language proc_name in Language.curr_language := procedure_language ; @@ -52,7 +51,7 @@ let iterate_procedure_callbacks exe_env summary = () )) ; let summary = Timer.time (Checker checker) - ~f:(fun () -> callback {summary; exe_env}) + ~f:(fun () -> callback {summary; exe_env; proc_desc}) ~on_timeout:(fun span -> L.debug Analysis Quiet "TIMEOUT in %s after %fs of CPU time analyzing %a:%a@\n" (Checker.get_id checker) span SourceFile.pp diff --git a/infer/src/backend/callbacks.mli b/infer/src/backend/callbacks.mli index 215d322dc9e..e273dcd24c6 100644 --- a/infer/src/backend/callbacks.mli +++ b/infer/src/backend/callbacks.mli @@ -27,7 +27,7 @@ open! IStd - get_proc_desc to get a proc desc from a proc name - Type environment. - Procedure for the callback to act on. *) -type proc_callback_args = {summary: Summary.t; exe_env: Exe_env.t} +type proc_callback_args = {summary: Summary.t; exe_env: Exe_env.t; proc_desc: Procdesc.t} (* Result is updated summary with all information relevant for the checker (including list of errors found by the checker for this procedure *) type proc_callback_t = proc_callback_args -> Summary.t @@ -47,7 +47,7 @@ val register_file_callback : Checker.t -> Language.t -> file_callback_t -> unit (** Register a file callback (see details above). [issues_dir] must be unique for this type of checker. *) -val iterate_procedure_callbacks : Exe_env.t -> Summary.t -> Summary.t +val iterate_procedure_callbacks : Exe_env.t -> Summary.t -> Procdesc.t -> Summary.t (** Invoke all registered procedure callbacks on the given procedure. *) val iterate_file_callbacks_and_store_issues : Procname.t list -> Exe_env.t -> SourceFile.t -> unit diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 7345f65f342..bc091e12c0e 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -123,8 +123,8 @@ let update_taskbar proc_name_opt source_file_opt = !ProcessPoolState.update_status t0 status -let analyze exe_env callee_summary = - let summary = Callbacks.iterate_procedure_callbacks exe_env callee_summary in +let analyze exe_env callee_summary callee_pdesc = + let summary = Callbacks.iterate_procedure_callbacks exe_env callee_summary callee_pdesc in Stats.incr_ondemand_procs_analyzed () ; summary @@ -187,7 +187,8 @@ let run_proc_analysis exe_env ~caller_pdesc callee_pdesc = let initial_callee_summary = preprocess () in try let callee_summary = - if callee_attributes.ProcAttributes.is_defined then analyze exe_env initial_callee_summary + if callee_attributes.ProcAttributes.is_defined then + analyze exe_env initial_callee_summary callee_pdesc else initial_callee_summary in let final_callee_summary = postprocess callee_summary in diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index d559bc6f2cc..6cc2965cfe1 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -154,7 +154,7 @@ let tests = (fun summary -> { analysis_data= CallbackOfChecker.mk_interprocedural_field_t Payloads.Fields.quandary - {exe_env= Exe_env.mk (); summary} + {proc_desc= summary.proc_desc; exe_env= Exe_env.mk (); summary} ~tenv:(Tenv.create ()) () |> fst ; formal_map= FormalMap.empty } ) From 18bfa91c8b07e01f3e4b39782aaef886701c8e7e Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 22 Feb 2023 06:05:53 -0800 Subject: [PATCH 13/25] Remove procdescs from summaries Summary: Remove procedure CFGs (i.e. procdescs) from summaries, to minimize analysis DB sizes and avoid some potential bugs that occur when multiple (possibly different) procdescs exist for the same procedure. Instead we now store procedure attributes only, which can provide most of the necessary information, and fallback to `Procdesc.load` when a full CFG is needed. Reviewed By: skcho Differential Revision: D43313295 fbshipit-source-id: f71e19dc17d0a88967afa64e310cf06b59f03776 --- infer/src/IR/Procdesc.ml | 2 + infer/src/IR/Procdesc.mli | 3 ++ infer/src/backend/AnalysisDependencyGraph.ml | 11 +++-- infer/src/backend/CallbackOfChecker.ml | 10 ++--- infer/src/backend/StarvationGlobalAnalysis.ml | 18 ++++----- infer/src/backend/Summary.ml | 40 ++++++------------- infer/src/backend/Summary.mli | 13 +----- infer/src/backend/callbacks.ml | 2 +- infer/src/backend/ondemand.ml | 30 ++++++-------- infer/src/backend/printer.ml | 4 +- infer/src/integration/ReportSimpleLineage.ml | 10 ++--- infer/src/unit/TaintTests.ml | 3 +- infer/src/unit/analyzerTester.ml | 2 +- infer/src/unit/livenessTests.ml | 2 +- 14 files changed, 63 insertions(+), 87 deletions(-) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 399d46ec59c..2c3e9e26ae4 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -965,6 +965,8 @@ let load = (run_query load_statement_adb) +let load_exn procname = load procname |> Option.value_exn + let mark_if_unchanged ~old_pdesc ~new_pdesc = (* map from exp names in [old_pdesc] to exp names in [new_pdesc] *) let exp_map = ref Exp.Map.empty in diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 7facbb53f44..b2d8fc7ef62 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -380,5 +380,8 @@ module SQLite : SqliteUtils.Data with type t = t option val load : Procname.t -> t option +val load_exn : Procname.t -> t +(** like [load], but raises an exception if no procdesc is available. *) + val mark_if_unchanged : old_pdesc:t -> new_pdesc:t -> unit (** Record the [changed] attribute in-place on [new_pdesc] if it is unchanged wrt [old_pdsec] *) diff --git a/infer/src/backend/AnalysisDependencyGraph.ml b/infer/src/backend/AnalysisDependencyGraph.ml index c42e188494c..f26d569d735 100644 --- a/infer/src/backend/AnalysisDependencyGraph.ml +++ b/infer/src/backend/AnalysisDependencyGraph.ml @@ -11,23 +11,22 @@ let build ~changed_files = let graph = CallGraph.(create default_initial_capacity) in let tenv_deps = SourceFile.Hash.create 0 in (* First, build a reverse analysis callgraph [graph] and tenv dependency map [tenv_deps]. *) - Summary.OnDisk.iter_specs ~f:(fun summary -> - let summary_pname = Summary.get_proc_name summary in + Summary.OnDisk.iter_specs ~f:(fun {Summary.proc_attrs= {proc_name}; dependencies} -> let Summary.Deps.{callees; used_tenv_sources} = - match summary.dependencies with + match dependencies with | Complete c -> c | Partial _ -> L.die InternalError "deserialized summary with incomplete dependencies" in List.iter callees ~f:(fun callee -> - CallGraph.add_edge graph ~pname:callee ~successor_pname:summary_pname ) ; + CallGraph.add_edge graph ~pname:callee ~successor_pname:proc_name ) ; List.iter used_tenv_sources ~f:(fun src_file -> match SourceFile.Hash.find_opt tenv_deps src_file with | Some deps -> - Procname.HashSet.add summary_pname deps + Procname.HashSet.add proc_name deps | None -> - Procname.HashSet.singleton summary_pname |> SourceFile.Hash.add tenv_deps src_file ) ) ; + Procname.HashSet.singleton proc_name |> SourceFile.Hash.add tenv_deps src_file ) ) ; (* Then, flag in [graph] any procedure with a summary depending (transitively) on either (1) the tenv of a changed file or (2) the summary of a changed procedure. *) SourceFile.Set.iter diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index 5b0fe27b67d..18f4fd31dc8 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -12,8 +12,8 @@ open! IStd let () = AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session} let mk_interprocedural_t ~f_analyze_dep ~get_payload - {Callbacks.exe_env; proc_desc; summary= {Summary.stats; err_log} as caller_summary} - ?(tenv = Exe_env.get_proc_tenv exe_env (Procdesc.get_proc_name proc_desc)) () = + {Callbacks.exe_env; proc_desc; summary= {Summary.stats; proc_attrs; err_log} as caller_summary} + ?(tenv = Exe_env.get_proc_tenv exe_env proc_attrs.proc_name) () = let analyze_dependency proc_name = let open IOption.Let_syntax in let* {Summary.payloads} = Ondemand.analyze_proc_name exe_env ~caller_summary proc_name in @@ -61,10 +61,10 @@ let interprocedural_file payload_field checker {Callbacks.procedures; exe_env; s {InterproceduralAnalysis.procedures; source_file; file_exe_env= exe_env; analyze_file_dependency} -let to_intraprocedural_t {Callbacks.summary; exe_env; proc_desc} = +let to_intraprocedural_t {Callbacks.summary= {proc_attrs; err_log}; exe_env; proc_desc} = { IntraproceduralAnalysis.proc_desc - ; tenv= Exe_env.get_proc_tenv exe_env (Summary.get_proc_name summary) - ; err_log= Summary.get_err_log summary } + ; tenv= Exe_env.get_proc_tenv exe_env proc_attrs.proc_name + ; err_log } let intraprocedural checker ({Callbacks.summary} as callbacks) = diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index 9cafc5be261..d535ff4142e 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -28,19 +28,17 @@ let iter_critical_pairs_of_scheduled_work f (work_item : Domain.ScheduledWorkIte |> Option.iter ~f:(iter_critical_pairs_of_summary (iter_scheduled_pair work_item f)) -let iter_summary ~f exe_env (summary : Summary.t) = +let iter_summary ~f exe_env ({payloads; proc_attrs= {proc_name}} : Summary.t) = let open Domain in - Payloads.starvation summary.payloads - |> Lazy.force + Payloads.starvation payloads |> Lazy.force |> Option.iter ~f:(fun (payload : summary) -> - let pname = Summary.get_proc_name summary in - let tenv = Exe_env.get_proc_tenv exe_env pname in + let tenv = Exe_env.get_proc_tenv exe_env proc_name in if - StarvationModels.is_java_main_method pname - || ConcurrencyModels.is_android_lifecycle_method tenv pname - then iter_critical_pairs_of_summary (f pname) payload ; + StarvationModels.is_java_main_method proc_name + || ConcurrencyModels.is_android_lifecycle_method tenv proc_name + then iter_critical_pairs_of_summary (f proc_name) payload ; ScheduledWorkDomain.iter - (iter_critical_pairs_of_scheduled_work (f pname)) + (iter_critical_pairs_of_scheduled_work (f proc_name)) payload.scheduled_work ) @@ -66,7 +64,7 @@ let report exe_env work_set = let wrap_report (procname, (pair : CriticalPair.t)) init = Summary.OnDisk.get ~lazy_payloads:true procname |> Option.fold ~init ~f:(fun acc summary -> - let pattrs = Attributes.load_exn procname in + let pattrs = summary.Summary.proc_attrs in let tenv = Exe_env.get_proc_tenv exe_env procname in let acc = Starvation.report_on_pair diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index 4565ca3d5bc..672c50548ef 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -81,30 +81,26 @@ type t = { payloads: Payloads.t ; mutable sessions: int ; stats: Stats.t - ; proc_desc: Procdesc.t + ; proc_attrs: ProcAttributes.t ; err_log: Errlog.t ; mutable dependencies: Deps.t } -let yojson_of_t {proc_desc; payloads} = - [%yojson_of: Procname.t * Payloads.t] (Procdesc.get_proc_name proc_desc, payloads) +let yojson_of_t {proc_attrs; payloads} = + [%yojson_of: Procname.t * Payloads.t] (proc_attrs.proc_name, payloads) type full_summary = t -let get_proc_desc summary = summary.proc_desc +let get_proc_name summary = summary.proc_attrs.proc_name -let get_attributes summary = Procdesc.get_attributes summary.proc_desc +let get_ret_type summary = summary.proc_attrs.ret_type -let get_proc_name summary = (get_attributes summary).ProcAttributes.proc_name +let get_formals summary = summary.proc_attrs.formals -let get_ret_type summary = (get_attributes summary).ProcAttributes.ret_type - -let get_formals summary = (get_attributes summary).ProcAttributes.formals +let get_loc summary = summary.proc_attrs.loc let get_err_log summary = summary.err_log -let get_loc summary = (get_attributes summary).ProcAttributes.loc - let pp_errlog fmt err_log = F.fprintf fmt "ERRORS: @[%a@]@\n%!" Errlog.pp_errors err_log ; F.fprintf fmt "WARNINGS: @[%a@]" Errlog.pp_warnings err_log @@ -156,13 +152,13 @@ module ReportSummary = struct end module SummaryMetadata = struct - type t = {sessions: int; stats: Stats.t; proc_desc: Procdesc.t; dependencies: Deps.complete} + type t = {sessions: int; stats: Stats.t; proc_attrs: ProcAttributes.t; dependencies: Deps.complete} [@@deriving fields] let of_full_summary (f : full_summary) : t = { sessions= f.sessions ; stats= f.stats - ; proc_desc= f.proc_desc + ; proc_attrs= f.proc_attrs ; dependencies= Deps.complete_exn f.dependencies } @@ -176,7 +172,7 @@ let mk_full_summary payloads (report_summary : ReportSummary.t) { payloads ; sessions= summary_metadata.sessions ; stats= summary_metadata.stats - ; proc_desc= summary_metadata.proc_desc + ; proc_attrs= summary_metadata.proc_attrs ; dependencies= Deps.Complete summary_metadata.dependencies ; err_log= report_summary.err_log } @@ -273,15 +269,6 @@ module OnDisk = struct load_summary_to_spec_table ~lazy_payloads proc_name - let get_model_proc_desc model_name = - if not (BiabductionModels.mem model_name) then - Logging.die InternalError "Requested summary of model that couldn't be found: %a@\n" - Procname.pp model_name - else - (* we only care about the proc_desc so load analysis payloads lazily (i.e. not at all) *) - Option.map (get ~lazy_payloads:true model_name) ~f:(fun (s : full_summary) -> s.proc_desc) - - (** Save summary for the procedure into the spec database *) let store (summary : t) = let proc_name = get_proc_name summary in @@ -297,17 +284,16 @@ module OnDisk = struct ~summary_metadata:(SummaryMetadata.SQLite.serialize summary_metadata) - let reset proc_desc = - let pname = Procdesc.get_proc_name proc_desc in + let reset proc_attrs = let summary = { sessions= 0 ; payloads= Payloads.empty ; stats= Stats.empty - ; proc_desc + ; proc_attrs ; err_log= Errlog.empty () ; dependencies= Deps.empty () } in - Procname.Hash.replace cache pname summary ; + Procname.Hash.replace cache (ProcAttributes.get_proc_name proc_attrs) summary ; summary diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index 45dd1713ea2..f5a720e8014 100644 --- a/infer/src/backend/Summary.mli +++ b/infer/src/backend/Summary.mli @@ -48,7 +48,7 @@ type t = { payloads: Payloads.t ; mutable sessions: int (** Session number: how many nodes went through symbolic execution *) ; stats: Stats.t - ; proc_desc: Procdesc.t + ; proc_attrs: ProcAttributes.t ; err_log: Errlog.t (** Those are issues that are detected for this procedure after per-procedure analysis. In addition to that there can be errors detected after file-level analysis (next stage @@ -58,13 +58,6 @@ type t = (** Dynamically discovered analysis-time dependencies used to compute this summary *) } [@@deriving yojson_of] -val get_proc_name : t -> Procname.t -(** Get the procedure name *) - -val get_proc_desc : t -> Procdesc.t - -val get_err_log : t -> Errlog.t - val pp_html : SourceFile.t -> Format.formatter -> t -> unit (** Print the summary in html format *) @@ -78,7 +71,7 @@ module OnDisk : sig val get : lazy_payloads:bool -> Procname.t -> t option (** Return the summary option for the procedure name *) - val reset : Procdesc.t -> t + val reset : ProcAttributes.t -> t (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *) val store : t -> unit @@ -105,8 +98,6 @@ module OnDisk : sig -> unit (** Iterates over all analysis artefacts listed above, for each procedure *) - val get_model_proc_desc : Procname.t -> Procdesc.t option - val get_count : unit -> int (** Counts the summaries currently stored on disk. *) end diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index e35d3d33b86..00f07c90261 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -37,7 +37,7 @@ let register_file_callback checker language (callback : file_callback_t) = let iterate_procedure_callbacks exe_env summary proc_desc = - let proc_name = Procdesc.get_proc_name proc_desc in + let proc_name = summary.Summary.proc_attrs.ProcAttributes.proc_name in let procedure_language = Procname.get_language proc_name in Language.curr_language := procedure_language ; let is_specialized = Procdesc.is_specialized proc_desc in diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index bc091e12c0e..f392cfe7faf 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -153,7 +153,7 @@ let run_proc_analysis exe_env ~caller_pdesc callee_pdesc = Preanal.do_preanalysis exe_env callee_pdesc ; if Config.debug_mode then DotCfg.emit_proc_desc callee_attributes.translation_unit callee_pdesc |> ignore ; - let initial_callee_summary = Summary.OnDisk.reset callee_pdesc in + let initial_callee_summary = Summary.OnDisk.reset (Procdesc.get_attributes callee_pdesc) in add_active callee_pname ; initial_callee_summary in @@ -165,18 +165,17 @@ let run_proc_analysis exe_env ~caller_pdesc callee_pdesc = log_elapsed_time () ; summary in - let log_error_and_continue exn (summary : Summary.t) kind = - BiabductionReporting.log_issue_using_state (Summary.get_proc_desc summary) - (Summary.get_err_log summary) exn ; - let stats = Summary.Stats.update summary.stats ~failure_kind:kind in + let log_error_and_continue exn ({Summary.err_log; stats; payloads} as summary) kind = + BiabductionReporting.log_issue_using_state callee_pdesc err_log exn ; + let stats = Summary.Stats.update stats ~failure_kind:kind in let payloads = let biabduction = Lazy.from_val (Some BiabductionSummary. - {preposts= []; phase= summary.payloads.biabduction |> Lazy.force |> opt_get_phase} ) + {preposts= []; phase= payloads.biabduction |> Lazy.force |> opt_get_phase} ) in - {summary.payloads with biabduction} + {payloads with biabduction} in let new_summary = {summary with stats; payloads} in Summary.OnDisk.store new_summary ; @@ -272,11 +271,6 @@ let register_callee ?caller_summary callee_pname = ~f:Summary.(fun {dependencies} -> Deps.add_exn dependencies callee_pname) -let get_proc_desc callee_pname = - if BiabductionModels.mem callee_pname then Summary.OnDisk.get_model_proc_desc callee_pname - else Procdesc.load callee_pname - - let analyze_callee exe_env ~lazy_payloads ?caller_summary callee_pname = register_callee ?caller_summary callee_pname ; if is_active callee_pname then None @@ -285,7 +279,7 @@ let analyze_callee exe_env ~lazy_payloads ?caller_summary callee_pname = | Some _ as summ_opt -> summ_opt | None when procedure_should_be_analyzed callee_pname -> - get_proc_desc callee_pname + Procdesc.load callee_pname |> Option.bind ~f:(fun callee_pdesc -> RestartScheduler.lock_exn callee_pname ; let previous_global_state = save_global_state () in @@ -294,10 +288,12 @@ let analyze_callee exe_env ~lazy_payloads ?caller_summary callee_pname = ~f:(fun () -> Timer.time Preanalysis ~f:(fun () -> - Some - (run_proc_analysis exe_env - ~caller_pdesc:(Option.map ~f:Summary.get_proc_desc caller_summary) - callee_pdesc ) ) + let caller_pdesc = + Option.bind + ~f:(fun {Summary.proc_attrs} -> Procdesc.load proc_attrs.proc_name) + caller_summary + in + Some (run_proc_analysis exe_env ~caller_pdesc callee_pdesc) ) ~on_timeout:(fun span -> L.debug Analysis Quiet "TIMEOUT after %fs of CPU time analyzing %a:%a, outside of any checkers \ diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 261a3743195..92a4de14f79 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -185,8 +185,8 @@ end = struct match Summary.OnDisk.get ~lazy_payloads:true proc_name with | None -> () - | Some summary -> - Errlog.update global_err_log (Summary.get_err_log summary) + | Some {err_log} -> + Errlog.update global_err_log err_log let write_html_file filename procs = diff --git a/infer/src/integration/ReportSimpleLineage.ml b/infer/src/integration/ReportSimpleLineage.ml index 5b4261d327f..94d0d1b42e2 100644 --- a/infer/src/integration/ReportSimpleLineage.ml +++ b/infer/src/integration/ReportSimpleLineage.ml @@ -8,13 +8,13 @@ open! IStd module L = Logging -let report {Summary.payloads= {simple_lineage}; proc_desc} = +let report {Summary.payloads= {simple_lineage}; proc_attrs} = + let proc_name = ProcAttributes.get_proc_name proc_attrs in match Lazy.force simple_lineage with | None -> - let procname = Procdesc.get_proc_name proc_desc in - L.user_warning "No summary for %a@\n" Procname.pp procname - | Some summary -> - SimpleLineage.Summary.report summary proc_desc + L.user_warning "No summary for %a@\n" Procname.pp proc_name + | Some lineage_summary -> + Procdesc.load_exn proc_name |> SimpleLineage.Summary.report lineage_summary let worker source_file = diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 6cc2965cfe1..93cc3ccbf35 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -152,9 +152,10 @@ let tests = , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ] |> TestInterpreter.create_tests ~pp_opt:pp_sparse (fun summary -> + let proc_desc = Procdesc.load_exn summary.proc_attrs.proc_name in { analysis_data= CallbackOfChecker.mk_interprocedural_field_t Payloads.Fields.quandary - {proc_desc= summary.proc_desc; exe_env= Exe_env.mk (); summary} + {proc_desc; exe_env= Exe_env.mk (); summary} ~tenv:(Tenv.create ()) () |> fst ; formal_map= FormalMap.empty } ) diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 5e83f3f1b5a..4eebe7e8744 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -293,7 +293,7 @@ struct set_succs last_node [exit_node] ~exn_handlers:no_exn_handlers ; Procdesc.set_exit_node pdesc exit_node ; Cfg.store src_file cfg ; - (Summary.OnDisk.reset pdesc, assert_map, pdesc) + (Summary.OnDisk.reset (Procdesc.get_attributes pdesc), assert_map, pdesc) let create_test test_program make_analysis_data ~initial pp_opt _ = diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 1329a04b63c..c5e04afcffb 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -141,7 +141,7 @@ let tests = , [invariant "normal:{ b, a }"; id_assign_var "x" "b"] , [id_assign_var "x" "a"] ) ] ) ] |> TestInterpreter.create_tests - (fun summary -> Summary.get_proc_desc summary) + (fun {proc_attrs} -> Procdesc.load_exn proc_attrs.proc_name) ~initial:Liveness.ExtendedDomain.bottom in "liveness_test_suite" >::: test_list From eb067600703acefb887e71c1fcf6e557b00823e5 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Wed, 22 Feb 2023 06:05:56 -0800 Subject: [PATCH 14/25] Replace proc attrs by names in summaries Summary: Take the previous diff one step further, removing proc attrs from summaries and replacing them with proc names. This incurs some amount of additional DB I/O when attributes are needed, but minimizes DB size and the risk of bugs from out-of-sync procedure attributes floating around. Reviewed By: skcho Differential Revision: D42968719 fbshipit-source-id: d4c3a9bcf66e92edcd67251c415eac81bf3ae41e --- infer/src/backend/AnalysisDependencyGraph.ml | 2 +- infer/src/backend/CallbackOfChecker.ml | 10 ++- infer/src/backend/StarvationGlobalAnalysis.ml | 4 +- infer/src/backend/Summary.ml | 65 ++++++++----------- infer/src/backend/Summary.mli | 4 +- infer/src/backend/callbacks.ml | 3 +- infer/src/backend/ondemand.ml | 6 +- infer/src/backend/preanal.ml | 2 +- infer/src/integration/ReportSimpleLineage.ml | 3 +- infer/src/unit/TaintTests.ml | 2 +- infer/src/unit/analyzerTester.ml | 2 +- infer/src/unit/livenessTests.ml | 2 +- 12 files changed, 44 insertions(+), 61 deletions(-) diff --git a/infer/src/backend/AnalysisDependencyGraph.ml b/infer/src/backend/AnalysisDependencyGraph.ml index f26d569d735..6d16a4346d5 100644 --- a/infer/src/backend/AnalysisDependencyGraph.ml +++ b/infer/src/backend/AnalysisDependencyGraph.ml @@ -11,7 +11,7 @@ let build ~changed_files = let graph = CallGraph.(create default_initial_capacity) in let tenv_deps = SourceFile.Hash.create 0 in (* First, build a reverse analysis callgraph [graph] and tenv dependency map [tenv_deps]. *) - Summary.OnDisk.iter_specs ~f:(fun {Summary.proc_attrs= {proc_name}; dependencies} -> + Summary.OnDisk.iter_specs ~f:(fun {Summary.proc_name; dependencies} -> let Summary.Deps.{callees; used_tenv_sources} = match dependencies with | Complete c -> diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index 18f4fd31dc8..5cfc2f680db 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -12,8 +12,8 @@ open! IStd let () = AnalysisCallbacks.set_callbacks {html_debug_new_node_session_f= NodePrinter.with_session} let mk_interprocedural_t ~f_analyze_dep ~get_payload - {Callbacks.exe_env; proc_desc; summary= {Summary.stats; proc_attrs; err_log} as caller_summary} - ?(tenv = Exe_env.get_proc_tenv exe_env proc_attrs.proc_name) () = + {Callbacks.exe_env; proc_desc; summary= {Summary.stats; proc_name; err_log} as caller_summary} + ?(tenv = Exe_env.get_proc_tenv exe_env proc_name) () = let analyze_dependency proc_name = let open IOption.Let_syntax in let* {Summary.payloads} = Ondemand.analyze_proc_name exe_env ~caller_summary proc_name in @@ -61,10 +61,8 @@ let interprocedural_file payload_field checker {Callbacks.procedures; exe_env; s {InterproceduralAnalysis.procedures; source_file; file_exe_env= exe_env; analyze_file_dependency} -let to_intraprocedural_t {Callbacks.summary= {proc_attrs; err_log}; exe_env; proc_desc} = - { IntraproceduralAnalysis.proc_desc - ; tenv= Exe_env.get_proc_tenv exe_env proc_attrs.proc_name - ; err_log } +let to_intraprocedural_t {Callbacks.summary= {proc_name; err_log}; exe_env; proc_desc} = + {IntraproceduralAnalysis.proc_desc; tenv= Exe_env.get_proc_tenv exe_env proc_name; err_log} let intraprocedural checker ({Callbacks.summary} as callbacks) = diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index d535ff4142e..b1f49a2f5dd 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -28,7 +28,7 @@ let iter_critical_pairs_of_scheduled_work f (work_item : Domain.ScheduledWorkIte |> Option.iter ~f:(iter_critical_pairs_of_summary (iter_scheduled_pair work_item f)) -let iter_summary ~f exe_env ({payloads; proc_attrs= {proc_name}} : Summary.t) = +let iter_summary ~f exe_env ({payloads; proc_name} : Summary.t) = let open Domain in Payloads.starvation payloads |> Lazy.force |> Option.iter ~f:(fun (payload : summary) -> @@ -64,7 +64,7 @@ let report exe_env work_set = let wrap_report (procname, (pair : CriticalPair.t)) init = Summary.OnDisk.get ~lazy_payloads:true procname |> Option.fold ~init ~f:(fun acc summary -> - let pattrs = summary.Summary.proc_attrs in + let pattrs = Attributes.load_exn procname in let tenv = Exe_env.get_proc_tenv exe_env procname in let acc = Starvation.report_on_pair diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index 672c50548ef..3d26d89e35c 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -81,54 +81,42 @@ type t = { payloads: Payloads.t ; mutable sessions: int ; stats: Stats.t - ; proc_attrs: ProcAttributes.t + ; proc_name: Procname.t ; err_log: Errlog.t ; mutable dependencies: Deps.t } -let yojson_of_t {proc_attrs; payloads} = - [%yojson_of: Procname.t * Payloads.t] (proc_attrs.proc_name, payloads) - +let yojson_of_t {proc_name; payloads} = [%yojson_of: Procname.t * Payloads.t] (proc_name, payloads) type full_summary = t -let get_proc_name summary = summary.proc_attrs.proc_name - -let get_ret_type summary = summary.proc_attrs.ret_type - -let get_formals summary = summary.proc_attrs.formals - -let get_loc summary = summary.proc_attrs.loc - -let get_err_log summary = summary.err_log - let pp_errlog fmt err_log = F.fprintf fmt "ERRORS: @[%a@]@\n%!" Errlog.pp_errors err_log ; F.fprintf fmt "WARNINGS: @[%a@]" Errlog.pp_warnings err_log -let pp_signature fmt summary = +let pp_signature fmt {proc_name} = + let {ProcAttributes.ret_type; formals} = Attributes.load_exn proc_name in let pp_formal fmt (p, typ, _) = F.fprintf fmt "%a %a" (Typ.pp_full Pp.text) typ Mangled.pp p in - F.fprintf fmt "%a %a(%a)" (Typ.pp_full Pp.text) (get_ret_type summary) Procname.pp - (get_proc_name summary) (Pp.seq ~sep:", " pp_formal) (get_formals summary) + F.fprintf fmt "%a %a(%a)" (Typ.pp_full Pp.text) ret_type Procname.pp proc_name + (Pp.seq ~sep:", " pp_formal) formals let pp_no_stats_specs fmt summary = F.fprintf fmt "%a@\n" pp_signature summary -let pp_text fmt summary = +let pp_text fmt ({err_log; payloads; stats} as summary) = pp_no_stats_specs fmt summary ; - F.fprintf fmt "%a@\n%a%a" pp_errlog (get_err_log summary) Stats.pp summary.stats - (Payloads.pp Pp.text) summary.payloads + F.fprintf fmt "%a@\n%a%a" pp_errlog err_log Stats.pp stats (Payloads.pp Pp.text) payloads -let pp_html source fmt summary = +let pp_html source fmt ({err_log; payloads; stats} as summary) = let pp_escaped pp fmt x = F.fprintf fmt "%s" (Escape.escape_xml (F.asprintf "%a" pp x)) in F.pp_force_newline fmt () ; Pp.html_with_color Black (pp_escaped pp_no_stats_specs) fmt summary ; - F.fprintf fmt "
%a
@\n" Stats.pp summary.stats ; - Errlog.pp_html source [] fmt (get_err_log summary) ; + F.fprintf fmt "
%a
@\n" Stats.pp stats ; + Errlog.pp_html source [] fmt err_log ; Io_infer.Html.pp_hline fmt () ; F.fprintf fmt "@\n" ; - pp_escaped (Payloads.pp (Pp.html Black)) fmt summary.payloads ; + pp_escaped (Payloads.pp (Pp.html Black)) fmt payloads ; F.fprintf fmt "@\n" @@ -139,11 +127,11 @@ module ReportSummary = struct ; config_impact_opt: ConfigImpactAnalysis.Summary.t option ; err_log: Errlog.t } - let of_full_summary (f : full_summary) : t = - { loc= get_loc f - ; cost_opt= Lazy.force f.payloads.Payloads.cost - ; config_impact_opt= Lazy.force f.payloads.Payloads.config_impact_analysis - ; err_log= f.err_log } + let of_full_summary ({proc_name; payloads; err_log} : full_summary) : t = + { loc= (Attributes.load_exn proc_name).loc + ; cost_opt= Lazy.force payloads.Payloads.cost + ; config_impact_opt= Lazy.force payloads.Payloads.config_impact_analysis + ; err_log } module SQLite = SqliteUtils.MarshalledDataNOTForComparison (struct @@ -152,13 +140,13 @@ module ReportSummary = struct end module SummaryMetadata = struct - type t = {sessions: int; stats: Stats.t; proc_attrs: ProcAttributes.t; dependencies: Deps.complete} + type t = {sessions: int; stats: Stats.t; proc_name: Procname.t; dependencies: Deps.complete} [@@deriving fields] let of_full_summary (f : full_summary) : t = { sessions= f.sessions ; stats= f.stats - ; proc_attrs= f.proc_attrs + ; proc_name= f.proc_name ; dependencies= Deps.complete_exn f.dependencies } @@ -172,7 +160,7 @@ let mk_full_summary payloads (report_summary : ReportSummary.t) { payloads ; sessions= summary_metadata.sessions ; stats= summary_metadata.stats - ; proc_attrs= summary_metadata.proc_attrs + ; proc_name= summary_metadata.proc_name ; dependencies= Deps.Complete summary_metadata.dependencies ; err_log= report_summary.err_log } @@ -270,30 +258,29 @@ module OnDisk = struct (** Save summary for the procedure into the spec database *) - let store (summary : t) = - let proc_name = get_proc_name summary in + let store ({proc_name; dependencies; payloads} as summary : t) = (* Make sure the summary in memory is identical to the saved one *) add proc_name summary ; - summary.dependencies <- Deps.(Complete (freeze proc_name summary.dependencies)) ; + summary.dependencies <- Deps.(Complete (freeze proc_name dependencies)) ; let report_summary = ReportSummary.of_full_summary summary in let summary_metadata = SummaryMetadata.of_full_summary summary in DBWriter.store_spec ~proc_uid:(Procname.to_unique_id proc_name) ~proc_name:(Procname.SQLite.serialize proc_name) - ~payloads:(Payloads.SQLite.serialize summary.payloads) + ~payloads:(Payloads.SQLite.serialize payloads) ~report_summary:(ReportSummary.SQLite.serialize report_summary) ~summary_metadata:(SummaryMetadata.SQLite.serialize summary_metadata) - let reset proc_attrs = + let reset proc_name = let summary = { sessions= 0 ; payloads= Payloads.empty ; stats= Stats.empty - ; proc_attrs + ; proc_name ; err_log= Errlog.empty () ; dependencies= Deps.empty () } in - Procname.Hash.replace cache (ProcAttributes.get_proc_name proc_attrs) summary ; + Procname.Hash.replace cache proc_name summary ; summary diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index f5a720e8014..6157682a108 100644 --- a/infer/src/backend/Summary.mli +++ b/infer/src/backend/Summary.mli @@ -48,7 +48,7 @@ type t = { payloads: Payloads.t ; mutable sessions: int (** Session number: how many nodes went through symbolic execution *) ; stats: Stats.t - ; proc_attrs: ProcAttributes.t + ; proc_name: Procname.t ; err_log: Errlog.t (** Those are issues that are detected for this procedure after per-procedure analysis. In addition to that there can be errors detected after file-level analysis (next stage @@ -71,7 +71,7 @@ module OnDisk : sig val get : lazy_payloads:bool -> Procname.t -> t option (** Return the summary option for the procedure name *) - val reset : ProcAttributes.t -> t + val reset : Procname.t -> t (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *) val store : t -> unit diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 00f07c90261..9ab8edccb4a 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -36,8 +36,7 @@ let register_file_callback checker language (callback : file_callback_t) = file_callbacks_rev := {checker; language; callback} :: !file_callbacks_rev -let iterate_procedure_callbacks exe_env summary proc_desc = - let proc_name = summary.Summary.proc_attrs.ProcAttributes.proc_name in +let iterate_procedure_callbacks exe_env ({Summary.proc_name} as summary) proc_desc = let procedure_language = Procname.get_language proc_name in Language.curr_language := procedure_language ; let is_specialized = Procdesc.is_specialized proc_desc in diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index f392cfe7faf..90b41b9fe52 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -153,7 +153,7 @@ let run_proc_analysis exe_env ~caller_pdesc callee_pdesc = Preanal.do_preanalysis exe_env callee_pdesc ; if Config.debug_mode then DotCfg.emit_proc_desc callee_attributes.translation_unit callee_pdesc |> ignore ; - let initial_callee_summary = Summary.OnDisk.reset (Procdesc.get_attributes callee_pdesc) in + let initial_callee_summary = Summary.OnDisk.reset callee_pname in add_active callee_pname ; initial_callee_summary in @@ -165,7 +165,7 @@ let run_proc_analysis exe_env ~caller_pdesc callee_pdesc = log_elapsed_time () ; summary in - let log_error_and_continue exn ({Summary.err_log; stats; payloads} as summary) kind = + let log_error_and_continue exn ({Summary.err_log; payloads; stats} as summary) kind = BiabductionReporting.log_issue_using_state callee_pdesc err_log exn ; let stats = Summary.Stats.update stats ~failure_kind:kind in let payloads = @@ -290,7 +290,7 @@ let analyze_callee exe_env ~lazy_payloads ?caller_summary callee_pname = ~f:(fun () -> let caller_pdesc = Option.bind - ~f:(fun {Summary.proc_attrs} -> Procdesc.load proc_attrs.proc_name) + ~f:(fun {Summary.proc_name} -> Procdesc.load proc_name) caller_summary in Some (run_proc_analysis exe_env ~caller_pdesc callee_pdesc) ) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index eefcb7ae7e6..7abef76d9c0 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -453,8 +453,8 @@ module NoReturn = struct end let do_preanalysis exe_env pdesc = - let tenv = Exe_env.get_proc_tenv exe_env (Procdesc.get_proc_name pdesc) in let proc_name = Procdesc.get_proc_name pdesc in + let tenv = Exe_env.get_proc_tenv exe_env proc_name in if Procname.is_java proc_name || Procname.is_csharp proc_name then InlineJavaSyntheticMethods.process pdesc ; (* NOTE: It is important that this preanalysis stays before Liveness *) diff --git a/infer/src/integration/ReportSimpleLineage.ml b/infer/src/integration/ReportSimpleLineage.ml index 94d0d1b42e2..742e72ee886 100644 --- a/infer/src/integration/ReportSimpleLineage.ml +++ b/infer/src/integration/ReportSimpleLineage.ml @@ -8,8 +8,7 @@ open! IStd module L = Logging -let report {Summary.payloads= {simple_lineage}; proc_attrs} = - let proc_name = ProcAttributes.get_proc_name proc_attrs in +let report {Summary.payloads= {simple_lineage}; proc_name} = match Lazy.force simple_lineage with | None -> L.user_warning "No summary for %a@\n" Procname.pp proc_name diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 93cc3ccbf35..53ad91ac876 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -152,7 +152,7 @@ let tests = , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ] |> TestInterpreter.create_tests ~pp_opt:pp_sparse (fun summary -> - let proc_desc = Procdesc.load_exn summary.proc_attrs.proc_name in + let proc_desc = Procdesc.load_exn summary.proc_name in { analysis_data= CallbackOfChecker.mk_interprocedural_field_t Payloads.Fields.quandary {proc_desc; exe_env= Exe_env.mk (); summary} diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 4eebe7e8744..49344a7a9d4 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -293,7 +293,7 @@ struct set_succs last_node [exit_node] ~exn_handlers:no_exn_handlers ; Procdesc.set_exit_node pdesc exit_node ; Cfg.store src_file cfg ; - (Summary.OnDisk.reset (Procdesc.get_attributes pdesc), assert_map, pdesc) + (Summary.OnDisk.reset pname, assert_map, pdesc) let create_test test_program make_analysis_data ~initial pp_opt _ = diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index c5e04afcffb..8c706d18664 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -141,7 +141,7 @@ let tests = , [invariant "normal:{ b, a }"; id_assign_var "x" "b"] , [id_assign_var "x" "a"] ) ] ) ] |> TestInterpreter.create_tests - (fun {proc_attrs} -> Procdesc.load_exn proc_attrs.proc_name) + (fun {proc_name} -> Procdesc.load_exn proc_name) ~initial:Liveness.ExtendedDomain.bottom in "liveness_test_suite" >::: test_list From 28e867254f6dc8c2a26d749575b472ca0ae27a0f Mon Sep 17 00:00:00 2001 From: Akos Hajdu Date: Wed, 22 Feb 2023 06:56:50 -0800 Subject: [PATCH 15/25] [erl-frontend] Add Topl taint tests with raw message passing Summary: Add some tests that illustrate taint properties in the presence of "raw" message passing (send/receive). Differential Revision: D43494631 fbshipit-source-id: eae87f6ec51621fbc65843bd597ed9015019c118 --- .../codetoanalyze/erlang/compiler/issues.exp | 8 ++ .../erlang/topl/taint/issues.exp | 4 + .../erlang/topl/taint/topl_taint.erl | 80 ++++++++++++++++++- 3 files changed, 91 insertions(+), 1 deletion(-) diff --git a/infer/tests/codetoanalyze/erlang/compiler/issues.exp b/infer/tests/codetoanalyze/erlang/compiler/issues.exp index 659f0f257c0..ced6b64a9a4 100644 --- a/infer/tests/codetoanalyze/erlang/compiler/issues.exp +++ b/infer/tests/codetoanalyze/erlang/compiler/issues.exp @@ -746,6 +746,8 @@ topl_process:test_2_Bad/0: expected_crash ----- topl_taint ----- topl_taint:fp_test_c2_Ok/0: ok +topl_taint:fp_test_send4_Ok/0: ok +topl_taint:fp_test_send8_Ok/0: ok topl_taint:test_a_Bad/0: taint_error topl_taint:test_b_Ok/0: ok topl_taint:test_c_Bad/0: taint_error @@ -756,4 +758,10 @@ topl_taint:test_g_Ok/0: ok topl_taint:test_h_Bad/0: taint_error topl_taint:test_i_Ok/0: ok topl_taint:test_j_Bad/0: case_clause +topl_taint:test_send1_Ok/0: ok +topl_taint:test_send2_Bad/0: taint_error +topl_taint:test_send3_Ok/0: ok +topl_taint:test_send5_Ok/0: ok +topl_taint:test_send6_Bad/0: taint_error +topl_taint:test_send7_Ok/0: ok diff --git a/infer/tests/codetoanalyze/erlang/topl/taint/issues.exp b/infer/tests/codetoanalyze/erlang/topl/taint/issues.exp index 22f2250d839..3c0be0cf16d 100644 --- a/infer/tests/codetoanalyze/erlang/topl/taint/issues.exp +++ b/infer/tests/codetoanalyze/erlang/topl/taint/issues.exp @@ -5,3 +5,7 @@ codetoanalyze/erlang/topl/taint/topl_taint.erl, test_d_Bad/0, 0, TOPL_ERROR, no_ codetoanalyze/erlang/topl/taint/topl_taint.erl, test_f_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to dirty_if_argument_nil/1,call to source/0,call to sink/1] codetoanalyze/erlang/topl/taint/topl_taint.erl, test_h_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to dirty_if_argument_nil/1,call to source/0,call to sink/1] codetoanalyze/erlang/topl/taint/topl_taint.erl, test_j_Bad/0, 1, NO_MATCHING_CASE_CLAUSE, no_bucket, ERROR, [no matching case clause here] +codetoanalyze/erlang/topl/taint/topl_taint.erl, test_send2_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to sink/1] +codetoanalyze/erlang/topl/taint/topl_taint.erl, fp_test_send4_Ok/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to sink/1] +codetoanalyze/erlang/topl/taint/topl_taint.erl, test_send6_Bad/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to sink/1] +codetoanalyze/erlang/topl/taint/topl_taint.erl, fp_test_send8_Ok/0, 0, TOPL_ERROR, no_bucket, ERROR, [call to source/0,call to sink/1] diff --git a/infer/tests/codetoanalyze/erlang/topl/taint/topl_taint.erl b/infer/tests/codetoanalyze/erlang/topl/taint/topl_taint.erl index 2a904549115..4169c7c899c 100644 --- a/infer/tests/codetoanalyze/erlang/topl/taint/topl_taint.erl +++ b/infer/tests/codetoanalyze/erlang/topl/taint/topl_taint.erl @@ -16,7 +16,17 @@ test_g_Ok/0, test_h_Bad/0, test_i_Ok/0, - test_j_Bad/0 + test_j_Bad/0, + tito_process/0, + sanitizer_process/0, + test_send1_Ok/0, + test_send2_Bad/0, + test_send3_Ok/0, + fp_test_send4_Ok/0, + test_send5_Ok/0, + test_send6_Bad/0, + test_send7_Ok/0, + fp_test_send8_Ok/0 ]). test_a_Bad() -> @@ -71,6 +81,74 @@ test_j_Bad() -> 2 -> sink(dirty_if_argument_nil([ok, ok, ok])) end. +%% Tests with message passing + +tito_process() -> + receive + {From, X} -> From ! X + end. + +sanitizer_process() -> + receive + {From, _} -> From ! not_dirty + end. + +test_send1_Ok() -> + Pid = spawn(topl_taint, tito_process, []), + Pid ! {self(), not_dirty}, + receive + X -> sink(X) + end. + +test_send2_Bad() -> + Pid = spawn(topl_taint, tito_process, []), + Pid ! {self(), source()}, + receive + X -> sink(X) + end. + +test_send3_Ok() -> + Pid = spawn(topl_taint, sanitizer_process, []), + Pid ! {self(), not_dirty}, + receive + X -> sink(X) + end. + +fp_test_send4_Ok() -> + Pid = spawn(topl_taint, sanitizer_process, []), + Pid ! {self(), source()}, + receive + X -> sink(X) + end. + +test_send5_Ok() -> + Pid = spawn(fun() -> tito_process() end), + Pid ! {self(), not_dirty}, + receive + X -> sink(X) + end. + +test_send6_Bad() -> + Pid = spawn(fun() -> tito_process() end), + Pid ! {self(), source()}, + receive + X -> sink(X) + end. + +test_send7_Ok() -> + Pid = spawn(fun() -> sanitizer_process() end), + Pid ! {self(), not_dirty}, + receive + X -> sink(X) + end. + +fp_test_send8_Ok() -> + Pid = spawn(fun() -> sanitizer_process() end), + Pid ! {self(), source()}, + receive + X -> sink(X) + end. + %% % tito = Taint-In Taint-Out From 56131c4e7ee055da84f1bb2b99af972ebdf78752 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Thu, 23 Feb 2023 03:09:31 -0800 Subject: [PATCH 16/25] [ios] Adding a model of the viewcontroller lifecycle Summary: According to the [Apple doc](https://developer.apple.com/documentation/uikit/uiviewcontroller?language=objc) > When the visibility of its views changes, a view controller automatically calls its own methods so that subclasses can respond to the change. Use a method like viewWillAppear: to prepare your views to appear onscreen, and use the viewWillDisappear: to save changes or other state information. Use other methods to make appropriate changes. So far Infer doesn't understand that these methods are called at all, and this leads to bugs being missed. This diff is an attempt to add a call to these methods after view controllers are created. Differential Revision: D42502082 fbshipit-source-id: b398f3d60b207f91db8e81aac17538ee376c16f7 --- infer/src/clang/CViewControllerLifecycle.ml | 82 ++++++++++++++++++ infer/src/clang/CViewControllerLifecycle.mli | 10 +++ infer/src/clang/cFrontend.ml | 1 + .../tests/codetoanalyze/objc/pulse/issues.exp | 1 + .../objc/pulse/null_deref/ControllerTest.m | 85 +++++++++++++++++++ 5 files changed, 179 insertions(+) create mode 100644 infer/src/clang/CViewControllerLifecycle.ml create mode 100644 infer/src/clang/CViewControllerLifecycle.mli create mode 100644 infer/tests/codetoanalyze/objc/pulse/null_deref/ControllerTest.m diff --git a/infer/src/clang/CViewControllerLifecycle.ml b/infer/src/clang/CViewControllerLifecycle.ml new file mode 100644 index 00000000000..1a3b288a953 --- /dev/null +++ b/infer/src/clang/CViewControllerLifecycle.ml @@ -0,0 +1,82 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +let is_view_controller tenv cls = + let uiviewcontroller = Typ.Name.Objc.from_string "UIViewController" in + let cls_name = Typ.Name.Objc.from_string cls in + PatternMatch.is_subtype tenv cls_name uiviewcontroller + && not (Typ.Name.equal cls_name uiviewcontroller) + + +let lifecycle_methods = + [ ("loadView", `NoArg) + ; ("viewDidLoad", `NoArg) + ; ("viewWillLayoutSubviews", `NoArg) + ; ("viewDidLayoutSubviews", `NoArg) + ; ("viewWillAppear:", `AnimatedArg) + ; ("viewDidAppear:", `AnimatedArg) + ; ("viewWillDisappear:", `AnimatedArg) + ; ("viewDidDisappear:", `AnimatedArg) ] + + +let is_overriden tenv cls (method_name, arg) = + match Tenv.lookup tenv cls with + | Some s -> + List.find_map s.Struct.methods ~f:(fun m -> + if String.equal (Procname.get_method m) method_name then Some (m, arg) else None ) + | None -> + None + + +let build_view_controller_methods tenv cls loc controller_arg = + let call_flags = {CallFlags.default with cf_virtual= true} in + let to_args param = + match param with + | `NoArg -> + [] + | `AnimatedArg -> + [(Exp.one, {Typ.desc= Typ.Tint IBool; Typ.quals= Typ.mk_type_quals ()})] + in + let build_view_controller_method (procname, params) instrs = + let ret_id = CTrans_utils.mk_fresh_void_id_typ () in + let args = controller_arg :: to_args params in + let instr = Sil.Call (ret_id, Const (Cfun procname), args, loc, call_flags) in + instr :: instrs + in + let overriden_methods = List.filter_map ~f:(is_overriden tenv cls) lifecycle_methods in + List.fold_right ~f:build_view_controller_method ~init:[] overriden_methods + + +let replace_calls tenv _ proc_desc = + let add_calls node _ instr = + let instrs = ProcCfg.Exceptional.instrs node in + Ident.update_name_generator (Instrs.instrs_get_normal_vars instrs) ; + let instrs = + match (instr : Sil.instr) with + | Call ((ret_id, ret_typ), Const (Cfun callee), _, loc, _) when Procname.is_objc_init callee + -> ( + match Procname.get_objc_class_name callee with + | Some cls when is_view_controller tenv cls -> + let cls_name = Typ.Name.Objc.from_string cls in + instr :: build_view_controller_methods tenv cls_name loc (Var ret_id, ret_typ) + | _ -> + [instr] ) + | _ -> + [instr] + in + Array.of_list instrs + in + let update_context () _ = () in + let context_at_node _ = () in + ignore + (Procdesc.replace_instrs_by_using_context proc_desc ~f:add_calls ~update_context + ~context_at_node ) + + +let process cfg tenv = Procname.Hash.iter (replace_calls tenv) cfg diff --git a/infer/src/clang/CViewControllerLifecycle.mli b/infer/src/clang/CViewControllerLifecycle.mli new file mode 100644 index 00000000000..4bd4e449137 --- /dev/null +++ b/infer/src/clang/CViewControllerLifecycle.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +val process : Cfg.t -> Tenv.t -> unit diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index 1a11f487fac..4c943298ecd 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -53,6 +53,7 @@ let do_source_file (translation_unit_context : CFrontend_config.translation_unit CAddImplicitDeallocImpl.process cfg tenv ; CAddImplicitGettersSetters.process cfg tenv ; CReplaceDynamicDispatch.process cfg ; + CViewControllerLifecycle.process cfg tenv ; L.(debug Capture Verbose) "@\n End building call/cfg graph for '%a'.@\n" SourceFile.pp source_file ; SourceFiles.add source_file cfg (Tenv.FileLocal tenv) (Some integer_type_widths) ; if Config.debug_mode then Tenv.store_debug_file_for_source source_file tenv ; diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index 297af17557d..c7ca10284d9 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -13,6 +13,7 @@ codetoanalyze/objc/pulse/null_deref/BlockVar.m, BlockVar.callBlockNPEBad, 7, NUL codetoanalyze/objc/pulse/null_deref/BlockVar.m, BlockVar.blockPostNullDerefBad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,in call to `objc_blockBlockVar.blockPostNullDerefBad_2`,value captured by value as `x`,returned,return from call to `objc_blockBlockVar.blockPostNullDerefBad_2`,invalid access occurs here] codetoanalyze/objc/pulse/null_deref/BlockVar.m, BlockVar.capturedNullDerefBad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,when calling `objc_blockBlockVar.capturedNullDerefBad_4` here,value captured by value as `x`,invalid access occurs here] codetoanalyze/objc/pulse/null_deref/Blocks_as_parameter.m, call_f_npe_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `B.f`,parameter `self` of B.f,in call to `B.call_block:[specialized with blocks][specialized with aliases]`,value captured by value as `self`,in call to `objc_blockB.f_1`,is assigned to the constant 5,assigned,return from call to `objc_blockB.f_1`,return from call to `B.call_block:[specialized with blocks][specialized with aliases]`,returned,return from call to `B.f`,assigned,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here] +codetoanalyze/objc/pulse/null_deref/ControllerTest.m, build_view_controller_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `alloc` (modelled),in call to `ViewController.viewDidLoad`,is assigned to the null pointer,assigned,return from call to `ViewController.viewDidLoad`,in call to `ViewController.a`,parameter `self` of ViewController.a,returned,return from call to `ViewController.a`,assigned,invalid access occurs here] codetoanalyze/objc/pulse/null_deref/FrontendCategoryPerson.m, categoryMethodsOkIsChildNPEBad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `CategoryPerson.isChild`,parameter `self` of CategoryPerson.isChild,taking "then" branch,is assigned to the constant 1,returned,return from call to `CategoryPerson.isChild`,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here] codetoanalyze/objc/pulse/null_deref/FrontendEqualNames.m, EqualNamesInstanceNPEBad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `EqualNamesA.meth`,is assigned to the null pointer,returned,return from call to `EqualNamesA.meth`,assigned,invalid access occurs here] codetoanalyze/objc/pulse/null_deref/FrontendExplicitIvarName.m, ExplicitIvarNameA.testExplicit, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/objc/pulse/null_deref/ControllerTest.m b/infer/tests/codetoanalyze/objc/pulse/null_deref/ControllerTest.m new file mode 100644 index 00000000000..f8909f48c74 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/pulse/null_deref/ControllerTest.m @@ -0,0 +1,85 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#import + +@interface AValue : NSObject +@end + +@implementation AValue { + @public + int* n; +} + +@end + +@interface ViewController : UIViewController + +@property(nonatomic, copy) AValue* a; + +- (instancetype)initWithAValue:(AValue*)a; + +@end + +@implementation ViewController + +- (instancetype)initWithAValue:(AValue*)a { + if (self = [super initWithNibName:nil bundle:nil]) { + _a = a; + } + return self; +} + +- (void)viewDidLoad { + self->_a = nil; +} + +@end + +@interface ViewController2 : UIViewController + +@property(nonatomic, copy) AValue* a; + +- (instancetype)initWithAValue:(AValue*)a; + +@end + +@implementation ViewController2 + +- (instancetype)initWithAValue:(AValue*)a { + if (self = [super initWithNibName:nil bundle:nil]) { + _a = a; + } + return self; +} + +- (void)viewDidLoad { + self->_a = nil; +} + +- (void)viewDidDisappear:(BOOL)b { + if (b) { + self->_a = [AValue new]; + } else { + [super viewDidDisappear:b]; + } +} + +@end + +int build_view_controller_bad() { + AValue* a = [AValue new]; + ViewController* controller = [[ViewController alloc] initWithAValue:a]; + AValue* controller_a = controller.a; + return controller_a->n; +} + +int build_view_controller2_good() { + AValue* a = [AValue new]; + ViewController2* controller = [[ViewController2 alloc] initWithAValue:a]; + AValue* controller_a = controller.a; + return controller_a->n; +} From b5eb60cfefd41e0fe21fb0577ba738d1a3625ef9 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 23 Feb 2023 03:36:17 -0800 Subject: [PATCH 17/25] [pulse] Fix a bug in calculating captured actuals in closure call Summary: This diff fixes a bug in binding captured values to corresponding variables in closure calls. - From procedure attributes, it constructs `captured_formals`. - Using the `captured_formals`, it constructs `captured_actuals`. - Then, actual binding is done with `captured_formals` and `captured_actuals`. A problem was that when the callee is a closure, it sometimes constructs `captured_actuals` the order of which is different to `captured_formals`. The mismatch is coming from: - `captured_formals` are made in the order of fieldnames, https://github.com/facebook/infer/blob/main/infer/src/absint/ClosureSpecialization.ml#L59 * `captured_actuals` are made in the order of edges, https://github.com/facebook/infer/blob/main/infer/src/pulse/PulseClosureSpecialization.ml#L208 To avoid the mismatch, this diff changes the type of `passed_closure` (which is the source of `captured_formals`) from a map to an assoc list, then makes sure that it is constructed with the same order with `captured_actuals`, i.e. the order of edges by `BaseMemory.Edges.fold`. Reviewed By: ezgicicek, dulmarod Differential Revision: D43437889 fbshipit-source-id: 93029bd40cdb56e736c67ec38ecd1f4b40ab6974 --- infer/src/IR/ProcAttributes.ml | 7 ++-- infer/src/IR/ProcAttributes.mli | 2 +- infer/src/absint/ClosureSpecialization.ml | 11 +++--- .../backend/ClosureSubstSpecializedMethod.ml | 2 +- infer/src/pulse/PulseClosureSpecialization.ml | 36 +++++++------------ 5 files changed, 24 insertions(+), 34 deletions(-) diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml index 7d4190e7707..79048725f0d 100644 --- a/infer/src/IR/ProcAttributes.ml +++ b/infer/src/IR/ProcAttributes.ml @@ -57,7 +57,7 @@ type specialized_with_aliasing_info = {orig_proc: Procname.t; aliases: Pvar.t li type 'captured_var passed_closure = | Closure of (Procname.t * 'captured_var list) - | Fields of 'captured_var passed_closure Fieldname.Map.t + | Fields of (Fieldname.t * 'captured_var passed_closure) list [@@deriving compare, equal] type specialized_with_closures_info = @@ -203,7 +203,10 @@ let pp_specialized_with_closures_info fmt info = let pp_captured_vars = Pp.semicolon_seq ~print_env:Pp.text_break CapturedVar.pp in Pp.pair ~fst:Procname.pp ~snd:pp_captured_vars fmt closure | Fields field_to_function_map -> - Fieldname.Map.pp ~pp_value:pp_passed_closure fmt field_to_function_map + PrettyPrintable.pp_collection + ~pp_item:(fun fmt (fld, func) -> + F.fprintf fmt "%a->%a" Fieldname.pp fld pp_passed_closure func ) + fmt field_to_function_map in F.fprintf fmt "orig_procname=%a, formals_to_closures=%a" Procname.pp info.orig_proc (Pvar.Map.pp ~pp_value:pp_passed_closure) diff --git a/infer/src/IR/ProcAttributes.mli b/infer/src/IR/ProcAttributes.mli index 10a87f15387..c1236d322c9 100644 --- a/infer/src/IR/ProcAttributes.mli +++ b/infer/src/IR/ProcAttributes.mli @@ -35,7 +35,7 @@ type specialized_with_aliasing_info = type 'captured_var passed_closure = | Closure of (Procname.t * 'captured_var list) - | Fields of 'captured_var passed_closure Fieldname.Map.t + | Fields of (Fieldname.t * 'captured_var passed_closure) list [@@deriving compare, equal] type specialized_with_closures_info = diff --git a/infer/src/absint/ClosureSpecialization.ml b/infer/src/absint/ClosureSpecialization.ml index 1df57221376..c8889653329 100644 --- a/infer/src/absint/ClosureSpecialization.ml +++ b/infer/src/absint/ClosureSpecialization.ml @@ -16,9 +16,8 @@ let pname_with_closure_actuals callee_pname formals_to_closures = | ProcAttributes.Closure (pname, _) when Procname.is_objc_block pname || Procname.is_c pname -> Procname.to_function_parameter pname :: acc | ProcAttributes.Fields passed_closures -> - Fieldname.Map.fold - (fun _ passed_closure acc -> get_function_parameters acc passed_closure) - passed_closures acc + List.fold_right passed_closures ~init:acc ~f:(fun (_, passed_closure) acc -> + get_function_parameters acc passed_closure ) | _ -> acc in @@ -56,9 +55,9 @@ let rec get_captured_in_passed_closure captured_vars_acc = function | ProcAttributes.Closure (_, captured_vars) -> captured_vars :: captured_vars_acc | ProcAttributes.Fields passed_closures -> - Fieldname.Map.fold - (fun _ actual captured_vars_acc -> get_captured_in_passed_closure captured_vars_acc actual) - passed_closures captured_vars_acc + List.fold_right passed_closures ~init:captured_vars_acc + ~f:(fun (_, actual) captured_vars_acc -> + get_captured_in_passed_closure captured_vars_acc actual ) let get_captured actuals = diff --git a/infer/src/backend/ClosureSubstSpecializedMethod.ml b/infer/src/backend/ClosureSubstSpecializedMethod.ml index 64a394f96ab..1efe289d385 100644 --- a/infer/src/backend/ClosureSubstSpecializedMethod.ml +++ b/infer/src/backend/ClosureSubstSpecializedMethod.ml @@ -45,7 +45,7 @@ let rec get_closure (id_to_closure_map, pvar_to_closure_map) exp = >>= SpecDom.get >>= function | ProcAttributes.Fields field_to_passed_closure_map -> - Fieldname.Map.find_opt fieldname field_to_passed_closure_map >>| SpecDom.v + List.Assoc.find field_to_passed_closure_map ~equal:Fieldname.equal fieldname >>| SpecDom.v | _ -> None ) | _ -> diff --git a/infer/src/pulse/PulseClosureSpecialization.ml b/infer/src/pulse/PulseClosureSpecialization.ml index f430e89cc0b..6d79810bf18 100644 --- a/infer/src/pulse/PulseClosureSpecialization.ml +++ b/infer/src/pulse/PulseClosureSpecialization.ml @@ -211,14 +211,10 @@ let actuals_of_func analysis_data func_actuals caller_values_to_closures astate match actual_of accessed_value seen with | Some passed_closure -> ( match res with - | Some (ProcAttributes.Fields map) -> - Some - (ProcAttributes.Fields - (Fieldname.Map.add fieldname passed_closure map) ) + | Some (ProcAttributes.Fields closures) -> + Some (ProcAttributes.Fields ((fieldname, passed_closure) :: closures)) | _ -> - Some - (ProcAttributes.Fields - (Fieldname.Map.singleton fieldname passed_closure) ) ) + Some (ProcAttributes.Fields [(fieldname, passed_closure)]) ) | None -> res ) | Dereference when Option.is_none res -> @@ -287,8 +283,8 @@ let deep_formals_to_closures_of_captured_vars ({InterproceduralAnalysis.proc_des dftb_and_passed_closure_of_closure (pname, captured) map astate seen | Fields passed_closures -> let astate, map, fields = - Fieldname.Map.fold - (fun fieldname passed_closure (astate, map, fields) -> + List.fold_right passed_closures ~init:(astate, map, Some []) + ~f:(fun (fieldname, passed_closure) (astate, map, fields) -> match fields with | None -> (astate, map, None) @@ -297,10 +293,8 @@ let deep_formals_to_closures_of_captured_vars ({InterproceduralAnalysis.proc_des | _, _, None -> (astate, map, None) | astate, map, Some passed_closure -> - let fields = Fieldname.Map.add fieldname passed_closure fields in + let fields = (fieldname, passed_closure) :: fields in (astate, map, Some fields) ) ) - passed_closures - (astate, map, Some Fieldname.Map.empty) in let fields = Option.map fields ~f:(fun fields -> Fields fields) in (astate, map, fields) @@ -334,17 +328,12 @@ let deep_formals_to_closures_of_captured_vars ({InterproceduralAnalysis.proc_des | astate, map, Some passed_closure -> ( match res with | None -> - ( astate - , map - , Some - (ProcAttributes.Fields - (Fieldname.Map.singleton fieldname passed_closure) ) ) + (astate, map, Some (ProcAttributes.Fields [(fieldname, passed_closure)])) | Some (ProcAttributes.Fields fields) -> ( astate , map - , Some - (ProcAttributes.Fields - (Fieldname.Map.add fieldname passed_closure fields) ) ) + , Some (ProcAttributes.Fields ((fieldname, passed_closure) :: fields)) + ) | Some _ -> (astate, map, res) ) ) | Dereference -> ( @@ -434,10 +423,9 @@ let prepend_deep_captured_vars deep_formals_to_closures captured_vars = | ProcAttributes.Closure (_, captured_vars) -> captured_vars :: captured_vars_acc | ProcAttributes.Fields passed_closures -> - Fieldname.Map.fold - (fun _ actual captured_vars_acc -> + List.fold_right passed_closures ~init:captured_vars_acc + ~f:(fun (_, actual) captured_vars_acc -> get_captured_vars_in_passed_closure captured_vars_acc actual ) - passed_closures captured_vars_acc in Pvar.Map.fold (fun _ actual captured_vars -> get_captured_vars_in_passed_closure captured_vars actual) @@ -481,7 +469,7 @@ let make_specialized_call_exp analysis_data func_args callee_pname call_kind pat , List.map captured_vars ~f:(fun (_, pvar, typ, capture_mode) -> CapturedVar.{pvar; typ; capture_mode} ) ) | ProcAttributes.Fields fields -> - ProcAttributes.Fields (Fieldname.Map.map convert fields) + ProcAttributes.Fields (List.map fields ~f:(fun (fld, v) -> (fld, convert v))) in Pvar.Map.map convert deep_formals_to_closures in From a54821f16bed3cca763ef8c43c4f70cb17a02430 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=3D=3FUTF-8=3Fq=3FEzgi=3D20=3DC3=3D87i=3DC3=3DA7ek=3F=3D?= Date: Thu, 23 Feb 2023 06:07:50 -0800 Subject: [PATCH 18/25] [pulse] Enable mature unnecessary copy issues by default Summary: Let's enable mature unnecessary copy issues by default. Reviewed By: skcho Differential Revision: D43462031 fbshipit-source-id: 05cea14ba7c6f0e9b9fd782928459408b05ad196 --- infer/man/man1/infer-full.txt | 11 +++++------ infer/man/man1/infer-report.txt | 11 +++++------ infer/man/man1/infer.txt | 11 +++++------ infer/src/base/IssueType.ml | 13 +++++-------- 4 files changed, 20 insertions(+), 26 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index f010d745210..ecf760b56ae 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -623,19 +623,18 @@ OPTIONS PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), PULSE_CONST_REFABLE (disabled by default), - PULSE_READONLY_SHARED_PTR_PARAM (disabled by default), + PULSE_READONLY_SHARED_PTR_PARAM (enabled by default), PULSE_RESOURCE_LEAK (enabled by default), PULSE_UNINITIALIZED_VALUE (enabled by default), PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default), - PULSE_UNNECESSARY_COPY (disabled by default), - PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default), + PULSE_UNNECESSARY_COPY (enabled by default), + PULSE_UNNECESSARY_COPY_ASSIGNMENT (enabled by default), PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST (disabled by default), - PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by - default), + PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (enabled by default), PULSE_UNNECESSARY_COPY_INTERMEDIATE (disabled by default), PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by default), - PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default), + PULSE_UNNECESSARY_COPY_MOVABLE (enabled by default), PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default), PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default), PULSE_UNNECESSARY_COPY_RETURN (disabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 887e384db4b..750d2537628 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -265,19 +265,18 @@ OPTIONS PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), PULSE_CONST_REFABLE (disabled by default), - PULSE_READONLY_SHARED_PTR_PARAM (disabled by default), + PULSE_READONLY_SHARED_PTR_PARAM (enabled by default), PULSE_RESOURCE_LEAK (enabled by default), PULSE_UNINITIALIZED_VALUE (enabled by default), PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default), - PULSE_UNNECESSARY_COPY (disabled by default), - PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default), + PULSE_UNNECESSARY_COPY (enabled by default), + PULSE_UNNECESSARY_COPY_ASSIGNMENT (enabled by default), PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST (disabled by default), - PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by - default), + PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (enabled by default), PULSE_UNNECESSARY_COPY_INTERMEDIATE (disabled by default), PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by default), - PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default), + PULSE_UNNECESSARY_COPY_MOVABLE (enabled by default), PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default), PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default), PULSE_UNNECESSARY_COPY_RETURN (disabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 340ad0325d0..0a3022fbbef 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -623,19 +623,18 @@ OPTIONS PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), PULSE_CONST_REFABLE (disabled by default), - PULSE_READONLY_SHARED_PTR_PARAM (disabled by default), + PULSE_READONLY_SHARED_PTR_PARAM (enabled by default), PULSE_RESOURCE_LEAK (enabled by default), PULSE_UNINITIALIZED_VALUE (enabled by default), PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default), - PULSE_UNNECESSARY_COPY (disabled by default), - PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default), + PULSE_UNNECESSARY_COPY (enabled by default), + PULSE_UNNECESSARY_COPY_ASSIGNMENT (enabled by default), PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST (disabled by default), - PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by - default), + PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (enabled by default), PULSE_UNNECESSARY_COPY_INTERMEDIATE (disabled by default), PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by default), - PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default), + PULSE_UNNECESSARY_COPY_MOVABLE (enabled by default), PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default), PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default), PULSE_UNNECESSARY_COPY_RETURN (disabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 515339b0b27..a367c3fe448 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -946,8 +946,7 @@ let quandary_taint_error = let readonly_shared_ptr_param = - register ~enabled:false ~id:"PULSE_READONLY_SHARED_PTR_PARAM" Error Pulse - ~hum:"Read-only Shared Parameter" + register ~id:"PULSE_READONLY_SHARED_PTR_PARAM" Error Pulse ~hum:"Read-only Shared Parameter" ~user_documentation:[%blob "./documentation/issues/PULSE_READONLY_SHARED_PTR_PARAM.md"] @@ -1075,13 +1074,12 @@ let uninitialized_value_pulse = let unnecessary_copy_pulse = - register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY" Error Pulse ~hum:"Unnecessary Copy" + register ~id:"PULSE_UNNECESSARY_COPY" Error Pulse ~hum:"Unnecessary Copy" ~user_documentation:[%blob "./documentation/issues/PULSE_UNNECESSARY_COPY.md"] let unnecessary_copy_assignment_pulse = - register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY_ASSIGNMENT" Error Pulse - ~hum:"Unnecessary Copy Assignment" + register ~id:"PULSE_UNNECESSARY_COPY_ASSIGNMENT" Error Pulse ~hum:"Unnecessary Copy Assignment" ~user_documentation:"See [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy)." @@ -1092,7 +1090,7 @@ let unnecessary_copy_assignment_const_pulse = let unnecessary_copy_assignment_movable_pulse = - register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE" Error Pulse + register ~id:"PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE" Error Pulse ~hum:"Unnecessary Copy Assignment Movable" ~user_documentation:"See [PULSE_UNNECESSARY_COPY_MOVABLE](#pulse_unnecessary_copy_movable)." @@ -1110,8 +1108,7 @@ let unnecessary_copy_intermediate_const_pulse = let unnecessary_copy_movable_pulse = - register ~enabled:false ~id:"PULSE_UNNECESSARY_COPY_MOVABLE" Error Pulse - ~hum:"Unnecessary Copy Movable" + register ~id:"PULSE_UNNECESSARY_COPY_MOVABLE" Error Pulse ~hum:"Unnecessary Copy Movable" ~user_documentation:[%blob "./documentation/issues/PULSE_UNNECESSARY_COPY_MOVABLE.md"] From aa258a890b53ba1b5965f92face2959b9a65bab5 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 23 Feb 2023 07:46:25 -0800 Subject: [PATCH 19/25] [make] no pretty colours for dumb terminals Summary: Emacs sets `TERM=dumb`, recognise this and suppress colour codes to avoid garbage in the emacs compilation buffer. Reviewed By: bennostein Differential Revision: D43501188 fbshipit-source-id: c0333cc19e8be7442b572b0b46131455bb449988 --- Makefile.config | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.config b/Makefile.config index 85f664262b3..f88507bd5e0 100644 --- a/Makefile.config +++ b/Makefile.config @@ -119,7 +119,7 @@ define copy_or_same_file $(COPY) "$(1)" "$(2)" || diff -q "$(1)" "$(2)" endef -INTERACTIVE := $(shell [ -t 0 ] && echo 1) +INTERACTIVE := $(shell [ -t 0 ] && ! [ x"$$TERM" = xdumb ] && echo 1) SILENT := $(findstring s,$(filter-out -%,$(firstword $(MAKEFLAGS)))) ifeq (1,$(INTERACTIVE)) From d201cc403832d9e2413d44ec65abb795c62a9702 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 23 Feb 2023 07:46:28 -0800 Subject: [PATCH 20/25] [pulse][minor] debug print (empty) for empty formulas Summary: instead of `conditions: (empty) formula: ` print `conditions: (empty) formula: (empty)` in the html debug when the formula is empty. Reviewed By: skcho Differential Revision: D43501258 fbshipit-source-id: 9477864820c39d74c60f8d71109577cca9f21a10 --- infer/src/pulse/PulseFormula.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 2a0a1befca5..9a0c93eca19 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -1666,15 +1666,23 @@ module Formula = struct ; atoms= Atom.Set.empty } - let pp_with_pp_var pp_var fmt + let is_empty ({var_eqs; linear_eqs; term_eqs; tableau; intervals; atoms} [@warning "+missing-record-field-pattern"] ) = + VarUF.is_empty var_eqs && Var.Map.is_empty linear_eqs && Term.VarMap.is_empty term_eqs + && Var.Map.is_empty tableau && Var.Map.is_empty intervals && Atom.Set.is_empty atoms + + + let pp_with_pp_var pp_var fmt + ( ({var_eqs; linear_eqs; term_eqs; tableau; intervals; atoms} + [@warning "+missing-record-field-pattern"] ) as phi ) = let is_first = ref true in let pp_if condition header pp fmt x = let pp_and fmt = if not !is_first then F.fprintf fmt "@;&& " else is_first := false in if condition then F.fprintf fmt "%t%s: %a" pp_and header pp x in F.pp_open_hvbox fmt 0 ; + if is_empty phi then F.pp_print_string fmt "(empty)" ; (pp_if (not (VarUF.is_empty var_eqs)) "var_eqs" (VarUF.pp pp_var)) fmt var_eqs ; (pp_if (not (Var.Map.is_empty linear_eqs)) From dbfb1591f73e09fee3d5e3909e62c6e96b3953d9 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Thu, 23 Feb 2023 09:30:48 -0800 Subject: [PATCH 21/25] Replace procdescs by procattrs where possible in checkers Summary: Procdescs are sometimes loaded from disk or passed around when only some attribute(s) are needed. This diff changes some of those to use lighter-weight structures (but is by no means exhaustive) Reviewed By: jvillard Differential Revision: D43539696 fbshipit-source-id: 09e5d49b5a4df0ff9ccae9d672e75b45a30b4184 --- infer/src/biabduction/SymExec.ml | 15 +++++++-------- infer/src/pulse/PulseNonDisjunctiveOperations.ml | 2 +- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index e6024c11c95..c5881c8d288 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -510,7 +510,7 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t (** Resolve the name of the procedure to call based on the type of the arguments *) -let resolve_pname ~caller_pdesc tenv prop args pname call_flags : Procname.t = +let resolve_pname ~caller_loc tenv prop args pname call_flags : Procname.t = let resolve_from_args resolved_pname args = let resolved_parameters = Procname.get_parameters resolved_pname in let resolved_params = @@ -525,12 +525,11 @@ let resolve_pname ~caller_pdesc tenv prop args pname call_flags : Procname.t = ~init:[] args resolved_parameters |> List.rev with Invalid_argument _ -> - let loc = (Procdesc.get_attributes caller_pdesc).loc in - let file = loc.Location.file in + let file = caller_loc.Location.file in L.(debug Analysis Medium) "Call mismatch: method %a has %i paramters but is called with %i arguments, in %a, %a@." Procname.pp pname (List.length resolved_parameters) (List.length args) SourceFile.pp file - Location.pp loc ; + Location.pp caller_loc ; raise SpecializeProcdesc.UnmatchedParameters in Procname.replace_parameters resolved_params resolved_pname @@ -557,12 +556,11 @@ let resolve_pname ~caller_pdesc tenv prop args pname call_flags : Procname.t = | args when match_parameters args (* Static call *) -> (pname, args) | args -> - let loc = (Procdesc.get_attributes caller_pdesc).loc in - let file = loc.Location.file in + let file = caller_loc.Location.file in L.(debug Analysis Medium) "Call mismatch: method %a has %i paramters but is called with %i arguments, in %a, %a@." Procname.pp pname (List.length parameters) (List.length args) SourceFile.pp file - Location.pp loc ; + Location.pp caller_loc ; raise SpecializeProcdesc.UnmatchedParameters in resolve_from_args resolved_pname other_args @@ -622,7 +620,8 @@ let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc; analyze_dependency resolved_pname ) ) in let resolved_pname = - resolve_pname ~caller_pdesc:proc_desc tenv prop args callee_proc_name call_flags + let caller_loc = Procdesc.get_loc proc_desc in + resolve_pname ~caller_loc tenv prop args callee_proc_name call_flags in let resolved_procdesc_opt, resolved_summary_opt = analyze_ondemand resolved_pname in {resolved_pname; resolved_procdesc_opt; resolved_summary_opt} diff --git a/infer/src/pulse/PulseNonDisjunctiveOperations.ml b/infer/src/pulse/PulseNonDisjunctiveOperations.ml index 331ffeb3f80..9cb741c92ed 100644 --- a/infer/src/pulse/PulseNonDisjunctiveOperations.ml +++ b/infer/src/pulse/PulseNonDisjunctiveOperations.ml @@ -345,7 +345,7 @@ let add_copied_return path location pname actuals (astate_n, astate) = let open IOption.Let_syntax in if is_lock pname then Some (NonDisjDomain.set_locked astate_n, astate) else if not (NonDisjDomain.is_locked astate_n) then - match (Option.map (Procdesc.load pname) ~f:Procdesc.get_attributes, List.last actuals) with + match (IRAttributes.load pname, List.last actuals) with | Some attrs, Some ((Exp.Lvar ret_pvar as ret), copy_type) when attrs.has_added_return_param -> let copied_var = Var.of_pvar ret_pvar in if is_copy_into_local copied_var then From fc5515fb73f7f3c1bd6bf7b24fac133a4e8b0962 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Thu, 23 Feb 2023 10:26:41 -0800 Subject: [PATCH 22/25] [nfc] change `let _` wildcards to `let ()` Summary: A wise man once said that "`let _` is evil" Reviewed By: jvillard Differential Revision: D43540326 fbshipit-source-id: 9ae829278dd90d557d483e65197acd5c25d08d18 --- infer/src/IR/Procdesc.ml | 24 ++++++++++++------------ infer/src/IR/Procdesc.mli | 2 ++ infer/src/backend/printer.ml | 2 +- infer/src/erlang/ErlangJsonParser.ml | 2 +- infer/src/integration/CaptureSILJson.ml | 10 ++++------ infer/src/istd/HashNormalizer.ml | 2 +- infer/src/java/jSourceAST.ml | 2 +- infer/src/pulse/PulseModelsCSharp.ml | 2 +- 8 files changed, 23 insertions(+), 23 deletions(-) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 2c3e9e26ae4..070ed682154 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -774,19 +774,19 @@ end module WTO = WeakTopologicalOrder.Bourdoncle_SCC (PreProcCfg) +let init_wto pdesc = + let wto = WTO.make pdesc in + let (_ : int) = + WeakTopologicalOrder.Partition.fold_nodes wto ~init:0 ~f:(fun idx node -> + node.Node.wto_index <- idx ; + idx + 1 ) + in + pdesc.wto <- Some wto + + let get_wto pdesc = - match pdesc.wto with - | Some wto -> - wto - | None -> - let wto = WTO.make pdesc in - let (_ : int) = - WeakTopologicalOrder.Partition.fold_nodes wto ~init:0 ~f:(fun idx node -> - node.Node.wto_index <- idx ; - idx + 1 ) - in - pdesc.wto <- Some wto ; - wto + if Option.is_none pdesc.wto then init_wto pdesc ; + Option.value_exn pdesc.wto (** Get loop heads for widening. It collects all target nodes of back-edges in a depth-first diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index b2d8fc7ef62..b630ebdaaae 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -344,6 +344,8 @@ val set_exit_node : t -> Node.t -> unit val set_start_node : t -> Node.t -> unit +val init_wto : t -> unit + val get_wto : t -> Node.t WeakTopologicalOrder.Partition.t val is_loop_head : t -> Node.t -> bool diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 92a4de14f79..836218e2729 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -175,7 +175,7 @@ end = struct let process_proc table_nodes_at_linenum global_err_log proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in - let _ = (* Initializes wto_indexes *) Procdesc.get_wto proc_desc in + Procdesc.init_wto proc_desc ; let process_node n = let lnum = (Procdesc.Node.get_loc n).Location.line in let curr_nodes = try Hashtbl.find table_nodes_at_linenum lnum with Caml.Not_found -> [] in diff --git a/infer/src/erlang/ErlangJsonParser.ml b/infer/src/erlang/ErlangJsonParser.ml index 688bd1b8169..ec5ca478eda 100644 --- a/infer/src/erlang/ErlangJsonParser.ml +++ b/infer/src/erlang/ErlangJsonParser.ml @@ -639,7 +639,7 @@ let rec to_type json : Ast.type_ option = Some (Ast.Var name) (* TODO: add more types *) | _ -> - let _ = unknown "type" json in + unknown "type" json |> ignore ; Some Ast.Unsupported diff --git a/infer/src/integration/CaptureSILJson.ml b/infer/src/integration/CaptureSILJson.ml index 9c2111cec18..fac2fbd5fa8 100644 --- a/infer/src/integration/CaptureSILJson.ml +++ b/infer/src/integration/CaptureSILJson.ml @@ -661,12 +661,10 @@ let parse_cfg (json : Safe.t) = List.iter ~f:(fun (_, pdjson) -> parse_pdesc cfg pd_id_to_pd pd_id_to_start_node pd_id_to_exit_node pdjson) (to_assoc (member "procs" json)) ; - let _ = - parse_list - (parse_node pd_id_to_pd nd_id_to_node nd_id_to_exn_nodes nd_id_to_pred_nodes - nd_id_to_succ_nodes ) - (member "nodes" json) - in + parse_list + (parse_node pd_id_to_pd nd_id_to_node nd_id_to_exn_nodes nd_id_to_pred_nodes nd_id_to_succ_nodes) + (member "nodes" json) + |> ignore ; (* Now fix up the dangling ends *) IntTbl.iter (fun pd_id pd -> diff --git a/infer/src/istd/HashNormalizer.ml b/infer/src/istd/HashNormalizer.ml index cc35d1ba32e..068bd4f6d05 100644 --- a/infer/src/istd/HashNormalizer.ml +++ b/infer/src/istd/HashNormalizer.ml @@ -27,7 +27,7 @@ module Make (T : NormalizedT) = struct let table : t H.t = H.create 11 - let _ = normalizer_reset_funs := (fun () -> H.reset table) :: !normalizer_reset_funs + let () = normalizer_reset_funs := (fun () -> H.reset table) :: !normalizer_reset_funs let normalize t = match H.find_opt table t with diff --git a/infer/src/java/jSourceAST.ml b/infer/src/java/jSourceAST.ml index af17fc28ff6..d618ca061cf 100644 --- a/infer/src/java/jSourceAST.ml +++ b/infer/src/java/jSourceAST.ml @@ -33,7 +33,7 @@ let rec iter ~action_on_class_location context {location; kind; inner_elements} let classname = previous_prefix ^ name in let col = location.col in let line = location.line in - let _ = action_on_class_location ~classname ~col ~line in + action_on_class_location ~classname ~col ~line ; List.iter inner_elements ~f:(iter ~action_on_class_location context) diff --git a/infer/src/pulse/PulseModelsCSharp.ml b/infer/src/pulse/PulseModelsCSharp.ml index 5bd9bcb07e0..4d2ee1ae776 100644 --- a/infer/src/pulse/PulseModelsCSharp.ml +++ b/infer/src/pulse/PulseModelsCSharp.ml @@ -424,7 +424,7 @@ module Resource = struct (arg_payload, typ) ) in let callee_data = analyze_dependency callee_procname in - (* let _ = Printf.printf "analysis occurs here. Found callee_data for %s? : %b \n" *) + (* let () = Printf.printf "analysis occurs here. Found callee_data for %s? : %b \n" *) (* (Procname.to_string callee_procname) (Option.is_some callee_data) *) (* in *) match callee_data with From fc6f72e3505365d8fdf551fd35bad2d62ba0267e Mon Sep 17 00:00:00 2001 From: Thibault Suzanne Date: Thu, 23 Feb 2023 11:12:22 -0800 Subject: [PATCH 23/25] First step of interprocedural Lineage: support structured function arguments Summary: When a function argument is known to be a structure (from the analysis of that function), upon callin the function with concrete arguments, we only derive flow from the components of these arguments that are known to flow into the result, instead of the whole concrete argument. For instance, upon calling a `fst` function that returns the first element of a tuple as `Y = fst(X)`, only `X#1` flows into `Y`. The generation of the graph will still involve one `fst/1:arg0` node (the fields are not splitted), only the `Derive` edges will be more carefully generated. Reviewed By: rgrig Differential Revision: D42998266 fbshipit-source-id: 64324cfb9e4a183bfc4bd7f875df48b5caab6570 --- infer/src/checkers/SimpleLineage.ml | 179 ++++++++++++++++++++-------- 1 file changed, 132 insertions(+), 47 deletions(-) diff --git a/infer/src/checkers/SimpleLineage.ml b/infer/src/checkers/SimpleLineage.ml index e460809fdd4..d3081c1a4ea 100644 --- a/infer/src/checkers/SimpleLineage.ml +++ b/infer/src/checkers/SimpleLineage.ml @@ -20,6 +20,10 @@ module PPNode = struct end module Fields = struct + (** A module to help manipulating lists of (nested) fields. *) + + (* The list is to be understood in "syntactic order": [["a"; "b"]] represents the field part of + [X#a#b].*) type t = Fieldname.t list [@@deriving compare, equal, sexp] let pp = Fmt.(list ~sep:nop (any "#" ++ Fieldname.pp)) @@ -44,8 +48,13 @@ module VariableIndex : sig val var : Var.t -> transient t + val subfield : _ t -> Fields.t -> transient t + (** Sub-field of an index. *) + val get_var : _ t -> Var.t + val get_fields : terminal t -> Fields.t + val make : Var.t -> Fields.t -> transient t val pvar : Pvar.t -> transient t @@ -88,16 +97,18 @@ end = struct type transient - type _ t = Var.t * Fields.t - (* The field list is in syntactic order: x#a#b is represented as (x, [a, b]) *) - [@@deriving compare, equal] + type _ t = Var.t * Fields.t [@@deriving compare, equal] let var v = (v, []) + let subfield (var, fields) subfields = (var, fields @ subfields) + let make var fields = (var, fields) let get_var (v, _) = v + let get_fields (_, fields) = fields + let pvar pvar = var (Var.of_pvar pvar) let ident id = var (Var.of_id id) @@ -153,7 +164,7 @@ module LineageGraph = struct type data = | Local of ((local * PPNode.t)[@sexp.opaque]) - | Argument of int + | Argument of int * Fields.t | ArgumentOf of int * (Procname.t[@sexp.opaque]) | Captured of int | CapturedBy of int * (Procname.t[@sexp.opaque]) @@ -218,8 +229,8 @@ module LineageGraph = struct match data with | Local (local, node) -> Format.fprintf fmt "%a@@%a" pp_local local PPNode.pp node - | Argument index -> - Format.fprintf fmt "arg%d" index + | Argument (index, fields) -> + Format.fprintf fmt "arg%d%a" index Fields.pp fields | Captured index -> Format.fprintf fmt "cap%d" index | Return -> @@ -424,8 +435,12 @@ module LineageGraph = struct type state_local = Start of Location.t | Exit of Location.t | Normal of PPNode.t - (** Like [LineageGraph.data], but without the ability to refer to other procedures, which makes - it "local". *) + (** Like [LineageGraph.data], but : + + - Without the ability to refer to other procedures, which makes it "local". + - With some information lost/summarised, such as fields of procedure arguments (although the + Derive edges will be generated taking fields into account, we only output one node for + each argument in the Json graph to denote function calls). *) type data_local = Argument of int | Captured of int | Return | Normal of local | Function module Id = struct @@ -498,9 +513,9 @@ module LineageGraph = struct let term_data = match data with | Argument index -> - Printf.sprintf "$arg%d" index + Format.asprintf "$arg%d" index | Captured index -> - Printf.sprintf "$cap%d" index + Format.asprintf "$cap%d" index | Return -> "$ret" | Normal (VariableIndex x) -> @@ -601,7 +616,9 @@ module LineageGraph = struct match data with | Local (var, node) -> save procname (Normal node) (Normal var) - | Argument index -> + | Argument (index, _fields) -> + (* We don't distinguish the fields of arguments when generating Argument nodes. See + {!type:data_local}. *) save procname start (Argument index) | ArgumentOf (index, callee_procname) -> save callee_procname (Start Location.dummy) (Argument index) @@ -683,19 +700,62 @@ let get_captured proc_desc : Var.t list = List.map ~f (Procdesc.get_captured proc_desc) -module Summary = struct +module Tito = struct (** TITO stands for "taint-in taint-out". In this context a tito argument is one that has a path - to the return node, without going through call edges; more precisely, [i] is a tito argument - if there is a path from [Argument i] to [Return] not going through [ArgumentOf _] nodes. *) - type tito_arguments = IntSet.t + to the return node, without going through call edges; more precisely, [i#foo#bar] is a tito + argument if there is a path from [Argument (i, \[foo, bar\])] to [Return] not going through + [ArgumentOf _] nodes. *) + + module FieldSet = struct + include Caml.Set.Make (Fields) + + let pp = Fmt.iter iter Fields.pp + end + + module IntMap = struct + include Caml.Map.Make (Int) + + let pp pp_data = + let sep = Fmt.any ":@ " in + Fmt.iter_bindings ~sep:Fmt.comma iter Fmt.(pair ~sep int pp_data) + end + + (** A [Tito.t] is a map from arguments indexes [i] to the set of [fields] field sequences such + that [i#fields] is a Tito argument. Note: for any sequence of [fields], if [i#fields] is a + Tito argument, then every [i#fields#foo] subfield of should be considered as also being one + (even if not explicitly present in the map). *) + type t = FieldSet.t IntMap.t + (* Note: making this an array could improve the performance (arguments indexes are small and + contiguous). *) + + let pp = IntMap.pp FieldSet.pp + + let empty = IntMap.empty + + let get i arguments = IntMap.find_opt i arguments |> Option.value ~default:FieldSet.empty + + let add i fields arguments = + IntMap.update i + (function + | None -> + Some (FieldSet.singleton fields) + | Some fieldset -> + Some (FieldSet.add fields fieldset) ) + arguments + + + (** Returns a TITO map holding every field of every parameter of a function having the given arity *) + let all_arguments arity = + IntMap.of_seq @@ Seq.init arity (fun arg_index -> (arg_index, FieldSet.singleton [])) +end + +module Summary = struct + type tito_arguments = Tito.t type t = {graph: LineageGraph.t; tito_arguments: tito_arguments; has_unsupported_features: bool} let pp_tito_arguments fmt arguments = - let pp_sep fmt () = Format.fprintf fmt ",@;" in - Format.fprintf fmt "@;@[<2>TitoArguments@;%a@]" - (Format.pp_print_list ~pp_sep Int.pp) - (IntSet.elements arguments) + Format.fprintf fmt "@;@[<2>TitoArguments@;%a@]" Tito.pp arguments let pp fmt {graph; tito_arguments} = @@ -727,9 +787,9 @@ module Summary = struct (* Collect reachable arguments. *) let tito_arguments = let add_node args (node : LineageGraph.data) = - match node with Argument i -> IntSet.add i args | _ -> args + match node with Argument (i, fields) -> Tito.add i fields args | _ -> args in - Set.fold reachable ~init:IntSet.empty ~f:add_node + Set.fold reachable ~init:Tito.empty ~f:add_node in tito_arguments @@ -924,10 +984,17 @@ module TransferFunctions = struct (** Make [LineageGraph.local] usable in Maps/Sets. *) include Comparable.Make (T) + + module Set = struct + include Set + + (** Shortcut for adding a VariableIndex-variant local *) + let add_variable_index set index = add set (VariableIndex index) + end end (** If an expression is made of a single variable index, return it *) - let single_var_index_of_exp (e : Exp.t) : _ VariableIndex.t option = + let exp_as_single_var_index (e : Exp.t) : _ VariableIndex.t option = let rec aux fields_acc = function | Exp.Lvar pvar -> Some (VariableIndex.make (Var.of_pvar pvar) fields_acc) @@ -950,9 +1017,7 @@ module TransferFunctions = struct (** Return the terminal free indices that can be derived from an index *) let terminal_free_locals_from_index shapes index = - VariableIndex.fold_terminal shapes index - ~f:(fun acc index -> Local.Set.add acc (VariableIndex index)) - ~init:Local.Set.empty + VariableIndex.fold_terminal shapes index ~f:Local.Set.add_variable_index ~init:Local.Set.empty (** Return constants and free terminal indices that occur in [e]. *) @@ -964,7 +1029,7 @@ module TransferFunctions = struct terminal_free_locals_from_index shapes (VariableIndex.ident id) | Lfield _ -> ( (* We only allow (sequences of) fields to be "applied" to a single variable, yielding a single index *) - match single_var_index_of_exp e with + match exp_as_single_var_index e with | None -> (* Debugging hint: if you run into this assertion, the easiest is likely to change the frontend to introduce a temporary variable. *) @@ -1003,10 +1068,6 @@ module TransferFunctions = struct Sequence.fold ~init:Procname.Set.empty ~f:add (Exp.closures e) - let free_locals_of_exp_list shapes (es : Exp.t list) : Local.Set.t = - Local.Set.union_list (List.rev_map ~f:(free_locals_of_exp shapes) es) - - type read_set = { free_locals: Local.Set.t (* constants and free variables *) ; captured_locals: Local.Set.t (* captured variables *) @@ -1157,7 +1218,7 @@ module TransferFunctions = struct let exec_assignment shapes node dst_index src_exp astate = - match single_var_index_of_exp src_exp with + match exp_as_single_var_index src_exp with | Some src_index -> (* Simple assignment of the form [dst := src_index]: we copy the fields of [src_index] into the corresponding fields of [dst]. *) @@ -1175,15 +1236,32 @@ module TransferFunctions = struct (* Add Summary (or Direct if this is a suppressed builtin call) edges from the concrete parameters to the concrete destination variable of a call, as specified by the tito_arguments summary information *) - let add_tito (shapes : SimpleShape.Summary.t) node (kind : LineageGraph.FlowKind.t) tito_arguments - (argument_list : Exp.t list) (ret_id : Ident.t) (astate : Domain.t) : Domain.t = + let add_tito (shapes : SimpleShape.Summary.t) node (kind : LineageGraph.FlowKind.t) + (tito_arguments : Tito.t) (argument_list : Exp.t list) (ret_id : Ident.t) (astate : Domain.t) + : Domain.t = + let collect_one_index var_index tito_subfields acc = + VariableIndex.fold_terminal shapes + (VariableIndex.subfield var_index tito_subfields) + ~f:Local.Set.add_variable_index ~init:acc + in let tito_locals = - let tito_exps = - List.filter_mapi - ~f:(fun index arg -> if IntSet.mem index tito_arguments then Some arg else None) - argument_list - in - free_locals_of_exp_list shapes tito_exps + List.foldi ~init:Local.Set.empty + ~f:(fun index acc arg -> + match exp_as_single_var_index arg with + | None -> + (* The Erlang frontend probably doesn't generate arguments that are not put in + intermediate variables first, but in any case we can just add edges from all + occurring locals and soundly not use the TITO information. *) + L.debug Analysis Verbose + "SimpleLineage: the analysis assumes that the frontend uses only single-var \ + expressions as actual arguments, otherwise it will lose precision (found actual \ + argument `%a` instead).@;" + Exp.pp arg ; + Local.Set.union acc (free_locals_of_exp shapes arg) + | Some var_index -> + Tito.FieldSet.fold (collect_one_index var_index) (Tito.get index tito_arguments) acc + ) + argument_list in update_write shapes node kind (VariableIndex.ident ret_id) tito_locals astate @@ -1192,8 +1270,9 @@ module TransferFunctions = struct when no summary is available. *) let add_tito_all (shapes : SimpleShape.Summary.t) node (kind : LineageGraph.FlowKind.t) (argument_list : Exp.t list) (ret_id : Ident.t) (astate : Domain.t) : Domain.t = - let all = IntSet.of_list (List.mapi argument_list ~f:(fun index _ -> index)) in - add_tito shapes node kind all argument_list ret_id astate + let arity = List.length argument_list in + let tito_all_arguments = Tito.all_arguments arity in + add_tito shapes node kind tito_all_arguments argument_list ret_id astate (* Add the relevant Summary/Direct call edges from concrete arguments to the destination, depending @@ -1366,17 +1445,23 @@ let unskipped_checker ({InterproceduralAnalysis.proc_desc} as analysis) shapes_o List.fold ~init:Domain.Real.LastWrites.bottom ~f:add_arg (captured @ formals) in let local_edges = - let add_index_flow ~source local_edges var_index = + let add_proc_start_flow ~source local_edges var_index = LineageGraph.add_flow ~kind:Direct ~node:start_node ~source ~target:(Local (VariableIndex var_index, start_node)) local_edges in - let add_flow ~source local_edges var = - VariableIndex.fold_terminal ~f:(add_index_flow ~source) ~init:local_edges shapes - (VariableIndex.var var) + let add_arg_flow i local_edges arg_var = + VariableIndex.fold_terminal + ~f:(fun acc idx -> + let fields = VariableIndex.get_fields idx in + add_proc_start_flow ~source:(Argument (i, fields)) acc idx ) + ~init:local_edges shapes (VariableIndex.var arg_var) + in + let add_cap_flow i local_edges var = + VariableIndex.fold_terminal + ~f:(add_proc_start_flow ~source:(Captured i)) + ~init:local_edges shapes (VariableIndex.var var) in - let add_arg_flow i = add_flow ~source:(Argument i) in - let add_cap_flow i = add_flow ~source:(Captured i) in let local_edges = [] in let local_edges = List.foldi ~init:local_edges ~f:add_arg_flow formals in let local_edges = List.foldi ~init:local_edges ~f:add_cap_flow captured in From 699c30d753ecd31bca6f24ac8adf39a6325260a5 Mon Sep 17 00:00:00 2001 From: Thibault Suzanne Date: Thu, 23 Feb 2023 11:12:25 -0800 Subject: [PATCH 24/25] Refactoring parts of Lineage Summary: - Slightly complete some comments - Refactor `add_arg_flows` to reduce let-nesting and try to have some more descriptive inner function names - Use `sources_of_local` in a place where it was syntactically inlined Reviewed By: rgrig Differential Revision: D43192611 fbshipit-source-id: 74b9b7fa109f0220c620a6f562fe65022df56f9c --- infer/src/checkers/SimpleLineage.ml | 35 ++++++++++++----------------- 1 file changed, 14 insertions(+), 21 deletions(-) diff --git a/infer/src/checkers/SimpleLineage.ml b/infer/src/checkers/SimpleLineage.ml index d3081c1a4ea..861652ef784 100644 --- a/infer/src/checkers/SimpleLineage.ml +++ b/infer/src/checkers/SimpleLineage.ml @@ -1124,27 +1124,27 @@ module TransferFunctions = struct List.fold ~init:astate ~f:one_exp (Sil.exps_of_instr instr) - (* Add flow from the concrete arguments to the special ArgumentOf nodes *) + (* Add Call flow from the concrete arguments to the special ArgumentOf nodes *) let add_arg_flows shapes (call_node : PPNode.t) (callee_pname : Procname.t) (argument_list : Exp.t list) (astate : Domain.t) : Domain.t = - let add_flows_all_to_arg index ((last_writes, has_unsupported_features), local_edges) arg = - let read_set = free_locals_of_exp shapes arg in - let add_flows_local_to_arg local_edges (local : Local.t) = + let add_one_arg_flows index ((last_writes, has_unsupported_features), local_edges) arg = + let add_one_source_edge local_edges source = + LineageGraph.add_flow ~kind:Call ~node:call_node ~source + ~target:(ArgumentOf (index, callee_pname)) + local_edges + in + let add_one_local_flows local_edges (local : Local.t) = let sources = sources_of_local call_node last_writes local in - let add_one_flow local_edges source = - LineageGraph.add_flow ~kind:Call ~node:call_node ~source - ~target:(ArgumentOf (index, callee_pname)) - local_edges - in - List.fold sources ~f:add_one_flow ~init:local_edges + List.fold sources ~f:add_one_source_edge ~init:local_edges in - let local_edges = Set.fold read_set ~init:local_edges ~f:add_flows_local_to_arg in + let read_set = free_locals_of_exp shapes arg in + let local_edges = Set.fold read_set ~init:local_edges ~f:add_one_local_flows in ((last_writes, has_unsupported_features), local_edges) in - List.foldi argument_list ~init:astate ~f:add_flows_all_to_arg + List.foldi argument_list ~init:astate ~f:add_one_arg_flows - (* Add flow from the special Return nodes to the destination variable of a call *) + (* Add Return flow from the special ReturnOf nodes to the destination variable of a call *) let add_ret_flows shapes node (callee_pname : Procname.t) (ret_id : Ident.t) (astate : Domain.t) : Domain.t = let last_writes, local_edges = astate in @@ -1179,14 +1179,7 @@ module TransferFunctions = struct (((last_writes, has_unsupported_features), local_edges) : Domain.t) : Domain.t = let target = LineageGraph.Local (VariableIndex write_var, node) in let add_read local_edges (read_local : Local.t) = - let sources = - match read_local with - | ConstantAtom _ | ConstantInt _ | ConstantString _ -> - [LineageGraph.Local (read_local, node)] - | VariableIndex read_var -> - let source_nodes = Domain.Real.LastWrites.get_all read_var last_writes in - List.map ~f:(fun node -> LineageGraph.Local (read_local, node)) source_nodes - in + let sources = sources_of_local node last_writes read_local in let add_edge local_edges source = LineageGraph.add_flow ~node ~kind ~source ~target local_edges in From c16e1ccebeed0220b1aeefc338cd2f273b0a8fe9 Mon Sep 17 00:00:00 2001 From: Thibault Suzanne Date: Thu, 23 Feb 2023 11:12:28 -0800 Subject: [PATCH 25/25] Add field Projection/Injection metadata in Lineage graph Summary: The ongoing work on interprocedural analysis aims at improving dataflow precision by removing spurious Derive edges generated on function calls, based on a better understanding of fields concerned by these calls. It relies on the fact that it is sufficient to follow Derive edges only, not Call-then-Return paths, when looking for data flows -- in other words, the Call and Return edges remain largely unaffected by this work, for various technical and theoretical reasons. Yet this assumption is not true when mixing in flows imported from another analysis such as a dynamic one: some actual flows may exist that will go though Call/Return edges (of the same function) and do not have a corresponding Derive edge. This jeopardises the precision improvement expected from interprocedural work. To alleviate this, we add some shape information into those edges, by annotating them with the fields that are projected from or injected into some node. Injection is generated on Call edges and on edges that have a special Return node as destination, meaning that the source only flows into the corresponding field of the destination. Projection is generated on edges from a formal parameter and on Return edges, meaning that only the corresponding field of the source flows into the destination. It becomes then possible to filter out impossible paths by removing those that involves an edge that inject into some field `f`, then only does some Copying, then projects from another field `f'` -- similar to what can already be done on Call stacks to prevent "returning" from a function that wasn't called in the first place. Note that, until further understanding, Derive edges between injection and projection should "reset" this tracking (as they could themselves involve a projection of some sort), and nested fields are to be understood in a "prefix" sense: injecting into `#foo#bar` then projecting from `#foo` doesn't break the chain either. *Implementation details.* Within the internal analysis, we add two knew new kinds of edges, `Project` and `Inject`, and also add field information on the `Call` and `Return` edges. The former are generated to complete the summary of the "current" procedure (replacing some Copies when formals fields are involved), whereas the latter keep being generated upon calling another procedure. The Json output however retains its old edge kinds, but they may now have an additional `edge_metadata` component. When present, its value will be either `{ "projection" : ["nested"; "field"; "list"] }` or `{ "injection" : ... }`. The current diff will not generate "trivial" projections or injections, that is with an empty field list. The schema doesn't forbid an edge that both projects and injects, but that will not currently happen. If the metadata is trivial, il will not be present at all on the edge entity. Reviewed By: rgrig Differential Revision: D43401524 fbshipit-source-id: 12bd5470920868964c23a9252ebfbd8259e57f55 --- infer/src/checkers/SimpleLineage.ml | 179 ++++++++++++++++++++++------ 1 file changed, 145 insertions(+), 34 deletions(-) diff --git a/infer/src/checkers/SimpleLineage.ml b/infer/src/checkers/SimpleLineage.ml index 861652ef784..4ad19c47054 100644 --- a/infer/src/checkers/SimpleLineage.ml +++ b/infer/src/checkers/SimpleLineage.ml @@ -22,9 +22,18 @@ end module Fields = struct (** A module to help manipulating lists of (nested) fields. *) + (** We define a type alias to be able use our own json exporting function *) + type fieldname = Fieldname.t [@@deriving compare, equal, sexp] + + let yojson_of_fieldname fieldname = + (* The ppx-generated [yojson_of] is unnecessarily complex for our purposes (it's a record that + involves "class_name", which incidentally seems to always be "_".) *) + `String (Fieldname.to_string fieldname) + + (* The list is to be understood in "syntactic order": [["a"; "b"]] represents the field part of [X#a#b].*) - type t = Fieldname.t list [@@deriving compare, equal, sexp] + type t = fieldname list [@@deriving compare, equal, sexp, yojson_of] let pp = Fmt.(list ~sep:nop (any "#" ++ Fieldname.pp)) end @@ -181,8 +190,10 @@ module LineageGraph = struct - INV2: There is no loop, because they don't mean anything. *) type t = | Direct (** Immediate copy; e.g., assigment or passing an argument *) - | Call (** Target is ArgumentOf *) - | Return (** Source is ReturnOf *) + | Inject of Fields.t + | Project of Fields.t + | Call of Fields.t (** Target is ArgumentOf, fields are injected into arg *) + | Return of Fields.t (** Source is ReturnOf, fields are projected from return *) | Capture (** [X=1, F=fun()->X end] has Capture flow from X to F *) | Summary (** Summarizes the effect of a procedure call *) | DynamicCallFunction @@ -253,10 +264,14 @@ module LineageGraph = struct Format.fprintf fmt "Capture" | Direct -> Format.fprintf fmt "Direct" - | Call -> - Format.fprintf fmt "Call" - | Return -> - Format.fprintf fmt "Return" + | Call fields -> + Format.fprintf fmt "Call%a" Fields.pp fields + | Inject fields -> + Format.fprintf fmt "Inject%a" Fields.pp fields + | Project fields -> + Format.fprintf fmt "Project%a" Fields.pp fields + | Return fields -> + Format.fprintf fmt "Return%a" Fields.pp fields | Summary -> Format.fprintf fmt "Summary" | DynamicCallFunction -> @@ -291,13 +306,13 @@ module LineageGraph = struct graph (* skip Summary loops*) | _, true, _, _ -> L.die InternalError "There shall be no fancy (%a) loops!" pp_flow_kind kind - | Call, _, ArgumentOf _, _ -> + | Call _, _, ArgumentOf _, _ -> added - | Call, _, _, _ -> + | Call _, _, _, _ -> L.die InternalError "Call edges shall return ArgumentOf!" - | Return, _, _, ReturnOf _ -> + | Return _, _, _, ReturnOf _ -> added - | Return, _, _, _ -> + | Return _, _, _, _ -> L.die InternalError "Return edges shall come form ReturnOf!" | _ -> added @@ -382,6 +397,15 @@ module LineageGraph = struct | DynamicCallModule | Return + type edge_metadata = + { inject: Fields.t [@default []] [@yojson_drop_default.equal] + ; project: Fields.t [@default []] [@yojson_drop_default.equal] } + [@@deriving yojson_of] + + let metadata_inject fields = {inject= fields; project= []} + + let metadata_project fields = {inject= []; project= fields} + let yojson_of_edge_type typ = match typ with | Capture -> @@ -400,7 +424,12 @@ module LineageGraph = struct `String "Return" - type _edge = {source: node_id; target: node_id; edge_type: edge_type; location: location_id} + type _edge = + { source: node_id + ; target: node_id + ; edge_type: edge_type + ; edge_metadata: edge_metadata option [@yojson.option] + ; location: location_id } [@@deriving yojson_of] type edge = {edge: _edge} [@@deriving yojson_of] @@ -647,27 +676,44 @@ module LineageGraph = struct let edge_id = Id.of_list [source_id; target_id; kind_id; location_id] in let edge_type = match kind with - | Call -> + | Call _ -> Json.Call | Capture -> Json.Capture | Direct -> Json.Copy + | Inject _ -> + Json.Copy + | Project _ -> + Json.Copy | Summary -> Json.Derive | DynamicCallFunction -> Json.DynamicCallFunction | DynamicCallModule -> Json.DynamicCallModule - | Return -> + | Return _ -> Json.Return in + let edge_metadata = + match kind with + | Direct | Capture | Summary | DynamicCallFunction | DynamicCallModule -> + None + | Call [] | Return [] -> + (* Don't generate "trivial" metadata *) + None + | Call fields | Inject fields -> + Some (Json.metadata_inject fields) + | Return fields | Project fields -> + Some (Json.metadata_project fields) + in write_json Edge edge_id (Json.yojson_of_edge { edge= { source= Id.out source_id ; target= Id.out target_id ; edge_type + ; edge_metadata ; location= Id.out location_id } } ) ; edge_id @@ -845,7 +891,14 @@ module Summary = struct match kind with | Direct -> false - | Call | Return | Capture | Summary | DynamicCallFunction | DynamicCallModule -> + | Call _ + | Return _ + | Capture + | Summary + | DynamicCallFunction + | DynamicCallModule + | Inject _ + | Project _ -> true in (* The set [todo] contains vertices considered for removal. We initialize this set with all @@ -993,6 +1046,25 @@ module TransferFunctions = struct end end + (** If an expression is made of a single variable, return it *) + let exp_as_single_var (e : Exp.t) : Var.t option = + match e with + | Exp.Lvar pvar -> + Some (Var.of_pvar pvar) + | Exp.Var id -> + Some (Var.of_id id) + | Exp.Lfield (_, _, _) + | Exp.UnOp (_, _, _) + | Exp.BinOp (_, _, _) + | Exp.Exn _ + | Exp.Closure _ + | Exp.Const _ + | Exp.Cast (_, _) + | Exp.Lindex (_, _) + | Exp.Sizeof _ -> + None + + (** If an expression is made of a single variable index, return it *) let exp_as_single_var_index (e : Exp.t) : _ VariableIndex.t option = let rec aux fields_acc = function @@ -1124,21 +1196,46 @@ module TransferFunctions = struct List.fold ~init:astate ~f:one_exp (Sil.exps_of_instr instr) + let warn_on_complex_arg arg_exp = + L.debug Analysis Verbose + "SimpleLineage: the analysis assumes that the frontend uses only single-var expressions as \ + actual arguments, otherwise it will lose precision (found actual argument `%a` instead).@;" + Exp.pp arg_exp + + (* Add Call flow from the concrete arguments to the special ArgumentOf nodes *) let add_arg_flows shapes (call_node : PPNode.t) (callee_pname : Procname.t) (argument_list : Exp.t list) (astate : Domain.t) : Domain.t = let add_one_arg_flows index ((last_writes, has_unsupported_features), local_edges) arg = - let add_one_source_edge local_edges source = - LineageGraph.add_flow ~kind:Call ~node:call_node ~source + let add_one_source_edge local_edges source ~injected_arg_field = + LineageGraph.add_flow ~kind:(Call injected_arg_field) ~node:call_node ~source ~target:(ArgumentOf (index, callee_pname)) local_edges in - let add_one_local_flows local_edges (local : Local.t) = + let add_one_local_flows local_edges (local : Local.t) ~injected_arg_field = let sources = sources_of_local call_node last_writes local in - List.fold sources ~f:add_one_source_edge ~init:local_edges + List.fold sources ~f:(add_one_source_edge ~injected_arg_field) ~init:local_edges + in + let local_edges = + match exp_as_single_var arg with + | None -> + (* The Erlang frontend probably doesn't generate non-single-var arguments. If that + happens however, we may simply collect all the locals from the actual argument and + have them flow on the full formal parameter (that is inject into the empty list of + nested fields) *) + warn_on_complex_arg arg ; + let read_set = free_locals_of_exp shapes arg in + Set.fold read_set ~init:local_edges ~f:(add_one_local_flows ~injected_arg_field:[]) + | Some arg_var -> + (* The concrete argument is a single var: we collect all its terminal fields and have + them flow onto the corresponding field of the formal parameter. *) + let arg_as_index = VariableIndex.var arg_var in + VariableIndex.fold_terminal shapes arg_as_index + ~f:(fun acc arg_terminal -> + add_one_local_flows acc (VariableIndex arg_terminal) + ~injected_arg_field:(VariableIndex.get_fields arg_terminal) ) + ~init:local_edges in - let read_set = free_locals_of_exp shapes arg in - let local_edges = Set.fold read_set ~init:local_edges ~f:add_one_local_flows in ((last_writes, has_unsupported_features), local_edges) in List.foldi argument_list ~init:astate ~f:add_one_arg_flows @@ -1148,9 +1245,12 @@ module TransferFunctions = struct let add_ret_flows shapes node (callee_pname : Procname.t) (ret_id : Ident.t) (astate : Domain.t) : Domain.t = let last_writes, local_edges = astate in - let add_one_return_edge local_edges target_index = - LineageGraph.add_flow ~kind:Return ~node ~source:(ReturnOf callee_pname) - ~target:(Local (VariableIndex target_index, node)) + let add_one_return_edge local_edges ret_terminal_index = + (* Add flow from the formal return to a terminal subfield of the actual ret_id: project the + return into the corresponding fields. *) + let target_field = VariableIndex.get_fields ret_terminal_index in + LineageGraph.add_flow ~kind:(Return target_field) ~node ~source:(ReturnOf callee_pname) + ~target:(Local (VariableIndex ret_terminal_index, node)) local_edges in let local_edges = @@ -1245,11 +1345,7 @@ module TransferFunctions = struct (* The Erlang frontend probably doesn't generate arguments that are not put in intermediate variables first, but in any case we can just add edges from all occurring locals and soundly not use the TITO information. *) - L.debug Analysis Verbose - "SimpleLineage: the analysis assumes that the frontend uses only single-var \ - expressions as actual arguments, otherwise it will lose precision (found actual \ - argument `%a` instead).@;" - Exp.pp arg ; + warn_on_complex_arg arg ; Local.Set.union acc (free_locals_of_exp shapes arg) | Some var_index -> Tito.FieldSet.fold (collect_one_index var_index) (Tito.get index tito_arguments) acc @@ -1438,21 +1534,27 @@ let unskipped_checker ({InterproceduralAnalysis.proc_desc} as analysis) shapes_o List.fold ~init:Domain.Real.LastWrites.bottom ~f:add_arg (captured @ formals) in let local_edges = - let add_proc_start_flow ~source local_edges var_index = - LineageGraph.add_flow ~kind:Direct ~node:start_node ~source + let add_proc_start_flow ~source ~kind local_edges var_index = + LineageGraph.add_flow ~kind ~node:start_node ~source ~target:(Local (VariableIndex var_index, start_node)) local_edges in + let arg_edge_kind arg_fields : LineageGraph.FlowKind.t = + (* Record that edges from fields of a formal parameter will represent a Projection of those + fields from the eventual summarised Argument node *) + match arg_fields with [] -> Direct | subfields -> Project subfields + in let add_arg_flow i local_edges arg_var = VariableIndex.fold_terminal ~f:(fun acc idx -> let fields = VariableIndex.get_fields idx in - add_proc_start_flow ~source:(Argument (i, fields)) acc idx ) + add_proc_start_flow ~kind:(arg_edge_kind fields) ~source:(Argument (i, fields)) acc idx + ) ~init:local_edges shapes (VariableIndex.var arg_var) in let add_cap_flow i local_edges var = VariableIndex.fold_terminal - ~f:(add_proc_start_flow ~source:(Captured i)) + ~f:(add_proc_start_flow ~kind:Direct ~source:(Captured i)) ~init:local_edges shapes (VariableIndex.var var) in let local_edges = [] in @@ -1477,8 +1579,17 @@ let unskipped_checker ({InterproceduralAnalysis.proc_desc} as analysis) shapes_o post_edges :: edges in let ret_var = VariableIndex.pvar (Procdesc.get_ret_var proc_desc) in + let ret_edge_kind into_ret_index : LineageGraph.FlowKind.t = + (* Record that edges into fields of the formal return will represent an Injection of those + fields into the eventual summarised Return node *) + match VariableIndex.get_fields into_ret_index with + | [] -> + Direct + | subfields -> + Inject subfields + in let add_one_ret_index_edge local_edges ret_index ret_node = - LineageGraph.add_flow ~kind:Direct ~node:ret_node + LineageGraph.add_flow ~kind:(ret_edge_kind ret_index) ~node:ret_node ~source:(Local (VariableIndex ret_index, ret_node)) ~target:Return local_edges in