escjava.tc
Class FlowInsensitiveChecks

java.lang.Object
  javafe.tc.FlowInsensitiveChecks
      escjava.tc.FlowInsensitiveChecks

public class FlowInsensitiveChecks

extends FlowInsensitiveChecks

Field Summary

protected static int	ACC_LOW_BOUND_Package
protected static int	ACC_LOW_BOUND_Private
protected static int	ACC_LOW_BOUND_Protected
protected static int	ACC_LOW_BOUND_Public
protected ASTNode	accessibilityContext If accessibilityLowerBound !
protected int	accessibilityLowerBound
AnnotationHandler	annotationHandler
protected int	countFreeVarsAccesses Counts the number of accesses of free variables and fields used for checking the appropriateness of invariants.
static ASTDecoration	envDecoration
static boolean	inAnnotation Are we in the middle of processing an annotation?
static boolean	inModelBody
protected boolean	invariantContext Indicates whether we are are checking an invariant pragma.
protected boolean	isInsidePRE Indicates whether checking is currently being done inside a PRE.
protected boolean	isLocksetContext Indicates whether LS is allowed in this context.
protected boolean	isPredicateContext Indicates whether a quantification or labeled predicate is allowed in this context.
protected boolean	isPrivateFieldAccessAllowed Indicates whether private field accesses are allowed in the current context.
protected boolean	isRESContext \result is allowed in this context when isRESContext is true and returnType !
protected boolean	isSpecDesignatorContext Acts as a parameter to checkExpr.
protected boolean	isTwoStateContext Indicates whether \old and \fresh are allowed in this context.
protected ExprStmtPragmaVec	loopDecreases Contains the loop decreases statement pragmas seen so far and not yet processed.
protected ExprStmtPragmaVec	loopInvariants Contains the loop invariant statement pragmas seen so far and not yet processed.
protected ExprStmtPragmaVec	loopPredicates
static int	MSTATUS_CLASS_NEW_METHOD
static int	MSTATUS_NEW_ROUTINE
static int	MSTATUS_OVERRIDE
protected LocalVarDeclVec	skolemConstants
static ASTDecoration	staticenvDecoration

Fields inherited from class javafe.tc.FlowInsensitiveChecks

allowedExceptions, dontAddImplicitConstructorInvocations, enclosingLabels, inst, leftToRight, returnType, rootIEnv, rootSEnv, sig, useUniverses

Constructor Summary

FlowInsensitiveChecks()

Method Summary

protected boolean	assignmentConvertable(Expr e, Type t) Checks if Exp e can be assigned to Type t.
protected Expr	checkExpr(Env env, Expr e) Typechecks expressions.
protected void	checkLoopDecreases(Env env, boolean allowed)
protected void	checkLoopInvariants(Env env, boolean allowed)
protected void	checkLoopPredicates(Env env, boolean allowed)
protected Env	checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env) Hook to do additional processing on Modifiers.
protected Expr	checkPredicate(Env env, Expr e)
protected Env	checkSkolemConstants(Env env, boolean allowed)
protected Env	checkStmt(Env env, Stmt s) Typecheck a statement in a given environment then return the environment in effect for statements that follow the given statement.
protected Env	checkStmtPragma(Env e, StmtPragma s)
void	checkTypeDeclaration(TypeSig s) Moves s into implementation checked state.
protected void	checkTypeDeclElem(TypeDeclElem e)
protected void	checkTypeDeclElemPragma(TypeDeclElemPragma e)
static void	copyType(VarInit from, VarInit to) Copy the Type associated with an expression by the typechecking pass to another Expr.
private void	errorExpectingLoop(int loc, int tag)
protected int	getAccessibility(int modifiers)
static Set	getAllOverrides(MethodDecl md)
static Set	getDirectOverrides(MethodDecl md)
static int	getOverrideStatus(RoutineDecl rd)
static MethodDecl	getSuperClassOverride(MethodDecl md)
static MethodDecl	getSuperNonNullStatus(RoutineDecl rd, int j)
static MethodDecl	getSuperNonNullStatus(RoutineDecl rd, int j, Set directOverrides)
static FlowInsensitiveChecks	inst()
int	isGhost(Expr t) Returns non-zero if the expression is a ghost expression - that is, it would not exist if all ghost declarations were removed.
int	isGhost(ObjectDesignator od)
static boolean	isMethodOverride(RoutineDecl rd)
static boolean	isOverridable(MethodDecl md)
protected boolean	isPure(RoutineDecl rd)
protected EnvForTypeSig	makeEnvForTypeSig(TypeSig s, boolean staticContext) Override so that we use GhostEnv instead of EnvForTypeSig.

