@@ -107,6 +107,14 @@ private cached newtype HCBase =
107107 or
108108 HC_AlignofExpr ( HashCons child ) { mk_AlignofExpr ( child , _) }
109109 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
110118 // Any expression that is not handled by the cases above is
111119 // given a unique number based on the expression itself.
112120 HC_Unanalyzable ( Expr e ) { not analyzableExpr ( e , _) }
@@ -144,6 +152,30 @@ private newtype HC_Args =
144152 mk_ArgCons ( fcn , hc , i , list , _)
145153 }
146154
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+ }
147179/**
148180 * HashCons is the hash-cons of an expression. The relationship between `Expr`
149181 * and `HC` is many-to-one: every `Expr` has exactly one `HC`, but multiple
@@ -188,6 +220,8 @@ class HashCons extends HCBase {
188220 if this instanceof HC_SizeofExpr then result = "SizeofExprOperator" else
189221 if this instanceof HC_AlignofType then result = "AlignofTypeOperator" else
190222 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
191225 result = "error"
192226 }
193227
@@ -690,6 +724,87 @@ private predicate mk_AlignofExpr(HashCons child, AlignofExprOperator e) {
690724 child = hashCons ( e .getAChild ( ) )
691725}
692726
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+
693808/** Gets the hash-cons of expression `e`. */
694809cached HashCons hashCons ( Expr e ) {
695810 exists ( int val , Type t
@@ -788,6 +903,16 @@ cached HashCons hashCons(Expr e) {
788903 result = HC_AlignofExpr ( child )
789904 )
790905 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
791916 (
792917 mk_Nullptr ( e ) and
793918 result = HC_Nullptr ( )
@@ -825,5 +950,8 @@ predicate analyzableExpr(Expr e, string kind) {
825950 ( analyzableSizeofType ( e ) and kind = "SizeofTypeOperator" ) or
826951 ( analyzableSizeofExpr ( e ) and kind = "SizeofExprOperator" ) or
827952 ( 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+
829957}
0 commit comments