@@ -215,6 +215,54 @@ module Public {
215215 abstract predicate required ( SummaryComponent head , SummaryComponentStack tail ) ;
216216 }
217217
218+ /**
219+ * Gets the valid model origin values.
220+ */
221+ private string getValidModelOrigin ( ) {
222+ result =
223+ [
224+ "ai" , // AI (machine learning)
225+ "df" , // Dataflow (model generator)
226+ "tb" , // Type based (model generator)
227+ "hq" , // Heuristic query
228+ ]
229+ }
230+
231+ /**
232+ * A class used to represent provenance values for MaD models.
233+ *
234+ * The provenance value is a string of the form `origin-verification`
235+ * (or just `manual`), where `origin` is a value indicating the
236+ * origin of the model, and `verification` is a value indicating, how
237+ * the model was verified.
238+ *
239+ * Examples could be:
240+ * - `df-generated`: A model produced by the model generator, but not verified by a human.
241+ * - `ai-manual`: A model produced by AI, but verified by a human.
242+ */
243+ class Provenance extends string {
244+ private string verification ;
245+
246+ Provenance ( ) {
247+ exists ( string origin | origin = getValidModelOrigin ( ) |
248+ this = origin + "-" + verification and
249+ verification = [ "manual" , "generated" ]
250+ )
251+ or
252+ this = verification and verification = "manual"
253+ }
254+
255+ /**
256+ * Holds if this is a valid generated provenance value.
257+ */
258+ predicate isGenerated ( ) { verification = "generated" }
259+
260+ /**
261+ * Holds if this is a valid manual provenance value.
262+ */
263+ predicate isManual ( ) { verification = "manual" }
264+ }
265+
218266 /** A callable with a flow summary. */
219267 abstract class SummarizedCallable extends SummarizedCallableBase {
220268 bindingset [ this ]
@@ -248,41 +296,61 @@ module Public {
248296 }
249297
250298 /**
251- * Holds if all the summaries that apply to ` this` are auto generated and not manually created .
299+ * Holds if there exists a generated summary that applies to this callable .
252300 */
253- final predicate isAutoGenerated ( ) {
254- this . hasProvenance ( [ "generated" , "ai-generated" ] ) and not this .isManual ( )
301+ final predicate hasGeneratedModel ( ) {
302+ exists ( Provenance p | p . isGenerated ( ) and this .hasProvenance ( p ) )
255303 }
256304
257305 /**
258- * Holds if there exists a manual summary that applies to `this`.
306+ * Holds if all the summaries that apply to this callable are auto generated and not manually created.
307+ * That is, only apply generated models, when there are no manual models.
259308 */
260- final predicate isManual ( ) { this .hasProvenance ( "manual" ) }
309+ final predicate applyGeneratedModel ( ) {
310+ this .hasGeneratedModel ( ) and
311+ not this .hasManualModel ( )
312+ }
261313
262314 /**
263- * Holds if there exists a summary that applies to ` this` that has provenance `provenance` .
315+ * Holds if there exists a manual summary that applies to this callable .
264316 */
265- predicate hasProvenance ( string provenance ) { none ( ) }
317+ final predicate hasManualModel ( ) {
318+ exists ( Provenance p | p .isManual ( ) and this .hasProvenance ( p ) )
319+ }
320+
321+ /**
322+ * Holds if there exists a manual summary that applies to this callable.
323+ * Always apply manual models if they exist.
324+ */
325+ final predicate applyManualModel ( ) { this .hasManualModel ( ) }
326+
327+ /**
328+ * Holds if there exists a summary that applies to this callable
329+ * that has provenance `provenance`.
330+ */
331+ predicate hasProvenance ( Provenance provenance ) { provenance = "manual" }
266332 }
267333
268334 /** A callable where there is no flow via the callable. */
269335 class NeutralCallable extends SummarizedCallableBase {
270- NeutralCallable ( ) { neutralElement ( this , _) }
336+ private Provenance provenance ;
337+
338+ NeutralCallable ( ) { neutralElement ( this , provenance ) }
271339
272340 /**
273341 * Holds if the neutral is auto generated.
274342 */
275- predicate isAutoGenerated ( ) { neutralElement ( this , [ "generated" , "ai-generated" ] ) }
343+ final predicate hasGeneratedModel ( ) { provenance . isGenerated ( ) }
276344
277345 /**
278- * Holds if there exists a manual neutral that applies to ` this` .
346+ * Holds if there exists a manual neutral that applies to this callable .
279347 */
280- final predicate isManual ( ) { this . hasProvenance ( "manual" ) }
348+ final predicate hasManualModel ( ) { provenance . isManual ( ) }
281349
282350 /**
283- * Holds if the neutral has provenance `provenance `.
351+ * Holds if the neutral has provenance `p `.
284352 */
285- predicate hasProvenance ( string provenance ) { neutralElement ( this , provenance ) }
353+ predicate hasProvenance ( Provenance p ) { p = provenance }
286354 }
287355}
288356
@@ -1017,12 +1085,18 @@ module Private {
10171085 private predicate relevantSummaryElementGenerated (
10181086 AccessPath inSpec , AccessPath outSpec , string kind
10191087 ) {
1020- summaryElement ( this , inSpec , outSpec , kind , [ "generated" , "ai-generated" ] ) and
1021- not summaryElement ( this , _, _, _, "manual" )
1088+ exists ( Provenance provenance |
1089+ provenance .isGenerated ( ) and
1090+ summaryElement ( this , inSpec , outSpec , kind , provenance )
1091+ ) and
1092+ not this .applyManualModel ( )
10221093 }
10231094
10241095 private predicate relevantSummaryElement ( AccessPath inSpec , AccessPath outSpec , string kind ) {
1025- summaryElement ( this , inSpec , outSpec , kind , "manual" )
1096+ exists ( Provenance provenance |
1097+ provenance .isManual ( ) and
1098+ summaryElement ( this , inSpec , outSpec , kind , provenance )
1099+ )
10261100 or
10271101 this .relevantSummaryElementGenerated ( inSpec , outSpec , kind )
10281102 }
@@ -1041,7 +1115,7 @@ module Private {
10411115 )
10421116 }
10431117
1044- override predicate hasProvenance ( string provenance ) {
1118+ override predicate hasProvenance ( Provenance provenance ) {
10451119 summaryElement ( this , _, _, _, provenance )
10461120 }
10471121 }
@@ -1052,6 +1126,10 @@ module Private {
10521126 not exists ( interpretComponent ( c ) )
10531127 }
10541128
1129+ /** Holds if `provenance` is not a valid provenance value. */
1130+ bindingset [ provenance]
1131+ predicate invalidProvenance ( string provenance ) { not provenance instanceof Provenance }
1132+
10551133 /**
10561134 * Holds if token `part` of specification `spec` has an invalid index.
10571135 * E.g., `Argument[-1]`.
@@ -1219,11 +1297,11 @@ module Private {
12191297 }
12201298
12211299 private string renderProvenance ( SummarizedCallable c ) {
1222- if c .isManual ( ) then result = "manual" else c .hasProvenance ( result )
1300+ if c .applyManualModel ( ) then result = "manual" else c .hasProvenance ( result )
12231301 }
12241302
12251303 private string renderProvenanceNeutral ( NeutralCallable c ) {
1226- if c .isManual ( ) then result = "manual" else c .hasProvenance ( result )
1304+ if c .hasManualModel ( ) then result = "manual" else c .hasProvenance ( result )
12271305 }
12281306
12291307 /**
0 commit comments