Refined argv-out-of-bounds-1 to precise result set

argv-out-of-bounds-1.ql

@@ -6,23 +6,23 @@
 
 import cpp
 import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+import semmle.code.cpp.controlflow.SSA
 
-/*
- * Use
- * https://codeql.github.com/docs/codeql-language-guides/codeql-library-for-cpp/
- * to find the codeql class matching c++ syntax
- *
- * See https://codeql.github.com/docs/codeql-language-guides/using-range-analsis-in-cpp/
- * for the entry points to the range analysis library.  Namely,
- * `import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis`
- * and
- * `lowerBound(expr)`
- */
+// 
+//    Use https://codeql.github.com/docs/codeql-language-guides/codeql-library-for-cpp/
+//    to find the codeql class matching c++ syntax
+// 
+//    See https://codeql.github.com/docs/codeql-language-guides/using-range-analsis-in-cpp/
+//    for the entry points to the range analysis library.  Namely,
+//    `import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis`
+//    and
+//    `lowerBound(expr)`
+// 
 
 from
   Parameter argc, RelationalOperation cmp, Variable n, Parameter argv, ArrayExpr argvAccess,
   AssignExpr argvSet, SsaDefinition invalidN, SsaDefinition invalidNDef
-where
+ where
   //
   //     consider argc and n when they occur in the same comparison
   //
@@ -94,15 +94,27 @@ where
   cmp.getLesserOperand() = invalidN.getAUse(n) and
   cmp.getGreaterOperand() = argc.getAnAccess() and
   invalidN.getAnUltimateDefiningValue(n).getValue().toInt() > 0 and
-  invalidNDef = invalidN.getAnUltimateSsaDefinition(n)
+  invalidNDef = invalidN.getAnUltimateSsaDefinition(n) and
   //
   //     We still find an access inside the loop,
   //        opt_user = g_strdup (argv[n]);
   //     so let's narrow:
-  and 
   invalidN.getAUse(n) = argvAccess.getArrayOffset() and
   argvSet = cmp.getAFalseSuccessor().getASuccessor*() and
-  argvAccess = cmp.getAFalseSuccessor().getASuccessor*() 
+  argvAccess = cmp.getAFalseSuccessor().getASuccessor*() and
+  // 
+  //    Reduce to a single invalidNDef location, the n = 1 case.
+  // // 
+  // //     Try one; still get `n = 1` and `n++`
+  // and  exists( Expr t| t =  invalidNDef.getDefiningValue(n))
+  //
+  //    Try two, require an explicit value:
+  exists(string t | t = invalidNDef.getDefiningValue(n).getValue())
+  // 
+  //    This works!  Some clean up/simplification, to be used in the next iteration.
+  and
+  invalidNDef = invalidN.getAnUltimateSsaDefinition(n) and 
+  invalidNDef.getDefiningValue(n).getValue().toInt() > 0
   
 select argc, "definition of argc", cmp, "use in comparison", n, "other var in comparison",
   argvAccess, "argv indexed", argvSet, "argv assigned", invalidNDef, "invalid n definition"