From 15613635827f8cba24e738a90cdd51b9b58d0a60 Mon Sep 17 00:00:00 2001
From: Geoffrey White <40627776+geoffw0@users.noreply.github.com>
Date: Fri, 2 Nov 2018 13:20:26 +0000
Subject: [PATCH 1/2] CPP: Speed up illDefined*ForStmt in
 inconsistentLoopDirection.ql.

---
 .../Likely Typos/inconsistentLoopDirection.ql | 89 ++++++++++---------
 1 file changed, 46 insertions(+), 43 deletions(-)

diff --git a/cpp/ql/src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql b/cpp/ql/src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql
index a12cbe08b030..9735d23c2e55 100644
--- a/cpp/ql/src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql	
+++ b/cpp/ql/src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql	
@@ -14,53 +14,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
-  and
-  exists( 
-    RelationalOperation rel |
-    rel = forstmt.getCondition() |
-    terminalCondition = rel.getGreaterOperand()
-    and v.getAnAccess() = rel.getLesserOperand()
-    and
-    DataFlow::localFlowStep(DataFlow::exprNode(initialCondition), DataFlow::exprNode(rel.getLesserOperand()))
+/**
+ * A `for` statement whose update is a crement operation on a variable.
+ */
+predicate candidateForStmt(ForStmt forStmt, Variable v, CrementOperation update, RelationalOperation rel) {
+  update = forStmt.getUpdate() and
+  update.getAnOperand() = v.getAnAccess() and
+  rel = forStmt.getCondition() 
+}
+
+predicate illDefinedDecrForStmt( ForStmt forstmt, Variable v, Expr initialCondition, Expr terminalCondition ) {
+  exists(DecrementOperation dec, RelationalOperation rel |
+    // decrementing for loop
+    candidateForStmt(forstmt, v, dec, rel) and
+
+    // condition is `v < terminalCondition`
+    terminalCondition = rel.getGreaterOperand() and
+    v.getAnAccess() = rel.getLesserOperand() and
+
+    // `initialCondition` is a value of `v` in the for loop
+    v.getAnAssignedValue() = initialCondition and
+    DataFlow::localFlowStep(DataFlow::exprNode(initialCondition), DataFlow::exprNode(rel.getLesserOperand())) and
+
+    // `initialCondition` < `terminalCondition`
+    (
+      ( upperBound(initialCondition) < lowerBound(terminalCondition) )
+      or
+      ( forstmt.conditionAlwaysFalse() or forstmt.conditionAlwaysTrue() )
     )
-  and
-  exists( 
-    DecrementOperation dec |
-    dec = forstmt.getUpdate().(DecrementOperation)
-    and dec.getAnOperand() = v.getAnAccess()
-  )
-  and
-  ( 
-    ( 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 |
-    rel = forstmt.getCondition() |
-    terminalCondition = rel.getLesserOperand()
-    and v.getAnAccess() = rel.getGreaterOperand()
-    and
-    DataFlow::localFlowStep(DataFlow::exprNode(initialCondition), DataFlow::exprNode(rel.getGreaterOperand()))
-  )
-  and
-  exists( IncrementOperation incr |
-    incr = forstmt.getUpdate().(IncrementOperation)
-    and
-    incr.getAnOperand() = v.getAnAccess()
-  )
-  and
-  ( 
-    ( upperBound(terminalCondition) < lowerBound(initialCondition))
-    or
-    ( forstmt.conditionAlwaysFalse() or forstmt.conditionAlwaysTrue())
+predicate illDefinedIncrForStmt( ForStmt forstmt, Variable v, Expr initialCondition, Expr terminalCondition ) {
+  exists(IncrementOperation inc, RelationalOperation rel |
+    // incrementing for loop
+    candidateForStmt(forstmt, v, inc, rel) and
+
+    // condition is `v > terminalCondition`
+    terminalCondition = rel.getLesserOperand() and
+    v.getAnAccess() = rel.getGreaterOperand() and
+
+    // `initialCondition` is a value of `v` in the for loop
+    v.getAnAssignedValue() = initialCondition and
+    DataFlow::localFlowStep(DataFlow::exprNode(initialCondition), DataFlow::exprNode(rel.getGreaterOperand())) and
+
+    // `terminalCondition` < `initialCondition`
+    (
+      ( upperBound(terminalCondition) < lowerBound(initialCondition) )
+      or
+      ( forstmt.conditionAlwaysFalse() or forstmt.conditionAlwaysTrue() )
+    )
   )
 }
  

From a38fefe7ba3a3f8ea1bd4934934013d20fead674 Mon Sep 17 00:00:00 2001
From: Geoffrey White <40627776+geoffw0@users.noreply.github.com>
Date: Mon, 5 Nov 2018 15:21:27 +0000
Subject: [PATCH 2/2] CPP: Fix trailing space.

---
 .../src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql   | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cpp/ql/src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql b/cpp/ql/src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql
index 9735d23c2e55..58cc278ece80 100644
--- a/cpp/ql/src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql	
+++ b/cpp/ql/src/Likely Bugs/Likely Typos/inconsistentLoopDirection.ql	
@@ -20,7 +20,7 @@ import semmle.code.cpp.dataflow.DataFlow
 predicate candidateForStmt(ForStmt forStmt, Variable v, CrementOperation update, RelationalOperation rel) {
   update = forStmt.getUpdate() and
   update.getAnOperand() = v.getAnAccess() and
-  rel = forStmt.getCondition() 
+  rel = forStmt.getCondition()
 }
 
 predicate illDefinedDecrForStmt( ForStmt forstmt, Variable v, Expr initialCondition, Expr terminalCondition ) {