Java/C#: Share model coverage code.

This commit is contained in:
Anders Schack-Mulligen
2025-12-11 08:44:09 +01:00
parent 0915db4f6b
commit 3b334ea215
3 changed files with 59 additions and 113 deletions

View File

@@ -107,62 +107,6 @@ private module MaD = SharedMaD::ModelsAsData<Extensions>;
import MaD
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 |
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, _)
)
)
}
/** Provides a query predicate to check the MaD models for validation errors. */
module ModelValidation {
private predicate getRelevantAccessPath(string path) {

View File

@@ -261,63 +261,6 @@ predicate interpretModelForTest(QlBuiltins::ExtensionId madId, string model) {
/** 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. */
module ModelValidation {
private import codeql.dataflow.internal.AccessPathSyntax as AccessPathSyntax

View File

@@ -121,4 +121,63 @@ module ModelsAsData<ExtensionsSig Extensions> {
"; " + ext + "; " + input + "; " + output + "; " + kind + "; " + provenance
)
}
private predicate relevantNamespace(string namespace) {
Extensions::sourceModel(namespace, _, _, _, _, _, _, _, _, _) or
Extensions::sinkModel(namespace, _, _, _, _, _, _, _, _, _) or
Extensions::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 |
canonicalNamespaceLink(namespace, subns) and
Extensions::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
Extensions::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
Extensions::summaryModel(subns, type, subtypes, name, signature, ext, input, output, kind,
provenance, _)
)
)
}
}