@@ -31,45 +31,83 @@ class EssentialTypeCategory extends TEssentialTypeCategory {
31
31
}
32
32
}
33
33
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
+
34
70
/**
35
71
* Gets the unsigned type of lowest rank that can represent the value of the given expression,
36
72
* assuming that the expression is essentially unsigned.
37
73
*/
38
- private IntegralType utlr ( Expr const ) {
74
+ pragma [ nomagic]
75
+ private IntegralType utlr ( ConstantIntegerExpr const ) {
39
76
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 ( )
52
89
)
53
90
}
54
91
55
92
/**
56
93
* Gets the signed type of lowest rank that can represent the value of the given expression,
57
94
* assuming that the expression is essentially signed.
58
95
*/
59
- private IntegralType stlr ( Expr const ) {
96
+ pragma [ nomagic]
97
+ private IntegralType stlr ( ConstantIntegerExpr const ) {
60
98
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 ( )
73
111
)
74
112
}
75
113
0 commit comments