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 aTypeElementToString(scenelib.annotations.el.ATypeElement) representation of an ATypeElement and its TypeUseLocation to a set of names of annotations.

Field Summary

Fields

Modifier and Type	Field and Description
protected AnnotatedTypeFactory	atypeFactory The type factory associated with this WholeProgramInferenceScenesStorage.
static String	JAIF_FILES_PATH Directory where .jaif files will be written to and read from.
Set<String>	modifiedScenes Scenes that were modified since the last time all Scenes were written into .jaif files.
Map<String,ASceneWrapper>	scenes Maps .jaif file paths (Strings) to Scenes.

Constructor Summary

Constructors

Constructor and Description
WholeProgramInferenceScenesStorage(AnnotatedTypeFactory atypeFactory, boolean ignoreNullAssignments) Default constructor.

Method Summary

Modifier and Type	Method and Description
AnnotatedTypeMirror	atmFromATypeElement(TypeMirror typeMirror, scenelib.annotations.el.ATypeElement type) Obtain the type from an ATypeElement (which is part of a Scene).
static String	aTypeElementToString(scenelib.annotations.el.ATypeElement aType) Returns a string representation of an ATypeElement, for use as part of a key in WholeProgramInferenceScenesStorage.AnnotationsInContexts.
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, TypeUseLocation defLoc, AnnotatedTypeMirror rhsATM, AnnotatedTypeMirror lhsATM, String jaifPath, boolean ignoreIfAnnotated) Updates the set of annotations in a location of a Scene, as the result of a pseudo-assignment.
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

atypeFactory

protected final AnnotatedTypeFactory atypeFactory

The type factory associated with this WholeProgramInferenceScenesStorage.

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.

scenes

public final Map<String,ASceneWrapper> scenes

Maps .jaif file paths (Strings) to Scenes. Relative to JAIF_FILES_PATH.

modifiedScenes

public final Set<String> modifiedScenes

Scenes that were modified since the last time all Scenes were written into .jaif files. Each String element of this set is a path (relative to JAIF_FILES_PATH) to the .jaif file of the corresponding Scene in the set. It is obtained by passing a class name as argument to the getJaifPath(java.lang.String) method.

Modifying a Scene means adding (or changing) a type annotation for a field, method return type, or method parameter type in the Scene. (Scenes are modified by the method updateAnnotationSetInScene(scenelib.annotations.el.ATypeElement, org.checkerframework.framework.qual.TypeUseLocation, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.framework.type.AnnotatedTypeMirror, java.lang.String, boolean).)

Constructor Detail

WholeProgramInferenceScenesStorage

public WholeProgramInferenceScenesStorage(AnnotatedTypeFactory atypeFactory,
                                          boolean ignoreNullAssignments)

Default constructor.

Parameters:

ignoreNullAssignments - if true, assignments where the rhs is null are ignored

atypeFactory - the type factory associated with this WholeProgramInferenceScenesStorage

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.qual.TypeUseLocation, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.framework.type.AnnotatedTypeMirror, java.lang.String, boolean).)

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,
                                          TypeUseLocation defLoc,
                                          AnnotatedTypeMirror rhsATM,
                                          AnnotatedTypeMirror lhsATM,
                                          String jaifPath,
                                          boolean ignoreIfAnnotated)

Updates the set of annotations in a location of a Scene, as the result of a pseudo-assignment.

• 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

jaifPath - path to a .jaif file for a Scene; used for marking the scene as modified (needing to be written to disk)

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

ignoreIfAnnotated - if true, don't update any type that is explicitly annotated in the source code

atmFromATypeElement

public AnnotatedTypeMirror atmFromATypeElement(TypeMirror typeMirror,
                                               scenelib.annotations.el.ATypeElement type)

Obtain the type from an ATypeElement (which is part of a Scene).

Parameters:

typeMirror - the underlying type for the result

type - the ATypeElement from which to obtain annotations

Returns:

an annotated type mirror with underlying type typeMirror and annotations from type

aTypeElementToString

public static String aTypeElementToString(scenelib.annotations.el.ATypeElement aType)

Returns a string representation of an ATypeElement, for use as part of a key in WholeProgramInferenceScenesStorage.AnnotationsInContexts.

Parameters:

aType - an ATypeElement to convert to a string representation

Returns:

a string representation of the argument