github · erik-krogh · Dec 21, 2021 · Jan 4, 2022 · Jan 4, 2022
@@ -63,6 +63,9 @@ class AstNode extends TAstNode {
     pred = directMember("getQLDoc") and result = this.getQLDoc()
   }
 
+  /** Gets any child of this node. */
+  AstNode getAChild() { result = this.getAChild(_) }
+
   /**
    * Gets the primary QL class for the ast node.
    */
@@ -274,9 +277,7 @@ class Predicate extends TPredicate, AstNode, PredicateOrBuiltin, Declaration {
     not this.(ClasslessPredicate).getAlias() instanceof PredicateExpr and
     result = count(this.getParameter(_))
     or
-    exists(PredicateExpr alias | alias = this.(ClasslessPredicate).getAlias() |
-      result = alias.getArity()
-    )
+    result = this.(ClasslessPredicate).getAlias().(PredicateExpr).getArity()
   }
 
   /**
@@ -1238,14 +1239,7 @@ class Boolean extends Literal {
 
 /** A comparison symbol, such as `"<"` or `"="`. */
 class ComparisonSymbol extends string {
-  ComparisonSymbol() {
-    this = "=" or
-    this = "!=" or
-    this = "<" or
-    this = ">" or
-    this = "<=" or
-    this = ">="
-  }
+  ComparisonSymbol() { this = ["=", "!=", "<", ">", "<=", ">="] }
 }
 
 /** A comparison formula, such as `x < 3` or `y = true`. */
@@ -1287,10 +1281,7 @@ class Quantifier extends TQuantifier, Formula {
   }
 
   /** Gets the ith variable declaration of this quantifier. */
-  VarDecl getArgument(int i) {
-    i >= 1 and
-    toQL(result) = quant.getChild(i - 1)
-  }
+  VarDecl getArgument(int i) { toQL(result) = quant.getChild(i + 1) }
 
   /** Gets an argument of this quantifier. */
   VarDecl getAnArgument() { result = this.getArgument(_) }
@@ -1661,6 +1652,15 @@ class FullAggregate extends TFullAggregate, Aggregate {
   }
 }
 
+/**
+ * A "any" expression, such as `any(int i | i > 0).toString()`.
+ */
+class Any extends FullAggregate {
+  Any() { this.getKind() = "any" }
+
+  override string getAPrimaryQlClass() { result = "Any" }
+}
+
 /**
  * A "rank" expression, such as `rank[4](int i | i = [5 .. 15] | i)`.
  */
