public class JifCheckedEndorseStmtExt extends JifEndorseStmtExt
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.CheckedEndorseStmt
,
Serialized FormstmtDel
Constructor and Description |
---|
JifCheckedEndorseStmtExt(ToJavaExt toJava) |
Modifier and Type | Method and Description |
---|---|
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
|
protected void |
updateContextForConsequent(LabelChecker lc,
JifContext A,
PathMap Xexpr)
Utility method for updating the context for the consequent.
|
declassifyConstraintContext, initPathMap, labelCheckStmt
copy, init, labelCheck, stmtDel, stmtDel
checkAndRemoveThrowType, checkThrowTypes, dump, getPathMap, integerBoundsCalculated, toJava, toJava, updatePathMap, X, X
addDecls, buildTypes, buildTypesEnter, checkConstants, childExpectedType, copy, copy, disambiguate, disambiguateEnter, disambiguateOverride, dump, dump, dump, dump, enterChildScope, enterScope, exceptionCheck, exceptionCheckEnter, ext, ext, extRewrite, extRewriteEnter, extRewriteOverride, initPred, lang, node, pred, prettyPrint, prettyPrint, prettyPrint, prettyPrint, prettyPrint, print, printBlock, printSubStmt, superLang, throwTypes, toString, translate, typeCheck, typeCheckEnter, typeCheckOverride, visitChild, visitChildren, visitList
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
addDecls, buildTypes, buildTypesEnter, checkConstants, childExpectedType, copy, copy, disambiguate, disambiguateEnter, disambiguateOverride, dump, dump, dump, dump, enterChildScope, enterScope, exceptionCheck, exceptionCheckEnter, extRewrite, extRewriteEnter, extRewriteOverride, lang, prettyPrint, prettyPrint, prettyPrint, prettyPrint, prettyPrint, throwTypes, translate, typeCheck, typeCheckEnter, typeCheckOverride, visitChild, visitChildren, visitList
public JifCheckedEndorseStmtExt(ToJavaExt toJava)
protected polyglot.ast.Stmt checkBody(LabelChecker lc, JifContext A, Label downgradeFrom, Label downgradeTo) throws polyglot.types.SemanticException
checkBody
in class JifDowngradeStmtExt
polyglot.types.SemanticException
protected void updateContextForConsequent(LabelChecker lc, JifContext A, PathMap Xexpr)
protected JifContext bodyContext(LabelChecker lc, JifContext A, Label downgradeFrom, Label downgradeTo)
bodyContext
in class JifDowngradeStmtExt
protected void checkPCconstraint(LabelChecker lc, JifContext A, Label pc, Label downgradeFrom, boolean boundSpecified) throws polyglot.types.SemanticException
checkPCconstraint
in class JifDowngradeStmtExt
polyglot.types.SemanticException
protected void checkOneDimenOnly(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos) throws polyglot.types.SemanticException
JifDowngradeStmtExt
checkOneDimenOnly
in class JifEndorseStmtExt
polyglot.types.SemanticException
protected void checkAuthority(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos) throws polyglot.types.SemanticException
JifDowngradeStmtExt
checkAuthority
in class JifEndorseStmtExt
polyglot.types.SemanticException
protected void checkRobustness(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos) throws polyglot.types.SemanticException
JifDowngradeStmtExt
checkRobustness
in class JifEndorseStmtExt
polyglot.types.SemanticException
protected void checkAdditionalConstraints(LabelChecker lc, JifContext A, Label labelFrom, Label labelTo, polyglot.util.Position pos) throws polyglot.types.SemanticException
JifDowngradeStmtExt
checkAdditionalConstraints
in class JifDowngradeStmtExt
polyglot.types.SemanticException