diff --git a/cpp/ql/lib/ext/empty.model.yml b/cpp/ql/lib/ext/empty.model.yml index 6f160b62d7a6..e5202b5ad73c 100644 --- a/cpp/ql/lib/ext/empty.model.yml +++ b/cpp/ql/lib/ext/empty.model.yml @@ -9,6 +9,14 @@ extensions: pack: codeql/cpp-all extensible: sinkModel data: [] + - addsTo: + pack: codeql/cpp-all + extensible: barrierModel + data: [] + - addsTo: + pack: codeql/cpp-all + extensible: barrierGuardModel + data: [] - addsTo: pack: codeql/cpp-all extensible: summaryModel diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/ExternalFlow.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/ExternalFlow.qll index 69e32d23ec1c..7232326f1b3d 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/ExternalFlow.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/ExternalFlow.qll @@ -101,9 +101,10 @@ private import internal.FlowSummaryImpl private import internal.FlowSummaryImpl::Public private import internal.FlowSummaryImpl::Private private import internal.FlowSummaryImpl::Private::External -private import internal.ExternalFlowExtensions as Extensions +private import internal.ExternalFlowExtensions::Extensions as Extensions private import codeql.mad.ModelValidation as SharedModelVal private import codeql.util.Unit +private import codeql.mad.static.ModelsAsData as SharedMaD /** * A unit class for adding additional source model rows. @@ -144,135 +145,82 @@ predicate sinkModel(string row) { any(SinkModelCsv s).row(row) } /** Holds if `row` is a summary model. */ predicate summaryModel(string row) { any(SummaryModelCsv s).row(row) } -/** Holds if a source model exists for the given parameters. */ -predicate sourceModel( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - string output, string kind, string provenance, string model -) { - exists(string row | - sourceModel(row) and - row.splitAt(";", 0) = namespace and - row.splitAt(";", 1) = type and - row.splitAt(";", 2) = subtypes.toString() and - subtypes = [true, false] and - row.splitAt(";", 3) = name and - row.splitAt(";", 4) = signature and - row.splitAt(";", 5) = ext and - row.splitAt(";", 6) = output and - row.splitAt(";", 7) = kind - ) and - provenance = "manual" and - model = "" - or - exists(QlBuiltins::ExtensionId madId | - Extensions::sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, - provenance, madId) and - model = "MaD:" + madId.toString() - ) -} - -/** Holds if a sink model exists for the given parameters. */ -predicate sinkModel( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - string input, string kind, string provenance, string model -) { - exists(string row | - sinkModel(row) and - row.splitAt(";", 0) = namespace and - row.splitAt(";", 1) = type and - row.splitAt(";", 2) = subtypes.toString() and - subtypes = [true, false] and - row.splitAt(";", 3) = name and - row.splitAt(";", 4) = signature and - row.splitAt(";", 5) = ext and - row.splitAt(";", 6) = input and - row.splitAt(";", 7) = kind - ) and - provenance = "manual" and - model = "" - or - exists(QlBuiltins::ExtensionId madId | - Extensions::sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, provenance, - madId) and - model = "MaD:" + madId.toString() - ) -} - -/** - * Holds if a summary model exists for the given parameters. - * - * This predicate does not expand `@` to `*`s. - */ -private predicate summaryModel0( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - string input, string output, string kind, string provenance, string model -) { - exists(string row | - summaryModel(row) and - row.splitAt(";", 0) = namespace and - row.splitAt(";", 1) = type and - row.splitAt(";", 2) = subtypes.toString() and - subtypes = [true, false] and - row.splitAt(";", 3) = name and - row.splitAt(";", 4) = signature and - row.splitAt(";", 5) = ext and - row.splitAt(";", 6) = input and - row.splitAt(";", 7) = output and - row.splitAt(";", 8) = kind - ) and - provenance = "manual" and - model = "" - or - exists(QlBuiltins::ExtensionId madId | - Extensions::summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, - provenance, madId) and - model = "MaD:" + madId.toString() - ) -} - -/** - * Holds if the given extension tuple `madId` should pretty-print as `model`. - * - * This predicate should only be used in tests. - */ -predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { - exists( +private module MadInput implements SharedMaD::InputSig { + /** Holds if a source model exists for the given parameters. */ + predicate additionalSourceModel( string namespace, string type, boolean subtypes, string name, string signature, string ext, - string output, string kind, string provenance - | - Extensions::sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, - provenance, madId) - | - model = - "Source: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " - + ext + "; " + output + "; " + kind + "; " + provenance - ) - or - exists( + string output, string kind, string provenance, string model + ) { + exists(string row | + sourceModel(row) and + row.splitAt(";", 0) = namespace and + row.splitAt(";", 1) = type and + row.splitAt(";", 2) = subtypes.toString() and + subtypes = [true, false] and + row.splitAt(";", 3) = name and + row.splitAt(";", 4) = signature and + row.splitAt(";", 5) = ext and + row.splitAt(";", 6) = output and + row.splitAt(";", 7) = kind + ) and + provenance = "manual" and + model = "" + } + + /** Holds if a sink model exists for the given parameters. */ + predicate additionalSinkModel( string namespace, string type, boolean subtypes, string name, string signature, string ext, - string input, string kind, string provenance - | - Extensions::sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, provenance, - madId) - | - model = - "Sink: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " + - ext + "; " + input + "; " + kind + "; " + provenance - ) - or - exists( + string input, string kind, string provenance, string model + ) { + exists(string row | + sinkModel(row) and + row.splitAt(";", 0) = namespace and + row.splitAt(";", 1) = type and + row.splitAt(";", 2) = subtypes.toString() and + subtypes = [true, false] and + row.splitAt(";", 3) = name and + row.splitAt(";", 4) = signature and + row.splitAt(";", 5) = ext and + row.splitAt(";", 6) = input and + row.splitAt(";", 7) = kind + ) and + provenance = "manual" and + model = "" + } + + /** + * Holds if a summary model exists for the given parameters. + * + * This predicate does not expand `@` to `*`s. + */ + predicate additionalSummaryModel( string namespace, string type, boolean subtypes, string name, string signature, string ext, - string input, string output, string kind, string provenance - | - Extensions::summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, - provenance, madId) - | - model = - "Summary: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + - "; " + ext + "; " + input + "; " + output + "; " + kind + "; " + provenance - ) + string input, string output, string kind, string provenance, string model + ) { + exists(string row | + summaryModel(row) and + row.splitAt(";", 0) = namespace and + row.splitAt(";", 1) = type and + row.splitAt(";", 2) = subtypes.toString() and + subtypes = [true, false] and + row.splitAt(";", 3) = name and + row.splitAt(";", 4) = signature and + row.splitAt(";", 5) = ext and + row.splitAt(";", 6) = input and + row.splitAt(";", 7) = output and + row.splitAt(";", 8) = kind + ) and + provenance = "manual" and + model = "" + } + + string namespaceSegmentSeparator() { result = "::" } } +private module MaD = SharedMaD::ModelsAsData; + +import MaD + /** * Holds if `input` is `input0`, but with all occurrences of `@` replaced * by `n` repetitions of `*` (and similarly for `output` and `output0`). @@ -294,69 +242,13 @@ predicate summaryModel( string input, string output, string kind, string provenance, string model ) { exists(string input0, string output0 | - summaryModel0(namespace, type, subtypes, name, signature, ext, input0, output0, kind, + MaD::summaryModel(namespace, type, subtypes, name, signature, ext, input0, output0, kind, provenance, model) and expandInputAndOutput(input0, input, output0, output, [0 .. Private::getMaxElementContentIndirectionIndex() - 1]) ) } -private predicate relevantNamespace(string namespace) { - sourceModel(namespace, _, _, _, _, _, _, _, _, _) or - sinkModel(namespace, _, _, _, _, _, _, _, _, _) or - summaryModel(namespace, _, _, _, _, _, _, _, _, _, _) -} - -private predicate namespaceLink(string shortns, string longns) { - relevantNamespace(shortns) and - relevantNamespace(longns) and - longns.prefix(longns.indexOf("::")) = shortns -} - -private predicate canonicalNamespace(string namespace) { - relevantNamespace(namespace) and not namespaceLink(_, namespace) -} - -private predicate canonicalNamespaceLink(string namespace, string subns) { - canonicalNamespace(namespace) and - (subns = namespace or namespaceLink(namespace, subns)) -} - -/** - * Holds if MaD framework coverage of `namespace` is `n` api endpoints of the - * kind `(kind, part)`, and `namespaces` is the number of subnamespaces of - * `namespace` which have MaD framework coverage (including `namespace` - * itself). - */ -predicate modelCoverage(string namespace, int namespaces, string kind, string part, int n) { - namespaces = strictcount(string subns | canonicalNamespaceLink(namespace, subns)) and - ( - part = "source" and - n = - strictcount(string subns, string type, boolean subtypes, string name, string signature, - string ext, string output, string provenance, string model | - canonicalNamespaceLink(namespace, subns) and - sourceModel(subns, type, subtypes, name, signature, ext, output, kind, provenance, model) - ) - or - part = "sink" and - n = - strictcount(string subns, string type, boolean subtypes, string name, string signature, - string ext, string input, string provenance, string model | - canonicalNamespaceLink(namespace, subns) and - sinkModel(subns, type, subtypes, name, signature, ext, input, kind, provenance, model) - ) - or - part = "summary" and - n = - strictcount(string subns, string type, boolean subtypes, string name, string signature, - string ext, string input, string output, string provenance | - canonicalNamespaceLink(namespace, subns) and - summaryModel(subns, type, subtypes, name, signature, ext, input, output, kind, provenance, _) - ) - ) -} - /** Provides a query predicate to check the CSV data for validation errors. */ module CsvValidation { private string getInvalidModelInput() { diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/ExternalFlowExtensions.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/ExternalFlowExtensions.qll index cd1af34c8d8a..1a572c221d9f 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/ExternalFlowExtensions.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/ExternalFlowExtensions.qll @@ -2,6 +2,8 @@ * This module provides extensible predicates for defining MaD models. */ +private import codeql.mad.static.ModelsAsData as SharedMaD + /** * Holds if an external source model exists for the given parameters. */ @@ -18,6 +20,22 @@ extensible predicate sinkModel( string input, string kind, string provenance, QlBuiltins::ExtensionId madId ); +/** + * Holds if a barrier model exists for the given parameters. + */ +extensible predicate barrierModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, QlBuiltins::ExtensionId madId +); + +/** + * Holds if a barrier guard model exists for the given parameters. + */ +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 +); + /** * Holds if an external summary model exists for the given parameters. */ @@ -25,3 +43,16 @@ extensible predicate summaryModel( string namespace, string type, boolean subtypes, string name, string signature, string ext, string input, string output, string kind, string provenance, QlBuiltins::ExtensionId madId ); + +/** + * Holds if a neutral model exists for the given parameters. + */ +extensible predicate neutralModel( + string namespace, string type, string name, string signature, string kind, string provenance +); + +module Extensions implements SharedMaD::ExtensionsSig { + import ExternalFlowExtensions + + predicate namespaceGrouping(string group, string namespace) { none() } +} diff --git a/csharp/ql/lib/ext/empty.model.yml b/csharp/ql/lib/ext/empty.model.yml index 6b38b783cbe2..09d848ea57d5 100644 --- a/csharp/ql/lib/ext/empty.model.yml +++ b/csharp/ql/lib/ext/empty.model.yml @@ -11,6 +11,16 @@ extensions: extensible: sinkModel data: [] + - addsTo: + pack: codeql/csharp-all + extensible: barrierModel + data: [] + + - addsTo: + pack: codeql/csharp-all + extensible: barrierGuardModel + data: [] + - addsTo: pack: codeql/csharp-all extensible: summaryModel diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/ExternalFlow.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/ExternalFlow.qll index 87b28b76e99a..75d14034e000 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/ExternalFlow.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/ExternalFlow.qll @@ -88,7 +88,7 @@ */ import csharp -import ExternalFlowExtensions +private import ExternalFlowExtensions::Extensions as Extensions private import DataFlowDispatch private import DataFlowPrivate private import DataFlowPublic @@ -101,100 +101,13 @@ private import semmle.code.csharp.dispatch.OverridableCallable private import semmle.code.csharp.frameworks.System private import codeql.dataflow.internal.AccessPathSyntax as AccessPathSyntax private import codeql.mad.ModelValidation as SharedModelVal +private import codeql.mad.static.ModelsAsData as SharedMaD -/** - * Holds if the given extension tuple `madId` should pretty-print as `model`. - * - * This predicate should only be used in tests. - */ -predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { - exists( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - string output, string kind, string provenance - | - sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, provenance, madId) and - model = - "Source: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " - + ext + "; " + output + "; " + kind + "; " + provenance - ) - or - exists( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - string input, string kind, string provenance - | - sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, provenance, madId) and - model = - "Sink: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " + - ext + "; " + input + "; " + kind + "; " + provenance - ) - or - exists( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - string input, string output, string kind, string provenance - | - summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, provenance, - madId) and - model = - "Summary: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + - "; " + ext + "; " + input + "; " + output + "; " + kind + "; " + provenance - ) -} +private module MadInput implements SharedMaD::InputSig { } -private predicate relevantNamespace(string namespace) { - sourceModel(namespace, _, _, _, _, _, _, _, _, _) or - sinkModel(namespace, _, _, _, _, _, _, _, _, _) or - summaryModel(namespace, _, _, _, _, _, _, _, _, _, _) -} +private module MaD = SharedMaD::ModelsAsData; -private predicate namespaceLink(string shortns, string longns) { - relevantNamespace(shortns) and - relevantNamespace(longns) and - longns.prefix(longns.indexOf(".")) = shortns -} - -private predicate canonicalNamespace(string namespace) { - relevantNamespace(namespace) and not namespaceLink(_, namespace) -} - -private predicate canonicalNamespaceLink(string namespace, string subns) { - canonicalNamespace(namespace) and - (subns = namespace or namespaceLink(namespace, subns)) -} - -/** - * Holds if MaD framework coverage of `namespace` is `n` api endpoints of the - * kind `(kind, part)`, and `namespaces` is the number of subnamespaces of - * `namespace` which have MaD framework coverage (including `namespace` - * itself). - */ -predicate modelCoverage(string namespace, int namespaces, string kind, string part, int n) { - namespaces = strictcount(string subns | canonicalNamespaceLink(namespace, subns)) and - ( - part = "source" and - n = - strictcount(string subns, string type, boolean subtypes, string name, string signature, - string ext, string output, string provenance | - canonicalNamespaceLink(namespace, subns) and - sourceModel(subns, type, subtypes, name, signature, ext, output, kind, provenance, _) - ) - or - part = "sink" and - n = - strictcount(string subns, string type, boolean subtypes, string name, string signature, - string ext, string input, string provenance | - canonicalNamespaceLink(namespace, subns) and - sinkModel(subns, type, subtypes, name, signature, ext, input, kind, provenance, _) - ) - or - part = "summary" and - n = - strictcount(string subns, string type, boolean subtypes, string name, string signature, - string ext, string input, string output, string provenance | - canonicalNamespaceLink(namespace, subns) and - summaryModel(subns, type, subtypes, name, signature, ext, input, output, kind, provenance, _) - ) - ) -} +import MaD /** Provides a query predicate to check the MaD models for validation errors. */ module ModelValidation { @@ -258,7 +171,7 @@ module ModelValidation { predicate sourceKind(string kind) { sourceModel(_, _, _, _, _, _, _, kind, _, _) } - predicate neutralKind(string kind) { neutralModel(_, _, _, _, kind, _) } + predicate neutralKind(string kind) { Extensions::neutralModel(_, _, _, _, kind, _) } } private module KindVal = SharedModelVal::KindValidation; @@ -275,7 +188,7 @@ module ModelValidation { summaryModel(namespace, type, _, name, signature, ext, _, _, _, provenance, _) and pred = "summary" or - neutralModel(namespace, type, name, signature, _, provenance) and + Extensions::neutralModel(namespace, type, name, signature, _, provenance) and ext = "" and pred = "neutral" | @@ -318,7 +231,7 @@ private predicate elementSpec( or summaryModel(namespace, type, subtypes, name, signature, ext, _, _, _, _, _) or - neutralModel(namespace, type, name, signature, _, _) and ext = "" and subtypes = true + Extensions::neutralModel(namespace, type, name, signature, _, _) and ext = "" and subtypes = true } private predicate elementSpec( @@ -590,19 +503,17 @@ private predicate interpretSummary( UnboundCallable c, string input, string output, string kind, string provenance, string model ) { exists( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - QlBuiltins::ExtensionId madId + string namespace, string type, boolean subtypes, string name, string signature, string ext | summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, provenance, - madId) and - model = "MaD:" + madId.toString() and + model) and c = interpretElement(namespace, type, subtypes, name, signature, ext) ) } predicate interpretNeutral(UnboundCallable c, string kind, string provenance) { exists(string namespace, string type, string name, string signature | - neutralModel(namespace, type, name, signature, kind, provenance) and + Extensions::neutralModel(namespace, type, name, signature, kind, provenance) and c = interpretElement(namespace, type, true, name, signature, "") ) } diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/ExternalFlowExtensions.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/ExternalFlowExtensions.qll index f761a0a9f5cd..3461f0a51863 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/ExternalFlowExtensions.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/ExternalFlowExtensions.qll @@ -2,6 +2,8 @@ * This module provides extensible predicates for defining MaD models. */ +private import codeql.mad.static.ModelsAsData as SharedMaD + /** * Holds if a source model exists for the given parameters. */ @@ -18,6 +20,22 @@ extensible predicate sinkModel( string input, string kind, string provenance, QlBuiltins::ExtensionId madId ); +/** + * Holds if a barrier model exists for the given parameters. + */ +extensible predicate barrierModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, QlBuiltins::ExtensionId madId +); + +/** + * Holds if a barrier guard model exists for the given parameters. + */ +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 +); + /** * Holds if a summary model exists for the given parameters. */ @@ -32,3 +50,9 @@ extensible predicate summaryModel( extensible predicate neutralModel( string namespace, string type, string name, string signature, string kind, string provenance ); + +module Extensions implements SharedMaD::ExtensionsSig { + import ExternalFlowExtensions + + predicate namespaceGrouping(string group, string namespace) { none() } +} diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll index 842c28ac75b0..56278b9ef950 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll @@ -213,11 +213,9 @@ module SourceSinkInterpretationInput implements Element e, string output, string kind, Public::Provenance provenance, string model ) { exists( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - QlBuiltins::ExtensionId madId + string namespace, string type, boolean subtypes, string name, string signature, string ext | - sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, provenance, madId) and - model = "MaD:" + madId.toString() and + sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, provenance, model) and e = interpretElement(namespace, type, subtypes, name, signature, ext) ) } @@ -226,11 +224,9 @@ module SourceSinkInterpretationInput implements Element e, string input, string kind, Public::Provenance provenance, string model ) { exists( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - QlBuiltins::ExtensionId madId + string namespace, string type, boolean subtypes, string name, string signature, string ext | - sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, provenance, madId) and - model = "MaD:" + madId.toString() and + sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, provenance, model) and e = interpretElement(namespace, type, subtypes, name, signature, ext) ) } diff --git a/go/ql/lib/ext/empty.model.yml b/go/ql/lib/ext/empty.model.yml index 8d661a9f1db6..1709a6098eb5 100644 --- a/go/ql/lib/ext/empty.model.yml +++ b/go/ql/lib/ext/empty.model.yml @@ -9,6 +9,14 @@ extensions: pack: codeql/go-all extensible: sinkModel data: [] + - addsTo: + pack: codeql/go-all + extensible: barrierModel + data: [] + - addsTo: + pack: codeql/go-all + extensible: barrierGuardModel + data: [] - addsTo: pack: codeql/go-all extensible: summaryModel diff --git a/go/ql/lib/semmle/go/dataflow/ExternalFlow.qll b/go/ql/lib/semmle/go/dataflow/ExternalFlow.qll index 3228f4248859..de1e3da62813 100644 --- a/go/ql/lib/semmle/go/dataflow/ExternalFlow.qll +++ b/go/ql/lib/semmle/go/dataflow/ExternalFlow.qll @@ -86,7 +86,7 @@ */ private import go -import internal.ExternalFlowExtensions as FlowExtensions +private import internal.ExternalFlowExtensions::Extensions as Extensions private import FlowSummary as FlowSummary private import internal.DataFlowPrivate private import internal.FlowSummaryImpl @@ -94,201 +94,32 @@ private import internal.FlowSummaryImpl::Public as Public private import internal.FlowSummaryImpl::Private private import internal.FlowSummaryImpl::Private::External private import codeql.mad.ModelValidation as SharedModelVal +private import codeql.mad.static.ModelsAsData as SharedMaD -/** Gets the prefix for a group of packages. */ -private string groupPrefix() { result = "group:" } - -/** - * Gets a package represented by `packageOrGroup`. - * - * If `packageOrGroup` is of the form `group:` then `result` is a - * package in the group ``, as determined by `packageGrouping`. - * Otherwise, `result` is `packageOrGroup`. - */ -bindingset[packageOrGroup] -private string getPackage(string packageOrGroup) { - not exists(string group | packageOrGroup = groupPrefix() + group) and result = packageOrGroup - or - exists(string group | - FlowExtensions::packageGrouping(group, result) and - packageOrGroup = groupPrefix() + group - ) -} - -/** - * Holds if a source model exists for the given parameters. - * - * Note that `group:` references are expanded into one or more actual packages - * by this predicate. - */ -predicate sourceModel( - string package, string type, boolean subtypes, string name, string signature, string ext, - string output, string kind, string provenance, QlBuiltins::ExtensionId madId -) { - exists(string packageOrGroup | - package = getPackage(packageOrGroup) and - FlowExtensions::sourceModel(packageOrGroup, type, subtypes, name, signature, ext, output, kind, - provenance, madId) - ) -} - -/** - * Holds if a sink model exists for the given parameters. - * - * Note that `group:` references are expanded into one or more actual packages - * by this predicate. - */ -predicate sinkModel( - string package, string type, boolean subtypes, string name, string signature, string ext, - string input, string kind, string provenance, QlBuiltins::ExtensionId madId -) { - exists(string packageOrGroup | package = getPackage(packageOrGroup) | - FlowExtensions::sinkModel(packageOrGroup, type, subtypes, name, signature, ext, input, kind, - provenance, madId) - ) -} - -/** - * Holds if a summary model exists for the given parameters. - * - * Note that `group:` references are expanded into one or more actual packages - * by this predicate. - */ -predicate summaryModel( - string package, string type, boolean subtypes, string name, string signature, string ext, - string input, string output, string kind, string provenance, QlBuiltins::ExtensionId madId -) { - exists(string packageOrGroup | package = getPackage(packageOrGroup) | - FlowExtensions::summaryModel(packageOrGroup, type, subtypes, name, signature, ext, input, - output, kind, provenance, madId) - ) -} - -/** - * Holds if a neutral model exists for the given parameters. - * - * Note that `group:` references are expanded into one or more actual packages - * by this predicate. - */ -predicate neutralModel( - string package, string type, string name, string signature, string kind, string provenance -) { - exists(string packageOrGroup | package = getPackage(packageOrGroup) | - FlowExtensions::neutralModel(packageOrGroup, type, name, signature, kind, provenance) - ) -} - -/** - * Holds if the given extension tuple `madId` should pretty-print as `model`. - * - * This predicate should only be used in tests. - */ -predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { - exists( - string package, string type, boolean subtypes, string name, string signature, string ext, - string output, string kind, string provenance - | - FlowExtensions::sourceModel(package, type, subtypes, name, signature, ext, output, kind, - provenance, madId) and - model = - "Source: " + package + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " + - ext + "; " + output + "; " + kind + "; " + provenance - ) - or - exists( - string package, string type, boolean subtypes, string name, string signature, string ext, - string input, string kind, string provenance - | - FlowExtensions::sinkModel(package, type, subtypes, name, signature, ext, input, kind, - provenance, madId) and - model = - "Sink: " + package + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " + - ext + "; " + input + "; " + kind + "; " + provenance - ) - or - exists( - string package, string type, boolean subtypes, string name, string signature, string ext, - string input, string output, string kind, string provenance - | - FlowExtensions::summaryModel(package, type, subtypes, name, signature, ext, input, output, kind, - provenance, madId) and - model = - "Summary: " + package + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " + - ext + "; " + input + "; " + output + "; " + kind + "; " + provenance - ) -} - -bindingset[p] -private string cleanPackage(string p) { - exists(string noPrefix | - p = fixedVersionPrefix() + noPrefix - or - not p = fixedVersionPrefix() + any(string s) and - noPrefix = p - | - result = noPrefix.regexpReplaceAll(majorVersionSuffixRegex(), "") - ) -} +private module MadInput implements SharedMaD::InputSig { + string namespaceSegmentSeparator() { result = "/" } -private predicate relevantPackage(string package) { - exists(string p | package = cleanPackage(p) | - sourceModel(p, _, _, _, _, _, _, _, _, _) or - sinkModel(p, _, _, _, _, _, _, _, _, _) or - summaryModel(p, _, _, _, _, _, _, _, _, _, _) - ) + bindingset[p] + string cleanNamespace(string p) { + exists(string noPrefix | + p = fixedVersionPrefix() + noPrefix + or + not p = fixedVersionPrefix() + any(string s) and + noPrefix = p + | + result = noPrefix.regexpReplaceAll(majorVersionSuffixRegex(), "") + ) + } } -private predicate packageLink(string shortpkg, string longpkg) { - relevantPackage(shortpkg) and - relevantPackage(longpkg) and - longpkg.prefix(longpkg.indexOf("/")) = shortpkg -} +private module MaD = SharedMaD::ModelsAsData; -private predicate canonicalPackage(string package) { - relevantPackage(package) and not packageLink(_, package) -} +import MaD -private predicate canonicalPkgLink(string package, string subpkg) { - canonicalPackage(package) and - (subpkg = package or packageLink(package, subpkg)) -} +module FlowExtensions = Extensions; -/** - * Holds if MaD framework coverage of `package` is `n` api endpoints of the - * kind `(kind, part)`, and `pkgs` is the number of subpackages of `package` - * which have MaD framework coverage (including `package` itself). - */ -predicate modelCoverage(string package, int pkgs, string kind, string part, int n) { - pkgs = strictcount(string subpkg | canonicalPkgLink(package, subpkg)) and - ( - part = "source" and - n = - strictcount(string subpkg, string type, boolean subtypes, string name, string signature, - string ext, string output, string provenance, string x | - canonicalPkgLink(package, subpkg) and - subpkg = cleanPackage(x) and - sourceModel(x, type, subtypes, name, signature, ext, output, kind, provenance, _) - ) - or - part = "sink" and - n = - strictcount(string subpkg, string type, boolean subtypes, string name, string signature, - string ext, string input, string provenance, string x | - canonicalPkgLink(package, subpkg) and - subpkg = cleanPackage(x) and - sinkModel(x, type, subtypes, name, signature, ext, input, kind, provenance, _) - ) - or - part = "summary" and - n = - strictcount(string subpkg, string type, boolean subtypes, string name, string signature, - string ext, string input, string output, string provenance, string x | - canonicalPkgLink(package, subpkg) and - subpkg = cleanPackage(x) and - summaryModel(x, type, subtypes, name, signature, ext, input, output, kind, provenance, _) - ) - ) -} +/** Gets the prefix for a group of packages. */ +private string groupPrefix() { result = "group:" } /** Provides a query predicate to check the MaD models for validation errors. */ module ModelValidation { diff --git a/go/ql/lib/semmle/go/dataflow/internal/ExternalFlowExtensions.qll b/go/ql/lib/semmle/go/dataflow/internal/ExternalFlowExtensions.qll index b1e1c906028c..2e962299f3ed 100644 --- a/go/ql/lib/semmle/go/dataflow/internal/ExternalFlowExtensions.qll +++ b/go/ql/lib/semmle/go/dataflow/internal/ExternalFlowExtensions.qll @@ -2,6 +2,8 @@ * This module provides extensible predicates for defining MaD models. */ +private import codeql.mad.static.ModelsAsData as SharedMaD + /** * Holds if a source model exists for the given parameters. */ @@ -18,6 +20,22 @@ extensible predicate sinkModel( string input, string kind, string provenance, QlBuiltins::ExtensionId madId ); +/** + * Holds if a barrier model exists for the given parameters. + */ +extensible predicate barrierModel( + string package, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, QlBuiltins::ExtensionId madId +); + +/** + * Holds if a barrier guard model exists for the given parameters. + */ +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 +); + /** * Holds if a summary model exists for the given parameters. */ @@ -37,3 +55,9 @@ extensible predicate neutralModel( * Holds if the package `package` is part of the group `group`. */ extensible predicate packageGrouping(string group, string package); + +module Extensions implements SharedMaD::ExtensionsSig { + import ExternalFlowExtensions + + predicate namespaceGrouping = packageGrouping/2; +} diff --git a/go/ql/lib/semmle/go/dataflow/internal/FlowSummaryImpl.qll b/go/ql/lib/semmle/go/dataflow/internal/FlowSummaryImpl.qll index 41ded04634be..39af0cef1ad0 100644 --- a/go/ql/lib/semmle/go/dataflow/internal/FlowSummaryImpl.qll +++ b/go/ql/lib/semmle/go/dataflow/internal/FlowSummaryImpl.qll @@ -137,11 +137,9 @@ module SourceSinkInterpretationInput implements SourceOrSinkElement e, string output, string kind, Public::Provenance provenance, string model ) { exists( - string package, string type, boolean subtypes, string name, string signature, string ext, - QlBuiltins::ExtensionId madId + string package, string type, boolean subtypes, string name, string signature, string ext | - sourceModel(package, type, subtypes, name, signature, ext, output, kind, provenance, madId) and - model = "MaD:" + madId.toString() and + sourceModel(package, type, subtypes, name, signature, ext, output, kind, provenance, model) and e = interpretElement(package, type, subtypes, name, signature, ext) ) } @@ -154,11 +152,9 @@ module SourceSinkInterpretationInput implements SourceOrSinkElement e, string input, string kind, Public::Provenance provenance, string model ) { exists( - string package, string type, boolean subtypes, string name, string signature, string ext, - QlBuiltins::ExtensionId madId + string package, string type, boolean subtypes, string name, string signature, string ext | - sinkModel(package, type, subtypes, name, signature, ext, input, kind, provenance, madId) and - model = "MaD:" + madId.toString() and + sinkModel(package, type, subtypes, name, signature, ext, input, kind, provenance, model) and e = interpretElement(package, type, subtypes, name, signature, ext) ) } @@ -504,12 +500,10 @@ module Private { string model ) { exists( - string namespace, string type, boolean subtypes, string name, string signature, string ext, - QlBuiltins::ExtensionId madId + string namespace, string type, boolean subtypes, string name, string signature, string ext | summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, - provenance, madId) and - model = "MaD:" + madId.toString() and + provenance, model) and c.asFunction() = interpretElement(namespace, type, subtypes, name, signature, ext).asEntity() ) diff --git a/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll b/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll index e612239a76ec..4a0fc3f85464 100644 --- a/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll +++ b/java/ql/lib/semmle/code/java/dataflow/ExternalFlow.qll @@ -98,8 +98,53 @@ private import internal.FlowSummaryImpl private import internal.FlowSummaryImpl::Public private import internal.FlowSummaryImpl::Private private import internal.FlowSummaryImpl::Private::External -private import internal.ExternalFlowExtensions as Extensions +private import internal.ExternalFlowExtensions::Extensions as Extensions private import codeql.mad.ModelValidation as SharedModelVal +private import codeql.mad.static.ModelsAsData as SharedMaD + +private module MadInput implements SharedMaD::InputSig { + /** Holds if a source model exists for the given parameters. */ + predicate additionalSourceModel( + string package, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, string model + ) { + exists(QlBuiltins::ExtensionId madId | + any(ActiveExperimentalModelsInternal q) + .sourceModel(package, type, subtypes, name, signature, ext, output, kind, provenance, + madId) and + model = "MaD:" + madId.toString() + ) + } + + /** Holds if a sink model exists for the given parameters. */ + predicate additionalSinkModel( + string package, string type, boolean subtypes, string name, string signature, string ext, + string input, string kind, string provenance, string model + ) { + exists(QlBuiltins::ExtensionId madId | + any(ActiveExperimentalModelsInternal q) + .sinkModel(package, type, subtypes, name, signature, ext, input, kind, provenance, madId) and + model = "MaD:" + madId.toString() + ) + } + + /** Holds if a summary model exists for the given parameters. */ + predicate additionalSummaryModel( + string package, string type, boolean subtypes, string name, string signature, string ext, + string input, string output, string kind, string provenance, string model + ) { + exists(QlBuiltins::ExtensionId madId | + any(ActiveExperimentalModelsInternal q) + .summaryModel(package, type, subtypes, name, signature, ext, input, output, kind, + provenance, madId) and + model = "MaD:" + madId.toString() + ) + } +} + +private module MaD = SharedMaD::ModelsAsData; + +import MaD /** * A class for activating additional model rows. @@ -147,78 +192,18 @@ abstract private class ActiveExperimentalModelsInternal extends string { deprecated class ActiveExperimentalModels = ActiveExperimentalModelsInternal; -/** Holds if a source model exists for the given parameters. */ -predicate sourceModel( - string package, string type, boolean subtypes, string name, string signature, string ext, - string output, string kind, string provenance, QlBuiltins::ExtensionId madId -) { - ( - Extensions::sourceModel(package, type, subtypes, name, signature, ext, output, kind, provenance, - madId) - or - any(ActiveExperimentalModelsInternal q) - .sourceModel(package, type, subtypes, name, signature, ext, output, kind, provenance, madId) - ) -} - -/** Holds if a sink model exists for the given parameters. */ -predicate sinkModel( - string package, string type, boolean subtypes, string name, string signature, string ext, - string input, string kind, string provenance, QlBuiltins::ExtensionId madId -) { - ( - Extensions::sinkModel(package, type, subtypes, name, signature, ext, input, kind, provenance, - madId) - or - any(ActiveExperimentalModelsInternal q) - .sinkModel(package, type, subtypes, name, signature, ext, input, kind, provenance, madId) - ) -} - -/** Holds if a barrier model exists for the given parameters. */ -predicate barrierModel( - string package, string type, boolean subtypes, string name, string signature, string ext, - string output, string kind, string provenance, QlBuiltins::ExtensionId madId -) { - Extensions::barrierModel(package, type, subtypes, name, signature, ext, output, kind, provenance, - madId) -} - -/** Holds if a barrier guard model exists for the given parameters. */ -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 -) { - Extensions::barrierGuardModel(package, type, subtypes, name, signature, ext, input, - acceptingvalue, kind, provenance, madId) -} - -/** Holds if a summary model exists for the given parameters. */ -predicate summaryModel( - string package, string type, boolean subtypes, string name, string signature, string ext, - string input, string output, string kind, string provenance, QlBuiltins::ExtensionId madId -) { - ( - Extensions::summaryModel(package, type, subtypes, name, signature, ext, input, output, kind, - provenance, madId) - or - any(ActiveExperimentalModelsInternal q) - .summaryModel(package, type, subtypes, name, signature, ext, input, output, kind, - provenance, madId) - ) -} - /** * Holds if the given extension tuple `madId` should pretty-print as `model`. * * This predicate should only be used in tests. */ predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { + MaD::interpretModelForTest(madId, model) + or exists( string package, string type, boolean subtypes, string name, string signature, string ext, string output, string kind, string provenance | - sourceModel(package, type, subtypes, name, signature, ext, output, kind, provenance, madId) or Extensions::experimentalSourceModel(package, type, subtypes, name, signature, ext, output, kind, provenance, _, madId) | @@ -231,7 +216,6 @@ predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { string package, string type, boolean subtypes, string name, string signature, string ext, string input, string kind, string provenance | - sinkModel(package, type, subtypes, name, signature, ext, input, kind, provenance, madId) or Extensions::experimentalSinkModel(package, type, subtypes, name, signature, ext, input, kind, provenance, _, madId) | @@ -244,8 +228,6 @@ predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { string package, string type, boolean subtypes, string name, string signature, string ext, string input, string output, string kind, string provenance | - summaryModel(package, type, subtypes, name, signature, ext, input, output, kind, provenance, - madId) or Extensions::experimentalSummaryModel(package, type, subtypes, name, signature, ext, input, output, kind, provenance, _, madId) | @@ -253,67 +235,6 @@ predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { "Summary: " + package + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " + ext + "; " + input + "; " + output + "; " + kind + "; " + provenance ) - //TODO: possibly barrier models? -} - -/** Holds if a neutral model exists for the given parameters. */ -predicate neutralModel = Extensions::neutralModel/6; - -private predicate relevantPackage(string package) { - sourceModel(package, _, _, _, _, _, _, _, _, _) or - sinkModel(package, _, _, _, _, _, _, _, _, _) or - summaryModel(package, _, _, _, _, _, _, _, _, _, _) -} - -private predicate packageLink(string shortpkg, string longpkg) { - relevantPackage(shortpkg) and - relevantPackage(longpkg) and - longpkg.prefix(longpkg.indexOf(".")) = shortpkg -} - -private predicate canonicalPackage(string package) { - relevantPackage(package) and not packageLink(_, package) -} - -private predicate canonicalPkgLink(string package, string subpkg) { - canonicalPackage(package) and - (subpkg = package or packageLink(package, subpkg)) -} - -/** - * Holds if MaD framework coverage of `package` is `n` api endpoints of the - * kind `(kind, part)`, and `pkgs` is the number of subpackages of `package` - * which have MaD framework coverage (including `package` itself). - */ -predicate modelCoverage(string package, int pkgs, string kind, string part, int n) { - pkgs = strictcount(string subpkg | canonicalPkgLink(package, subpkg)) and - ( - part = "source" and - n = - strictcount(string subpkg, string type, boolean subtypes, string name, string signature, - string ext, string output, string provenance | - canonicalPkgLink(package, subpkg) and - sourceModel(subpkg, type, subtypes, name, signature, ext, output, kind, provenance, _) - ) - or - part = "sink" and - n = - strictcount(string subpkg, string type, boolean subtypes, string name, string signature, - string ext, string input, string provenance | - canonicalPkgLink(package, subpkg) and - sinkModel(subpkg, type, subtypes, name, signature, ext, input, kind, provenance, _) - ) - or - part = "summary" and - n = - strictcount(string subpkg, string type, boolean subtypes, string name, string signature, - string ext, string input, string output, string provenance | - canonicalPkgLink(package, subpkg) and - summaryModel(subpkg, type, subtypes, name, signature, ext, input, output, kind, provenance, - _) - ) - // TODO: possibly barrier models? - ) } /** Provides a query predicate to check the MaD models for validation errors. */ diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/ExternalFlowExtensions.qll b/java/ql/lib/semmle/code/java/dataflow/internal/ExternalFlowExtensions.qll index 5386d916e240..be474ad45352 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/ExternalFlowExtensions.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/ExternalFlowExtensions.qll @@ -4,6 +4,8 @@ overlay[local?] module; +private import codeql.mad.static.ModelsAsData as SharedMaD + /** * Holds if a source model exists for the given parameters. */ @@ -93,3 +95,9 @@ extensible predicate experimentalSummaryModel( string input, string output, string kind, string provenance, string filter, QlBuiltins::ExtensionId madId ); + +module Extensions implements SharedMaD::ExtensionsSig { + import ExternalFlowExtensions + + predicate namespaceGrouping(string group, string namespace) { none() } +} diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll index c712e1ae5fb6..b9d8f58cecbc 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll @@ -228,11 +228,10 @@ module SourceSinkInterpretationInput implements ) { exists( string namespace, string type, boolean subtypes, string name, string signature, string ext, - SourceOrSinkElement baseSource, string originalOutput, QlBuiltins::ExtensionId madId + SourceOrSinkElement baseSource, string originalOutput | sourceModel(namespace, type, subtypes, name, signature, ext, originalOutput, kind, provenance, - madId) and - model = "MaD:" + madId.toString() and + model) and baseSource = interpretElement(namespace, type, subtypes, name, signature, ext, _) and ( e = baseSource and output = originalOutput @@ -247,11 +246,10 @@ module SourceSinkInterpretationInput implements ) { exists( string namespace, string type, boolean subtypes, string name, string signature, string ext, - SourceOrSinkElement baseSink, string originalInput, QlBuiltins::ExtensionId madId + SourceOrSinkElement baseSink, string originalInput | sinkModel(namespace, type, subtypes, name, signature, ext, originalInput, kind, provenance, - madId) and - model = "MaD:" + madId.toString() and + model) and baseSink = interpretElement(namespace, type, subtypes, name, signature, ext, _) and ( e = baseSink and originalInput = input @@ -266,11 +264,10 @@ module SourceSinkInterpretationInput implements ) { exists( string namespace, string type, boolean subtypes, string name, string signature, string ext, - SourceOrSinkElement baseBarrier, string originalOutput, QlBuiltins::ExtensionId madId + SourceOrSinkElement baseBarrier, string originalOutput | barrierModel(namespace, type, subtypes, name, signature, ext, originalOutput, kind, - provenance, madId) and - model = "MaD:" + madId.toString() and + provenance, model) and baseBarrier = interpretElement(namespace, type, subtypes, name, signature, ext, _) and ( e = baseBarrier and output = originalOutput @@ -286,11 +283,10 @@ module SourceSinkInterpretationInput implements ) { exists( string namespace, string type, boolean subtypes, string name, string signature, string ext, - SourceOrSinkElement baseBarrier, string originalInput, QlBuiltins::ExtensionId madId + SourceOrSinkElement baseBarrier, string originalInput | barrierGuardModel(namespace, type, subtypes, name, signature, ext, originalInput, - acceptingvalue, kind, provenance, madId) and - model = "MaD:" + madId.toString() and + acceptingvalue, kind, provenance, model) and baseBarrier = interpretElement(namespace, type, subtypes, name, signature, ext, _) and ( e = baseBarrier and input = originalInput @@ -384,12 +380,10 @@ module Private { ) { exists( string namespace, string type, boolean subtypes, string name, string signature, string ext, - string originalInput, string originalOutput, Callable baseCallable, - QlBuiltins::ExtensionId madId + string originalInput, string originalOutput, Callable baseCallable | summaryModel(namespace, type, subtypes, name, signature, ext, originalInput, originalOutput, - kind, provenance, madId) and - model = "MaD:" + madId.toString() and + kind, provenance, model) and baseCallable = interpretElement(namespace, type, subtypes, name, signature, ext, isExact) and ( c.asCallable() = baseCallable and input = originalInput and output = originalOutput diff --git a/shared/mad/codeql/mad/static/ModelsAsData.qll b/shared/mad/codeql/mad/static/ModelsAsData.qll new file mode 100644 index 000000000000..84daaa9b6c86 --- /dev/null +++ b/shared/mad/codeql/mad/static/ModelsAsData.qll @@ -0,0 +1,345 @@ +overlay[local?] +module; + +signature module ExtensionsSig { + /** + * Holds if a source model exists for the given parameters. + */ + predicate sourceModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, QlBuiltins::ExtensionId madId + ); + + /** + * Holds if a sink model exists for the given parameters. + */ + predicate sinkModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string kind, string provenance, QlBuiltins::ExtensionId madId + ); + + /** + * Holds if a barrier model exists for the given parameters. + */ + predicate barrierModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, QlBuiltins::ExtensionId madId + ); + + /** + * 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, + QlBuiltins::ExtensionId madId + ); + + /** + * Holds if a summary model exists for the given parameters. + */ + predicate summaryModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string output, string kind, string provenance, QlBuiltins::ExtensionId madId + ); + + /** + * Holds if a neutral model exists for the given parameters. + */ + predicate neutralModel( + string namespace, string type, string name, string signature, string kind, string provenance + ); + + /** + * Holds if the namespace `namespace` is part of the group `group`. + */ + predicate namespaceGrouping(string group, string namespace); +} + +signature module InputSig { + /** + * Holds if a source model exists for the given parameters. + */ + default predicate additionalSourceModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, string model + ) { + none() + } + + /** + * Holds if a sink model exists for the given parameters. + */ + default predicate additionalSinkModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string kind, string provenance, string model + ) { + none() + } + + /** + * Holds if a summary model exists for the given parameters. + */ + default predicate additionalSummaryModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string output, string kind, string provenance, string model + ) { + none() + } + + /** Gets the separator used between namespace segments. */ + default string namespaceSegmentSeparator() { result = "." } + + /** Gets a cleaned-up version of the namespace for presentation in model coverage. */ + bindingset[ns] + default string cleanNamespace(string ns) { result = ns } +} + +module ModelsAsData { + /** + * Holds if the given extension tuple `madId` should pretty-print as `model`. + * + * Barrier models are included for completeness even though they will not show up in a path. + * + * This predicate should only be used in tests. + */ + predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) { + exists( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance + | + Extensions::sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, + provenance, madId) + | + model = + "Source: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + + "; " + ext + "; " + output + "; " + kind + "; " + provenance + ) + or + exists( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string kind, string provenance + | + Extensions::sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, + provenance, madId) + | + model = + "Sink: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + "; " + + ext + "; " + input + "; " + kind + "; " + provenance + ) + or + exists( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance + | + Extensions::barrierModel(namespace, type, subtypes, name, signature, ext, output, kind, + provenance, madId) + | + model = + "Barrier: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + + "; " + ext + "; " + output + "; " + kind + "; " + provenance + ) + or + exists( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string acceptingvalue, string kind, string provenance + | + Extensions::barrierGuardModel(namespace, type, subtypes, name, signature, ext, input, + acceptingvalue, kind, provenance, madId) + | + model = + "Barrier Guard: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + + signature + "; " + ext + "; " + input + "; " + acceptingvalue + "; " + kind + "; " + + provenance + ) + or + exists( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string output, string kind, string provenance + | + Extensions::summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, + provenance, madId) + | + model = + "Summary: " + namespace + "; " + type + "; " + subtypes + "; " + name + "; " + signature + + "; " + ext + "; " + input + "; " + output + "; " + kind + "; " + provenance + ) + } + + /** Gets the prefix for a group of namespaces. */ + private string groupPrefix() { result = "group:" } + + /** + * Gets a namespace represented by `namespaceOrGroup`. + * + * If `namespaceOrGroup` is of the form `group:` then `result` is a + * namespace in the group ``, as determined by `namespaceGrouping`. + * Otherwise, `result` is `namespaceOrGroup`. + */ + bindingset[namespaceOrGroup] + private string getNamespace(string namespaceOrGroup) { + not exists(string group | namespaceOrGroup = groupPrefix() + group) and + result = namespaceOrGroup + or + exists(string group | + Extensions::namespaceGrouping(group, result) and + namespaceOrGroup = groupPrefix() + group + ) + } + + /** + * Holds if a source model exists for the given parameters. + */ + predicate sourceModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, string model + ) { + exists(string namespaceOrGroup | namespace = getNamespace(namespaceOrGroup) | + exists(QlBuiltins::ExtensionId madId | + Extensions::sourceModel(namespaceOrGroup, type, subtypes, name, signature, ext, output, + kind, provenance, madId) and + model = "MaD:" + madId.toString() + ) + or + Input::additionalSourceModel(namespaceOrGroup, type, subtypes, name, signature, ext, output, + kind, provenance, model) + ) + } + + /** + * Holds if a sink model exists for the given parameters. + */ + predicate sinkModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string kind, string provenance, string model + ) { + exists(string namespaceOrGroup | namespace = getNamespace(namespaceOrGroup) | + exists(QlBuiltins::ExtensionId madId | + Extensions::sinkModel(namespaceOrGroup, type, subtypes, name, signature, ext, input, kind, + provenance, madId) and + model = "MaD:" + madId.toString() + ) + or + Input::additionalSinkModel(namespaceOrGroup, type, subtypes, name, signature, ext, input, + kind, provenance, model) + ) + } + + /** Holds if a barrier model exists for the given parameters. */ + predicate barrierModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string output, string kind, string provenance, string model + ) { + exists(string namespaceOrGroup, QlBuiltins::ExtensionId madId | + namespace = getNamespace(namespaceOrGroup) and + Extensions::barrierModel(namespaceOrGroup, type, subtypes, name, signature, ext, output, kind, + provenance, madId) and + model = "MaD:" + madId.toString() + ) + } + + /** 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 + ) { + exists(string namespaceOrGroup, QlBuiltins::ExtensionId madId | + namespace = getNamespace(namespaceOrGroup) and + Extensions::barrierGuardModel(namespaceOrGroup, type, subtypes, name, signature, ext, input, + acceptingvalue, kind, provenance, madId) and + model = "MaD:" + madId.toString() + ) + } + + /** + * Holds if a summary model exists for the given parameters. + */ + predicate summaryModel( + string namespace, string type, boolean subtypes, string name, string signature, string ext, + string input, string output, string kind, string provenance, string model + ) { + exists(string namespaceOrGroup | namespace = getNamespace(namespaceOrGroup) | + exists(QlBuiltins::ExtensionId madId | + Extensions::summaryModel(namespaceOrGroup, type, subtypes, name, signature, ext, input, + output, kind, provenance, madId) and + model = "MaD:" + madId.toString() + ) + or + Input::additionalSummaryModel(namespaceOrGroup, type, subtypes, name, signature, ext, input, + output, kind, provenance, model) + ) + } + + /** + * Holds if a neutral model exists for the given parameters. + */ + predicate neutralModel( + string namespace, string type, string name, string signature, string kind, string provenance + ) { + exists(string namespaceOrGroup | namespace = getNamespace(namespaceOrGroup) | + Extensions::neutralModel(namespaceOrGroup, type, name, signature, kind, provenance) + ) + } + + private predicate relevantNamespace(string namespace) { + exists(string ns | namespace = Input::cleanNamespace(ns) | + sourceModel(ns, _, _, _, _, _, _, _, _, _) or + sinkModel(ns, _, _, _, _, _, _, _, _, _) or + summaryModel(ns, _, _, _, _, _, _, _, _, _, _) + ) + } + + private predicate namespaceLink(string shortns, string longns) { + relevantNamespace(shortns) and + relevantNamespace(longns) and + longns.prefix(longns.indexOf(Input::namespaceSegmentSeparator())) = shortns + } + + private predicate canonicalNamespace(string namespace) { + relevantNamespace(namespace) and not namespaceLink(_, namespace) + } + + private predicate canonicalNamespaceLink(string namespace, string subns) { + canonicalNamespace(namespace) and + (subns = namespace or namespaceLink(namespace, subns)) + } + + /** + * Holds if MaD framework coverage of `namespace` is `n` api endpoints of the + * kind `(kind, part)`, and `namespaces` is the number of subnamespaces of + * `namespace` which have MaD framework coverage (including `namespace` + * itself). + */ + predicate modelCoverage(string namespace, int namespaces, string kind, string part, int n) { + namespaces = strictcount(string subns | canonicalNamespaceLink(namespace, subns)) and + ( + part = "source" and + n = + strictcount(string subns, string subnsClean, string type, boolean subtypes, string name, + string signature, string ext, string output, string provenance | + canonicalNamespaceLink(namespace, subnsClean) and + subnsClean = Input::cleanNamespace(subns) and + sourceModel(subns, type, subtypes, name, signature, ext, output, kind, provenance, _) + ) + or + part = "sink" and + n = + strictcount(string subns, string subnsClean, string type, boolean subtypes, string name, + string signature, string ext, string input, string provenance | + canonicalNamespaceLink(namespace, subnsClean) and + subnsClean = Input::cleanNamespace(subns) and + sinkModel(subns, type, subtypes, name, signature, ext, input, kind, provenance, _) + ) + or + part = "summary" and + n = + strictcount(string subns, string subnsClean, string type, boolean subtypes, string name, + string signature, string ext, string input, string output, string provenance | + canonicalNamespaceLink(namespace, subnsClean) and + subnsClean = Input::cleanNamespace(subns) and + summaryModel(subns, type, subtypes, name, signature, ext, input, output, kind, provenance, + _) + ) + ) + } +}