Skip to content

Commit 4a04ff2

Browse files
authored
Merge pull request #257 from github/lcartey/improve-essential-type-performance
EssentialTypes: Improve performance.
2 parents 278e29a + bc4db01 commit 4a04ff2

File tree

3 files changed

+88
-30
lines changed

3 files changed

+88
-30
lines changed

c/misra/src/codingstandards/c/misra/EssentialTypes.qll

Lines changed: 65 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -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]
111150
Type getEssentialType(Expr e) {
112151
if e.hasExplicitConversion()
113152
then

c/misra/src/rules/RULE-10-5/InappropriateEssentialTypeCast.ql

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -49,16 +49,23 @@ predicate isIncompatibleEssentialTypeCast(EssentialTypeCategory fromCat, Essenti
4949
]
5050
}
5151

52+
predicate isCastTypes(
53+
Cast c, Type essentialFromType, Type essentialToType, EssentialTypeCategory fromCategory,
54+
EssentialTypeCategory toCategory
55+
) {
56+
essentialFromType = getEssentialTypeBeforeConversions(c.getExpr()) and
57+
essentialToType = c.getType() and
58+
fromCategory = getEssentialTypeCategory(essentialFromType) and
59+
toCategory = getEssentialTypeCategory(essentialToType)
60+
}
61+
5262
from
5363
Cast c, Type essentialFromType, Type essentialToType, EssentialTypeCategory fromCategory,
5464
EssentialTypeCategory toCategory, string message
5565
where
5666
not isExcluded(c, EssentialTypesPackage::inappropriateEssentialTypeCastQuery()) and
5767
not c.isImplicit() and
58-
essentialFromType = getEssentialTypeBeforeConversions(c.getExpr()) and
59-
essentialToType = c.getType() and
60-
fromCategory = getEssentialTypeCategory(essentialFromType) and
61-
toCategory = getEssentialTypeCategory(essentialToType) and
68+
isCastTypes(c, essentialFromType, essentialToType, fromCategory, toCategory) and
6269
isIncompatibleEssentialTypeCast(fromCategory, toCategory) and
6370
(
6471
if fromCategory = EssentiallyEnumType() and toCategory = EssentiallyEnumType()
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
* The performance of the following queries related to essential types have been improved:
2+
* `Rule 10.1`
3+
* `Rule 10.2`
4+
* `Rule 10.3`
5+
* `Rule 10.4`
6+
* `Rule 10.5`
7+
* `Rule 10.6`
8+
* `Rule 10.7`
9+
* `Rule 10.8`
10+
* `Rule 14.1`
11+
* `Rule 21.14`
12+
* `Rule 21.16`

0 commit comments

Comments
 (0)