Skip to content

Commit

Permalink
SE: Add RemainderOperation (#7263)
Browse files Browse the repository at this point in the history
  • Loading branch information
@Tim-Pohlmann
Tim-Pohlmann authored May 31, 2023
1 parent 0fa082c commit c0ead58
Show file tree
Hide file tree
Showing 4 changed files with 201 additions and 2 deletions.
84 changes: 84 additions & 0 deletions ...rc/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 && 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)),
BinaryOperatorKind.Or when left.IsSingleValue && right.IsSingleValue => NumberConstraint.From(left.Min.Value | right.Min.Value),
Expand Down Expand Up @@ -113,6 +115,69 @@ private static NumberConstraint CalculateDivide(NumberConstraint left, NumberCon
return NumberConstraint.From(min, max);
}

private static NumberConstraint CalculateRemainder(NumberConstraint left, NumberConstraint right)
{
if (right.Min == 0 && right.Max == 0)
{
return null;
}
else
{
right = AccountForZero(right);
return NumberConstraint.From(CalculateRemainderMin(left, right), CalculateRemainderMax(left, right));
}
}

private static BigInteger? CalculateRemainderMin(NumberConstraint left, NumberConstraint right)
{
// 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 for which its absolute value is bigger than the absolute value of any value in left => resulting range == dividend range.
return left.Min;
}
else
{
// 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);
}
}
else
{
return 0;
}
}

private static BigInteger? CalculateRemainderMax(NumberConstraint left, NumberConstraint right)
{
// 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 for which its absolute value is bigger than the absolute value of any value in left => resulting range == dividend range.
return left.Max;
}
else
{
// 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);
}
}
else
{
return 0;
}
}

private static NumberConstraint AccountForZero(NumberConstraint constraint)
{
if (constraint.Min == 0)
Expand All @@ -129,6 +194,25 @@ private static NumberConstraint AccountForZero(NumberConstraint constraint)
}
}

private static BigInteger MaxOfAbsoluteValues(NumberConstraint constraint) =>
BigInteger.Max(BigInteger.Abs(constraint.Min.Value), BigInteger.Abs(constraint.Max.Value));

private static BigInteger MinOfAbsoluteValues(NumberConstraint constraint)
{
if (constraint.IsPositive)
{
return constraint.Min.Value;
}
else if (constraint.IsNegative)
{
return -constraint.Max.Value;
}
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.
Expand Down
115 changes: 115 additions & 0 deletions ...sts/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -908,6 +908,121 @@ 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)]
[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 = $$"""
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)]
Expand Down
2 changes: 1 addition & 1 deletion ...onarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,7 @@ public void BasicOperators()
_ = i * 2147483600; // FN

i = 2 % j;
_ = i * 2147483600; // FN
_ = i * 2147483600; // Noncompliant
}

public void AssignmentOperators()
Expand Down
2 changes: 1 addition & 1 deletion ...onarAnalyzer.UnitTest/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.vb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit c0ead58

Please sign in to comment.