@@ -72,6 +72,60 @@ predicate variableModifiedInExpression(Expr expr, VariableAccess va) {
7272 valueToUpdate ( va , _, expr )
7373}
7474
75+ abstract class LegacyForLoopUpdateExpression extends Expr {
76+ ForStmt forLoop ;
77+
78+ LegacyForLoopUpdateExpression ( ) { this = forLoop .getUpdate ( ) .getAChild * ( ) }
79+
80+ abstract Expr getLoopStep ( ) ;
81+ }
82+
83+ class CrementLegacyForLoopUpdateExpression extends LegacyForLoopUpdateExpression {
84+ CrementLegacyForLoopUpdateExpression ( ) { this instanceof CrementOperation }
85+
86+ override Expr getLoopStep ( ) { none ( ) }
87+ }
88+
89+ class AssignAddOrSubExpr extends LegacyForLoopUpdateExpression {
90+ AssignAddOrSubExpr ( ) {
91+ this instanceof AssignAddExpr or
92+ this instanceof AssignSubExpr
93+ }
94+
95+ override Expr getLoopStep ( ) {
96+ result = this .( AssignAddExpr ) .getRValue ( ) or
97+ result = this .( AssignSubExpr ) .getRValue ( )
98+ }
99+ }
100+
101+ class AddOrSubThenAssignExpr extends LegacyForLoopUpdateExpression {
102+ Expr assignRhs ;
103+
104+ AddOrSubThenAssignExpr ( ) {
105+ this .( AssignExpr ) .getRValue ( ) = assignRhs and
106+ (
107+ assignRhs instanceof AddExpr or
108+ assignRhs instanceof SubExpr
109+ )
110+ }
111+
112+ override Expr getLoopStep ( ) {
113+ (
114+ result = assignRhs .( AddExpr ) .getAnOperand ( ) or
115+ result = assignRhs .( SubExpr ) .getAnOperand ( )
116+ ) and
117+ exists ( VariableAccess iterationVariableAccess |
118+ (
119+ iterationVariableAccess = assignRhs .( AddExpr ) .getAnOperand ( )
120+ or
121+ iterationVariableAccess = assignRhs .( SubExpr ) .getAnOperand ( )
122+ ) and
123+ iterationVariableAccess .getTarget ( ) = forLoop .getAnIterationVariable ( ) and
124+ result != iterationVariableAccess
125+ )
126+ }
127+ }
128+
75129/**
76130 * Gets the loop step of a legacy for loop.
77131 *
@@ -81,8 +135,36 @@ predicate variableModifiedInExpression(Expr expr, VariableAccess va) {
81135 * predicate.
82136 */
83137Expr getLoopStepOfForStmt ( ForStmt forLoop ) {
84- result = forLoop .getUpdate ( ) .( AssignAddExpr ) .getRValue ( ) or
85- result = forLoop .getUpdate ( ) .( AssignSubExpr ) .getRValue ( )
138+ /*
139+ * NOTE: We compute the transitive closure of `getAChild` on the update expression,
140+ * since the update expression may be a compound one that embeds the four aforementioned
141+ * expression types, such as a comma expression (e.g. `i += 1, E` where `E` is an
142+ * arbitrary expression).
143+ *
144+ * This may be detrimental to performance, but we keep it for soundness. A possible
145+ * alternative is an IR-based solution.
146+ */
147+
148+ /* 1. Get the expression `E` when the update expression is `i += E` or `i -= E`. */
149+ result = forLoop .getUpdate ( ) .getAChild * ( ) .( AssignAddExpr ) .getRValue ( )
150+ or
151+ result = forLoop .getUpdate ( ) .getAChild * ( ) .( AssignSubExpr ) .getRValue ( )
152+ or
153+ /* 2. Get the expression `E` when the update expression is `i = i + E` or `i = i - E`. */
154+ (
155+ result = forLoop .getUpdate ( ) .getAChild * ( ) .( AssignExpr ) .getRValue ( ) .( AddExpr ) .getAnOperand ( ) or
156+ result = forLoop .getUpdate ( ) .getAChild * ( ) .( AssignExpr ) .getRValue ( ) .( SubExpr ) .getAnOperand ( )
157+ ) and
158+ exists ( VariableAccess iterationVariableAccess |
159+ (
160+ iterationVariableAccess =
161+ forLoop .getUpdate ( ) .getAChild * ( ) .( AssignExpr ) .getRValue ( ) .( AddExpr ) .getAnOperand ( ) or
162+ iterationVariableAccess =
163+ forLoop .getUpdate ( ) .getAChild * ( ) .( AssignExpr ) .getRValue ( ) .( SubExpr ) .getAnOperand ( )
164+ ) and
165+ iterationVariableAccess .getTarget ( ) = forLoop .getAnIterationVariable ( ) and
166+ result != iterationVariableAccess
167+ )
86168}
87169
88170/**
@@ -184,9 +266,15 @@ private newtype TAlertType =
184266 condition = forLoop .getCondition ( ) and
185267 not condition instanceof LegacyForLoopCondition
186268 } or
187- /* 3. The loop counter is mutated somewhere other than its update expression. */
269+ /* 3-1 . The loop counter is mutated somewhere other than its update expression. */
188270 TLoopCounterMutatedInLoopBody ( ForStmt forLoop , Variable loopCounter ) {
189- isIrregularLoopCounterModification ( forLoop , loopCounter , loopCounter .getAnAccess ( ) )
271+ loopCounter = forLoop .getAnIterationVariable ( ) and
272+ variableModifiedInExpression ( forLoop .getStmt ( ) .getChildStmt ( ) .getAChild * ( ) ,
273+ loopCounter .getAnAccess ( ) )
274+ } or
275+ /* 3-2. The loop counter is not updated using either of `++`, `--`, `+=`, or `-=`. */
276+ TLoopCounterUpdatedNotByCrementOrAddSubAssignmentExpr ( ForStmt forLoop ) {
277+ none ( ) // TODO
190278 } or
191279 /* 4. The type size of the loop counter is smaller than that of the loop bound. */
192280 TLoopCounterSmallerThanLoopBound ( ForStmt forLoop , LegacyForLoopCondition forLoopCondition ) {
0 commit comments