jif.types
Interface JifContext

All Superinterfaces:
java.lang.Cloneable, polyglot.types.Context, polyglot.util.Copy, polyglot.types.Resolver
All Known Implementing Classes:
JifContext_c

public interface JifContext
extends polyglot.types.Context

The context for Jif type checking. JifContext extends Context with contextual information needed for checking labels, and also with some utility methods to assist in the implementation of label checking. The JifContext object contains a label environment, which contains a principal hierarchy; most access to these objects should be through the JifContext object, for example, the methods addActsFor, actsFor, addContraintLE.


Method Summary
 void addActsFor(Principal p1, Principal p2)
          Add an actsfor relation to the principal hierarchy.
 void addAssertionLE(Label L1, Label L2)
          Add a less than or equal assertion to the label environment.
 void addCheckedEndorse(polyglot.types.LocalInstance li, Label downgradeTo)
          Add a checked endorse for the local instance li.
 void addDefinitionalAssertionEquiv(AccessPath p, AccessPath q)
          Adds the assertion that the access path p is equivalent to the access path q to this context, and all outer contexts up to the method/constructor/initializer level
 void addDefinitionalAssertionEquiv(Label L1, Label L2)
          Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level
 void addDefinitionalAssertionEquiv(Label L1, Label L2, boolean addToClass)
          Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level.
 void addDefinitionalEquiv(Principal p1, Principal p2)
          Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level
 void addEquiv(AccessPath p, AccessPath q)
          Adds the assertion that the access path p is equivalent to the access path q to this context
 void addEquiv(Label L1, Label L2)
          Add an equivalence to the label environment.
 void addEquiv(Principal p1, Principal p2)
          Add an actsfor relation both ways to the principal hierarchy.
 Label authLabel()
          Get the authority of the current code, represented as a confidentiality label.
 Label authLabelInteg()
          Get the authority of the current code, represented as an integrity label.
 java.util.Set authority()
          The authority of a class or a procedure is the set of principals who have authorized that code.
 boolean checkingInits()
          Indicates if we are currently checking the initializers within a constructor.
 void clearPH()
          Clears the principal hierarchy of all actsfor relations.
 Label constructorReturnLabel()
          If the current code is a constructor, returns the return label of that constructor.
 Label currentCodePCBound()
          The currentCodePCBound is an upper bound on the PC of the caller of the current code, and a lower bound on the observable effects of the current code.
 Label gotoLabel(polyglot.ast.Branch.Kind kind, java.lang.String label)
          Retrieve the Label associated with branching to the location label, with the branch kind kind.
 void gotoLabel(polyglot.ast.Branch.Kind kind, java.lang.String label, Label L)
          Record the Label associated with branching to the location label, with the branch kind kind.
 boolean inConstructorCall()
          Is the Context in a constructor call, e.g.
 LabelEnv labelEnv()
           
 PathMap pathMapForLocal(polyglot.types.LocalInstance li, LabelChecker lc)
          Return the path map for evaluating a local variable
 Label pc()
           
 PrincipalHierarchy ph()
           
 polyglot.types.Context pushConstructorCall()
          Push a Context onto the stack for a constructor call, e.g.
 void setAuthority(java.util.Set authority)
           
 void setCheckingInits(boolean checkingInits)
          Set whether we are currently checking the initializers within a constructor.
 void setConstructorReturnLabel(Label Lr)
           
 void setCurrentCodePCBound(Label label)
           
 void setPc(Label label, LabelChecker lc)
           
 boolean updateAllowed(polyglot.ast.Expr e)
          Can this expression be updated, e.g.
 
Methods inherited from interface polyglot.types.Context
addMethod, addNamed, addVariable, currentClass, currentClassScope, currentCode, definingCodeDef, findField, findFieldScope, findLocal, findMethod, findMethodScope, findVariable, findVariableSilent, importTable, inCode, inStaticContext, isLocal, outerResolver, package_, pop, pushBlock, pushClass, pushCode, pushSource, pushStatic, typeSystem
 
Methods inherited from interface polyglot.types.Resolver
find
 
Methods inherited from interface polyglot.util.Copy
copy
 

Method Detail

labelEnv

