Java/C++/C#: Sync dataflow.

This commit is contained in:
Anders Schack-Mulligen
2019-08-05 12:07:32 +02:00
parent f8804943ee
commit 2dc83c539c
13 changed files with 195 additions and 65 deletions

View File

@@ -57,9 +57,15 @@ abstract class Configuration extends string {
/** Holds if data flow through `node` is prohibited. */
predicate isBarrier(Node node) { none() }
/** DEPRECATED: override `isBarrier` instead. */
/** DEPRECATED: override `isBarrierIn` and `isBarrierOut` instead. */
deprecated predicate isBarrierEdge(Node node1, Node node2) { none() }
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis.
@@ -104,18 +110,22 @@ abstract class Configuration extends string {
}
private predicate inBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierIn(node) and
config.isSource(node)
}
private predicate outBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierOut(node) and
config.isSink(node)
}
private predicate fullBarrier(Node node, Configuration config) {
config.isBarrier(node) and
not config.isSource(node) and
config.isBarrier(node)
or
config.isBarrierIn(node) and
not config.isSource(node)
or
config.isBarrierOut(node) and
not config.isSink(node)
}

View File

@@ -57,9 +57,15 @@ abstract class Configuration extends string {
/** Holds if data flow through `node` is prohibited. */
predicate isBarrier(Node node) { none() }
/** DEPRECATED: override `isBarrier` instead. */
/** DEPRECATED: override `isBarrierIn` and `isBarrierOut` instead. */
deprecated predicate isBarrierEdge(Node node1, Node node2) { none() }
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis.
@@ -104,18 +110,22 @@ abstract class Configuration extends string {
}
private predicate inBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierIn(node) and
config.isSource(node)
}
private predicate outBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierOut(node) and
config.isSink(node)
}
private predicate fullBarrier(Node node, Configuration config) {
config.isBarrier(node) and
not config.isSource(node) and
config.isBarrier(node)
or
config.isBarrierIn(node) and
not config.isSource(node)
or
config.isBarrierOut(node) and
not config.isSink(node)
}

View File

@@ -57,9 +57,15 @@ abstract class Configuration extends string {
/** Holds if data flow through `node` is prohibited. */
predicate isBarrier(Node node) { none() }
/** DEPRECATED: override `isBarrier` instead. */
/** DEPRECATED: override `isBarrierIn` and `isBarrierOut` instead. */
deprecated predicate isBarrierEdge(Node node1, Node node2) { none() }
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis.
@@ -104,18 +110,22 @@ abstract class Configuration extends string {
}
private predicate inBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierIn(node) and
config.isSource(node)
}
private predicate outBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierOut(node) and
config.isSink(node)
}
private predicate fullBarrier(Node node, Configuration config) {
config.isBarrier(node) and
not config.isSource(node) and
config.isBarrier(node)
or
config.isBarrierIn(node) and
not config.isSource(node)
or
config.isBarrierOut(node) and
not config.isSink(node)
}

View File

@@ -57,9 +57,15 @@ abstract class Configuration extends string {
/** Holds if data flow through `node` is prohibited. */
predicate isBarrier(Node node) { none() }
/** DEPRECATED: override `isBarrier` instead. */
/** DEPRECATED: override `isBarrierIn` and `isBarrierOut` instead. */
deprecated predicate isBarrierEdge(Node node1, Node node2) { none() }
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if the additional flow step from `node1` to `node2` must be taken
* into account in the analysis.
@@ -104,18 +110,22 @@ abstract class Configuration extends string {
}
private predicate inBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierIn(node) and
config.isSource(node)
}
private predicate outBarrier(Node node, Configuration config) {
config.isBarrier(node) and
config.isBarrierOut(node) and
config.isSink(node)
}
private predicate fullBarrier(Node node, Configuration config) {
config.isBarrier(node) and
not config.isSource(node) and
config.isBarrier(node)
or
config.isBarrierIn(node) and
not config.isSource(node)
or
config.isBarrierOut(node) and
not config.isSink(node)
}