Skip to content

EssentialTypes: Improve performance. #257

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Mar 17, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
91 changes: 65 additions & 26 deletions c/misra/src/codingstandards/c/misra/EssentialTypes.qll
Original file line number Diff line number Diff line change
Expand Up @@ -31,45 +31,83 @@ class EssentialTypeCategory extends TEssentialTypeCategory {
}
}

/**
* An expression in the program that evaluates to a compile time constant signed or unsigned integer.
*/
private class ConstantIntegerExpr extends Expr {
pragma[noinline]
ConstantIntegerExpr() {
getEssentialTypeCategory(this.getType()) =
[
EssentiallyUnsignedType().(EssentialTypeCategory),
EssentiallySignedType().(EssentialTypeCategory)
] and
exists(this.getValue().toFloat()) and
not this instanceof Conversion
}
}

/** A `float` which represents an integer constant in the program. */
private class IntegerConstantAsFloat extends float {
IntegerConstantAsFloat() { exists(ConstantIntegerExpr ce | this = ce.getValue().toFloat()) }
}

/**
* Identifies which integral types from which type categories can represent a given integer constant
* in the program.
*/
pragma[nomagic]
private predicate isCandidateIntegralType(
EssentialTypeCategory cat, IntegralType it, IntegerConstantAsFloat c
) {
getEssentialTypeCategory(it) = cat and
c = any(ConstantIntegerExpr ce).getValue().toFloat() and
// As with range analysis, we assume two's complement representation
typeLowerBound(it) <= c and
typeUpperBound(it) >= c
}

/**
* Gets the unsigned type of lowest rank that can represent the value of the given expression,
* assuming that the expression is essentially unsigned.
*/
private IntegralType utlr(Expr const) {
pragma[nomagic]
private IntegralType utlr(ConstantIntegerExpr const) {
getEssentialTypeCategory(const.getType()) = EssentiallyUnsignedType() and
getEssentialTypeCategory(result) = EssentiallyUnsignedType() and
exists(float c | c = const.getValue().toFloat() |
// As with range analysis, we assume two's complement representation
typeLowerBound(result) <= c and
typeUpperBound(result) >= c and
forall(IntegralType it |
getEssentialTypeCategory(it) = EssentiallyUnsignedType() and
typeLowerBound(it) <= c and
typeUpperBound(it) >= c
|
result.getSize() <= it.getSize()
)
result = utlr_c(const.getValue().toFloat())
}

/**
* Given an integer constant that appears in the program, gets the unsigned type of lowest rank
* that can hold it.
*/
pragma[nomagic]
private IntegralType utlr_c(IntegerConstantAsFloat c) {
isCandidateIntegralType(EssentiallyUnsignedType(), result, c) and
forall(IntegralType it | isCandidateIntegralType(EssentiallyUnsignedType(), it, c) |
result.getSize() <= it.getSize()
)
}

/**
* Gets the signed type of lowest rank that can represent the value of the given expression,
* assuming that the expression is essentially signed.
*/
private IntegralType stlr(Expr const) {
pragma[nomagic]
private IntegralType stlr(ConstantIntegerExpr const) {
getEssentialTypeCategory(const.getType()) = EssentiallySignedType() and
getEssentialTypeCategory(result) = EssentiallySignedType() and
exists(float c | c = const.getValue().toFloat() |
// As with range analysis, we assume two's complement representation
typeLowerBound(result) <= c and
typeUpperBound(result) >= c and
forall(IntegralType it |
getEssentialTypeCategory(it) = EssentiallySignedType() and
typeLowerBound(it) <= c and
typeUpperBound(it) >= c
|
result.getSize() <= it.getSize()
)
result = stlr_c(const.getValue().toFloat())
}

/**
* Given an integer constant that appears in the program, gets the signed type of lowest rank
* that can hold it.
*/
pragma[nomagic]
private IntegralType stlr_c(IntegerConstantAsFloat c) {
isCandidateIntegralType(EssentiallySignedType(), result, c) and
forall(IntegralType it | isCandidateIntegralType(EssentiallySignedType(), it, c) |
result.getSize() <= it.getSize()
)
}

Expand Down Expand Up @@ -108,6 +146,7 @@ EssentialTypeCategory getEssentialTypeCategory(Type type) {
/**
* Gets the essential type of the given expression `e`, considering any explicit conversions.
*/
pragma[nomagic]
Type getEssentialType(Expr e) {
if e.hasExplicitConversion()
then
Expand Down
15 changes: 11 additions & 4 deletions c/misra/src/rules/RULE-10-5/InappropriateEssentialTypeCast.ql
Original file line number Diff line number Diff line change
Expand Up @@ -49,16 +49,23 @@ predicate isIncompatibleEssentialTypeCast(EssentialTypeCategory fromCat, Essenti
]
}

predicate isCastTypes(
Cast c, Type essentialFromType, Type essentialToType, EssentialTypeCategory fromCategory,
EssentialTypeCategory toCategory
) {
essentialFromType = getEssentialTypeBeforeConversions(c.getExpr()) and
essentialToType = c.getType() and
fromCategory = getEssentialTypeCategory(essentialFromType) and
toCategory = getEssentialTypeCategory(essentialToType)
}

from
Cast c, Type essentialFromType, Type essentialToType, EssentialTypeCategory fromCategory,
EssentialTypeCategory toCategory, string message
where
not isExcluded(c, EssentialTypesPackage::inappropriateEssentialTypeCastQuery()) and
not c.isImplicit() and
essentialFromType = getEssentialTypeBeforeConversions(c.getExpr()) and
essentialToType = c.getType() and
fromCategory = getEssentialTypeCategory(essentialFromType) and
toCategory = getEssentialTypeCategory(essentialToType) and
isCastTypes(c, essentialFromType, essentialToType, fromCategory, toCategory) and
isIncompatibleEssentialTypeCast(fromCategory, toCategory) and
(
if fromCategory = EssentiallyEnumType() and toCategory = EssentiallyEnumType()
Expand Down
12 changes: 12 additions & 0 deletions change_notes/2023-03-16-essential-types-performance.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
* The performance of the following queries related to essential types have been improved:
* `Rule 10.1`
* `Rule 10.2`
* `Rule 10.3`
* `Rule 10.4`
* `Rule 10.5`
* `Rule 10.6`
* `Rule 10.7`
* `Rule 10.8`
* `Rule 14.1`
* `Rule 21.14`
* `Rule 21.16`