[OLD] Improve Symbolic Execution to handle Nullables

sonaranalyzer-dotnet/src/SonarAnalyzer.CSharp/Helpers/SymbolicExecution/InvocationVisitor.cs

@@ -44,6 +44,7 @@ public InvocationVisitor(InvocationExpressionSyntax invocation, SemanticModel se
         internal ProgramState ProcessInvocation()
         {
             var symbol = semanticModel.GetSymbolInfo(invocation).Symbol;
+            var typeSymbol = semanticModel.GetTypeInfo(invocation).Type;
 
             var methodSymbol = symbol as IMethodSymbol;
             var invocationArgsCount = invocation.ArgumentList?.Arguments.Count ?? 0;
@@ -75,7 +76,7 @@ internal ProgramState ProcessInvocation()
 
             return programState
                 .PopValues(invocationArgsCount + 1)
-                .PushValue(new SymbolicValue());
+                .PushValue(SymbolicValue.Create(typeSymbol));
         }
 
         private ProgramState HandleNameofExpression(int argumentsCount)
@@ -86,7 +87,7 @@ private ProgramState HandleNameofExpression(int argumentsCount)
                 .PopValues(argumentsCount)
                 .PopValue();
 
-            var nameof = new SymbolicValue();
+            var nameof = SymbolicValue.Create();
             newProgramState = newProgramState.PushValue(nameof);
             return nameof.SetConstraint(ObjectConstraint.NotNull, newProgramState);
         }
@@ -105,7 +106,7 @@ private ProgramState HandleStringNullCheckMethod()
                 return newProgramState.PushValue(SymbolicValue.True);
             }
 
-            return newProgramState.PushValue(new SymbolicValue());
+            return newProgramState.PushValue(SymbolicValue.Create()); // never returns a nullable<T>
         }
 
         private ProgramState HandleStaticEqualsCall()
@@ -236,13 +237,15 @@ public ProgramState PushWithConstraint()
 
             private ProgramState SetConstraint(ReferenceEqualsSymbolicValue refEquals, ProgramState programState)
             {
-                if (AreBothArgumentsNull())
+                if (AreBothArgumentsNull() ||
+                    IsComparingNullToOptionalNone())
                 {
                     return refEquals.SetConstraint(BoolConstraint.True, programState);
                 }
 
                 if (IsAnyArgumentNonNullValueType() ||
-                    ArgumentsHaveDifferentNullability())
+                    ArgumentsHaveDifferentNullability() ||
+                    IsComparingNullToOptionalSome())
                 {
                     return refEquals.SetConstraint(BoolConstraint.False, programState);
                 }
@@ -287,6 +290,18 @@ private bool AreBothArgumentsNull()
                 return valueLeft.HasConstraint(ObjectConstraint.Null, programState) &&
                     valueRight.HasConstraint(ObjectConstraint.Null, programState);
             }
+
+            private bool IsComparingNullToOptionalNone()
+            {
+                return valueLeft.HasConstraint(OptionalConstraint.None, programState) && valueRight.HasConstraint(ObjectConstraint.Null, programState) ||
+                    valueLeft.HasConstraint(ObjectConstraint.Null, programState) && valueRight.HasConstraint(OptionalConstraint.None, programState);
+            }
+
+            private bool IsComparingNullToOptionalSome()
+            {
+                return valueLeft.HasConstraint(OptionalConstraint.Some, programState) && valueRight.HasConstraint(ObjectConstraint.Null, programState) ||
+                    valueLeft.HasConstraint(ObjectConstraint.Null, programState) && valueRight.HasConstraint(OptionalConstraint.Some, programState);
+            }
         }
     }
 }

sonaranalyzer-dotnet/src/SonarAnalyzer.CSharp/Helpers/SymbolicExecution/SymbolicValueHelper.cs

@@ -27,9 +27,11 @@ public static class SymbolicValueHelper
     {
         public static SymbolicValue CreateFieldSymbolicValue(this IFieldSymbol fieldSymbol)
         {
+            var symbolicValue = SymbolicValue.Create(fieldSymbol.Type);
+
             if (!fieldSymbol.IsConst || !fieldSymbol.HasConstantValue)
             {
-                return new SymbolicValue();
+                return symbolicValue;
             }
 
             var boolValue = fieldSymbol.ConstantValue as bool?;
@@ -42,7 +44,7 @@ public static SymbolicValue CreateFieldSymbolicValue(this IFieldSymbol fieldSymb
 
             return fieldSymbol.ConstantValue == null
                 ? SymbolicValue.Null
-                : new SymbolicValue();
+                : symbolicValue;
         }
     }
 }

