Merge pull request #1189 from aschackmull/java/preconditions

Java: Support precondition calls as guards (ODASA-7796).

Author: yh-semmle

change-notes/1.21/analysis-java.md

@@ -0,0 +1,24 @@
+# Improvements to Java analysis
+
+## New queries
+
+| **Query**                   | **Tags**  | **Purpose**                                                        |
+|-----------------------------|-----------|--------------------------------------------------------------------|
+
+## Changes to existing queries
+
+| **Query**                  | **Expected impact**    | **Change**                                                       |
+|----------------------------|------------------------|------------------------------------------------------------------|
+
+## Changes to QL libraries
+
+* The `Guards` library has been extended to account for method calls that check
+  conditions by conditionally throwing an exception. This includes the
+  `checkArgument` and `checkState` methods in
+  `com.google.common.base.Preconditions`, the `isTrue` and `validState` methods
+  in `org.apache.commons.lang3.Validate`, as well as any similar custom
+  methods. This means that more guards are recognized yielding precision
+  improvements in a number of queries including `java/index-out-of-bounds`,
+  `java/dereferenced-value-may-be-null`, and `java/useless-null-check`.
+
+

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

@@ -81,6 +81,7 @@
 
 import java
 private import Completion
+private import controlflow.internal.Preconditions
 
 /** A node in the expression-level control-flow graph. */
 class ControlFlowNode extends Top, @exprparent {
@@ -169,7 +170,8 @@ private module ControlFlowGraphImpl {
     exists(Call c | c = n |
       t = c.getCallee().getAThrownExceptionType() or
       uncheckedExceptionFromCatch(n, t) or
-      uncheckedExceptionFromFinally(n, t)
+      uncheckedExceptionFromFinally(n, t) or
+      uncheckedExceptionFromMethod(c, t)
     )
     or
     exists(CastExpr c | c = n |
@@ -178,6 +180,14 @@ private module ControlFlowGraphImpl {
     )
   }
 
+  /**
+   * Bind `t` to an unchecked exception that may occur in a precondition check.
+   */
+  private predicate uncheckedExceptionFromMethod(MethodAccess ma, ThrowableType t) {
+    conditionCheck(ma, _) and
+    (t instanceof TypeError or t instanceof TypeRuntimeException)
+  }
+
   /**
    * Bind `t` to an unchecked exception that may transfer control to a finally
    * block inside which `n` is nested.

java/ql/src/semmle/code/java/controlflow/Guards.qll

@@ -1,6 +1,7 @@
 import java
 private import semmle.code.java.controlflow.Dominance
 private import semmle.code.java.controlflow.internal.GuardsLogic
+private import semmle.code.java.controlflow.internal.Preconditions
 
 /**
  * A basic block that terminates in a condition, splitting the subsequent control flow.
@@ -71,7 +72,7 @@ class ConditionBlock extends BasicBlock {
 /**
  * A condition that can be evaluated to either true or false. This can either
  * be an `Expr` of boolean type that isn't a boolean literal, or a case of a
- * switch statement.
+ * switch statement, or a method access that acts as a precondition check.
  *
  * Evaluating a switch case to true corresponds to taking that switch case, and
  * evaluating it to false corresponds to taking some other branch.
@@ -81,6 +82,8 @@ class Guard extends ExprParent {
     this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral
     or
     this instanceof SwitchCase
+    or
+    conditionCheck(this, _)
   }
 
   /** Gets the immediately enclosing callable whose body contains this guard. */
@@ -128,6 +131,8 @@ class Guard extends ExprParent {
       pred.(Expr).getParent*() = sc.getSwitch().getExpr() and
       bb1 = pred.getBasicBlock()
     )
+    or
+    preconditionBranchEdge(this, bb1, bb2, branch)
   }
 
   /**
@@ -142,6 +147,8 @@ class Guard extends ExprParent {
     )
     or
     switchCaseControls(this, controlled) and branch = true
+    or
+    preconditionControls(this, controlled, branch)
   }
 
   /**
@@ -165,6 +172,24 @@ private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) {
   )
 }
 
+private predicate preconditionBranchEdge(
+  MethodAccess ma, BasicBlock bb1, BasicBlock bb2, boolean branch
+) {
+  conditionCheck(ma, branch) and
+  bb1.getLastNode() = ma.getControlFlowNode() and
+  bb2 = bb1.getLastNode().getANormalSuccessor()
+}
+
+private predicate preconditionControls(MethodAccess ma, BasicBlock controlled, boolean branch) {
+  exists(BasicBlock check, BasicBlock succ |
+    preconditionBranchEdge(ma, check, succ, branch) and
+    succ.bbDominates(controlled) and
+    forall(BasicBlock pred | pred = succ.getABBPredecessor() and pred != check |
+      succ.bbDominates(pred)
+    )
+  )
+}
+
 /**
  * INTERNAL: Use `Guards.controls` instead.
  *

java/ql/src/semmle/code/java/controlflow/internal/GuardsLogic.qll

@@ -5,6 +5,7 @@
 
 import java
 import semmle.code.java.controlflow.Guards
+private import Preconditions
 private import semmle.code.java.dataflow.SSA
 private import semmle.code.java.dataflow.internal.BaseSSA
 private import semmle.code.java.dataflow.NullGuards
@@ -61,6 +62,13 @@ predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
   or
   g1.(DefaultCase).getSwitch().getAConstCase() = g2 and b1 = true and b2 = false
   or
+  exists(MethodAccess check | check = g1 |
+    conditionCheck(check, _) and
+    g2 = check.getArgument(0) and
+    (b1 = true or b1 = false) and
+    b2 = b1
+  )
+  or
   exists(BaseSsaUpdate vbool |
     vbool.getAUse() = g1 and
     vbool.getDefiningExpr().(VariableAssign).getSource() = g2 and

java/ql/src/semmle/code/java/controlflow/internal/Preconditions.qll

@@ -0,0 +1,59 @@
+/**
+ * Provides predicates for identifying precondition checks like
+ * `com.google.common.base.Preconditions` and
+ * `org.apache.commons.lang3.Validate`.
+ */
+import java
+
+/**
+ * Holds if `m` is a non-overridable method that checks that its first argument
+ * is equal to `checkTrue` and throws otherwise.
+ */
+predicate conditionCheckMethod(Method m, boolean checkTrue) {
+  m.getDeclaringType().hasQualifiedName("com.google.common.base", "Preconditions") and
+  checkTrue = true and
+  (m.hasName("checkArgument") or m.hasName("checkState"))
+  or
+  m.getDeclaringType().hasQualifiedName("org.apache.commons.lang3", "Validate") and
+  checkTrue = true and
+  (m.hasName("isTrue") or m.hasName("validState"))
+  or
+  exists(Parameter p, IfStmt ifstmt, Expr cond |
+    p = m.getParameter(0) and
+    not m.isOverridable() and
+    p.getType() instanceof BooleanType and
+    m.getBody().getStmt(0) = ifstmt and
+    ifstmt.getCondition().getProperExpr() = cond and
+    (
+      cond.(LogNotExpr).getExpr().getProperExpr().(VarAccess).getVariable() = p and checkTrue = true
+      or
+      cond.(VarAccess).getVariable() = p and checkTrue = false
+    ) and
+    (
+      ifstmt.getThen() instanceof ThrowStmt or
+      ifstmt.getThen().(SingletonBlock).getStmt() instanceof ThrowStmt
+    )
+  )
+  or
+  exists(Parameter p, MethodAccess ma, boolean ct, Expr arg |
+    p = m.getParameter(0) and
+    not m.isOverridable() and
+    m.getBody().getStmt(0).(ExprStmt).getExpr() = ma and
+    conditionCheck(ma, ct) and
+    ma.getArgument(0).getProperExpr() = arg and
+    (
+      arg.(LogNotExpr).getExpr().getProperExpr().(VarAccess).getVariable() = p and
+      checkTrue = ct.booleanNot()
+      or
+      arg.(VarAccess).getVariable() = p and checkTrue = ct
+    )
+  )
+}
+
+/**
+ * Holds if `ma` is an access to a non-overridable method that checks that its
+ * first argument is equal to `checkTrue` and throws otherwise.
+ */
+predicate conditionCheck(MethodAccess ma, boolean checkTrue) {
+  conditionCheckMethod(ma.getMethod().getSourceDeclaration(), checkTrue)
+}

java/ql/src/semmle/code/java/frameworks/Assertions.qll

@@ -39,10 +39,6 @@ private predicate assertionMethod(Method m, AssertKind kind) {
     preconditions.hasQualifiedName("com.google.common.base", "Preconditions")
   |
     m.hasName("checkNotNull") and kind = AssertKindNotNull()
-    or
-    m.hasName("checkArgument") and kind = AssertKindTrue()
-    or
-    m.hasName("checkState") and kind = AssertKindTrue()
   )
 }
 

