Merge pull request #12595 from michaelnebel/enhanceprovenance

Java/C# : Enhance provenance.
This commit is contained in:
Michael Nebel
2023-04-13 14:27:53 +02:00
committed by GitHub
107 changed files with 107256 additions and 106710 deletions

View File

@@ -215,6 +215,54 @@ module Public {
abstract predicate required(SummaryComponent head, SummaryComponentStack tail);
}
/**
* Gets the valid model origin values.
*/
private string getValidModelOrigin() {
result =
[
"ai", // AI (machine learning)
"df", // Dataflow (model generator)
"tb", // Type based (model generator)
"hq", // Heuristic query
]
}
/**
* A class used to represent provenance values for MaD models.
*
* The provenance value is a string of the form `origin-verification`
* (or just `manual`), where `origin` is a value indicating the
* origin of the model, and `verification` is a value indicating, how
* the model was verified.
*
* Examples could be:
* - `df-generated`: A model produced by the model generator, but not verified by a human.
* - `ai-manual`: A model produced by AI, but verified by a human.
*/
class Provenance extends string {
private string verification;
Provenance() {
exists(string origin | origin = getValidModelOrigin() |
this = origin + "-" + verification and
verification = ["manual", "generated"]
)
or
this = verification and verification = "manual"
}
/**
* Holds if this is a valid generated provenance value.
*/
predicate isGenerated() { verification = "generated" }
/**
* Holds if this is a valid manual provenance value.
*/
predicate isManual() { verification = "manual" }
}
/** A callable with a flow summary. */
abstract class SummarizedCallable extends SummarizedCallableBase {
bindingset[this]
@@ -248,41 +296,61 @@ module Public {
}
/**
* Holds if all the summaries that apply to `this` are auto generated and not manually created.
* Holds if there exists a generated summary that applies to this callable.
*/
final predicate isAutoGenerated() {
this.hasProvenance(["generated", "ai-generated"]) and not this.isManual()
final predicate hasGeneratedModel() {
exists(Provenance p | p.isGenerated() and this.hasProvenance(p))
}
/**
* Holds if there exists a manual summary that applies to `this`.
* Holds if all the summaries that apply to this callable are auto generated and not manually created.
* That is, only apply generated models, when there are no manual models.
*/
final predicate isManual() { this.hasProvenance("manual") }
final predicate applyGeneratedModel() {
this.hasGeneratedModel() and
not this.hasManualModel()
}
/**
* Holds if there exists a summary that applies to `this` that has provenance `provenance`.
* Holds if there exists a manual summary that applies to this callable.
*/
predicate hasProvenance(string provenance) { none() }
final predicate hasManualModel() {
exists(Provenance p | p.isManual() and this.hasProvenance(p))
}
/**
* Holds if there exists a manual summary that applies to this callable.
* Always apply manual models if they exist.
*/
final predicate applyManualModel() { this.hasManualModel() }
/**
* Holds if there exists a summary that applies to this callable
* that has provenance `provenance`.
*/
predicate hasProvenance(Provenance provenance) { provenance = "manual" }
}
/** A callable where there is no flow via the callable. */
class NeutralCallable extends SummarizedCallableBase {
NeutralCallable() { neutralElement(this, _) }
private Provenance provenance;
NeutralCallable() { neutralElement(this, provenance) }
/**
* Holds if the neutral is auto generated.
*/
predicate isAutoGenerated() { neutralElement(this, ["generated", "ai-generated"]) }
final predicate hasGeneratedModel() { provenance.isGenerated() }
/**
* Holds if there exists a manual neutral that applies to `this`.
* Holds if there exists a manual neutral that applies to this callable.
*/
final predicate isManual() { this.hasProvenance("manual") }
final predicate hasManualModel() { provenance.isManual() }
/**
* Holds if the neutral has provenance `provenance`.
* Holds if the neutral has provenance `p`.
*/
predicate hasProvenance(string provenance) { neutralElement(this, provenance) }
predicate hasProvenance(Provenance p) { p = provenance }
}
}
@@ -1017,12 +1085,18 @@ module Private {
private predicate relevantSummaryElementGenerated(
AccessPath inSpec, AccessPath outSpec, string kind
) {
summaryElement(this, inSpec, outSpec, kind, ["generated", "ai-generated"]) and
not summaryElement(this, _, _, _, "manual")
exists(Provenance provenance |
provenance.isGenerated() and
summaryElement(this, inSpec, outSpec, kind, provenance)
) and
not this.applyManualModel()
}
private predicate relevantSummaryElement(AccessPath inSpec, AccessPath outSpec, string kind) {
summaryElement(this, inSpec, outSpec, kind, "manual")
exists(Provenance provenance |
provenance.isManual() and
summaryElement(this, inSpec, outSpec, kind, provenance)
)
or
this.relevantSummaryElementGenerated(inSpec, outSpec, kind)
}
@@ -1041,7 +1115,7 @@ module Private {
)
}
override predicate hasProvenance(string provenance) {
override predicate hasProvenance(Provenance provenance) {
summaryElement(this, _, _, _, provenance)
}
}
@@ -1052,6 +1126,10 @@ module Private {
not exists(interpretComponent(c))
}
/** Holds if `provenance` is not a valid provenance value. */
bindingset[provenance]
predicate invalidProvenance(string provenance) { not provenance instanceof Provenance }
/**
* Holds if token `part` of specification `spec` has an invalid index.
* E.g., `Argument[-1]`.
@@ -1219,11 +1297,11 @@ module Private {
}
private string renderProvenance(SummarizedCallable c) {
if c.isManual() then result = "manual" else c.hasProvenance(result)
if c.applyManualModel() then result = "manual" else c.hasProvenance(result)
}
private string renderProvenanceNeutral(NeutralCallable c) {
if c.isManual() then result = "manual" else c.hasProvenance(result)
if c.hasManualModel() then result = "manual" else c.hasProvenance(result)
}
/**