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, NotTaken, ParamLabel, PolicyLabel, RuntimeLabel, ThisLabel, TopLabel, UnknownLabel, VarLabel

All Known Implementing Classes:

ArgLabel_c, CovariantParamLabel_c, DynamicLabel_c, JoinLabel_c, Label_c, NotTaken_c, ParamLabel_c, PolicyLabel_c, RuntimeLabel_c, ThisLabel_c, TopLabel_c, UnknownLabel_c, VarLabel_c

public interface Label
extends Param

This class represents the Jif security label.

Method Summary

java.util.Collection	components() Retrieve the collection of components.
java.lang.String	componentString()
java.lang.String	componentString(java.util.Set printedLabels)
java.lang.String	description()
boolean	hasVariables() Does the label contain any variables, that is, labels of type VarLabel?
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	isSingleton() Does this label represent only a single label?
boolean	isTop() Is this label equivalent to top?
Label	join(Label L) Returns the join of this label and L.
PathMap	labelCheck(JifContext A) 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
void	setDescription(java.lang.String d)
Label	simplify()
Label	singletonComponent() Retrieve the singleton component that this label represents.
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	variables() The set of variables that this contains, i.e., labels of type VarLabel?

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?

join

Label join(Label L)

Returns the join of this label and L.

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)

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)

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?

components

java.util.Collection components()

Retrieve the collection of components. This method should only be called if isEnumerable returns true. This collection should not be modified.

isSingleton

boolean isSingleton()

Does this label represent only a single label?

For example, a JoinLabel with more than one component returns false, a MeetLabel with more than one component returns false, most other Labels return true.

singletonComponent

Label singletonComponent()

Retrieve the singleton component that this label represents. Should only be called is isSingleton returns true.

simplify

Label simplify()

hasVariables

boolean hasVariables()

Does the label contain any variables, that is, labels of type VarLabel?

variables

java.util.Set variables()

The set of variables that this contains, i.e., labels of type VarLabel?

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

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)