@@ -215,6 +215,54 @@ module Public {
215
215
abstract predicate required ( SummaryComponent head , SummaryComponentStack tail ) ;
216
216
}
217
217
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
+
218
266
/** A callable with a flow summary. */
219
267
abstract class SummarizedCallable extends SummarizedCallableBase {
220
268
bindingset [ this ]
@@ -248,41 +296,61 @@ module Public {
248
296
}
249
297
250
298
/**
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 .
252
300
*/
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 ) )
255
303
}
256
304
257
305
/**
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.
259
308
*/
260
- final predicate isManual ( ) { this .hasProvenance ( "manual" ) }
309
+ final predicate applyGeneratedModel ( ) {
310
+ this .hasGeneratedModel ( ) and
311
+ not this .hasManualModel ( )
312
+ }
261
313
262
314
/**
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 .
264
316
*/
265
- predicate hasProvenance ( string provenance ) { provenance = "manual" }
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" }
266
332
}
267
333
268
334
/** A callable where there is no flow via the callable. */
269
335
class NeutralCallable extends SummarizedCallableBase {
270
- NeutralCallable ( ) { neutralElement ( this , _) }
336
+ private Provenance provenance ;
337
+
338
+ NeutralCallable ( ) { neutralElement ( this , provenance ) }
271
339
272
340
/**
273
341
* Holds if the neutral is auto generated.
274
342
*/
275
- predicate isAutoGenerated ( ) { neutralElement ( this , [ "generated" , "ai-generated" ] ) }
343
+ final predicate hasGeneratedModel ( ) { provenance . isGenerated ( ) }
276
344
277
345
/**
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 .
279
347
*/
280
- final predicate isManual ( ) { this . hasProvenance ( "manual" ) }
348
+ final predicate hasManualModel ( ) { provenance . isManual ( ) }
281
349
282
350
/**
283
- * Holds if the neutral has provenance `provenance `.
351
+ * Holds if the neutral has provenance `p `.
284
352
*/
285
- predicate hasProvenance ( string provenance ) { neutralElement ( this , provenance ) }
353
+ predicate hasProvenance ( Provenance p ) { p = provenance }
286
354
}
287
355
}
288
356
@@ -1017,12 +1085,18 @@ module Private {
1017
1085
private predicate relevantSummaryElementGenerated (
1018
1086
AccessPath inSpec , AccessPath outSpec , string kind
1019
1087
) {
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 ( )
1022
1093
}
1023
1094
1024
1095
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
+ )
1026
1100
or
1027
1101
this .relevantSummaryElementGenerated ( inSpec , outSpec , kind )
1028
1102
}
@@ -1041,7 +1115,7 @@ module Private {
1041
1115
)
1042
1116
}
1043
1117
1044
- override predicate hasProvenance ( string provenance ) {
1118
+ override predicate hasProvenance ( Provenance provenance ) {
1045
1119
summaryElement ( this , _, _, _, provenance )
1046
1120
}
1047
1121
}
@@ -1052,6 +1126,10 @@ module Private {
1052
1126
not exists ( interpretComponent ( c ) )
1053
1127
}
1054
1128
1129
+ /** Holds if `provenance` is not a valid provenance value. */
1130
+ bindingset [ provenance]
1131
+ predicate invalidProvenance ( string provenance ) { not provenance instanceof Provenance }
1132
+
1055
1133
/**
1056
1134
* Holds if token `part` of specification `spec` has an invalid index.
1057
1135
* E.g., `Argument[-1]`.
@@ -1219,11 +1297,11 @@ module Private {
1219
1297
}
1220
1298
1221
1299
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 )
1223
1301
}
1224
1302
1225
1303
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 )
1227
1305
}
1228
1306
1229
1307
/**
0 commit comments