jif.extension

## Class JifProcedureDeclExt_c

- java.lang.Object
- - polyglot.ast.Ext_c
  - - jif.ast.JifExt_c
    - - jif.extension.JifProcedureDeclExt_c

- All Implemented Interfaces:
    java.io.Serializable, java.lang.Cloneable, JifExt, JifProcedureDeclExt, polyglot.ast.Ext, polyglot.ast.NodeOps, polyglot.util.Copy<polyglot.ast.Ext>
  Direct Known Subclasses:
    JifConstructorDeclExt, JifMethodDeclExt

      public class JifProcedureDeclExt_c
      extends JifExt_c
      implements JifProcedureDeclExt

  The Jif extension of the `ProcedureDecl` node.
  See Also:
    `ProcedureDecl`, `JifProcedureInstance`, Serialized Form

- - ### Nested Class Summary

    Nested Classes
    Modifier and Type | Class and Description
    --- | ---
    `protected static class` | `JifProcedureDeclExt_c.ConstraintVarianceLabelChecker` Checker to ensure that labels do not use covariant labels in the wrong places

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

      `polyglot.util.Copy.Util`

  - ### Field Summary

    Fields
    Modifier and Type | Field and Description
    --- | ---
    `protected static java.lang.String` | `jif_verbose`

    - ### Fields inherited from class jif.ast.JifExt_c

      `toJava, X`

    - ### Fields inherited from class polyglot.ast.Ext_c

      `ext, node, pred`

  - ### Constructor Summary

    Constructors
    Constructor and Description
    `JifProcedureDeclExt_c(ToJavaExt toJava)`

  - ### Method Summary

    All Methods Static Methods Instance Methods Concrete Methods
    Modifier and Type | Method and Description
    --- | ---
    `protected static void` | `addCallers(JifProcedureInstance mi, java.util.Set<Principal> auth)` Adds the caller's authorities into `auth`
    `protected void` | `addReturnConstraints(Label Li, PathMap X, JifProcedureInstance mi, LabelChecker lc, polyglot.types.Type returnType)` This method corresponds to most of the check-body predicate in the thesis (Figure 4.40).
    `protected void` | `checkActsForAuthority(Principal p, JifContext A, LabelChecker lc)` Check that there is a p' in the old "auth" set such that p' actsFor p.
    `protected Label` | `checkAutoEndorseConstrainPC(JifProcedureInstance mi, LabelChecker lc)`
    `protected void` | `checkConstraintVariance(JifProcedureInstance mi, LabelChecker lc)` Check that covariant labels do not appear in contravariant positions
    `protected Label` | `checkEnforceSignature(JifProcedureInstance mi, LabelChecker lc)` This methods corresponds to the check-arguments predicate in the thesis (Figure 4.37).
    `protected java.util.List<polyglot.ast.Formal>` | `checkFormals(java.util.List<polyglot.ast.Formal> formals, JifProcedureInstance ci, LabelChecker lc)` Label check the formals.
    `protected void` | `checkProviderAuthority(JifProcedureInstance mi, LabelChecker lc)`
    `protected java.util.Set<Principal>` | `constrainAuth(JifProcedureInstance mi, JifContext A)` This method corresponds to the constraint-authority predicate in the thesis (Figure 4.39).
    `static void` | `constrainLabelEnv(JifProcedureInstance mi, JifContext A, CallHelper ch)` This method corresponds to the constraint-ph predicate in the thesis (Figure 4.39).

    - ### Methods inherited from class jif.ast.JifExt_c

      `checkAndRemoveThrowType, checkThrowTypes, copy, dump, getPathMap, init, integerBoundsCalculated, labelCheck, toJava, toJava, updatePathMap, X, X`

    - ### Methods inherited from class polyglot.ast.Ext_c

      `addDecls, buildTypes, buildTypesEnter, checkConstants, childExpectedType, copy, copy, disambiguate, disambiguateEnter, disambiguateOverride, dump, dump, dump, dump, enterChildScope, enterScope, exceptionCheck, exceptionCheckEnter, ext, ext, extRewrite, extRewriteEnter, extRewriteOverride, initPred, lang, node, pred, prettyPrint, prettyPrint, prettyPrint, prettyPrint, prettyPrint, print, printBlock, printSubStmt, superLang, throwTypes, toString, translate, typeCheck, typeCheckEnter, typeCheckOverride, visitChild, visitChildren, visitList`

    - ### Methods inherited from class java.lang.Object

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

    - ### Methods inherited from interface jif.ast.JifExt

      `integerBoundsCalculated, labelCheck, toJava, toJava, X, X`

    - ### Methods inherited from interface polyglot.ast.Ext

      `dump, ext, ext, init, initPred, node, pred`

    - ### Methods inherited from interface polyglot.ast.NodeOps

      `addDecls, buildTypes, buildTypesEnter, checkConstants, childExpectedType, copy, copy, disambiguate, disambiguateEnter, disambiguateOverride, dump, dump, dump, dump, enterChildScope, enterScope, exceptionCheck, exceptionCheckEnter, extRewrite, extRewriteEnter, extRewriteOverride, lang, prettyPrint, prettyPrint, prettyPrint, prettyPrint, prettyPrint, throwTypes, translate, typeCheck, typeCheckEnter, typeCheckOverride, visitChild, visitChildren, visitList`

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

      `copy`

