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

    Fields
    Modifier and Type | Field and Description
    --- | ---
    `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>` | `labelAssertions`
    `protected LabelEnv_c` | `parent`
    `protected PrincipalHierarchy` | `ph`
    `protected Solver` | `solver`
    `protected static java.util.Collection<java.lang.String>` | `topics` Topics to report
    `protected JifTypeSystem` | `ts`
    `protected boolean` | `useCache`

  - ### Constructor Summary

    Constructors
    Modifier | Constructor and Description
    --- | ---
    `` | `LabelEnv_c(JifTypeSystem ts, boolean useCache)`
    `protected` | `LabelEnv_c(JifTypeSystem ts, PrincipalHierarchy ph, java.util.List<LabelLeAssertion> assertions, java.lang.String displayLabelAssertions, boolean hasVariables, boolean useCache, java.util.Map<AccessPath,AccessPath> accessPathEquivReps, LabelEnv_c parent)`

  - ### Method Summary

    All Methods Instance Methods Concrete Methods
    Modifier and Type | Method and Description
    --- | ---
    `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<Label> 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` | `findLowerBound(Label L)` Finds a PairLabel lower bound.
    `protected Label` | `findLowerBound(Label L, java.util.Collection<java.io.Serializable> seen, boolean noArgLabels)`
    `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<Label> 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?
    `java.util.Collection<LabelLeAssertion>` | `labelAssertions()` The collection of label assertions
    `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()`
    `PrincipalHierarchy` | `principalHierarchy()` The static principal hierarchy
    `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> 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<java.lang.String> 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> 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`

    - #### principalHierarchy

          public PrincipalHierarchy principalHierarchy()

      Description copied from interface: `LabelEnv`
      The static principal hierarchy
      Specified by:
        `principalHierarchy` in interface `LabelEnv`

    - #### labelAssertions

          public java.util.Collection<LabelLeAssertion> labelAssertions()

      Description copied from interface: `LabelEnv`
      The collection of label assertions
      Specified by:
        `labelAssertions` 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`

    - #### findLowerBound

          public Label findLowerBound(Label L)

      Finds a PairLabel lower bound. It does not use leq
      Specified by:
        `findLowerBound` in interface `LabelEnv`

    - #### findLowerBound

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

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