jif.types

## Interface JifContext

- All Superinterfaces:
    java.lang.Cloneable, polyglot.types.Context, polyglot.util.Copy<polyglot.types.Context>, polyglot.types.Resolver
  All Known Implementing Classes:
    JifContext_c

      public interface JifContext
      extends polyglot.types.Context

  The context for Jif type checking. `JifContext` extends `Context` with contextual information needed for checking labels, and also with some utility methods to assist in the implementation of label checking. The `JifContext` object contains a `label environment`, which contains a `principal hierarchy`; most access to these objects should be through the `JifContext` object, for example, the methods `addActsFor`, `actsFor`, `addContraintLE`.

- - ### Nested Class Summary

    - ### Nested classes/interfaces inherited from interface polyglot.util.Copy

      `polyglot.util.Copy.Util`

  - ### Method Summary

    All Methods Instance Methods Abstract Methods
    Modifier and Type | Method and Description
    --- | ---
    `void` | `addActsFor(ActsForParam actor, Principal granter)`
    `void` | `addActsFor(Label L, Principal p)` Adds a label-actsfor-principal assumption to the label environment.
    `void` | `addActsFor(Principal p1, Principal p2)` Add an actsfor relation to the principal hierarchy.
    `void` | `addAssertionLE(Label L1, Label L2)` Add a less than or equal assertion to the label environment.
    `void` | `addCheckedEndorse(polyglot.types.LocalInstance li, Label downgradeTo)` Add a checked endorse for the local instance li.
    `void` | `addDefinitionalAssertionEquiv(AccessPath p, AccessPath q)` Adds the assertion that the access path p is equivalent to the access path q to this context, and all outer contexts up to the method/constructor/initializer level
    `void` | `addDefinitionalAssertionEquiv(Label L1, Label L2)` Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level
    `void` | `addDefinitionalAssertionEquiv(Label L1, Label L2, boolean addToClass)` Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level.
    `void` | `addDefinitionalEquiv(Principal p1, Principal p2)` Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level
    `void` | `addEquiv(AccessPath p, AccessPath q)` Adds the assertion that the access path p is equivalent to the access path q to this context
    `void` | `addEquiv(Label L1, Label L2)` Add an equivalence to the label environment.
    `void` | `addEquiv(Principal p1, Principal p2)` Add an actsfor relation both ways to the principal hierarchy.
    `Label` | `authLabel()` Get the authority of the current code, represented as a confidentiality label.
    `Label` | `authLabelInteg()` Get the authority of the current code, represented as an integrity label.
    `java.util.Set<Principal>` | `authority()` The authority of a class or a procedure is the set of principals who have authorized that code.
    `boolean` | `checkingInits()` Indicates if we are currently checking the initializers within a constructor.
    `void` | `clearPH()` Clears the principal hierarchy of all actsfor relations.
    `Label` | `constructorReturnLabel()` If the current code is a constructor, returns the return label of that constructor.
    `Label` | `currentCodePCBound()` The currentCodePCBound is an upper bound on the PC of the caller of the current code, and a lower bound on the observable effects of the current code.
    `Label` | `gotoLabel(polyglot.ast.Branch.Kind kind, java.lang.String label)` Retrieve the `Label` associated with branching to the location `label`, with the branch kind `kind`.
    `void` | `gotoLabel(polyglot.ast.Branch.Kind kind, java.lang.String label, Label L)` Record the `Label` associated with branching to the location `label`, with the branch kind `kind`.
    `boolean` | `inConstructorCall()` Is the Context in a constructor call, e.g.
    `LabelEnv` | `labelEnv()`
    `PathMap` | `pathMapForLocal(polyglot.types.LocalInstance li, LabelChecker lc)` Return the path map for evaluating a local variable
    `Label` | `pc()`
    `PrincipalHierarchy` | `ph()`
    `ProviderLabel` | `provider()`
    `polyglot.types.Context` | `pushConstructorCall()` Push a Context onto the stack for a constructor call, e.g.
    `polyglot.types.Context` | `pushPrologue()`
    `void` | `setAuthority(java.util.Set<Principal> authority)`
    `void` | `setCheckingInits(boolean checkingInits)` Set whether we are currently checking the initializers within a constructor.
    `void` | `setConstructorReturnLabel(Label Lr)`
    `void` | `setCurrentCodePCBound(Label label)`
    `void` | `setPc(Label label, LabelChecker lc)`
    `void` | `setProvider(ProviderLabel provider)`
    `boolean` | `updateAllowed(polyglot.ast.Expr e)` Can this expression be updated, e.g.

    - ### Methods inherited from interface polyglot.types.Context

      `addMethod, addNamed, addVariable, currentClass, currentClassScope, currentCode, definingCodeDef, findField, findFieldScope, findLabelSilent, findLocal, findLocalSilent, findMethod, findMethodScope, findVariable, findVariableSilent, importTable, inCode, inStaticContext, isLocal, lang, outerResolver, package_, pop, pushBlock, pushClass, pushCode, pushLabel, pushSource, pushStatic, typeSystem`

    - ### Methods inherited from interface polyglot.types.Resolver

      `find`

    - ### Methods inherited from interface polyglot.util.Copy

      `copy`

