Merge pull request #4362 from tamasvajk/feature/sign-analysis-cleanup

Sign analysis cleanup

Author: aschackmull

csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/Sign.qll

@@ -3,6 +3,25 @@ newtype TSign =
   TZero() or
   TPos()
 
+newtype TUnarySignOperation =
+  TNegOp() or
+  TIncOp() or
+  TDecOp() or
+  TBitNotOp()
+
+newtype TBinarySignOperation =
+  TAddOp() or
+  TSubOp() or
+  TMulOp() or
+  TDivOp() or
+  TRemOp() or
+  TBitAndOp() or
+  TBitOrOp() or
+  TBitXorOp() or
+  TLShiftOp() or
+  TRShiftOp() or
+  TURShiftOp()
+
 /** Class representing expression signs (+, -, 0). */
 class Sign extends TSign {
   /** Gets the string representation of this sign. */
@@ -67,6 +86,12 @@ class Sign extends TSign {
     this = TNeg() and s = TPos()
   }
 
+  /**
+   * Gets a possible sign after subtracting an expression with sign `s` from an expression
+   * that has this sign.
+   */
+  Sign sub(Sign s) { result = add(s.neg()) }
+
   /**
    * Gets a possible sign after multiplying an expression with sign `s` to an expression
    * that has this sign.
@@ -216,4 +241,40 @@ class Sign extends TSign {
     or
     result != TNeg() and this = TPos() and s != TZero()
   }
+
+  /** Perform `op` on this sign. */
+  Sign applyUnaryOp(TUnarySignOperation op) {
+    op = TIncOp() and result = inc()
+    or
+    op = TDecOp() and result = dec()
+    or
+    op = TNegOp() and result = neg()
+    or
+    op = TBitNotOp() and result = bitnot()
+  }
+
+  /** Perform `op` on this sign and sign `s`. */
+  Sign applyBinaryOp(Sign s, TBinarySignOperation op) {
+    op = TAddOp() and result = add(s)
+    or
+    op = TSubOp() and result = sub(s)
+    or
+    op = TMulOp() and result = mul(s)
+    or
+    op = TDivOp() and result = div(s)
+    or
+    op = TRemOp() and result = rem(s)
+    or
+    op = TBitAndOp() and result = bitand(s)
+    or
+    op = TBitOrOp() and result = bitor(s)
+    or
+    op = TBitXorOp() and result = bitxor(s)
+    or
+    op = TLShiftOp() and result = lshift(s)
+    or
+    op = TRShiftOp() and result = rshift(s)
+    or
+    op = TURShiftOp() and result = urshift(s)
+  }
 }

csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll

@@ -11,7 +11,7 @@ private import SsaReadPositionCommon
 private import Sign
 
 /** Gets the sign of `e` if this can be directly determined. */
