From 3875c27b13fbbdc0a6caa72c4704cc8730e194a5 Mon Sep 17 00:00:00 2001 From: Luke Cartey Date: Thu, 16 Mar 2023 17:59:23 +0000 Subject: [PATCH 1/4] EssentialTypes: Address performance issues with stlr/utlr The calculatons for signed and unsigned type of lowest rank were expensive when there were a large number of constant expressions in the program. This commit improves performance by: 1. Creating classes to represent the set of integer constant expressions and integer constants in the program. 2. Creating a candidate table of IntegralTypes for each known constant integer value in the program, to avoid duplicate work. 3. Calculating the stlr and utlr for each constant value, not each constant expression. --- .../c/misra/EssentialTypes.qll | 90 +++++++++++++------ 1 file changed, 64 insertions(+), 26 deletions(-) diff --git a/c/misra/src/codingstandards/c/misra/EssentialTypes.qll b/c/misra/src/codingstandards/c/misra/EssentialTypes.qll index 697a24513f..ceba70fbfb 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() ) } From 982b5b34efbedb03c6b5b7ef3de1754426e1091f Mon Sep 17 00:00:00 2001 From: Luke Cartey Date: Thu, 16 Mar 2023 18:05:12 +0000 Subject: [PATCH 2/4] EssentialTypes: Improve performance of Rule 10.5 This improves the performance of Rule 10.5 by computing all the types of the cast first, before determining whether they were invalid. Previously the join orderer found the essential type category of the "from" type, then joined that will invalid type categories, then joined that with all expressions of that type before filtering down to the cast. --- .../RULE-10-5/InappropriateEssentialTypeCast.ql | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) 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() From fdd1d5c6553bf06d1a761197e03ae02276f272fa Mon Sep 17 00:00:00 2001 From: Luke Cartey Date: Thu, 16 Mar 2023 18:12:49 +0000 Subject: [PATCH 3/4] EssentialTypes: Avoid recalculation of essential types --- c/misra/src/codingstandards/c/misra/EssentialTypes.qll | 1 + 1 file changed, 1 insertion(+) diff --git a/c/misra/src/codingstandards/c/misra/EssentialTypes.qll b/c/misra/src/codingstandards/c/misra/EssentialTypes.qll index ceba70fbfb..9bec0e518f 100644 --- a/c/misra/src/codingstandards/c/misra/EssentialTypes.qll +++ b/c/misra/src/codingstandards/c/misra/EssentialTypes.qll @@ -146,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 From bc4db01e757d481856bffd56f8e4ac664462f70b Mon Sep 17 00:00:00 2001 From: Luke Cartey Date: Fri, 17 Mar 2023 13:12:36 +0000 Subject: [PATCH 4/4] Add a change note. --- .../2023-03-16-essential-types-performance.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 change_notes/2023-03-16-essential-types-performance.md 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