@@ -98,11 +98,17 @@ private cached newtype HCBase =
9898 mk_MemberFunctionCall ( trg , qual , args , _)
9999 }
100100 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 , _)
106112 }
107113 or
108114 HC_SizeofType ( Type t ) { mk_SizeofType ( t , _) }
@@ -147,30 +153,27 @@ private cached newtype HCBase =
147153 // given a unique number based on the expression itself.
148154 HC_Unanalyzable ( Expr e ) { not analyzableExpr ( e , _) }
149155
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-
163156/** Used to implement optional init on `new` expressions */
164157private newtype HC_Init =
165158 HC_NoInit ( )
166159 or
167160 HC_HasInit ( HashCons hc ) { mk_HasInit ( hc , _) }
168161
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 ( )
171167 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 , _) }
174177/** Used to implement hash-consing of argument lists */
175178private newtype HC_Args =
176179 HC_EmptyArgs ( ) {
@@ -260,6 +263,7 @@ class HashCons extends HCBase {
260263 if this instanceof HC_ExprCall then result = "ExprCall" else
261264 if this instanceof HC_ConditionalExpr then result = "ConditionalExpr" else
262265 if this instanceof HC_NoExceptExpr then result = "NoExceptExpr" else
266+ if this instanceof HC_AllocatorArgZero then result = "AllocatorArgZero" else
263267 result = "error"
264268 }
265269
@@ -563,145 +567,92 @@ private predicate mk_ArgConsInner(HashCons head, HC_Args tail, int i, HC_Args li
563567 mk_ArgCons ( head , i , tail , c )
564568}
565569
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
569573 */
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 ( )
596584 )
597585}
598586
599587private 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 ( ) )
602590}
603591
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 ( ) )
606599}
607600
608601private predicate analyzableNewExpr ( NewExpr new ) {
609- strictcount ( new .getAllocatedType ( ) ) = 1 and
602+ strictcount ( new .getAllocatedType ( ) . getUnspecifiedType ( ) ) = 1 and
610603 count ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) <= 1 and
611604 count ( new .getInitializer ( ) .getFullyConverted ( ) ) <= 1
612605}
613606
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 ) {
616608 analyzableNewExpr ( new ) and
617- t = new .getAllocatedType ( ) and
609+ t = new .getAllocatedType ( ) . getUnspecifiedType ( ) and
618610 (
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 ( ) ) )
645612 or
646- not exists ( new .getAllocatorCall ( ) ) and
613+ not exists ( new .getAllocatorCall ( ) . getFullyConverted ( ) ) and
647614 alloc = HC_NoAlloc ( )
648615 )
649616 and
650617 (
651- init = HC_HasInit ( hashCons ( new .getInitializer ( ) ) )
618+ init = HC_HasInit ( hashCons ( new .getInitializer ( ) . getFullyConverted ( ) ) )
652619 or
653- not exists ( new .getInitializer ( ) ) and
620+ not exists ( new .getInitializer ( ) . getFullyConverted ( ) ) and
654621 init = HC_NoInit ( )
655622 )
656623}
657624
658625private predicate analyzableNewArrayExpr ( NewArrayExpr new ) {
659626 strictcount ( new .getAllocatedType ( ) .getUnspecifiedType ( ) ) = 1 and
660627 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
662630}
663631
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 ) {
666633 analyzableNewArrayExpr ( new ) and
667634 t = new .getAllocatedType ( ) and
635+
668636 (
669- align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) .getFullyConverted ( ) ) ) and
670- aligned = true
637+ alloc = HC_HasAlloc ( hashCons ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) )
671638 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 ( )
675641 )
676642 and
677643 (
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 ( ) ) )
695645 or
696- not exists ( new .getAllocatorCall ( ) ) and
697- alloc = HC_NoAlloc ( )
646+ not exists ( new .getInitializer ( ) . getFullyConverted ( ) ) and
647+ init = HC_NoInit ( )
698648 )
699649 and
650+
700651 (
701- init = HC_HasInit ( hashCons ( new .getInitializer ( ) ) )
652+ extent = HC_HasExtent ( hashCons ( new .getExtent ( ) . getFullyConverted ( ) ) )
702653 or
703- not exists ( new .getInitializer ( ) ) and
704- init = HC_NoInit ( )
654+ not exists ( new .getExtent ( ) . getFullyConverted ( ) ) and
655+ extent = HC_NoExtent ( )
705656 )
706657}
707658
@@ -984,14 +935,20 @@ cached HashCons hashCons(Expr e) {
984935 result = HC_MemberFunctionCall ( fcn , qual , args )
985936 )
986937 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 )
990947 )
991948 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 )
995952 )
996953 or
997954 exists ( Type t
@@ -1108,5 +1065,6 @@ predicate analyzableExpr(Expr e, string kind) {
11081065 ( analyzableThrowExpr ( e ) and kind = "ThrowExpr" ) or
11091066 ( analyzableReThrowExpr ( e ) and kind = "ReThrowExpr" ) or
11101067 ( 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" )
11121070}
0 commit comments