Methods inherited from class javafe.tc.FlowInsensitiveChecks

checkAmbiguousMethodInvocationExpr, checkAmbiguousVariableAccessExpr, checkArrayRefExpr, checkAssignmentExpr, checkBinaryExpr, checkBinaryExpr, checkBitnotExpr, checkBooleanLitExpr, checkCastExpr, checkCharLitExpr, checkClassDeclStmt, checkClassLiteralExpr, checkCondExpr, checkDesignator, checkDoubleLitExpr, checkExpr, checkExprVec, checkFieldAccessExpr, checkFieldDecl, checkFloatLitExpr, checkForLoopAfterInit, checkIncDecExpr, checkInit, checkInstanceOfExpr, checkIntLitExpr, checkLongLitExpr, checkMethodInvocationExpr, checkModifierPragmaVec, checkNewArrayExpr, checkNewInstanceExpr, checkNoRepInStaticContext, checkNotExpr, checkNullLitExpr, checkObjectDesignator, checkParenExpr, checkSignExpr, checkStmtVec, checkStringLitExpr, checkSwitchStmt, checkThisExpr, checkTypeModifierPragma, checkTypeModifierPragmaVec, checkTypeModifiers, checkUniverseAssignability, checkUniverseCastability, checkUniverseForField, checkVarDeclStmt, checkVariableAccessExpr, copyUniverses, determineUniverseForArrayRefExpr, determineUniverseForFieldAccess, determineUniverseForMethodInvocation, getType, getTypeOrNull, leastUpperUniverseBound, reportLookupException, setType, universeIsSubtypeOf, universeTypeCombiner, universeTypeCombiner

Methods inherited from class java.lang.Object

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

Field Detail

inAnnotation

public static boolean inAnnotation

Are we in the middle of processing an annotation? (Used by GhostEnv.)

inModelBody

public static boolean inModelBody

annotationHandler

public AnnotationHandler annotationHandler

isLocksetContext

protected boolean isLocksetContext

Indicates whether LS is allowed in this context. The default is true. For contexts where LS is not allowed, isLocksetContext should be set false only temporarily.

isRESContext

protected boolean isRESContext

\result is allowed in this context when isRESContext is true and returnType != null. The default value of isRESContext is false. For contexts where isRESContext should be true, isRESContext should be set to true only temporarily.

isTwoStateContext

protected boolean isTwoStateContext

Indicates whether \old and \fresh are allowed in this context. The default is false. For contexts where these functions are allowed, isTwoStateContext should be set true only temporarily.

isInsidePRE

protected boolean isInsidePRE

Indicates whether checking is currently being done inside a PRE. This is used by the code that disallows nested PRE expressions. Note: alternatively, one could use isTwoStateContext to implement this functionality, but by having a separate bit, a more precise error message can be produced.

isPredicateContext

protected boolean isPredicateContext

Indicates whether a quantification or labeled predicate is allowed in this context. This boolean is used only between one call of checkExpr to a following recursive call.

isPrivateFieldAccessAllowed

protected boolean isPrivateFieldAccessAllowed

Indicates whether private field accesses are allowed in the current context. Private field accesses are allowed everywhere, except in postconditions of overridable methods.

accessibilityLowerBound

protected int accessibilityLowerBound

ACC_LOW_BOUND_Private

protected static final int ACC_LOW_BOUND_Private

