jif.types.hierarchy

## Interface LabelEnv

- All Known Implementing Classes:
    LabelEnv_c

      public interface LabelEnv

  An environment of assertions about label relationships. The relationships between different labels can be queried in this environment using `leq`".

- - ### Nested Class Summary

    Nested Classes
    Modifier and Type | Interface and Description
    --- | ---
    `static interface` | `LabelEnv.SearchState` Encapsulates the solvers search state.

  - ### Method Summary

    All Methods Instance Methods Abstract Methods
    Modifier and Type | Method and Description
    --- | ---
    `boolean` | `actsFor(Principal p, Principal q)`
    `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.
    `boolean` | `equivalentAccessPaths(AccessPath p, AccessPath q)` This method checks if two access paths are equivalent.
    `Label` | `findLowerBound(Label L)` Finds an lower bound for L using the assertions in this environment.
    `Label` | `findNonArgLabelUpperBound(Label L)` Finds an upper bound for L that does not have any arg labels in it.
    `Label` | `findUpperBound(Label L)` Finds an upper bound for L using the assertions in this environment.
    `boolean` | `hasVariables()` Do any of the assertions in this label environment contain variables?
    `boolean` | `isEmpty()` Is this environment empty, or does is contain some constraints?
    `java.util.Collection<LabelLeAssertion>` | `labelAssertions()` The collection of label assertions
    `boolean` | `leq(Label L1, Label L2)`
    `boolean` | `leq(Label L1, Label L2, LabelEnv.SearchState state)`
    `boolean` | `leq(Policy p1, Policy p2)`
    `boolean` | `leq(Policy p1, Policy p2, LabelEnv.SearchState state)`
    `PrincipalHierarchy` | `principalHierarchy()` The static principal hierarchy
    `void` | `setSolver(Solver solver)` Set the solver used for this Label Environment.
    `Label` | `triggerTransforms(Label label)` Trigger any writersToReaders transforms in label, and return the result.

- - ### Method Detail

    - #### leq

          boolean leq(Label L1,
                      Label L2)

    - #### leq

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

    - #### leq

          boolean leq(Policy p1,
                      Policy p2)

    - #### leq

          boolean leq(Policy p1,
                      Policy p2,
                      LabelEnv.SearchState state)

    - #### actsFor

          boolean actsFor(Principal p,
                          Principal q)

    - #### findUpperBound

          Label findUpperBound(Label L)

      Finds an upper bound for L using the assertions in this environment. May return the top label if there is insufficient information to determine a more precise bound.

    - #### findLowerBound

          Label findLowerBound(Label L)

      Finds an lower bound for L using the assertions in this environment. May return the bottom label if there is insufficient information to determine a more precise bound.

    - #### findNonArgLabelUpperBound

          Label findNonArgLabelUpperBound(Label L)

      Finds an upper bound for L that does not have any arg labels in it. May return the top label if there is insufficient information to determine a more precise bound.

    - #### definitions

          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.

    - #### labelAssertions

          java.util.Collection<LabelLeAssertion> labelAssertions()

      The collection of label assertions

    - #### principalHierarchy

          PrincipalHierarchy principalHierarchy()

      The static principal hierarchy

    - #### triggerTransforms

          Label triggerTransforms(Label label)

      Trigger any writersToReaders transforms in label, and return the result.

    - #### isEmpty

          boolean isEmpty()

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

    - #### hasVariables

          boolean hasVariables()

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

    - #### setSolver

          void setSolver(Solver solver)

      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.

    - #### equivalentAccessPaths

          boolean equivalentAccessPaths(AccessPath p,
                                        AccessPath q)

      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
      Parameters:
        `p` -
        `q` -
      Returns:
        true if the two access paths are equivalent