org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceScenesStorage

java.lang.Object

org.checkerframework.common.wholeprograminference.WholeProgramInferenceScenesStorage

public class WholeProgramInferenceScenesStorage
extends Object

This class stores annotations for fields, method return types, and method parameters.

The set of annotations inferred for a certain class is stored in an AScene, which writeScenes() can write into a file. For example, a class my.pakkage.MyClass will have its members' inferred types stored in a Scene, and later written into a file named my.pakkage.MyClass.jaif if using WholeProgramInference.OutputFormat.JAIF, or my.pakkage.MyClass.astub if using WholeProgramInference.OutputFormat.STUB.

This class populates the initial Scenes by reading existing .jaif files on the JAIF_FILES_PATH directory (regardless of output format). Having more information in those initial .jaif files means that the precision achieved by the whole-program inference analysis will be better. writeScenes(org.checkerframework.common.wholeprograminference.WholeProgramInference.OutputFormat, org.checkerframework.common.basetype.BaseTypeChecker) rewrites the initial .jaif files, and may create new ones.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	WholeProgramInferenceScenesStorage.AnnotationsInContexts Maps the toString() representation of an ATypeElement and its TypeUseLocation to a set of names of annotations.

Field Summary

Fields

Modifier and Type	Field and Description
static String	JAIF_FILES_PATH Directory where .jaif files will be written to and read from.

Constructor Summary

Constructors

Constructor and Description
WholeProgramInferenceScenesStorage(boolean ignoreNullAssignments) Default constructor.

Method Summary

Modifier and Type	Method and Description
protected scenelib.annotations.el.AClass	getAClass(@BinaryName String className, String jaifPath) Returns the scene-lib representation of the given className in the scene identified by the given jaifPath.
protected scenelib.annotations.el.AClass	getAClass(@BinaryName String className, String jaifPath, @Nullable com.sun.tools.javac.code.Symbol.ClassSymbol classSymbol) Returns the scene-lib representation of the given className in the scene identified by the given jaifPath.
protected String	getJaifPath(String className) Returns the String representing the .jaif path of a class given its name.
protected ASceneWrapper	getScene(String jaifPath) Reads a Scene from the given .jaif file, or returns an empty Scene if the file does not exist.
protected void	updateAnnotationSetInScene(scenelib.annotations.el.ATypeElement type, AnnotatedTypeFactory atf, String jaifPath, AnnotatedTypeMirror rhsATM, AnnotatedTypeMirror lhsATM, TypeUseLocation defLoc) Updates the set of annotations in a location of a Scene.
void	writeScenes(WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker) Write all modified scenes into files.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

JAIF_FILES_PATH

public static final String JAIF_FILES_PATH

Directory where .jaif files will be written to and read from. This directory is relative to where the CF's javac command is executed.

Constructor Detail

WholeProgramInferenceScenesStorage

public WholeProgramInferenceScenesStorage(boolean ignoreNullAssignments)

Default constructor.

Parameters:

ignoreNullAssignments - indicates whether assignments where the rhs is null should be ignored

Method Detail

writeScenes

public void writeScenes(WholeProgramInference.OutputFormat outputFormat,
                        BaseTypeChecker checker)

Write all modified scenes into files. (Scenes are modified by the method updateAnnotationSetInScene(scenelib.annotations.el.ATypeElement, org.checkerframework.framework.type.AnnotatedTypeFactory, java.lang.String, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.framework.qual.TypeUseLocation).)

Parameters:

outputFormat - the output format to use when writing files

checker - the checker from which this method is called, for naming stub files

getJaifPath

protected String getJaifPath(String className)

Returns the String representing the .jaif path of a class given its name.

Parameters:

className - the simple name of a class

Returns:

the path to the .jaif file

getScene

protected ASceneWrapper getScene(String jaifPath)

Reads a Scene from the given .jaif file, or returns an empty Scene if the file does not exist.

Parameters:

jaifPath - the .jaif file

Returns:

the Scene read from the file, or an empty Scene if the file does not exist

getAClass

protected scenelib.annotations.el.AClass getAClass(@BinaryName String className,
                                                   String jaifPath,
                                                   @Nullable com.sun.tools.javac.code.Symbol.ClassSymbol classSymbol)

Returns the scene-lib representation of the given className in the scene identified by the given jaifPath.

Parameters:

className - the name of the class to get, in binary form

jaifPath - the path to the jaif file that would represent that class (must end in ".jaif")

classSymbol - optionally, the ClassSymbol representing the class. Used to set the symbol information stored on an AClass.

Returns:

a version of the scene-lib representation of the class, augmented with symbol information if classSymbol was non-null

getAClass

protected scenelib.annotations.el.AClass getAClass(@BinaryName String className,
                                                   String jaifPath)

Returns the scene-lib representation of the given className in the scene identified by the given jaifPath.

Parameters:

className - the name of the class to get, in binary form

jaifPath - the path to the jaif file that would represent that class (must end in ".jaif")

Returns:

the scene-lib representation of the class, possibly augmented with symbol information if getAClass(String, String, com.sun.tools.javac.code.Symbol.ClassSymbol) has already been called with a non-null third argument

updateAnnotationSetInScene

protected void updateAnnotationSetInScene(scenelib.annotations.el.ATypeElement type,
                                          AnnotatedTypeFactory atf,
                                          String jaifPath,
                                          AnnotatedTypeMirror rhsATM,
                                          AnnotatedTypeMirror lhsATM,
                                          TypeUseLocation defLoc)

Updates the set of annotations in a location of a Scene.

• If there was no previous annotation for that location, then the updated set will be the annotations in rhsATM.
• If there was a previous annotation, the updated set will be the LUB between the previous annotation and rhsATM.

Parameters:

type - ATypeElement of the Scene which will be modified

atf - the annotated type factory of a given type system, whose type hierarchy will be used

jaifPath - used to identify a Scene

rhsATM - the RHS of the annotated type on the source code

lhsATM - the LHS of the annotated type on the source code

defLoc - the location where the annotation will be added