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
Fields inherited from class polyglot.ast.Ext_c |
ext, node |
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)
Check that there is a p' in the old "auth" set such that p' actsFor p. |
protected Label |
checkAutoEndorseConstrainPC(JifProcedureInstance mi,
LabelChecker lc)
|
protected Label |
checkEnforceSignature(JifProcedureInstance mi,
LabelChecker lc)
This methods corresponds to the check-arguments predicate in the
thesis (Figure 4.37). |
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, del, del, init, labelCheck, toJava, toJava, X, X, 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 polyglot.ast.Ext |
dump, ext, ext, init, node |
Methods inherited from interface polyglot.util.Copy |
copy |
JifProcedureDeclExt_c
public JifProcedureDeclExt_c(ToJavaExt toJava)
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)
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