pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
infer_clone/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp

12 lines
322 B
Raw Normal View History Unescape

[pulse][impurity] Use pulse for detecting impurity Summary: Introduce a new experimental checker (`--impurity`) that detects impurity information, tracking which parameters and global variables of a function are modified. The checker relies on Pulse to detect how the state changes: it traverses the pre and post pairs starting from the parameter/global variable and finds where the pre and post heaps diverge. At diversion points, we expect to see WrittenTo/Invalid attributes containing a trace of how the address was modified. We use these to construct the trace of impurity. This checker is a complement to the purity checker that exists mainly for Java (and used for cost and loop-hoisting analyses). The aim of this new experimental checker is to rely on Pulse's precise memory treatment and come up with a more precise im(purity) analysis. To distinguish the two checkers, we introduce a new issue type `IMPURE_FUNCTION` that reports when a function is impure, rather than when it is pure (as in the purity checker). TODO: - improve the analysis to rely on impurity information of external library calls. Currently, all library calls are assumed to be nops, hence pure. - de-entangle Pulse reporting from analysis. Reviewed By: skcho Differential Revision: D17051567 fbshipit-source-id: 5e10afb4f
6 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.
*/
#include <iostream>
[pulse] havoc formals passed by reference to unknown procedures Summary: This gets rid of false positives when something invalid (eg null) is passed by reference to an initialisation function. Havoc'ing what the contents of the pointer to results in being optimistic about said contents in the future. Also surprisingly gets rid of some FNs (which means it can also introduce FPs) in the `std::atomic` tests because a path condition becomes feasible with havoc'ing. There's a slight refinement possible where we don't havoc pointers to const but that's more involved and left as future work. Reviewed By: skcho Differential Revision: D18726203 fbshipit-source-id: 264b5daeb
5 years ago
void output_stream_impure() { std::cout << "Hello, world!" << std::endl; }
[pulse][impurity] Use pulse for detecting impurity Summary: Introduce a new experimental checker (`--impurity`) that detects impurity information, tracking which parameters and global variables of a function are modified. The checker relies on Pulse to detect how the state changes: it traverses the pre and post pairs starting from the parameter/global variable and finds where the pre and post heaps diverge. At diversion points, we expect to see WrittenTo/Invalid attributes containing a trace of how the address was modified. We use these to construct the trace of impurity. This checker is a complement to the purity checker that exists mainly for Java (and used for cost and loop-hoisting analyses). The aim of this new experimental checker is to rely on Pulse's precise memory treatment and come up with a more precise im(purity) analysis. To distinguish the two checkers, we introduce a new issue type `IMPURE_FUNCTION` that reports when a function is impure, rather than when it is pure (as in the purity checker). TODO: - improve the analysis to rely on impurity information of external library calls. Currently, all library calls are assumed to be nops, hence pure. - de-entangle Pulse reporting from analysis. Reviewed By: skcho Differential Revision: D17051567 fbshipit-source-id: 5e10afb4f
6 years ago
[impurity] Rely on set of skipped functions to determine impurity Summary: Currently, impurity analysis is oblivious to skipped functions which might e.g. return a non-deterministic value, write to memory or have some other side-effect. This diff fixes that by relying on Pulse's skipped functions to determine impurity. Any unknown function which is not modeled to be pure is assumed to be impure. This is a heuristic. We could have assumed them to be pure by default as well. Reviewed By: jvillard Differential Revision: D19428514 fbshipit-source-id: 82efe04f9
5 years ago
int random_impure() { std::rand(); }