Skip to content

Commit ab04b8f

Browse files
MichaelRFairhurstMichaelRFairhurst
authored
Merge pull request #1003 from github/michaelrfairhurst/deadcode-4-rule-0-0-2
First implementation of Rule-0-0-2, invariant conditions.
2 parents 8c86c07 + bd7bc2f commit ab04b8f

File tree

12 files changed

+423
-141
lines changed

12 files changed

+423
-141
lines changed

‎change_notes/2025-12-17-unfeasible-statement-refactor.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
- `M0-1-2` - `InfeasiblePath.ql`:
2+
- Refactored to share logic with `RULE-0-0-2` while allowing for different exceptional cases. No change in behavior expected.

‎cpp/autosar/src/rules/M0-1-2/InfeasiblePath.ql‎

Lines changed: 14 additions & 140 deletions
Original file line numberDiff line numberDiff line change
@@ -16,22 +16,7 @@
1616

1717
import cpp
1818
import codingstandards.cpp.autosar
19-
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
20-
import codingstandards.cpp.deadcode.UnreachableCode
21-
import semmle.code.cpp.controlflow.Guards
22-
23-
/**
24-
* A "conditional" node in the control flow graph, i.e. one that can potentially have a true and false path.
25-
*/
26-
class ConditionalControlFlowNode extends ControlFlowNode {
27-
ConditionalControlFlowNode() {
28-
// A conditional node is one with at least one of a true or false successor
29-
(exists(getATrueSuccessor()) or exists(getAFalseSuccessor())) and
30-
// Ignore conditions affected by macros, as they may include deliberate infeasible paths, or
31-
// paths which are only feasible in certain macro expansions
32-
not isAffectedByMacro()
33-
}
34-
}
19+
import codingstandards.cpp.rules.invariantcondition.InvariantCondition
3520