java/ql/test/library-tests/guards/Logic.java

@@ -30,4 +30,21 @@ void f(int[] a, String s) {
     if (o instanceof String) {
     }
   }
+
+  void f2(int i) {
+    checkTrue(i > 0, "i pos");
+    checkFalse(g(100), "g");
+    if (i > 10) {
+      checkTrue(i > 20, "");
+    }
+    int dummy = 0;
+  }
+
+  private static void checkTrue(boolean b, String msg) {
+    if (!b) throw new Exception(msg);
+  }
+
+  private static void checkFalse(boolean b, String msg) {
+    checkTrue(!b, msg);
+  }
 }

java/ql/test/library-tests/guards/guardslogic.expected

@@ -30,3 +30,19 @@
 | Logic.java:29:16:29:19 | g(...) | false | Logic.java:30:30:31:5 | stmt |
 | Logic.java:29:16:29:19 | g(...) | true | Logic.java:29:23:29:26 | null |
 | Logic.java:30:9:30:27 | ...instanceof... | true | Logic.java:30:30:31:5 | stmt |
+| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:36:5:36:28 | stmt |
+| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:37:5:37:15 | stmt |
+| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:37:17:39:5 | stmt |
+| Logic.java:35:5:35:29 | checkTrue(...) | true | Logic.java:40:5:40:18 | stmt |
+| Logic.java:35:15:35:19 | ... > ... | true | Logic.java:36:5:36:28 | stmt |
+| Logic.java:35:15:35:19 | ... > ... | true | Logic.java:37:5:37:15 | stmt |
+| Logic.java:35:15:35:19 | ... > ... | true | Logic.java:37:17:39:5 | stmt |
+| Logic.java:35:15:35:19 | ... > ... | true | Logic.java:40:5:40:18 | stmt |
+| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:37:5:37:15 | stmt |
+| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:37:17:39:5 | stmt |
+| Logic.java:36:5:36:27 | checkFalse(...) | false | Logic.java:40:5:40:18 | stmt |
+| Logic.java:36:16:36:21 | g(...) | false | Logic.java:37:5:37:15 | stmt |
+| Logic.java:36:16:36:21 | g(...) | false | Logic.java:37:17:39:5 | stmt |
+| Logic.java:36:16:36:21 | g(...) | false | Logic.java:40:5:40:18 | stmt |
+| Logic.java:37:9:37:14 | ... > ... | true | Logic.java:37:17:39:5 | stmt |
+| Logic.java:44:10:44:10 | b | false | Logic.java:44:33:44:35 | msg |