jif.extension
Class JifCheckedEndorseStmtExt

java.lang.Object
  polyglot.ast.Ext_c
      jif.ast.Jif_c
          jif.extension.JifStmtExt_c
              jif.extension.JifDowngradeStmtExt
                  jif.extension.JifEndorseStmtExt
                      jif.extension.JifCheckedEndorseStmtExt

All Implemented Interfaces:

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

public class JifCheckedEndorseStmtExt
extends JifEndorseStmtExt

The Jif extension of the CheckedEndorseStmt node. A checked endorse is of the form: endorse (x, Lfrom to Lto) if (e) S else S' and is approximately equivalent to T x' = endorse(x, Lfrom to Lto); if (e[x'/x]) S[x'/x] else S' To actually implement this, however, we use a different context for label checking e and S, that gives the local variable x the label Lto.

See Also:

CheckedEndorseStmt

Field Summary

Fields inherited from class jif.extension.JifStmtExt_c

stmtDel

Fields inherited from class jif.ast.Jif_c

toJava, X

Fields inherited from class polyglot.ast.Ext_c

ext, node

Constructor Summary

JifCheckedEndorseStmtExt(ToJavaExt toJava)

Method Summary

protected JifContext	bodyContext(LabelChecker lc, JifContext A, Label downgradeFrom, Label downgradeTo)
protected void	checkAdditionalConstraints(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos) Check any additional constraints
protected void	checkAuthority(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos) Check the authority condition
protected polyglot.ast.Stmt	checkBody(LabelChecker lc, JifContext A, Label downgradeFrom, Label downgradeTo)
protected 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 void	checkPCconstraint(LabelChecker lc, JifContext A, Label pc, Label downgradeFrom, boolean boundSpecified)
protected void	checkRobustness(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos) Check the robustness condition

Methods inherited from class jif.extension.JifDowngradeStmtExt

declassifyConstraintContext, initPathMap, labelCheckStmt

Methods inherited from class jif.extension.JifStmtExt_c

copy, init, labelCheck, stmtDel, stmtDel

Methods inherited from class jif.ast.Jif_c

checkAndRemoveThrowType, checkThrowTypes, getPathMap, 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

JifCheckedEndorseStmtExt

public JifCheckedEndorseStmtExt(ToJavaExt toJava)

Method Detail

checkBody

protected polyglot.ast.Stmt checkBody(LabelChecker lc,
                                      JifContext A,
                                      Label downgradeFrom,
                                      Label downgradeTo)
                               throws polyglot.types.SemanticException

Overrides:

checkBody in class JifDowngradeStmtExt

Throws:

polyglot.types.SemanticException

bodyContext

protected JifContext bodyContext(LabelChecker lc,
                                 JifContext A,
                                 Label downgradeFrom,
                                 Label downgradeTo)

Overrides:

bodyContext in class JifDowngradeStmtExt

checkPCconstraint

protected void checkPCconstraint(LabelChecker lc,
                                 JifContext A,
                                 Label pc,
                                 Label downgradeFrom,
                                 boolean boundSpecified)
                          throws polyglot.types.SemanticException

Overrides:

checkPCconstraint in class JifDowngradeStmtExt

Throws:

polyglot.types.SemanticException

checkOneDimenOnly

protected void checkOneDimenOnly(LabelChecker lc,
                                 JifContext A,
                                 Label labelFrom,
                                 Label labelTo,
                                 polyglot.util.Position pos)
                          throws polyglot.types.SemanticException

Description copied from class: JifDowngradeStmtExt

Check that only the integrity/confidentiality is downgraded, and not the other dimension.

Overrides:

checkOneDimenOnly in class JifEndorseStmtExt

Throws:

polyglot.types.SemanticException

checkAuthority

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

Description copied from class: JifDowngradeStmtExt

Check the authority condition

Overrides:

checkAuthority in class JifEndorseStmtExt

Throws:

polyglot.types.SemanticException

checkRobustness

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

Description copied from class: JifDowngradeStmtExt

Check the robustness condition

Overrides:

checkRobustness in class JifEndorseStmtExt

Throws:

polyglot.types.SemanticException

checkAdditionalConstraints

protected void checkAdditionalConstraints(LabelChecker lc,
                                          JifContext A,
                                          Label labelFrom,
                                          Label labelTo,
                                          polyglot.util.Position pos)
                                   throws polyglot.types.SemanticException

Description copied from class: JifDowngradeStmtExt

Check any additional constraints

Overrides:

checkAdditionalConstraints in class JifDowngradeStmtExt

Throws:

polyglot.types.SemanticException