Rangeanalysis: Implement shared ssaRead predicate

Author: aschackmull

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll

@@ -23,6 +23,8 @@ class SemSsaExplicitUpdate extends SemSsaVariable {
   SemSsaExplicitUpdate() { Specific::explicitUpdate(this, sourceExpr) }
 
   final SemExpr getSourceExpr() { result = sourceExpr }
+
+  final SemExpr getDefiningExpr() { result = sourceExpr }
 }
 
 class SemSsaPhiNode extends SemSsaVariable {

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll

@@ -52,9 +52,21 @@ module Sem implements Semantic {
 
   class NegateExpr = SemNegateExpr;
 
-  class AddOneExpr = SemAddOneExpr;
+  class PreIncExpr = SemAddOneExpr;
 
-  class SubOneExpr = SemSubOneExpr;
+  class PreDecExpr = SemSubOneExpr;
+
+  class PostIncExpr extends SemUnaryExpr {
+    PostIncExpr() { none() }
+  }
+
+  class PostDecExpr extends SemUnaryExpr {
+    PostDecExpr() { none() }
+  }
+
+  class CopyValueExpr extends SemUnaryExpr {
+    CopyValueExpr() { this instanceof SemCopyValueExpr or this instanceof SemStoreExpr }
+  }
 
   class ConditionalExpr = SemConditionalExpr;
 

java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

@@ -150,6 +150,8 @@ module Sem implements Semantic {
     }
   }
 
+  predicate isAssignOp(BinaryExpr bin) { bin instanceof AssignOp }
+
   class RelationalExpr = J::ComparisonExpr;
 
   abstract class UnaryExpr extends Expr {
@@ -176,18 +178,34 @@ module Sem implements Semantic {
     override Expr getOperand() { result = super.getExpr() }
   }
 
-  // TODO: Implement once utils are properly shared
-  class AddOneExpr extends UnaryExpr {
-    AddOneExpr() { none() }
+  class PreIncExpr extends UnaryExpr instanceof J::PreIncExpr {
+    override Expr getOperand() { result = super.getExpr() }
+  }
 
-    override Expr getOperand() { none() }
+  class PreDecExpr extends UnaryExpr instanceof J::PreDecExpr {
+    override Expr getOperand() { result = super.getExpr() }
   }
 
-  // TODO: Implement once utils are properly shared
-  class SubOneExpr extends UnaryExpr {
-    SubOneExpr() { none() }
+  class PostIncExpr extends UnaryExpr instanceof J::PostIncExpr {
+    override Expr getOperand() { result = super.getExpr() }
+  }
 
-    override Expr getOperand() { none() }
+  class PostDecExpr extends UnaryExpr instanceof J::PostDecExpr {
+    override Expr getOperand() { result = super.getExpr() }
+  }
+
+  class CopyValueExpr extends UnaryExpr {
+    CopyValueExpr() {
+      this instanceof J::PlusExpr or
+      this instanceof J::AssignExpr or
+      this instanceof LocalVariableDeclExpr
+    }
+
+    override Expr getOperand() {
+      result = this.(J::PlusExpr).getExpr() or
+      result = this.(J::AssignExpr).getSource() or
+      result = this.(J::LocalVariableDeclExpr).getInit()
+    }
   }
 
   class ConditionalExpr = J::ConditionalExpr;
@@ -228,7 +246,9 @@ module Sem implements Semantic {
 
   class SsaPhiNode extends SsaVariable instanceof SSA::SsaPhiNode { }
 
-  class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate { }
+  class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate {
+    Expr getDefiningExpr() { result = super.getDefiningExpr() }
+  }
 
   final private class FinalSsaReadPosition = SsaReadPos::SsaReadPosition;
 

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

@@ -106,6 +106,8 @@ signature module Semantic {
 
   class ShiftRightUnsignedExpr extends BinaryExpr;
 
+  default predicate isAssignOp(BinaryExpr bin) { none() }
+
   class RelationalExpr extends Expr {
     Expr getLesserOperand();
 
@@ -126,9 +128,15 @@ signature module Semantic {
 
   class NegateExpr extends UnaryExpr;
 
-  class AddOneExpr extends UnaryExpr;
+  class PreIncExpr extends UnaryExpr;
+
+  class PreDecExpr extends UnaryExpr;
+
+  class PostIncExpr extends UnaryExpr;
 
-  class SubOneExpr extends UnaryExpr;
+  class PostDecExpr extends UnaryExpr;
+
+  class CopyValueExpr extends UnaryExpr;
 
   class ConditionalExpr extends Expr {
     Expr getBranchExpr(boolean branch);
@@ -168,7 +176,9 @@ signature module Semantic {
 
   class SsaPhiNode extends SsaVariable;
 
-  class SsaExplicitUpdate extends SsaVariable;
+  class SsaExplicitUpdate extends SsaVariable {
+    Expr getDefiningExpr();
+  }
 
   class SsaReadPosition {
     predicate hasReadOfVar(SsaVariable v);
@@ -1188,12 +1198,12 @@ module RangeStage<
     positively = false and
     (
       expr instanceof Sem::NegateExpr or
-      expr instanceof Sem::SubOneExpr or
+      expr instanceof Sem::PreDecExpr or
       getTrackedType(expr.(Sem::DivExpr)) instanceof Sem::FloatingPointType
     )
     or
     positively = true and
-    expr instanceof Sem::AddOneExpr
+    expr instanceof Sem::PreIncExpr
   }
 
   /**

shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll

@@ -0,0 +1,37 @@
+private import codeql.rangeanalysis.RangeAnalysis
+
+module MakeUtils<Semantic Lang, DeltaSig D> {
+  /**
+   * Gets an expression that equals `v - d`.
+   */
+  Lang::Expr ssaRead(Lang::SsaVariable v, D::Delta delta) {
+    result = v.getAUse() and delta = D::fromInt(0)
+    or
+    exists(D::Delta d1, Lang::ConstantIntegerExpr c |
+      result.(Lang::AddExpr).hasOperands(ssaRead(v, d1), c) and
+      delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) and
+      // In the scope of `x += ..`, which is SSA translated as `x2 = x1 + ..`,
+      // the variable `x1` is shadowed by `x2`, so there's no need to view this
+      // as a read of `x1`.
+      not Lang::isAssignOp(result)
+    )
+    or
+    exists(Lang::SubExpr sub, D::Delta d1, Lang::ConstantIntegerExpr c |
+      result = sub and
+      sub.getLeftOperand() = ssaRead(v, d1) and
+      sub.getRightOperand() = c and
+      delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) and
+      not Lang::isAssignOp(result)
+    )
+    or
+    result = v.(Lang::SsaExplicitUpdate).getDefiningExpr() and
+    if result instanceof Lang::PostIncExpr
+    then delta = D::fromFloat(1) // x++ === ++x - 1
+    else
+      if result instanceof Lang::PostDecExpr
+      then delta = D::fromFloat(-1) // x-- === --x + 1
+      else delta = D::fromFloat(0)
+    or
+    result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta)
+  }
+}