sonaranalyzer-dotnet/src/SonarAnalyzer.Common/Helpers/SymbolicExecution/Constraints/OptionalConstraint.cs

@@ -0,0 +1,38 @@
+/*
+ * SonarAnalyzer for .NET
+ * Copyright (C) 2015-2017 SonarSource SA
+ * mailto: contact AT sonarsource DOT com
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 3 of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License
+ * along with this program; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
+ */
+
+namespace SonarAnalyzer.Helpers.FlowAnalysis.Common
+{
+    internal sealed class OptionalConstraint : SymbolicValueConstraint
+    {
+        public static readonly OptionalConstraint None = new OptionalConstraint();
+        public static readonly OptionalConstraint Some = new OptionalConstraint();
+
+        public override SymbolicValueConstraint OppositeForLogicalNot =>
+            this == None ? Some : None;
+
+        public override string ToString()
+        {
+            return this == None
+                ? "None"
+                : "Some";
+        }
+    }
+}

sonaranalyzer-dotnet/src/SonarAnalyzer.Common/Helpers/SymbolicExecution/ExplodedGraph.cs

@@ -326,7 +326,7 @@ private void EnqueueStartNode()
             var initialProgramState = new ProgramState();
             foreach (var parameter in declarationParameters)
             {
-                var sv = new SymbolicValue();
+                var sv = SymbolicValue.Create(parameter.Type);
                 initialProgramState = initialProgramState.StoreSymbolicValue(parameter, sv);
                 initialProgramState = SetNonNullConstraintIfValueType(parameter, sv, initialProgramState);
             }

sonaranalyzer-dotnet/src/SonarAnalyzer.Common/Helpers/SymbolicExecution/ProgramState.cs

@@ -347,6 +347,7 @@ internal ProgramState RemoveSymbols(Func<ISymbol, bool> predicate)
             // SVs for live symbols
             var usedSymbolicValues = cleanedValues.Values
                 .Concat(DistinguishedReferences)
+                .Concat(cleanedValues.Values.OfType<NullableSymbolicValue>().Select(x => x.WrappedValue))
                 .ToImmutableHashSet();
 
             var cleanedConstraints = Constraints

sonaranalyzer-dotnet/src/SonarAnalyzer.Common/Helpers/SymbolicExecution/SymbolicValues/Binary/EqualsSymbolicValue.cs

@@ -40,8 +40,33 @@ internal override IEnumerable<ProgramState> SetConstraint(BoolConstraint boolCon
                     .SelectMany(ps => LeftOperand.TrySetConstraint(rightConstraint, ps));
             }
 
-            return RightOperand.TrySetConstraint(leftConstraint?.OppositeForLogicalNot, programState)
-                .SelectMany(ps => LeftOperand.TrySetConstraint(rightConstraint?.OppositeForLogicalNot, ps));
+            return NegateConstraint(RightOperand, leftConstraint)
+                .SelectMany(constraint => RightOperand.TrySetConstraint(constraint, programState))
+                .SelectMany(ps => NegateConstraint(LeftOperand, rightConstraint)
+                    .SelectMany(constraint => LeftOperand.TrySetConstraint(constraint, ps)));
+        }
+
+        private static IEnumerable<SymbolicValueConstraint> NegateConstraint(SymbolicValue value, SymbolicValueConstraint constraint)
+        {
+            if (value is NullableSymbolicValue)
+            {
+                if (constraint is BoolConstraint)
+                {
+                    return new[] { constraint?.OppositeForLogicalNot, OptionalConstraint.None };
+                }
+
+                if (constraint == ObjectConstraint.Null)
+                {
+                    return new[] { BoolConstraint.True, BoolConstraint.False };
+                }
+
+                if (constraint == ObjectConstraint.NotNull)
+                {
+                    return new[] { OptionalConstraint.None };
+                }
+            }
+
+            return new[] { constraint?.OppositeForLogicalNot };
         }
     }
 }

