This chapter describes how to build a checker for an accumulation analysis. If you want to use an existing checker, you do not need to read this chapter.
An accumulation analysis is a program analysis where the analysis abstraction is a monotonically increasing set — that is, the analysis learns new facts, and facts are never retracted. Typically, some operation in code is legal only when the set is large enough — that is, the estimate has accumulated sufficiently many facts.
The Called Methods Checker (Chapter 7) is an accumulation analysis. The Test Accumulation Checker is a simplified version of the Called Methods Checker that you can also use as a model.
Accumulation analysis is a special case of typestate analysis in which (1) the order in which operations are performed does not affect what is subsequently legal, and (2) the accumulation does not add restrictions; that is, as more operations are performed, more operations become legal. Unlike a traditional typestate analysis, an accumulation analysis does not require an alias analysis for soundness. It can therefore be implemented as a flow-sensitive type system.
The rest of this chapter assumes you have read how to create a checker (Chapter 37).
Defining type qualifiers Define 2 or 3 type qualifiers.
• The “accumulator” type qualifier has a single argument: a String[] named value that defaults to an empty array. Note that the Checker Framework’s support for accumulation analysis requires you to accumulate a string representation of whatever you are accumulating. For example,
when accumulating which methods have been called, you might choose to accumulate method names.
The accumulator qualifier should have no supertypes (@SubtypeOf({})) and should be the default qualifier in the hierarchy (@DefaultQualifierInHierarchy).
An example of such a qualifier can be found in the Checker Framework’s tests: TestAccumulation.java.
• Define a bottom type, analogous to TestAccumulationBottom.java. It should take no arguments, and should be a subtype of the accumulator type you defined earlier.
• Optionally, define a predicate annotation, analogous to TestAccumulationPredicate.java. It must have a single argument named value of type String. The predicate syntax supports
– || disjunctions
– && conjunctions
– ! logical complement. "!x" means “it is not true that x was definitely accumulated” or, equivalently, “there is some path on which x was not accumulated”. Note that this does not mean “x was not accumulated” — it is
not a violation of the specification "!x" if x is accumulated on some paths, but not others.
– (...) parentheses for precedence
Define a new class that extends AccumulationChecker. It does not need any content.
Define a new class that extends AccumulationAnnotatedTypeFactory. You must create a new constructor whose only argument is a BaseTypeChecker. Your constructor should call one of the super constructors defined in AccumulationAnnotatedTypeFactory (which one depends on whether or not you defined a predicate annotation).
Define a class that extends AccumulationTransfer. To update the estimate of what has been accumulated, override some method in CFAbstractTransfer to call accumulate.
For example, to accumulate the names of methods called, a checker would override CFAbstractTransfer.visitMethodInvocation to: call super to get a TransferResult, compute the method name from the MethodInvocationNode, and then call accumulate.
At this point, your checker ensures that all annotations are consistent with one another and the source code, and it flow-sensitively refines the annotations. To enforce properties in the code being type-checked, write type rules (Section 37.7) that are specific to your type system.
The paper “Accumulation Analysis” [KSSE22] describes theoretical properties of accumulation analysis. The papers “Verifying Object Construction” [KRS+20] and “Lightweight and modular resource leak verification” [KSSE21] describe specific accumulation analyses.