3621
/**
3722
* A `Loop` that contains a `break` statement.
@@ -40,132 +25,21 @@ class BreakingLoop extends Loop {
4025
BreakingLoop() { exists(BreakStmt break | this = break.getBreakable()) }
4126
}
4227

43-
/**
44-
* Holds if the `ConditionalNode` has an infeasible `path` according to the control flow graph library.
45-
*/
46-
predicate hasCFGDeducedInfeasiblePath(
47-
ConditionalControlFlowNode cond, boolean infeasiblePath, string explanation
48-
) {
49-
not cond.isFromTemplateInstantiation(_) and
50-
// No true successor, so the true path has already been deduced as infeasible
51-
not exists(cond.getATrueSuccessor()) and
52-
infeasiblePath = true and
53-
explanation = "this expression consists of constants which evaluate to false"
54-
or
55-
// No false successor, so false path has already been deduced as infeasible
56-
not exists(cond.getAFalseSuccessor()) and
57-
not cond.getEnclosingStmt() instanceof BreakingLoop and
58-
infeasiblePath = false and
59-
explanation = "this expression consists of constants which evaluate to true"
60-
}
61-
62-
predicate isConstantRelationalOperation(
63-
RelationalOperation rel, boolean infeasiblePath, string explanation
64-
) {
65-
/*
66-
* This predicate identifies a number of a cases where we can conclusive determine that a relational
67-
* operation will always return true or false, based on the ranges for each operand as determined
68-
* by the SimpleRangeAnalysis library (and any extensions provide in the Coding Standards library).
69-
*
70-
* Important note: in order to deduce that an relational operation _always_ returns true or false,
71-
* we must ensure that it returns true or false for _all_ possible values of the operands. For
72-
* example, it may be tempting to look at this relational operation on these ranges:
73-
* ```
74-
* [0..5] < [0..10]
75-
* ```
76-
* And say that ub(lesser) < ub(greater) and therefore it is `true`, however this is not the case
77-
* for all permutations (e.g. 5 < 0).
78-
*
79-
* Instead, we look at all four permutations of these two dimensions:
80-
* - Equal-to or not equal-to
81-
* - Always true or always false
82-
*/
28+
module AutosarConfig implements InvariantConditionConfigSig {
29+
Query getQuery() { result = DeadCodePackage::infeasiblePathQuery() }
8330

84-
// This restricts the comparison to occur directly within the conditional node
85-
// In theory we could also extend this to identify comparisons where the result is stored, then
86-
// later read in a conditional control flow node within the same function (using SSA)
87-
// Doing so would benefit from path explanations, but would require a more complex analysis
88-
rel instanceof ConditionalControlFlowNode and
89-
// If at least one operand includes an access of a volatile variable, the range analysis library may
90-
// provide inaccurate results, so we ignore this case
91-
not rel.getAnOperand().getAChild*().(VariableAccess).getTarget().isVolatile() and
92-
exists(boolean isEqual |
93-
if
94-
rel instanceof GEExpr
95-
or
96-
rel instanceof LEExpr
97-
then isEqual = true
98-
else isEqual = false
99-
|
100-
// Not equal-to/always true
101-
// If the largest value of the lesser operand is less than the smallest value of the greater
102-
// operand, then the LT/GT comparison is always true
103-
// Example: [0..5] < [6..10]
104-
upperBound(rel.getLesserOperand()) < lowerBound(rel.getGreaterOperand()) and
105-
explanation =
106-
rel.getLesserOperand() + " (max value: " + upperBound(rel.getLesserOperand()) +
107-
") is always less than " + rel.getGreaterOperand() + " (minimum value: " +
108-
lowerBound(rel.getGreaterOperand()) + ")" and
109-
isEqual = false and
110-
infeasiblePath = false
111-
or
112-
// Equal-to/always true
113-
// If the largest value of the lesser operand is less than or equal to the smallest value of the
114-
// greater operand, then the LTE/GTE comparison is always true
115-
// Example: [0..6] <= [6..10]
116-
upperBound(rel.getLesserOperand()) <= lowerBound(rel.getGreaterOperand()) and
117-
explanation =
118-
rel.getLesserOperand() + " (max value: " + upperBound(rel.getLesserOperand()) +
119-
") is always less than or equal to " + rel.getGreaterOperand() + " (minimum value: " +
120-
lowerBound(rel.getGreaterOperand()) + ")" and
121-
isEqual = true and
122-
infeasiblePath = false
123-
or
124-
// Equal to/always false
125-
// If the largest value of the greater operand is less than the smallest value of the lesser
126-
// operand, then the LTE/GTE comparison is always false
127-
// Example: [6..10] <= [0..5]
128-
upperBound(rel.getGreaterOperand()) < lowerBound(rel.getLesserOperand()) and
129-
explanation =
130-
rel.getGreaterOperand() + " (max value: " + upperBound(rel.getGreaterOperand()) +
131-
") is always less than " + rel.getLesserOperand() + " (minimum value: " +
132-
lowerBound(rel.getLesserOperand()) + ")" and
133-
isEqual = true and
134-
infeasiblePath = true
31+
predicate isException(ControlFlowNode node) {
32+
node.getEnclosingElement() instanceof BreakingLoop and
33+
exists(node.getATrueSuccessor())
13534
or
136-
// Equal to/always true
137-
// If the largest value of the greater operand is less than or equal to the smallest value of the
138-
// lesser operand, then the LT/GT comparison is always false
139-
// Example: [6..10] < [0..6]
140-
upperBound(rel.getGreaterOperand()) <= lowerBound(rel.getLesserOperand()) and
141-
explanation =
142-
rel.getGreaterOperand() + " (max value: " + upperBound(rel.getGreaterOperand()) +
143-
") is always less than or equal to " + rel.getLesserOperand() + " (minimum value: " +
144-
lowerBound(rel.getLesserOperand()) + ")" and
145-
isEqual = false and
146-
infeasiblePath = true
147-
)
148-
}
149-
150-
/**
151-
* Holds if the `ConditionalNode` has an infeasible `path` for the reason given in `explanation`.
152-
*/
153-
predicate hasInfeasiblePath(ConditionalControlFlowNode node, string message) {
154-
exists(boolean infeasiblePath, string explanation |
155-
not node.isFromTemplateInstantiation(_) and
156-
if node.isFromUninstantiatedTemplate(_)
157-
then message = "The path is unreachable in a template."
158-
else message = "The " + infeasiblePath + " path is infeasible because " + explanation + "."
159-
|
160-
hasCFGDeducedInfeasiblePath(node, infeasiblePath, explanation) and
161-
not isConstantRelationalOperation(node, infeasiblePath, _)
35+
// Ignore conditions affected by macros, as they may include deliberate infeasible paths, or
36+
// paths which are only feasible in certain macro expansions
37+
node.isAffectedByMacro()
16238
or
163-
isConstantRelationalOperation(node, infeasiblePath, explanation)
164-
)
39+
// Only consider reachability in uninstantiated templates, to avoid false positives
40+
node.isFromTemplateInstantiation(_)
41+
}
16542
}
16643

167-
from ConditionalControlFlowNode cond, string explanation
168-
where
169-
not isExcluded(cond, DeadCodePackage::infeasiblePathQuery()) and
170-
hasInfeasiblePath(cond, explanation)
171-
select cond, explanation
44+
// Import the problems query predicate
45+
import InvariantCondition<AutosarConfig>

‎cpp/common/src/codingstandards/cpp/Literals.qll‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,10 @@ class BoolLiteral extends Literal {
6969
or
7070
this.getValue() = "0" and this.getValueText() = "false"
7171
}
72+
73+
predicate isTrue() { this.getValue() = "1" }
74+
75+
predicate isFalse() { this.getValue() = "0" }
7276
}
7377

