jif.types.label
Interface Label

All Superinterfaces:

java.lang.Cloneable, polyglot.util.Copy, Param, java.io.Serializable, polyglot.types.TypeObject

All Known Subinterfaces:

ArgLabel, CovariantParamLabel, DynamicLabel, JoinLabel, MeetLabel, NotTaken, PairLabel, ParamLabel, ThisLabel, UnknownLabel, VarLabel, WritersToReadersLabel

All Known Implementing Classes:

ArgLabel_c, CovariantParamLabel_c, DynamicLabel_c, JoinLabel_c, Label_c, MeetLabel_c, NotTaken_c, PairLabel_c, ParamLabel_c, ThisLabel_c, UnknownLabel_c, VarLabel_c, WritersToReadersLabel_c

public interface Label
extends Param

This class represents the Jif security label.

Method Summary

java.lang.String	componentString()
java.lang.String	componentString(java.util.Set printedLabels)
ConfPolicy	confProjection()
java.lang.String	description()
boolean	hasVariableComponents() Does the label contain any variables as components? This does not include variables that are in bounds of arg labels.
boolean	hasVariables() Does the label contain any variables at all? This includes variables that are in bounds of arg labels.
boolean	hasWritersToReaders() Does the label contain any writersToReaders constructs?
IntegPolicy	integProjection()
boolean	isBottom() Is this label equivalent to bottom?
boolean	isComparable() Is this label comparable to other labels?
boolean	isCovariant() Is this label covariant?
boolean	isDisambiguated() Are the components of this label all disambiguated?
boolean	isEnumerable() Are the components of this label enumerable?
boolean	isInvariant() Is this label invariant?
boolean	isRuntimeRepresentable()
boolean	isTop() Is this label equivalent to top?
PathMap	labelCheck(JifContext A, LabelChecker lc) Label check the label, which will determine how much information may be gained if the label is evaluated at runtime.
boolean	leq_(Label L, LabelEnv H, LabelEnv.SearchState state) Implementation of leq, should only be called by JifTypeSystem
Label	normalize() Normalize the label.
void	setDescription(java.lang.String d)
Label	simplify() Simplify the label, using leq if needed
Label	subst(LabelSubstitution labelSubst)
java.util.List	throwTypes(polyglot.types.TypeSystem ts) If the label is runtime representable, when it is evaluated at runtime it may throw exceptions.
polyglot.ast.Expr	toJava(JifToJavaRewriter rw)
java.lang.String	toString(java.util.Set printedLabels)
java.util.Set	variableComponents() The set of variables that this label contains as components.
java.util.Set	variables() The set of variables that this label contains including variables contained in upper bounds of arg labels.

Methods inherited from interface jif.types.Param

isCanonical

Methods inherited from interface polyglot.types.TypeObject

equalsImpl, position, typeSystem

Methods inherited from interface polyglot.util.Copy

copy

Method Detail

isBottom

boolean isBottom()

Is this label equivalent to bottom?

For example, a JoinLabel with no components would return true for this method.

isTop

boolean isTop()

Is this label equivalent to top?

For example, a JoinLabel with two components, one of which is Top, would return true for this method.

isInvariant

boolean isInvariant()

Is this label invariant?

isCovariant

boolean isCovariant()

Is this label covariant?

isComparable

boolean isComparable()

Is this label comparable to other labels?

For example, an UnknownLabel is not comparable to others, neither is a VarLabel. Most other labels are.

description

java.lang.String description()

setDescription

void setDescription(java.lang.String d)

subst

Label subst(LabelSubstitution labelSubst)
            throws polyglot.types.SemanticException

Parameters:

labelSubst - The LabelSubstitution to apply to this label

Returns:

the result of applying labelSubst to this label.

Throws:

polyglot.types.SemanticException

labelCheck

PathMap labelCheck(JifContext A,
                   LabelChecker lc)

Label check the label, which will determine how much information may be gained if the label is evaluated at runtime. For example, given the dynamic label {*lb}, where lb is a local variable, evaluation of this label at runtime will reveal as much information as the label of lb. For example, the following code is illegal, as the runtime evaluation of the label reveals too much information

 
  boolean{Alice:} secret = ...;
  final label{Alice:} lb = secret?new label{}:new label{Bob:};
  boolean{} leak = false;
  if ((*lb} <= new label{}) { // evaluation of lb reveals 
                           // information at level {Alice:} 
     leak = true;
  } 
  
 

See Also:

Jif.labelCheck(LabelChecker), Principal.labelCheck(JifContext, LabelChecker)

isEnumerable

boolean isEnumerable()

Are the components of this label enumerable?

For example, Singletons are enumerable, JoinLabels are enumerable, RuntimeLabel (the label of all runtime representable components) is not enumerable. NOTE: The components of a label are not neccessarily stuck together with a join operation. For example, the MeetLabel uses the meet operation between its components.

isDisambiguated

boolean isDisambiguated()

Are the components of this label all disambiguated?

simplify

Label simplify()

Simplify the label, using leq if needed

normalize

Label normalize()

Normalize the label. Essentially, simplify as much as possible without using the leq ordering

hasWritersToReaders

boolean hasWritersToReaders()

Does the label contain any writersToReaders constructs?

hasVariableComponents

boolean hasVariableComponents()

Does the label contain any variables as components? This does not include variables that are in bounds of arg labels.

hasVariables

boolean hasVariables()

Does the label contain any variables at all? This includes variables that are in bounds of arg labels.

variableComponents

java.util.Set variableComponents()

The set of variables that this label contains as components. This is a subset of variables(), since it does not count var labels contained in upper bounds of arg labels.

variables

java.util.Set variables()

The set of variables that this label contains including variables contained in upper bounds of arg labels.

leq_

boolean leq_(Label L,
             LabelEnv H,
             LabelEnv.SearchState state)

Implementation of leq, should only be called by JifTypeSystem

Parameters:

L - the label to determine if this label is leq to. This label always satisfies !this.equals(L)

H - the label environment (including principal hierarchy). Will always be non-null.

isRuntimeRepresentable

boolean isRuntimeRepresentable()

Specified by:

isRuntimeRepresentable in interface Param

confProjection

ConfPolicy confProjection()

integProjection

IntegPolicy integProjection()

throwTypes

java.util.List throwTypes(polyglot.types.TypeSystem ts)

If the label is runtime representable, when it is evaluated at runtime it may throw exceptions. This method returns a list of the exceptions that the runtime evaluation of the label may produce. If the label cannot be evaluated at runtime, an empty list should be returned.

toJava

polyglot.ast.Expr toJava(JifToJavaRewriter rw)
                         throws polyglot.types.SemanticException

Throws:

polyglot.types.SemanticException

componentString

java.lang.String componentString()

componentString

java.lang.String componentString(java.util.Set printedLabels)

toString

java.lang.String toString(java.util.Set printedLabels)