See Also:

Constant Field Values

ACC_LOW_BOUND_Package

protected static final int ACC_LOW_BOUND_Package

See Also:

Constant Field Values

ACC_LOW_BOUND_Protected

protected static final int ACC_LOW_BOUND_Protected

See Also:

Constant Field Values

ACC_LOW_BOUND_Public

protected static final int ACC_LOW_BOUND_Public

See Also:

Constant Field Values

accessibilityContext

protected ASTNode accessibilityContext

If accessibilityLowerBound != ACC_LOW_BOUND_Private, then accessibilityContext is the field or routine whose modifier pragma is being type checked.

isSpecDesignatorContext

protected boolean isSpecDesignatorContext

Acts as a parameter to checkExpr. Its value is meaningful only on entry to checkExpr. It indicates whether the expression to be checked is in a specification designator context. In particular, this parameter is used to disallow array index wild cards in non-spec designator contexts.

loopInvariants

protected ExprStmtPragmaVec loopInvariants

Contains the loop invariant statement pragmas seen so far and not yet processed.

loopDecreases

protected ExprStmtPragmaVec loopDecreases

Contains the loop decreases statement pragmas seen so far and not yet processed.

loopPredicates

protected ExprStmtPragmaVec loopPredicates

skolemConstants

protected LocalVarDeclVec skolemConstants

invariantContext

protected boolean invariantContext

Indicates whether we are are checking an invariant pragma.

countFreeVarsAccesses

protected int countFreeVarsAccesses

Counts the number of accesses of free variables and fields used for checking the appropriateness of invariants.

envDecoration

public static ASTDecoration envDecoration

staticenvDecoration

public static ASTDecoration staticenvDecoration

MSTATUS_NEW_ROUTINE

public static final int MSTATUS_NEW_ROUTINE

See Also:

Constant Field Values

MSTATUS_CLASS_NEW_METHOD

public static final int MSTATUS_CLASS_NEW_METHOD

See Also:

Constant Field Values

MSTATUS_OVERRIDE

public static final int MSTATUS_OVERRIDE

See Also:

Constant Field Values

Constructor Detail

FlowInsensitiveChecks

public FlowInsensitiveChecks()

Method Detail

inst

public static FlowInsensitiveChecks inst()

makeEnvForTypeSig

protected EnvForTypeSig makeEnvForTypeSig(TypeSig s,
                                          boolean staticContext)

Override so that we use GhostEnv instead of EnvForTypeSig.

Overrides:

makeEnvForTypeSig in class FlowInsensitiveChecks

checkTypeDeclaration

public void checkTypeDeclaration(TypeSig s)

Description copied from class: FlowInsensitiveChecks

Moves s into implementation checked state.

Overrides:

checkTypeDeclaration in class FlowInsensitiveChecks

checkTypeDeclElem

protected void checkTypeDeclElem(TypeDeclElem e)

Overrides:

checkTypeDeclElem in class FlowInsensitiveChecks

checkStmt

protected Env checkStmt(Env env,
                        Stmt s)

Description copied from class: FlowInsensitiveChecks

Typecheck a statement in a given environment then return the environment in effect for statements that follow the given statement.

(The returned environment will be the same as the one passed in unless the statement is a declaration.)

Overrides:

checkStmt in class FlowInsensitiveChecks

checkLoopInvariants

protected void checkLoopInvariants(Env env,
                                   boolean allowed)

checkLoopDecreases

protected void checkLoopDecreases(Env env,
                                  boolean allowed)

checkLoopPredicates

protected void checkLoopPredicates(Env env,
                                   boolean allowed)

checkSkolemConstants

protected Env checkSkolemConstants(Env env,
                                   boolean allowed)

errorExpectingLoop

private void errorExpectingLoop(int loc,
                                int tag)

checkPredicate

protected Expr checkPredicate(Env env,
                              Expr e)

checkExpr

protected Expr checkExpr(Env env,
                         Expr e)

Description copied from class: FlowInsensitiveChecks

