@@ -98,11 +98,17 @@ private cached newtype HCBase =
98
98
mk_MemberFunctionCall ( trg , qual , args , _)
99
99
}
100
100
or
101
- HC_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align ) {
102
- mk_NewExpr ( t , alloc , init , align , _, _)
103
- } or
104
- HC_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align ) {
105
- mk_NewArrayExpr ( t , alloc , init , align , _, _)
101
+ // Hack to get around argument 0 of allocator calls being an error expression
102
+ HC_AllocatorArgZero ( Type t ) {
103
+ mk_AllocatorArgZero ( t , _)
104
+ }
105
+ or
106
+ HC_NewExpr ( Type t , HC_Alloc alloc , HC_Init init ) {
107
+ mk_NewExpr ( t , alloc , init , _)
108
+ }
109
+ or
110
+ HC_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Extent extent , HC_Init init ) {
111
+ mk_NewArrayExpr ( t , alloc , extent , init , _)
106
112
}
107
113
or
108
114
HC_SizeofType ( Type t ) { mk_SizeofType ( t , _) }
@@ -147,30 +153,27 @@ private cached newtype HCBase =
147
153
// given a unique number based on the expression itself.
148
154
HC_Unanalyzable ( Expr e ) { not analyzableExpr ( e , _) }
149
155
150
- /** Used to implement hash-consing of `new` placement argument lists */
151
- private newtype HC_Alloc =
152
- HC_EmptyAllocArgs ( Function fcn ) {
153
- exists ( NewOrNewArrayExpr n |
154
- n .getAllocator ( ) = fcn
155
- )
156
- }
157
- or HC_AllocArgCons ( Function fcn , HashCons hc , int i , HC_Alloc list , boolean aligned ) {
158
- mk_AllocArgCons ( fcn , hc , i , list , aligned , _)
159
- }
160
- or
161
- HC_NoAlloc ( )
162
-
163
156
/** Used to implement optional init on `new` expressions */
164
157
private newtype HC_Init =
165
158
HC_NoInit ( )
166
159
or
167
160
HC_HasInit ( HashCons hc ) { mk_HasInit ( hc , _) }
168
161
169
- private newtype HC_Align =
170
- HC_NoAlign ( )
162
+ /**
163
+ * Used to implement optional allocator call on `new` expressions
164
+ */
165
+ private newtype HC_Alloc =
166
+ HC_NoAlloc ( )
171
167
or
172
- HC_HasAlign ( HashCons hc ) { mk_HasAlign ( hc , _) }
173
-
168
+ HC_HasAlloc ( HashCons hc ) { mk_HasAlloc ( hc , _) }
169
+
170
+ /**
171
+ * Used to implement optional extent expression on `new[]` exprtessions
172
+ */
173
+ private newtype HC_Extent =
174
+ HC_NoExtent ( )
175
+ or
176
+ HC_HasExtent ( HashCons hc ) { mk_HasExtent ( hc , _) }
174
177
/** Used to implement hash-consing of argument lists */
175
178
private newtype HC_Args =
176
179
HC_EmptyArgs ( ) {
@@ -260,6 +263,7 @@ class HashCons extends HCBase {
260
263
if this instanceof HC_ExprCall then result = "ExprCall" else
261
264
if this instanceof HC_ConditionalExpr then result = "ConditionalExpr" else
262
265
if this instanceof HC_NoExceptExpr then result = "NoExceptExpr" else
266
+ if this instanceof HC_AllocatorArgZero then result = "AllocatorArgZero" else
263
267
result = "error"
264
268
}
265
269
@@ -563,145 +567,92 @@ private predicate mk_ArgConsInner(HashCons head, HC_Args tail, int i, HC_Args li
563
567
mk_ArgCons ( head , i , tail , c )
564
568
}
565
569
566
- /**
567
- * Holds if `fc` is a call to `fcn`, `fc`'s first `i` arguments have hash-cons
568
- * `list`, and `fc`'s argument at index `i` has hash-cons `hc`.
570
+ /*
571
+ * The 0th argument of an allocator call in a new expression is always an error expression;
572
+ * this works around it
569
573
*/
570
- private predicate mk_AllocArgCons ( Function fcn , HashCons hc , int i , HC_Alloc list , boolean aligned ,
571
- Call c ) {
572
- analyzableCall ( c ) and
573
- c .getTarget ( ) = fcn and
574
- hc = hashCons ( c .getArgument ( i ) .getFullyConverted ( ) ) and
575
- (
576
- exists ( HashCons head , HC_Alloc tail |
577
- list = HC_AllocArgCons ( fcn , head , i - 1 , tail , aligned ) and
578
- mk_AllocArgCons ( fcn , head , i - 1 , tail , aligned , c ) and
579
- (
580
- aligned = true and
581
- i > 2
582
- or
583
- aligned = false and
584
- i > 1
585
- )
586
- )
587
- or
588
- (
589
- aligned = true and
590
- i = 2
591
- or
592
- aligned = false and
593
- i = 1
594
- ) and
595
- list = HC_EmptyAllocArgs ( fcn )
574
+ private predicate analyzableAllocatorArgZero ( ErrorExpr e ) {
575
+ exists ( NewOrNewArrayExpr new |
576
+ new .getAllocatorCall ( ) .getChild ( 0 ) = e
577
+ )
578
+ }
579
+
580
+ private predicate mk_AllocatorArgZero ( Type t , ErrorExpr e ) {
581
+ exists ( NewOrNewArrayExpr new |
582
+ new .getAllocatorCall ( ) .getChild ( 0 ) = e and
583
+ t = new .getType ( ) .getUnspecifiedType ( )
596
584
)
597
585
}
598
586
599
587
private predicate mk_HasInit ( HashCons hc , NewOrNewArrayExpr new ) {
600
- hc = hashCons ( new .( NewExpr ) .getInitializer ( ) ) or
601
- hc = hashCons ( new .( NewArrayExpr ) .getInitializer ( ) )
588
+ hc = hashCons ( new .( NewExpr ) .getInitializer ( ) . getFullyConverted ( ) ) or
589
+ hc = hashCons ( new .( NewArrayExpr ) .getInitializer ( ) . getFullyConverted ( ) )
602
590
}
603
591
604
- private predicate mk_HasAlign ( HashCons hc , NewOrNewArrayExpr new ) {
605
- hc = hashCons ( new .getAlignmentArgument ( ) .getFullyConverted ( ) )
592
+ private predicate mk_HasAlloc ( HashCons hc , NewOrNewArrayExpr new ) {
593
+ hc = hashCons ( new .( NewExpr ) .getAllocatorCall ( ) .getFullyConverted ( ) ) or
594
+ hc = hashCons ( new .( NewArrayExpr ) .getAllocatorCall ( ) .getFullyConverted ( ) )
595
+ }
596
+
597
+ private predicate mk_HasExtent ( HashCons hc , NewArrayExpr new ) {
598
+ hc = hashCons ( new .( NewArrayExpr ) .getExtent ( ) .getFullyConverted ( ) )
606
599
}
607
600
608
601
private predicate analyzableNewExpr ( NewExpr new ) {
609
- strictcount ( new .getAllocatedType ( ) ) = 1 and
602
+ strictcount ( new .getAllocatedType ( ) . getUnspecifiedType ( ) ) = 1 and
610
603
count ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) <= 1 and
611
604
count ( new .getInitializer ( ) .getFullyConverted ( ) ) <= 1
612
605
}
613
606
614
- private predicate mk_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align , boolean aligned ,
615
- NewExpr new ) {
607
+ private predicate mk_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , NewExpr new ) {
616
608
analyzableNewExpr ( new ) and
617
- t = new .getAllocatedType ( ) and
609
+ t = new .getAllocatedType ( ) . getUnspecifiedType ( ) and
618
610
(
619
- align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) .getFullyConverted ( ) ) ) and
620
- aligned = true
621
- or
622
- not new .hasAlignedAllocation ( ) and
623
- align = HC_NoAlign ( ) and
624
- aligned = false
625
- )
626
- and
627
- (
628
- exists ( FunctionCall fc , HashCons head , HC_Alloc tail |
629
- fc = new .getAllocatorCall ( ) and
630
- alloc = HC_AllocArgCons ( fc .getTarget ( ) , head , fc .getNumberOfArguments ( ) - 1 , tail , aligned ) and
631
- mk_AllocArgCons ( fc .getTarget ( ) , head , fc .getNumberOfArguments ( ) - 1 , tail , aligned , fc )
632
- )
633
- or
634
- exists ( FunctionCall fc |
635
- fc = new .getAllocatorCall ( ) and
636
- (
637
- aligned = true and
638
- fc .getNumberOfArguments ( ) = 2
639
- or
640
- aligned = false and
641
- fc .getNumberOfArguments ( ) = 1
642
- ) and
643
- alloc = HC_EmptyAllocArgs ( fc .getTarget ( ) )
644
- )
611
+ alloc = HC_HasAlloc ( hashCons ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) )
645
612
or
646
- not exists ( new .getAllocatorCall ( ) ) and
613
+ not exists ( new .getAllocatorCall ( ) . getFullyConverted ( ) ) and
647
614
alloc = HC_NoAlloc ( )
648
615
)
649
616
and
650
617
(
651
- init = HC_HasInit ( hashCons ( new .getInitializer ( ) ) )
618
+ init = HC_HasInit ( hashCons ( new .getInitializer ( ) . getFullyConverted ( ) ) )
652
619
or
653
- not exists ( new .getInitializer ( ) ) and
620
+ not exists ( new .getInitializer ( ) . getFullyConverted ( ) ) and
654
621
init = HC_NoInit ( )
655
622
)
656
623
}
657
624
658
625
private predicate analyzableNewArrayExpr ( NewArrayExpr new ) {
659
626
strictcount ( new .getAllocatedType ( ) .getUnspecifiedType ( ) ) = 1 and
660
627
count ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) <= 1 and
661
- count ( new .getInitializer ( ) .getFullyConverted ( ) ) <= 1
628
+ count ( new .getInitializer ( ) .getFullyConverted ( ) ) <= 1 and
629
+ count ( new .( NewArrayExpr ) .getExtent ( ) .getFullyConverted ( ) ) <= 1
662
630
}
663
631
664
- private predicate mk_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align ,
665
- boolean aligned , NewArrayExpr new ) {
632
+ private predicate mk_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Extent extent , HC_Init init , NewArrayExpr new ) {
666
633
analyzableNewArrayExpr ( new ) and
667
634
t = new .getAllocatedType ( ) and
635
+
668
636
(
669
- align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) .getFullyConverted ( ) ) ) and
670
- aligned = true
637
+ alloc = HC_HasAlloc ( hashCons ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) )
671
638
or
672
- not new .hasAlignedAllocation ( ) and
673
- align = HC_NoAlign ( ) and
674
- aligned = false
639
+ not exists ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) and
640
+ alloc = HC_NoAlloc ( )
675
641
)
676
642
and
677
643
(
678
- exists ( FunctionCall fc , HashCons head , HC_Alloc tail |
679
- fc = new .getAllocatorCall ( ) and
680
- alloc = HC_AllocArgCons ( fc .getTarget ( ) , head , fc .getNumberOfArguments ( ) - 1 , tail , aligned ) and
681
- mk_AllocArgCons ( fc .getTarget ( ) , head , fc .getNumberOfArguments ( ) - 1 , tail , aligned , fc )
682
- )
683
- or
684
- exists ( FunctionCall fc |
685
- fc = new .getAllocatorCall ( ) and
686
- (
687
- aligned = true and
688
- fc .getNumberOfArguments ( ) = 2
689
- or
690
- aligned = false and
691
- fc .getNumberOfArguments ( ) = 1
692
- ) and
693
- alloc = HC_EmptyAllocArgs ( fc .getTarget ( ) )
694
- )
644
+ init = HC_HasInit ( hashCons ( new .getInitializer ( ) .getFullyConverted ( ) ) )
695
645
or
696
- not exists ( new .getAllocatorCall ( ) ) and
697
- alloc = HC_NoAlloc ( )
646
+ not exists ( new .getInitializer ( ) . getFullyConverted ( ) ) and
647
+ init = HC_NoInit ( )
698
648
)
699
649
and
650
+
700
651
(
701
- init = HC_HasInit ( hashCons ( new .getInitializer ( ) ) )
652
+ extent = HC_HasExtent ( hashCons ( new .getExtent ( ) . getFullyConverted ( ) ) )
702
653
or
703
- not exists ( new .getInitializer ( ) ) and
704
- init = HC_NoInit ( )
654
+ not exists ( new .getExtent ( ) . getFullyConverted ( ) ) and
655
+ extent = HC_NoExtent ( )
705
656
)
706
657
}
707
658
@@ -984,14 +935,20 @@ cached HashCons hashCons(Expr e) {
984
935
result = HC_MemberFunctionCall ( fcn , qual , args )
985
936
)
986
937
or
987
- exists ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align , boolean aligned
988
- | mk_NewExpr ( t , alloc , init , align , aligned , e ) and
989
- result = HC_NewExpr ( t , alloc , init , align )
938
+ // works around an extractor issue class
939
+ exists ( Type t
940
+ | mk_AllocatorArgZero ( t , e ) and
941
+ result = HC_AllocatorArgZero ( t )
942
+ )
943
+ or
944
+ exists ( Type t , HC_Alloc alloc , HC_Init init
945
+ | mk_NewExpr ( t , alloc , init , e ) and
946
+ result = HC_NewExpr ( t , alloc , init )
990
947
)
991
948
or
992
- exists ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align , boolean aligned
993
- | mk_NewArrayExpr ( t , alloc , init , align , aligned , e ) and
994
- result = HC_NewArrayExpr ( t , alloc , init , align )
949
+ exists ( Type t , HC_Alloc alloc , HC_Extent extent , HC_Init init
950
+ | mk_NewArrayExpr ( t , alloc , extent , init , e ) and
951
+ result = HC_NewArrayExpr ( t , alloc , extent , init )
995
952
)
996
953
or
997
954
exists ( Type t
@@ -1108,5 +1065,6 @@ predicate analyzableExpr(Expr e, string kind) {
1108
1065
( analyzableThrowExpr ( e ) and kind = "ThrowExpr" ) or
1109
1066
( analyzableReThrowExpr ( e ) and kind = "ReThrowExpr" ) or
1110
1067
( analyzableConditionalExpr ( e ) and kind = "ConditionalExpr" ) or
1111
- ( analyzableNoExceptExpr ( e ) and kind = "NoExceptExpr" )
1068
+ ( analyzableNoExceptExpr ( e ) and kind = "NoExceptExpr" ) or
1069
+ ( analyzableAllocatorArgZero ( e ) and kind = "AllocatorArgZero" )
1112
1070
}
0 commit comments