- - ### Field Detail

    - #### jif_verbose

          protected static java.lang.String jif_verbose

  - ### Constructor Detail

    - #### JifProcedureDeclExt_c

          public JifProcedureDeclExt_c(ToJavaExt toJava)

  - ### Method Detail

    - #### checkFormals

          protected java.util.List<polyglot.ast.Formal> checkFormals(java.util.List<polyglot.ast.Formal> formals,
                                                                     JifProcedureInstance ci,
                                                                     LabelChecker lc)
                                                              throws polyglot.types.SemanticException

      Label check the formals.
      Throws:
        `polyglot.types.SemanticException`

    - #### checkEnforceSignature

          protected Label checkEnforceSignature(JifProcedureInstance mi,
                                                LabelChecker lc)
                                         throws polyglot.types.SemanticException

      This methods corresponds to the check-arguments predicate in the thesis (Figure 4.37). It returns the start label of the method. It mutates the local context (to the A'' in the rule).
      Throws:
        `polyglot.types.SemanticException`

    - #### checkProviderAuthority

          protected void checkProviderAuthority(JifProcedureInstance mi,
                                                LabelChecker lc)
                                         throws polyglot.types.SemanticException

      Throws:
        `polyglot.types.SemanticException`

    - #### checkAutoEndorseConstrainPC

          protected Label checkAutoEndorseConstrainPC(JifProcedureInstance mi,
                                                      LabelChecker lc)
                                               throws polyglot.types.SemanticException

      Throws:
        `polyglot.types.SemanticException`

    - #### constrainAuth

          protected java.util.Set<Principal> constrainAuth(JifProcedureInstance mi,
                                                           JifContext A)

      This method corresponds to the constraint-authority predicate in the thesis (Figure 4.39). It returns the set of principals for which the method can act.

    - #### addCallers

          protected static void addCallers(JifProcedureInstance mi,
                                           java.util.Set<Principal> auth)

      Adds the caller's authorities into `auth`

    - #### checkActsForAuthority

          protected void checkActsForAuthority(Principal p,
                                               JifContext A,
                                               LabelChecker lc)
                                        throws polyglot.types.SemanticException

      Check that there is a p' in the old "auth" set such that p' actsFor p.
      Throws:
        `polyglot.types.SemanticException`

    - #### constrainLabelEnv

          public static void constrainLabelEnv(JifProcedureInstance mi,
                                               JifContext A,
                                               CallHelper ch)
                                        throws polyglot.types.SemanticException

      This method corresponds to the constraint-ph predicate in the thesis (Figure 4.39). It returns the principal hierarchy used to check the body of the method.
      Throws:
        `polyglot.types.SemanticException`

    - #### addReturnConstraints

          protected void addReturnConstraints(Label Li,
                                              PathMap X,
                                              JifProcedureInstance mi,
                                              LabelChecker lc,
                                              polyglot.types.Type returnType)
                                       throws polyglot.types.SemanticException

      This method corresponds to most of the check-body predicate in the thesis (Figure 4.40). It assumes the body has already been checked and that the path map X is the join of the body's path map and the initial path map of the method. It adds the constraints that associate return termination and return value labels in the path map X with the declared return label and associates the exception labels in the path map X with the declared labels in the methods "throws" clause.
      Throws:
        `polyglot.types.SemanticException`

    - #### checkConstraintVariance

          protected void checkConstraintVariance(JifProcedureInstance mi,
                                                 LabelChecker lc)
                                          throws polyglot.types.SemanticException

      Check that covariant labels do not appear in contravariant positions
      Parameters:
        `mi` -
        `lc` -
      Throws:
        `polyglot.types.SemanticException`