You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

14 lines
329 B

[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
5 years ago
/*
* 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; }