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
Fields inherited from class polyglot.ast.Ext_c |
ext, node |
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 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 |
JifCheckedEndorseStmtExt
public JifCheckedEndorseStmtExt(ToJavaExt toJava)
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