Demo of MIN_INT negate query

CodeQL_Queries/cpp/MinIntNegate/.gitignore

@@ -0,0 +1,2 @@
+MinIntNegateDB
+test.o

CodeQL_Queries/cpp/MinIntNegate/00_MinIntNegate.ql

@@ -0,0 +1,29 @@
+/**
+ * @name 00_MinIntNegate
+ * @description Negating MIN_INT is an integer overflow
+ * @kind problem
+ * @id cpp/min-int-negate
+ * @problem.severity warning
+ */
+
+import cpp
+import semmle.code.cpp.controlflow.Guards
+
+// Find this pattern:
+//
+// ```
+// if (x < 0) {
+//   x = -x;
+// }
+// ```
+//
+// If the value of `x` is `0x80000000` then this will not make the value of `x` positive.
+from GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Variable v, Expr use
+where
+  guard.(LTExpr).getLeftOperand() = v.getAnAccess() and
+  guard.(LTExpr).getRightOperand().getValue().toInt() = 0 and
+  guard.controls(block, true) and
+  block.contains(unaryMinus) and
+  unaryMinus.getOperand() = v.getAnAccess()
+select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", v,
+  v.getName()

CodeQL_Queries/cpp/MinIntNegate/01_MinIntNegate.ql

@@ -0,0 +1,29 @@
+/**
+ * @name 01_MinIntNegate
+ * @description Negating MIN_INT is an integer overflow
+ * @kind problem
+ * @id cpp/min-int-negate
+ * @problem.severity warning
+ */
+
+import cpp
+import semmle.code.cpp.controlflow.Guards
+
+// The previous query had an incorrect result at test.cpp, line 20:
+//
+//   if (s->myfield < 0) {
+//     s->myfield = -t->myfield;
+//   }
+//
+// The problem is that the query used `Variable`, which includes fields.
+// So here we restrict the query to use `LocalScopeVariable` instead.
+from
+  GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, LocalScopeVariable v, Expr use
+where
+  guard.(LTExpr).getLeftOperand() = v.getAnAccess() and
+  guard.(LTExpr).getRightOperand().getValue().toInt() = 0 and
+  guard.controls(block, true) and
+  block.contains(unaryMinus) and
+  unaryMinus.getOperand() = v.getAnAccess()
+select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", v,
+  v.getName()

CodeQL_Queries/cpp/MinIntNegate/02_MinIntNegate.ql

@@ -0,0 +1,34 @@
+/**
+ * @name 02_MinIntNegate
+ * @description Negating MIN_INT is an integer overflow
+ * @kind problem
+ * @id cpp/min-int-negate
+ * @problem.severity warning
+ */
+
+import cpp
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+// The previous query, 01_MinIntNegate, eliminated a bad result
+// from 00_MinIntNegate, but it also lost a good result.
+// The missing result is test.cpp, line 14:
+//
+//   if (s->myfield < 0) {
+//     s->myfield = -s->myfield;
+//   }
+//
+// The problem is that `s->myfield` is not a `LocalScopeVariable`.
+// The solution is to use the GlobalValueNumbering library, which
+// is a more general way to find expressions that compute the same
+// value.
+from GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2
+where
+  guard.(LTExpr).getLeftOperand() = use1 and
+  guard.(LTExpr).getRightOperand().getValue().toInt() = 0 and
+  guard.controls(block, true) and
+  block.contains(unaryMinus) and
+  unaryMinus.getOperand() = use2 and
+  globalValueNumber(use1) = globalValueNumber(use2)
+select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive",
+  use2, use2.toString()

CodeQL_Queries/cpp/MinIntNegate/03_MinIntNegate.ql

