diff --git a/c/misra/src/codingstandards/c/misra/EssentialTypes.qll b/c/misra/src/codingstandards/c/misra/EssentialTypes.qll index 697a24513f..9bec0e518f 100644 --- a/c/misra/src/codingstandards/c/misra/EssentialTypes.qll +++ b/c/misra/src/codingstandards/c/misra/EssentialTypes.qll @@ -31,24 +31,61 @@ 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() ) } @@ -56,20 +93,21 @@ private IntegralType utlr(Expr const) { * 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() ) } @@ -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 diff --git a/c/misra/src/rules/RULE-10-5/InappropriateEssentialTypeCast.ql b/c/misra/src/rules/RULE-10-5/InappropriateEssentialTypeCast.ql index 10d54c4fff..1ff8374e97 100644 --- a/c/misra/src/rules/RULE-10-5/InappropriateEssentialTypeCast.ql +++ b/c/misra/src/rules/RULE-10-5/InappropriateEssentialTypeCast.ql @@ -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() diff --git a/change_notes/2023-03-16-essential-types-performance.md b/change_notes/2023-03-16-essential-types-performance.md new file mode 100644 index 0000000000..115c162e89 --- /dev/null +++ b/change_notes/2023-03-16-essential-types-performance.md @@ -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` \ No newline at end of file