Zero diffs between Java AST and Semantic range analysis

Author: Dave Bartolomeo

java/ql/lib/semmle/code/java/semantic/SemanticExpr.qll

@@ -43,6 +43,8 @@ private newtype TOpcode =
   TSubOne() or // TODO: Combine with `TSub`
   TConditional() or // TODO: Represent as flow
   TCall() or
+  TBox() or
+  TUnbox() or
   TUnknown()
 
 class Opcode extends TOpcode {
@@ -170,6 +172,14 @@ module Opcode {
     override string toString() { result = "StringConstant" }
   }
 
+  class Box extends Opcode, TBox {
+    override string toString() { result = "Box" }
+  }
+
+  class Unbox extends Opcode, TUnbox {
+    override string toString() { result = "Unbox" }
+  }
+
   class Unknown extends Opcode, TUnknown {
     override string toString() { result = "Unknown" }
   }
@@ -325,6 +335,10 @@ class SemShiftRightExpr extends SemBinaryExpr {
   SemShiftRightExpr() { opcode instanceof Opcode::ShiftRight }
 }
 
+class SemShiftRightUnsignedExpr extends SemBinaryExpr {
+  SemShiftRightUnsignedExpr() { opcode instanceof Opcode::ShiftRightUnsigned }
+}
+
 class SemBitAndExpr extends SemBinaryExpr {
   SemBitAndExpr() { opcode instanceof Opcode::BitAnd }
 }
@@ -345,6 +359,14 @@ class SemUnaryExpr extends SemKnownExpr {
   final SemExpr getOperand() { result = operand }
 }
 
+class SemBoxExpr extends SemUnaryExpr {
+  SemBoxExpr() { opcode instanceof Opcode::Box }
+}
+
+class SemUnboxExpr extends SemUnaryExpr {
+  SemUnboxExpr() { opcode instanceof Opcode::Unbox }
+}
+
 class SemConvertExpr extends SemUnaryExpr {
   SemConvertExpr() { opcode instanceof Opcode::Convert }
 }

java/ql/lib/semmle/code/java/semantic/SemanticExprSpecific.qll

@@ -249,12 +249,24 @@ module SemanticExprConfig {
       )
     )
     or
-    exists(J::CastExpr cast | cast = javaExpr |
-      // TODO: Boolean? Null? Boxing?
-      getSemanticType(cast.getType()) instanceof SemNumericType and
-      getSemanticType(cast.getExpr().getType()) instanceof SemNumericType and
-      opcode instanceof Opcode::Convert and
-      operand = getResultExpr(cast.getExpr())
+    exists(J::CastExpr cast, J::Type srcType, J::Type destType |
+      cast = javaExpr and srcType = cast.getExpr().getType() and destType = cast.getType()
+    |
+      operand = getResultExpr(cast.getExpr()) and
+      (
+        // TODO: Conversions between `boolean` and numeric types should probably be comparisons
+        srcType instanceof J::PrimitiveType and
+        destType instanceof J::PrimitiveType and
+        opcode instanceof Opcode::Convert
+        or
+        srcType instanceof J::PrimitiveType and
+        destType instanceof J::RefType and
+        opcode instanceof Opcode::Box
+        or
+        srcType instanceof J::RefType and
+        destType instanceof J::PrimitiveType and
+        opcode instanceof Opcode::Unbox
+      )
     )
     or
     exists(J::AssignExpr assign | assign = javaExpr |
@@ -344,9 +356,8 @@ module SemanticExprConfig {
     final Location getLocation() { result = super.getLocation() }
   }
 
-  predicate explicitUpdate(SsaVariable v, SemType type, Expr sourceExpr) {
+  predicate explicitUpdate(SsaVariable v, Expr sourceExpr) {
     exists(SSA::SsaExplicitUpdate update | v = update |
-      type = getSemanticType(update.getSourceVariable().getType()) and
       exists(J::Expr expr | expr = update.getDefiningExpr() |
         (
           expr instanceof J::AssignOp or
@@ -370,14 +381,16 @@ module SemanticExprConfig {
     )
   }
 
-  predicate phi(SsaVariable v, SemType type) {
-    type = getSemanticType(v.(SSA::SsaPhiNode).getSourceVariable().getType())
-  }
+  predicate phi(SsaVariable v) { v instanceof SSA::SsaPhiNode }
 
   SsaVariable getAPhiInput(SsaVariable v) { result = v.(SSA::SsaPhiNode).getAPhiInput() }
 
   Expr getAUse(SsaVariable v) { result = getResultExpr(v.(SSA::SsaVariable).getAUse()) }
 
+  SemType getSsaVariableType(SsaVariable v) {
+    result = getSemanticType(v.(SSA::SsaVariable).getSourceVariable().getType())
+  }
+
   BasicBlock getSsaVariableBasicBlock(SsaVariable v) {
     result = v.(SSA::SsaVariable).getBasicBlock()
   }

java/ql/lib/semmle/code/java/semantic/SemanticGuard.qll

@@ -14,6 +14,8 @@ class SemGuard instanceof Specific::Guard {
 
   final string toString() { result = super.toString() }
 
+  final Specific::Location getLocation() { result = super.getLocation() }
+
   final predicate isEquality(SemExpr e1, SemExpr e2, boolean polarity) {
     Specific::equalityGuard(this, e1, e2, polarity)
   }

java/ql/lib/semmle/code/java/semantic/SemanticSSA.qll

@@ -8,29 +8,27 @@ private import SemanticType
 private import SemanticExprSpecific::SemanticExprConfig as Specific
 
 class SemSsaVariable instanceof Specific::SsaVariable {
-  SemType type;
-
   final string toString() { result = super.toString() }
 
   final Specific::Location getLocation() { result = super.getLocation() }
 
   final SemLoadExpr getAUse() { result = Specific::getAUse(this) }
 
-  final SemType getType() { result = type }
+  final SemType getType() { result = Specific::getSsaVariableType(this) }
 
   final SemBasicBlock getBasicBlock() { result = Specific::getSsaVariableBasicBlock(this) }
 }
 
 class SemSsaExplicitUpdate extends SemSsaVariable {
   SemExpr sourceExpr;
 
-  SemSsaExplicitUpdate() { Specific::explicitUpdate(this, type, sourceExpr) }
+  SemSsaExplicitUpdate() { Specific::explicitUpdate(this, sourceExpr) }
 
   final SemExpr getSourceExpr() { result = sourceExpr }
 }
 
 class SemSsaPhiNode extends SemSsaVariable {
-  SemSsaPhiNode() { Specific::phi(this, type) }
+  SemSsaPhiNode() { Specific::phi(this) }
 
   final SemSsaVariable getAPhiInput() { result = Specific::getAPhiInput(this) }
 }