jif.types.hierarchy
Class LabelEnv_c

java.lang.Object
  jif.types.hierarchy.LabelEnv_c

All Implemented Interfaces:

LabelEnv

public class LabelEnv_c
extends java.lang.Object
implements LabelEnv

The wrapper of a set of assumptions that can be used to decide whether L1 <= L2.

Nested Class Summary

Nested classes/interfaces inherited from interface jif.types.hierarchy.LabelEnv

LabelEnv.SearchState

Field Summary

protected java.util.Map<AccessPath,AccessPath>	accessPathEquivReps A map from AccessPath to representatives of the equivalent set of the AcessPath.
protected java.lang.StringBuffer	displayLabelAssertions
protected boolean	hasVariables Do any of the assertions have variables in them?
protected java.util.List<LabelLeAssertion_c>	labelAssertions
protected LabelEnv_c	parent
protected PrincipalHierarchy	ph
protected Solver	solver
protected static java.util.Collection	topics Topics to report
protected JifTypeSystem	ts
protected boolean	useCache

Constructor Summary

	LabelEnv_c(JifTypeSystem ts, boolean useCache)
protected	LabelEnv_c(JifTypeSystem ts, PrincipalHierarchy ph, java.util.List<LabelLeAssertion_c> assertions, java.lang.String displayLabelAssertions, boolean hasVariables, boolean useCache, java.util.Map<AccessPath,AccessPath> accessPathEquivReps, LabelEnv_c parent)

Method Summary

boolean	actsFor(Principal p, Principal q)
void	addActsFor(Principal p1, Principal p2)
void	addAssertionLE(Label L1, Label L2)
void	addEquiv(AccessPath p, AccessPath q)
void	addEquiv(Label L1, Label L2)
void	addEquiv(Principal p1, Principal p2)
protected void	cacheResult(jif.types.hierarchy.LabelEnv_c.LeqGoal g, LabelEnv.SearchState s, boolean result)
protected java.lang.Boolean	checkCache(jif.types.hierarchy.LabelEnv_c.LeqGoal g)
LabelEnv_c	copy()
java.util.Map<java.lang.String,java.util.List<java.lang.String>>	definitions(VarMap bounds, java.util.Set seenComponents) Returns a Map of Strings to List[String]s which is the descriptions of any components that appear in the environment.
protected java.util.Set<java.io.Serializable>	equivAccessPaths(AccessPathRoot p)
boolean	equivalentAccessPaths(AccessPath p, AccessPath q)
Label	findNonArgLabelUpperBound(Label L) Finds an upper bound that does not contain arg labels.
Label	findUpperBound(Label L) Finds a PairLabel upper bound.
protected Label	findUpperBound(Label L, java.util.Collection<java.io.Serializable> seen, boolean noArgLabels)
protected LabelEnv.SearchState	freshSearchState()
boolean	hasVariables() Do any of the assertions in this label environment contain variables?
boolean	isEmpty() Is this enviornment empty, or does is contain some constraints?
boolean	leq(ConfPolicy p1, ConfPolicy p2, LabelEnv.SearchState state)
boolean	leq(IntegPolicy p1, IntegPolicy p2, LabelEnv.SearchState state)
boolean	leq(Label L1, Label L2)
boolean	leq(Label L1, Label L2, LabelEnv.SearchState state) Recursive implementation of L1 <= L2.
boolean	leq(Policy p1, Policy p2)
boolean	leq(Policy p1, Policy p2, LabelEnv.SearchState state_)
PrincipalHierarchy	ph()
void	setSolver(Solver s) Set the solver used for this Label Environment.
java.lang.String	toString()
Label	triggerTransforms(Label label) Trigger the transformation of WritersToReaders labels.

Methods inherited from class java.lang.Object

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

Field Detail

ph

protected final PrincipalHierarchy ph

labelAssertions

protected final java.util.List<LabelLeAssertion_c> labelAssertions

displayLabelAssertions

protected final java.lang.StringBuffer displayLabelAssertions

ts

protected final JifTypeSystem ts

accessPathEquivReps

protected final java.util.Map<AccessPath,AccessPath> accessPathEquivReps

A map from AccessPath to representatives of the equivalent set of the AcessPath. No mapping if the element is its own representative.

parent

protected final LabelEnv_c parent

solver

protected Solver solver

hasVariables

protected boolean hasVariables

Do any of the assertions have variables in them?

topics

protected static java.util.Collection topics

