Skip to content

Commit

Permalink
Merge pull request #622 from knewbury01/knewbury01/fix-376
Browse files Browse the repository at this point in the history
M0-1-2: improve template handling
  • Loading branch information
knewbury01 authored Jun 14, 2024
2 parents 90abc2d + 7697c69 commit 6714fe7
Show file tree
Hide file tree
Showing 4 changed files with 224 additions and 18 deletions.
2 changes: 2 additions & 0 deletions change_notes/2024-06-11-fix-fp-376-M-0-1-2.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
- `M0-1-2` - `InfeasiblePath.ql`:
- Fixes #376. For template functions we now only report when a path is infeasible regardless of instantiations present.
193 changes: 184 additions & 9 deletions cpp/autosar/src/rules/M0-1-2/InfeasiblePath.ql
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@
import cpp
import codingstandards.cpp.autosar
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
import codingstandards.cpp.deadcode.UnreachableCode
import semmle.code.cpp.controlflow.Guards

/**
* A "conditional" node in the control flow graph, i.e. one that can potentially have a true and false path.
Expand Down Expand Up @@ -44,6 +46,7 @@ class BreakingLoop extends Loop {
predicate hasCFGDeducedInfeasiblePath(
ConditionalControlFlowNode cond, boolean infeasiblePath, string explanation
) {
not cond.isFromTemplateInstantiation(_) and
// No true successor, so the true path has already been deduced as infeasible
not exists(cond.getATrueSuccessor()) and
infeasiblePath = true and
Expand Down Expand Up @@ -147,17 +150,189 @@ predicate isConstantRelationalOperation(
/**
* Holds if the `ConditionalNode` has an infeasible `path` for the reason given in `explanation`.
*/
predicate hasInfeasiblePath(
ConditionalControlFlowNode node, boolean infeasiblePath, string explanation
) {
hasCFGDeducedInfeasiblePath(node, infeasiblePath, explanation) and
not isConstantRelationalOperation(node, infeasiblePath, _)
predicate hasInfeasiblePath(ConditionalControlFlowNode node, string message) {
//deal with the infeasible in all uninstantiated templates separately
node.isFromUninstantiatedTemplate(_) and
node instanceof ConditionControllingUnreachable and
message = "The path is unreachable in a template."
or
isConstantRelationalOperation(node, infeasiblePath, explanation)
exists(boolean infeasiblePath, string explanation |
(
not node.isFromUninstantiatedTemplate(_) and
not node.isFromTemplateInstantiation(_) and
message = "The " + infeasiblePath + " path is infeasible because " + explanation + "."
) and
(
hasCFGDeducedInfeasiblePath(node, infeasiblePath, explanation) and
not isConstantRelationalOperation(node, infeasiblePath, _)
or
isConstantRelationalOperation(node, infeasiblePath, explanation)
)
)
}

/**
* A newtype representing "unreachable" blocks in the program. We use a newtype here to avoid
* reporting the same block in multiple `Function` instances created from one function in a template.
*/
private newtype TUnreachableBasicBlock =
TUnreachableNonTemplateBlock(BasicBlock bb) {
bb.isUnreachable() and
// Exclude anything template related from this case
not bb.getEnclosingFunction().isFromTemplateInstantiation(_) and
not bb.getEnclosingFunction().isFromUninstantiatedTemplate(_) and
// Exclude compiler generated basic blocks
not isCompilerGenerated(bb)
} or
/**
* A `BasicBlock` that occurs in at least one `Function` instance for a template. `BasicBlock`s
* are matched up across templates by location.
*/
TUnreachableTemplateBlock(
string filepath, int startline, int startcolumn, int endline, int endcolumn,
GuardCondition uninstantiatedGuardCondition
) {
exists(BasicBlock bb |
// BasicBlock occurs in this location
bb.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
// And is contained in the `uninstantiatedFunction` only
// not from anything constructed from it
// because we want infeasible paths independent of parameters
exists(Function enclosing | enclosing = bb.getEnclosingFunction() |
//guard is in the template function
(
enclosing.getBlock().getAChild*() = uninstantiatedGuardCondition and
//function template
enclosing.isFromUninstantiatedTemplate(_) and
uninstantiatedGuardCondition.isFromUninstantiatedTemplate(_) and
//true condition is unreachable: basic block starts on same line as guard
(
not exists(uninstantiatedGuardCondition.getATrueSuccessor()) and
bb.hasLocationInfo(filepath, uninstantiatedGuardCondition.getLocation().getStartLine(),
startcolumn, endline, endcolumn)
or
//false condition is unreachable: false basic block starts on one line after its true basic block
not exists(uninstantiatedGuardCondition.getAFalseSuccessor()) and
bb.hasLocationInfo(filepath,
uninstantiatedGuardCondition.getATrueSuccessor().getLocation().getEndLine() + 1,
startcolumn, endline, endcolumn)
)
)
) and
// And is unreachable
bb.isUnreachable() and
// //Exclude compiler generated control flow nodes
not isCompilerGenerated(bb) and
//Exclude nodes affected by macros, because our find-the-same-basic-block-by-location doesn't
//work in that case
not bb.(ControlFlowNode).isAffectedByMacro()
)
}

/**
* An unreachable basic block.
*/
class UnreachableBasicBlock extends TUnreachableBasicBlock {
/** Gets a `BasicBlock` which is represented by this set of unreachable basic blocks. */
BasicBlock getABasicBlock() { none() }

/** Gets a `GuardCondition` instance which we treat as the original GuardCondition. */
GuardCondition getGuardCondition() { none() }

predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
none()
}

string toString() { result = "default" }
}

