Merge pull request #11721 from michaelnebel/csharpjava/refactorprovenance

C#/Java: Re-factor provenance related predicates.
This commit is contained in:
Michael Nebel
2023-01-12 10:50:31 +01:00
committed by GitHub
20 changed files with 269 additions and 291 deletions

View File

@@ -124,17 +124,10 @@ 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) }
bindingset[input]
private predicate getKind(string input, string kind, boolean generated) {
input.splitAt(":", 0) = "generated" and kind = input.splitAt(":", 1) and generated = true
or
not input.matches("%:%") and kind = input and generated = false
}
/** 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, boolean generated
string output, string kind, string provenance
) {
exists(string row |
sourceModel(row) and
@@ -146,14 +139,15 @@ predicate sourceModel(
row.splitAt(";", 4) = signature and
row.splitAt(";", 5) = ext and
row.splitAt(";", 6) = output and
exists(string k | row.splitAt(";", 7) = k and getKind(k, kind, generated))
row.splitAt(";", 7) = kind and
provenance = "manual"
)
}
/** 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, boolean generated
string input, string kind, string provenance
) {
exists(string row |
sinkModel(row) and
@@ -165,34 +159,30 @@ predicate sinkModel(
row.splitAt(";", 4) = signature and
row.splitAt(";", 5) = ext and
row.splitAt(";", 6) = input and
exists(string k | row.splitAt(";", 7) = k and getKind(k, kind, generated))
row.splitAt(";", 7) = kind and
provenance = "manual"
)
}
/** 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, boolean generated
string input, string output, string kind, string provenance
) {
summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, generated, _)
}
/** Holds if a summary model `row` 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, boolean generated, 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
exists(string k | row.splitAt(";", 8) = k and getKind(k, kind, generated))
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"
}
/** Holds if `package` have CSV framework coverage. */
@@ -241,25 +231,25 @@ predicate modelCoverage(string package, int pkgs, string kind, string part, int
part = "source" and
n =
strictcount(string subpkg, string type, boolean subtypes, string name, string signature,
string ext, string output, boolean generated |
string ext, string output, string provenance |
canonicalPackageHasASubpackage(package, subpkg) and
sourceModel(subpkg, type, subtypes, name, signature, ext, output, kind, generated)
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, boolean generated |
string ext, string input, string provenance |
canonicalPackageHasASubpackage(package, subpkg) and
sinkModel(subpkg, type, subtypes, name, signature, ext, input, kind, generated)
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, boolean generated |
string ext, string input, string output, string provenance |
canonicalPackageHasASubpackage(package, subpkg) and
summaryModel(subpkg, type, subtypes, name, signature, ext, input, output, kind, generated)
summaryModel(subpkg, type, subtypes, name, signature, ext, input, output, kind, provenance)
)
)
}
@@ -298,9 +288,8 @@ module CsvValidation {
}
private string getInvalidModelKind() {
exists(string row, string k, string kind | summaryModel(row) |
k = row.splitAt(";", 8) and
getKind(k, kind, _) and
exists(string row, string kind | summaryModel(row) |
kind = row.splitAt(";", 8) and
not kind = ["taint", "value"] and
result = "Invalid kind \"" + kind + "\" in summary model."
)

View File

@@ -241,15 +241,19 @@ module Public {
}
/**
* Holds if the summary is auto generated and not manually generated.
* Holds if all the summaries that apply to `this` are auto generated and not manually created.
*/
predicate isAutoGenerated() { none() }
final predicate isAutoGenerated() { this.hasProvenance("generated") and not this.isManual() }
/**
* Holds if the summary has the given provenance where `true` is
* `generated` and `false` is `manual`.
* Holds if there exists a manual summary that applies to `this`.
*/
predicate hasProvenance(boolean generated) { none() }
final predicate isManual() { this.hasProvenance("manual") }
/**
* Holds if there exists a summary that applies to `this` that has provenance `provenance`.
*/
predicate hasProvenance(string provenance) { none() }
}
/** A callable where there is no flow via the callable. */
@@ -257,15 +261,19 @@ module Public {
NeutralCallable() { neutralElement(this, _) }
/**
* Holds if the neutral is auto generated.
* Holds if the neutral is auto generated.
*/
predicate isAutoGenerated() { neutralElement(this, true) }
predicate isAutoGenerated() { neutralElement(this, "generated") }
/**
* Holds if the neutral has the given provenance where `true` is
* `generated` and `false` is `manual`.
* Holds if there exists a manual neutral that applies to `this`.
*/
predicate hasProvenance(boolean generated) { neutralElement(this, generated) }
final predicate isManual() { this.hasProvenance("manual") }
/**
* Holds if the neutral has provenance `provenance`.
*/
predicate hasProvenance(string provenance) { neutralElement(this, provenance) }
}
}
@@ -997,12 +1005,12 @@ module Private {
private predicate relevantSummaryElementGenerated(
AccessPath inSpec, AccessPath outSpec, string kind
) {
summaryElement(this, inSpec, outSpec, kind, true) and
not summaryElement(this, _, _, _, false)
summaryElement(this, inSpec, outSpec, kind, "generated") and
not summaryElement(this, _, _, _, "manual")
}
private predicate relevantSummaryElement(AccessPath inSpec, AccessPath outSpec, string kind) {
summaryElement(this, inSpec, outSpec, kind, false)
summaryElement(this, inSpec, outSpec, kind, "manual")
or
this.relevantSummaryElementGenerated(inSpec, outSpec, kind)
}
@@ -1021,10 +1029,8 @@ module Private {
)
}
override predicate isAutoGenerated() { this.relevantSummaryElementGenerated(_, _, _) }
override predicate hasProvenance(boolean generated) {
summaryElement(this, _, _, _, generated)
override predicate hasProvenance(string provenance) {
summaryElement(this, _, _, _, provenance)
}
}