- - ### Method Detail

    - #### labelEnv

          LabelEnv labelEnv()

    - #### addAssertionLE

          void addAssertionLE(Label L1,
                              Label L2)

      Add a less than or equal assertion to the label environment.

    - #### addActsFor

          void addActsFor(Label L,
                          Principal p)

      Adds a label-actsfor-principal assumption to the label environment.

    - #### addEquiv

          void addEquiv(Label L1,
                        Label L2)

      Add an equivalence to the label environment.

    - #### addDefinitionalAssertionEquiv

          void addDefinitionalAssertionEquiv(Label L1,
                                             Label L2)

      Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level
      Parameters:
        `L1` -
        `L2` -

    - #### addDefinitionalAssertionEquiv

          void addDefinitionalAssertionEquiv(Label L1,
                                             Label L2,
                                             boolean addToClass)

      Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level. If addToClass is true, then the definition will also be added to the class. This should only be used for assignments to final fields.
      Parameters:
        `L1` -
        `L2` -

    - #### addEquiv

          void addEquiv(AccessPath p,
                        AccessPath q)

      Adds the assertion that the access path p is equivalent to the access path q to this context

    - #### addDefinitionalAssertionEquiv

          void addDefinitionalAssertionEquiv(AccessPath p,
                                             AccessPath q)

      Adds the assertion that the access path p is equivalent to the access path q to this context, and all outer contexts up to the method/constructor/initializer level

    - #### ph

          PrincipalHierarchy ph()

    - #### addActsFor

          void addActsFor(Principal p1,
                          Principal p2)

      Add an actsfor relation to the principal hierarchy.

    - #### addEquiv

          void addEquiv(Principal p1,
                        Principal p2)

      Add an actsfor relation both ways to the principal hierarchy.

    - #### addDefinitionalEquiv

          void addDefinitionalEquiv(Principal p1,
                                    Principal p2)

      Adds the assertion to this context, and all outer contexts up to the method/constructor/initializer level

    - #### clearPH

          void clearPH()

      Clears the principal hierarchy of all actsfor relations.

    - #### pc

          Label pc()

    - #### setPc

          void setPc(Label label,
                     LabelChecker lc)

    - #### currentCodePCBound

          Label currentCodePCBound()

      The currentCodePCBound is an upper bound on the PC of the caller of the current code, and a lower bound on the observable effects of the current code.

    - #### setCurrentCodePCBound

          void setCurrentCodePCBound(Label label)

    - #### gotoLabel

          Label gotoLabel(polyglot.ast.Branch.Kind kind,
                          java.lang.String label)
                   throws polyglot.types.SemanticException

      Retrieve the `Label` associated with branching to the location `label`, with the branch kind `kind`.
      Throws:
        `polyglot.types.SemanticException`

    - #### gotoLabel

          void gotoLabel(polyglot.ast.Branch.Kind kind,
                         java.lang.String label,
                         Label L)

      Record the `Label` associated with branching to the location `label`, with the branch kind `kind`.

    - #### authority

          java.util.Set<Principal> authority()

      The authority of a class or a procedure is the set of principals who have authorized that code.

    - #### setAuthority

          void setAuthority(java.util.Set<Principal> authority)

    - #### authLabel

          Label authLabel()

      Get the authority of the current code, represented as a confidentiality label.

    - #### authLabelInteg

          Label authLabelInteg()

      Get the authority of the current code, represented as an integrity label.

    - #### checkingInits

          boolean checkingInits()

      Indicates if we are currently checking the initializers within a constructor. If we are, then more permissive label checking can be used for field assignments.

    - #### setCheckingInits

          void setCheckingInits(boolean checkingInits)

      Set whether we are currently checking the initializers within a constructor.

    - #### constructorReturnLabel

          Label constructorReturnLabel()

      If the current code is a constructor, returns the return label of that constructor. The value returned is only valid if `checkingInits` is true, and is used for more permissive label checking for field assignments.

    - #### setConstructorReturnLabel

          void setConstructorReturnLabel(Label Lr)

    - #### pushConstructorCall

          polyglot.types.Context pushConstructorCall()

      Push a Context onto the stack for a constructor call, e.g. "super(...)" or "this(...)". Jif needs to distinguish constructor call contexts from other static contexts because the this label may appear in constructor call contexts, but not other static contexts.

    - #### inConstructorCall

          boolean inConstructorCall()

      Is the Context in a constructor call, e.g. "super(...)" or "this(...)"?

    - #### pathMapForLocal

          PathMap pathMapForLocal(polyglot.types.LocalInstance li,
                                  LabelChecker lc)

      Return the path map for evaluating a local variable

    - #### updateAllowed

          boolean updateAllowed(polyglot.ast.Expr e)

      Can this expression be updated, e.g. is "e++" or "e = e'" allowed?

    - #### addCheckedEndorse

          void addCheckedEndorse(polyglot.types.LocalInstance li,
                                 Label downgradeTo)

      Add a checked endorse for the local instance li.

    - #### provider

          ProviderLabel provider()

    - #### setProvider

          void setProvider(ProviderLabel provider)

    - #### addActsFor

          void addActsFor(ActsForParam actor,
                          Principal granter)

    - #### pushPrologue

          polyglot.types.Context pushPrologue()