Java: Basic support for pass-through barrier models.

This commit is contained in:
Anders Schack-Mulligen
2025-12-08 14:53:09 +01:00
parent e13bb0f866
commit d24b0ff596
5 changed files with 104 additions and 6 deletions

View File

@@ -2052,6 +2052,14 @@ module Make<
Element n, string input, string kind, Provenance provenance, string model
);
/**
* Holds if an external barrier specification exists for `n` with output specification
* `output` and kind `kind`.
*/
predicate barrierElement(
Element n, string output, string kind, Provenance provenance, string model
);
class SourceOrSinkElement extends Element;
/** An entity used to interpret a source/sink specification. */
@@ -2105,7 +2113,8 @@ module Make<
private predicate sourceSinkSpec(string spec) {
sourceElement(_, spec, _, _, _) or
sinkElement(_, spec, _, _, _)
sinkElement(_, spec, _, _, _) or
barrierElement(_, spec, _, _, _)
}
private module AccessPath = AccessPathSyntax::AccessPath<sourceSinkSpec/1>;
@@ -2160,11 +2169,22 @@ module Make<
)
}
private predicate barrierElementRef(
InterpretNode ref, SourceSinkAccessPath output, string kind, string model
) {
exists(SourceOrSinkElement e |
barrierElement(e, output, kind, _, model) and
if outputNeedsReferenceExt(output.getToken(0))
then e = ref.getCallTarget()
else e = ref.asElement()
)
}
/** Holds if the first `n` tokens of `output` resolve to the given interpretation. */
private predicate interpretOutput(
SourceSinkAccessPath output, int n, InterpretNode ref, InterpretNode node
) {
sourceElementRef(ref, output, _, _) and
(sourceElementRef(ref, output, _, _) or barrierElementRef(ref, output, _, _)) and
n = 0 and
(
if output = ""
@@ -2280,6 +2300,17 @@ module Make<
)
}
/**
* Holds if `node` is specified as a barrier with the given kind in a MaD flow
* model.
*/
predicate isBarrierNode(InterpretNode node, string kind, string model) {
exists(InterpretNode ref, SourceSinkAccessPath output |
barrierElementRef(ref, output, kind, model) and
interpretOutput(output, output.getNumToken(), ref, node)
)
}
final private class SourceOrSinkElementFinal = SourceOrSinkElement;
signature predicate sourceOrSinkElementSig(

View File

@@ -173,7 +173,7 @@ module KindValidation<KindValidationConfigSig Config> {
or
exists(string kind, string msg | Config::sinkKind(kind) |
not kind instanceof ValidSinkKind and
msg = "Invalid kind \"" + kind + "\" in sink model." and
msg = "Invalid kind \"" + kind + "\" in sink or barrier model." and
// The part of this message that refers to outdated sink kinds can be deleted after June 1st, 2024.
if kind instanceof OutdatedSinkKind
then result = msg + " " + kind.(OutdatedSinkKind).outdatedMessage()