Package org.checkerframework.checker.resourceleak

Class MustCallConsistencyAnalyzer

java.lang.Object
org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer
public class MustCallConsistencyAnalyzer extends Object
An analyzer that checks consistency of 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.

  • Constructor Details

    • MustCallConsistencyAnalyzer

      public MustCallConsistencyAnalyzer(ResourceLeakChecker rlc)
      Creates a consistency analyzer. Typically, the type factory's postAnalyze method would instantiate a new consistency analyzer using this constructor and then call analyze(ControlFlowGraph).
      Parameters:
      rlc - the resource leak checker

  • Method Details

    • analyze

      public void analyze(ControlFlowGraph cfg)
      The main function of the consistency dataflow analysis. The analysis tracks dataflow facts ("Obligations") of type MustCallConsistencyAnalyzer.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 in obligations. 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() or super() 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-effected
      node - the invocation node to check; must be MethodInvocationNode or ObjectCreationNode
      isMustCallInference - true if this method is invoked as part of a MustCall inference
      Returns:
      true iff the result of node should be tracked in obligations

    • formatMissingMustCallMethods

      public static String formatMissingMustCallMethods(List<String> mustCallVal)
      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