JS: Embed check for in/out barriers in edge barrier check

This commit is contained in:
Asger F 2023-07-11 11:03:39 +02:00
Родитель 4964d811a5
Коммит d53beb3784
1 изменённых файлов: 32 добавлений и 2 удалений

Просмотреть файл

@ -514,7 +514,7 @@ private BasicBlock getADominatedBasicBlock(BarrierGuardNode guard, ConditionGuar
*
* Only holds for barriers that should apply to all flow labels.
*/
private predicate isBarrierEdge(Configuration cfg, DataFlow::Node pred, DataFlow::Node succ) {
private predicate isBarrierEdgeRaw(Configuration cfg, DataFlow::Node pred, DataFlow::Node succ) {
cfg.isBarrierEdge(pred, succ)
or
exists(DataFlow::BarrierGuardNode guard |
@ -523,11 +523,26 @@ private predicate isBarrierEdge(Configuration cfg, DataFlow::Node pred, DataFlow
)
}
/**
* Holds if there is a barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
* or one implied by a barrier guard, or by an out/in barrier for `pred` or `succ`, respectively.
*
* Only holds for barriers that should apply to all flow labels.
*/
pragma[inline]
private predicate isBarrierEdge(Configuration cfg, DataFlow::Node pred, DataFlow::Node succ) {
isBarrierEdgeRaw(cfg, pred, succ)
or
cfg.isBarrierOut(pred)
or
cfg.isBarrierIn(succ)
}
/**
* Holds if there is a labeled barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
* or one implied by a barrier guard.
*/
private predicate isLabeledBarrierEdge(
private predicate isLabeledBarrierEdgeRaw(
Configuration cfg, DataFlow::Node pred, DataFlow::Node succ, DataFlow::FlowLabel label
) {
cfg.isBarrierEdge(pred, succ, label)
@ -538,6 +553,21 @@ private predicate isLabeledBarrierEdge(
)
}
/**
* Holds if there is a labeled barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
* or one implied by a barrier guard, or by an out/in barrier for `pred` or `succ`, respectively.
*/
pragma[inline]
private predicate isLabeledBarrierEdge(
Configuration cfg, DataFlow::Node pred, DataFlow::Node succ, DataFlow::FlowLabel label
) {
isLabeledBarrierEdgeRaw(cfg, pred, succ, label)
or
cfg.isBarrierOut(pred, label)
or
cfg.isBarrierIn(succ, label)
}
/**
* A guard node that only blocks specific labels.
*/