Class MustCallConsistencyAnalyzer
MustCall
and CalledMethods
types, thereby
detecting resource leaks. For any expression e the analyzer ensures that when e
goes out of scope, there exists a resource alias r of e (which might be
e itself) such that the must-call methods of r (i.e. the values of r's
MustCall type) are contained in the value of r's CalledMethods type. For any e
for which this property does not hold, the analyzer reports a
"required.method.not.called"
error, indicating a possible resource leak.
Mechanically, the analysis does two tasks.
- Tracks must-aliases, implemented via a dataflow analysis. Each dataflow fact is a set of resource-aliases that refer to the same resource. Furthermore, that resource is owned. No dataflow facts are maintained for a non-owned resource.
- When the last resource alias in a resource-alias set goes out-of-scope, it checks their must-call and called-methods types. The analysis does not track must-call or called-methods types, but queries other checkers to obtain them.
Class MustCallConsistencyAnalyzer.Obligation
represents a single such dataflow fact. Abstractly, each dataflow
fact is a pair: a set of resource aliases to some resource, and the must-call obligations of that
resource (i.e the list of must-call methods that need to be called on one of the resource
aliases). Concretely, the Must Call Checker is responsible for tracking the latter - an
expression's must-call type indicates which methods must be called - so this dataflow analysis
only actually tracks the sets of resource aliases.
The dataflow algorithm adds, modifies, or removes dataflow facts when certain code patterns are encountered, to account for ownership transfer. Here are non-exhaustive examples:
- A new fact is added to the tracked set when a constructor or a method with an owning return is invoked.
- A fact is modified when an expression with a tracked Obligation is the RHS of a (pseudo-)assignment. The LHS is added to the existing resource alias set.
- A fact can be removed when a member of a resource-alias set is assigned to an owning field
or passed to a method in a parameter location that is annotated as
@Owning
.
The dataflow analysis for these Obligations is conservative in that it guarantees that for every resource which actually does have a must-call obligation, at least one Obligation will exist. However, it does not guarantee the opposite: Obligations may also exist for resources without a must-call obligation (or for non-resources) as a result of analysis imprecision. That is, the set of Obligations tracked by the analysis over-approximates the actual set of resources in the analyzed program with must-call obligations.
Throughout, this class uses the temporary-variable facilities provided by the Must Call and
Resource Leak type factories both to emulate a three-address-form IR (simplifying some analysis
logic) and to permit expressions to have their types refined in their respective checkers'
stores. These temporary variables can be members of resource-alias sets. Without temporary
variables, the checker wouldn't be able to verify code such as new Socket(host,
port).close()
, which would cause false positives. Temporaries are created for new
expressions, method calls (for the return value), and ternary expressions. Other types of
expressions may be supported in the future.
-
Nested Class Summary
Nested ClassesModifier and TypeClassDescriptionstatic enum
A description for how a method might exit. -
Constructor Summary
ConstructorsConstructorDescriptionCreates a consistency analyzer. -
Method Summary
Modifier and TypeMethodDescriptionvoid
analyze
(ControlFlowGraph cfg) The main function of the consistency dataflow analysis.static String
formatMissingMustCallMethods
(List<String> mustCallVal) Formats a list of must-call method names to be printed in an error message.boolean
shouldTrackInvocationResult
(Set<org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.Obligation> obligations, Node node, boolean isMustCallInference) Returns true if the result of the given method or constructor invocation node should be tracked inobligations
.
-
Constructor Details
-
MustCallConsistencyAnalyzer
Creates a consistency analyzer. Typically, the type factory's postAnalyze method would instantiate a new consistency analyzer using this constructor and then callanalyze(ControlFlowGraph)
.- Parameters:
rlc
- the resource leak checker
-
-
Method Details
-
analyze
The main function of the consistency dataflow analysis. The analysis tracks dataflow facts ("Obligations") of typeMustCallConsistencyAnalyzer.Obligation
, each representing a set of owning resource aliases for some value with a non-empty@MustCall
obligation. The set of tracked Obligations is guaranteed to include at least one Obligation for each actual resource in the program, but might include other, spurious Obligations, too (that is, it is a conservative over-approximation of the true Obligation set).The analysis improves its precision by removing Obligations from tracking when it can prove that they do not represent real resources. For example, it is not necessary to track expressions with empty
@MustCall
obligations, because they are trivially fulfilled. Nor is tracking non-owning aliases necessary, because by definition they cannot be used to fulfill must-call obligations.- Parameters:
cfg
- the control flow graph of the method to check
-
shouldTrackInvocationResult
public boolean shouldTrackInvocationResult(Set<org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.Obligation> obligations, Node node, boolean isMustCallInference) Returns true if the result of the given method or constructor invocation node should be tracked inobligations
. In some cases, there is no need to track the result because the must-call obligations are already satisfied in some other way or there cannot possibly be must-call obligations because of the structure of the code.Specifically, an invocation result does NOT need to be tracked if any of the following is true:
- The invocation is a call to a
this()
orsuper()
constructor. - The method's return type is annotated with MustCallAlias and the argument passed in this invocation in the corresponding position is an owning field.
- The method's return type is non-owning, which can either be because the method has no
return type or because the return type is annotated with
NotOwning
.
This method can also side-effect
obligations
, if node is a super or this constructor call with MustCallAlias annotations, by removing that Obligation.- Parameters:
obligations
- the current set of Obligations, which may be side-effectednode
- the invocation node to check; must beMethodInvocationNode
orObjectCreationNode
isMustCallInference
- true if this method is invoked as part of a MustCall inference- Returns:
- true iff the result of
node
should be tracked inobligations
- The invocation is a call to a
-
formatMissingMustCallMethods
Formats a list of must-call method names to be printed in an error message.- Parameters:
mustCallVal
- the list of must-call strings- Returns:
- a formatted string
-