@@ -92,11 +92,11 @@ private cached newtype HCBase =
9292 mk_MemberFunctionCall ( trg , qual , args , _)
9393 }
9494 or
95- HC_NewExpr ( Type t , HC_Alloc alloc , HC_Init init ) {
96- mk_NewExpr ( t , alloc , init , _, _)
95+ HC_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align ) {
96+ mk_NewExpr ( t , alloc , init , align , _, _)
9797 } or
98- HC_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init ) {
99- mk_NewArrayExpr ( t , alloc , init , _, _)
98+ HC_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align ) {
99+ mk_NewArrayExpr ( t , alloc , init , align , _, _)
100100 }
101101 or
102102 HC_SizeofType ( Type t ) { mk_SizeofType ( t , _) }
@@ -123,11 +123,18 @@ private newtype HC_Alloc =
123123 }
124124 or
125125 HC_NoAlloc ( )
126+
127+ /** Used to implement optional init on `new` expressions */
126128private newtype HC_Init =
127129 HC_NoInit ( )
128130 or
129131 HC_HasInit ( HashCons hc ) { mk_HasInit ( hc , _) }
130132
133+ private newtype HC_Align =
134+ HC_NoAlign ( )
135+ or
136+ HC_HasAlign ( HashCons hc ) { mk_HasAlign ( hc , _) }
137+
131138/** Used to implement hash-consing of argument lists */
132139private newtype HC_Args =
133140 HC_EmptyArgs ( Function fcn ) {
@@ -525,6 +532,10 @@ private predicate mk_HasInit(HashCons hc, NewOrNewArrayExpr new) {
525532 hc = hashCons ( new .( NewArrayExpr ) .getInitializer ( ) )
526533}
527534
535+ private predicate mk_HasAlign ( HashCons hc , NewOrNewArrayExpr new ) {
536+ hc = hashCons ( new .getAlignmentArgument ( ) )
537+ }
538+
528539private predicate analyzableNewExpr ( NewExpr new ) {
529540 strictcount ( new .getAllocatedType ( ) ) = 1 and
530541 (
@@ -538,14 +549,16 @@ private predicate analyzableNewExpr(NewExpr new) {
538549 )
539550}
540551
541- private predicate mk_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , boolean aligned , NewExpr new ) {
552+ private predicate mk_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align , boolean aligned ,
553+ NewExpr new ) {
542554 analyzableNewExpr ( new ) and
543555 t = new .getAllocatedType ( ) and
544556 (
545- new .hasAlignedAllocation ( ) and
557+ align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) ) ) and
546558 aligned = true
547559 or
548560 not new .hasAlignedAllocation ( ) and
561+ align = HC_NoAlign ( ) and
549562 aligned = false
550563 )
551564 and
@@ -594,15 +607,16 @@ private predicate analyzableNewArrayExpr(NewArrayExpr new) {
594607 )
595608}
596609
597- private predicate mk_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init , boolean aligned ,
598- NewArrayExpr new ) {
610+ private predicate mk_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align ,
611+ boolean aligned , NewArrayExpr new ) {
599612 analyzableNewArrayExpr ( new ) and
600613 t = new .getAllocatedType ( ) and
601614 (
602- new .hasAlignedAllocation ( ) and
615+ align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) ) ) and
603616 aligned = true
604617 or
605618 not new .hasAlignedAllocation ( ) and
619+ align = HC_NoAlign ( ) and
606620 aligned = false
607621 )
608622 and
@@ -744,14 +758,14 @@ cached HashCons hashCons(Expr e) {
744758 result = HC_MemberFunctionCall ( fcn , qual , args )
745759 )
746760 or
747- exists ( Type t , HC_Alloc alloc , HC_Init init , boolean aligned
748- | mk_NewExpr ( t , alloc , init , aligned , e ) and
749- result = HC_NewExpr ( t , alloc , init )
761+ exists ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align , boolean aligned
762+ | mk_NewExpr ( t , alloc , init , align , aligned , e ) and
763+ result = HC_NewExpr ( t , alloc , init , align )
750764 )
751765 or
752- exists ( Type t , HC_Alloc alloc , HC_Init init , boolean aligned
753- | mk_NewArrayExpr ( t , alloc , init , aligned , e ) and
754- result = HC_NewArrayExpr ( t , alloc , init )
766+ exists ( Type t , HC_Alloc alloc , HC_Init init , HC_Align align , boolean aligned
767+ | mk_NewArrayExpr ( t , alloc , init , align , aligned , e ) and
768+ result = HC_NewArrayExpr ( t , alloc , init , align )
755769 )
756770 or
757771 exists ( Type t
0 commit comments