mirror of
https://github.com/github/codeql.git
synced 2026-04-15 03:54:02 +02:00
Merge pull request #21584 from owen-mc/shared/update-mad-comments
Shared: update code comments explaining models-as-data format to include barriers and barrier guards
This commit is contained in:
@@ -6,11 +6,15 @@
|
||||
*
|
||||
* The extensible relations have the following columns:
|
||||
* - Sources:
|
||||
* `namespace; type; subtypes; name; signature; ext; output; kind`
|
||||
* `namespace; type; subtypes; name; signature; ext; output; kind; provenance`
|
||||
* - Sinks:
|
||||
* `namespace; type; subtypes; name; signature; ext; input; kind`
|
||||
* `namespace; type; subtypes; name; signature; ext; input; kind; provenance`
|
||||
* - Summaries:
|
||||
* `namespace; type; subtypes; name; signature; ext; input; output; kind`
|
||||
* `namespace; type; subtypes; name; signature; ext; input; output; kind; provenance`
|
||||
* - Barriers:
|
||||
* `namespace; type; subtypes; name; signature; ext; output; kind; provenance`
|
||||
* - BarrierGuards:
|
||||
* `namespace; type; subtypes; name; signature; ext; input; acceptingValue; kind; provenance`
|
||||
*
|
||||
* The interpretation of a row is similar to API-graphs with a left-to-right
|
||||
* reading.
|
||||
@@ -87,11 +91,23 @@
|
||||
* value, and
|
||||
* - flow from the _second_ indirection of the 0th argument to the first
|
||||
* indirection of the return value, etc.
|
||||
* 8. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* 8. The `acceptingValue` column of barrier guard models specifies the condition
|
||||
* under which the guard blocks flow. It can be one of "true" or "false". In
|
||||
* the future "no-exception", "not-zero", "null", "not-null" may be supported.
|
||||
* 9. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* which classes the interpreted elements should be added. For example, for
|
||||
* sources "remote" indicates a default remote flow source, and for summaries
|
||||
* "taint" indicates a default additional taint step and "value" indicates a
|
||||
* globally applicable value-preserving step.
|
||||
* 10. The `provenance` column is a tag to indicate the origin and verification of a model.
|
||||
* The format is {origin}-{verification} or just "manual" where the origin describes
|
||||
* the origin of the model and verification describes how the model has been verified.
|
||||
* Some examples are:
|
||||
* - "df-generated": The model has been generated by the model generator tool.
|
||||
* - "df-manual": The model has been generated by the model generator and verified by a human.
|
||||
* - "manual": The model has been written by hand.
|
||||
* This information is used in a heuristic for dataflow analysis to determine, if a
|
||||
* model or source code should be used for determining flow.
|
||||
*/
|
||||
|
||||
import cpp
|
||||
@@ -931,13 +947,13 @@ private module Cached {
|
||||
|
||||
private predicate barrierGuardChecks(IRGuardCondition g, Expr e, boolean gv, TKindModelPair kmp) {
|
||||
exists(
|
||||
SourceSinkInterpretationInput::InterpretNode n, Public::AcceptingValue acceptingvalue,
|
||||
SourceSinkInterpretationInput::InterpretNode n, Public::AcceptingValue acceptingValue,
|
||||
string kind, string model
|
||||
|
|
||||
isBarrierGuardNode(n, acceptingvalue, kind, model) and
|
||||
isBarrierGuardNode(n, acceptingValue, kind, model) and
|
||||
n.asNode().asExpr() = e and
|
||||
kmp = TMkPair(kind, model) and
|
||||
gv = convertAcceptingValue(acceptingvalue).asBooleanValue() and
|
||||
gv = convertAcceptingValue(acceptingValue).asBooleanValue() and
|
||||
n.asNode().(Private::ArgumentNode).getCall().asCallInstruction() = g
|
||||
)
|
||||
}
|
||||
@@ -954,14 +970,14 @@ private module Cached {
|
||||
) {
|
||||
exists(
|
||||
SourceSinkInterpretationInput::InterpretNode interpretNode,
|
||||
Public::AcceptingValue acceptingvalue, string kind, string model, int indirectionIndex,
|
||||
Public::AcceptingValue acceptingValue, string kind, string model, int indirectionIndex,
|
||||
Private::ArgumentNode arg
|
||||
|
|
||||
isBarrierGuardNode(interpretNode, acceptingvalue, kind, model) and
|
||||
isBarrierGuardNode(interpretNode, acceptingValue, kind, model) and
|
||||
arg = interpretNode.asNode() and
|
||||
arg.asIndirectExpr(indirectionIndex) = e and
|
||||
kmp = MkKindModelPairIntPair(TMkPair(kind, model), indirectionIndex) and
|
||||
gv = convertAcceptingValue(acceptingvalue).asBooleanValue() and
|
||||
gv = convertAcceptingValue(acceptingValue).asBooleanValue() and
|
||||
arg.getCall().asCallInstruction() = g
|
||||
)
|
||||
}
|
||||
|
||||
@@ -33,7 +33,7 @@ extensible predicate barrierModel(
|
||||
*/
|
||||
extensible predicate barrierGuardModel(
|
||||
string namespace, string type, boolean subtypes, string name, string signature, string ext,
|
||||
string input, string acceptingvalue, string kind, string provenance, QlBuiltins::ExtensionId madId
|
||||
string input, string acceptingValue, string kind, string provenance, QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
/**
|
||||
|
||||
@@ -162,13 +162,13 @@ module SourceSinkInterpretationInput implements
|
||||
}
|
||||
|
||||
predicate barrierGuardElement(
|
||||
Element e, string input, Public::AcceptingValue acceptingvalue, string kind,
|
||||
Element e, string input, Public::AcceptingValue acceptingValue, string kind,
|
||||
Public::Provenance provenance, string model
|
||||
) {
|
||||
exists(
|
||||
string package, string type, boolean subtypes, string name, string signature, string ext
|
||||
|
|
||||
barrierGuardModel(package, type, subtypes, name, signature, ext, input, acceptingvalue, kind,
|
||||
barrierGuardModel(package, type, subtypes, name, signature, ext, input, acceptingValue, kind,
|
||||
provenance, model) and
|
||||
e = interpretElement(package, type, subtypes, name, signature, ext)
|
||||
)
|
||||
|
||||
@@ -4,13 +4,17 @@
|
||||
* Provides classes and predicates for dealing with MaD flow models specified
|
||||
* in data extensions and CSV format.
|
||||
*
|
||||
* The CSV specification has the following columns:
|
||||
* The extensible relations have the following columns:
|
||||
* - Sources:
|
||||
* `namespace; type; subtypes; name; signature; ext; output; kind; provenance`
|
||||
* - Sinks:
|
||||
* `namespace; type; subtypes; name; signature; ext; input; kind; provenance`
|
||||
* - Summaries:
|
||||
* `namespace; type; subtypes; name; signature; ext; input; output; kind; provenance`
|
||||
* - Barriers:
|
||||
* `namespace; type; subtypes; name; signature; ext; output; kind; provenance`
|
||||
* - BarrierGuards:
|
||||
* `namespace; type; subtypes; name; signature; ext; input; acceptingValue; kind; provenance`
|
||||
* - Neutrals:
|
||||
* `namespace; type; name; signature; kind; provenance`
|
||||
* A neutral is used to indicate that a callable is neutral with respect to flow (no summary), source (is not a source) or sink (is not a sink).
|
||||
@@ -69,14 +73,17 @@
|
||||
* - "Field[f]": Selects the contents of field `f`.
|
||||
* - "Property[p]": Selects the contents of property `p`.
|
||||
*
|
||||
* 8. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* 8. The `acceptingValue` column of barrier guard models specifies the condition
|
||||
* under which the guard blocks flow. It can be one of "true" or "false". In
|
||||
* the future "no-exception", "not-zero", "null", "not-null" may be supported.
|
||||
* 9. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* which classes the interpreted elements should be added. For example, for
|
||||
* sources "remote" indicates a default remote flow source, and for summaries
|
||||
* "taint" indicates a default additional taint step and "value" indicates a
|
||||
* globally applicable value-preserving step. For neutrals the kind can be `summary`,
|
||||
* `source` or `sink` to indicate that the neutral is neutral with respect to
|
||||
* flow (no summary), source (is not a source) or sink (is not a sink).
|
||||
* 9. The `provenance` column is a tag to indicate the origin and verification of a model.
|
||||
* 10. The `provenance` column is a tag to indicate the origin and verification of a model.
|
||||
* The format is {origin}-{verification} or just "manual" where the origin describes
|
||||
* the origin of the model and verification describes how the model has been verified.
|
||||
* Some examples are:
|
||||
@@ -230,11 +237,11 @@ module ModelValidation {
|
||||
result = "Unrecognized provenance description \"" + provenance + "\" in " + pred + " model."
|
||||
)
|
||||
or
|
||||
exists(string acceptingvalue |
|
||||
barrierGuardModel(_, _, _, _, _, _, _, acceptingvalue, _, _, _) and
|
||||
invalidAcceptingValue(acceptingvalue) and
|
||||
exists(string acceptingValue |
|
||||
barrierGuardModel(_, _, _, _, _, _, _, acceptingValue, _, _, _) and
|
||||
invalidAcceptingValue(acceptingValue) and
|
||||
result =
|
||||
"Unrecognized accepting value description \"" + acceptingvalue +
|
||||
"Unrecognized accepting value description \"" + acceptingValue +
|
||||
"\" in barrier guard model."
|
||||
)
|
||||
}
|
||||
@@ -482,13 +489,13 @@ private module Cached {
|
||||
|
||||
private predicate barrierGuardChecks(Guard g, Expr e, GuardValue gv, TKindModelPair kmp) {
|
||||
exists(
|
||||
SourceSinkInterpretationInput::InterpretNode n, AcceptingValue acceptingvalue, string kind,
|
||||
SourceSinkInterpretationInput::InterpretNode n, AcceptingValue acceptingValue, string kind,
|
||||
string model
|
||||
|
|
||||
isBarrierGuardNode(n, acceptingvalue, kind, model) and
|
||||
isBarrierGuardNode(n, acceptingValue, kind, model) and
|
||||
n.asNode().asExpr() = e and
|
||||
kmp = TMkPair(kind, model) and
|
||||
gv = convertAcceptingValue(acceptingvalue)
|
||||
gv = convertAcceptingValue(acceptingValue)
|
||||
|
|
||||
g.(Call).getAnArgument() = e or g.(QualifiableExpr).getQualifier() = e
|
||||
)
|
||||
|
||||
@@ -33,7 +33,7 @@ extensible predicate barrierModel(
|
||||
*/
|
||||
extensible predicate barrierGuardModel(
|
||||
string namespace, string type, boolean subtypes, string name, string signature, string ext,
|
||||
string input, string acceptingvalue, string kind, string provenance, QlBuiltins::ExtensionId madId
|
||||
string input, string acceptingValue, string kind, string provenance, QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
/**
|
||||
|
||||
@@ -253,13 +253,13 @@ module SourceSinkInterpretationInput implements
|
||||
}
|
||||
|
||||
predicate barrierGuardElement(
|
||||
Element e, string input, Public::AcceptingValue acceptingvalue, string kind,
|
||||
Element e, string input, Public::AcceptingValue acceptingValue, string kind,
|
||||
Public::Provenance provenance, string model
|
||||
) {
|
||||
exists(
|
||||
string namespace, string type, boolean subtypes, string name, string signature, string ext
|
||||
|
|
||||
barrierGuardModel(namespace, type, subtypes, name, signature, ext, input, acceptingvalue,
|
||||
barrierGuardModel(namespace, type, subtypes, name, signature, ext, input, acceptingValue,
|
||||
kind, provenance, model) and
|
||||
e = interpretElement(namespace, type, subtypes, name, signature, ext, _)
|
||||
)
|
||||
|
||||
@@ -4,13 +4,17 @@
|
||||
* Provides classes and predicates for dealing with flow models specified
|
||||
* in data extensions and CSV format.
|
||||
*
|
||||
* The CSV specification has the following columns:
|
||||
* The extensible relations have the following columns:
|
||||
* - Sources:
|
||||
* `package; type; subtypes; name; signature; ext; output; kind; provenance`
|
||||
* - Sinks:
|
||||
* `package; type; subtypes; name; signature; ext; input; kind; provenance`
|
||||
* - Summaries:
|
||||
* `package; type; subtypes; name; signature; ext; input; output; kind; provenance`
|
||||
* - Barriers:
|
||||
* `package; type; subtypes; name; signature; ext; output; kind; provenance`
|
||||
* - BarrierGuards:
|
||||
* `package; type; subtypes; name; signature; ext; input; acceptingValue; kind; provenance`
|
||||
* - Neutrals:
|
||||
* `package; type; name; signature; kind; provenance`
|
||||
* A neutral is used to indicate that a callable is neutral with respect to flow (no summary), source (is not a source) or sink (is not a sink).
|
||||
@@ -78,11 +82,23 @@
|
||||
* - "MapValue": Selects a value in a map.
|
||||
* - "Dereference": Selects the value referenced by a pointer.
|
||||
*
|
||||
* 8. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* 8. The `acceptingValue` column of barrier guard models specifies the condition
|
||||
* under which the guard blocks flow. It can be one of "true" or "false". In
|
||||
* the future "no-exception", "not-zero", "null", "not-null" may be supported.
|
||||
* 9. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* which classes the interpreted elements should be added. For example, for
|
||||
* sources "remote" indicates a default remote flow source, and for summaries
|
||||
* "taint" indicates a default additional taint step and "value" indicates a
|
||||
* globally applicable value-preserving step.
|
||||
* 10. The `provenance` column is a tag to indicate the origin and verification of a model.
|
||||
* The format is {origin}-{verification} or just "manual" where the origin describes
|
||||
* the origin of the model and verification describes how the model has been verified.
|
||||
* Some examples are:
|
||||
* - "df-generated": The model has been generated by the model generator tool.
|
||||
* - "df-manual": The model has been generated by the model generator and verified by a human.
|
||||
* - "manual": The model has been written by hand.
|
||||
* This information is used in a heuristic for dataflow analysis to determine, if a
|
||||
* model or source code should be used for determining flow.
|
||||
*/
|
||||
overlay[local?]
|
||||
module;
|
||||
@@ -250,11 +266,11 @@ module ModelValidation {
|
||||
result = "Unrecognized provenance description \"" + provenance + "\" in " + pred + " model."
|
||||
)
|
||||
or
|
||||
exists(string acceptingvalue |
|
||||
barrierGuardModel(_, _, _, _, _, _, _, acceptingvalue, _, _, _) and
|
||||
invalidAcceptingValue(acceptingvalue) and
|
||||
exists(string acceptingValue |
|
||||
barrierGuardModel(_, _, _, _, _, _, _, acceptingValue, _, _, _) and
|
||||
invalidAcceptingValue(acceptingValue) and
|
||||
result =
|
||||
"Unrecognized accepting value description \"" + acceptingvalue +
|
||||
"Unrecognized accepting value description \"" + acceptingValue +
|
||||
"\" in barrier guard model."
|
||||
)
|
||||
}
|
||||
@@ -462,13 +478,13 @@ private module Cached {
|
||||
|
||||
private predicate barrierGuardChecks(DataFlow::Node g, Expr e, boolean gv, TKindModelPair kmp) {
|
||||
exists(
|
||||
SourceSinkInterpretationInput::InterpretNode n, Public::AcceptingValue acceptingvalue,
|
||||
SourceSinkInterpretationInput::InterpretNode n, Public::AcceptingValue acceptingValue,
|
||||
string kind, string model
|
||||
|
|
||||
isBarrierGuardNode(n, acceptingvalue, kind, model) and
|
||||
isBarrierGuardNode(n, acceptingValue, kind, model) and
|
||||
n.asNode().asExpr() = e and
|
||||
kmp = TMkPair(kind, model) and
|
||||
gv = convertAcceptingValue(acceptingvalue)
|
||||
gv = convertAcceptingValue(acceptingValue)
|
||||
|
|
||||
g.asExpr().(CallExpr).getAnArgument() = e // TODO: qualifier?
|
||||
)
|
||||
|
||||
@@ -35,7 +35,7 @@ extensible predicate barrierModel(
|
||||
*/
|
||||
extensible predicate barrierGuardModel(
|
||||
string package, string type, boolean subtypes, string name, string signature, string ext,
|
||||
string input, string acceptingvalue, string kind, string provenance, QlBuiltins::ExtensionId madId
|
||||
string input, string acceptingValue, string kind, string provenance, QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
/**
|
||||
|
||||
@@ -174,13 +174,13 @@ module SourceSinkInterpretationInput implements
|
||||
}
|
||||
|
||||
predicate barrierGuardElement(
|
||||
Element e, string input, Public::AcceptingValue acceptingvalue, string kind,
|
||||
Element e, string input, Public::AcceptingValue acceptingValue, string kind,
|
||||
Public::Provenance provenance, string model
|
||||
) {
|
||||
exists(
|
||||
string package, string type, boolean subtypes, string name, string signature, string ext
|
||||
|
|
||||
barrierGuardModel(package, type, subtypes, name, signature, ext, input, acceptingvalue, kind,
|
||||
barrierGuardModel(package, type, subtypes, name, signature, ext, input, acceptingValue, kind,
|
||||
provenance, model) and
|
||||
e = interpretElement(package, type, subtypes, name, signature, ext)
|
||||
)
|
||||
|
||||
@@ -4,13 +4,17 @@
|
||||
* Provides classes and predicates for dealing with flow models specified
|
||||
* in data extensions and CSV format.
|
||||
*
|
||||
* The CSV specification has the following columns:
|
||||
* The extensible relations have the following columns:
|
||||
* - Sources:
|
||||
* `package; type; subtypes; name; signature; ext; output; kind; provenance`
|
||||
* - Sinks:
|
||||
* `package; type; subtypes; name; signature; ext; input; kind; provenance`
|
||||
* - Summaries:
|
||||
* `package; type; subtypes; name; signature; ext; input; output; kind; provenance`
|
||||
* - Barriers:
|
||||
* `package; type; subtypes; name; signature; ext; output; kind; provenance`
|
||||
* - BarrierGuards:
|
||||
* `package; type; subtypes; name; signature; ext; input; acceptingValue; kind; provenance`
|
||||
* - Neutrals:
|
||||
* `package; type; name; signature; kind; provenance`
|
||||
* A neutral is used to indicate that a callable is neutral with respect to flow (no summary), source (is not a source) or sink (is not a sink).
|
||||
@@ -69,14 +73,17 @@
|
||||
* in the given range. The range is inclusive at both ends.
|
||||
* - "ReturnValue": Selects the return value of a call to the selected element.
|
||||
* - "Element": Selects the collection elements of the selected element.
|
||||
* 8. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* 8. The `acceptingValue` column of barrier guard models specifies the condition
|
||||
* under which the guard blocks flow. It can be one of "true" or "false". In
|
||||
* the future "no-exception", "not-zero", "null", "not-null" may be supported.
|
||||
* 9. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* which classes the interpreted elements should be added. For example, for
|
||||
* sources "remote" indicates a default remote flow source, and for summaries
|
||||
* "taint" indicates a default additional taint step and "value" indicates a
|
||||
* globally applicable value-preserving step. For neutrals the kind can be `summary`,
|
||||
* `source` or `sink` to indicate that the neutral is neutral with respect to
|
||||
* flow (no summary), source (is not a source) or sink (is not a sink).
|
||||
* 9. The `provenance` column is a tag to indicate the origin and verification of a model.
|
||||
* 10. The `provenance` column is a tag to indicate the origin and verification of a model.
|
||||
* The format is {origin}-{verification} or just "manual" where the origin describes
|
||||
* the origin of the model and verification describes how the model has been verified.
|
||||
* Some examples are:
|
||||
@@ -358,11 +365,11 @@ module ModelValidation {
|
||||
result = "Unrecognized provenance description \"" + provenance + "\" in " + pred + " model."
|
||||
)
|
||||
or
|
||||
exists(string acceptingvalue |
|
||||
barrierGuardModel(_, _, _, _, _, _, _, acceptingvalue, _, _, _) and
|
||||
invalidAcceptingValue(acceptingvalue) and
|
||||
exists(string acceptingValue |
|
||||
barrierGuardModel(_, _, _, _, _, _, _, acceptingValue, _, _, _) and
|
||||
invalidAcceptingValue(acceptingValue) and
|
||||
result =
|
||||
"Unrecognized accepting value description \"" + acceptingvalue +
|
||||
"Unrecognized accepting value description \"" + acceptingValue +
|
||||
"\" in barrier guard model."
|
||||
)
|
||||
}
|
||||
@@ -583,13 +590,13 @@ private module Cached {
|
||||
|
||||
private predicate barrierGuardChecks(Guard g, Expr e, GuardValue gv, TKindModelPair kmp) {
|
||||
exists(
|
||||
SourceSinkInterpretationInput::InterpretNode n, AcceptingValue acceptingvalue, string kind,
|
||||
SourceSinkInterpretationInput::InterpretNode n, AcceptingValue acceptingValue, string kind,
|
||||
string model
|
||||
|
|
||||
isBarrierGuardNode(n, acceptingvalue, kind, model) and
|
||||
isBarrierGuardNode(n, acceptingValue, kind, model) and
|
||||
n.asNode().asExpr() = e and
|
||||
kmp = TMkPair(kind, model) and
|
||||
gv = convertAcceptingValue(acceptingvalue)
|
||||
gv = convertAcceptingValue(acceptingValue)
|
||||
|
|
||||
g.(Call).getAnArgument() = e or g.(MethodCall).getQualifier() = e
|
||||
)
|
||||
|
||||
@@ -35,7 +35,7 @@ extensible predicate barrierModel(
|
||||
*/
|
||||
extensible predicate barrierGuardModel(
|
||||
string package, string type, boolean subtypes, string name, string signature, string ext,
|
||||
string input, string acceptingvalue, string kind, string provenance, QlBuiltins::ExtensionId madId
|
||||
string input, string acceptingValue, string kind, string provenance, QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
/**
|
||||
|
||||
@@ -282,7 +282,7 @@ module SourceSinkInterpretationInput implements
|
||||
}
|
||||
|
||||
predicate barrierGuardElement(
|
||||
Element e, string input, Public::AcceptingValue acceptingvalue, string kind,
|
||||
Element e, string input, Public::AcceptingValue acceptingValue, string kind,
|
||||
Public::Provenance provenance, string model
|
||||
) {
|
||||
exists(
|
||||
@@ -290,7 +290,7 @@ module SourceSinkInterpretationInput implements
|
||||
SourceOrSinkElement baseBarrier, string originalInput
|
||||
|
|
||||
barrierGuardModel(namespace, type, subtypes, name, signature, ext, originalInput,
|
||||
acceptingvalue, kind, provenance, model) and
|
||||
acceptingValue, kind, provenance, model) and
|
||||
baseBarrier = interpretElement(namespace, type, subtypes, name, signature, ext, _) and
|
||||
(
|
||||
e = baseBarrier and input = originalInput
|
||||
|
||||
@@ -10,6 +10,10 @@
|
||||
* `type, path, kind`
|
||||
* - Summaries:
|
||||
* `type, path, input, output, kind`
|
||||
* - Barriers:
|
||||
* `type, path, kind`
|
||||
* - BarrierGuards:
|
||||
* `type, path, acceptingValue, kind`
|
||||
* - Types:
|
||||
* `type1, type2, path`
|
||||
*
|
||||
@@ -42,7 +46,8 @@
|
||||
* 3. The `input` and `output` columns specify how data enters and leaves the element selected by the
|
||||
* first `(type, path)` tuple. Both strings are `.`-separated access paths
|
||||
* of the same syntax as the `path` column.
|
||||
* 4. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* 4. The `acceptingValue` column of barrier guard models specifies which branch of the guard is blocking flow. It can be "true" or "false".
|
||||
* 5. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* which classes the interpreted elements should be added. For example, for
|
||||
* sources `"remote"` indicates a default remote flow source, and for summaries
|
||||
* `"taint"` indicates a default additional taint step and `"value"` indicates a
|
||||
@@ -355,11 +360,11 @@ private predicate barrierModel(string type, string path, string kind, string mod
|
||||
|
||||
/** Holds if a barrier guard model exists for the given parameters. */
|
||||
private predicate barrierGuardModel(
|
||||
string type, string path, string branch, string kind, string model
|
||||
string type, string path, string acceptingValue, string kind, string model
|
||||
) {
|
||||
// No deprecation adapter for barrier models, they were not around back then.
|
||||
exists(QlBuiltins::ExtensionId madId |
|
||||
Extensions::barrierGuardModel(type, path, branch, kind, madId) and
|
||||
Extensions::barrierGuardModel(type, path, acceptingValue, kind, madId) and
|
||||
model = "MaD:" + madId.toString()
|
||||
)
|
||||
}
|
||||
@@ -783,16 +788,16 @@ module ModelOutput {
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a barrier model contributed `barrier` with the given `kind` for the given `branch`.
|
||||
* Holds if a barrier model contributed `barrier` with the given `kind` for the given `acceptingValue`.
|
||||
*/
|
||||
cached
|
||||
API::Node getABarrierGuardNode(string kind, boolean branch, string model) {
|
||||
exists(string type, string path, string branch_str |
|
||||
branch = true and branch_str = "true"
|
||||
API::Node getABarrierGuardNode(string kind, boolean acceptingValue, string model) {
|
||||
exists(string type, string path, string acceptingValue_str |
|
||||
acceptingValue = true and acceptingValue_str = "true"
|
||||
or
|
||||
branch = false and branch_str = "false"
|
||||
acceptingValue = false and acceptingValue_str = "false"
|
||||
|
|
||||
barrierGuardModel(type, path, branch_str, kind, model) and
|
||||
barrierGuardModel(type, path, acceptingValue_str, kind, model) and
|
||||
result = getNodeFromPath(type, path)
|
||||
)
|
||||
}
|
||||
@@ -856,12 +861,12 @@ module ModelOutput {
|
||||
API::Node getABarrierNode(string kind) { result = getABarrierNode(kind, _) }
|
||||
|
||||
/**
|
||||
* Holds if an external model contributed `barrier-guard` with the given `kind` and `branch`.
|
||||
* Holds if an external model contributed `barrier-guard` with the given `kind` and `acceptingValue`.
|
||||
*
|
||||
* INTERNAL: Do not use.
|
||||
*/
|
||||
API::Node getABarrierGuardNode(string kind, boolean branch) {
|
||||
result = getABarrierGuardNode(kind, branch, _)
|
||||
API::Node getABarrierGuardNode(string kind, boolean acceptingValue) {
|
||||
result = getABarrierGuardNode(kind, acceptingValue, _)
|
||||
}
|
||||
|
||||
/**
|
||||
|
||||
@@ -33,11 +33,11 @@ extensible predicate barrierModel(
|
||||
* of the given `kind` and `madId` is the data extension row number.
|
||||
* `path` is assumed to lead to a parameter of a call (possibly `self`), and
|
||||
* the call is guarding the parameter.
|
||||
* `branch` is either `true` or `false`, indicating which branch of the guard
|
||||
* is protecting the parameter.
|
||||
* `acceptingValue` is either `true` or `false`, indicating which branch of
|
||||
* the guard is protecting the parameter.
|
||||
*/
|
||||
extensible predicate barrierGuardModel(
|
||||
string type, string path, string branch, string kind, QlBuiltins::ExtensionId madId
|
||||
string type, string path, string acceptingValue, string kind, QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
/**
|
||||
|
||||
@@ -10,6 +10,10 @@
|
||||
* `type, path, kind`
|
||||
* - Summaries:
|
||||
* `type, path, input, output, kind`
|
||||
* - Barriers:
|
||||
* `type, path, kind`
|
||||
* - BarrierGuards:
|
||||
* `type, path, acceptingValue, kind`
|
||||
* - Types:
|
||||
* `type1, type2, path`
|
||||
*
|
||||
@@ -42,7 +46,8 @@
|
||||
* 3. The `input` and `output` columns specify how data enters and leaves the element selected by the
|
||||
* first `(type, path)` tuple. Both strings are `.`-separated access paths
|
||||
* of the same syntax as the `path` column.
|
||||
* 4. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* 4. The `acceptingValue` column of barrier guard models specifies which branch of the guard is blocking flow. It can be "true" or "false".
|
||||
* 5. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* which classes the interpreted elements should be added. For example, for
|
||||
* sources `"remote"` indicates a default remote flow source, and for summaries
|
||||
* `"taint"` indicates a default additional taint step and `"value"` indicates a
|
||||
@@ -355,11 +360,11 @@ private predicate barrierModel(string type, string path, string kind, string mod
|
||||
|
||||
/** Holds if a barrier guard model exists for the given parameters. */
|
||||
private predicate barrierGuardModel(
|
||||
string type, string path, string branch, string kind, string model
|
||||
string type, string path, string acceptingValue, string kind, string model
|
||||
) {
|
||||
// No deprecation adapter for barrier models, they were not around back then.
|
||||
exists(QlBuiltins::ExtensionId madId |
|
||||
Extensions::barrierGuardModel(type, path, branch, kind, madId) and
|
||||
Extensions::barrierGuardModel(type, path, acceptingValue, kind, madId) and
|
||||
model = "MaD:" + madId.toString()
|
||||
)
|
||||
}
|
||||
@@ -783,16 +788,16 @@ module ModelOutput {
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a barrier model contributed `barrier` with the given `kind` for the given `branch`.
|
||||
* Holds if a barrier model contributed `barrier` with the given `kind` for the given `acceptingValue`.
|
||||
*/
|
||||
cached
|
||||
API::Node getABarrierGuardNode(string kind, boolean branch, string model) {
|
||||
exists(string type, string path, string branch_str |
|
||||
branch = true and branch_str = "true"
|
||||
API::Node getABarrierGuardNode(string kind, boolean acceptingValue, string model) {
|
||||
exists(string type, string path, string acceptingValue_str |
|
||||
acceptingValue = true and acceptingValue_str = "true"
|
||||
or
|
||||
branch = false and branch_str = "false"
|
||||
acceptingValue = false and acceptingValue_str = "false"
|
||||
|
|
||||
barrierGuardModel(type, path, branch_str, kind, model) and
|
||||
barrierGuardModel(type, path, acceptingValue_str, kind, model) and
|
||||
result = getNodeFromPath(type, path)
|
||||
)
|
||||
}
|
||||
@@ -856,12 +861,12 @@ module ModelOutput {
|
||||
API::Node getABarrierNode(string kind) { result = getABarrierNode(kind, _) }
|
||||
|
||||
/**
|
||||
* Holds if an external model contributed `barrier-guard` with the given `kind` and `branch`.
|
||||
* Holds if an external model contributed `barrier-guard` with the given `kind` and `acceptingValue`.
|
||||
*
|
||||
* INTERNAL: Do not use.
|
||||
*/
|
||||
API::Node getABarrierGuardNode(string kind, boolean branch) {
|
||||
result = getABarrierGuardNode(kind, branch, _)
|
||||
API::Node getABarrierGuardNode(string kind, boolean acceptingValue) {
|
||||
result = getABarrierGuardNode(kind, acceptingValue, _)
|
||||
}
|
||||
|
||||
/**
|
||||
|
||||
@@ -33,11 +33,11 @@ extensible predicate barrierModel(
|
||||
* of the given `kind` and `madId` is the data extension row number.
|
||||
* `path` is assumed to lead to a parameter of a call (possibly `self`), and
|
||||
* the call is guarding the parameter.
|
||||
* `branch` is either `true` or `false`, indicating which branch of the guard
|
||||
* is protecting the parameter.
|
||||
* `acceptingValue` is either `true` or `false`, indicating which branch of
|
||||
* the guard is protecting the parameter.
|
||||
*/
|
||||
extensible predicate barrierGuardModel(
|
||||
string type, string path, string branch, string kind, QlBuiltins::ExtensionId madId
|
||||
string type, string path, string acceptingValue, string kind, QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
/**
|
||||
|
||||
@@ -10,6 +10,10 @@
|
||||
* `type, path, kind`
|
||||
* - Summaries:
|
||||
* `type, path, input, output, kind`
|
||||
* - Barriers:
|
||||
* `type, path, kind`
|
||||
* - BarrierGuards:
|
||||
* `type, path, acceptingValue, kind`
|
||||
* - Types:
|
||||
* `type1, type2, path`
|
||||
*
|
||||
@@ -42,7 +46,8 @@
|
||||
* 3. The `input` and `output` columns specify how data enters and leaves the element selected by the
|
||||
* first `(type, path)` tuple. Both strings are `.`-separated access paths
|
||||
* of the same syntax as the `path` column.
|
||||
* 4. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* 4. The `acceptingValue` column of barrier guard models specifies which branch of the guard is blocking flow. It can be "true" or "false".
|
||||
* 5. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* which classes the interpreted elements should be added. For example, for
|
||||
* sources `"remote"` indicates a default remote flow source, and for summaries
|
||||
* `"taint"` indicates a default additional taint step and `"value"` indicates a
|
||||
@@ -355,11 +360,11 @@ private predicate barrierModel(string type, string path, string kind, string mod
|
||||
|
||||
/** Holds if a barrier guard model exists for the given parameters. */
|
||||
private predicate barrierGuardModel(
|
||||
string type, string path, string branch, string kind, string model
|
||||
string type, string path, string acceptingValue, string kind, string model
|
||||
) {
|
||||
// No deprecation adapter for barrier models, they were not around back then.
|
||||
exists(QlBuiltins::ExtensionId madId |
|
||||
Extensions::barrierGuardModel(type, path, branch, kind, madId) and
|
||||
Extensions::barrierGuardModel(type, path, acceptingValue, kind, madId) and
|
||||
model = "MaD:" + madId.toString()
|
||||
)
|
||||
}
|
||||
@@ -783,16 +788,16 @@ module ModelOutput {
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a barrier model contributed `barrier` with the given `kind` for the given `branch`.
|
||||
* Holds if a barrier model contributed `barrier` with the given `kind` for the given `acceptingValue`.
|
||||
*/
|
||||
cached
|
||||
API::Node getABarrierGuardNode(string kind, boolean branch, string model) {
|
||||
exists(string type, string path, string branch_str |
|
||||
branch = true and branch_str = "true"
|
||||
API::Node getABarrierGuardNode(string kind, boolean acceptingValue, string model) {
|
||||
exists(string type, string path, string acceptingValue_str |
|
||||
acceptingValue = true and acceptingValue_str = "true"
|
||||
or
|
||||
branch = false and branch_str = "false"
|
||||
acceptingValue = false and acceptingValue_str = "false"
|
||||
|
|
||||
barrierGuardModel(type, path, branch_str, kind, model) and
|
||||
barrierGuardModel(type, path, acceptingValue_str, kind, model) and
|
||||
result = getNodeFromPath(type, path)
|
||||
)
|
||||
}
|
||||
@@ -856,12 +861,12 @@ module ModelOutput {
|
||||
API::Node getABarrierNode(string kind) { result = getABarrierNode(kind, _) }
|
||||
|
||||
/**
|
||||
* Holds if an external model contributed `barrier-guard` with the given `kind` and `branch`.
|
||||
* Holds if an external model contributed `barrier-guard` with the given `kind` and `acceptingValue`.
|
||||
*
|
||||
* INTERNAL: Do not use.
|
||||
*/
|
||||
API::Node getABarrierGuardNode(string kind, boolean branch) {
|
||||
result = getABarrierGuardNode(kind, branch, _)
|
||||
API::Node getABarrierGuardNode(string kind, boolean acceptingValue) {
|
||||
result = getABarrierGuardNode(kind, acceptingValue, _)
|
||||
}
|
||||
|
||||
/**
|
||||
|
||||
@@ -33,11 +33,11 @@ extensible predicate barrierModel(
|
||||
* of the given `kind` and `madId` is the data extension row number.
|
||||
* `path` is assumed to lead to a parameter of a call (possibly `self`), and
|
||||
* the call is guarding the parameter.
|
||||
* `branch` is either `true` or `false`, indicating which branch of the guard
|
||||
* is protecting the parameter.
|
||||
* `acceptingValue` is either `true` or `false`, indicating which branch of
|
||||
* the guard is protecting the parameter.
|
||||
*/
|
||||
extensible predicate barrierGuardModel(
|
||||
string type, string path, string branch, string kind, QlBuiltins::ExtensionId madId
|
||||
string type, string path, string acceptingValue, string kind, QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
/**
|
||||
|
||||
@@ -1183,12 +1183,12 @@ private module Cached {
|
||||
exists(
|
||||
FlowSummaryImpl::Public::BarrierGuardElement b,
|
||||
FlowSummaryImpl::Private::SummaryComponentStack stack,
|
||||
FlowSummaryImpl::Public::AcceptingValue acceptingvalue, string kind, string model
|
||||
FlowSummaryImpl::Public::AcceptingValue acceptingValue, string kind, string model
|
||||
|
|
||||
FlowSummaryImpl::Private::barrierGuardSpec(b, stack, acceptingvalue, kind, model) and
|
||||
FlowSummaryImpl::Private::barrierGuardSpec(b, stack, acceptingValue, kind, model) and
|
||||
e = FlowSummaryImpl::StepsInput::getSinkNode(b, stack.headOfSingleton()).asExpr() and
|
||||
kmp = TMkPair(kind, model) and
|
||||
gv = convertAcceptingValue(acceptingvalue) and
|
||||
gv = convertAcceptingValue(acceptingValue) and
|
||||
g = b.getCall()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -9,6 +9,13 @@
|
||||
* `path; input; kind; provenance`
|
||||
* - Summaries:
|
||||
* `path; input; output; kind; provenance`
|
||||
* - Barriers:
|
||||
* `path; output; kind; provenance`
|
||||
* - BarrierGuards:
|
||||
* `path; input; acceptingValue; kind; provenance`
|
||||
* - Neutrals:
|
||||
* `path; kind; provenance`
|
||||
* A neutral is used to indicate that a callable is neutral with respect to flow (no summary), source (is not a source) or sink (is not a sink).
|
||||
*
|
||||
* The interpretation of a row is similar to API-graphs with a left-to-right
|
||||
* reading.
|
||||
@@ -34,12 +41,15 @@
|
||||
* - `Field[i]`: the `i`th element of a tuple.
|
||||
* - `Reference`: the referenced value.
|
||||
* - `Future`: the value being computed asynchronously.
|
||||
* 3. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* 3. The `acceptingValue` column of barrier guard models specifies which branch of the
|
||||
* guard is blocking flow. It can be "true" or "false". In the future
|
||||
* "no-exception", "not-zero", "null", "not-null" may be supported.
|
||||
* 4. The `kind` column is a tag that can be referenced from QL to determine to
|
||||
* which classes the interpreted elements should be added. For example, for
|
||||
* sources `"remote"` indicates a default remote flow source, and for summaries
|
||||
* `"taint"` indicates a default additional taint step and `"value"` indicates a
|
||||
* globally applicable value-preserving step.
|
||||
* 4. The `provenance` column is mainly used internally, and should be set to `"manual"` for
|
||||
* 5. The `provenance` column is mainly used internally, and should be set to `"manual"` for
|
||||
* all custom models.
|
||||
*/
|
||||
|
||||
@@ -114,11 +124,12 @@ extensible predicate barrierModel(
|
||||
* extension row number.
|
||||
*
|
||||
* The value referred to by `input` is assumed to lead to an argument of a call
|
||||
* (possibly `self`), and the call is guarding the argument. `branch` is either `true`
|
||||
* or `false`, indicating which branch of the guard is protecting the argument.
|
||||
* (possibly `self`), and the call is guarding the argument.
|
||||
* `acceptingValue` is either `true` or `false`, indicating which branch of
|
||||
* the guard is protecting the parameter.
|
||||
*/
|
||||
extensible predicate barrierGuardModel(
|
||||
string path, string input, string branch, string kind, string provenance,
|
||||
string path, string input, string acceptingValue, string kind, string provenance,
|
||||
QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
@@ -153,9 +164,9 @@ predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) {
|
||||
model = "Barrier: " + path + "; " + output + "; " + kind
|
||||
)
|
||||
or
|
||||
exists(string path, string input, string branch, string kind |
|
||||
barrierGuardModel(path, input, branch, kind, _, madId) and
|
||||
model = "Barrier guard: " + path + "; " + input + "; " + branch + "; " + kind
|
||||
exists(string path, string input, string acceptingValue, string kind |
|
||||
barrierGuardModel(path, input, acceptingValue, kind, _, madId) and
|
||||
model = "Barrier guard: " + path + "; " + input + "; " + acceptingValue + "; " + kind
|
||||
)
|
||||
}
|
||||
|
||||
@@ -265,10 +276,10 @@ private class FlowBarrierGuardFromModel extends FlowBarrierGuard::Range {
|
||||
}
|
||||
|
||||
override predicate isBarrierGuard(
|
||||
string input, string branch, string kind, Provenance provenance, string model
|
||||
string input, string acceptingValue, string kind, Provenance provenance, string model
|
||||
) {
|
||||
exists(QlBuiltins::ExtensionId madId |
|
||||
barrierGuardModel(path, input, branch, kind, provenance, madId) and
|
||||
barrierGuardModel(path, input, acceptingValue, kind, provenance, madId) and
|
||||
model = "MaD:" + madId.toString()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -388,11 +388,11 @@ module Make<
|
||||
|
||||
/**
|
||||
* Holds if this element is a flow barrier guard of kind `kind`, for data
|
||||
* flowing in as described by `input`, when `this` evaluates to `branch`.
|
||||
* flowing in as described by `input`, when `this` evaluates to `acceptingValue`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
abstract predicate isBarrierGuard(
|
||||
string input, string branch, string kind, Provenance provenance, string model
|
||||
string input, string acceptingValue, string kind, Provenance provenance, string model
|
||||
);
|
||||
}
|
||||
|
||||
@@ -764,10 +764,10 @@ module Make<
|
||||
}
|
||||
|
||||
private predicate isRelevantBarrierGuard(
|
||||
BarrierGuardElement e, string input, string branch, string kind, Provenance provenance,
|
||||
string model
|
||||
BarrierGuardElement e, string input, string acceptingValue, string kind,
|
||||
Provenance provenance, string model
|
||||
) {
|
||||
e.isBarrierGuard(input, branch, kind, provenance, model) and
|
||||
e.isBarrierGuard(input, acceptingValue, kind, provenance, model) and
|
||||
(
|
||||
provenance.isManual()
|
||||
or
|
||||
@@ -1588,11 +1588,11 @@ module Make<
|
||||
* Holds if `barrierGuard` is a relevant barrier guard element with input specification `inSpec`.
|
||||
*/
|
||||
predicate barrierGuardSpec(
|
||||
BarrierGuardElement barrierGuard, SummaryComponentStack inSpec, string branch, string kind,
|
||||
string model
|
||||
BarrierGuardElement barrierGuard, SummaryComponentStack inSpec, string acceptingValue,
|
||||
string kind, string model
|
||||
) {
|
||||
exists(string input |
|
||||
isRelevantBarrierGuard(barrierGuard, input, branch, kind, _, model) and
|
||||
isRelevantBarrierGuard(barrierGuard, input, acceptingValue, kind, _, model) and
|
||||
External::interpretSpec(input, inSpec)
|
||||
)
|
||||
}
|
||||
@@ -2189,10 +2189,10 @@ module Make<
|
||||
not exists(interpretComponent(c))
|
||||
}
|
||||
|
||||
/** Holds if `acceptingvalue` is not a valid barrier guard accepting-value. */
|
||||
bindingset[acceptingvalue]
|
||||
predicate invalidAcceptingValue(string acceptingvalue) {
|
||||
not acceptingvalue instanceof AcceptingValue
|
||||
/** Holds if `acceptingValue` is not a valid barrier guard accepting-value. */
|
||||
bindingset[acceptingValue]
|
||||
predicate invalidAcceptingValue(string acceptingValue) {
|
||||
not acceptingValue instanceof AcceptingValue
|
||||
}
|
||||
|
||||
/** Holds if `provenance` is not a valid provenance value. */
|
||||
@@ -2242,10 +2242,10 @@ module Make<
|
||||
|
||||
/**
|
||||
* Holds if an external barrier guard specification exists for `n` with input
|
||||
* specification `input`, accepting value `acceptingvalue`, and kind `kind`.
|
||||
* specification `input`, accepting value `acceptingValue`, and kind `kind`.
|
||||
*/
|
||||
predicate barrierGuardElement(
|
||||
Element n, string input, AcceptingValue acceptingvalue, string kind,
|
||||
Element n, string input, AcceptingValue acceptingValue, string kind,
|
||||
Provenance provenance, string model
|
||||
);
|
||||
|
||||
@@ -2371,11 +2371,11 @@ module Make<
|
||||
}
|
||||
|
||||
private predicate barrierGuardElementRef(
|
||||
InterpretNode ref, SourceSinkAccessPath input, AcceptingValue acceptingvalue, string kind,
|
||||
InterpretNode ref, SourceSinkAccessPath input, AcceptingValue acceptingValue, string kind,
|
||||
string model
|
||||
) {
|
||||
exists(SourceOrSinkElement e |
|
||||
barrierGuardElement(e, input, acceptingvalue, kind, _, model) and
|
||||
barrierGuardElement(e, input, acceptingValue, kind, _, model) and
|
||||
if inputNeedsReferenceExt(input.getToken(0))
|
||||
then e = ref.getCallTarget()
|
||||
else e = ref.asElement()
|
||||
@@ -2518,10 +2518,10 @@ module Make<
|
||||
* given kind in a MaD flow model.
|
||||
*/
|
||||
predicate isBarrierGuardNode(
|
||||
InterpretNode node, AcceptingValue acceptingvalue, string kind, string model
|
||||
InterpretNode node, AcceptingValue acceptingValue, string kind, string model
|
||||
) {
|
||||
exists(InterpretNode ref, SourceSinkAccessPath input |
|
||||
barrierGuardElementRef(ref, input, acceptingvalue, kind, model) and
|
||||
barrierGuardElementRef(ref, input, acceptingValue, kind, model) and
|
||||
interpretInput(input, input.getNumToken(), ref, node)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -31,7 +31,7 @@ signature module ExtensionsSig {
|
||||
*/
|
||||
predicate barrierGuardModel(
|
||||
string namespace, string type, boolean subtypes, string name, string signature, string ext,
|
||||
string input, string acceptingvalue, string kind, string provenance,
|
||||
string input, string acceptingValue, string kind, string provenance,
|
||||
QlBuiltins::ExtensionId madId
|
||||
);
|
||||
|
||||
@@ -142,14 +142,14 @@ module ModelsAsData<ExtensionsSig Extensions, InputSig Input> {
|
||||
or
|
||||
exists(
|
||||
string namespace, string type, boolean subtypes, string name, string signature, string ext,
|
||||
string input, string acceptingvalue, string kind, string provenance
|
||||
string input, string acceptingValue, string kind, string provenance
|
||||
|
|
||||
Extensions::barrierGuardModel(namespace, type, subtypes, name, signature, ext, input,
|
||||
acceptingvalue, kind, provenance, madId)
|
||||
acceptingValue, kind, provenance, madId)
|
||||
|
|
||||
model =
|
||||
"Barrier Guard: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " +
|
||||
signature + "; " + ext + "; " + input + "; " + acceptingvalue + "; " + kind + "; " +
|
||||
signature + "; " + ext + "; " + input + "; " + acceptingValue + "; " + kind + "; " +
|
||||
provenance
|
||||
)
|
||||
or
|
||||
@@ -241,12 +241,12 @@ module ModelsAsData<ExtensionsSig Extensions, InputSig Input> {
|
||||
/** Holds if a barrier guard model exists for the given parameters. */
|
||||
predicate barrierGuardModel(
|
||||
string namespace, string type, boolean subtypes, string name, string signature, string ext,
|
||||
string input, string acceptingvalue, string kind, string provenance, string model
|
||||
string input, string acceptingValue, string kind, string provenance, string model
|
||||
) {
|
||||
exists(string namespaceOrGroup, QlBuiltins::ExtensionId madId |
|
||||
namespace = getNamespace(namespaceOrGroup) and
|
||||
Extensions::barrierGuardModel(namespaceOrGroup, type, subtypes, name, signature, ext, input,
|
||||
acceptingvalue, kind, provenance, madId) and
|
||||
acceptingValue, kind, provenance, madId) and
|
||||
model = "MaD:" + madId.toString()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -168,7 +168,7 @@ module SourceSinkInterpretationInput implements
|
||||
}
|
||||
|
||||
predicate barrierGuardElement(
|
||||
Element n, string input, Public::AcceptingValue acceptingvalue, string kind,
|
||||
Element n, string input, Public::AcceptingValue acceptingValue, string kind,
|
||||
Public::Provenance provenance, string model
|
||||
) {
|
||||
none()
|
||||
|
||||
Reference in New Issue
Block a user