Support conditional branching in SE

analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/RoslynSymbolicExecution.cs

@@ -22,6 +22,7 @@
 using System.Collections.Generic;
 using System.Linq;
 using SonarAnalyzer.CFG.Roslyn;
+using SonarAnalyzer.SymbolicExecution.Constraints;
 using SonarAnalyzer.SymbolicExecution.Roslyn.Checks;
 using SonarAnalyzer.SymbolicExecution.Roslyn.OperationProcessors;
 using StyleCop.Analyzers.Lightup;
@@ -92,14 +93,13 @@ private IEnumerable<ExplodedNode> ProcessBranching(ExplodedNode node)
             }
             else
             {
-                // ToDo: This is a temporary simplification until we support condition-based and condition-building decisions https://github.com/SonarSource/sonar-dotnet/issues/5308
-                foreach (var successor in node.Block.Successors)
+                foreach (var successor in node.Block.Successors.Where(x => IsReachable(node, x)))
                 {
                     if (successor.Destination is not null)
                     {
                         yield return successor.FinallyRegions.Any() // When exiting finally region(s), redirect to 1st finally instead of the normal destination
                             ? FromFinally(new FinallyPoint(node.FinallyPoint, successor))
-                            : new ExplodedNode(successor.Destination, node.State, node.FinallyPoint);
+                            : new(successor.Destination, node.State, node.FinallyPoint);
                     }
                     else if (successor.Source.EnclosingRegion.Kind == ControlFlowRegionKind.Finally)    // Redirect from finally back to the original place (or outer finally on the same branch)
                     {
@@ -109,7 +109,7 @@ private IEnumerable<ExplodedNode> ProcessBranching(ExplodedNode node)
             }
 
             ExplodedNode FromFinally(FinallyPoint finallyPoint) =>
-                new ExplodedNode(cfg.Blocks[finallyPoint.BlockIndex], node.State, finallyPoint.IsFinallyBlock ? finallyPoint : finallyPoint.Previous);
+                new(cfg.Blocks[finallyPoint.BlockIndex], node.State, finallyPoint.IsFinallyBlock ? finallyPoint : finallyPoint.Previous);
         }
 
         private IEnumerable<ExplodedNode> ProcessOperation(ExplodedNode node)
@@ -167,5 +167,16 @@ private void NotifyExecutionCompleted()
 
         private SymbolicContext EnsureContext(SymbolicContext current, ProgramState newState) =>
             current.State == newState ? current : new SymbolicContext(symbolicValueCounter, current.Operation, newState);
+
+        private static bool IsReachable(ExplodedNode node, ControlFlowBranch branch) =>
+            node.Block.ConditionKind != ControlFlowConditionKind.None
+            && node.Block.BranchValue.TrackedSymbol() is { } branchSymbol
+            && node.State[branchSymbol] is { } sv
+            && sv.HasConstraint<BoolConstraint>()
+                ? IsReachable(branch, node.Block.ConditionKind == ControlFlowConditionKind.WhenTrue, sv.HasConstraint(BoolConstraint.True))
+                : true;    // Unconditional or we don't know the value and need to explore both paths
+
+        private static bool IsReachable(ControlFlowBranch branch, bool condition, bool constraint) =>
+            branch.IsConditionalSuccessor ? condition == constraint : condition != constraint;
     }
 }

analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Branching.cs

@@ -296,5 +296,195 @@ public void Branching_VisitedSymbolicValue_IsImmutable()
             validator.ValidateTag("GetHashCode", x => x.HasConstraint(TestConstraint.First).Should().BeFalse()); // Nobody set the constraint on that path
             validator.ValidateExitReachCount(2);    // Once for each state
         }
