From cc815f5d20098315c276a85d546136d92b53f2eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 18 Mar 2020 02:21:43 -0700 Subject: [PATCH] [pulse] Only propagate existing WrittenTo attributes at function calls Summary: Previously, at each function call, we added a `WrittenTo` attribute for applying the address of the actuals. However, this results in mistakenly considering each function application that inspects its argument as impure. Instead, we should only propagate `WrittenTo` if the actuals have already `WrittenTo` attributes. For instance, for the following functions ``` public static boolean is_null(Byte a) { return a == null; } public static boolean call_is_null(Byte a) { return is_null(a); } ``` We used to get the following pulse summary for `call_is_null` (showing only one of the disjuncts): ``` #0: PRE: { roots={ &a=v1 }; mem ={ v1 -> { * -> v2 } }; attrs={ v1 -> { MustBeValid }, v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };} POST: { roots={ &a=v1, &return=v8 }; mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } }; attrs={ v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]), WrittenTo-----------WRONG }, v4 -> { Arith =1, BoItv (1), Invalid ConstantDereference(is the constant 1), WrittenTo-----------WRONG }, v8 -> { WrittenTo } };} SKIPPED_CALLS: { } ``` where we mistakenly recorded a `WrittenTo` for `v2` (what `a` points to). As a result, we considered `call_is_null` as impure :( This diff fixes that since the callee `is_null` doesn't have any `WrittenTo` attributes for its parameter `a`. So, we don't propagate `WrittenTo` and get the following summary ``` #0: PRE: { roots={ &a=v1 }; mem ={ v1 -> { * -> v2 } }; attrs={ v1 -> { MustBeValid }, v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };} POST: { roots={ &a=v1, &return=v8 }; mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } }; attrs={ v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) }, v4 -> { Arith =1, BoItv (1), Invalid ConstantDereference(is the constant 1) }, v8 -> { WrittenTo } };} SKIPPED_CALLS: { } ``` Reviewed By: skcho Differential Revision: D20490102 fbshipit-source-id: 253d8ef64 --- infer/src/pulse/PulseAbductiveDomain.ml | 37 +++++++++---------- .../codetoanalyze/cpp/impurity/issues.exp | 2 - .../cpp/impurity/struct_test.cpp | 13 +++++++ .../java/impurity/Localities.java | 8 ++++ 4 files changed, 38 insertions(+), 22 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/impurity/struct_test.cpp diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 5a04e84e7..2d401920c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -817,27 +817,24 @@ module PrePost = struct BaseMemory.add addr_caller edges_post_caller heap in let attrs = - let written_to = - let written_to_callee_opt = - let open IOption.Let_syntax in - let* attrs = BaseAddressAttributes.find_opt addr_caller attrs in - Attributes.get_written_to attrs - in - let callee_trace = - match written_to_callee_opt with - | None -> - Trace.Immediate {location= call_loc; history= []} - | Some access_trace -> - access_trace - in - Attribute.WrittenTo - (ViaCall - { in_call= callee_trace - ; f= Call callee_proc_name - ; location= call_loc - ; history= hist_caller }) + let written_to_callee_opt = + let open IOption.Let_syntax in + let* attrs = BaseAddressAttributes.find_opt addr_caller attrs in + Attributes.get_written_to attrs in - BaseAddressAttributes.add_one addr_caller written_to attrs + match written_to_callee_opt with + | None -> + attrs + | Some callee_trace -> + let written_to = + Attribute.WrittenTo + (ViaCall + { in_call= callee_trace + ; f= Call callee_proc_name + ; location= call_loc + ; history= hist_caller }) + in + BaseAddressAttributes.add_one addr_caller written_to attrs in let caller_post = Domain.update ~heap ~attrs call_state.astate.post in {call_state with subst; astate= {call_state.astate with post= caller_post}} diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index b1646de4f..89838c79a 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -1,7 +1,5 @@ ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter::operator++,parameter `this` modified here] ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter::operator++,parameter `this` modified here] -../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=,when calling `std::operator==` here,parameter `__x` modified here,when calling `std::operator==` here,parameter `__y` modified here] -../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=,when calling `std::operator==` here,parameter `__x` modified here,when calling `std::operator==` here,parameter `__y` modified here] codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter `array` modified here] codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter `a` modified here] codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter `b` modified here,parameter `a` modified here] diff --git a/infer/tests/codetoanalyze/cpp/impurity/struct_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/struct_test.cpp new file mode 100644 index 000000000..463b067a2 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/struct_test.cpp @@ -0,0 +1,13 @@ +/* + * 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. + */ +struct Foo { + int x; + + bool operator<(const Foo& rhs) const { return x < rhs.x; } +}; + +void call_lt_pure(Foo& lhs, Foo& rhs) { lhs < rhs; } diff --git a/infer/tests/codetoanalyze/java/impurity/Localities.java b/infer/tests/codetoanalyze/java/impurity/Localities.java index 0714902d1..5212c5888 100644 --- a/infer/tests/codetoanalyze/java/impurity/Localities.java +++ b/infer/tests/codetoanalyze/java/impurity/Localities.java @@ -174,4 +174,12 @@ class Localities { Foo first = get_first_pure(list); first.inc_impure(); } + + public static boolean is_null_pure(Byte a) { + return a == null; + } + + public static boolean call_is_null_pure(Byte a) { + return is_null_pure(a); + } }