Skip to content

Commit 5a5da3c

Browse files
MichaelRFairhurstMichaelRFairhurst
committed
First implementation of Rule-0-0-2, invariant conditions.
1 parent 6c50c4c commit 5a5da3c

File tree

11 files changed

+417
-140
lines changed

11 files changed

+417
-140
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
@@ -16,6 +16,7 @@ import Const
1616
import Conversions
1717
import Conversions2
1818
import DeadCode
19+
import DeadCode4
1920
import Declarations
2021
import ExceptionSafety
2122
import Exceptions1
@@ -78,6 +79,7 @@ newtype TCPPQuery =
7879
TConversionsPackageQuery(ConversionsQuery q) or
7980
TConversions2PackageQuery(Conversions2Query q) or
8081
TDeadCodePackageQuery(DeadCodeQuery q) or
82+
TDeadCode4PackageQuery(DeadCode4Query q) or
8183
TDeclarationsPackageQuery(DeclarationsQuery q) or
8284
TExceptionSafetyPackageQuery(ExceptionSafetyQuery q) or
8385
TExceptions1PackageQuery(Exceptions1Query q) or
@@ -140,6 +142,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat
140142
isConversionsQueryMetadata(query, queryId, ruleId, category) or
141143
isConversions2QueryMetadata(query, queryId, ruleId, category) or
142144
isDeadCodeQueryMetadata(query, queryId, ruleId, category) or
145+
isDeadCode4QueryMetadata(query, queryId, ruleId, category) or
143146
isDeclarationsQueryMetadata(query, queryId, ruleId, category) or
144147
isExceptionSafetyQueryMetadata(query, queryId, ruleId, category) or
145148
isExceptions1QueryMetadata(query, queryId, ruleId, category) or

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

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

0 commit comments

Comments
 (0)