/**
* A non-templated unreachable basic block.
*/
class UnreachableNonTemplateBlock extends UnreachableBasicBlock, TUnreachableNonTemplateBlock {
BasicBlock getBasicBlock() { this = TUnreachableNonTemplateBlock(result) }

override BasicBlock getABasicBlock() { result = getBasicBlock() }

override GuardCondition getGuardCondition() { result.controls(getBasicBlock(), true) }

override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
getBasicBlock().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}

override string toString() { result = getBasicBlock().toString() }
}

/**
* A templated unreachable basic block.
*/
class UnreachableTemplateBlock extends UnreachableBasicBlock, TUnreachableTemplateBlock {
override BasicBlock getABasicBlock() {
exists(
string filepath, int startline, int startcolumn, int endline, int endcolumn,
GuardCondition uninstantiatedGuardCondition
|
this =
TUnreachableTemplateBlock(filepath, startline, startcolumn, endline, endcolumn,
uninstantiatedGuardCondition) and
result.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
exists(Function enclosing |
//guard is in the template function
(
enclosing.getBlock().getAChild*() = uninstantiatedGuardCondition and
//function template
enclosing.isFromUninstantiatedTemplate(_) and
uninstantiatedGuardCondition.isFromUninstantiatedTemplate(_) and
//true condition is unreachable: basic block starts on same line as guard
(
not exists(uninstantiatedGuardCondition.getATrueSuccessor()) and
this.hasLocationInfo(filepath,
uninstantiatedGuardCondition.getLocation().getStartLine(), startcolumn, endline,
endcolumn)
or
//false condition is unreachable: false basic block starts on one line after its true basic block
not exists(uninstantiatedGuardCondition.getAFalseSuccessor()) and
this.hasLocationInfo(filepath,
uninstantiatedGuardCondition.getATrueSuccessor().getLocation().getEndLine() + 1,
startcolumn, endline, endcolumn)
)
)
)
|
result.isUnreachable() and
// Exclude compiler generated control flow nodes
not isCompilerGenerated(result) and
// Exclude nodes affected by macros, because our find-the-same-basic-block-by-location doesn't
// work in that case
not result.(ControlFlowNode).isAffectedByMacro()
)
}

override GuardCondition getGuardCondition() {
this = TUnreachableTemplateBlock(_, _, _, _, _, result)
}

override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this = TUnreachableTemplateBlock(filepath, startline, startcolumn, endline, endcolumn, _)
}

override string toString() { result = getABasicBlock().toString() }
}

class ConditionControllingUnreachable extends GuardCondition {
ConditionControllingUnreachable() {
exists(UnreachableTemplateBlock b | this = b.getGuardCondition())
}
}

