Merge pull request #4324 from tamasvajk/feature/unsigned-sign-analysis

Handle unsigned types in sign analysis (C# and Java)

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

@@ -245,24 +245,30 @@ Sign ssaDefSign(SsaVariable v) {
 /** Gets a possible sign for `e`. */
 cached
 Sign exprSign(Expr e) {
-  result = certainExprSign(e)
-  or
-  not exists(certainExprSign(e)) and
-  (
-    unknownSign(e)
+  exists(Sign s |
+    s = certainExprSign(e)
     or
-    exists(SsaVariable v | getARead(v) = e | result = ssaVariableSign(v, e))
-    or
-    e =
-      any(VarAccess access |
-        not exists(SsaVariable v | getARead(v) = access) and
-        (
-          result = fieldSign(getField(access.(FieldAccess))) or
-          not access instanceof FieldAccess
+    not exists(certainExprSign(e)) and
+    (
+      unknownSign(e)
+      or
+      exists(SsaVariable v | getARead(v) = e | s = ssaVariableSign(v, e))
+      or
+      e =
+        any(VarAccess access |
+          not exists(SsaVariable v | getARead(v) = access) and
+          (
+            s = fieldSign(getField(access.(FieldAccess))) or
+            not access instanceof FieldAccess
+          )
         )
-      )
-    or
-    result = specificSubExprSign(e)
+      or
+      s = specificSubExprSign(e)
+    )
+  |
+    if e.getType() instanceof UnsignedNumericType and s = TNeg()
+    then result = TPos()
+    else result = s
   )
 }
 

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

@@ -71,14 +71,29 @@ private module Impl {
 
   predicate positiveExpression(Expr e) { e instanceof SizeofExpr }
 
-  class NumericOrCharType extends Type {
-    NumericOrCharType() {
-      this instanceof CharType or
-      this instanceof IntegralType or
-      this instanceof FloatingPointType or
-      this instanceof DecimalType or
-      this instanceof Enum or
-      this instanceof PointerType // should be similar to unsigned integers
+  abstract class NumericOrCharType extends Type { }
+
+  class UnsignedNumericType extends NumericOrCharType {
+    UnsignedNumericType() {
+      this instanceof CharType
+      or
+      this instanceof UnsignedIntegralType
+      or
+      this instanceof PointerType
+      or
+      this instanceof Enum and this.(Enum).getUnderlyingType() instanceof UnsignedIntegralType
+    }
+  }
+
+  class SignedNumericType extends NumericOrCharType {
+    SignedNumericType() {
+      this instanceof SignedIntegralType
+      or
+      this instanceof FloatingPointType
+      or
+      this instanceof DecimalType
+      or
+      this instanceof Enum and this.(Enum).getUnderlyingType() instanceof SignedIntegralType
     }
   }
 
@@ -125,6 +140,7 @@ private module Impl {
     e.getType() instanceof NumericOrCharType and
     not e = getARead(_) and
     not e instanceof FieldAccess and
+    not e instanceof TypeAccess and
     // The expression types that are listed here are the ones handled in `specificSubExprSign`.
     // Keep them in sync.
     not e instanceof AssignExpr and

csharp/ql/test/library-tests/dataflow/signanalysis/MissingSign.ql

@@ -4,6 +4,7 @@ import semmle.code.csharp.dataflow.SignAnalysis
 from Expr e
 where
   not exists(exprSign(e)) and
+  not e instanceof TypeAccess and
   (
     e.getType() instanceof CharType or
     e.getType() instanceof IntegralType or

csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs

@@ -437,7 +437,7 @@ class SignAnalysis
 
     unsafe void PointerCast(byte* src, byte* dst)
     {
-        var x = (int)(src-dst);
+        var x = (int)(src - dst);
         if (x < 0)
         {
             System.Console.WriteLine(x); // strictly negative
@@ -450,6 +450,20 @@ class SignAnalysis
             System.Console.WriteLine((int)to);
         }
     }
+
+    uint Unsigned() { return 1; }
+    void UnsignedCheck(int i)
+    {
+        long l = Unsigned();
+        if (l != 0)
+        {
+            System.Console.WriteLine(l); // strictly positive
+        }
+
+        uint x = (uint)i;
+        x++;
+        System.Console.WriteLine(x); // strictly positive
+    }
 }
 
 // semmle-extractor-options: /r:System.Linq.dll

csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected

@@ -90,6 +90,7 @@
 | SignAnalysis.cs:108:13:108:21 | Decimal de = ... | strictlyPositive |
 | SignAnalysis.cs:108:18:108:21 | 4.2 | strictlyPositive |
 | SignAnalysis.cs:109:34:109:35 | access to local variable de | strictlyPositive |
+| SignAnalysis.cs:110:13:110:13 | access to local variable c | positive |
 | SignAnalysis.cs:110:13:110:19 | Char c = ... | strictlyPositive |
 | SignAnalysis.cs:110:17:110:19 | a | strictlyPositive |
 | SignAnalysis.cs:111:34:111:34 | access to local variable c | strictlyPositive |
@@ -162,6 +163,8 @@
 | SignAnalysis.cs:306:21:306:22 | -... | strictlyNegative |
 | SignAnalysis.cs:306:22:306:22 | 1 | strictlyPositive |
 | SignAnalysis.cs:309:38:309:38 | access to local variable x | strictlyNegative |
+| SignAnalysis.cs:315:13:315:15 | access to local variable min | positive |
+| SignAnalysis.cs:316:13:316:15 | access to local variable max | positive |
 | SignAnalysis.cs:316:13:316:31 | Char max = ... | strictlyPositive |
 | SignAnalysis.cs:316:19:316:31 | access to constant MaxValue | strictlyPositive |
 | SignAnalysis.cs:317:13:317:23 | Int32 c = ... | strictlyPositive |
@@ -193,7 +196,13 @@
 | SignAnalysis.cs:342:38:342:38 | access to local variable x | negative |
 | SignAnalysis.cs:348:62:348:62 | 5 | strictlyPositive |
 | SignAnalysis.cs:351:38:351:38 | access to local variable i | strictlyNegative |
+| SignAnalysis.cs:357:13:357:13 | access to parameter i | positive |
+| SignAnalysis.cs:359:38:359:38 | access to parameter i | strictlyPositive |
 | SignAnalysis.cs:371:38:371:38 | access to local variable y | strictlyNegative |
+| SignAnalysis.cs:377:16:377:17 | access to local variable dp | positive |
+| SignAnalysis.cs:377:16:377:22 | Single* dp = ... | positive |
+| SignAnalysis.cs:377:21:377:22 | &... | positive |
+| SignAnalysis.cs:378:18:378:19 | access to local variable dp | positive |
 | SignAnalysis.cs:381:38:381:38 | access to local variable x | strictlyNegative |
 | SignAnalysis.cs:385:50:385:99 | access to constant Explicit | strictlyPositive |
 | SignAnalysis.cs:385:109:385:110 | 15 | strictlyPositive |
@@ -215,5 +224,25 @@
 | SignAnalysis.cs:428:19:428:24 | ... = ... | strictlyPositive |
 | SignAnalysis.cs:428:23:428:24 | 12 | strictlyPositive |
 | SignAnalysis.cs:434:38:434:38 | access to local variable i | strictlyNegative |
+| SignAnalysis.cs:440:23:440:25 | access to parameter src | positive |
+| SignAnalysis.cs:440:29:440:31 | access to parameter dst | positive |
 | SignAnalysis.cs:443:38:443:38 | access to local variable x | strictlyNegative |
 | SignAnalysis.cs:446:31:446:32 | 10 | strictlyPositive |
+| SignAnalysis.cs:448:22:448:23 | access to local variable to | positive |
+| SignAnalysis.cs:448:22:448:29 | Byte* to = ... | positive |
+| SignAnalysis.cs:448:27:448:29 | (...) ... | positive |
+| SignAnalysis.cs:450:38:450:44 | (...) ... | positive |
+| SignAnalysis.cs:450:43:450:44 | access to local variable to | positive |
+| SignAnalysis.cs:454:30:454:30 | 1 | strictlyPositive |
+| SignAnalysis.cs:454:30:454:30 | (...) ... | strictlyPositive |
+| SignAnalysis.cs:457:14:457:27 | Int64 l = ... | positive |
+| SignAnalysis.cs:457:18:457:27 | (...) ... | positive |
+| SignAnalysis.cs:457:18:457:27 | call to method Unsigned | positive |
+| SignAnalysis.cs:458:13:458:13 | access to local variable l | positive |
+| SignAnalysis.cs:460:38:460:38 | access to local variable l | strictlyPositive |
+| SignAnalysis.cs:463:14:463:14 | access to local variable x | positive |
+| SignAnalysis.cs:463:14:463:24 | UInt32 x = ... | positive |
+| SignAnalysis.cs:463:18:463:24 | (...) ... | positive |
+| SignAnalysis.cs:464:9:464:9 | access to local variable x | positive |
+| SignAnalysis.cs:464:9:464:11 | ...++ | positive |
+| SignAnalysis.cs:465:34:465:34 | access to local variable x | strictlyPositive |

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

@@ -245,24 +245,30 @@ Sign ssaDefSign(SsaVariable v) {
 /** Gets a possible sign for `e`. */
 cached
 Sign exprSign(Expr e) {
-  result = certainExprSign(e)
-  or
-  not exists(certainExprSign(e)) and
-  (
-    unknownSign(e)
+  exists(Sign s |
+    s = certainExprSign(e)
     or
-    exists(SsaVariable v | getARead(v) = e | result = ssaVariableSign(v, e))
-    or
-    e =
-      any(VarAccess access |
-        not exists(SsaVariable v | getARead(v) = access) and
-        (
-          result = fieldSign(getField(access.(FieldAccess))) or
-          not access instanceof FieldAccess
+    not exists(certainExprSign(e)) and
+    (
+      unknownSign(e)
+      or
+      exists(SsaVariable v | getARead(v) = e | s = ssaVariableSign(v, e))
+      or
+      e =
+        any(VarAccess access |
+          not exists(SsaVariable v | getARead(v) = access) and
+          (
+            s = fieldSign(getField(access.(FieldAccess))) or
+            not access instanceof FieldAccess
+          )
         )
-      )
-    or
-    result = specificSubExprSign(e)
+      or
+      s = specificSubExprSign(e)
+    )
+  |
+    if e.getType() instanceof UnsignedNumericType and s = TNeg()
+    then result = TPos()
+    else result = s
   )
 }
 

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

@@ -53,6 +53,8 @@ private module Impl {
   private import SignAnalysisCommon
   private import SsaReadPositionCommon
 
+  class UnsignedNumericType = CharacterType;
+
   float getNonIntegerValue(Expr e) {
     result = e.(LongLiteral).getValue().toFloat() or
     result = e.(FloatingPointLiteral).getValue().toFloat() or

java/ql/test/library-tests/dataflow/sign-analysis/A.java

@@ -9,4 +9,9 @@ public class A {
 
     return 0;
   }
+
+  void unsigned(int x) {
+    char c = (char)x;
+    System.out.println(c); // positive
+  }
 }

java/ql/test/library-tests/dataflow/sign-analysis/SignAnalysis.expected

@@ -1,3 +1,5 @@
 | A.java:4:14:4:14 | x | strictlyNegative |
 | A.java:6:9:6:9 | x | positive |
 | A.java:7:14:7:14 | y | strictlyPositive |
+| A.java:14:14:14:20 | (...)... | positive |
+| A.java:15:24:15:24 | c | positive |