sonaranalyzer-dotnet/src/SonarAnalyzer.Common/Helpers/SymbolicExecution/SymbolicValues/Binary/ReferenceEqualsSymbolicValue.cs

@@ -31,7 +31,7 @@ protected override BinaryRelationship GetRelationship(SymbolicValue left, Symbol
         {
             return new ReferenceEqualsRelationship(left, right);
         }
-        
+
         public override string ToString()
         {
             return $"RefEq({LeftOperand}, {RightOperand})";

sonaranalyzer-dotnet/src/SonarAnalyzer.Common/Helpers/SymbolicExecution/SymbolicValues/NullableSymbolicValue.cs

@@ -0,0 +1,119 @@
+/*
+ * SonarAnalyzer for .NET
+ * Copyright (C) 2015-2017 SonarSource SA
+ * mailto: contact AT sonarsource DOT com
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 3 of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License
+ * along with this program; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
+ */
+
+using System;
+using System.Collections.Generic;
+using System.Collections.Immutable;
+using System.Linq;
+
+namespace SonarAnalyzer.Helpers.FlowAnalysis.Common
+{
+    public class NullableSymbolicValue : SymbolicValue
+    {
+        public SymbolicValue WrappedValue { get; }
+
+        public NullableSymbolicValue(SymbolicValue wrappedValue)
+        {
+            this.WrappedValue = wrappedValue;
+        }
+
+        public override IEnumerable<ProgramState> TrySetConstraint(SymbolicValueConstraint constraint,
+            ProgramState currentProgramState)
+        {
+            var oldConstraint = currentProgramState.Constraints.GetValueOrDefault(this);
+
+            if (constraint == ObjectConstraint.Null)
+            {
+                if (oldConstraint == null)
+                {
+                    return new[] { SetConstraint(OptionalConstraint.None, currentProgramState) };
+                }
+                else if (oldConstraint == OptionalConstraint.None)
+                {
+                    return new[] { currentProgramState };
+                }
+                else if (oldConstraint == OptionalConstraint.Some)
+                {
+                    return Enumerable.Empty<ProgramState>();
+                }
+                else
+                {
+                    throw new InvalidOperationException($"Not expecting to set a {ObjectConstraint.Null} " +
+                        $"constraint on a Symbolic Value with the {constraint} constraint.");
+                }
+            }
+            else if (constraint == ObjectConstraint.NotNull)
+            {
+                if (oldConstraint == null)
+                {
+                    return new[] { SetConstraint(OptionalConstraint.Some, currentProgramState) };
+                }
+                else if (oldConstraint == OptionalConstraint.None)
+                {
+                    return Enumerable.Empty<ProgramState>();
+                }
+                else if (oldConstraint == OptionalConstraint.Some)
+                {
+                    return new[] { currentProgramState };
+                }
+                else
+                {
+                    throw new InvalidOperationException($"Not expecting to set a {ObjectConstraint.NotNull} " +
+                        $"constraint on a Symbolic Value with the {constraint} constraint.");
+                }
+            }
+            else
+            {
+                if (oldConstraint == null)
+                {
+                    if (constraint is OptionalConstraint)
+                    {
+                        return new[] { SetConstraint(constraint, currentProgramState) };
+                    }
+
+                    return new[] { this.WrappedValue.SetConstraint(constraint,
+                        SetConstraint(OptionalConstraint.Some, currentProgramState)) };
+                }
+                else if (oldConstraint == OptionalConstraint.None)
+                {
+                    return Enumerable.Empty<ProgramState>();
+                }
+                else if (oldConstraint == OptionalConstraint.Some)
+                {
+                    return new[] { this.WrappedValue.SetConstraint(constraint, currentProgramState) };
+                }
+                else
+                {
+                    return new[] { this.WrappedValue.SetConstraint(constraint, currentProgramState) };
+                }
+            }
+        }
+
+        public override string ToString()
+        {
+            if (base.identifier != null)
+            {
+                return $"NULLABLE_SV_{base.identifier}";
+            }
+
+            return this.WrappedValue?.ToString() ?? base.ToString();
+        }
+    }
+}