Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SE Loops: Addition for same sign operands #8760

Merged
merged 4 commits into from
Feb 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -25,23 +25,37 @@ namespace SonarAnalyzer.SymbolicExecution.Roslyn.OperationProcessors;

internal static class ArithmeticCalculator
{
public static NumberConstraint Calculate(BinaryOperatorKind kind, NumberConstraint left, NumberConstraint right, bool isInLoop) =>
isInLoop ? null : kind switch
{
BinaryOperatorKind.Add => NumberConstraint.From(left.Min + right.Min, left.Max + right.Max),
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),
BinaryOperatorKind.Or => NumberConstraint.From(CalculateOrMin(left, right), CalculateOrMax(left, right)),
BinaryOperatorKind.ExclusiveOr when left.IsSingleValue && right.IsSingleValue => NumberConstraint.From(left.Min.Value ^ right.Min.Value),
BinaryOperatorKind.ExclusiveOr => NumberConstraint.From(CalculateXorMin(left, right), CalculateXorMax(left, right)),
_ => null
};
public static NumberConstraint Calculate(BinaryOperatorKind kind, NumberConstraint left, NumberConstraint right, bool isInLoop)
{
if (isInLoop)
{
return kind switch
{
BinaryOperatorKind.Add when left.IsPositive && right.IsPositive => NumberConstraint.From(left.Min + right.Min, null),
BinaryOperatorKind.Add when left.IsNegative && right.IsNegative => NumberConstraint.From(null, left.Max + right.Max),
gregory-paidis-sonarsource marked this conversation as resolved.
Show resolved Hide resolved
_ => null
};
}
else
{
return kind switch
{
BinaryOperatorKind.Add => NumberConstraint.From(left.Min + right.Min, left.Max + right.Max),
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),
BinaryOperatorKind.Or => NumberConstraint.From(CalculateOrMin(left, right), CalculateOrMax(left, right)),
BinaryOperatorKind.ExclusiveOr when left.IsSingleValue && right.IsSingleValue => NumberConstraint.From(left.Min.Value ^ right.Min.Value),
BinaryOperatorKind.ExclusiveOr => NumberConstraint.From(CalculateXorMin(left, right), CalculateXorMax(left, right)),
_ => null
};
}
}

public static BigInteger? BiggestMinimum(NumberConstraint left, NumberConstraint right)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -619,4 +619,31 @@ public void Calculate_BitXor_Range(string expression, int? expectedMin, int? exp
validator.TagValue("I").Should().HaveOnlyConstraints(ObjectConstraint.NotNull);
}
}