Typechecks expressions. Work is delegated to specialized methods. This way the clients that inherit from this class have a finer grained control by overriding methods.

Overrides:

checkExpr in class FlowInsensitiveChecks

Parameters:

env - The current environment.

e - The expression to typecheck.

Returns:

The checked expression. It has the type set.

checkTypeDeclElemPragma

protected void checkTypeDeclElemPragma(TypeDeclElemPragma e)

Overrides:

checkTypeDeclElemPragma in class FlowInsensitiveChecks

checkModifierPragma

protected Env checkModifierPragma(ModifierPragma p,
                                  ASTNode ctxt,
                                  Env env)

Description copied from class: FlowInsensitiveChecks

Hook to do additional processing on Modifiers. The ASTNode is the parent of the ModifierPragma, and env is the current environment.

Overrides:

checkModifierPragma in class FlowInsensitiveChecks

Returns:

true if pragma should be deleted

isOverridable

public static boolean isOverridable(MethodDecl md)

Returns:

whether or not md can be overridden in some possible subclass.

getAccessibility

protected int getAccessibility(int modifiers)

Returns:

a value appropriate for assignment to accessibilityLowerBound, given member modifiers.

checkStmtPragma

protected Env checkStmtPragma(Env e,
                              StmtPragma s)

Overrides:

checkStmtPragma in class FlowInsensitiveChecks

copyType

public static void copyType(VarInit from,
                            VarInit to)

Copy the Type associated with an expression by the typechecking pass to another Expr. This is used by Substitute to ensure it returns an Expr of the same Type.

getAllOverrides

public static Set getAllOverrides(MethodDecl md)

Returns:

a set of *all* the methods a given method overrides. This includes transitivity.

getDirectOverrides

public static Set getDirectOverrides(MethodDecl md)

getSuperClassOverride

public static MethodDecl getSuperClassOverride(MethodDecl md)

Returns:

If md is a method that overrides a method in a superclass, the overridden method is returned. Otherwise, if md overrides a method in an interface, such a method is returned. Otherwise, null is returned.

isMethodOverride

public static boolean isMethodOverride(RoutineDecl rd)

Returns:

whether or not rd is a method override declaration, that is, whether or not rd overrides a method declared in a superclass or superinterface.

getOverrideStatus

public static int getOverrideStatus(RoutineDecl rd)

Returns:

MSTATUS_NEW_ROUTINE if rd is a routine that doesn't override any other method. This includes the case where rd is a constructor or a static method.

Returns MSTATUS_CLASS_NEW_METHOD if rd is a method declared in a class, doesn't override any method in any superclass, but overrides a method in an interface.

Otherwise, returns MSTATUS_OVERRIDE.

getSuperNonNullStatus

public static MethodDecl getSuperNonNullStatus(RoutineDecl rd,
                                               int j)

Returns:

null if method md is allowed to declare its jth (counting from 0) formal parameter as non_null. That is the case if the method does not override anything, or if in everything that it does override that parameter is declared non_null. Otherwise returns the MethodDecl corresponding to the overridden method with which the argument rd is in conflict.

Todo:

kiniry - implement nullable versions of this or make two new methods

getSuperNonNullStatus

public static MethodDecl getSuperNonNullStatus(RoutineDecl rd,
                                               int j,
                                               Set directOverrides)

isGhost

public int isGhost(Expr t)

Returns non-zero if the expression is a ghost expression - that is, it would not exist if all ghost declarations were removed. Otherwise returns a Location value of a relevant non-ghost declaration.

isGhost

public int isGhost(ObjectDesignator od)

assignmentConvertable

protected boolean assignmentConvertable(Expr e,
                                        Type t)

Description copied from class: FlowInsensitiveChecks

Checks if Exp e can be assigned to Type t. This method is here instead of in Types, because it needs to mess with constants.

Overrides:

assignmentConvertable in class FlowInsensitiveChecks

isPure

protected boolean isPure(RoutineDecl rd)

Overrides:

isPure in class FlowInsensitiveChecks