@@ -0,0 +1,36 @@
+/**
+ * @name 03_MinIntNegate
+ * @description Negating MIN_INT is an integer overflow
+ * @kind problem
+ * @id cpp/min-int-negate
+ * @problem.severity warning
+ */
+
+import cpp
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+// The previous query only worked for `x < 0` and not for the
+// equivalent `0 > x`. It's easier to handle both if we refactor
+// the logic into a separate predicate.
+
+/** Holds if `cond` is a comparison of the form `lhs < rhs`. */
+predicate lessThan(Expr cond, Expr lhs, Expr rhs) {
+  cond.(LTExpr).getLeftOperand() = lhs and
+  cond.(LTExpr).getRightOperand() = rhs
+  or
+  cond.(GTExpr).getLeftOperand() = rhs and
+  cond.(GTExpr).getRightOperand() = lhs
+}
+
+from
+  GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2, Expr zero
+where
+  lessThan(guard, use1, zero) and
+  zero.getValue().toInt() = 0 and
+  guard.controls(block, true) and
+  block.contains(unaryMinus) and
+  unaryMinus.getOperand() = use2 and
+  globalValueNumber(use1) = globalValueNumber(use2)
+select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive",
+  use2, use2.toString()

CodeQL_Queries/cpp/MinIntNegate/04_MinIntNegate.ql

@@ -0,0 +1,47 @@
+/**
+ * @name 04_MinIntNegate
+ * @description Negating MIN_INT is an integer overflow
+ * @kind problem
+ * @id cpp/min-int-negate
+ * @problem.severity warning
+ */
+
+import cpp
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+// Let's also add support for <= and >=.
+
+/**
+ * Holds if `cond` is a comparison of the form `lhs < rhs`.
+ * `isStrict` is true for < and >, and false for <= and >=.
+ */
+predicate lessThan(Expr cond, Expr lhs, Expr rhs, boolean isStrict) {
+  cond.(LTExpr).getLeftOperand() = lhs and
+  cond.(LTExpr).getRightOperand() = rhs and
+  isStrict = true
+  or
+  cond.(GTExpr).getLeftOperand() = rhs and
+  cond.(GTExpr).getRightOperand() = lhs and
+  isStrict = true
+  or
+  cond.(LEExpr).getLeftOperand() = lhs and
+  cond.(LEExpr).getRightOperand() = rhs and
+  isStrict = false
+  or
+  cond.(GEExpr).getLeftOperand() = rhs and
+  cond.(GEExpr).getRightOperand() = lhs and
+  isStrict = false
+}
+
+from
+  GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2, Expr zero
+where
+  lessThan(guard, use1, zero, _) and
+  zero.getValue().toInt() = 0 and
+  guard.controls(block, true) and
+  block.contains(unaryMinus) and
+  unaryMinus.getOperand() = use2 and
+  globalValueNumber(use1) = globalValueNumber(use2)
+select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive",
+  use2, use2.toString()

CodeQL_Queries/cpp/MinIntNegate/05_MinIntNegate.ql

@@ -0,0 +1,63 @@
+/**
+ * @name 05_MinIntNegate
+ * @description Negating MIN_INT is an integer overflow
+ * @kind problem
+ * @id cpp/min-int-negate
+ * @problem.severity warning
+ */
+
+import cpp
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+// The previous query added support for <= and >=, but failed to
+// find any new results. That's because the comparison is 0 <= x,
+// so the operands are the wrong way around. We can solve this by
+// adding a recursive predicate which swaps them.
+
+/**
+ * Holds if `cond` is a comparison of the form `lhs < rhs`.
+ * `isStrict` is true for < and >, and false for <= and >=.
+ */
+predicate lessThan(Expr cond, Expr lhs, Expr rhs, boolean isStrict) {
+  cond.(LTExpr).getLeftOperand() = lhs and
+  cond.(LTExpr).getRightOperand() = rhs and
+  isStrict = true
+  or
+  cond.(GTExpr).getLeftOperand() = rhs and
+  cond.(GTExpr).getRightOperand() = lhs and
+  isStrict = true
+  or
+  cond.(LEExpr).getLeftOperand() = lhs and
+  cond.(LEExpr).getRightOperand() = rhs and
+  isStrict = false
+  or
+  cond.(GEExpr).getLeftOperand() = rhs and
+  cond.(GEExpr).getRightOperand() = lhs and
+  isStrict = false
+}
+
+/**
+ * Holds if `cond` is a comparison of the form `lhs < rhs`.
+ * `isStrict` is true for < and >, and false for <= and >=.
+ * `branch` is true if the comparison is true and false if it is not.
+ */
+predicate lessThanWithNegate(Expr cond, Expr lhs, Expr rhs, boolean isStrict, boolean branch) {
+  branch = true and lessThan(cond, lhs, rhs, isStrict)
+  or
+  // (x < y) == !(y <= x)
+  lessThanWithNegate(cond, rhs, lhs, isStrict.booleanNot(), branch.booleanNot())
+}
+
+from
+  GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2,
+  Expr zero, boolean branch
+where
+  lessThanWithNegate(guard, use1, zero, _, branch) and
+  zero.getValue().toInt() = 0 and
+  guard.controls(block, branch) and
+  block.contains(unaryMinus) and
+  unaryMinus.getOperand() = use2 and
+  globalValueNumber(use1) = globalValueNumber(use2)
+select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive",
+  use2, use2.toString()

