jif.extension
Class JifDowngradeExprExt

java.lang.Object
  extended by polyglot.ast.Ext_c
      extended by jif.ast.Jif_c
          extended by jif.extension.JifExprExt
              extended by jif.extension.JifDowngradeExprExt
All Implemented Interfaces:
java.lang.Cloneable, Jif, polyglot.ast.Ext, polyglot.util.Copy
Direct Known Subclasses:
JifDeclassifyExprExt, JifEndorseExprExt

public abstract class JifDowngradeExprExt
extends JifExprExt

The Jif extension of the DowngradeExpr node.

See Also:
DowngradeExpr

Field Summary
 
Fields inherited from class jif.ast.Jif_c
toJava, X
 
Fields inherited from class polyglot.ast.Ext_c
ext, node
 
Constructor Summary
JifDowngradeExprExt(ToJavaExt toJava)
           
 
Method Summary
protected abstract  void checkAuthority(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos)
          Check the authority condition
protected  void checkDowngradeFromBound(LabelChecker lc, JifContext A, PathMap Xe, DowngradeExpr d, Label downgradeFrom, Label downgradeTo, boolean boundSpecified)
           
protected abstract  void checkOneDimenOnly(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos)
          Check that only the integrity/confidentiality is downgraded, and not the other dimension.
protected abstract  void checkRobustness(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos)
          Check the robustness condition
protected  JifContext declassifyConstraintContext(LabelChecker lc, JifContext A, Label downgradeFrom, Label downgradeTo)
           
protected  PathMap downgradeExprPathMap(LabelChecker lc, PathMap Xe)
           
 polyglot.ast.Node labelCheck(LabelChecker lc)
          Label check the node to which this extension is attached.
 
Methods inherited from class jif.extension.JifExprExt
getNumericBounds, setNumericBounds
 
Methods inherited from class jif.ast.Jif_c
checkAndRemoveThrowType, checkThrowTypes, copy, getPathMap, init, integerBoundsCalculated, 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 polyglot.ast.Ext
dump, ext, ext, node
 

Constructor Detail

JifDowngradeExprExt

public JifDowngradeExprExt(ToJavaExt toJava)
Method Detail

declassifyConstraintContext

protected JifContext declassifyConstraintContext(LabelChecker lc,
                                                 JifContext A,
                                                 Label downgradeFrom,
                                                 Label downgradeTo)
                                          throws polyglot.types.SemanticException
Throws:
polyglot.types.SemanticException

labelCheck

public polyglot.ast.Node labelCheck(LabelChecker lc)
                             throws polyglot.types.SemanticException
Description copied from interface: Jif
Label check the node to which this extension is attached.

Specified by:
labelCheck in interface Jif
Overrides:
labelCheck in class Jif_c
Throws:
polyglot.types.SemanticException

checkDowngradeFromBound

protected void checkDowngradeFromBound(LabelChecker lc,
                                       JifContext A,
                                       PathMap Xe,
                                       DowngradeExpr d,
                                       Label downgradeFrom,
                                       Label downgradeTo,
                                       boolean boundSpecified)
                                throws polyglot.types.SemanticException
Throws:
polyglot.types.SemanticException

downgradeExprPathMap

protected PathMap downgradeExprPathMap(LabelChecker lc,
                                       PathMap Xe)
                                throws polyglot.types.SemanticException
Throws:
polyglot.types.SemanticException

checkOneDimenOnly

protected abstract void checkOneDimenOnly(LabelChecker lc,
                                          JifContext A,
                                          Label labelFrom,
                                          Label labelTo,
                                          polyglot.util.Position pos)
                                   throws polyglot.types.SemanticException
Check that only the integrity/confidentiality is downgraded, and not the other dimension.

Parameters:
lc -
labelFrom -
labelTo -
Throws:
polyglot.types.SemanticException

checkAuthority

protected abstract void checkAuthority(LabelChecker lc,
                                       JifContext A,
                                       Label labelFrom,
                                       Label labelTo,
                                       polyglot.util.Position pos)
                                throws polyglot.types.SemanticException
Check the authority condition

Parameters:
lc -
labelFrom -
labelTo -
Throws:
polyglot.types.SemanticException

checkRobustness

protected abstract void checkRobustness(LabelChecker lc,
                                        JifContext A,
                                        Label labelFrom,
                                        Label labelTo,
                                        polyglot.util.Position pos)
                                 throws polyglot.types.SemanticException
Check the robustness condition

Parameters:
lc -
labelFrom -
labelTo -
Throws:
polyglot.types.SemanticException