Java: Improve barriers for the CWE-190 Arithmetic* queries.

java/ql/src/Security/CWE/CWE-190/ArithmeticCommon.qll

@@ -1,7 +1,11 @@
 import semmle.code.java.arithmetic.Overflow
-import semmle.code.java.controlflow.Dominance
-import semmle.code.java.dataflow.DefUse
 import semmle.code.java.controlflow.Guards
+private import semmle.code.java.dataflow.SSA
+private import semmle.code.java.dataflow.DataFlow
+private import semmle.code.java.dataflow.RangeAnalysis
+private import semmle.code.java.dataflow.RangeUtils
+private import semmle.code.java.dataflow.SignAnalysis
+private import semmle.code.java.controlflow.internal.GuardsLogic
 
 /**
  * Holds if the type of `exp` is narrower than or equal to `numType`,
@@ -15,102 +19,138 @@ predicate narrowerThanOrEqualTo(ArithExpr exp, NumType numType) {
   )
 }
 
-/** Holds if the size of this use is guarded using `Math.abs`. */
-predicate guardedAbs(ArithExpr e, Expr use) {
-  exists(MethodAccess m | m.getMethod() instanceof MethodAbs |
-    m.getArgument(0) = use and
-    guardedLesser(e, m)
-  )
-}
-
-/** Holds if the size of this use is guarded to be less than something. */
-predicate guardedLesser(ArithExpr e, Expr use) {
-  exists(ConditionBlock c, ComparisonExpr guard |
-    use = guard.getLesserOperand() and
-    guard = c.getCondition() and
-    c.controls(e.getBasicBlock(), true)
+private Guard sizeGuard(SsaVariable v, boolean branch, boolean upper) {
+  exists(ComparisonExpr comp | comp = result |
+    comp.getLesserOperand() = ssaRead(v, 0) and
+    (
+      branch = true and upper = true
+      or
+      branch = false and upper = false
+    )
+    or
+    comp.getGreaterOperand() = ssaRead(v, 0) and
+    (
+      branch = true and upper = false
+      or
+      branch = false and upper = true
+    )
+    or
+    exists(MethodAccess ma |
+      ma.getMethod() instanceof MethodAbs and
+      ma.getArgument(0) = ssaRead(v, 0) and
+      (
+        comp.getLesserOperand() = ma and branch = true
+        or
+        comp.getGreaterOperand() = ma and branch = false
+      ) and
+      (upper = false or upper = true)
+    )
+    or
+    // overflow test
+    exists(AddExpr add, RValue use, Expr pos |
+      use = ssaRead(v, 0) and
+      add.hasOperands(use, pos) and
+      positive(use) and
+      positive(pos) and
+      upper = true
+    |
+      comp.getLesserOperand().getProperExpr() = add and
+      comp.getGreaterOperand().(IntegerLiteral).getIntValue() = 0 and
+      branch = false
+      or
+      comp.getGreaterOperand().getProperExpr() = add and
+      comp.getLesserOperand().(IntegerLiteral).getIntValue() = 0 and
+      branch = true
+    )
   )
   or
-  guardedAbs(e, use)
+  result.isEquality(ssaRead(v, 0), _, branch) and
+  (upper = true or upper = false)
+  or
+  exists(MethodAccess call, Method m, int ix |
+    call = result and
+    call.getArgument(ix) = ssaRead(v, 0) and
+    call.getMethod().getSourceDeclaration() = m and
+    m = customSizeGuard(ix, branch, upper)
+  )
 }
 
-/** Holds if the size of this use is guarded to be greater than something. */
-predicate guardedGreater(ArithExpr e, Expr use) {
-  exists(ConditionBlock c, ComparisonExpr guard |
-    use = guard.getGreaterOperand() and
-    guard = c.getCondition() and
-    c.controls(e.getBasicBlock(), true)
+private Guard derivedSizeGuard(SsaVariable v, boolean branch, boolean upper) {
+  result = sizeGuard(v, branch, upper) or
+  exists(boolean branch0 | implies_v3(result, branch, derivedSizeGuard(v, branch0, upper), branch0))
+}
+
+private Method customSizeGuard(int index, boolean retval, boolean upper) {
+  exists(Parameter p, SsaImplicitInit v |
+    result.getReturnType().(PrimitiveType).hasName("boolean") and
+    not result.isOverridable() and
+    p.getCallable() = result and
+    not p.isVarargs() and
+    p.getType() instanceof NumericOrCharType and
+    p.getPosition() = index and
+    v.isParameterDefinition(p) and
+    forex(ReturnStmt ret |
+      ret.getEnclosingCallable() = result and
+      exists(Expr res | res = ret.getResult() |
+        not res.(BooleanLiteral).getBooleanValue() = retval.booleanNot()
+      )
+    |
+      ret.getResult() = derivedSizeGuard(v, retval, upper)
+    )
+  )
+}
+
+/**
+ * Holds if `e` is bounded in a way that is likely to prevent overflow.
+ */
+predicate guardedLessThanSomething(Expr e) {
+  exists(SsaVariable v, Guard guard, boolean branch |
+    e = v.getAUse() and
+    guard = sizeGuard(v.getAPhiInputOrPriorDef*(), branch, true) and
+    guard.controls(e.getBasicBlock(), branch)
   )
   or
-  guardedAbs(e, use)
+  negative(e)
+  or
+  e.(MethodAccess).getMethod() instanceof MethodMathMin
 }
 
-/** Holds if this expression is (crudely) guarded by `use`. */
-predicate guarded(ArithExpr e, Expr use) {
-  exists(ConditionBlock c, ComparisonExpr guard |
-    use = guard.getAnOperand() and
-    guard = c.getCondition() and
-    c.controls(e.getBasicBlock(), true)
+/**
+ * Holds if `e` is bounded in a way that is likely to prevent underflow.
+ */
+predicate guardedGreaterThanSomething(Expr e) {
+  exists(SsaVariable v, Guard guard, boolean branch |
+    e = v.getAUse() and
+    guard = sizeGuard(v.getAPhiInputOrPriorDef*(), branch, false) and
+    guard.controls(e.getBasicBlock(), branch)
   )
+  or
+  positive(e)
+  or
+  e.(MethodAccess).getMethod() instanceof MethodMathMax
 }
 
-/** A prior use of the same variable that could see the same value. */
-VarAccess priorAccess(VarAccess access) { useUsePair(result, access) }
-
-/** Holds if `e` is guarded against overflow by `use`. */
-predicate guardedAgainstOverflow(ArithExpr e, VarAccess use) {
-  use = e.getAnOperand() and
-  (
-    // overflow possible if large
-    e instanceof AddExpr and guardedLesser(e, priorAccess(use))
+/** Holds if `e` occurs in a context where it will be upcast to a wider type. */
+predicate upcastToWiderType(Expr e) {
+  exists(NumType t1, NumType t2 |
+    t1 = e.getType() and
+    (
+      t2.widerThan(t1)
+      or
+      t1 instanceof CharacterType and t2.getWidthRank() >= 3
+    )
+  |
+    exists(Variable v | v.getAnAssignedValue() = e and t2 = v.getType())
     or
-    e instanceof PreIncExpr and guardedLesser(e, priorAccess(use))
+    exists(CastExpr c | c.getExpr() = e and t2 = c.getType())
     or
-    e instanceof PostIncExpr and guardedLesser(e, priorAccess(use))
+    exists(ReturnStmt ret | ret.getResult() = e and t2 = ret.getEnclosingCallable().getReturnType())
     or
-    // overflow unlikely with subtraction
-    e instanceof SubExpr
+    exists(Parameter p | p.getAnArgument() = e and t2 = p.getType())
     or
-    e instanceof PreDecExpr
-    or
-    e instanceof PostDecExpr
-    or
-    // overflow possible if large or small
-    e instanceof MulExpr and
-    guardedLesser(e, priorAccess(use)) and
-    guardedGreater(e, priorAccess(use))
-    or
-    // overflow possible if MIN_VALUE
-    e instanceof DivExpr and guardedGreater(e, priorAccess(use))
-  )
-}
-
-/** Holds if `e` is guarded against underflow by `use`. */
-predicate guardedAgainstUnderflow(ArithExpr e, VarAccess use) {
-  use = e.getAnOperand() and
-  (
-    // underflow unlikely for addition
-    e instanceof AddExpr
-    or
-    e instanceof PreIncExpr
-    or
-    e instanceof PostIncExpr
-    or
-    // underflow possible if use is left operand and small
-    e instanceof SubExpr and
-    (use = e.getRightOperand() or guardedGreater(e, priorAccess(use)))
-    or
-    e instanceof PreDecExpr and guardedGreater(e, priorAccess(use))
-    or
-    e instanceof PostDecExpr and guardedGreater(e, priorAccess(use))
-    or
-    // underflow possible if large or small
-    e instanceof MulExpr and
-    guardedLesser(e, priorAccess(use)) and
-    guardedGreater(e, priorAccess(use))
-    or
-    // underflow possible if MAX_VALUE
-    e instanceof DivExpr and guardedLesser(e, priorAccess(use))
+    exists(ConditionalExpr cond | cond.getTrueExpr() = e or cond.getFalseExpr() = e |
+      t2 = cond.getType()
+    )
   )
 }
 
@@ -124,7 +164,77 @@ private predicate inBitwiseAnd(Expr exp) {
 }
 
 /** Holds if overflow/underflow is irrelevant for this expression. */
-predicate overflowIrrelevant(ArithExpr exp) {
+predicate overflowIrrelevant(Expr exp) {
   inBitwiseAnd(exp) or
   exp.getEnclosingCallable() instanceof HashCodeMethod
 }
+
+/**
+ * Holds if `n` is unlikely to be part in a path from some source containing
+ * numeric data to some arithmetic expression that may overflow/underflow.
+ */
+private predicate unlikelyNode(DataFlow::Node n) {
+  n.getTypeBound() instanceof TypeObject and
+  not exists(CastExpr cast |
+    DataFlow::localFlow(n, DataFlow::exprNode(cast.getExpr())) and
+    cast.getType() instanceof NumericOrCharType
+  )
+}
+
+/** Holds if `n` is likely guarded against overflow. */
+predicate overflowBarrier(DataFlow::Node n) {
+  n.getType() instanceof BooleanType or
+  guardedLessThanSomething(n.asExpr()) or
+  unlikelyNode(n) or
+  upcastToWiderType(n.asExpr()) or
+  overflowIrrelevant(n.asExpr())
+}
+
+/** Holds if `n` is likely guarded against underflow. */
+predicate underflowBarrier(DataFlow::Node n) {
+  n.getType() instanceof BooleanType or
+  guardedGreaterThanSomething(n.asExpr()) or
+  unlikelyNode(n) or
+  upcastToWiderType(n.asExpr()) or
+  overflowIrrelevant(n.asExpr())
+}
+
+/**
+ * Holds if `use` is an operand of `exp` that acts as a sink for
+ * overflow-related dataflow.
+ */
+predicate overflowSink(ArithExpr exp, VarAccess use) {
+  exp.getAnOperand() = use and
+  (
+    // overflow unlikely for subtraction and division
+    exp instanceof AddExpr or
+    exp instanceof PreIncExpr or
+    exp instanceof PostIncExpr or
+    exp instanceof MulExpr
+  ) and
+  not guardedLessThanSomething(use) and
+  // Exclude widening conversions of tainted values due to binary numeric promotion (JLS 5.6.2)
+  // unless there is an enclosing cast down to a narrower type.
+  narrowerThanOrEqualTo(exp, use.getType()) and
+  not overflowIrrelevant(exp)
+}
+
+/**
+ * Holds if `use` is an operand of `exp` that acts as a sink for
+ * underflow-related dataflow.
+ */
+predicate underflowSink(ArithExpr exp, VarAccess use) {
+  exp.getAnOperand() = use and
+  (
+    // underflow unlikely for addition and division
+    exp.(SubExpr).getLeftOperand() = use or
+    exp instanceof PreDecExpr or
+    exp instanceof PostDecExpr or
+    exp instanceof MulExpr
+  ) and
+  not guardedGreaterThanSomething(use) and
+  // Exclude widening conversions of tainted values due to binary numeric promotion (JLS 5.6.2)
+  // unless there is an enclosing cast down to a narrower type.
+  narrowerThanOrEqualTo(exp, use.getType()) and
+  not overflowIrrelevant(exp)
+}

java/ql/src/Security/CWE/CWE-190/ArithmeticTainted.ql

@@ -16,35 +16,35 @@ import semmle.code.java.dataflow.FlowSources
 import ArithmeticCommon
 import DataFlow::PathGraph
 
-predicate sink(ArithExpr exp, VarAccess tainted, string effect) {
-  exp.getAnOperand() = tainted and
-  (
-    not guardedAgainstUnderflow(exp, tainted) and effect = "underflow"
-    or
-    not guardedAgainstOverflow(exp, tainted) and effect = "overflow"
-  ) and
-  // Exclude widening conversions of tainted values due to binary numeric promotion (JLS 5.6.2)
-  // unless there is an enclosing cast down to a narrower type.
-  narrowerThanOrEqualTo(exp, tainted.getType()) and
-  not overflowIrrelevant(exp)
-}
-
-class RemoteUserInputConfig extends TaintTracking::Configuration {
-  RemoteUserInputConfig() { this = "ArithmeticTainted.ql:RemoteUserInputConfig" }
+class RemoteUserInputOverflowConfig extends TaintTracking::Configuration {
+  RemoteUserInputOverflowConfig() { this = "ArithmeticTainted.ql:RemoteUserInputOverflowConfig" }
 
   override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
 
-  override predicate isSink(DataFlow::Node sink) { sink(_, sink.asExpr(), _) }
+  override predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
 
-  override predicate isSanitizer(DataFlow::Node n) { n.getType() instanceof BooleanType }
+  override predicate isSanitizer(DataFlow::Node n) { overflowBarrier(n) }
 }
 
-from
-  DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, string effect,
-  RemoteUserInputConfig conf
+class RemoteUserInputUnderflowConfig extends TaintTracking::Configuration {
+  RemoteUserInputUnderflowConfig() { this = "ArithmeticTainted.ql:RemoteUserInputUnderflowConfig" }
+
+  override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
+
+  override predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
+
+  override predicate isSanitizer(DataFlow::Node n) { underflowBarrier(n) }
+}
+
+from DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, string effect
 where
-  conf.hasFlowPath(source, sink) and
-  sink(exp, sink.getNode().asExpr(), effect)
+  any(RemoteUserInputOverflowConfig c).hasFlowPath(source, sink) and
+  overflowSink(exp, sink.getNode().asExpr()) and
+  effect = "overflow"
+  or
+  any(RemoteUserInputUnderflowConfig c).hasFlowPath(source, sink) and
+  underflowSink(exp, sink.getNode().asExpr()) and
+  effect = "underflow"
 select exp, source, sink,
   "$@ flows to here and is used in arithmetic, potentially causing an " + effect + ".",
   source.getNode(), "User-provided value"

java/ql/src/Security/CWE/CWE-190/ArithmeticTaintedLocal.ql

@@ -16,33 +16,35 @@ import semmle.code.java.dataflow.FlowSources
 import ArithmeticCommon
 import DataFlow::PathGraph
 
-predicate sink(ArithExpr exp, VarAccess tainted, string effect) {
-  exp.getAnOperand() = tainted and
-  (
-    not guardedAgainstUnderflow(exp, tainted) and effect = "underflow"
-    or
-    not guardedAgainstOverflow(exp, tainted) and effect = "overflow"
-  ) and
-  // Exclude widening conversions of tainted values due to binary numeric promotion (JLS 5.6.2)
-  // unless there is an enclosing cast down to a narrower type.
-  narrowerThanOrEqualTo(exp, tainted.getType()) and
-  not overflowIrrelevant(exp)
+class ArithmeticTaintedLocalOverflowConfig extends TaintTracking::Configuration {
+  ArithmeticTaintedLocalOverflowConfig() { this = "ArithmeticTaintedLocalOverflowConfig" }
+
+  override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
+
+  override predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
+
+  override predicate isSanitizer(DataFlow::Node n) { overflowBarrier(n) }
 }
 
-class ArithmeticTaintedLocalFlowConfig extends TaintTracking::Configuration {
-  ArithmeticTaintedLocalFlowConfig() { this = "ArithmeticTaintedLocalFlowConfig" }
+class ArithmeticTaintedLocalUnderflowConfig extends TaintTracking::Configuration {
+  ArithmeticTaintedLocalUnderflowConfig() { this = "ArithmeticTaintedLocalUnderflowConfig" }
 
-  override predicate isSource(DataFlow::Node source) { source instanceof LocalUserInput }
+  override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
 
-  override predicate isSink(DataFlow::Node sink) { sink(_, sink.asExpr(), _) }
+  override predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
 
-  override predicate isSanitizer(DataFlow::Node n) { n.getType() instanceof BooleanType }
+  override predicate isSanitizer(DataFlow::Node n) { underflowBarrier(n) }
 }
 
 from DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, string effect
 where
-  any(ArithmeticTaintedLocalFlowConfig conf).hasFlowPath(source, sink) and
-  sink(exp, sink.getNode().asExpr(), effect)
+  any(ArithmeticTaintedLocalOverflowConfig c).hasFlowPath(source, sink) and
+  overflowSink(exp, sink.getNode().asExpr()) and
+  effect = "overflow"
+  or
+  any(ArithmeticTaintedLocalUnderflowConfig c).hasFlowPath(source, sink) and
+  underflowSink(exp, sink.getNode().asExpr()) and
+  effect = "underflow"
 select exp, source, sink,
   "$@ flows to here and is used in arithmetic, potentially causing an " + effect + ".",
   source.getNode(), "User-provided value"

java/ql/src/Security/CWE/CWE-190/ArithmeticUncontrolled.ql

@@ -44,36 +44,35 @@ class TaintSource extends DataFlow::ExprNode {
   }
 }
 
-predicate sink(ArithExpr exp, VarAccess tainted, string effect) {
-  exp.getAnOperand() = tainted and
-  (
-    not guardedAgainstUnderflow(exp, tainted) and effect = "underflow"
-    or
-    not guardedAgainstOverflow(exp, tainted) and effect = "overflow"
-  ) and
-  // Exclude widening conversions of tainted values due to binary numeric promotion (JLS 5.6.2)
-  // unless there is an enclosing cast down to a narrower type.
-  narrowerThanOrEqualTo(exp, tainted.getType()) and
-  not overflowIrrelevant(exp) and
-  not exp.getEnclosingCallable().getDeclaringType() instanceof NonSecurityTestClass
-}
-
-class ArithmeticUncontrolledFlowConfig extends TaintTracking::Configuration {
-  ArithmeticUncontrolledFlowConfig() { this = "ArithmeticUncontrolledFlowConfig" }
+class ArithmeticUncontrolledOverflowConfig extends TaintTracking::Configuration {
+  ArithmeticUncontrolledOverflowConfig() { this = "ArithmeticUncontrolledOverflowConfig" }
 
   override predicate isSource(DataFlow::Node source) { source instanceof TaintSource }
 
-  override predicate isSink(DataFlow::Node sink) { sink(_, sink.asExpr(), _) }
+  override predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
 
-  override predicate isSanitizer(DataFlow::Node n) { n.getType() instanceof BooleanType }
+  override predicate isSanitizer(DataFlow::Node n) { overflowBarrier(n) }
 }
 
-from
-  DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, string effect,
-  ArithmeticUncontrolledFlowConfig conf
+class ArithmeticUncontrolledUnderflowConfig extends TaintTracking::Configuration {
+  ArithmeticUncontrolledUnderflowConfig() { this = "ArithmeticUncontrolledUnderflowConfig" }
+
+  override predicate isSource(DataFlow::Node source) { source instanceof TaintSource }
+
+  override predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
+
+  override predicate isSanitizer(DataFlow::Node n) { underflowBarrier(n) }
+}
+
+from DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, string effect
 where
-  conf.hasFlowPath(source, sink) and
-  sink(exp, sink.getNode().asExpr(), effect)
+  any(ArithmeticUncontrolledOverflowConfig c).hasFlowPath(source, sink) and
+  overflowSink(exp, sink.getNode().asExpr()) and
+  effect = "overflow"
+  or
+  any(ArithmeticUncontrolledUnderflowConfig c).hasFlowPath(source, sink) and
+  underflowSink(exp, sink.getNode().asExpr()) and
+  effect = "underflow"
 select exp, source, sink,
   "$@ flows to here and is used in arithmetic, potentially causing an " + effect + ".",
   source.getNode(), "Uncontrolled value"

java/ql/src/Security/CWE/CWE-190/ArithmeticWithExtremeValues.ql

@@ -33,60 +33,59 @@ class ExtremeSource extends VarAccess {
   ExtremeSource() { this.getVariable() instanceof ExtremeValueField }
 }
 
-class ExtremeSourceFlowConfig extends DataFlow::Configuration {
-  ExtremeSourceFlowConfig() { this = "ExtremeSourceFlowConfig" }
+class MaxValueFlowConfig extends DataFlow::Configuration {
+  MaxValueFlowConfig() { this = "MaxValueFlowConfig" }
 
-  override predicate isSource(DataFlow::Node source) { source.asExpr() instanceof ExtremeSource }
+  override predicate isSource(DataFlow::Node source) {
+    source.asExpr().(ExtremeSource).getVariable() instanceof MaxValueField
+  }
 
-  override predicate isSink(DataFlow::Node sink) { sink(_, sink.asExpr()) }
+  override predicate isSink(DataFlow::Node sink) { overflowSink(_, sink.asExpr()) }
 
   override predicate isBarrierIn(DataFlow::Node n) { isSource(n) }
 
-  override predicate isBarrier(DataFlow::Node n) { n.getType() instanceof BooleanType }
+  override predicate isBarrier(DataFlow::Node n) { overflowBarrier(n) }
 }
 
-predicate sink(ArithExpr exp, VarAccess use) {
-  use = exp.getAnOperand() and
-  (
-    not guardedAgainstUnderflow(exp, use) or
-    not guardedAgainstOverflow(exp, use)
-  ) and
-  not overflowIrrelevant(exp) and
-  not exp instanceof DivExpr
+class MinValueFlowConfig extends DataFlow::Configuration {
+  MinValueFlowConfig() { this = "MinValueFlowConfig" }
+
+  override predicate isSource(DataFlow::Node source) {
+    source.asExpr().(ExtremeSource).getVariable() instanceof MinValueField
+  }
+
+  override predicate isSink(DataFlow::Node sink) { underflowSink(_, sink.asExpr()) }
+
+  override predicate isBarrierIn(DataFlow::Node n) { isSource(n) }
+
+  override predicate isBarrier(DataFlow::Node n) { underflowBarrier(n) }
 }
 
 predicate query(
-  DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, Variable v,
-  ExtremeValueField f, VarAccess use, ExtremeSource s, Type t
+  DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, string effect, Type srctyp
 ) {
-  // `use` is the use of `v` in `exp`.
-  use = exp.getAnOperand() and
-  use = v.getAnAccess() and
-  // An extreme field flows to `use`.
-  f = s.getVariable() and
-  any(ExtremeSourceFlowConfig conf).hasFlowPath(source, sink) and
-  s = source.getNode().asExpr() and
-  use = sink.getNode().asExpr() and
-  t = s.getType() and
-  // Division isn't a problem in this case.
-  not exp instanceof DivExpr
+  (
+    any(MaxValueFlowConfig c).hasFlowPath(source, sink) and
+    overflowSink(exp, sink.getNode().asExpr()) and
+    effect = "overflow"
+    or
+    any(MinValueFlowConfig c).hasFlowPath(source, sink) and
+    underflowSink(exp, sink.getNode().asExpr()) and
+    effect = "underflow"
+  ) and
+  srctyp = source.getNode().asExpr().getType()
 }
 
 from
-  DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, Variable v,
-  ExtremeValueField f, VarAccess use, ExtremeSource s, string effect, Type t
+  DataFlow::PathNode source, DataFlow::PathNode sink, ArithExpr exp, Variable v, ExtremeSource s,
+  string effect, Type srctyp
 where
-  query(source, sink, exp, v, f, use, s, t) and
-  // We're not guarded against the appropriate kind of flow error.
-  (
-    f instanceof MinValueField and not guardedAgainstUnderflow(exp, use) and effect = "underflow"
-    or
-    f instanceof MaxValueField and not guardedAgainstOverflow(exp, use) and effect = "overflow"
-  ) and
+  query(source, sink, exp, effect, srctyp) and
   // Exclude widening conversions of extreme values due to binary numeric promotion (JLS 5.6.2)
   // unless there is an enclosing cast down to a narrower type.
-  narrowerThanOrEqualTo(exp, t) and
-  not overflowIrrelevant(exp)
+  narrowerThanOrEqualTo(exp, srctyp) and
+  v = sink.getNode().asExpr().(VarAccess).getVariable() and
+  s = source.getNode().asExpr()
 select exp, source, sink,
   "Variable " + v.getName() + " is assigned an extreme value $@, and may cause an " + effect + ".",
-  s, f.getName()
+  s, s.getVariable().getName()

java/ql/src/semmle/code/java/JDK.qll

@@ -265,6 +265,22 @@ class MethodAbs extends Method {
   }
 }
 
+/** The method `Math.min`. */
+class MethodMathMin extends Method {
+  MethodMathMin() {
+    this.getDeclaringType() instanceof TypeMath and
+    this.getName() = "min"
+  }
+}
+
+/** The method `Math.min`. */
+class MethodMathMax extends Method {
+  MethodMathMax() {
+    this.getDeclaringType() instanceof TypeMath and
+    this.getName() = "max"
+  }
+}
+
 // --- Standard fields ---
 /** The field `System.in`. */
 class SystemIn extends Field {

java/ql/src/semmle/code/java/dataflow/SSA.qll

@@ -964,7 +964,7 @@ class SsaVariable extends TSsaVariable {
    * includes inputs to phi nodes, the prior definition of uncertain updates,
    * and the captured ssa variable for a closure variable.
    */
-  private SsaVariable getAPhiInputOrPriorDef() {
+  SsaVariable getAPhiInputOrPriorDef() {
     result = this.(SsaPhiNode).getAPhiInput() or
     result = this.(SsaUncertainImplicitUpdate).getPriorDef() or
     this.(SsaImplicitInit).captures(result)