1
+ signature string getJsonSig ( ) ;
1
2
2
- signature class JsonStringReader {
3
- string read ( ) ;
4
- }
5
-
6
- module JsonParser< JsonStringReader Reader> {
3
+ module JsonParser< getJsonSig / 0 getJson> {
7
4
private newtype TJsonToken =
8
5
MkLeftBracketToken ( int begin , int end , string value , string source ) {
9
- source = any ( Reader r ) . read ( ) and
6
+ source = getJson ( ) and
10
7
begin = source .indexOf ( "{" ) and
11
8
begin = end and
12
9
value = "{"
13
10
} or
14
11
MkRightBracketToken ( int begin , int end , string value , string source ) {
15
- source = any ( Reader r ) . read ( ) and
12
+ source = getJson ( ) and
16
13
begin = source .indexOf ( "}" ) and
17
14
begin = end and
18
15
value = "}"
19
16
} or
20
17
MkLeftSquareBracketToken ( int begin , int end , string value , string source ) {
21
- source = any ( Reader r ) . read ( ) and
18
+ source = getJson ( ) and
22
19
begin = source .indexOf ( "[" ) and
23
20
begin = end and
24
21
value = "["
25
22
} or
26
23
MkRightSquareBracketToken ( int begin , int end , string value , string source ) {
27
- source = any ( Reader r ) . read ( ) and
24
+ source = getJson ( ) and
28
25
begin = source .indexOf ( "]" ) and
29
26
begin = end and
30
27
value = "]"
31
28
} or
32
29
MkWhiteSpaceToken ( int begin , int end , string value , string source ) {
33
- source = any ( Reader r ) . read ( ) and
30
+ source = getJson ( ) and
34
31
value = source .regexpFind ( "[\\s\\v\\h]" , _, begin ) and
35
32
begin + value .length ( ) - 1 = end
36
33
} or
37
34
MkCommaToken ( int begin , int end , string value , string source ) {
38
- source = any ( Reader r ) . read ( ) and
35
+ source = getJson ( ) and
39
36
begin = source .indexOf ( "," ) and
40
37
begin = end and
41
38
value = ","
42
39
} or
43
40
MkColonToken ( int begin , int end , string value , string source ) {
44
- source = any ( Reader r ) . read ( ) and
41
+ source = getJson ( ) and
45
42
begin = source .indexOf ( ":" ) and
46
43
begin = end and
47
44
value = ":"
48
45
} or
49
46
MkNumberToken ( int begin , int end , string value , string source ) {
50
- source = any ( Reader r ) . read ( ) and
47
+ source = getJson ( ) and
51
48
value = source .regexpFind ( "-?[1-9]\\d*(\\.\\d+)?((e|E)?(\\+|-)?\\d+)?" , _, begin ) and
52
49
begin + value .length ( ) - 1 = end
53
50
} or
54
51
MkStringToken ( int begin , int end , string value , string source ) {
55
- source = any ( Reader r ) . read ( ) and
52
+ source = getJson ( ) and
56
53
value = source .regexpFind ( "\"[^\"]*\"" , _, begin ) and
57
54
begin + value .length ( ) - 1 = end
58
55
} or
59
56
MkTrueToken ( int begin , int end , string value , string source ) {
60
- source = any ( Reader r ) . read ( ) and
57
+ source = getJson ( ) and
61
58
value = source .regexpFind ( "true" , _, begin ) and
62
59
begin + value .length ( ) - 1 = end
63
60
} or
64
61
MkFalseToken ( int begin , int end , string value , string source ) {
65
- source = any ( Reader r ) . read ( ) and
62
+ source = getJson ( ) and
66
63
value = source .regexpFind ( "false" , _, begin ) and
67
64
begin + value .length ( ) - 1 = end
68
65
} or
69
66
MkNullToken ( int begin , int end , string value , string source ) {
70
- source = any ( Reader r ) . read ( ) and
67
+ source = getJson ( ) and
71
68
value = source .regexpFind ( "null" , _, begin ) and
72
69
begin + value .length ( ) - 1 = end
73
70
}
@@ -382,96 +379,128 @@ module JsonParser<JsonStringReader Reader> {
382
379
}
383
380
384
381
private newtype TJsonValue =
385
- MkJsonNumber ( float n ) {
386
- exists ( NumberToken t | t .getValue ( ) .toFloat ( ) = n | not any ( StringToken str ) .contains ( t ) )
382
+ MkJsonNumber ( float n , JsonToken source ) {
383
+ exists ( NumberToken t | t .getValue ( ) .toFloat ( ) = n and source = t |
384
+ not any ( StringToken str ) .contains ( t )
385
+ )
386
+ } or
387
+ MkJsonString ( string s , JsonToken source ) {
388
+ exists ( StringToken t | t .( JsonToken ) .getValue ( ) = s and t = source )
387
389
} or
388
- MkJsonString ( string s ) { exists ( StringToken t | t .( JsonToken ) .getValue ( ) = s ) } or
389
- MkJsonObject ( JsonMemberList members ) {
390
+ MkJsonObject ( JsonMemberList members , JsonToken source ) {
390
391
exists ( LeftBracketToken l , RightBracketToken r , JsonToken last |
391
392
getNextSkippingWhitespace ( l ) != r
392
393
|
393
394
mkJsonMembers ( getNextSkippingWhitespace ( l ) , members , last ) and
394
- getNextSkippingWhitespace ( last ) = r
395
+ getNextSkippingWhitespace ( last ) = r and
396
+ source = l
395
397
)
396
398
or
397
399
exists ( LeftBracketToken l , RightBracketToken r | getNextSkippingWhitespace ( l ) = r |
398
- members = EmtpyMemberList ( )
400
+ members = EmtpyMemberList ( ) and source = l
399
401
)
400
402
} or
401
- MkJsonArray ( JsonValueList values ) {
403
+ MkJsonArray ( JsonValueList values , JsonToken source ) {
402
404
exists ( LeftSquareBracketToken l , RightSquareBracketToken r , JsonToken last |
403
405
mkJsonValues ( getNextSkippingWhitespace ( l ) , values , last ) and
404
- getNextSkippingWhitespace ( last ) = r
406
+ getNextSkippingWhitespace ( last ) = r and
407
+ source = l
405
408
)
406
409
or
407
410
exists ( LeftSquareBracketToken l , RightSquareBracketToken r |
408
411
getNextSkippingWhitespace ( l ) = r
409
412
|
410
- values = EmtpyJsonValueList ( )
413
+ values = EmtpyJsonValueList ( ) and source = l
411
414
)
412
415
} or
413
- MkJsonTrue ( ) { exists ( TrueToken t | not any ( StringToken str ) .contains ( t ) ) } or
414
- MkJsonFalse ( ) { exists ( FalseToken t | not any ( StringToken str ) .contains ( t ) ) } or
415
- MkJsonNull ( ) { exists ( NullToken t | not any ( StringToken str ) .contains ( t ) ) }
416
+ MkJsonTrue ( JsonToken source ) {
417
+ exists ( TrueToken t | not any ( StringToken str ) .contains ( t ) and source = t )
418
+ } or
419
+ MkJsonFalse ( JsonToken source ) {
420
+ exists ( FalseToken t | not any ( StringToken str ) .contains ( t ) and source = t )
421
+ } or
422
+ MkJsonNull ( JsonToken source ) {
423
+ exists ( NullToken t | not any ( StringToken str ) .contains ( t ) and source = t )
424
+ }
416
425
417
426
private predicate mkJsonValue ( JsonToken first , JsonValue value , JsonToken last ) {
418
427
first instanceof StringToken and
419
428
first = last and
420
- value = MkJsonString ( first .getValue ( ) )
429
+ value = MkJsonString ( first .getValue ( ) , _ )
421
430
or
422
431
first instanceof NumberToken and
423
432
first = last and
424
- value = MkJsonNumber ( first .getValue ( ) .toFloat ( ) )
433
+ value = MkJsonNumber ( first .getValue ( ) .toFloat ( ) , _ )
425
434
or
426
435
first instanceof LeftBracketToken and
427
436
exists ( JsonMemberList members , JsonToken membersLast |
428
437
mkJsonMembers ( getNextSkippingWhitespace ( first ) , members , membersLast ) and
429
- value = MkJsonObject ( members ) and
438
+ value = MkJsonObject ( members , _ ) and
430
439
last = getNextSkippingWhitespace ( membersLast )
431
440
) and
432
441
last instanceof RightBracketToken
433
442
or
434
443
first instanceof LeftSquareBracketToken and
435
444
exists ( JsonValueList values , JsonToken valuesLast |
436
445
mkJsonValues ( getNextSkippingWhitespace ( first ) , values , valuesLast ) and
437
- value = MkJsonArray ( values ) and
446
+ value = MkJsonArray ( values , _ ) and
438
447
last = getNextSkippingWhitespace ( valuesLast )
439
448
) and
440
449
last instanceof RightSquareBracketToken
441
450
or
442
451
first instanceof TrueToken and
443
452
first = last and
444
- value = MkJsonTrue ( )
453
+ value = MkJsonTrue ( _ )
445
454
or
446
455
first instanceof FalseToken and
447
456
first = last and
448
- value = MkJsonFalse ( )
457
+ value = MkJsonFalse ( _ )
449
458
or
450
459
first instanceof NullToken and
451
460
first = last and
452
- value = MkJsonNull ( )
461
+ value = MkJsonNull ( _ )
453
462
}
454
463
455
464
class JsonValue extends TJsonValue {
456
465
string toString ( ) {
457
- this = MkJsonString ( result )
466
+ this = MkJsonString ( result , _ )
458
467
or
459
- exists ( float number | this = MkJsonNumber ( number ) | result = number .toString ( ) )
468
+ exists ( float number | this = MkJsonNumber ( number , _ ) | result = number .toString ( ) )
460
469
or
461
- exists ( JsonMemberList members | this = MkJsonObject ( members ) | result = members .toString ( ) )
470
+ exists ( JsonMemberList members | this = MkJsonObject ( members , _ ) | result = members .toString ( ) )
462
471
or
463
- exists ( JsonValueList values | this = MkJsonArray ( values ) | result = values .toString ( ) )
472
+ exists ( JsonValueList values | this = MkJsonArray ( values , _ ) | result = values .toString ( ) )
464
473
or
465
- this = MkJsonTrue ( ) and result = "true"
474
+ this = MkJsonTrue ( _ ) and result = "true"
466
475
or
467
- this = MkJsonFalse ( ) and result = "false"
476
+ this = MkJsonFalse ( _ ) and result = "false"
468
477
or
469
- this = MkJsonNull ( ) and result = "null"
478
+ this = MkJsonNull ( _) and result = "null"
479
+ }
480
+
481
+ string getSource ( ) {
482
+ exists ( JsonToken token |
483
+ this = MkJsonString ( _, token )
484
+ or
485
+ this = MkJsonNumber ( _, token )
486
+ or
487
+ this = MkJsonObject ( _, token )
488
+ or
489
+ this = MkJsonArray ( _, token )
490
+ or
491
+ this = MkJsonTrue ( token )
492
+ or
493
+ this = MkJsonFalse ( token )
494
+ or
495
+ this = MkJsonNull ( token )
496
+ |
497
+ result = token .getSource ( )
498
+ )
470
499
}
471
500
}
472
501
473
502
class JsonObject extends JsonValue , MkJsonObject {
474
- JsonMemberList getMembers ( ) { this = MkJsonObject ( result ) }
503
+ JsonMemberList getMembers ( ) { this = MkJsonObject ( result , _ ) }
475
504
476
505
JsonMember getMember ( int index ) { result = getMembers ( ) .getMember ( index ) }
477
506
@@ -483,19 +512,20 @@ module JsonParser<JsonStringReader Reader> {
483
512
class JsonNumber extends JsonValue , MkJsonNumber { }
484
513
485
514
class JsonArray extends JsonValue , MkJsonArray {
486
- JsonValueList getValues ( ) { this = MkJsonArray ( result ) }
515
+ JsonValueList getValues ( ) { this = MkJsonArray ( result , _ ) }
487
516
488
517
JsonValue getValue ( int index ) { result = getValues ( ) .getValue ( index ) }
489
518
490
519
JsonValue getAValue ( ) { result = getValue ( _) }
491
520
}
492
521
493
- JsonValue parse ( ) {
522
+ JsonValue parse ( string json ) {
523
+ result .getSource ( ) = json and
494
524
exists ( JsonToken firstToken |
495
- not any ( JsonToken t ) .getBegin ( ) < firstToken .getBegin ( ) and
496
- if firstToken instanceof WhiteSpaceToken
497
- then mkJsonValue ( getNextSkippingWhitespace ( firstToken ) , result , _)
498
- else mkJsonValue ( firstToken , result , _)
525
+ not any ( JsonToken t ) .getBegin ( ) < firstToken .getBegin ( ) and
526
+ if firstToken instanceof WhiteSpaceToken
527
+ then mkJsonValue ( getNextSkippingWhitespace ( firstToken ) , result , _)
528
+ else mkJsonValue ( firstToken , result , _)
499
529
)
500
530
}
501
- }
531
+ }
0 commit comments