@@ -107,6 +107,14 @@ private cached newtype HCBase =
107
107
or
108
108
HC_AlignofExpr ( HashCons child ) { mk_AlignofExpr ( child , _) }
109
109
or
110
+ HC_ClassAggregateLiteral ( Class c , HC_Fields hcf ) {
111
+ mk_ClassAggregateLiteral ( c , hcf , _)
112
+ }
113
+ or
114
+ HC_ArrayAggregateLiteral ( Type t , HC_Array hca ) {
115
+ mk_ArrayAggregateLiteral ( t , hca , _)
116
+ }
117
+ or
110
118
// Any expression that is not handled by the cases above is
111
119
// given a unique number based on the expression itself.
112
120
HC_Unanalyzable ( Expr e ) { not analyzableExpr ( e , _) }
@@ -144,6 +152,30 @@ private newtype HC_Args =
144
152
mk_ArgCons ( fcn , hc , i , list , _)
145
153
}
146
154
155
+ /**
156
+ * Used to implement hash-consing of struct initizializers.
157
+ */
158
+ private newtype HC_Fields =
159
+ HC_EmptyFields ( Class c ) {
160
+ exists ( ClassAggregateLiteral cal |
161
+ c = cal .getType ( ) .getUnspecifiedType ( )
162
+ )
163
+ }
164
+ or
165
+ HC_FieldCons ( Class c , int i , Field f , HashCons hc , HC_Fields hcf ) {
166
+ mk_FieldCons ( c , i , f , hc , hcf , _)
167
+ }
168
+
169
+ private newtype HC_Array =
170
+ HC_EmptyArray ( Type t ) {
171
+ exists ( ArrayAggregateLiteral aal |
172
+ aal .getType ( ) = t
173
+ )
174
+ }
175
+ or
176
+ HC_ArrayCons ( Type t , int i , HashCons hc , HC_Array hca ) {
177
+ mk_ArrayCons ( t , i , hc , hca , _)
178
+ }
147
179
/**
148
180
* HashCons is the hash-cons of an expression. The relationship between `Expr`
149
181
* and `HC` is many-to-one: every `Expr` has exactly one `HC`, but multiple
@@ -188,6 +220,8 @@ class HashCons extends HCBase {
188
220
if this instanceof HC_SizeofExpr then result = "SizeofExprOperator" else
189
221
if this instanceof HC_AlignofType then result = "AlignofTypeOperator" else
190
222
if this instanceof HC_AlignofExpr then result = "AlignofExprOperator" else
223
+ if this instanceof HC_ArrayAggregateLiteral then result = "ArrayAggregateLiteral" else
224
+ if this instanceof HC_ClassAggregateLiteral then result = "ClassAggreagateLiteral" else
191
225
result = "error"
192
226
}
193
227
@@ -690,6 +724,87 @@ private predicate mk_AlignofExpr(HashCons child, AlignofExprOperator e) {
690
724
child = hashCons ( e .getAChild ( ) )
691
725
}
692
726
727
+ private predicate mk_FieldCons ( Class c , int i , Field f , HashCons hc , HC_Fields hcf ,
728
+ ClassAggregateLiteral cal ) {
729
+ analyzableClassAggregateLiteral ( cal ) and
730
+ cal .getType ( ) .getUnspecifiedType ( ) = c and
731
+ exists ( Expr e |
732
+ e = cal .getFieldExpr ( f ) .getFullyConverted ( ) and
733
+ e = cal .getChild ( i ) .getFullyConverted ( ) and
734
+ hc = hashCons ( e ) and
735
+ (
736
+ exists ( HashCons head , Field f2 , HC_Fields tail |
737
+ hcf = HC_FieldCons ( c , i - 1 , f2 , head , tail ) and
738
+ cal .getChild ( i - 1 ) .getFullyConverted ( ) = cal .getFieldExpr ( f2 ) .getFullyConverted ( ) and
739
+ mk_FieldCons ( c , i - 1 , f2 , head , tail , cal )
740
+
741
+ )
742
+ or
743
+ i = 0 and
744
+ hcf = HC_EmptyFields ( c )
745
+ )
746
+ )
747
+ }
748
+
749
+ private predicate analyzableClassAggregateLiteral ( ClassAggregateLiteral cal ) {
750
+ forall ( int i |
751
+ exists ( cal .getChild ( i ) ) |
752
+ strictcount ( cal .getChild ( i ) .getFullyConverted ( ) ) = 1 and
753
+ strictcount ( Field f | cal .getChild ( i ) = cal .getFieldExpr ( f ) ) = 1
754
+ )
755
+ }
756
+
757
+ private predicate mk_ClassAggregateLiteral ( Class c , HC_Fields hcf , ClassAggregateLiteral cal ) {
758
+ analyzableClassAggregateLiteral ( cal ) and
759
+ c = cal .getType ( ) .getUnspecifiedType ( ) and
760
+ (
761
+ exists ( HC_Fields tail , Expr e , Field f |
762
+ e = cal .getChild ( cal .getNumChild ( ) - 1 ) .getFullyConverted ( ) and
763
+ e = cal .getFieldExpr ( f ) .getFullyConverted ( ) and
764
+ hcf = HC_FieldCons ( c , cal .getNumChild ( ) - 1 , f , hashCons ( e ) , tail ) and
765
+ mk_FieldCons ( c , cal .getNumChild ( ) - 1 , f , hashCons ( e ) , tail , cal )
766
+ )
767
+ or
768
+ cal .getNumChild ( ) = 0 and
769
+ hcf = HC_EmptyFields ( c )
770
+ )
771
+ }
772
+
773
+ private predicate analyzableArrayAggregateLiteral ( ArrayAggregateLiteral aal ) {
774
+ forall ( int i |
775
+ exists ( aal .getChild ( i ) ) |
776
+ strictcount ( aal .getChild ( i ) .getFullyConverted ( ) ) = 1
777
+ )
778
+ }
779
+
780
+ private predicate mk_ArrayCons ( Type t , int i , HashCons hc , HC_Array hca , ArrayAggregateLiteral aal ) {
781
+ t = aal .getType ( ) .getUnspecifiedType ( ) and
782
+ hc = hashCons ( aal .getChild ( i ) ) and
783
+ (
784
+ exists ( HC_Array tail , HashCons head |
785
+ hca = HC_ArrayCons ( t , i - 1 , head , tail ) and
786
+ mk_ArrayCons ( t , i - 1 , head , tail , aal )
787
+ )
788
+ or
789
+ i = 0 and
790
+ hca = HC_EmptyArray ( t )
791
+ )
792
+ }
793
+
794
+ private predicate mk_ArrayAggregateLiteral ( Type t , HC_Array hca , ArrayAggregateLiteral aal ) {
795
+ t = aal .getType ( ) .getUnspecifiedType ( ) and
796
+ (
797
+ exists ( HashCons head , HC_Array tail |
798
+ hca = HC_ArrayCons ( t , aal .getNumChild ( ) - 1 , head , tail ) and
799
+ mk_ArrayCons ( t , aal .getNumChild ( ) - 1 , head , tail , aal )
800
+ )
801
+ or
802
+ aal .getNumChild ( ) = 0 and
803
+ hca = HC_EmptyArray ( t )
804
+ )
805
+ }
806
+
807
+
693
808
/** Gets the hash-cons of expression `e`. */
694
809
cached HashCons hashCons ( Expr e ) {
695
810
exists ( int val , Type t
@@ -788,6 +903,16 @@ cached HashCons hashCons(Expr e) {
788
903
result = HC_AlignofExpr ( child )
789
904
)
790
905
or
906
+ exists ( Class c , HC_Fields hfc
907
+ | mk_ClassAggregateLiteral ( c , hfc , e ) and
908
+ result = HC_ClassAggregateLiteral ( c , hfc )
909
+ )
910
+ or
911
+ exists ( Type t , HC_Array hca
912
+ | mk_ArrayAggregateLiteral ( t , hca , e ) and
913
+ result = HC_ArrayAggregateLiteral ( t , hca )
914
+ )
915
+ or
791
916
(
792
917
mk_Nullptr ( e ) and
793
918
result = HC_Nullptr ( )
@@ -825,5 +950,8 @@ predicate analyzableExpr(Expr e, string kind) {
825
950
( analyzableSizeofType ( e ) and kind = "SizeofTypeOperator" ) or
826
951
( analyzableSizeofExpr ( e ) and kind = "SizeofExprOperator" ) or
827
952
( analyzableAlignofType ( e ) and kind = "AlignofTypeOperator" ) or
828
- ( analyzableAlignofExpr ( e ) and kind = "AlignofExprOperator" )
953
+ ( analyzableAlignofExpr ( e ) and kind = "AlignofExprOperator" ) or
954
+ ( analyzableClassAggregateLiteral ( e ) and kind = "ClassAggregateLiteral" ) or
955
+ ( analyzableArrayAggregateLiteral ( e ) and kind = "ArrayAggregateLiteral" )
956
+
829
957
}
0 commit comments