View File

@@ -60,26 +60,25 @@ DataFlowType getSyntheticGlobalType(SummaryComponent::SyntheticGlobal sg) { any(
/**
* Holds if an external flow summary exists for `c` with input specification
* `input`, output specification `output`, kind `kind`, and a flag `generated`
* stating whether the summary is autogenerated.
* `input`, output specification `output`, kind `kind`, and provenance `provenance`.
*/
predicate summaryElement(
SummarizedCallableBase c, string input, string output, string kind, boolean generated
SummarizedCallableBase c, string input, string output, string kind, string provenance
) {
exists(
string namespace, string type, boolean subtypes, string name, string signature, string ext
|
summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, generated) and
summaryModel(namespace, type, subtypes, name, signature, ext, input, output, kind, provenance) and
c.asFunction() = interpretElement(namespace, type, subtypes, name, signature, ext).asEntity()
)
}
/**
* Holds if a neutral model exists for `c`, which means that there is no
* flow through `c`. The flag `generated` states whether the model is autogenerated.
* Holds if a neutral model exists for `c` with provenance `provenance`,
* which means that there is no flow through `c`.
* Note. Neutral models have not been implemented for Go.
*/
predicate neutralElement(SummarizedCallable c, boolean generated) { none() }
predicate neutralElement(SummarizedCallable c, string provenance) { none() }
/** Gets the summary component for specification component `c`, if any. */
bindingset[c]
@@ -152,28 +151,26 @@ class SourceOrSinkElement extends TSourceOrSinkElement {
/**
* Holds if an external source specification exists for `e` with output specification
* `output`, kind `kind`, and a flag `generated` stating whether the source specification is
* autogenerated.
* `output`, kind `kind`, and provenance `provenance`.
*/
predicate sourceElement(SourceOrSinkElement e, string output, string kind, boolean generated) {
predicate sourceElement(SourceOrSinkElement e, string output, string kind, string provenance) {
exists(
string namespace, string type, boolean subtypes, string name, string signature, string ext
|
sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, generated) and
sourceModel(namespace, type, subtypes, name, signature, ext, output, kind, provenance) and
e = interpretElement(namespace, type, subtypes, name, signature, ext)
)
}
/**
* Holds if an external sink specification exists for `e` with input specification
* `input`, kind `kind` and a flag `generated` stating whether the sink specification is
* autogenerated.
* `input`, kind `kind` and provenance `provenance`.
*/
predicate sinkElement(SourceOrSinkElement e, string input, string kind, boolean generated) {
predicate sinkElement(SourceOrSinkElement e, string input, string kind, string provenance) {
exists(
string namespace, string type, boolean subtypes, string name, string signature, string ext
|
sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, generated) and
sinkModel(namespace, type, subtypes, name, signature, ext, input, kind, provenance) and
e = interpretElement(namespace, type, subtypes, name, signature, ext)
)
}