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 6665e0e7480..890025a9483 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll @@ -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) } /** diff --git a/go/ql/lib/semmle/go/dataflow/internal/FlowSummaryImpl.qll b/go/ql/lib/semmle/go/dataflow/internal/FlowSummaryImpl.qll index 6665e0e7480..890025a9483 100644 --- a/go/ql/lib/semmle/go/dataflow/internal/FlowSummaryImpl.qll +++ b/go/ql/lib/semmle/go/dataflow/internal/FlowSummaryImpl.qll @@ -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) } /** diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/FlowSummaryImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/FlowSummaryImpl.qll index 6665e0e7480..890025a9483 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/FlowSummaryImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/FlowSummaryImpl.qll @@ -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) } /** diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/FlowSummaryImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/FlowSummaryImpl.qll index 6665e0e7480..890025a9483 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/FlowSummaryImpl.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/FlowSummaryImpl.qll @@ -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) } /** diff --git a/swift/ql/lib/codeql/swift/dataflow/internal/FlowSummaryImpl.qll b/swift/ql/lib/codeql/swift/dataflow/internal/FlowSummaryImpl.qll index 6665e0e7480..890025a9483 100644 --- a/swift/ql/lib/codeql/swift/dataflow/internal/FlowSummaryImpl.qll +++ b/swift/ql/lib/codeql/swift/dataflow/internal/FlowSummaryImpl.qll @@ -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) } /**