From 127902222db05dd163b25be569ad683353c4beed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 29 Jul 2019 02:16:10 -0700 Subject: [PATCH] [pulse] Filter AddressOfStackVariable from read only heuristic check Reviewed By: skcho Differential Revision: D16518259 fbshipit-source-id: 92a631a82 --- infer/src/istd/PrettyPrintable.ml | 4 ++++ infer/src/istd/PrettyPrintable.mli | 2 ++ infer/src/pulse/PulseAbductiveDomain.ml | 3 ++- infer/src/pulse/PulseDomain.ml | 5 +++++ infer/src/pulse/PulseDomain.mli | 2 ++ infer/tests/codetoanalyze/cpp/pulse/issues.exp | 2 +- 6 files changed, 16 insertions(+), 2 deletions(-) diff --git a/infer/src/istd/PrettyPrintable.ml b/infer/src/istd/PrettyPrintable.ml index 47b9b3602..a9550794b 100644 --- a/infer/src/istd/PrettyPrintable.ml +++ b/infer/src/istd/PrettyPrintable.ml @@ -223,6 +223,8 @@ module type PPUniqRankSet = sig val is_empty : t -> bool + val is_singleton : t -> bool + val is_subset : t -> of_:t -> bool val map : t -> f:(elt -> elt) -> t @@ -253,6 +255,8 @@ module MakePPUniqRankSet (Val : PrintableRankedType) : PPUniqRankSet with type e let is_empty = Map.is_empty + let is_singleton m = Int.equal 1 (Map.cardinal m) + let is_subset m ~of_ = Map.for_all (fun rank value -> diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli index cd07488be..1779115a9 100644 --- a/infer/src/istd/PrettyPrintable.mli +++ b/infer/src/istd/PrettyPrintable.mli @@ -174,6 +174,8 @@ module type PPUniqRankSet = sig val is_empty : t -> bool + val is_singleton : t -> bool + val is_subset : t -> of_:t -> bool val map : t -> f:(elt -> elt) -> t diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 271256c40..d7fbd11aa 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -473,7 +473,8 @@ module PrePost = struct | None -> false | Some (edges_pre, _) -> - Attributes.is_empty attrs_post + ( Attributes.is_empty attrs_post + || Attributes.only_contains_address_of_stack_variable attrs_post ) && PulseDomain.Memory.Edges.equal (fun (addr_dest_pre, _) (addr_dest_post, _) -> (* NOTE: ignores traces diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index cd888bc6e..65dec9326 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -330,6 +330,11 @@ module Attributes = struct Set.find_rank attrs Attribute.std_vector_reserve_rank |> Option.is_some + let only_contains_address_of_stack_variable attrs = + Set.is_singleton attrs + && Option.is_some (Set.find_rank attrs Attribute.address_of_stack_variable_rank) + + include Set end diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index fcb6894c0..ad1849d4b 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -96,6 +96,8 @@ module Attributes : sig val get_must_be_valid : t -> unit InterprocAction.t option val get_address_of_stack_variable : t -> (Var.t * ValueHistory.t * Location.t) option + + val only_contains_address_of_stack_variable : t -> bool end module AbstractAddress : sig diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index ff7bd637e..9d219c4ec 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `Range::Range()`,when calling `setLanguage()` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `Range::operator[]()` here,invalid access occurs here] +codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage()` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `Range::operator[]()` here,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()()` here,invalid access occurs here]