Fixing typos & implementing the PR feedback

This commit is contained in:
Raul Garcia
2018-10-18 14:44:24 -07:00
parent ce99f469a9
commit e2fcaa9e20
5 changed files with 116 additions and 43 deletions

View File

@@ -9,7 +9,7 @@
</overview>
<recommendation>
<p>Verify the iteration expression on the <code>for-loop</code> and make sure the direction of the iteration expression is correct.</p>
<p>To fix this issue, check that the loop condition is correct and change the iteration expression to match.</p>
</recommendation>
<example>

View File

@@ -10,58 +10,56 @@
*/
import cpp
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
import semmle.code.cpp.dataflow.DataFlow
predicate illDefinedDecrForStmt( ForStmt forstmt, Variable v, Expr initialCondition, Expr terminalCondition ) {
v.getAnAssignedValue() = initialCondition
v.getAnAssignedValue() = initialCondition
and
exists(
RelationalOperation rel, Expr e |
RelationalOperation rel |
rel = forstmt.getCondition() |
e = rel.getGreaterOperand()
terminalCondition = rel.getGreaterOperand()
and v.getAnAccess() = rel.getLesserOperand()
and terminalCondition = e
)
and
(
exists(
PostfixDecrExpr pdec |
pdec = forstmt.getUpdate().(PostfixDecrExpr)
and pdec.getAnOperand() = v.getAnAccess()
) or
exists(
PrefixDecrExpr pdec |
pdec = forstmt.getUpdate().(PrefixDecrExpr)
and pdec.getAnOperand() = v.getAnAccess()
and
DataFlow::localFlowStep(DataFlow::exprNode(initialCondition), DataFlow::exprNode(rel.getLesserOperand()))
)
and
exists(
DecrementOperation dec |
dec = forstmt.getUpdate().(DecrementOperation)
and dec.getAnOperand() = v.getAnAccess()
)
and
upperBound(initialCondition) < lowerBound(terminalCondition)
(
( upperBound(initialCondition) < lowerBound(terminalCondition) )
or
( forstmt.conditionAlwaysFalse() or forstmt.conditionAlwaysTrue() )
)
}
predicate illDefinedIncrForStmt( ForStmt forstmt, Variable v, Expr initialCondition, Expr terminalCondition ) {
v.getAnAssignedValue() = initialCondition
and
exists(
RelationalOperation rel, Expr e |
RelationalOperation rel |
rel = forstmt.getCondition() |
e = rel.getLesserOperand()
terminalCondition = rel.getLesserOperand()
and v.getAnAccess() = rel.getGreaterOperand()
and terminalCondition = e
and
DataFlow::localFlowStep(DataFlow::exprNode(initialCondition), DataFlow::exprNode(rel.getGreaterOperand()))
)
and
( exists( PostfixIncrExpr pincr |
pincr = forstmt.getUpdate().(PostfixIncrExpr)
and
pincr.getAnOperand() = v.getAnAccess()
) or
exists( PrefixIncrExpr pincr |
pincr = forstmt.getUpdate().(PrefixIncrExpr)
and
pincr.getAnOperand() = v.getAnAccess()
)
exists( IncrementOperation incr |
incr = forstmt.getUpdate().(IncrementOperation)
and
incr.getAnOperand() = v.getAnAccess()
)
and
upperBound(terminalCondition) < lowerBound(initialCondition)
(
( upperBound(terminalCondition) < lowerBound(initialCondition))
or
( forstmt.conditionAlwaysFalse() or forstmt.conditionAlwaysTrue())
)
}
predicate illDefinedForStmtWrongDirection( ForStmt forstmt, Variable v, Expr initialCondition, Expr terminalCondition
@@ -91,9 +89,23 @@ private string forLoopTerminalConditionRelationship(boolean b){
Expr terminalCondition |
illDefinedForStmtWrongDirection(for, v, initialCondition, terminalCondition, isIncr)
and
message = "Ill-defined for-loop: a loop using variable \"" + v + "\" counts "
+ forLoopdirection(isIncr) + " from a value ("+ initialCondition +"), but the terminal condition is "
+ forLoopTerminalConditionRelationship(isIncr) + " (" + terminalCondition + ")."
if( for.conditionAlwaysFalse() ) then
(
message = "Ill-defined for-loop: a loop using variable \"" + v + "\" counts "
+ forLoopdirection(isIncr) + " from a value ("+ initialCondition +"), but the terminal condition is always false."
)
else if
(
for.conditionAlwaysTrue() ) then (
message = "Ill-defined for-loop: a loop using variable \"" + v + "\" counts "
+ forLoopdirection(isIncr) + " from a value ("+ initialCondition +"), but the terminal condition is always true."
)
else
(
message = "Ill-defined for-loop: a loop using variable \"" + v + "\" counts "
+ forLoopdirection(isIncr) + " from a value ("+ initialCondition +"), but the terminal condition is "
+ forLoopTerminalConditionRelationship(isIncr) + " (" + terminalCondition + ")."
)
)
}

View File

@@ -43,19 +43,19 @@ void Unsigned()
void DeclarationInLoop()
{
for (signed char i = 0; i < 100; i--) //BUG
for (signed char i = 0; i < 100; --i) //BUG
{
}
for (signed char i = 0; i < 100; i++)
for (signed char i = 0; i < 100; ++i)
{
}
for (unsigned char i = 100; i >= 0; i++) //BUG
for (unsigned char i = 100; i >= 0; ++i) //BUG
{
}
for (unsigned char i = 100; i >= 0; i--)
for (unsigned char i = 100; i >= 0; --i)
{
}
}
@@ -88,22 +88,56 @@ void InitializationOutsideLoop()
{
signed char i = 0;
for (; i < 100; i--) //BUG
for (; i < 100; --i) //BUG
{
}
i = 0;
for (; i < 100; i++)
for (; i < 100; ++i)
{
}
i = 100;
for (; i >= 0; i++) //BUG
for (; i >= 0; ++i) //BUG
{
}
i = 100;
for (; i >= 0; i--)
for (; i >= 0; --i)
{
}
}
void InvalidCondition()
{
signed char i;
signed char min = 0;
signed char max = 100;
for (i = max; i < min; i--) //BUG
{
}
for (i = min; i > max; i++) //BUG
{
}
}
void InvalidConditionUnsignedCornerCase()
{
unsigned char i;
unsigned char min = 0;
unsigned char max = 100;
for (i = 100; i < 0; i--) //BUG
{
}
// Limitation.
// Currently odasa will not detect this for-loop condition as always true
// The rule will still detect the mismatch iterator, but the error message may change in the future.
for (i = 200; i >= 0; i++) //BUG
{
}
}
@@ -126,3 +160,21 @@ void NegativeTestCaseNested()
}
}
}
//////////////////////////////////////
// Query limitation:
//
// The following test cases are bugs,
// but will not be found due to the itearion expression
// not being a prefix or postfix increment/decrement
//
void FalseNegativeTestCases()
{
for (int i = 0; i < 10; i = i - 1) {}
// For comparison
for (int i = 0; i < 10; i-- ) {} // BUG
for (int i = 100; i > 0; i += 2) {}
// For comparison
for (int i = 100; i > 0; i ++ ) {} // BUG
}

View File

@@ -14,3 +14,9 @@
| illDefinedForLoop.cpp:77:5:79:5 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts upward from a value (max), but the terminal condition is lower (min). |
| illDefinedForLoop.cpp:91:5:93:5 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts downward from a value (0), but the terminal condition is higher (100). |
| illDefinedForLoop.cpp:101:5:103:5 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts upward from a value (100), but the terminal condition is lower (0). |
| illDefinedForLoop.cpp:118:5:120:5 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts downward from a value (max), but the terminal condition is always false. |
| illDefinedForLoop.cpp:122:5:124:5 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts upward from a value (min), but the terminal condition is always false. |
| illDefinedForLoop.cpp:133:5:135:5 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts downward from a value (100), but the terminal condition is always false. |
| illDefinedForLoop.cpp:140:5:142:5 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts upward from a value (200), but the terminal condition is lower (0). |
| illDefinedForLoop.cpp:175:5:175:36 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts downward from a value (0), but the terminal condition is higher (10). |
| illDefinedForLoop.cpp:179:5:179:38 | for(...;...;...) ... | Ill-defined for-loop: a loop using variable "i" counts upward from a value (100), but the terminal condition is lower (0). |