@@ -1855,7 +1855,7 @@ class ExprAnnotation extends TExprAnnotation, Expr {
 
 /** A function symbol, such as `+` or `*`. */
 class FunctionSymbol extends string {
-  FunctionSymbol() { this = "+" or this = "-" or this = "*" or this = "/" or this = "%" }
+  FunctionSymbol() { this = ["+", "-", "*", "/", "%"] }
 }
 
 /**

@@ -104,9 +104,7 @@ class ClassType extends Type, TClass {
 
   VarDecl getField(string name) {
     result = fieldCandidate(this, name) and
-    not exists(VarDecl other | other = fieldCandidate(this, name) |
-      other.getDeclaringType().getASuperType+() = result.getDeclaringType()
-    )
+    not fieldCandidate(this, name).getDeclaringType().getASuperType+() = result.getDeclaringType()
   }
 }
 

@@ -0,0 +1,96 @@
+import ql
+
+/**
+ * Holds if `aggr` is of one of the following forms:
+ * `exists(var | range | formula)` or `any(var | range | formula)`
+ */
+private predicate aggregate(AstNode aggr, Formula range, AstNode formula, VarDecl var) {
+  exists(Exists ex | aggr = ex |
+    ex.getRange() = range and
+    ex.getFormula() = formula and
+    count(ex.getArgument(_)) = 1 and
+    ex.getArgument(0) = var
+  )
+  or
+  exists(Any anyy | aggr = anyy |
+    anyy.getRange() = range and
+    anyy.getExpr(0) = formula and
+    count(anyy.getExpr(_)) = 1 and
+    count(anyy.getArgument(_)) = 1 and
+    anyy.getArgument(0) = var
+  )
+}
+
+/**
+ * Holds if `aggr` is a redundant aggregate.
+ * The aggregate declares a single variable `var`, the value of which is `operand`, and it is only used once in `formula` (and the formula does not contain negative edges).
+ */
+predicate redundatAggregate(AstNode aggr, AstNode formula, VarDecl var, AstNode operand) {
+  exists(ComparisonFormula comp |
+    aggregate(aggr, comp, formula, var) and
+    comp.getOperator() = "=" and
+    comp.getAnOperand().(VarAccess).getDeclaration() = var and
+    not operand.(VarAccess).getDeclaration() = var and
+    operand = comp.getAnOperand() and
+    count(VarAccess access | access.getDeclaration() = var) = 2 and
+    any(VarAccess access | access.getDeclaration() = var) = getAChildOfAggregateFormula(formula)
+  ) and
+  // negative edges are not neccessarily semantics preserving - we are conservative here and just check for the existance of `not` or similar inside the formula
+  not getAChildOfAggregateFormula(formula) instanceof Negation and
+  not getAChildOfAggregateFormula(formula) instanceof Aggregate and
+  not getAChildOfAggregateFormula(formula) instanceof IfFormula and
+  not getAChildOfAggregateFormula(formula) instanceof Forall and
+  not getAChildOfAggregateFormula(formula) instanceof Forex and
+  // it's not neccessarily redundant inside noopt.
+  not aggr.getEnclosingPredicate().getAnAnnotation() instanceof NoOpt
+}
+
+/** Gets a (transitive) child of the formula from a `exists(..)` or `any(..)`. */
+AstNode getAChildOfAggregateFormula(AstNode formula) {
+  aggregate(_, _, formula, _) and result = formula
+  or
+  result = getAChildOfAggregateFormula(formula).getAChild()
+}
+
+/**
+ * Holds if `aggr` is of one of the following forms:
+ * `exists(var | range)` or `any(var | range)` or `any(var | | range)`
+ */
+private predicate castAggregate(AstNode aggr, Formula range, VarDecl var, string kind) {
+  kind = "exists" and
+  exists(Exists ex | aggr = ex |
+    ex.getRange() = range and
+    not exists(ex.getFormula()) and
+    count(ex.getArgument(_)) = 1 and
+    ex.getArgument(0) = var
+  )
+  or
+  kind = "any" and
+  exists(Any anyy | aggr = anyy |
+    not exists(anyy.getRange()) and
+    anyy.getExpr(0) = range and
+    count(anyy.getExpr(_)) = 1 and
+    count(anyy.getArgument(_)) = 1 and
+    anyy.getArgument(0) = var
+  )
+  or
+  kind = "any" and
+  exists(Any anyy | aggr = anyy |
+    range = anyy.getRange() and
+    count(anyy.getArgument(_)) = 1 and
+    anyy.getArgument(0) = var and
+    not exists(anyy.getExpr(0))
+  )
+}
+
+/** Holds if `aggr` is an aggregate that could be replaced with an instanceof expression or an inline cast. */
+predicate aggregateCouldBeCast(
+  AstNode aggr, ComparisonFormula comp, string kind, VarDecl var, AstNode operand
+) {
+  castAggregate(aggr, comp, var, kind) and
+  comp.getOperator() = "=" and
+  count(VarAccess access | access.getDeclaration() = var) = 1 and
+  comp.getAnOperand().(VarAccess).getDeclaration() = var and
+  operand = comp.getAnOperand() and
+  not operand.(VarAccess).getDeclaration() = var
+}
@@ -37,7 +37,7 @@ predicate alwaysBindsVar(VarDef var, AstNode node) {
     disj.getAnOperand() instanceof NoneCall
   )
   or
-  exists(IfFormula ifForm | ifForm = node | alwaysBindsVar(var, ifForm.getCondition()))
+  alwaysBindsVar(var, node.(IfFormula).getCondition())
 }
 
 /**
@@ -165,7 +165,7 @@ predicate varIsAlwaysBound(VarDef var, AstNode node) {
   onlyUseInOneBranch(_, var) // <- manual magic
   or
   // recursive cases
-  exists(AstNode parent | node.getParent() = parent | varIsAlwaysBound(var, parent))
+  varIsAlwaysBound(var, node.getParent())
   or
   exists(EffectiveConjunction parent |
     varIsAlwaysBound(var, parent.getLeft()) and

@@ -0,0 +1,27 @@
+/**
+ * @name Redundant aggregate
+ * @description An exists/any aggregate where a single variable is assigned in the range,
+ *              and used once in the formula, can be replaced with something simpler.
+ * @kind problem
+ * @problem.severity warning
+ * @id ql/redundant-aggregate
+ * @precision very-high
+ */
+
+import ql
+import codeql_ql.style.RedundantAggregateQuery
+
+from AstNode aggr, VarDecl var, string msg
+where
+  redundatAggregate(aggr, _, var, _) and
+  msg =
+    "The $@ variable in this aggregate is assigned and used exactly once, and the aggregate is therefore redundant."
+  or
+  exists(string kind | aggregateCouldBeCast(aggr, _, kind, var, _) |
+    kind = "exists" and
+    msg = "The assignment to $@ in the exists(..) can replaced with an instanceof expression."
+    or
+    kind = "any" and
+    msg = "The assignment to $@ in this any(..) can be replaced with an inline cast."
+  )
+select aggr, msg, var, var.getName()
@@ -2,7 +2,7 @@
  * @name Redundant inline cast
  * @description Redundant inline casts
  * @kind problem
