From bfc761ec1bf7e3b4a587ac3c598c9df5cea9e1d8 Mon Sep 17 00:00:00 2001 From: Tim Pohlmann Date: Wed, 24 May 2023 16:06:46 +0200 Subject: [PATCH 1/7] Add tests for remainder --- .../RoslynSymbolicExecutionTest.Binary.cs | 113 ++++++++++++++++++ 1 file changed, 113 insertions(+) diff --git a/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs b/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs index 03fc6d2c8ee..5cc5e4e7c19 100644 --- a/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs +++ b/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs @@ -903,6 +903,119 @@ public void Binary_Division_Range(string expression, int? expectedMin, int? expe SETestContext.CreateCS(code, "int i, int j").Validator.TagValue("Value").Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(expectedMin, expectedMax)); } + [DataTestMethod] + [DataRow(21, 4, 1)] + [DataRow(21, -4, 1)] + [DataRow(-21, 4, -1)] + [DataRow(-21, -4, -1)] + [DataRow(4, 5, 4)] + [DataRow(-4, 5, -4)] + [DataRow(4, -5, 4)] + [DataRow(-4, -5, -4)] + [DataRow(5, 5, 0)] + [DataRow(5, -5, 0)] + [DataRow(-5, 5, 0)] + [DataRow(-5, -5, 0)] + [DataRow(5, 1, 0)] + [DataRow(5, -1, 0)] + [DataRow(-5, 1, 0)] + [DataRow(-5, -1, 0)] + public void Binary_Remainder_SingleValue(int left, int right, int expected) + { + var code = $""" + var left = {left}; + var right = {right}; + var value = left % right; + Tag("Value", value); + """; + SETestContext.CreateCS(code).Validator.TagValue("Value").Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(expected)); + } + + [DataTestMethod] + [DataRow("i >= 21 && j >= 5", 0, null)] + [DataRow("i >= 21 && j >= -5", 0, null)] + [DataRow("i >= 21 && j == 5", 0, 4)] + [DataRow("i >= 21 && j == -5", 0, 4)] + [DataRow("i >= 21 && j <= 5", 0, null)] + [DataRow("i >= 21 && j <= -5", 0, null)] + [DataRow("i >= -21 && j >= 5", -21, null)] + [DataRow("i >= -21 && j >= -5", -21, null)] + [DataRow("i >= -21 && j == 5", -4, 4)] + [DataRow("i >= -21 && j == -5", -4, 4)] + [DataRow("i >= -21 && j <= 5", -21, null)] + [DataRow("i >= -21 && j <= -5", -21, null)] + [DataRow("i == 21 && j >= 5", 0, 21)] + [DataRow("i == 21 && j >= -5", 0, 21)] + [DataRow("i == 21 && j <= 5", 0, 21)] + [DataRow("i == 21 && j <= -5", 0, 21)] + [DataRow("i == -21 && j >= 5", -21, 0)] + [DataRow("i == -21 && j >= -5", -21, 0)] + [DataRow("i == -21 && j <= 5", -21, 0)] + [DataRow("i == -21 && j <= -5", -21, 0)] + [DataRow("i <= 21 && j >= 5", null, 21)] + [DataRow("i <= 21 && j >= -5", null, 21)] + [DataRow("i <= 21 && j == 5", -4, 4)] + [DataRow("i <= 21 && j == -5", -4, 4)] + [DataRow("i <= 21 && j <= 5", null, 21)] + [DataRow("i <= 21 && j <= -5", null, 21)] + [DataRow("i <= -21 && j >= 5", null, 0)] + [DataRow("i <= -21 && j >= -5", null, 0)] + [DataRow("i <= -21 && j == 5", -4, 0)] + [DataRow("i <= -21 && j == -5", -4, 0)] + [DataRow("i <= -21 && j <= 5", null, 0)] + [DataRow("i <= -21 && j <= -5", null, 0)] + [DataRow("i >= 21 && j >= 0", 0, null)] + [DataRow("i >= 21 && j == 0", null, null)] + [DataRow("i >= 21 && j <= 0", 0, null)] + [DataRow("i >= -21 && j >= 0", -21, null)] + [DataRow("i >= -21 && j == 0", null, null)] + [DataRow("i >= -21 && j <= 0", -21, null)] + [DataRow("i <= 21 && j >= 0", null, 21)] + [DataRow("i <= 21 && j == 0", null, null)] + [DataRow("i <= 21 && j <= 0", null, 21)] + [DataRow("i <= -21 && j >= 0", null, 0)] + [DataRow("i <= -21 && j == 0", null, null)] + [DataRow("i <= -21 && j <= 0", null, 0)] + [DataRow("i >= 21 && j == 1", 0, 0)] + [DataRow("i >= -21 && j == 1", 0, 0)] + [DataRow("i <= 21 && j == 1", 0, 0)] + [DataRow("i <= -21 && j == 1", 0, 0)] + [DataRow("i >= 21 && j >= 5 && j <= 10", 0, 9)] + [DataRow("i >= 21 && j >= -5 && j <= 10", 0, 9)] + [DataRow("i >= 21 && j >= -10 && j <= 5", 0, 9)] + [DataRow("i >= 21 && j >= -10 && j <= -5", 0, 9)] + [DataRow("i >= -21 && j >= 5 && j <= 10", -9, 9)] + [DataRow("i >= -21 && j >= -5 && j <= 10", -9, 9)] + [DataRow("i >= -21 && j >= -10 && j <= 5", -9, 9)] + [DataRow("i >= -21 && j >= -10 && j <= -5", -9, 9)] + [DataRow("i <= 21 && j >= 5 && j <= 10", -9, 9)] + [DataRow("i <= 21 && j >= -5 && j <= 10", -9, 9)] + [DataRow("i <= 21 && j >= -10 && j <= 5", -9, 9)] + [DataRow("i <= 21 && j >= -10 && j <= -5", -9, 9)] + [DataRow("i <= -21 && j >= 5 && j <= 10", -9, 0)] + [DataRow("i <= -21 && j >= -5 && j <= 10", -9, 0)] + [DataRow("i <= -21 && j >= -10 && j <= 5", -9, 0)] + [DataRow("i <= -21 && j >= -10 && j <= -5", -9, 0)] + [DataRow("i >= 5 && i <= 10 && j >= 21", 5, 10)] + [DataRow("i >= 5 && i <= 10 && j <= -21", 5, 10)] + [DataRow("i >= -5 && i <= 10 && j >= 21", -5, 10)] + [DataRow("i >= -5 && i <= 10 && j <= -21", -5, 10)] + [DataRow("i >= -10 && i <= 5 && j >= 21", -10, 5)] + [DataRow("i >= -10 && i <= 5 && j <= -21", -10, 5)] + [DataRow("i >= -10 && i <= -5 && j >= 21", -10, -5)] + [DataRow("i >= -10 && i <= -5 && j <= -21", -10, -5)] + public void Binary_Remainder_Range(string expression, int? expectedMin, int? expectedMax) + { + var code = $$""" + if ({{expression}}) + { + var value = i % j; + Tag("Value", value); + } + """; + SETestContext.CreateCS(code, "int i, int j").Validator.TagValue("Value").Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(expectedMin, expectedMax)); + } + [DataTestMethod] [DataRow(0b0000, 0b0000, 0b0000)] [DataRow(0b0101, 0b0101, 0b0101)] From 6d216b0b611aad1f4e5976106606b1d8f9a117db Mon Sep 17 00:00:00 2001 From: Tim Pohlmann Date: Wed, 24 May 2023 18:00:29 +0200 Subject: [PATCH 2/7] Implement remainder logic --- .../OperationProcessors/Binary.Arithmetic.cs | 78 +++++++++++++++++++ 1 file changed, 78 insertions(+) diff --git a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs index 89b0db8f694..5f1071e5bb4 100644 --- a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs +++ b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs @@ -31,6 +31,8 @@ internal sealed partial class Binary BinaryOperatorKind.Subtract => NumberConstraint.From(left.Min - right.Max, left.Max - right.Min), BinaryOperatorKind.Multiply => CalculateMultiply(left, right), BinaryOperatorKind.Divide => CalculateDivide(left, right), + BinaryOperatorKind.Remainder when left.IsSingleValue && right.IsSingleValue => NumberConstraint.From(left.Min.Value % right.Min.Value), + BinaryOperatorKind.Remainder => CalculateRemainder(left, right), BinaryOperatorKind.And when left.IsSingleValue && right.IsSingleValue => NumberConstraint.From(left.Min.Value & right.Min.Value), BinaryOperatorKind.And => NumberConstraint.From(CalculateAndMin(left, right), CalculateAndMax(left, right)), BinaryOperatorKind.Or when left.IsSingleValue && right.IsSingleValue => NumberConstraint.From(left.Min.Value | right.Min.Value), @@ -129,6 +131,82 @@ private static NumberConstraint AccountForZero(NumberConstraint constraint) } } + private static NumberConstraint CalculateRemainder(NumberConstraint left, NumberConstraint right) + { + if (right.Min == 0 && right.Max == 0) + { + return null; + } + else if (right.Min == 0) + { + right = NumberConstraint.From(1, right.Max); + } + else if (right.Max == 0) + { + right = NumberConstraint.From(right.Min, -1); + } + return NumberConstraint.From(CalculateRemainderMin(left, right), CalculateRemainderMax(left, right)); + } + + private static BigInteger? CalculateRemainderMin(NumberConstraint left, NumberConstraint right) + { + if (left.IsPositive) + { + return left.Min >= AbsoluteMin(right) ? 0 : left.Min; + } + else + { + var minDerivedFromRight = -AbsoluteMax(right) + 1; + if (minDerivedFromRight is null) + { + return left.Min; + } + else + { + return left.Min is null ? minDerivedFromRight : BigInteger.Max(left.Min.Value, minDerivedFromRight.Value); + } + } + } + + private static BigInteger? CalculateRemainderMax(NumberConstraint left, NumberConstraint right) + { + if (left.IsNegative) + { + return left.Max <= -AbsoluteMin(right) ? 0 : left.Max; + } + else + { + var maxDerivedFromRight = AbsoluteMax(right) - 1; + if (maxDerivedFromRight is null) + { + return left.Max; + } + else + { + return left.Max is null ? maxDerivedFromRight : BigInteger.Min(left.Max.Value, maxDerivedFromRight.Value); + } + } + } + + private static BigInteger? AbsoluteMax(NumberConstraint constraint) => + constraint.Min is null || constraint.Max is null ? null : BigInteger.Max(BigInteger.Abs(constraint.Min.Value), BigInteger.Abs(constraint.Max.Value)); + + private static BigInteger? AbsoluteMin(NumberConstraint constraint) + { + if (constraint.IsPositive) + { + return constraint.Min; + } + else if (constraint.IsNegative) + { + return -constraint.Max; + } + else + { + return 0; + } + } + private static BigInteger? CalculateAndMin(NumberConstraint left, NumberConstraint right) { // The result can only be negative if both operands are negative => The result must be >= 0 unless both ranges include negative numbers. From 59fefc2e9587194db53c02b7c9f9849b0d32fdc8 Mon Sep 17 00:00:00 2001 From: Tim Pohlmann Date: Thu, 25 May 2023 17:01:48 +0200 Subject: [PATCH 3/7] Review 1 --- .../OperationProcessors/Binary.Arithmetic.cs | 44 +++++++++++++------ .../RoslynSymbolicExecutionTest.Binary.cs | 1 + 2 files changed, 31 insertions(+), 14 deletions(-) diff --git a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs index 5f1071e5bb4..60293585a56 100644 --- a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs +++ b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs @@ -19,6 +19,7 @@ */ using System.Numerics; +using Google.Protobuf.WellKnownTypes; using SonarAnalyzer.SymbolicExecution.Constraints; namespace SonarAnalyzer.SymbolicExecution.Roslyn.OperationProcessors; @@ -137,14 +138,7 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number { return null; } - else if (right.Min == 0) - { - right = NumberConstraint.From(1, right.Max); - } - else if (right.Max == 0) - { - right = NumberConstraint.From(right.Min, -1); - } + right = AccountForZero(right); return NumberConstraint.From(CalculateRemainderMin(left, right), CalculateRemainderMax(left, right)); } @@ -152,13 +146,16 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number { if (left.IsPositive) { - return left.Min >= AbsoluteMin(right) ? 0 : left.Min; + // Assuming both ranges are positive and every possible divisor value is > every possible dividend value => resulting range == dividend range. + // The sign of the divisor has no impact on the result => For negative or mixed divisor, we can take its absolute value and apply the same logic as above. + return left.Max is null || left.Max >= MinOfAbsoluteValues(right) ? 0 : left.Min; } else { - var minDerivedFromRight = -AbsoluteMax(right) + 1; + var minDerivedFromRight = -MaxOfAbsoluteValues(right) + 1; if (minDerivedFromRight is null) { + // If righ is not finite, there will always be a divisor which is absolutely bigger than any value in left => resulting range == dividend range. return left.Min; } else @@ -172,13 +169,16 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number { if (left.IsNegative) { - return left.Max <= -AbsoluteMin(right) ? 0 : left.Max; + // Assuming both ranges are negative and every possible divisor value is < every possible dividend value => resulting range == dividend range. + // The sign of the divisor has no impact on the result => For positive or mixed divisor, we can take its absolute value and apply the same logic as above. + return left.Max <= -MinOfAbsoluteValues(right) ? 0 : left.Max; } else { - var maxDerivedFromRight = AbsoluteMax(right) - 1; + var maxDerivedFromRight = MaxOfAbsoluteValues(right) - 1; if (maxDerivedFromRight is null) { + // If righ is not finite, there will always be a divisor which is absolutely bigger than any value in left => resulting range == dividend range. return left.Max; } else @@ -188,10 +188,26 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number } } - private static BigInteger? AbsoluteMax(NumberConstraint constraint) => + private static NumberConstraint AccountForZero(NumberConstraint constraint) + { + if (constraint.Min == 0) + { + return NumberConstraint.From(1, constraint.Max); + } + else if (constraint.Max == 0) + { + return NumberConstraint.From(constraint.Min, -1); + } + else + { + return constraint; + } + } + + private static BigInteger? MaxOfAbsoluteValues(NumberConstraint constraint) => constraint.Min is null || constraint.Max is null ? null : BigInteger.Max(BigInteger.Abs(constraint.Min.Value), BigInteger.Abs(constraint.Max.Value)); - private static BigInteger? AbsoluteMin(NumberConstraint constraint) + private static BigInteger? MinOfAbsoluteValues(NumberConstraint constraint) { if (constraint.IsPositive) { diff --git a/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs b/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs index 5cc5e4e7c19..595eea89530 100644 --- a/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs +++ b/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs @@ -1004,6 +1004,7 @@ public void Binary_Remainder_SingleValue(int left, int right, int expected) [DataRow("i >= -10 && i <= 5 && j <= -21", -10, 5)] [DataRow("i >= -10 && i <= -5 && j >= 21", -10, -5)] [DataRow("i >= -10 && i <= -5 && j <= -21", -10, -5)] + [DataRow("i >= 4 && i <= 7 && j >= 5 && j <= 10", 0, 7)] public void Binary_Remainder_Range(string expression, int? expectedMin, int? expectedMax) { var code = $$""" From eecb5cab48c88b5b6aef4ca4505832dd4c4f07b2 Mon Sep 17 00:00:00 2001 From: Tim Pohlmann Date: Thu, 25 May 2023 17:46:41 +0200 Subject: [PATCH 4/7] Refactor --- .../OperationProcessors/Binary.Arithmetic.cs | 44 ++++++++++--------- 1 file changed, 23 insertions(+), 21 deletions(-) diff --git a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs index 60293585a56..4a092e73943 100644 --- a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs +++ b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs @@ -144,48 +144,50 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number private static BigInteger? CalculateRemainderMin(NumberConstraint left, NumberConstraint right) { - if (left.IsPositive) + // If every divisor is absolutely bigger than any dividend => resulting range == dividend range. + // Otherwise, the result is bigger or equals 0 for positive dividend values and absolutely bigger than the divisor for negative dividend values. + if (left.CanBeNegative || left.Max < MinOfAbsoluteValues(right)) { - // Assuming both ranges are positive and every possible divisor value is > every possible dividend value => resulting range == dividend range. - // The sign of the divisor has no impact on the result => For negative or mixed divisor, we can take its absolute value and apply the same logic as above. - return left.Max is null || left.Max >= MinOfAbsoluteValues(right) ? 0 : left.Min; - } - else - { - var minDerivedFromRight = -MaxOfAbsoluteValues(right) + 1; - if (minDerivedFromRight is null) + if (right.Min is null || right.Max is null) { - // If righ is not finite, there will always be a divisor which is absolutely bigger than any value in left => resulting range == dividend range. + // If right is not finite, there will always be a divisor which is absolutely bigger than any value in left => resulting range == dividend range. return left.Min; } else { - return left.Min is null ? minDerivedFromRight : BigInteger.Max(left.Min.Value, minDerivedFromRight.Value); + // The result cannot be absolutely bigger than the absolute divisor - 1. For negative dividends the inverse is true. + var minDerivedFromRight = -MaxOfAbsoluteValues(right).Value + 1; + return left.Min is null ? minDerivedFromRight : BigInteger.Max(left.Min.Value, minDerivedFromRight); } } + else + { + return 0; + } } private static BigInteger? CalculateRemainderMax(NumberConstraint left, NumberConstraint right) { - if (left.IsNegative) + // If every divisor is absolutely bigger than any dividend => resulting range == dividend range. + // Otherwise, the result is smaller or equals 0 for negative dividend values and absolutely smaller than the divisor for positive dividend values. + if (left.CanBePositive || -left.Max < MinOfAbsoluteValues(right)) { - // Assuming both ranges are negative and every possible divisor value is < every possible dividend value => resulting range == dividend range. - // The sign of the divisor has no impact on the result => For positive or mixed divisor, we can take its absolute value and apply the same logic as above. - return left.Max <= -MinOfAbsoluteValues(right) ? 0 : left.Max; - } - else - { - var maxDerivedFromRight = MaxOfAbsoluteValues(right) - 1; - if (maxDerivedFromRight is null) + if (right.Min is null || right.Max is null) { - // If righ is not finite, there will always be a divisor which is absolutely bigger than any value in left => resulting range == dividend range. + // If right is not finite, there will always be a divisor which is absolutely bigger than any value in left => resulting range == dividend range. return left.Max; } else { + // The result cannot be absolutely bigger than the absolute divisor - 1. + var maxDerivedFromRight = MaxOfAbsoluteValues(right) - 1; return left.Max is null ? maxDerivedFromRight : BigInteger.Min(left.Max.Value, maxDerivedFromRight.Value); } } + else + { + return 0; + } } private static NumberConstraint AccountForZero(NumberConstraint constraint) From a28e61cc132f78bc3b7442ca08d761512e82fc2a Mon Sep 17 00:00:00 2001 From: Tim Pohlmann Date: Fri, 26 May 2023 10:18:58 +0200 Subject: [PATCH 5/7] Improve coverage by removing unnecessary null handling --- .../OperationProcessors/Binary.Arithmetic.cs | 31 +++++-------------- 1 file changed, 7 insertions(+), 24 deletions(-) diff --git a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs index 4a092e73943..648f10a1b39 100644 --- a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs +++ b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs @@ -19,7 +19,6 @@ */ using System.Numerics; -using Google.Protobuf.WellKnownTypes; using SonarAnalyzer.SymbolicExecution.Constraints; namespace SonarAnalyzer.SymbolicExecution.Roslyn.OperationProcessors; @@ -116,22 +115,6 @@ private static NumberConstraint CalculateDivide(NumberConstraint left, NumberCon return NumberConstraint.From(min, max); } - private static NumberConstraint AccountForZero(NumberConstraint constraint) - { - if (constraint.Min == 0) - { - return NumberConstraint.From(1, constraint.Max); - } - else if (constraint.Max == 0) - { - return NumberConstraint.From(constraint.Min, -1); - } - else - { - return constraint; - } - } - private static NumberConstraint CalculateRemainder(NumberConstraint left, NumberConstraint right) { if (right.Min == 0 && right.Max == 0) @@ -156,7 +139,7 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number else { // The result cannot be absolutely bigger than the absolute divisor - 1. For negative dividends the inverse is true. - var minDerivedFromRight = -MaxOfAbsoluteValues(right).Value + 1; + var minDerivedFromRight = -MaxOfAbsoluteValues(right) + 1; return left.Min is null ? minDerivedFromRight : BigInteger.Max(left.Min.Value, minDerivedFromRight); } } @@ -181,7 +164,7 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number { // The result cannot be absolutely bigger than the absolute divisor - 1. var maxDerivedFromRight = MaxOfAbsoluteValues(right) - 1; - return left.Max is null ? maxDerivedFromRight : BigInteger.Min(left.Max.Value, maxDerivedFromRight.Value); + return left.Max is null ? maxDerivedFromRight : BigInteger.Min(left.Max.Value, maxDerivedFromRight); } } else @@ -206,18 +189,18 @@ private static NumberConstraint AccountForZero(NumberConstraint constraint) } } - private static BigInteger? MaxOfAbsoluteValues(NumberConstraint constraint) => - constraint.Min is null || constraint.Max is null ? null : BigInteger.Max(BigInteger.Abs(constraint.Min.Value), BigInteger.Abs(constraint.Max.Value)); + private static BigInteger MaxOfAbsoluteValues(NumberConstraint constraint) => + BigInteger.Max(BigInteger.Abs(constraint.Min.Value), BigInteger.Abs(constraint.Max.Value)); - private static BigInteger? MinOfAbsoluteValues(NumberConstraint constraint) + private static BigInteger MinOfAbsoluteValues(NumberConstraint constraint) { if (constraint.IsPositive) { - return constraint.Min; + return constraint.Min.Value; } else if (constraint.IsNegative) { - return -constraint.Max; + return -constraint.Max.Value; } else { From 4ae6e73e7cbeb9bbc02f7ef3604fcde18dd7f2e4 Mon Sep 17 00:00:00 2001 From: Tim Pohlmann Date: Fri, 26 May 2023 15:29:05 +0200 Subject: [PATCH 6/7] Update UT --- .../SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.cs | 2 +- .../SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.vb | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.cs b/analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.cs index c2970daa71a..fbd3978c2ad 100644 --- a/analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.cs +++ b/analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.cs @@ -118,7 +118,7 @@ public void BasicOperators() _ = i * 2147483600; // FN i = 2 % j; - _ = i * 2147483600; // FN + _ = i * 2147483600; // Noncompliant } public void AssignmentOperators() diff --git a/analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.vb b/analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.vb index 9d08f8490e1..dd1fa5adff3 100644 --- a/analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.vb +++ b/analyzers/tests/SonarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.vb @@ -79,7 +79,7 @@ Public Class Sample __ = i * 2147483600 ' FN i = 2 Mod j - __ = i * 2147483600 ' FN + __ = i * 2147483600 ' Noncompliant Dim Result = Integer.MaxValue ^ 2 ' Compliant, result is Double End Sub From 30a5f828ef843aa30e5e663a79d3d99fbdf50d98 Mon Sep 17 00:00:00 2001 From: Tim Pohlmann Date: Wed, 31 May 2023 10:59:52 +0200 Subject: [PATCH 7/7] Review 2 --- .../OperationProcessors/Binary.Arithmetic.cs | 27 +++++++++++-------- .../RoslynSymbolicExecutionTest.Binary.cs | 1 + 2 files changed, 17 insertions(+), 11 deletions(-) diff --git a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs index 648f10a1b39..2d6d5063ad2 100644 --- a/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs +++ b/analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs @@ -31,7 +31,7 @@ internal sealed partial class Binary BinaryOperatorKind.Subtract => NumberConstraint.From(left.Min - right.Max, left.Max - right.Min), BinaryOperatorKind.Multiply => CalculateMultiply(left, right), BinaryOperatorKind.Divide => CalculateDivide(left, right), - BinaryOperatorKind.Remainder when left.IsSingleValue && right.IsSingleValue => NumberConstraint.From(left.Min.Value % right.Min.Value), + BinaryOperatorKind.Remainder when left.IsSingleValue && right.IsSingleValue && right.Min != 0 => NumberConstraint.From(left.Min.Value % right.Min.Value), BinaryOperatorKind.Remainder => CalculateRemainder(left, right), BinaryOperatorKind.And when left.IsSingleValue && right.IsSingleValue => NumberConstraint.From(left.Min.Value & right.Min.Value), BinaryOperatorKind.And => NumberConstraint.From(CalculateAndMin(left, right), CalculateAndMax(left, right)), @@ -121,24 +121,28 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number { return null; } - right = AccountForZero(right); - return NumberConstraint.From(CalculateRemainderMin(left, right), CalculateRemainderMax(left, right)); + else + { + right = AccountForZero(right); + return NumberConstraint.From(CalculateRemainderMin(left, right), CalculateRemainderMax(left, right)); + } } private static BigInteger? CalculateRemainderMin(NumberConstraint left, NumberConstraint right) { - // If every divisor is absolutely bigger than any dividend => resulting range == dividend range. - // Otherwise, the result is bigger or equals 0 for positive dividend values and absolutely bigger than the divisor for negative dividend values. + // If the absolute value of the divisor is bigger than the absolute value of the dividend, the result is equal to the dividend => + // If the absolute value of every divisor is bigger than the absolute value of any dividend => resulting range == dividend range. + // Otherwise, the result is between 0 and the absolute value of the divisor - 1 for positive dividends or in the same range multiplied by -1 for negative dividends. if (left.CanBeNegative || left.Max < MinOfAbsoluteValues(right)) { if (right.Min is null || right.Max is null) { - // If right is not finite, there will always be a divisor which is absolutely bigger than any value in left => resulting range == dividend range. + // If right is not finite, there will always be a divisor for which its absolute value is bigger than the absolute value of any value in left => resulting range == dividend range. return left.Min; } else { - // The result cannot be absolutely bigger than the absolute divisor - 1. For negative dividends the inverse is true. + // Otherwise, the result value is limited by the dividend and the divisor. var minDerivedFromRight = -MaxOfAbsoluteValues(right) + 1; return left.Min is null ? minDerivedFromRight : BigInteger.Max(left.Min.Value, minDerivedFromRight); } @@ -151,18 +155,19 @@ private static NumberConstraint CalculateRemainder(NumberConstraint left, Number private static BigInteger? CalculateRemainderMax(NumberConstraint left, NumberConstraint right) { - // If every divisor is absolutely bigger than any dividend => resulting range == dividend range. - // Otherwise, the result is smaller or equals 0 for negative dividend values and absolutely smaller than the divisor for positive dividend values. + // If the absolute value of the divisor is bigger than the absolute value of the dividend, the result is equal to the dividend => + // If the absolute value of every divisor is bigger than the absolute value of any dividend => resulting range == dividend range. + // Otherwise, the result is between 0 and the absolute value of the divisor - 1 for positive dividends or in the same range multiplied by -1 for negative dividends. if (left.CanBePositive || -left.Max < MinOfAbsoluteValues(right)) { if (right.Min is null || right.Max is null) { - // If right is not finite, there will always be a divisor which is absolutely bigger than any value in left => resulting range == dividend range. + // If right is not finite, there will always be a divisor for which its absolute value is bigger than the absolute value of any value in left => resulting range == dividend range. return left.Max; } else { - // The result cannot be absolutely bigger than the absolute divisor - 1. + // Otherwise, the result value is limited by the dividend and the divisor. var maxDerivedFromRight = MaxOfAbsoluteValues(right) - 1; return left.Max is null ? maxDerivedFromRight : BigInteger.Min(left.Max.Value, maxDerivedFromRight); } diff --git a/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs b/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs index 595eea89530..5f7878c912a 100644 --- a/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs +++ b/analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs @@ -1005,6 +1005,7 @@ public void Binary_Remainder_SingleValue(int left, int right, int expected) [DataRow("i >= -10 && i <= -5 && j >= 21", -10, -5)] [DataRow("i >= -10 && i <= -5 && j <= -21", -10, -5)] [DataRow("i >= 4 && i <= 7 && j >= 5 && j <= 10", 0, 7)] + [DataRow("i == 5 && j == 0", null, null)] public void Binary_Remainder_Range(string expression, int? expectedMin, int? expectedMax) { var code = $$"""