from ConditionalControlFlowNode cond, boolean infeasiblePath, string explanation
from ConditionalControlFlowNode cond, string explanation
where
not isExcluded(cond, DeadCodePackage::infeasiblePathQuery()) and
hasInfeasiblePath(cond, infeasiblePath, explanation)
select cond, "The " + infeasiblePath + " path is infeasible because " + explanation + "."
hasInfeasiblePath(cond, explanation)
select cond, explanation
10 changes: 3 additions & 7 deletions cpp/autosar/test/rules/M0-1-2/InfeasiblePath.expected
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,9 @@
| test.cpp:7:7:7:22 | ... <= ... | The false path is infeasible because a (max value: 4294967295) is always less than or equal to 4294967295 (minimum value: 4294967295). |
| test.cpp:15:7:15:13 | ... < ... | The false path is infeasible because l1 (max value: 2) is always less than l2 (minimum value: 10). |
| test.cpp:19:9:19:14 | ... < ... | The false path is infeasible because a (max value: 1) is always less than l2 (minimum value: 10). |
| test.cpp:33:7:33:7 | 0 | The true path is infeasible because this expression consists of constants which evaluate to false. |
| test.cpp:33:7:33:7 | 0 | The true path is infeasible because this expression consists of constants which evaluate to false. |
| test.cpp:33:7:33:7 | 0 | The true path is infeasible because this expression consists of constants which evaluate to false. |
| test.cpp:36:7:36:14 | call to isVal | The false path is infeasible because this expression consists of constants which evaluate to true. |
| test.cpp:36:7:36:14 | call to isVal | The false path is infeasible because this expression consists of constants which evaluate to true. |
| test.cpp:43:7:43:15 | call to isVal2 | The false path is infeasible because this expression consists of constants which evaluate to true. |
| test.cpp:43:7:43:15 | call to isVal2 | The true path is infeasible because this expression consists of constants which evaluate to false. |
| test.cpp:33:7:33:7 | 0 | The path is unreachable in a template. |
| test.cpp:77:9:77:14 | ... < ... | The true path is infeasible because 0 (max value: 0) is always less than or equal to a (minimum value: 0). |
| test.cpp:80:9:80:15 | ... >= ... | The false path is infeasible because 0 (max value: 0) is always less than or equal to a (minimum value: 0). |
| test.cpp:86:9:86:14 | ... < ... | The true path is infeasible because 0 (max value: 0) is always less than or equal to a (minimum value: 0). |
| test.cpp:117:7:117:7 | 0 | The path is unreachable in a template. |
| test.cpp:123:7:123:8 | ! ... | The path is unreachable in a template. |
37 changes: 35 additions & 2 deletions cpp/autosar/test/rules/M0-1-2/test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -33,14 +33,14 @@ template <class T> int f() {
if (0) { // NON_COMPLIANT - true path is infeasible in all circumstances
return 3;
}
if (T::isVal()) { // COMPLIANT[FALSE_POSITIVE] - `isVal` is `true` for all
if (T::isVal()) { // COMPLIANT - `isVal` is `true` for all
// visible instantiations, but in the uninstantiated
// template both paths are feasible. This represents that
// this is template dependent, so we consider it compliant
return 2;
}

if (T::isVal2()) { // COMPLIANT[FALSE_POSITIVE] - `isVal2` is either true or
if (T::isVal2()) { // COMPLIANT - `isVal2` is either true or
// false
return 2;
}
Expand Down Expand Up @@ -99,3 +99,36 @@ void test_loop(int a) {
a++;
}
}

template <bool x> int foo() {
if (x) { // COMPLIANT - block is reachable in the one of the instantiated
// template
return 1;
}
return 0; // COMPLIANT - block is reachable in the uninstantiated template
}

void test() {
foo<true>();
foo<false>();
}

template <class T> int template_infeasible_true_path() {
if (0) { // NON_COMPLIANT - true path is infeasible in all circumstances
return 3;
}
}

template <class T> int template_infeasible_false_path() {
if (!0) {
return 3;
}
return 1; // NON_COMPLIANT - false path is infeasible in all circumstances
}

void test_infeasible_instantiates() {
template_infeasible_true_path<A>();
template_infeasible_true_path<B>();
template_infeasible_false_path<A>();
template_infeasible_false_path<B>();
}

0 comments on commit 6714fe7

Please sign in to comment.