- * @problem.severity error
+ * @problem.severity warning
  * @id ql/redundant-inline-cast
  * @tags maintainability
  * @precision high

@@ -121,8 +121,8 @@ nodes
 | Foo.qll:22:3:22:3 | f | semmle.order | 60 |
 | Foo.qll:22:3:22:16 | ComparisonFormula | semmle.label | [ComparisonFormula] ComparisonFormula |
 | Foo.qll:22:3:22:16 | ComparisonFormula | semmle.order | 60 |
-| Foo.qll:22:7:22:16 | FullAggregate[any] | semmle.label | [FullAggregate[any]] FullAggregate[any] |
-| Foo.qll:22:7:22:16 | FullAggregate[any] | semmle.order | 62 |
+| Foo.qll:22:7:22:16 | Any | semmle.label | [Any] Any |
+| Foo.qll:22:7:22:16 | Any | semmle.order | 62 |
 | Foo.qll:22:11:22:13 | TypeExpr | semmle.label | [TypeExpr] TypeExpr |
 | Foo.qll:22:11:22:13 | TypeExpr | semmle.order | 63 |
 | Foo.qll:22:11:22:15 | f | semmle.label | [VarDecl] f |
@@ -363,10 +363,10 @@ edges
 | Foo.qll:20:3:20:13 | ComparisonFormula | Foo.qll:20:13:20:13 | f | semmle.order | 59 |
 | Foo.qll:22:3:22:16 | ComparisonFormula | Foo.qll:22:3:22:3 | f | semmle.label | getLeftOperand() |
 | Foo.qll:22:3:22:16 | ComparisonFormula | Foo.qll:22:3:22:3 | f | semmle.order | 60 |
-| Foo.qll:22:3:22:16 | ComparisonFormula | Foo.qll:22:7:22:16 | FullAggregate[any] | semmle.label | getRightOperand() |
-| Foo.qll:22:3:22:16 | ComparisonFormula | Foo.qll:22:7:22:16 | FullAggregate[any] | semmle.order | 62 |
-| Foo.qll:22:7:22:16 | FullAggregate[any] | Foo.qll:22:11:22:15 | f | semmle.label | getArgument(_) |
-| Foo.qll:22:7:22:16 | FullAggregate[any] | Foo.qll:22:11:22:15 | f | semmle.order | 63 |
+| Foo.qll:22:3:22:16 | ComparisonFormula | Foo.qll:22:7:22:16 | Any | semmle.label | getRightOperand() |
+| Foo.qll:22:3:22:16 | ComparisonFormula | Foo.qll:22:7:22:16 | Any | semmle.order | 62 |
+| Foo.qll:22:7:22:16 | Any | Foo.qll:22:11:22:15 | f | semmle.label | getArgument(_) |
+| Foo.qll:22:7:22:16 | Any | Foo.qll:22:11:22:15 | f | semmle.order | 63 |
 | Foo.qll:22:11:22:15 | f | Foo.qll:22:11:22:13 | TypeExpr | semmle.label | getTypeExpr() |
 | Foo.qll:22:11:22:15 | f | Foo.qll:22:11:22:13 | TypeExpr | semmle.order | 63 |
 | Foo.qll:24:3:24:23 | ComparisonFormula | Foo.qll:24:3:24:3 | Integer | semmle.label | getLeftOperand() |

@@ -0,0 +1,17 @@
+bindingset[i]
+predicate foo(int i) {
+  exists(int j | j = i | j = 2) // redundant
+  or
+  exists(Even j | j = i) // redundant
+  or
+  exists(int j |
+    j = i // NOT redundant, inlining into a `forall` is not semantics preserving
+  |
+    forall(int k | k = j | k = 2)
+  )
+}
+
+class Even extends int {
+  bindingset[this]
+  Even() { this % 2 = 0 }
+}
@@ -0,0 +1,2 @@
+| Foo.qll:3:3:3:31 | Exists | The $@ variable in this aggregate is assigned and used exactly once, and the aggregate is therefore redundant. | Foo.qll:3:10:3:14 | j | j |
+| Foo.qll:5:3:5:24 | Exists | The assignment to $@ in the exists(..) can replaced with an instanceof expression. | Foo.qll:5:10:5:15 | j | j |
@@ -0,0 +1 @@
+queries/style/RedundantAggregate.ql