@@ -92,11 +92,11 @@ private cached newtype HCBase =
92
92
mk_MemberFunctionCall ( trg , qual , args , _)
93
93
}
94
94
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 , _, _)
97
97
} 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 , _, _)
100
100
}
101
101
or
102
102
HC_SizeofType ( Type t ) { mk_SizeofType ( t , _) }
@@ -123,11 +123,18 @@ private newtype HC_Alloc =
123
123
}
124
124
or
125
125
HC_NoAlloc ( )
126
+
127
+ /** Used to implement optional init on `new` expressions */
126
128
private newtype HC_Init =
127
129
HC_NoInit ( )
128
130
or
129
131
HC_HasInit ( HashCons hc ) { mk_HasInit ( hc , _) }
130
132
133
+ private newtype HC_Align =
134
+ HC_NoAlign ( )
135
+ or
136
+ HC_HasAlign ( HashCons hc ) { mk_HasAlign ( hc , _) }
137
+
131
138
/** Used to implement hash-consing of argument lists */
132
139
private newtype HC_Args =
133
140
HC_EmptyArgs ( Function fcn ) {
@@ -525,6 +532,10 @@ private predicate mk_HasInit(HashCons hc, NewOrNewArrayExpr new) {
525
532
hc = hashCons ( new .( NewArrayExpr ) .getInitializer ( ) )
526
533
}
527
534
535
+ private predicate mk_HasAlign ( HashCons hc , NewOrNewArrayExpr new ) {
536
+ hc = hashCons ( new .getAlignmentArgument ( ) )
537
+ }
538
+
528
539
private predicate analyzableNewExpr ( NewExpr new ) {
529
540
strictcount ( new .getAllocatedType ( ) ) = 1 and
530
541
(
@@ -538,14 +549,16 @@ private predicate analyzableNewExpr(NewExpr new) {
538
549
)
539
550
}
540
551
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 ) {
542
554
analyzableNewExpr ( new ) and
543
555
t = new .getAllocatedType ( ) and
544
556
(
545
- new .hasAlignedAllocation ( ) and
557
+ align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) ) ) and
546
558
aligned = true
547
559
or
548
560
not new .hasAlignedAllocation ( ) and
561
+ align = HC_NoAlign ( ) and
549
562
aligned = false
550
563
)
551
564
and
@@ -594,15 +607,16 @@ private predicate analyzableNewArrayExpr(NewArrayExpr new) {
594
607
)
595
608
}
596
609
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 ) {
599
612
analyzableNewArrayExpr ( new ) and
600
613
t = new .getAllocatedType ( ) and
601
614
(
602
- new .hasAlignedAllocation ( ) and
615
+ align = HC_HasAlign ( hashCons ( new .getAlignmentArgument ( ) ) ) and
603
616
aligned = true
604
617
or
605
618
not new .hasAlignedAllocation ( ) and
619
+ align = HC_NoAlign ( ) and
606
620
aligned = false
607
621
)
608
622
and
@@ -744,14 +758,14 @@ cached HashCons hashCons(Expr e) {
744
758
result = HC_MemberFunctionCall ( fcn , qual , args )
745
759
)
746
760
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 )
750
764
)
751
765
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 )
755
769
)
756
770
or
757
771
exists ( Type t
0 commit comments