-Sign certainExprSign(Expr e) {
+private Sign certainExprSign(Expr e) {
   exists(int i | e.(ConstantIntegerExpr).getIntValue() = i |
     i < 0 and result = TNeg()
     or
@@ -42,7 +42,7 @@ Sign certainExprSign(Expr e) {
 }
 
 /** Holds if the sign of `e` is too complicated to determine. */
-predicate unknownSign(Expr e) {
+private predicate unknownSign(Expr e) {
   not exists(certainExprSign(e)) and
   (
     exists(IntegerLiteral lit | lit = e and not exists(lit.getValue().toInt()))
@@ -55,7 +55,7 @@ predicate unknownSign(Expr e) {
       not fromtyp instanceof NumericOrCharType
     )
     or
-    unknownIntegerAccess(e)
+    numericExprWithUnknownSign(e)
   )
 }
 
@@ -185,29 +185,32 @@ private predicate hasGuard(SsaVariable v, SsaReadPosition pos, Sign s) {
   s = TZero() and zeroBound(_, v, pos)
 }
 
+/**
+ * Gets a possible sign of `v` at `pos` based on its definition, where the sign
+ * might be ruled out by a guard.
+ */
 pragma[noinline]
 private Sign guardedSsaSign(SsaVariable v, SsaReadPosition pos) {
-  // SSA variable can have sign `result`
   result = ssaDefSign(v) and
   pos.hasReadOfVar(v) and
-  // there are guards at this position on `v` that might restrict it to be sign `result`.
-  // (So we need to check if they are satisfied)
   hasGuard(v, pos, result)
 }
 
+/**
+ * Gets a possible sign of `v` at `pos` based on its definition, where no guard
+ * can rule it out.
+ */
 pragma[noinline]
 private Sign unguardedSsaSign(SsaVariable v, SsaReadPosition pos) {
-  // SSA variable can have sign `result`
   result = ssaDefSign(v) and
   pos.hasReadOfVar(v) and
-  // there's no guard at this position on `v` that might restrict it to be sign `result`.
   not hasGuard(v, pos, result)
 }
 
 /**
- * Gets the sign of `v` at read position `pos`, when there's at least one guard
- * on `v` at position `pos`. Each bound corresponding to a given sign must be met
- * in order for `v` to be of that sign.
+ * Gets a possible sign of `v` at read position `pos`, where a guard could have
+ * ruled out the sign but does not.
+ * This does not check that the definition of `v` also allows the sign.
  */
 private Sign guardedSsaSignOk(SsaVariable v, SsaReadPosition pos) {
   result = TPos() and
@@ -221,7 +224,7 @@ private Sign guardedSsaSignOk(SsaVariable v, SsaReadPosition pos) {
 }
 
 /** Gets a possible sign for `v` at `pos`. */
-Sign ssaSign(SsaVariable v, SsaReadPosition pos) {
+private Sign ssaSign(SsaVariable v, SsaReadPosition pos) {
   result = unguardedSsaSign(v, pos)
   or
   result = guardedSsaSign(v, pos) and
@@ -230,7 +233,7 @@ Sign ssaSign(SsaVariable v, SsaReadPosition pos) {
 
 /** Gets a possible sign for `v`. */
 pragma[nomagic]
-Sign ssaDefSign(SsaVariable v) {
+private Sign ssaDefSign(SsaVariable v) {
   result = explicitSsaDefSign(v)
   or
   result = implicitSsaDefSign(v)
@@ -242,6 +245,40 @@ Sign ssaDefSign(SsaVariable v) {
   )
 }
 
+/** Returns the sign of explicit SSA definition `v`. */
+private Sign explicitSsaDefSign(SsaVariable v) {
+  exists(VariableUpdate def | def = getExplicitSsaAssignment(v) |
+    result = exprSign(getExprFromSsaAssignment(def))
+    or
+    anySign(result) and explicitSsaDefWithAnySign(def)
+    or
+    result = exprSign(getIncrementOperand(def)).inc()
+    or
+    result = exprSign(getDecrementOperand(def)).dec()
+  )
+}
+
+/** Returns the sign of implicit SSA definition `v`. */
+private Sign implicitSsaDefSign(SsaVariable v) {
+  result = fieldSign(getImplicitSsaDeclaration(v))
+  or
+  anySign(result) and nonFieldImplicitSsaDefinition(v)
+}
+
+/** Gets a possible sign for `f`. */
+private Sign fieldSign(Field f) {
+  if not fieldWithUnknownSign(f)
+  then
+    result = exprSign(getAssignedValueToField(f))
+    or
+    fieldIncrementOperationOperand(f) and result = fieldSign(f).inc()
+    or
+    fieldDecrementOperationOperand(f) and result = fieldSign(f).dec()
+    or
+    result = specificFieldSign(f)
+  else anySign(result)
+}
+
 /** Gets a possible sign for `e`. */
 cached
 Sign exprSign(Expr e) {
@@ -250,18 +287,23 @@ Sign exprSign(Expr e) {
     or
     not exists(certainExprSign(e)) and
     (
-      unknownSign(e)
+      anySign(s) and unknownSign(e)
       or
-      exists(SsaVariable v | getARead(v) = e | s = ssaVariableSign(v, e))
+      exists(SsaVariable v | getARead(v) = e |
+        s = ssaSign(v, any(SsaReadPositionBlock bb | getAnExpression(bb) = e))
+        or
+        not exists(SsaReadPositionBlock bb | getAnExpression(bb) = e) and
+        s = ssaDefSign(v)
+      )
       or
-      e =
-        any(VarAccess access |
-          not exists(SsaVariable v | getARead(v) = access) and
-          (
-            s = fieldSign(getField(access.(FieldAccess))) or
-            not access instanceof FieldAccess
-          )
+      exists(VarAccess access | access = e |
+        not exists(SsaVariable v | getARead(v) = access) and
+        (
+          s = fieldSign(getField(access.(FieldAccess)))
+          or
+          anySign(s) and not access instanceof FieldAccess
         )
+      )
       or
       s = specificSubExprSign(e)
     )
@@ -272,6 +314,41 @@ Sign exprSign(Expr e) {
   )
 }
 
+/** Gets a possible sign for `e` from the signs of its child nodes. */
+private Sign specificSubExprSign(Expr e) {
+  result = exprSign(getASubExprWithSameSign(e))
+  or
+  exists(DivExpr div | div = e |
+    result = exprSign(div.getLeftOperand()) and
+    result != TZero() and
+    div.getRightOperand().(RealLiteral).getValue().toFloat() = 0
+  )
+  or
+  exists(UnaryOperation unary | unary = e |
+    result = exprSign(unary.getOperand()).applyUnaryOp(unary.getOp())
+  )
+  or
+  exists(Sign s1, Sign s2 | binaryOpSigns(e, s1, s2) |
+    result = s1.applyBinaryOp(s2, e.(BinaryOperation).getOp())
+  )
+}
+
+pragma[noinline]
+private predicate binaryOpSigns(Expr e, Sign lhs, Sign rhs) {
+  lhs = binaryOpLhsSign(e) and
+  rhs = binaryOpRhsSign(e)
+}
+
+private Sign binaryOpLhsSign(BinaryOperation e) { result = exprSign(e.getLeftOperand()) }
+
+private Sign binaryOpRhsSign(BinaryOperation e) { result = exprSign(e.getRightOperand()) }
+
+/**
+ * Dummy predicate that holds for any sign. This is added to improve readability
+ * of cases where the sign is unrestricted.
+ */
+predicate anySign(Sign s) { any() }
+
 /** Holds if `e` can be positive and cannot be negative. */
 predicate positive(Expr e) {
   exprSign(e) = TPos() and