[DataTestMethod]
[DataRow(5, 5, 10, null)]
[DataRow(5, -5, null, null)]
[DataRow(-5, 5, null, null)]
[DataRow(-5, -5, null, -10)]
public void Calculate_InLoop_Addition(int i, int j, int? valMin, int? valMax)
{
var code = $$"""
var i = {{i}};
var j = {{j}};
while (Condition)
{
var value = i + j;
Tag("Value", value);
}
""";
var validator = SETestContext.CreateCS(code).Validator;
if (valMin.HasValue || valMax.HasValue)
{
validator.TagValues("Value").Should().AllSatisfy(x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(valMin, valMax)));
}
else
{
validator.TagValues("Value").Should().AllSatisfy(x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull));
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -209,7 +209,7 @@ End If
},
x =>
{
x[i].Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(null, 9));
x[i].Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(1, 9));
x[value].Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(42));
});
validator.TagStates("Unreachable").Should().BeEmpty();
Expand Down Expand Up @@ -390,15 +390,16 @@ End If
End While
""";
var validator = SETestContext.CreateVB(code, new AddConstraintOnInvocationCheck()).Validator;
validator.ValidateExitReachCount(3);
validator.ValidateTagOrder("If", "After", "If", "Else", "After");
validator.ValidateExitReachCount(4);
validator.ValidateTagOrder("If", "After", "If", "Else", "After", "After");
validator.TagValues("If").Should().SatisfyRespectively(
x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(0)),
x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(null, 9)));
x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(1, 9)));
validator.TagValue("Else").Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(10, null));
validator.TagValues("After").Should().SatisfyRespectively(
x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull), // Initial pass through "if"
x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(10, null))); // Second pass through "if", false branch
x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(1, null)), // Initial pass through "if"
x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(10, null)), // Second pass through "if", false branch
x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(2, null))); // Second pass through "if", true branch
}

[TestMethod]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -186,7 +186,7 @@ public void Branching(int i)
for (i = 2147483546; i <= 2147483547; i++)
_ = i + 100; // Compliant
for (i = 2147483546; i <= 2147483547; i++)
_ = i + 101; // FN
_ = i + 101; // Noncompliant
}

public void Branching2(int i)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ Public Class Sample
__ = i + 100 ' Compliant
Next
For i = 2147483546 To 2147483547
__ = i + 101 ' FN
__ = i + 101 ' Noncompliant
Next
End Sub

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1670,8 +1670,10 @@ void ForLoop_Nested()
for (int i = 0; i < 10; i++)
for (int j = i + 1; j < i + 10; j++)
{
_ = j >= 0 ? 0 : 42; // FN
_ = j > 0 ? 0 : 42; // FN
_ = j >= 0 ? 0 : 42; // Noncompliant
// Secondary@-1
_ = j > 0 ? 0 : 42; // Noncompliant
// Secondary@-1
_ = j < 18 ? 0 : 42; // Compliant
_ = j < 19 ? 0 : 42; // FN
_ = i + j < 27 ? 0 : 42; // Compliant
Expand All @@ -1687,8 +1689,10 @@ void ForLoop_Nested_IncrementInside()
{
for (int j = i + 1; j < i + 10;)
{
_ = j >= 0 ? 0 : 42; // FN
_ = j > 0 ? 0 : 42; // FN
_ = j >= 0 ? 0 : 42; // Noncompliant
// Secondary@-1
_ = j > 0 ? 0 : 42; // Noncompliant
// Secondary@-1
_ = j < 18 ? 0 : 42; // Compliant
_ = j < 19 ? 0 : 42; // FN
_ = i + j < 27 ? 0 : 42; // Compliant
Expand All @@ -1710,7 +1714,8 @@ void ForLoop_MultipleLoopVariables()
_ = j > 0 ? 0 : 42; // Noncompliant
// Secondary@-1
_ = j < 3 ? 0 : 42; // Compliant
_ = i + j > 0 ? 0 : 42; // FN
_ = i + j > 0 ? 0 : 42; // Noncompliant
// Secondary@-1
_ = i + j > 1 ? 0 : 42; // Compliant
}
}
Expand All @@ -1737,6 +1742,79 @@ void ForLoop_ZeroOrOneExecutions()
}
}

class LoopVariableTracking
{
void InitializationInLoop(bool condition)

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't you add any testcases for double-negative, or did I miss it?

{
while (condition)
{
var i = 0;
i = i + 1;
if (i != 0) // Noncompliant
{
Console.WriteLine();
}
}
}

void InitializationInLoop_TwoVariables(bool condition)
{
while (condition)
{
var i = 1;
var j = 1;
j = i + j;
if (j >= 0) // Noncompliant
{
Console.WriteLine();
}
}
}

void InitializationBeforeLoop(bool condition)
{
var i = 0;
while (condition)
{
i = i + 1;
if (i != 0) // Noncompliant
{
Console.WriteLine();
}
}
}

void AssignmentToOtherVariable(bool condition)
{
var i = 0;
var j = 0;
while (condition)
{
if (j >= 0) // Noncompliant FP
{
Console.WriteLine();
}
j = i + 1;
i = -5;
}
}

void AssignmentFromInLoopVariable(bool condition)
{
var j = 0;
while (condition)
{
var i = 0;
if (j >= 0) // Noncompliant
{
Console.WriteLine();
}
j = i + 1;
i = -5;
}
}
}

public class GuardedTests
{
public void Guarded(string s1)
Expand Down
Loading