@@ -31,45 +31,83 @@ class EssentialTypeCategory extends TEssentialTypeCategory {
3131 }
3232}
3333
34+ /**
35+ * An expression in the program that evaluates to a compile time constant signed or unsigned integer.
36+ */
37+ private class ConstantIntegerExpr extends Expr {
38+ pragma [ noinline]
39+ ConstantIntegerExpr ( ) {
40+ getEssentialTypeCategory ( this .getType ( ) ) =
41+ [
42+ EssentiallyUnsignedType ( ) .( EssentialTypeCategory ) ,
43+ EssentiallySignedType ( ) .( EssentialTypeCategory )
44+ ] and
45+ exists ( this .getValue ( ) .toFloat ( ) ) and
46+ not this instanceof Conversion
47+ }
48+ }
49+
50+ /** A `float` which represents an integer constant in the program. */
51+ private class IntegerConstantAsFloat extends float {
52+ IntegerConstantAsFloat ( ) { exists ( ConstantIntegerExpr ce | this = ce .getValue ( ) .toFloat ( ) ) }
53+ }
54+
55+ /**
56+ * Identifies which integral types from which type categories can represent a given integer constant
57+ * in the program.
58+ */
59+ pragma [ nomagic]
60+ private predicate isCandidateIntegralType (
61+ EssentialTypeCategory cat , IntegralType it , IntegerConstantAsFloat c
62+ ) {
63+ getEssentialTypeCategory ( it ) = cat and
64+ c = any ( ConstantIntegerExpr ce ) .getValue ( ) .toFloat ( ) and
65+ // As with range analysis, we assume two's complement representation
66+ typeLowerBound ( it ) <= c and
67+ typeUpperBound ( it ) >= c
68+ }
69+
3470/**
3571 * Gets the unsigned type of lowest rank that can represent the value of the given expression,
3672 * assuming that the expression is essentially unsigned.
3773 */
38- private IntegralType utlr ( Expr const ) {
74+ pragma [ nomagic]
75+ private IntegralType utlr ( ConstantIntegerExpr const ) {
3976 getEssentialTypeCategory ( const .getType ( ) ) = EssentiallyUnsignedType ( ) and
40- getEssentialTypeCategory ( result ) = EssentiallyUnsignedType ( ) and
41- exists ( float c | c = const . getValue ( ) . toFloat ( ) |
42- // As with range analysis, we assume two's complement representation
43- typeLowerBound ( result ) <= c and
44- typeUpperBound ( result ) >= c and
45- forall ( IntegralType it |
46- getEssentialTypeCategory ( it ) = EssentiallyUnsignedType ( ) and
47- typeLowerBound ( it ) <= c and
48- typeUpperBound ( it ) >= c
49- |
50- result . getSize ( ) <= it . getSize ( )
51- )
77+ result = utlr_c ( const . getValue ( ) . toFloat ( ) )
78+ }
79+
80+ /**
81+ * Given an integer constant that appears in the program, gets the unsigned type of lowest rank
82+ * that can hold it.
83+ */
84+ pragma [ nomagic ]
85+ private IntegralType utlr_c ( IntegerConstantAsFloat c ) {
86+ isCandidateIntegralType ( EssentiallyUnsignedType ( ) , result , c ) and
87+ forall ( IntegralType it | isCandidateIntegralType ( EssentiallyUnsignedType ( ) , it , c ) |
88+ result . getSize ( ) <= it . getSize ( )
5289 )
5390}
5491
5592/**
5693 * Gets the signed type of lowest rank that can represent the value of the given expression,
5794 * assuming that the expression is essentially signed.
5895 */
59- private IntegralType stlr ( Expr const ) {
96+ pragma [ nomagic]
97+ private IntegralType stlr ( ConstantIntegerExpr const ) {
6098 getEssentialTypeCategory ( const .getType ( ) ) = EssentiallySignedType ( ) and
61- getEssentialTypeCategory ( result ) = EssentiallySignedType ( ) and
62- exists ( float c | c = const . getValue ( ) . toFloat ( ) |
63- // As with range analysis, we assume two's complement representation
64- typeLowerBound ( result ) <= c and
65- typeUpperBound ( result ) >= c and
66- forall ( IntegralType it |
67- getEssentialTypeCategory ( it ) = EssentiallySignedType ( ) and
68- typeLowerBound ( it ) <= c and
69- typeUpperBound ( it ) >= c
70- |
71- result . getSize ( ) <= it . getSize ( )
72- )
99+ result = stlr_c ( const . getValue ( ) . toFloat ( ) )
100+ }
101+
102+ /**
103+ * Given an integer constant that appears in the program, gets the signed type of lowest rank
104+ * that can hold it.
105+ */
106+ pragma [ nomagic ]
107+ private IntegralType stlr_c ( IntegerConstantAsFloat c ) {
108+ isCandidateIntegralType ( EssentiallySignedType ( ) , result , c ) and
109+ forall ( IntegralType it | isCandidateIntegralType ( EssentiallySignedType ( ) , it , c ) |
110+ result . getSize ( ) <= it . getSize ( )
73111 )
74112}
75113
@@ -108,6 +146,7 @@ EssentialTypeCategory getEssentialTypeCategory(Type type) {
108146/**
109147 * Gets the essential type of the given expression `e`, considering any explicit conversions.
110148 */
149+ pragma [ nomagic]
111150Type getEssentialType ( Expr e ) {
112151 if e .hasExplicitConversion ( )
113152 then
0 commit comments