22 * Provides an implementation of Hash consing.
33 * See https://en.wikipedia.org/wiki/Hash_consing
44 *
5- * The predicate `hashCons` converts an expression into a `HC `, which is an
5+ * The predicate `hashCons` converts an expression into a `HashCons `, which is an
66 * abstract type presenting the hash-cons of the expression. If two
7- * expressions have the same `HC ` then they are structurally equal.
7+ * expressions have the same `HashCons ` then they are structurally equal.
88 *
99 * Important note: this library ignores the possibility that the value of
1010 * an expression might change between one occurrence and the next. For
@@ -92,18 +92,51 @@ 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 , _, _)
97+ } or
98+ HC_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init ) {
99+ mk_NewArrayExpr ( t , alloc , init , _, _)
100+ }
101+ or
102+ HC_SizeofType ( Type t ) { mk_SizeofType ( t , _) }
103+ or
104+ HC_SizeofExpr ( HashCons child ) { mk_SizeofExpr ( child , _) }
105+ or
106+ HC_AlignofType ( Type t ) { mk_AlignofType ( t , _) }
107+ or
108+ HC_AlignofExpr ( HashCons child ) { mk_AlignofExpr ( child , _) }
109+ or
95110 // Any expression that is not handled by the cases above is
96111 // given a unique number based on the expression itself.
97112 HC_Unanalyzable ( Expr e ) { not analyzableExpr ( e , _) }
98113
114+ /** Used to implement hash-consing of `new` placement argument lists */
115+ private newtype HC_Alloc =
116+ HC_EmptyAllocArgs ( Function fcn ) {
117+ exists ( NewOrNewArrayExpr n |
118+ n .getAllocator ( ) = fcn
119+ )
120+ }
121+ or HC_AllocArgCons ( Function fcn , HashCons hc , int i , HC_Alloc list , boolean aligned ) {
122+ mk_AllocArgCons ( fcn , hc , i , list , aligned , _)
123+ }
124+ or
125+ HC_NoAlloc ( )
126+ private newtype HC_Init =
127+ HC_NoInit ( )
128+ or
129+ HC_HasInit ( HashCons hc ) { mk_HasInit ( hc , _) }
130+
99131/** Used to implement hash-consing of argument lists */
100- private cached newtype HC_Args =
132+ private newtype HC_Args =
101133 HC_EmptyArgs ( Function fcn ) {
102134 any ( )
103135 }
104136 or HC_ArgCons ( Function fcn , HashCons hc , int i , HC_Args list ) {
105137 mk_ArgCons ( fcn , hc , i , list , _)
106138 }
139+
107140/**
108141 * HashCons is the hash-cons of an expression. The relationship between `Expr`
109142 * and `HC` is many-to-one: every `Expr` has exactly one `HC`, but multiple
@@ -127,8 +160,10 @@ class HashCons extends HCBase {
127160 /** Gets the kind of the HC. This can be useful for debugging. */
128161 string getKind ( ) {
129162 if this instanceof HC_IntLiteral then result = "IntLiteral" else
163+ if this instanceof HC_EnumConstantAccess then result = "EnumConstantAccess" else
130164 if this instanceof HC_FloatLiteral then result = "FloatLiteral" else
131165 if this instanceof HC_StringLiteral then result = "StringLiteral" else
166+ if this instanceof HC_Nullptr then result = "Nullptr" else
132167 if this instanceof HC_Variable then result = "Variable" else
133168 if this instanceof HC_FieldAccess then result = "FieldAccess" else
134169 if this instanceof HC_Deref then result = "Deref" else
@@ -140,6 +175,12 @@ class HashCons extends HCBase {
140175 if this instanceof HC_Unanalyzable then result = "Unanalyzable" else
141176 if this instanceof HC_NonmemberFunctionCall then result = "NonmemberFunctionCall" else
142177 if this instanceof HC_MemberFunctionCall then result = "MemberFunctionCall" else
178+ if this instanceof HC_NewExpr then result = "NewExpr" else
179+ if this instanceof HC_NewArrayExpr then result = "NewArrayExpr" else
180+ if this instanceof HC_SizeofType then result = "SizeofTypeOperator" else
181+ if this instanceof HC_SizeofExpr then result = "SizeofExprOperator" else
182+ if this instanceof HC_AlignofType then result = "AlignofTypeOperator" else
183+ if this instanceof HC_AlignofExpr then result = "AlignofExprOperator" else
143184 result = "error"
144185 }
145186
@@ -446,6 +487,195 @@ private predicate mk_ArgCons(Function fcn, HashCons hc, int i, HC_Args list, Fun
446487 )
447488}
448489
490+
491+ /**
492+ * Holds if `fc` is a call to `fcn`, `fc`'s first `i` arguments have hash-cons
493+ * `list`, and `fc`'s argument at index `i` has hash-cons `hc`.
494+ */
495+ private predicate mk_AllocArgCons ( Function fcn , HashCons hc , int i , HC_Alloc list , boolean aligned , FunctionCall fc ) {
496+ analyzableFunctionCall ( fc ) and
497+ fc .getTarget ( ) = fcn and
498+ hc = hashCons ( fc .getArgument ( i ) .getFullyConverted ( ) ) and
499+ (
500+ exists ( HashCons head , HC_Alloc tail |
501+ list = HC_AllocArgCons ( fcn , head , i - 1 , tail , aligned ) and
502+ mk_AllocArgCons ( fcn , head , i - 1 , tail , aligned , fc ) and
503+ (
504+ aligned = true and
505+ i > 2
506+ or
507+ aligned = false and
508+ i > 1
509+ )
510+ )
511+ or
512+ (
513+ aligned = true and
514+ i = 2
515+ or
516+ aligned = false and
517+ i = 1
518+ ) and
519+ list = HC_EmptyAllocArgs ( fcn )
520+ )
521+ }
522+
523+ private predicate mk_HasInit ( HashCons hc , NewOrNewArrayExpr new ) {
524+ hc = hashCons ( new .( NewExpr ) .getInitializer ( ) ) or
525+ hc = hashCons ( new .( NewArrayExpr ) .getInitializer ( ) )
526+ }
527+
528+ private predicate analyzableNewExpr ( NewExpr new ) {
529+ strictcount ( new .getAllocatedType ( ) ) = 1 and
530+ (
531+ not exists ( new .getAllocatorCall ( ) )
532+ or
533+ strictcount ( new .getAllocatorCall ( ) ) = 1
534+ ) and (
535+ not exists ( new .getInitializer ( ) )
536+ or
537+ strictcount ( new .getInitializer ( ) ) = 1
538+ )
539+ }
540+
541+ private predicate mk_NewExpr ( Type t , HC_Alloc alloc , HC_Init init , boolean aligned , NewExpr new ) {
542+ analyzableNewExpr ( new ) and
543+ t = new .getAllocatedType ( ) and
544+ (
545+ new .hasAlignedAllocation ( ) and
546+ aligned = true
547+ or
548+ not new .hasAlignedAllocation ( ) and
549+ aligned = false
550+ )
551+ and
552+ (
553+ exists ( FunctionCall fc , HashCons head , HC_Alloc tail |
554+ fc = new .getAllocatorCall ( ) and
555+ alloc = HC_AllocArgCons ( fc .getTarget ( ) , head , fc .getNumberOfArguments ( ) - 1 , tail , aligned ) and
556+ mk_AllocArgCons ( fc .getTarget ( ) , head , fc .getNumberOfArguments ( ) - 1 , tail , aligned , fc )
557+ )
558+ or
559+ exists ( FunctionCall fc |
560+ fc = new .getAllocatorCall ( ) and
561+ (
562+ aligned = true and
563+ fc .getNumberOfArguments ( ) = 2
564+ or
565+ aligned = false and
566+ fc .getNumberOfArguments ( ) = 1
567+ ) and
568+ alloc = HC_EmptyAllocArgs ( fc .getTarget ( ) )
569+ )
570+ or
571+ not exists ( new .getAllocatorCall ( ) ) and
572+ alloc = HC_NoAlloc ( )
573+ )
574+ and
575+ (
576+ init = HC_HasInit ( hashCons ( new .getInitializer ( ) ) )
577+ or
578+ not exists ( new .getInitializer ( ) ) and
579+ init = HC_NoInit ( )
580+ )
581+ }
582+
583+ private predicate analyzableNewArrayExpr ( NewArrayExpr new ) {
584+ strictcount ( new .getAllocatedType ( ) .getUnspecifiedType ( ) ) = 1 and
585+ strictcount ( new .getAllocatedType ( ) .getUnspecifiedType ( ) ) = 1 and
586+ (
587+ not exists ( new .getAllocatorCall ( ) )
588+ or
589+ strictcount ( new .getAllocatorCall ( ) .getFullyConverted ( ) ) = 1
590+ ) and (
591+ not exists ( new .getInitializer ( ) )
592+ or
593+ strictcount ( new .getInitializer ( ) .getFullyConverted ( ) ) = 1
594+ )
595+ }
596+
597+ private predicate mk_NewArrayExpr ( Type t , HC_Alloc alloc , HC_Init init , boolean aligned ,
598+ NewArrayExpr new ) {
599+ analyzableNewArrayExpr ( new ) and
600+ t = new .getAllocatedType ( ) and
601+ (
602+ new .hasAlignedAllocation ( ) and
603+ aligned = true
604+ or
605+ not new .hasAlignedAllocation ( ) and
606+ aligned = false
607+ )
608+ and
609+ (
610+ exists ( FunctionCall fc , HashCons head , HC_Alloc tail |
611+ fc = new .getAllocatorCall ( ) and
612+ alloc = HC_AllocArgCons ( fc .getTarget ( ) , head , fc .getNumberOfArguments ( ) - 1 , tail , aligned ) and
613+ mk_AllocArgCons ( fc .getTarget ( ) , head , fc .getNumberOfArguments ( ) - 1 , tail , aligned , fc )
614+ )
615+ or
616+ exists ( FunctionCall fc |
617+ fc = new .getAllocatorCall ( ) and
618+ (
619+ aligned = true and
620+ fc .getNumberOfArguments ( ) = 2
621+ or
622+ aligned = false and
623+ fc .getNumberOfArguments ( ) = 1
624+ ) and
625+ alloc = HC_EmptyAllocArgs ( fc .getTarget ( ) )
626+ )
627+ or
628+ not exists ( new .getAllocatorCall ( ) ) and
629+ alloc = HC_NoAlloc ( )
630+ )
631+ and
632+ (
633+ init = HC_HasInit ( hashCons ( new .getInitializer ( ) ) )
634+ or
635+ not exists ( new .getInitializer ( ) ) and
636+ init = HC_NoInit ( )
637+ )
638+ }
639+
640+ private predicate analyzableSizeofType ( SizeofTypeOperator e ) {
641+ strictcount ( e .getType ( ) .getUnspecifiedType ( ) ) = 1 and
642+ strictcount ( e .getTypeOperand ( ) ) = 1
643+ }
644+
645+ private predicate mk_SizeofType ( Type t , SizeofTypeOperator e ) {
646+ analyzableSizeofType ( e ) and
647+ t = e .getTypeOperand ( )
648+ }
649+
650+ private predicate analyzableSizeofExpr ( Expr e ) {
651+ e instanceof SizeofExprOperator and
652+ strictcount ( e .getAChild ( ) .getFullyConverted ( ) ) = 1
653+ }
654+
655+ private predicate mk_SizeofExpr ( HashCons child , SizeofExprOperator e ) {
656+ analyzableSizeofExpr ( e ) and
657+ child = hashCons ( e .getAChild ( ) )
658+ }
659+
660+ private predicate analyzableAlignofType ( AlignofTypeOperator e ) {
661+ strictcount ( e .getType ( ) .getUnspecifiedType ( ) ) = 1 and
662+ strictcount ( e .getTypeOperand ( ) ) = 1
663+ }
664+
665+ private predicate mk_AlignofType ( Type t , AlignofTypeOperator e ) {
666+ analyzableAlignofType ( e ) and
667+ t = e .getTypeOperand ( )
668+ }
669+
670+ private predicate analyzableAlignofExpr ( AlignofExprOperator e ) {
671+ strictcount ( e .getExprOperand ( ) ) = 1
672+ }
673+
674+ private predicate mk_AlignofExpr ( HashCons child , AlignofExprOperator e ) {
675+ analyzableAlignofExpr ( e ) and
676+ child = hashCons ( e .getAChild ( ) )
677+ }
678+
449679/** Gets the hash-cons of expression `e`. */
450680cached HashCons hashCons ( Expr e ) {
451681 exists ( int val , Type t
@@ -514,6 +744,36 @@ cached HashCons hashCons(Expr e) {
514744 result = HC_MemberFunctionCall ( fcn , qual , args )
515745 )
516746 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 )
750+ )
751+ 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 )
755+ )
756+ or
757+ exists ( Type t
758+ | mk_SizeofType ( t , e ) and
759+ result = HC_SizeofType ( t )
760+ )
761+ or
762+ exists ( HashCons child
763+ | mk_SizeofExpr ( child , e ) and
764+ result = HC_SizeofExpr ( child )
765+ )
766+ or
767+ exists ( Type t
768+ | mk_AlignofType ( t , e ) and
769+ result = HC_AlignofType ( t )
770+ )
771+ or
772+ exists ( HashCons child
773+ | mk_AlignofExpr ( child , e ) and
774+ result = HC_AlignofExpr ( child )
775+ )
776+ or
517777 (
518778 mk_Nullptr ( e ) and
519779 result = HC_Nullptr ( )
@@ -545,5 +805,11 @@ predicate analyzableExpr(Expr e, string kind) {
545805 ( analyzableArrayAccess ( e ) and kind = "ArrayAccess" ) or
546806 ( analyzablePointerDereferenceExpr ( e ) and kind = "PointerDereferenceExpr" ) or
547807 ( analyzableNonmemberFunctionCall ( e ) and kind = "NonmemberFunctionCall" ) or
548- ( analyzableMemberFunctionCall ( e ) and kind = "MemberFunctionCall" )
808+ ( analyzableMemberFunctionCall ( e ) and kind = "MemberFunctionCall" ) or
809+ ( analyzableNewExpr ( e ) and kind = "NewExpr" ) or
810+ ( analyzableNewArrayExpr ( e ) and kind = "NewArrayExpr" ) or
811+ ( analyzableSizeofType ( e ) and kind = "SizeofTypeOperator" ) or
812+ ( analyzableSizeofExpr ( e ) and kind = "SizeofExprOperator" ) or
813+ ( analyzableAlignofType ( e ) and kind = "AlignofTypeOperator" ) or
814+ ( analyzableAlignofExpr ( e ) and kind = "AlignofExprOperator" )
549815}
0 commit comments