LabelEnv labelEnv()

addAssertionLE

void addAssertionLE(Label L1,
                    Label L2)
Add a less than or equal assertion to the label environment.


addEquiv

void addEquiv(Label L1,
              Label L2)
Add an equivalence to the label environment.


addDefinitionalAssertionEquiv

void addDefinitionalAssertionEquiv(Label L1,
                                   Label L2)
Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level

Parameters:
L1 -
L2 -

addDefinitionalAssertionEquiv

void addDefinitionalAssertionEquiv(Label L1,
                                   Label L2,
                                   boolean addToClass)
Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level. If addToClass is true, then the definition will also be added to the class. This should only be used for assignments to final fields.

Parameters:
L1 -
L2 -

addEquiv

void addEquiv(AccessPath p,
              AccessPath q)
Adds the assertion that the access path p is equivalent to the access path q to this context


addDefinitionalAssertionEquiv

void addDefinitionalAssertionEquiv(AccessPath p,
                                   AccessPath q)
Adds the assertion that the access path p is equivalent to the access path q to this context, and all outer contexts up to the method/constructor/initializer level


ph

PrincipalHierarchy ph()

addActsFor

void addActsFor(Principal p1,
                Principal p2)
Add an actsfor relation to the principal hierarchy.


addEquiv

void addEquiv(Principal p1,
              Principal p2)
Add an actsfor relation both ways to the principal hierarchy.


addDefinitionalEquiv

void addDefinitionalEquiv(Principal p1,
                          Principal p2)
Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level


clearPH

void clearPH()
Clears the principal hierarchy of all actsfor relations.


pc

Label pc()

setPc

void setPc(Label label,
           LabelChecker lc)

currentCodePCBound

Label currentCodePCBound()
The currentCodePCBound is an upper bound on the PC of the caller of the current code, and a lower bound on the observable effects of the current code.


setCurrentCodePCBound

void setCurrentCodePCBound(Label label)

gotoLabel

Label gotoLabel(polyglot.ast.Branch.Kind kind,
                java.lang.String label)
                throws polyglot.types.SemanticException
Retrieve the Label associated with branching to the location label, with the branch kind kind.

Throws:
polyglot.types.SemanticException

gotoLabel

void gotoLabel(polyglot.ast.Branch.Kind kind,
               java.lang.String label,
               Label L)
Record the Label associated with branching to the location label, with the branch kind kind.


authority

java.util.Set authority()
The authority of a class or a procedure is the set of principals who have authorized that code.


setAuthority

void setAuthority(java.util.Set authority)

authLabel

Label authLabel()
Get the authority of the current code, represented as a confidentiality label.


authLabelInteg

Label authLabelInteg()
Get the authority of the current code, represented as an integrity label.


checkingInits

boolean checkingInits()
Indicates if we are currently checking the initializers within a constructor. If we are, then more permissive label checking can be used for field assignments.


setCheckingInits

void setCheckingInits(boolean checkingInits)
Set whether we are currently checking the initializers within a constructor.


constructorReturnLabel

Label constructorReturnLabel()
If the current code is a constructor, returns the return label of that constructor. The value returned is only valid if checkingInits is true, and is used for more permissive label checking for field assignments.


setConstructorReturnLabel

void setConstructorReturnLabel(Label Lr)

pushConstructorCall

polyglot.types.Context pushConstructorCall()
Push a Context onto the stack for a constructor call, e.g. "super(...)" or "this(...)". Jif needs to distinguish constructor call contexts from other static contexts because the this label may appear in constructor call contexts, but not other static contexts.


inConstructorCall

boolean inConstructorCall()
Is the Context in a constructor call, e.g. "super(...)" or "this(...)"?


pathMapForLocal

PathMap pathMapForLocal(polyglot.types.LocalInstance li,
                        LabelChecker lc)
Return the path map for evaluating a local variable


updateAllowed

boolean updateAllowed(polyglot.ast.Expr e)
Can this expression be updated, e.g. is "e++" or "e = e'" allowed?


addCheckedEndorse

void addCheckedEndorse(polyglot.types.LocalInstance li,
                       Label downgradeTo)
Add a checked endorse for the local instance li.