@@ -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