@@ -179,25 +179,23 @@ class NegativeSummaryModelCsv extends Unit {
179
179
abstract predicate row ( string row ) ;
180
180
}
181
181
182
- /** Holds if `row` is a source model. */
183
- predicate sourceModel ( string row ) { any ( SourceModelCsv s ) .row ( row ) }
182
+ private predicate sourceModelInternal ( string row ) { any ( SourceModelCsv s ) .row ( row ) }
184
183
185
- /** Holds if `row` is a sink model. */
186
- predicate sinkModel ( string row ) { any ( SinkModelCsv s ) .row ( row ) }
184
+ private predicate summaryModelInternal ( string row ) { any ( SummaryModelCsv s ) .row ( row ) }
187
185
188
- /** Holds if `row` is a summary model. */
189
- predicate summaryModel ( string row ) { any ( SummaryModelCsv s ) .row ( row ) }
186
+ private predicate sinkModelInternal ( string row ) { any ( SinkModelCsv s ) .row ( row ) }
190
187
191
- /** Holds if `row` is a negative summary model. */
192
- predicate negativeSummaryModel ( string row ) { any ( NegativeSummaryModelCsv s ) .row ( row ) }
188
+ private predicate negativeSummaryModelInternal ( string row ) {
189
+ any ( NegativeSummaryModelCsv s ) .row ( row )
190
+ }
193
191
194
192
/** Holds if a source model exists for the given parameters. */
195
193
predicate sourceModel (
196
194
string namespace , string type , boolean subtypes , string name , string signature , string ext ,
197
195
string output , string kind , string provenance
198
196
) {
199
197
exists ( string row |
200
- sourceModel ( row ) and
198
+ sourceModelInternal ( row ) and
201
199
row .splitAt ( ";" , 0 ) = namespace and
202
200
row .splitAt ( ";" , 1 ) = type and
203
201
row .splitAt ( ";" , 2 ) = subtypes .toString ( ) and
@@ -211,13 +209,33 @@ predicate sourceModel(
211
209
)
212
210
}
213
211
212
+ /** Holds if `row` is a source model. */
213
+ predicate sourceModel ( string row ) {
214
+ exists (
215
+ string namespace , string type , boolean subtypes , string name , string signature , string ext ,
216
+ string output , string kind , string provenance
217
+ |
218
+ sourceModel ( namespace , type , subtypes , name , signature , ext , output , kind , provenance ) and
219
+ row =
220
+ namespace + ";" //
221
+ + type + ";" //
222
+ + subtypes .toString ( ) + ";" //
223
+ + name + ";" //
224
+ + signature + ";" //
225
+ + ext + ";" //
226
+ + output + ";" //
227
+ + kind + ";" //
228
+ + provenance
229
+ )
230
+ }
231
+
214
232
/** Holds if a sink model exists for the given parameters. */
215
233
predicate sinkModel (
216
234
string namespace , string type , boolean subtypes , string name , string signature , string ext ,
217
235
string input , string kind , string provenance
218
236
) {
219
237
exists ( string row |
220
- sinkModel ( row ) and
238
+ sinkModelInternal ( row ) and
221
239
row .splitAt ( ";" , 0 ) = namespace and
222
240
row .splitAt ( ";" , 1 ) = type and
223
241
row .splitAt ( ";" , 2 ) = subtypes .toString ( ) and
@@ -231,13 +249,33 @@ predicate sinkModel(
231
249
)
232
250
}
233
251
252
+ /** Holds if `row` is a sink model. */
253
+ predicate sinkModel ( string row ) {
254
+ exists (
255
+ string namespace , string type , boolean subtypes , string name , string signature , string ext ,
256
+ string input , string kind , string provenance
257
+ |
258
+ sinkModel ( namespace , type , subtypes , name , signature , ext , input , kind , provenance ) and
259
+ row =
260
+ namespace + ";" //
261
+ + type + ";" //
262
+ + subtypes .toString ( ) + ";" //
263
+ + name + ";" //
264
+ + signature + ";" //
265
+ + ext + ";" //
266
+ + input + ";" //
267
+ + kind + ";" //
268
+ + provenance
269
+ )
270
+ }
271
+
234
272
/** Holds if a summary model exists for the given parameters. */
235
273
predicate summaryModel (
236
274
string namespace , string type , boolean subtypes , string name , string signature , string ext ,
237
275
string input , string output , string kind , string provenance
238
276
) {
239
277
exists ( string row |
240
- summaryModel ( row ) and
278
+ summaryModelInternal ( row ) and
241
279
row .splitAt ( ";" , 0 ) = namespace and
242
280
row .splitAt ( ";" , 1 ) = type and
243
281
row .splitAt ( ";" , 2 ) = subtypes .toString ( ) and
@@ -252,12 +290,33 @@ predicate summaryModel(
252
290
)
253
291
}
254
292
293
+ /** Holds if `row` is a summary model. */
294
+ predicate summaryModel ( string row ) {
295
+ exists (
296
+ string namespace , string type , boolean subtypes , string name , string signature , string ext ,
297
+ string input , string output , string kind , string provenance
298
+ |
299
+ summaryModel ( namespace , type , subtypes , name , signature , ext , input , output , kind , provenance ) and
300
+ row =
301
+ namespace + ";" //
302
+ + type + ";" //
303
+ + subtypes .toString ( ) + ";" //
304
+ + name + ";" //
305
+ + signature + ";" //
306
+ + ext + ";" //
307
+ + input + ";" //
308
+ + output + ";" //
309
+ + kind + ";" //
310
+ + provenance
311
+ )
312
+ }
313
+
255
314
/** Holds if a summary model exists indicating there is no flow for the given parameters. */
256
315
predicate negativeSummaryModel (
257
316
string namespace , string type , string name , string signature , string provenance
258
317
) {
259
318
exists ( string row |
260
- negativeSummaryModel ( row ) and
319
+ negativeSummaryModelInternal ( row ) and
261
320
row .splitAt ( ";" , 0 ) = namespace and
262
321
row .splitAt ( ";" , 1 ) = type and
263
322
row .splitAt ( ";" , 2 ) = name and
@@ -266,6 +325,19 @@ predicate negativeSummaryModel(
266
325
)
267
326
}
268
327
328
+ /** Holds if `row` is a negative summary model. */
329
+ predicate negativeSummaryModel ( string row ) {
330
+ exists ( string namespace , string type , string name , string signature , string provenance |
331
+ negativeSummaryModel ( namespace , type , name , signature , provenance ) and
332
+ row =
333
+ namespace + ";" //
334
+ + type + ";" //
335
+ + name + ";" //
336
+ + signature + ";" //
337
+ + provenance
338
+ )
339
+ }
340
+
269
341
private predicate relevantNamespace ( string namespace ) {
270
342
sourceModel ( namespace , _, _, _, _, _, _, _, _) or
271
343
sinkModel ( namespace , _, _, _, _, _, _, _, _) or
@@ -355,33 +427,30 @@ module CsvValidation {
355
427
}
356
428
357
429
private string getInvalidModelKind ( ) {
358
- exists ( string row , string kind | summaryModel ( row ) |
359
- kind = row .splitAt ( ";" , 8 ) and
430
+ exists ( string kind | summaryModel ( _, _, _, _, _, _, _, _, kind , _) |
360
431
not kind = [ "taint" , "value" ] and
361
432
result = "Invalid kind \"" + kind + "\" in summary model."
362
433
)
363
434
or
364
- exists ( string row , string kind | sinkModel ( row ) |
365
- kind = row .splitAt ( ";" , 7 ) and
435
+ exists ( string kind | sinkModel ( _, _, _, _, _, _, _, kind , _) |
366
436
not kind = [ "code" , "sql" , "xss" , "remote" , "html" ] and
367
437
not kind .matches ( "encryption-%" ) and
368
438
result = "Invalid kind \"" + kind + "\" in sink model."
369
439
)
370
440
or
371
- exists ( string row , string kind | sourceModel ( row ) |
372
- kind = row .splitAt ( ";" , 7 ) and
441
+ exists ( string kind | sourceModel ( _, _, _, _, _, _, _, kind , _) |
373
442
not kind = [ "local" , "file" ] and
374
443
result = "Invalid kind \"" + kind + "\" in source model."
375
444
)
376
445
}
377
446
378
447
private string getInvalidModelSubtype ( ) {
379
448
exists ( string pred , string row |
380
- sourceModel ( row ) and pred = "source"
449
+ sourceModelInternal ( row ) and pred = "source"
381
450
or
382
- sinkModel ( row ) and pred = "sink"
451
+ sinkModelInternal ( row ) and pred = "sink"
383
452
or
384
- summaryModel ( row ) and pred = "summary"
453
+ summaryModelInternal ( row ) and pred = "summary"
385
454
|
386
455
exists ( string b |
387
456
b = row .splitAt ( ";" , 2 ) and
@@ -393,13 +462,13 @@ module CsvValidation {
393
462
394
463
private string getInvalidModelColumnCount ( ) {
395
464
exists ( string pred , string row , int expect |
396
- sourceModel ( row ) and expect = 9 and pred = "source"
465
+ sourceModelInternal ( row ) and expect = 9 and pred = "source"
397
466
or
398
- sinkModel ( row ) and expect = 9 and pred = "sink"
467
+ sinkModelInternal ( row ) and expect = 9 and pred = "sink"
399
468
or
400
- summaryModel ( row ) and expect = 10 and pred = "summary"
469
+ summaryModelInternal ( row ) and expect = 10 and pred = "summary"
401
470
or
402
- negativeSummaryModel ( row ) and expect = 5 and pred = "negative summary"
471
+ negativeSummaryModelInternal ( row ) and expect = 5 and pred = "negative summary"
403
472
|
404
473
exists ( int cols |
405
474
cols = 1 + max ( int n | exists ( row .splitAt ( ";" , n ) ) ) and
0 commit comments