Skip to content

Commit

Permalink
SE Loops: Addition for same sign operands (#8760)
Browse files Browse the repository at this point in the history
  • Loading branch information
@Tim-Pohlmann
Tim-Pohlmann authored Feb 16, 2024
1 parent 32f2bdb commit 5d6b781
Show file tree
Hide file tree
Showing 6 changed files with 150 additions and 30 deletions.
48 changes: 31 additions & 17 deletions ...SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/ArithmeticCalculator.cs
View file
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),
_ => 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
27 changes: 27 additions & 0 deletions ...nalyzer.Test/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.ArithmeticCalculator.cs
View file
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));
}
}
}
13 changes: 7 additions & 6 deletions ...rs/tests/SonarAnalyzer.Test/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Loops.cs
View file
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
2 changes: 1 addition & 1 deletion ...ts/SonarAnalyzer.Test/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.cs
View file
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
2 changes: 1 addition & 1 deletion ...ts/SonarAnalyzer.Test/TestCases/SymbolicExecution/Roslyn/CalculationsShouldNotOverflow.vb
View file
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
88 changes: 83 additions & 5 deletions ...sts/SonarAnalyzer.Test/TestCases/SymbolicExecution/Roslyn/ConditionEvaluatesToConstant.cs
View file
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)
{
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

0 comments on commit 5d6b781

Please sign in to comment.