+
+        [TestMethod]
+        public void Branching_TrueConstraint_VisitsIfBranch()
+        {
+            const string code = @"
+var value = true;
+if (value)
+{
+    Tag(""If"");
+}
+else
+{
+    Tag(""Else"");
+}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder(
+                "If",
+                "End");
+        }
+
+        [TestMethod]
+        public void Branching_TrueConstraintNegated_VisitsElseBranch()
+        {
+            const string code = @"
+var value = true;
+if (!value)
+{
+    Tag(""If"");
+}
+else
+{
+    Tag(""Else"");
+}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder(
+                "Else",
+                "End");
+        }
+
+        [TestMethod]
+        public void Branching_FalseConstraint_VisitsElseBranch()
+        {
+            const string code = @"
+var value = false;
+if (value)
+{
+    Tag(""If"");
+}
+else
+{
+    Tag(""Else"");
+}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder(
+                "Else",
+                "End");
+        }
+
+        [TestMethod]
+        public void Branching_FalseConstraintNegated_VisitsIfBranch()
+        {
+            const string code = @"
+var value = false;
+if (!value)
+{
+    Tag(""If"");
+}
+else
+{
+    Tag(""Else"");
+}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder(
+                "If",
+                "End");
+        }
+
+        [TestMethod]
+        public void Branching_NoConstraint_VisitsBothBranches()
+        {
+            const string code = @"
+var value = boolParameter; // Unknown constraints
+if (value)
+{
+    Tag(""If"");
+}
+else
+{
+    Tag(""Else"");
+}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder(
+                "If",
+                "Else",
+                "End");
+        }
+
+        [TestMethod]
+        public void Branching_OtherConstraint_VisitsBothBranches()
+        {
+            const string code = @"
+if (boolParameter)
+{
+    Tag(""If"");
+}
+else
+{
+    Tag(""Else"");
+}
+Tag(""End"");";
+            var check = new PostProcessTestCheck(x => x.Operation.Instance.TrackedSymbol() is { } symbol ? x.SetSymbolConstraint(symbol, DummyConstraint.Dummy) : x.State);
+            SETestContext.CreateCS(code, check).Validator.ValidateTagOrder(
+                "If",
+                "Else",
+                "End");
+        }
+
+        [TestMethod]
+        public void Branching_BoolConstraints_ComplexCase()
+        {
+            const string code = @"
+var isTrue = true;
+var isFalse = false;
+if (isTrue && isTrue && !isFalse)
+{
+    if (isFalse || !isTrue)
+    {
+        Tag(""UnreachableIf"");
+    }
+    else if (isFalse)
+    {
+        Tag(""UnreachableElseIf"");
+    }
+    else
+    {
+        Tag(""Reachable"");
+    }
+}
+else
+{
+    Tag(""UnreachableElse"");
+}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder(
+                "Reachable",
+                "End");
+        }
+
+        [TestMethod]
+        public void Branching_TrueLiteral_VisitsIfBranch_NotSupported()
+        {
+            const string code = @"
+if (true)
+{
+    Tag(""If"");
+}
+else
+{
+    Tag(""Else"");
+}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder(
+                "If",
+                "Else", // ToDo: This should not be here, branch operation symbolic value is not persisted yet
+                "End");
+        }
+
+        [TestMethod]
+        public void Branching_TrueConstraint_SwitchStatement_BinaryOperationNotSupported()
+        {
+            const string code = @"
+var isTrue = true;
+switch (isTrue)
+{
+    case true:
+        Tag(""True"");
+        break;
+    case false:
+        Tag(""False"");
+        break;
+    default:
+        Tag(""Default"");
+}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder(
+                "True",
+                "False",    // This should not be here, switch statement produces BinaryOperatin with isTrue==true
+                "Default",  // This should not be here, switch statement produces BinaryOperatin with isTrue==true
+                "End");
+        }
     }
 }

analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Constants.cs

@@ -84,6 +84,18 @@ public void PreProcess_EqualityCheck_ConstantPropagation()
             validator.Validate("SimpleAssignment: t = 0 == zero (Implicit)", x => x.State[x.Operation].HasConstraint(BoolConstraint.True).Should().BeTrue());
         }
 
+        [TestMethod]
+        public void PreProcess_OptionalArgument_DoesNotSetConstraint()
+        {
+            const string code = @"
+public void Main(bool arg = true)
+{
+    Tag(""Arg"", arg);
+}
+private void Tag(string name, object arg) { }";
+            SETestContext.CreateCSMethod(code, new EmptyTestCheck()).Validator.ValidateTag("Arg", x => x.Should().BeNull());
+        }
+
         private static BoolConstraint GetConstraint(bool value) =>
             value ? BoolConstraint.True : BoolConstraint.False;
     }

analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Loops.cs

@@ -149,5 +149,20 @@ public void GoTo_InstructionVisitedMaxTwice()
                 .And.ContainSingle(x => x.HasConstraint(TestConstraint.First) && !x.HasConstraint(BoolConstraint.True))
                 .And.ContainSingle(x => x.HasConstraint(TestConstraint.First) && x.HasConstraint(BoolConstraint.True) && !x.HasConstraint(DummyConstraint.Dummy));
         }
+
+        [DataTestMethod]
+        [DataRow("for (var i = 0; condition; i++)")]
+        [DataRow("while (condition)")]
+        public void Loops_FalseConditionNotExecuted(string loop)
+        {
+            var code = $@"
+var condition = false;
+{loop}
+{{
+    Tag(""Loop"");
+}}
+Tag(""End"");";
+            SETestContext.CreateCS(code).Validator.ValidateTagOrder("End");
+        }
     }
 }

analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.PatternMatching.cs

@@ -0,0 +1,43 @@
+/*
+ * SonarAnalyzer for .NET
+ * Copyright (C) 2015-2022 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 FluentAssertions;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using SonarAnalyzer.UnitTest.TestFramework.SymbolicExecution;
+
+namespace SonarAnalyzer.UnitTest.SymbolicExecution.Roslyn
+{
+    public partial class RoslynSymbolicExecutionTest
+    {
+        [TestMethod]
+        public void Patterns_TrueConstraint_SwitchExpression_NotSupported()
+        {
+            const string code = @"
+var isTrue = true;
+var value = isTrue switch
+{
+    true => true,
+    false => false
+};
+Tag(""Value"", value);";
+            SETestContext.CreateCS(code).Validator.ValidateTag("Value", x => x.Should().BeNull()); // Should have BoolConstraint.True instead
+        }
+    }
+}

analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/LocksReleasedAllPaths.Mutex.NetFx.cs

@@ -94,7 +94,7 @@ public static void CompliantFromDocs(string mutexName, MutexSecurity mutexSecuri
             // Enter the mutex, and hold it until the program exits.
             try
             {
-                m.WaitOne(); // Noncompliant
+                m.WaitOne();
             }
             catch (UnauthorizedAccessException ex)
             {