@@ -3936,40 +3936,6 @@ module Impl<FullStateConfigSig Config> {
3936
3936
}
3937
3937
}
3938
3938
3939
- private newtype TRevPartialAccessPath =
3940
- TRevPartialNil ( ) or
3941
- TRevPartialCons ( Content c , int len ) { len in [ 1 .. accessPathLimit ( ) ] }
3942
-
3943
- /**
3944
- * Conceptually a list of `Content`s, but only the first
3945
- * element of the list and its length are tracked.
3946
- */
3947
- private class RevPartialAccessPath extends TRevPartialAccessPath {
3948
- abstract string toString ( ) ;
3949
-
3950
- Content getHead ( ) { this = TRevPartialCons ( result , _) }
3951
-
3952
- int len ( ) {
3953
- this = TRevPartialNil ( ) and result = 0
3954
- or
3955
- this = TRevPartialCons ( _, result )
3956
- }
3957
- }
3958
-
3959
- private class RevPartialAccessPathNil extends RevPartialAccessPath , TRevPartialNil {
3960
- override string toString ( ) { result = "" }
3961
- }
3962
-
3963
- private class RevPartialAccessPathCons extends RevPartialAccessPath , TRevPartialCons {
3964
- override string toString ( ) {
3965
- exists ( Content c , int len | this = TRevPartialCons ( c , len ) |
3966
- if len = 1
3967
- then result = "[" + c .toString ( ) + "]"
3968
- else result = "[" + c .toString ( ) + ", ... (" + len .toString ( ) + ")]"
3969
- )
3970
- }
3971
- }
3972
-
3973
3939
private predicate relevantState ( FlowState state ) {
3974
3940
sourceNode ( _, state ) or
3975
3941
sinkNode ( _, state ) or
@@ -4005,7 +3971,7 @@ module Impl<FullStateConfigSig Config> {
4005
3971
4006
3972
private newtype TRevSummaryCtx3 =
4007
3973
TRevSummaryCtx3None ( ) or
4008
- TRevSummaryCtx3Some ( RevPartialAccessPath ap )
3974
+ TRevSummaryCtx3Some ( PartialAccessPath ap )
4009
3975
4010
3976
private newtype TPartialPathNode =
4011
3977
TPartialPathNodeFwd (
@@ -4027,13 +3993,13 @@ module Impl<FullStateConfigSig Config> {
4027
3993
} or
4028
3994
TPartialPathNodeRev (
4029
3995
NodeEx node , FlowState state , TRevSummaryCtx1 sc1 , TRevSummaryCtx2 sc2 , TRevSummaryCtx3 sc3 ,
4030
- RevPartialAccessPath ap
3996
+ PartialAccessPath ap
4031
3997
) {
4032
3998
sinkNode ( node , state ) and
4033
3999
sc1 = TRevSummaryCtx1None ( ) and
4034
4000
sc2 = TRevSummaryCtx2None ( ) and
4035
4001
sc3 = TRevSummaryCtx3None ( ) and
4036
- ap = TRevPartialNil ( ) and
4002
+ ap = TPartialNil ( ) and
4037
4003
exists ( explorationLimit ( ) )
4038
4004
or
4039
4005
revPartialPathStep ( _, node , state , sc1 , sc2 , sc3 , ap ) and
@@ -4208,7 +4174,7 @@ module Impl<FullStateConfigSig Config> {
4208
4174
TRevSummaryCtx1 sc1 ;
4209
4175
TRevSummaryCtx2 sc2 ;
4210
4176
TRevSummaryCtx3 sc3 ;
4211
- RevPartialAccessPath ap ;
4177
+ PartialAccessPath ap ;
4212
4178
4213
4179
PartialPathNodeRev ( ) { this = TPartialPathNodeRev ( node , state , sc1 , sc2 , sc3 , ap ) }
4214
4180
@@ -4222,7 +4188,7 @@ module Impl<FullStateConfigSig Config> {
4222
4188
4223
4189
TRevSummaryCtx3 getSummaryCtx3 ( ) { result = sc3 }
4224
4190
4225
- RevPartialAccessPath getAp ( ) { result = ap }
4191
+ PartialAccessPath getAp ( ) { result = ap }
4226
4192
4227
4193
override PartialPathNodeRev getASuccessor ( ) {
4228
4194
revPartialPathStep ( result , this .getNodeEx ( ) , this .getState ( ) , this .getSummaryCtx1 ( ) ,
@@ -4234,7 +4200,7 @@ module Impl<FullStateConfigSig Config> {
4234
4200
sc1 = TRevSummaryCtx1None ( ) and
4235
4201
sc2 = TRevSummaryCtx2None ( ) and
4236
4202
sc3 = TRevSummaryCtx3None ( ) and
4237
- ap = TRevPartialNil ( )
4203
+ ap = TPartialNil ( )
4238
4204
}
4239
4205
}
4240
4206
@@ -4501,7 +4467,7 @@ module Impl<FullStateConfigSig Config> {
4501
4467
pragma [ nomagic]
4502
4468
private predicate revPartialPathStep (
4503
4469
PartialPathNodeRev mid , NodeEx node , FlowState state , TRevSummaryCtx1 sc1 ,
4504
- TRevSummaryCtx2 sc2 , TRevSummaryCtx3 sc3 , RevPartialAccessPath ap
4470
+ TRevSummaryCtx2 sc2 , TRevSummaryCtx3 sc3 , PartialAccessPath ap
4505
4471
) {
4506
4472
localFlowStepEx ( node , mid .getNodeEx ( ) ) and
4507
4473
state = mid .getState ( ) and
@@ -4515,15 +4481,15 @@ module Impl<FullStateConfigSig Config> {
4515
4481
sc1 = mid .getSummaryCtx1 ( ) and
4516
4482
sc2 = mid .getSummaryCtx2 ( ) and
4517
4483
sc3 = mid .getSummaryCtx3 ( ) and
4518
- mid .getAp ( ) instanceof RevPartialAccessPathNil and
4519
- ap = TRevPartialNil ( )
4484
+ mid .getAp ( ) instanceof PartialAccessPathNil and
4485
+ ap = TPartialNil ( )
4520
4486
or
4521
4487
additionalLocalStateStep ( node , state , mid .getNodeEx ( ) , mid .getState ( ) ) and
4522
4488
sc1 = mid .getSummaryCtx1 ( ) and
4523
4489
sc2 = mid .getSummaryCtx2 ( ) and
4524
4490
sc3 = mid .getSummaryCtx3 ( ) and
4525
- mid .getAp ( ) instanceof RevPartialAccessPathNil and
4526
- ap = TRevPartialNil ( )
4491
+ mid .getAp ( ) instanceof PartialAccessPathNil and
4492
+ ap = TPartialNil ( )
4527
4493
or
4528
4494
jumpStepEx ( node , mid .getNodeEx ( ) ) and
4529
4495
state = mid .getState ( ) and
@@ -4537,23 +4503,23 @@ module Impl<FullStateConfigSig Config> {
4537
4503
sc1 = TRevSummaryCtx1None ( ) and
4538
4504
sc2 = TRevSummaryCtx2None ( ) and
4539
4505
sc3 = TRevSummaryCtx3None ( ) and
4540
- mid .getAp ( ) instanceof RevPartialAccessPathNil and
4541
- ap = TRevPartialNil ( )
4506
+ mid .getAp ( ) instanceof PartialAccessPathNil and
4507
+ ap = TPartialNil ( )
4542
4508
or
4543
4509
additionalJumpStateStep ( node , state , mid .getNodeEx ( ) , mid .getState ( ) ) and
4544
4510
sc1 = TRevSummaryCtx1None ( ) and
4545
4511
sc2 = TRevSummaryCtx2None ( ) and
4546
4512
sc3 = TRevSummaryCtx3None ( ) and
4547
- mid .getAp ( ) instanceof RevPartialAccessPathNil and
4548
- ap = TRevPartialNil ( )
4513
+ mid .getAp ( ) instanceof PartialAccessPathNil and
4514
+ ap = TPartialNil ( )
4549
4515
or
4550
4516
revPartialPathReadStep ( mid , _, _, node , ap ) and
4551
4517
state = mid .getState ( ) and
4552
4518
sc1 = mid .getSummaryCtx1 ( ) and
4553
4519
sc2 = mid .getSummaryCtx2 ( ) and
4554
4520
sc3 = mid .getSummaryCtx3 ( )
4555
4521
or
4556
- exists ( RevPartialAccessPath ap0 , Content c |
4522
+ exists ( PartialAccessPath ap0 , Content c |
4557
4523
revPartialPathStoreStep ( mid , ap0 , c , node ) and
4558
4524
state = mid .getState ( ) and
4559
4525
sc1 = mid .getSummaryCtx1 ( ) and
@@ -4588,8 +4554,8 @@ module Impl<FullStateConfigSig Config> {
4588
4554
4589
4555
pragma [ inline]
4590
4556
private predicate revPartialPathReadStep (
4591
- PartialPathNodeRev mid , RevPartialAccessPath ap1 , Content c , NodeEx node ,
4592
- RevPartialAccessPath ap2
4557
+ PartialPathNodeRev mid , PartialAccessPath ap1 , Content c , NodeEx node ,
4558
+ PartialAccessPath ap2
4593
4559
) {
4594
4560
exists ( NodeEx midNode |
4595
4561
midNode = mid .getNodeEx ( ) and
@@ -4601,13 +4567,13 @@ module Impl<FullStateConfigSig Config> {
4601
4567
}
4602
4568
4603
4569
pragma [ nomagic]
4604
- private predicate apConsRev ( RevPartialAccessPath ap1 , Content c , RevPartialAccessPath ap2 ) {
4570
+ private predicate apConsRev ( PartialAccessPath ap1 , Content c , PartialAccessPath ap2 ) {
4605
4571
revPartialPathReadStep ( _, ap1 , c , _, ap2 )
4606
4572
}
4607
4573
4608
4574
pragma [ nomagic]
4609
4575
private predicate revPartialPathStoreStep (
4610
- PartialPathNodeRev mid , RevPartialAccessPath ap , Content c , NodeEx node
4576
+ PartialPathNodeRev mid , PartialAccessPath ap , Content c , NodeEx node
4611
4577
) {
4612
4578
exists ( NodeEx midNode |
4613
4579
midNode = mid .getNodeEx ( ) and
@@ -4620,7 +4586,7 @@ module Impl<FullStateConfigSig Config> {
4620
4586
pragma [ nomagic]
4621
4587
private predicate revPartialPathIntoReturn (
4622
4588
PartialPathNodeRev mid , ReturnPosition pos , FlowState state , TRevSummaryCtx1Some sc1 ,
4623
- TRevSummaryCtx2Some sc2 , TRevSummaryCtx3Some sc3 , DataFlowCall call , RevPartialAccessPath ap
4589
+ TRevSummaryCtx2Some sc2 , TRevSummaryCtx3Some sc3 , DataFlowCall call , PartialAccessPath ap
4624
4590
) {
4625
4591
exists ( NodeEx out |
4626
4592
mid .getNodeEx ( ) = out and
@@ -4636,7 +4602,7 @@ module Impl<FullStateConfigSig Config> {
4636
4602
pragma [ nomagic]
4637
4603
private predicate revPartialPathFlowsThrough (
4638
4604
ArgumentPosition apos , FlowState state , TRevSummaryCtx1Some sc1 , TRevSummaryCtx2Some sc2 ,
4639
- TRevSummaryCtx3Some sc3 , RevPartialAccessPath ap
4605
+ TRevSummaryCtx3Some sc3 , PartialAccessPath ap
4640
4606
) {
4641
4607
exists ( PartialPathNodeRev mid , ParamNodeEx p , ParameterPosition ppos |
4642
4608
mid .getNodeEx ( ) = p and
@@ -4653,7 +4619,7 @@ module Impl<FullStateConfigSig Config> {
4653
4619
pragma [ nomagic]
4654
4620
private predicate revPartialPathThroughCallable0 (
4655
4621
DataFlowCall call , PartialPathNodeRev mid , ArgumentPosition pos , FlowState state ,
4656
- RevPartialAccessPath ap
4622
+ PartialAccessPath ap
4657
4623
) {
4658
4624
exists ( TRevSummaryCtx1Some sc1 , TRevSummaryCtx2Some sc2 , TRevSummaryCtx3Some sc3 |
4659
4625
revPartialPathIntoReturn ( mid , _, _, sc1 , sc2 , sc3 , call , _) and
@@ -4663,7 +4629,7 @@ module Impl<FullStateConfigSig Config> {
4663
4629
4664
4630
pragma [ nomagic]
4665
4631
private predicate revPartialPathThroughCallable (
4666
- PartialPathNodeRev mid , ArgNodeEx node , FlowState state , RevPartialAccessPath ap
4632
+ PartialPathNodeRev mid , ArgNodeEx node , FlowState state , PartialAccessPath ap
4667
4633
) {
4668
4634
exists ( DataFlowCall call , ArgumentPosition pos |
4669
4635
revPartialPathThroughCallable0 ( call , mid , pos , state , ap ) and
0 commit comments