7478
/**

‎cpp/common/src/codingstandards/cpp/exclusions/cpp/DeadCode4.qll‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY. **/
2+
import cpp
3+
import RuleMetadata
4+
import codingstandards.cpp.exclusions.RuleMetadata
5+
6+
newtype DeadCode4Query = TInvariantConditionQuery()
7+
8+
predicate isDeadCode4QueryMetadata(Query query, string queryId, string ruleId, string category) {
9+
query =
10+
// `Query` instance for the `invariantCondition` query
11+
DeadCode4Package::invariantConditionQuery() and
12+
queryId =
13+
// `@id` for the `invariantCondition` query
14+
"cpp/misra/invariant-condition" and
15+
ruleId = "RULE-0-0-2" and
16+
category = "advisory"
17+
}
18+
19+
module DeadCode4Package {
20+
Query invariantConditionQuery() {
21+
//autogenerate `Query` type
22+
result =
23+
// `Query` type for `invariantCondition` query
24+
TQueryCPP(TDeadCode4PackageQuery(TInvariantConditionQuery()))
25+
}
26+
}

‎cpp/common/src/codingstandards/cpp/exclusions/cpp/RuleMetadata.qll‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ import Conversions
1818
import Conversions2
1919
import DeadCode
2020
import DeadCode3
21+
import DeadCode4
2122
import Declarations
2223
import ExceptionSafety
2324
import Exceptions1
@@ -88,6 +89,7 @@ newtype TCPPQuery =
8889
TConversions2PackageQuery(Conversions2Query q) or
8990
TDeadCodePackageQuery(DeadCodeQuery q) or
9091
TDeadCode3PackageQuery(DeadCode3Query q) or
92+
TDeadCode4PackageQuery(DeadCode4Query q) or
9193
TDeclarationsPackageQuery(DeclarationsQuery q) or
9294
TExceptionSafetyPackageQuery(ExceptionSafetyQuery q) or
9395
TExceptions1PackageQuery(Exceptions1Query q) or
@@ -158,6 +160,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat
158160
isConversions2QueryMetadata(query, queryId, ruleId, category) or
159161
isDeadCodeQueryMetadata(query, queryId, ruleId, category) or
160162
isDeadCode3QueryMetadata(query, queryId, ruleId, category) or
163+
isDeadCode4QueryMetadata(query, queryId, ruleId, category) or
161164
isDeclarationsQueryMetadata(query, queryId, ruleId, category) or
162165
isExceptionSafetyQueryMetadata(query, queryId, ruleId, category) or
163166
isExceptions1QueryMetadata(query, queryId, ruleId, category) or

