Java, C#: cleanup sign analysis

Add missing QL doc, improve readability

java/ql/src/semmle/code/java/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
@@ -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)
@@ -250,18 +253,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 +280,12 @@ Sign exprSign(Expr e) {
   )
 }
 
+/**
+ * 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

java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll

@@ -55,14 +55,22 @@ private module Impl {
 
   class UnsignedNumericType = CharacterType;
 
+  /**
+   * Gets the `float` value of expression `e` where `e` has no `int` value.
+   */
   float getNonIntegerValue(Expr e) {
     result = e.(LongLiteral).getValue().toFloat() or
     result = e.(FloatingPointLiteral).getValue().toFloat() or
     result = e.(DoubleLiteral).getValue().toFloat()
   }
 
+  /** Gets the character value of expression `e`. */
   string getCharValue(Expr e) { result = e.(CharacterLiteral).getValue() }
 
+  /**
+   * Holds if `e` is an access to the size of a container (`string`, `Map`, or
+   * `Collection`).
+   */
   predicate containerSizeAccess(Expr e) {
     e.(MethodAccess).getMethod() instanceof StringLengthMethod
     or
@@ -71,8 +79,15 @@ private module Impl {
     e.(MethodAccess).getMethod() instanceof MapSizeMethod
   }
 
+  /** Holds if `e` is by definition strictly positive. */
   predicate positiveExpression(Expr e) { none() }
 
+  /**
+   * Holds if `e` has type `NumericOrCharType`, but the sign of `e` is unknown.
+   *
+   * The expression types handled in the predicate complements the expression
+   * types handled in `specificSubExprSign`.
+   */
   predicate unknownIntegerAccess(Expr e) {
     e instanceof ArrayAccess and e.getType() instanceof NumericOrCharType
     or
@@ -81,6 +96,7 @@ private module Impl {
     e instanceof ClassInstanceExpr and e.getType() instanceof NumericOrCharType
   }
 
+  /** Returns the sign of explicit SSA definition `v`. */
   Sign explicitSsaDefSign(SsaVariable v) {
     exists(VariableUpdate def | def = v.(SsaExplicitUpdate).getDefiningExpr() |
       result = exprSign(def.(VariableAssign).getSource())
@@ -99,20 +115,13 @@ private module Impl {
     )
   }
 
+  /** Returns the sign of implicit SSA definition `v`. */
   Sign implicitSsaDefSign(SsaVariable v) {
     result = fieldSign(v.(SsaImplicitUpdate).getSourceVariable().getVariable())
     or
     result = fieldSign(v.(SsaImplicitInit).getSourceVariable().getVariable())
     or
-    exists(Parameter p | v.(SsaImplicitInit).isParameterDefinition(p))
-  }
-
-  pragma[inline]
-  Sign ssaVariableSign(SsaVariable v, Expr e) {
-    result = ssaSign(v, any(SsaReadPositionBlock bb | getAnExpression(bb) = e))
-    or
-    not exists(SsaReadPositionBlock bb | getAnExpression(bb) = e) and
-    result = ssaDefSign(v)
+    anySign(result) and exists(Parameter p | v.(SsaImplicitInit).isParameterDefinition(p))
   }
 
   /** Gets a possible sign for `f`. */
@@ -129,7 +138,7 @@ private module Impl {
     or
     exists(AssignOp a | a.getDest() = f.getAnAccess() | result = exprSign(a))
     or
-    exists(ReflectiveFieldAccess rfa | rfa.inferAccessedField() = f)
+    anySign(result) and exists(ReflectiveFieldAccess rfa | rfa.inferAccessedField() = f)
     or
     if f.fromSource()
     then not exists(f.getInitializer()) and result = TZero()
@@ -142,9 +151,10 @@ private module Impl {
         else
           if f.hasName("MIN_VALUE")
           then result = TNeg()
-          else any()
+          else anySign(result)
   }
 
+  /** Gets a possible sign for `e` from the signs of its child nodes. */
   Sign specificSubExprSign(Expr e) {
     result = exprSign(e.(AssignExpr).getSource())
     or