diff --git a/rust/ql/lib/codeql/rust/dataflow/FlowBarrier.qll b/rust/ql/lib/codeql/rust/dataflow/FlowBarrier.qll new file mode 100644 index 000000000000..7ca64bedb5fa --- /dev/null +++ b/rust/ql/lib/codeql/rust/dataflow/FlowBarrier.qll @@ -0,0 +1,77 @@ +/** + * Provides classes and predicates for defining barriers. + * + * Flow barriers defined here feed into data flow configurations as follows: + * + * ```text + * data from *.model.yml | QL extensions of FlowBarrier::Range + * v v + * FlowBarrier (associated with a models-as-data kind string) + * v + * barrierNode predicate | other QL defined barriers, for example using concepts + * v v + * various Barrier classes for specific data flow configurations <- extending QueryBarrier + * ``` + * + * New barriers should be defined using models-as-data, QL extensions of + * `FlowBarrier::Range`, or concepts. Data flow configurations should use the + * `barrierNode` predicate and/or concepts to define their barriers. + */ + +private import rust +private import internal.FlowSummaryImpl as Impl +private import internal.DataFlowImpl as DataFlowImpl + +// import all instances below +private module Barriers { + private import codeql.rust.Frameworks + private import codeql.rust.dataflow.internal.ModelsAsData +} + +/** Provides the `Range` class used to define the extent of `FlowBarrier`. */ +module FlowBarrier { + /** A flow barrier. */ + abstract class Range extends Impl::Public::BarrierElement { + bindingset[this] + Range() { any() } + + override predicate isBarrier( + string output, string kind, Impl::Public::Provenance provenance, string model + ) { + this.isBarrier(output, kind) and provenance = "manual" and model = "" + } + + /** + * Holds if this element is a flow barrier of kind `kind`, where data + * flows out as described by `output`. + */ + predicate isBarrier(string output, string kind) { none() } + } +} + +final class FlowBarrier = FlowBarrier::Range; + +/** Provides the `Range` class used to define the extent of `FlowBarrierGuard`. */ +module FlowBarrierGuard { + /** A flow barrier guard. */ + abstract class Range extends Impl::Public::BarrierGuardElement { + bindingset[this] + Range() { any() } + + override predicate isBarrierGuard( + string input, string branch, string kind, Impl::Public::Provenance provenance, string model + ) { + this.isBarrierGuard(input, branch, kind) and provenance = "manual" and model = "" + } + + /** + * 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`. + */ + predicate isBarrierGuard(string input, string branch, string kind) { none() } + } +} + +final class FlowBarrierGuard = FlowBarrierGuard::Range; + +predicate barrierNode = DataFlowImpl::barrierNode/2; diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll index 23424dbffd92..be6750c18a35 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/DataFlowImpl.qll @@ -1157,6 +1157,62 @@ private module Cached { cached predicate sinkNode(Node n, string kind) { n.(FlowSummaryNode).isSink(kind, _) } + private newtype TKindModelPair = + TMkPair(string kind, string model) { FlowSummaryImpl::Private::barrierSpec(_, _, kind, model) } + + private boolean convertAcceptingValue(FlowSummaryImpl::Public::AcceptingValue av) { + av.isTrue() and result = true + or + av.isFalse() and result = false + // Remaining cases are not supported yet, they depend on the shared Guards library. + // or + // av.isNoException() and result.getDualValue().isThrowsException() + // or + // av.isZero() and result.asIntValue() = 0 + // or + // av.isNotZero() and result.getDualValue().asIntValue() = 0 + // or + // av.isNull() and result.isNullValue() + // or + // av.isNotNull() and result.isNonNullValue() + } + + private predicate barrierGuardChecks(Node g, Expr e, boolean gv, TKindModelPair kmp) { + exists( + FlowSummaryImpl::Public::BarrierElement n, + FlowSummaryImpl::Public::AcceptingValue acceptingvalue, string kind, string model + | + FlowSummaryImpl::Private::barrierSpec(n, acceptingvalue, kind, model) and + n.asNode().asExpr() = e and + kmp = TMkPair(kind, model) and + gv = convertAcceptingValue(acceptingvalue) + | + g.asExpr().(CallExpr).getAnArgument() = e // TODO: qualifier? + ) + } + + /** Holds if `n` is a flow barrier of kind `kind` and model `model`. */ + cached + predicate barrierNode(Node n, string kind, string model) { + exists( + FlowSummaryImpl::Public::BarrierElement b, + FlowSummaryImpl::Private::SummaryComponentStack stack + | + FlowSummaryImpl::Private::barrierSpec(b, stack, kind, model) + | + n = FlowSummaryImpl::StepsInput::getSourceNode(b, stack, false) + or + // For barriers like `Argument[0]` we want to target the pre-update node + n = + FlowSummaryImpl::StepsInput::getSourceNode(b, stack, true) + .(PostUpdateNode) + .getPreUpdateNode() + ) + or + ParameterizedBarrierGuard::getABarrierNode(TMkPair(kind, + model)) = n + } + /** * A step in a flow summary defined using `OptionalStep[name]`. An `OptionalStep` is "opt-in", which means * that by default the step is not present in the flow summary and needs to be explicitly enabled by defining @@ -1180,3 +1236,34 @@ private module Cached { } import Cached + +/** Holds if `n` is a flow barrier of kind `kind`. */ +predicate barrierNode(Node n, string kind) { barrierNode(n, kind, _) } + +bindingset[this] +private signature class ParamSig; + +private module WithParam { + /** + * Holds if the guard `g` validates the expression `e` upon evaluating to `gv`. + * + * The expression `e` is expected to be a syntactic part of the guard `g`. + * For example, the guard `g` might be a call `isSafe(x)` and the expression `e` + * the argument `x`. + */ + signature predicate guardChecksSig(AstNode g, Expr e, boolean branch, P param); +} + +/** + * Provides a set of barrier nodes for a guard that validates an expression. + * + * This is expected to be used in `isBarrier`/`isSanitizer` definitions + * in data flow and taint tracking. + */ +module ParameterizedBarrierGuard::guardChecksSig/4 guardChecks> { + /** Gets a node that is safely guarded by the given guard check. */ + Node getABarrierNode(P param) { + SsaFlow::asNode(result) = + SsaImpl::DataFlowIntegration::ParameterizedBarrierGuard::getABarrierNode(param) + } +} diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/FlowSummaryImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/FlowSummaryImpl.qll index ab0b3aff9ca9..850328146518 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/FlowSummaryImpl.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/FlowSummaryImpl.qll @@ -143,7 +143,7 @@ module Input implements InputSig { private import Make as Impl -private module StepsInput implements Impl::Private::StepsInputSig { +module StepsInput implements Impl::Private::StepsInputSig { DataFlowCall getACall(Public::SummarizedCallable sc) { result.asCall().getStaticTarget() = sc } /** Gets the argument of `source` described by `sc`, if any. */ @@ -171,18 +171,27 @@ private module StepsInput implements Impl::Private::StepsInputSig { result.asCfgScope() = source.getEnclosingCfgScope() } - RustDataFlow::Node getSourceNode(Input::SourceBase source, Impl::Private::SummaryComponentStack s) { + additional RustDataFlow::Node getSourceNode( + Input::SourceBase source, Impl::Private::SummaryComponentStack s, boolean isArgPostUpdate + ) { s.head() = Impl::Private::SummaryComponent::return(_) and - result.asExpr() = source.getCall() + result.asExpr() = source.getCall() and + isArgPostUpdate = false or exists(RustDataFlow::ArgumentPosition pos, Expr arg | s.head() = Impl::Private::SummaryComponent::parameter(pos) and arg = getSourceNodeArgument(source, s.tail().headOfSingleton()) and - result.asParameter() = getCallable(arg).getParam(pos.getPosition()) + result.asParameter() = getCallable(arg).getParam(pos.getPosition()) and + isArgPostUpdate = false ) or result.(RustDataFlow::PostUpdateNode).getPreUpdateNode().asExpr() = - getSourceNodeArgument(source, s.headOfSingleton()) + getSourceNodeArgument(source, s.headOfSingleton()) and + isArgPostUpdate = true + } + + RustDataFlow::Node getSourceNode(Input::SourceBase source, Impl::Private::SummaryComponentStack s) { + result = getSourceNode(source, s, _) } RustDataFlow::Node getSinkNode(Input::SinkBase sink, Impl::Private::SummaryComponent sc) { diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/ModelsAsData.qll b/rust/ql/lib/codeql/rust/dataflow/internal/ModelsAsData.qll index 8b55de8d54dc..a3f3da9364de 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/ModelsAsData.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/ModelsAsData.qll @@ -44,6 +44,7 @@ */ private import rust +private import codeql.rust.dataflow.FlowBarrier private import codeql.rust.dataflow.FlowSummary private import codeql.rust.dataflow.FlowSource private import codeql.rust.dataflow.FlowSink @@ -98,6 +99,29 @@ extensible predicate neutralModel( string path, string kind, string provenance, QlBuiltins::ExtensionId madId ); +/** + * Holds if in a call to the function with canonical path `path`, the value referred + * to by `output` is a barrier of the given `kind` and `madId` is the data + * extension row number. + */ +extensible predicate barrierModel( + string path, string output, string kind, string provenance, QlBuiltins::ExtensionId madId +); + +/** + * Holds if in a call to the function with canonical path `path`, the value referred + * to by `input` is a barrier guard of the given `kind` and `madId` is the data + * extension row number. + * the value referred to by `input` 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. + */ +extensible predicate barrierGuardModel( + string path, string input, string branch, string kind, string provenance, + QlBuiltins::ExtensionId madId +); + /** * Holds if the given extension tuple `madId` should pretty-print as `model`. * @@ -123,6 +147,16 @@ predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { neutralModel(path, kind, _, madId) and model = "Neutral: " + path + "; " + kind ) + or + exists(string path, string output, string kind | + barrierModel(path, output, kind, _, madId) and + 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 + ) } private class SummarizedCallableFromModel extends SummarizedCallable::Range { @@ -206,6 +240,40 @@ private class FlowSinkFromModel extends FlowSink::Range { } } +private class FlowBarrierFromModel extends FlowBarrier::Range { + private string path; + + FlowBarrierFromModel() { + barrierModel(path, _, _, _, _) and + this.callResolvesTo(path) + } + + override predicate isBarrier(string output, string kind, Provenance provenance, string model) { + exists(QlBuiltins::ExtensionId madId | + barrierModel(path, output, kind, provenance, madId) and + model = "MaD:" + madId.toString() + ) + } +} + +private class FlowBarrierGuardFromModel extends FlowBarrierGuard::Range { + private string path; + + FlowBarrierGuardFromModel() { + barrierGuardModel(path, _, _, _, _, _) and + this.callResolvesTo(path) + } + + override predicate isBarrierGuard( + string input, string branch, string kind, Provenance provenance, string model + ) { + exists(QlBuiltins::ExtensionId madId | + barrierGuardModel(path, input, branch, kind, provenance, madId) and + model = "MaD:" + madId.toString() + ) + } +} + private module Debug { private import FlowSummaryImpl private import Private diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/Node.qll b/rust/ql/lib/codeql/rust/dataflow/internal/Node.qll index 1fa3983f8112..1ccb7db73f52 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/Node.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/Node.qll @@ -82,12 +82,12 @@ class FlowSummaryNode extends Node, TFlowSummaryNode { result = this.getSummaryNode().getSinkElement() } - /** Holds is this node is a source node of kind `kind`. */ + /** Holds if this node is a source node of kind `kind`. */ predicate isSource(string kind, string model) { this.getSummaryNode().(FlowSummaryImpl::Private::SourceOutputNode).isEntry(kind, model) } - /** Holds is this node is a sink node of kind `kind`. */ + /** Holds if this node is a sink node of kind `kind`. */ predicate isSink(string kind, string model) { this.getSummaryNode().(FlowSummaryImpl::Private::SinkInputNode).isExit(kind, model) } diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll index 03db7c35b4d4..874126f6a08c 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll @@ -305,6 +305,31 @@ private module Cached { predicate getABarrierNode = getABarrierNodeImpl/0; } + + bindingset[this] + private signature class ParamSig; + + private module WithParam { + signature predicate guardChecksSig(AstNode g, Expr e, boolean branch, P param); + } + + overlay[global] + cached // nothing is actually cached + module ParameterizedBarrierGuard::guardChecksSig/4 guardChecks> { + private predicate guardChecksAdjTypes( + DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, + DataFlowIntegrationInput::GuardValue branch, P param + ) { + guardChecks(g, e, branch, param) + } + + private Node getABarrierNodeImpl(P param) { + result = + DataFlowIntegrationImpl::BarrierGuardWithState::getABarrierNode(param) + } + + predicate getABarrierNode = getABarrierNodeImpl/1; + } } } diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/empty.model.yml b/rust/ql/lib/codeql/rust/dataflow/internal/empty.model.yml index 1a33951dfc38..61c0327171a7 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/empty.model.yml +++ b/rust/ql/lib/codeql/rust/dataflow/internal/empty.model.yml @@ -15,3 +15,13 @@ extensions: pack: codeql/rust-all extensible: summaryModel data: [] + + - addsTo: + pack: codeql/rust-all + extensible: barrierModel + data: [] + + - addsTo: + pack: codeql/rust-all + extensible: barrierGuardModel + data: [] diff --git a/rust/ql/test/library-tests/dataflow/barrier/inline-flow.expected b/rust/ql/test/library-tests/dataflow/barrier/inline-flow.expected index 68da00c4312f..b1e32f95fb90 100644 --- a/rust/ql/test/library-tests/dataflow/barrier/inline-flow.expected +++ b/rust/ql/test/library-tests/dataflow/barrier/inline-flow.expected @@ -1,41 +1,26 @@ models edges -| main.rs:9:13:9:19 | ...: ... | main.rs:10:11:10:11 | s | provenance | | -| main.rs:10:11:10:11 | s | main.rs:12:9:12:9 | s | provenance | | -| main.rs:12:9:12:9 | s | main.rs:9:30:14:1 | { ... } | provenance | | | main.rs:21:9:21:9 | s | main.rs:22:10:22:10 | s | provenance | | | main.rs:21:13:21:21 | source(...) | main.rs:21:9:21:9 | s | provenance | | -| main.rs:26:9:26:9 | s | main.rs:27:22:27:22 | s | provenance | | -| main.rs:26:13:26:21 | source(...) | main.rs:26:9:26:9 | s | provenance | | -| main.rs:27:9:27:9 | s | main.rs:28:10:28:10 | s | provenance | | -| main.rs:27:13:27:23 | sanitize(...) | main.rs:27:9:27:9 | s | provenance | | -| main.rs:27:22:27:22 | s | main.rs:9:13:9:19 | ...: ... | provenance | | -| main.rs:27:22:27:22 | s | main.rs:27:13:27:23 | sanitize(...) | provenance | | | main.rs:32:9:32:9 | s | main.rs:33:10:33:10 | s | provenance | | | main.rs:32:13:32:21 | source(...) | main.rs:32:9:32:9 | s | provenance | | +| main.rs:44:9:44:9 | s | main.rs:46:14:46:14 | s | provenance | | +| main.rs:44:13:44:21 | source(...) | main.rs:44:9:44:9 | s | provenance | | nodes -| main.rs:9:13:9:19 | ...: ... | semmle.label | ...: ... | -| main.rs:9:30:14:1 | { ... } | semmle.label | { ... } | -| main.rs:10:11:10:11 | s | semmle.label | s | -| main.rs:12:9:12:9 | s | semmle.label | s | | main.rs:17:10:17:18 | source(...) | semmle.label | source(...) | | main.rs:21:9:21:9 | s | semmle.label | s | | main.rs:21:13:21:21 | source(...) | semmle.label | source(...) | | main.rs:22:10:22:10 | s | semmle.label | s | -| main.rs:26:9:26:9 | s | semmle.label | s | -| main.rs:26:13:26:21 | source(...) | semmle.label | source(...) | -| main.rs:27:9:27:9 | s | semmle.label | s | -| main.rs:27:13:27:23 | sanitize(...) | semmle.label | sanitize(...) | -| main.rs:27:22:27:22 | s | semmle.label | s | -| main.rs:28:10:28:10 | s | semmle.label | s | | main.rs:32:9:32:9 | s | semmle.label | s | | main.rs:32:13:32:21 | source(...) | semmle.label | source(...) | | main.rs:33:10:33:10 | s | semmle.label | s | +| main.rs:44:9:44:9 | s | semmle.label | s | +| main.rs:44:13:44:21 | source(...) | semmle.label | source(...) | +| main.rs:46:14:46:14 | s | semmle.label | s | subpaths -| main.rs:27:22:27:22 | s | main.rs:9:13:9:19 | ...: ... | main.rs:9:30:14:1 | { ... } | main.rs:27:13:27:23 | sanitize(...) | testFailures #select | main.rs:17:10:17:18 | source(...) | main.rs:17:10:17:18 | source(...) | main.rs:17:10:17:18 | source(...) | $@ | main.rs:17:10:17:18 | source(...) | source(...) | | main.rs:22:10:22:10 | s | main.rs:21:13:21:21 | source(...) | main.rs:22:10:22:10 | s | $@ | main.rs:21:13:21:21 | source(...) | source(...) | -| main.rs:28:10:28:10 | s | main.rs:26:13:26:21 | source(...) | main.rs:28:10:28:10 | s | $@ | main.rs:26:13:26:21 | source(...) | source(...) | | main.rs:33:10:33:10 | s | main.rs:32:13:32:21 | source(...) | main.rs:33:10:33:10 | s | $@ | main.rs:32:13:32:21 | source(...) | source(...) | +| main.rs:46:14:46:14 | s | main.rs:44:13:44:21 | source(...) | main.rs:46:14:46:14 | s | $@ | main.rs:44:13:44:21 | source(...) | source(...) | diff --git a/rust/ql/test/library-tests/dataflow/barrier/inline-flow.ext.yml b/rust/ql/test/library-tests/dataflow/barrier/inline-flow.ext.yml new file mode 100644 index 000000000000..58e55a040d21 --- /dev/null +++ b/rust/ql/test/library-tests/dataflow/barrier/inline-flow.ext.yml @@ -0,0 +1,11 @@ +extensions: + - addsTo: + pack: codeql/rust-all + extensible: barrierModel + data: + - ["main::sanitize", "ReturnValue", "test-barrier", "manual"] + - addsTo: + pack: codeql/rust-all + extensible: barrierGuardModel + data: + - ["main::verify_safe", "Argument[0]", "true", "test-barrier", "manual"] diff --git a/rust/ql/test/library-tests/dataflow/barrier/inline-flow.ql b/rust/ql/test/library-tests/dataflow/barrier/inline-flow.ql index 5dcb7ee70a9d..7cc30bf63508 100644 --- a/rust/ql/test/library-tests/dataflow/barrier/inline-flow.ql +++ b/rust/ql/test/library-tests/dataflow/barrier/inline-flow.ql @@ -3,8 +3,19 @@ */ import rust +import codeql.rust.dataflow.DataFlow +import codeql.rust.dataflow.FlowBarrier import utils.test.InlineFlowTest -import DefaultFlowTest + +module CustomConfig implements DataFlow::ConfigSig { + predicate isSource = DefaultFlowConfig::isSource/1; + + predicate isSink = DefaultFlowConfig::isSink/1; + + predicate isBarrier(DataFlow::Node n) { barrierNode(n, "test-barrier") } +} + +import FlowTest import TaintFlow::PathGraph from TaintFlow::PathNode source, TaintFlow::PathNode sink diff --git a/rust/ql/test/library-tests/dataflow/barrier/main.rs b/rust/ql/test/library-tests/dataflow/barrier/main.rs index 14935f0f3286..268a8673bc9b 100644 --- a/rust/ql/test/library-tests/dataflow/barrier/main.rs +++ b/rust/ql/test/library-tests/dataflow/barrier/main.rs @@ -25,10 +25,24 @@ fn through_variable() { fn with_barrier() { let s = source(1); let s = sanitize(s); - sink(s); // $ SPURIOUS: hasValueFlow=1 + sink(s); } fn main() { let s = source(1); sink(s); // $ hasValueFlow=1 } + +fn verify_safe(s: &str) -> bool { + match s { + "dangerous" => false, + _ => true, + } +} + +fn with_barrier_guard() { + let s = source(1); + if verify_safe(s) { + sink(s); + } +} diff --git a/shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll b/shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll index d76672571921..75c6ab9ce3d9 100644 --- a/shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll @@ -368,6 +368,34 @@ module Make< abstract predicate isSink(string input, string kind, Provenance provenance, string model); } + /** A barrier element. */ + abstract class BarrierElement extends SourceBaseFinal { + bindingset[this] + BarrierElement() { any() } + + /** + * Holds if this element is a flow barrier of kind `kind`, where data + * flows out as described by `output`. + */ + pragma[nomagic] + abstract predicate isBarrier(string output, string kind, Provenance provenance, string model); + } + + /** A barrier guard element. */ + abstract class BarrierGuardElement extends SinkBaseFinal { + bindingset[this] + BarrierGuardElement() { any() } + + /** + * 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`. + */ + pragma[nomagic] + abstract predicate isBarrierGuard( + string input, string branch, string kind, Provenance provenance, string model + ); + } + private signature predicate hasKindSig(string kind); signature class NeutralCallableSig extends SummarizedCallableBaseFinal { @@ -723,7 +751,32 @@ module Make< ) } - private predicate summarySpec(string spec) { + private predicate isRelevantBarrier( + BarrierElement e, string output, string kind, Provenance provenance, string model + ) { + e.isBarrier(output, kind, provenance, model) and + ( + provenance.isManual() + or + provenance.isGenerated() and + not exists(Provenance p | p.isManual() and e.isBarrier(_, kind, p, _)) + ) + } + + private predicate isRelevantBarrierGuard( + BarrierGuardElement e, string input, string branch, string kind, Provenance provenance, + string model + ) { + e.isBarrierGuard(input, branch, kind, provenance, model) and + ( + provenance.isManual() + or + provenance.isGenerated() and + not exists(Provenance p | p.isManual() and e.isBarrierGuard(_, _, kind, p, _)) + ) + } + + private predicate flowSpec(string spec) { exists(SummarizedCallable c | c.propagatesFlow(spec, _, _, _, _, _) or @@ -732,10 +785,14 @@ module Make< or isRelevantSource(_, spec, _, _, _) or + isRelevantBarrier(_, spec, _, _, _) + or + isRelevantBarrierGuard(_, spec, _, _, _, _) + or isRelevantSink(_, spec, _, _, _) } - import AccessPathSyntax::AccessPath + import AccessPathSyntax::AccessPath /** Holds if specification component `token` parses as parameter `pos`. */ predicate parseParam(AccessPathToken token, ArgumentPosition pos) { @@ -1515,6 +1572,31 @@ module Make< ) } + /** + * Holds if `barrier` is a relevant barrier element with output specification `outSpec`. + */ + predicate barrierSpec( + BarrierElement barrier, SummaryComponentStack outSpec, string kind, string model + ) { + exists(string output | + isRelevantBarrier(barrier, output, kind, _, model) and + External::interpretSpec(output, outSpec) + ) + } + + /** + * Holds if `barrierGuard` is a relevant barrier guard element with input specification `inSpec`. + */ + predicate barrierSpec( + BarrierGuardElement barrierGuard, SummaryComponentStack inSpec, string branch, string kind, + string model + ) { + exists(string input | + isRelevantBarrierGuard(barrierGuard, input, branch, kind, _, model) and + External::interpretSpec(input, inSpec) + ) + } + signature module TypesInputSig { /** Gets the type of content `c`. */ DataFlowType getContentType(ContentSet c);