Topics to report

useCache

protected final boolean useCache

Constructor Detail

LabelEnv_c

public LabelEnv_c(JifTypeSystem ts,
                  boolean useCache)

LabelEnv_c

protected LabelEnv_c(JifTypeSystem ts,
                     PrincipalHierarchy ph,
                     java.util.List<LabelLeAssertion_c> assertions,
                     java.lang.String displayLabelAssertions,
                     boolean hasVariables,
                     boolean useCache,
                     java.util.Map<AccessPath,AccessPath> accessPathEquivReps,
                     LabelEnv_c parent)

Method Detail

setSolver

public void setSolver(Solver s)

Description copied from interface: LabelEnv

Set the solver used for this Label Environment. When necessary, the label environment will use the variable bounds of label variables when determining if constraints are satisfied.

Specified by:

setSolver in interface LabelEnv

ph

public PrincipalHierarchy ph()

hasVariables

public boolean hasVariables()

Description copied from interface: LabelEnv

Do any of the assertions in this label environment contain variables?

Specified by:

hasVariables in interface LabelEnv

addActsFor

public void addActsFor(Principal p1,
                       Principal p2)

addEquiv

public void addEquiv(Principal p1,
                     Principal p2)

addAssertionLE

public void addAssertionLE(Label L1,
                           Label L2)

addEquiv

public void addEquiv(Label L1,
                     Label L2)

copy

public LabelEnv_c copy()

actsFor

public boolean actsFor(Principal p,
                       Principal q)

Specified by:

actsFor in interface LabelEnv

leq

public boolean leq(Label L1,
                   Label L2)

Specified by:

leq in interface LabelEnv

equivalentAccessPaths

public boolean equivalentAccessPaths(AccessPath p,
                                     AccessPath q)

Specified by:

equivalentAccessPaths in interface LabelEnv

addEquiv

public void addEquiv(AccessPath p,
                     AccessPath q)

equivAccessPaths

protected java.util.Set<java.io.Serializable> equivAccessPaths(AccessPathRoot p)

leq

public boolean leq(Label L1,
                   Label L2,
                   LabelEnv.SearchState state)

Recursive implementation of L1 <= L2.

Specified by:

leq in interface LabelEnv

checkCache

protected java.lang.Boolean checkCache(jif.types.hierarchy.LabelEnv_c.LeqGoal g)

cacheResult

protected void cacheResult(jif.types.hierarchy.LabelEnv_c.LeqGoal g,
                           LabelEnv.SearchState s,
                           boolean result)

leq

public boolean leq(Policy p1,
                   Policy p2)

Specified by:

leq in interface LabelEnv

leq

public boolean leq(Policy p1,
                   Policy p2,
                   LabelEnv.SearchState state_)

Specified by:

leq in interface LabelEnv

leq

public boolean leq(ConfPolicy p1,
                   ConfPolicy p2,
                   LabelEnv.SearchState state)

leq

public boolean leq(IntegPolicy p1,
                   IntegPolicy p2,
                   LabelEnv.SearchState state)

isEmpty

public boolean isEmpty()

Is this enviornment empty, or does is contain some constraints?

Specified by:

isEmpty in interface LabelEnv

findUpperBound

public Label findUpperBound(Label L)

Finds a PairLabel upper bound. It does not use leq

Specified by:

findUpperBound in interface LabelEnv

findNonArgLabelUpperBound

public Label findNonArgLabelUpperBound(Label L)

Finds an upper bound that does not contain arg labels. It does not use leq.

Specified by:

findNonArgLabelUpperBound in interface LabelEnv

findUpperBound

protected Label findUpperBound(Label L,
                               java.util.Collection<java.io.Serializable> seen,
                               boolean noArgLabels)

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

definitions

public java.util.Map<java.lang.String,java.util.List<java.lang.String>> definitions(VarMap bounds,
                                                                                    java.util.Set seenComponents)

Returns a Map of Strings to List[String]s which is the descriptions of any components that appear in the environment. This map is used for verbose output to the user, to help explain the meaning of constraints and labels. Seen components is a Set of Labels whose definitions will not be displayed.

Specified by:

definitions in interface LabelEnv

triggerTransforms

public Label triggerTransforms(Label label)

Trigger the transformation of WritersToReaders labels. Not guaranteed to remove all writersToReaders labels.

Specified by:

triggerTransforms in interface LabelEnv

freshSearchState

protected LabelEnv.SearchState freshSearchState()