CodeQL_Queries/cpp/MinIntNegate/06_MinIntNegate.ql

@@ -0,0 +1,75 @@
+/**
+ * @name 06_MinIntNegate
+ * @description Negating MIN_INT is an integer overflow
+ * @kind problem
+ * @id cpp/min-int-negate
+ * @problem.severity warning
+ */
+
+import cpp
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+import semmle.code.cpp.dataflow.DataFlow
+
+// Let's add local dataflow, so that we can also handle cases like this:
+//
+// ```
+// bool b = x < 0;
+// if (b) {
+//   x = -x;
+// }
+// ```
+
+/**
+ * Holds if `cond` is a comparison of the form `lhs < rhs`.
+ * `isStrict` is true for < and >, and false for <= and >=.
+ */
+predicate lessThan(Expr cond, Expr lhs, Expr rhs, boolean isStrict) {
+  cond.(LTExpr).getLeftOperand() = lhs and
+  cond.(LTExpr).getRightOperand() = rhs and
+  isStrict = true
+  or
+  cond.(GTExpr).getLeftOperand() = rhs and
+  cond.(GTExpr).getRightOperand() = lhs and
+  isStrict = true
+  or
+  cond.(LEExpr).getLeftOperand() = lhs and
+  cond.(LEExpr).getRightOperand() = rhs and
+  isStrict = false
+  or
+  cond.(GEExpr).getLeftOperand() = rhs and
+  cond.(GEExpr).getRightOperand() = lhs and
+  isStrict = false
+}
+
+/**
+ * Holds if `cond` is a comparison of the form `lhs < rhs`.
+ * `isStrict` is true for < and >, and false for <= and >=.
+ * `branch` is true if the comparison is true and false if it is not.
+ */
+predicate lessThanWithNegate(Expr cond, Expr lhs, Expr rhs, boolean isStrict, boolean branch) {
+  branch = true and lessThan(cond, lhs, rhs, isStrict)
+  or
+  // (x < y) == !(y <= x)
+  lessThanWithNegate(cond, rhs, lhs, isStrict.booleanNot(), branch.booleanNot())
+  or
+  // bool b = x < 0;
+  // if (b) { ... }
+  exists(Expr prev |
+    DataFlow::localExprFlow(prev, cond) and
+    lessThanWithNegate(prev, lhs, rhs, branch, isStrict)
+  )
+}
+
+from
+  GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2,
+  Expr zero, boolean branch
+where
+  lessThanWithNegate(guard, use1, zero, _, branch) and
+  zero.getValue().toInt() = 0 and
+  guard.controls(block, branch) and
+  block.contains(unaryMinus) and
+  unaryMinus.getOperand() = use2 and
+  globalValueNumber(use1) = globalValueNumber(use2)
+select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive",
+  use2, use2.toString()