Pulse
General-purpose memory and value analysis engine.
Activate with --pulse
.
Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: Experimental
- Hack: Yes
- Java: Yes
- Python: No
What is Infer:Pulse?β
Pulse is an interprocedural memory safety analysis. Pulse can detect, for instance, Null dereferences in Java. Errors are only reported when all conditions on the erroneous path are true regardless of input. Pulse should gradually replace the original biabduction analysis of Infer. An example of a Null dereference found by Pulse is given below.
class Person {
Person emergencyContact;
String address;
Person getEmergencyContact() {
return this.emergencyContact;
}
}
class Registry {
void create() {
Person p = new Person();
Person c = p.getEmergencyContact();
// Null dereference here
System.out.println(c.address);
}
void printContact(Person p) {
// No null dereference, as we don't know anything about `p`
System.out.println(p.getEmergencyContact().address);
}
}
How to run pulse for Java:
infer run --pulse -- javac Test.java
Pulse reports a Null dereference on this file on create()
, as it tries to access the field address
of object c
, and c
has value null
. In contrast, Pulse gives no report for printContact(Person p)
, as we cannot be sure that p.getEmergencyContact()
will return null
. But, thanks to the fact that the analysis is inter-procedural, Pulse will report a Null dereference on calls to printContact(p)
when it detects that p
is null.
Latent Issuesβ
When an error can occur only on some values of the parameters of the current function, Pulse does not report an issue. Such issues are called latent. But, if Pulse then sees a call site at which all the conditions for the error are satisfied then the error becomes manifest and is reported. This example (in C) illustrates how latent issues are created and then reported when they become manifest:
// for more realism, imagine that this function does other things as well
void set_to_null_if_positive(int n, int* p) {
if (n > 0) {
p = NULL;
}
}
void latent_null_dereference(int n, int* p) {
set_to_null_if_positive(n, p);
*p = 42; // NULL dereference! but only if n > 0 so no report yet
}
void manifest_error(int *p) {
// no way to avoid the bug here => Pulse reports an error
latent_null_dereference(1, p);
}
Unknown Functionsβ
In order to avoid false positives, Pulse makes optimistic assumptions about calls to unknown functions. Unknown functions (or unknown methods) are functions for which Infer didn't find any code. For example, it could be because the function belongs to a third-party library and we know only its signature, or because a function is made through a function pointer that Pulse wasn't able to resolve to a concrete function. In either case, Pulse will scramble the parts of the state reachable from the parameters of the call. In general, this helps avoid false positives but note that this may cause false negatives as well as false positives:
void unknown(int* p); // third-party code that does [*p = 5]
// Infer doesn't have access to that code
void false_negative() {
int* x = (int*) malloc(sizeof(int));
if (x) {
// unknown call to x makes Pulse forget that x was allocated, in case it frees x
unknown(x);
}
} // no memory leak reported: false negative!
void false_positive(int *x) {
unknown(x); // this sets *x to 5
if (x != 5) {
// unreachable
int* p = NULL;
*p = 42; // false positive reported here
}
}
You can check if a given function called any unknown functions by inspecting its Pulse summary. For example, for the code above:
$ infer --pulse-only -- clang -c unknown_code.c
No issues found
$ infer debug --procedures --procedures-filter 'false_negative' --procedures-summary
...
skipped_calls={ unknown -> call to skipped function occurs here }
Pulse x Nullsafeβ
Nullsafe is a type checker for @Nullable
annotations for Java. Classes following the Nullsafe discipline are annotated with @Nullsafe
.
Consider the classes Person
and Registry
from the previous example. Assuming that class Person
is annotated with @Nullsafe
. In this case, we also annotate getEmergencyContact()
with @Nullable
, to make explicit that this method can return the null
value. There is still the risk that classes depending on Person
have Null dereferences. In this case, Pulse would report a Null dereference on Registry
. It could also be the case that class Registry
is annotated with @Nullsafe
. By default Pulse reports on @Nullsafe
files too, see the --pulse-nullsafe-report-npe
option (Facebook-specific: Pulse does not report on @Nullsafe
files).
@Nullsafe(Nullsafe.Mode.LOCAL)
class Person {
Person emergencyContact;
String address;
@Nullable Person getEmergencyContact() {
return this.emergencyContact;
}
}
class Registry {
... // Pulse reports here
}
List of Issue Typesβ
The following issue types are reported by this checker:
- BAD_ARG
- BAD_ARG_LATENT
- BAD_GENERATOR
- BAD_GENERATOR_LATENT
- BAD_KEY
- BAD_KEY_LATENT
- BAD_MAP
- BAD_MAP_LATENT
- BAD_RECORD
- BAD_RECORD_LATENT
- BAD_RETURN
- BAD_RETURN_LATENT
- COMPARED_TO_NULL_AND_DEREFERENCED
- CONFIG_USAGE
- CONSTANT_ADDRESS_DEREFERENCE
- CONSTANT_ADDRESS_DEREFERENCE_LATENT
- DATA_FLOW_TO_SINK
- MEMORY_LEAK_C
- MEMORY_LEAK_CPP
- MUTUAL_RECURSION_CYCLE
- NIL_BLOCK_CALL
- NIL_BLOCK_CALL_LATENT
- NIL_INSERTION_INTO_COLLECTION
- NIL_INSERTION_INTO_COLLECTION_LATENT
- NIL_MESSAGING_TO_NON_POD
- NIL_MESSAGING_TO_NON_POD_LATENT
- NO_MATCHING_BRANCH_IN_TRY
- NO_MATCHING_BRANCH_IN_TRY_LATENT
- NO_MATCHING_CASE_CLAUSE
- NO_MATCHING_CASE_CLAUSE_LATENT
- NO_MATCHING_ELSE_CLAUSE
- NO_MATCHING_ELSE_CLAUSE_LATENT
- NO_MATCHING_FUNCTION_CLAUSE
- NO_MATCHING_FUNCTION_CLAUSE_LATENT
- NO_MATCH_OF_RHS
- NO_MATCH_OF_RHS_LATENT
- NO_TRUE_BRANCH_IN_IF
- NO_TRUE_BRANCH_IN_IF_LATENT
- NULLPTR_DEREFERENCE
- NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS
- NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS_LATENT
- NULLPTR_DEREFERENCE_LATENT
- NULL_ARGUMENT
- NULL_ARGUMENT_LATENT
- OPTIONAL_EMPTY_ACCESS
- OPTIONAL_EMPTY_ACCESS_LATENT
- PULSE_CANNOT_INSTANTIATE_ABSTRACT_CLASS
- PULSE_CONST_REFABLE
- PULSE_DICT_MISSING_KEY
- PULSE_DYNAMIC_TYPE_MISMATCH
- PULSE_READONLY_SHARED_PTR_PARAM
- PULSE_REFERENCE_STABILITY
- PULSE_RESOURCE_LEAK
- PULSE_TRANSITIVE_ACCESS
- PULSE_UNAWAITED_AWAITABLE
- PULSE_UNFINISHED_BUILDER
- PULSE_UNINITIALIZED_CONST
- PULSE_UNINITIALIZED_VALUE
- PULSE_UNNECESSARY_COPY
- PULSE_UNNECESSARY_COPY_ASSIGNMENT
- PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST
- PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE
- PULSE_UNNECESSARY_COPY_INTERMEDIATE
- PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST
- PULSE_UNNECESSARY_COPY_MOVABLE
- PULSE_UNNECESSARY_COPY_OPTIONAL
- PULSE_UNNECESSARY_COPY_OPTIONAL_CONST
- PULSE_UNNECESSARY_COPY_RETURN
- PULSE_UNNECESSARY_COPY_THRIFT_ASSIGNMENT
- RETAIN_CYCLE
- RETAIN_CYCLE_NO_WEAK_INFO
- SENSITIVE_DATA_FLOW
- STACK_VARIABLE_ADDRESS_ESCAPE
- TAINT_ERROR
- USE_AFTER_DELETE
- USE_AFTER_DELETE_LATENT
- USE_AFTER_FREE
- USE_AFTER_FREE_LATENT
- USE_AFTER_LIFETIME
- USE_AFTER_LIFETIME_LATENT
- VECTOR_INVALIDATION
- VECTOR_INVALIDATION_LATENT