Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## 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)` This method checks if two access paths are equivalent.
`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)

  Description copied from interface: `LabelEnv`
  This method checks if two access paths are equivalent. Called in two cases: a. To check if a dynamic principal acts for another b. While checking a label constraint involving a DynamicLabel

  Specified by:
    `equivalentAccessPaths` in interface `LabelEnv`
  Returns:
    true if the two access paths are equivalent

### 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()

Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD