jif.extension
Class JifProcedureDeclExt_c

java.lang.Object
  polyglot.ast.Ext_c
      jif.ast.Jif_c
          jif.extension.JifProcedureDeclExt_c

All Implemented Interfaces:

java.lang.Cloneable, Jif, JifProcedureDeclExt, polyglot.ast.Ext, polyglot.util.Copy

Direct Known Subclasses:

JifConstructorDeclExt, JifMethodDeclExt

public class JifProcedureDeclExt_c
extends Jif_c
implements JifProcedureDeclExt

The Jif extension of the ProcedureDecl node.

See Also:

ProcedureDecl, JifProcedureInstance

Nested Class Summary

protected static class

JifProcedureDeclExt_c.ConstraintVarianceLabelChecker Checker to ensure that labels do not use covariant labels in the wrong places

Field Summary

Fields inherited from class jif.ast.Jif_c

toJava, X

Fields inherited from class polyglot.ast.Ext_c

ext, node

Constructor Summary

JifProcedureDeclExt_c(ToJavaExt toJava)

Method Summary

protected static void	addCallers(JifProcedureInstance mi, JifContext A, java.util.Set 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	checkFormals(java.util.List formals, JifProcedureInstance ci, LabelChecker lc) Label check the formals.
protected java.util.Set	constrainAuth(JifProcedureInstance mi, JifContext A) This method corresponds to the constraint-authority predicate in the thesis (Figure 4.39).
protected 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.Jif_c

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

Methods inherited from class polyglot.ast.Ext_c

dump, ext, ext, node, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface jif.ast.Jif

integerBoundsCalculated, labelCheck, toJava, toJava, X, X

Methods inherited from interface polyglot.ast.Ext

dump, ext, ext, init, node

Methods inherited from interface polyglot.util.Copy

copy

Constructor Detail

JifProcedureDeclExt_c

public JifProcedureDeclExt_c(ToJavaExt toJava)

Method Detail

checkFormals

protected java.util.List checkFormals(java.util.List 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

checkAutoEndorseConstrainPC

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

Throws:

polyglot.types.SemanticException

constrainAuth

protected java.util.Set 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,
                                 JifContext A,
                                 java.util.Set 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

protected 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