‎cpp/common/src/codingstandards/cpp/rules/invariantcondition/InvariantCondition.qll‎

Lines changed: 163 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,163 @@
1+
/**
2+
* Provides a library which includes a `problems` predicate for reporting
3+
* invariant/infeasible code paths.
4+
*/
5+
6+
import cpp
7+
import codingstandards.cpp.Customizations
8+
import codingstandards.cpp.Exclusions
9+
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
10+
import codingstandards.cpp.deadcode.UnreachableCode
11+
import semmle.code.cpp.controlflow.Guards
12+
13+
signature module InvariantConditionConfigSig {
14+
Query getQuery();
15+
16+
predicate isException(ControlFlowNode element);
17+
}
18+
19+
private module Impl {
20+
/**
21+
* A "conditional" node in the control flow graph, i.e. one that can potentially have a true and
22+
* false path.
23+
*/
24+
class ConditionalControlFlowNode extends ControlFlowNode {
25+
ConditionalControlFlowNode() {
26+
// A conditional node is one with at least one of a true or false successor
27+
(exists(getATrueSuccessor()) or exists(getAFalseSuccessor()))
28+
}
29+
}
30+
31+
/**
32+
* Holds if the `ConditionalNode` has an infeasible `path` according to the control flow graph
33+
* library.
34+
*/
35+
predicate hasCFGDeducedInfeasiblePath(
36+
ConditionalControlFlowNode cond, boolean infeasiblePath, string explanation
37+
) {
38+
not cond.isFromTemplateInstantiation(_) and
39+
// No true successor, so the true path has already been deduced as infeasible
40+
not exists(cond.getATrueSuccessor()) and
41+
infeasiblePath = true and
42+
explanation = "this expression consists of constants which evaluate to false"
43+
or
44+
// No false successor, so false path has already been deduced as infeasible
45+
not exists(cond.getAFalseSuccessor()) and
46+
infeasiblePath = false and
47+
explanation = "this expression consists of constants which evaluate to true"
48+
}
49+
50+
predicate isConstantRelationalOperation(
51+
RelationalOperation rel, boolean infeasiblePath, string explanation
52+
) {
53+
/*
54+
* This predicate identifies a number of cases where we can conclusive determine that a
55+
* relational operation will always return true or false, based on the ranges for each operand
56+
* as determined by the SimpleRangeAnalysis library (and any extensions provided in the Coding
57+
* Standards library).
58+
*
59+
* Important note: in order to deduce that a relational operation _always_ returns true or
60+
* false, we must ensure that it returns true or false for _all_ possible values of the
61+
* operands. For example, it may be tempting to look at this relational operation on these
62+
* ranges:
63+
* ```
64+
* [0..5] < [0..10]
65+
* ```
66+
* And say that ub(lesser) < ub(greater) and therefore it is `true`, however this is not the
67+
* case for all permutations (e.g. 5 < 0).
68+
*
69+
* Instead, we look at all four permutations of these two dimensions:
70+
* - Equal-to or not equal-to
71+
* - Always true or always false
72+
*/
73+
74+
// This restricts the comparison to occur directly within the conditional node
75+
// In theory we could also extend this to identify comparisons where the result is stored, then
76+
// later read in a conditional control flow node within the same function (using SSA)
77+
// Doing so would benefit from path explanations, but would require a more complex analysis
78+
rel instanceof ConditionalControlFlowNode and
79+
// If at least one operand includes an access of a volatile variable, the range analysis library
80+
// may provide inaccurate results, so we ignore this case
81+
not rel.getAnOperand().getAChild*().(VariableAccess).getTarget().isVolatile() and
82+
exists(boolean isEqual |
83+
if
84+
rel instanceof GEExpr
85+
or
86+
rel instanceof LEExpr
87+
then isEqual = true
88+
else isEqual = false
89+
|
90+
// Not equal-to/always true
91+
// If the largest value of the lesser operand is less than the smallest value of the greater
92+
// operand, then the LT/GT comparison is always true
93+
// Example: [0..5] < [6..10]
94+
upperBound(rel.getLesserOperand()) < lowerBound(rel.getGreaterOperand()) and
95+
explanation =
96+
rel.getLesserOperand() + " (max value: " + upperBound(rel.getLesserOperand()) +
97+
") is always less than " + rel.getGreaterOperand() + " (minimum value: " +
98+
lowerBound(rel.getGreaterOperand()) + ")" and
99+
isEqual = false and
100+
infeasiblePath = false
101+
or
102+
// Equal-to/always true
103+
// If the largest value of the lesser operand is less than or equal to the smallest value of
104+
// the greater operand, then the LTE/GTE comparison is always true
105+
// Example: [0..6] <= [6..10]
106+
upperBound(rel.getLesserOperand()) <= lowerBound(rel.getGreaterOperand()) and
107+
explanation =
108+
rel.getLesserOperand() + " (max value: " + upperBound(rel.getLesserOperand()) +
109+
") is always less than or equal to " + rel.getGreaterOperand() + " (minimum value: " +
110+
lowerBound(rel.getGreaterOperand()) + ")" and
111+
isEqual = true and
112+
infeasiblePath = false
113+
or
114+
// Equal to/always false
115+
// If the largest value of the greater operand is less than the smallest value of the lesser
116+
// operand, then the LTE/GTE comparison is always false
117+
// Example: [6..10] <= [0..5]
118+
upperBound(rel.getGreaterOperand()) < lowerBound(rel.getLesserOperand()) and
119+
explanation =
120+
rel.getGreaterOperand() + " (max value: " + upperBound(rel.getGreaterOperand()) +
121+
") is always less than " + rel.getLesserOperand() + " (minimum value: " +
122+
lowerBound(rel.getLesserOperand()) + ")" and
123+
isEqual = true and
124+
infeasiblePath = true
125+
or
126+
// Equal to/always false
127+
// If the largest value of the greater operand is less than or equal to the smallest value of
128+
// the lesser operand, then the LT/GT comparison is always false
129+
// Example: [6..10] < [0..6]
130+
upperBound(rel.getGreaterOperand()) <= lowerBound(rel.getLesserOperand()) and
131+
explanation =
132+
rel.getGreaterOperand() + " (max value: " + upperBound(rel.getGreaterOperand()) +
133+
") is always less than or equal to " + rel.getLesserOperand() + " (minimum value: " +
134+
lowerBound(rel.getLesserOperand()) + ")" and
135+
isEqual = false and
136+
infeasiblePath = true
137+
)
138+
}
139+
140+
/**
141+
* Holds if the `ConditionalNode` has an infeasible `path` for the reason given in `explanation`.
142+
*/
143+
predicate hasInfeasiblePath(ConditionalControlFlowNode node, string message) {
144+
exists(boolean infeasiblePath, string explanation |
145+
if node.isFromUninstantiatedTemplate(_)
146+
then message = "The path is unreachable in a template."
147+
else message = "The " + infeasiblePath + " path is infeasible because " + explanation + "."
148+
|
149+
hasCFGDeducedInfeasiblePath(node, infeasiblePath, explanation) and
150+
not isConstantRelationalOperation(node, infeasiblePath, _)
151+
or
152+
isConstantRelationalOperation(node, infeasiblePath, explanation)
153+
)
154+
}
155+
}
156+
157+
module InvariantCondition<InvariantConditionConfigSig Config> {
158+
query predicate problems(Impl::ConditionalControlFlowNode cond, string explanation) {
159+
not isExcluded(cond, Config::getQuery()) and
160+
Impl::hasInfeasiblePath(cond, explanation) and
161+
not Config::isException(cond)
162+
}
163+
}

0 commit comments

Comments
 (0)