Skip to content

Commit

Permalink
Review 1
Browse files Browse the repository at this point in the history
  • Loading branch information
Tim-Pohlmann committed May 8, 2023
1 parent d048521 commit 2b3af3b
Show file tree
Hide file tree
Showing 2 changed files with 51 additions and 41 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
*/

using System.Numerics;
using Microsoft.CodeAnalysis;
using SonarAnalyzer.SymbolicExecution.Constraints;

namespace SonarAnalyzer.SymbolicExecution.Roslyn.OperationProcessors;
Expand Down Expand Up @@ -47,34 +48,29 @@ protected override ProgramState LearnBranchingConstraint(ProgramState state, IBi

protected override ProgramState PreProcess(ProgramState state, IBinaryOperationWrapper operation)
{
if (Calculation(operation.OperatorKind) is { } calculation
&& operation.LeftOperand?.TrackedSymbol() is { } leftSymbol
&& operation.RightOperand?.TrackedSymbol() is { } rightSymbol
&& state[leftSymbol]?.Constraint<NumberConstraint>() is { } leftNumber
&& state[rightSymbol]?.Constraint<NumberConstraint>() is { } rightNumber)
if (operation.LeftOperand is { } leftOperand
&& operation.RightOperand is { } rightOperand
&& state[leftOperand]?.Constraint<NumberConstraint>() is { } leftNumber
&& state[rightOperand]?.Constraint<NumberConstraint>() is { } rightNumber
&& Calculate(operation.OperatorKind, leftNumber, rightNumber) is { } newConstraint)
{
state = state.SetOperationConstraint(operation.WrappedOperation, Calculate(leftNumber, rightNumber, calculation));
state = state.SetOperationConstraint(operation.WrappedOperation, newConstraint);
}
return state;
}

private static Func<BigInteger?, BigInteger?, BigInteger?> Calculation(BinaryOperatorKind kind) => kind switch
{
BinaryOperatorKind.Add => (a, b) => a + b,
BinaryOperatorKind.Subtract => (a, b) => a - b,
_ => null
};
private static NumberConstraint Calculate(BinaryOperatorKind kind, NumberConstraint left, NumberConstraint right) =>
NumberConstraint.From(Calculation(kind, left.Min, right.Min), Calculation(kind, left.Max, right.Max));

private static NumberConstraint Calculate(NumberConstraint left, NumberConstraint right, Func<BigInteger?, BigInteger?, BigInteger?> calculation)
{
var min = left.Min is not null && right.Min is not null
? calculation(left.Min, right.Min)
: null;
var max = left.Max is not null && right.Max is not null
? calculation(left.Max, right.Max)
: null;
return NumberConstraint.From(min, max);
}
private static BigInteger? Calculation(BinaryOperatorKind kind, BigInteger? a, BigInteger? b) =>
a is not null && b is not null
? kind switch
{
BinaryOperatorKind.Add => a + b,
BinaryOperatorKind.Subtract => a - b,
_ => null
}
: null;

private static ProgramState LearnBranchingEqualityConstraint<T>(ProgramState state, IBinaryOperationWrapper binary, bool falseBranch)
where T : SymbolicConstraint
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -658,29 +658,43 @@ public void Binary_StringConcatenation_Compund_CS(string expression)
validator.ValidateTag("S", x => x.Should().HaveOnlyConstraint(ObjectConstraint.Null)); // FIXME: s is not null here (https://github.com/SonarSource/sonar-dotnet/issues/7111)
}

[TestMethod]
public void Binary_Add_UpdatesNumberConstraint_CS()
{
var code = """
var i = 42;
var j = 5;
var x = i + j;
Tag("X", x);
""";
var validator = SETestContext.CreateCS(code).Validator;
validator.ValidateTag("X", x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(47)));
}

[TestMethod]
public void Binary_Substract_UpdatesNumberConstraint_CS()
[DataTestMethod]
[DataRow("i + j", 47)]
[DataRow("i + 1", 43)]
[DataRow("i + j + 1", 48)]
[DataRow("(i + 1) + j", 48)]
[DataRow("(i + j) + 1", 48)]
[DataRow("i + (1 + j)", 48)]
[DataRow("1 + (i + j)", 48)]
[DataRow("i - j", 37)]
[DataRow("j - i", -37)]
[DataRow("i - 1", 41)]
[DataRow("i - j - 1", 36)]
[DataRow("(i - 1) - j", 36)]
[DataRow("(i - j) - 1", 36)]
[DataRow("i - (j - 1)", 38)]
[DataRow("i - (1 - j)", 46)]
[DataRow("1 - (i - j)", -36)]
[DataRow("i + j - 1", 46)]
[DataRow("(i + j) - 1", 46)]
[DataRow("(i + 1) - j", 38)]
[DataRow("i + (j - 1)", 46)]
[DataRow("i + (1 - j)", 38)]
[DataRow("1 + (i - j)", 38)]
[DataRow("i - j + 1", 38)]
[DataRow("(i - j) + 1", 38)]
[DataRow("(i - 1) + j", 46)]
[DataRow("i - (j + 1)", 36)]
[DataRow("1 - (i + j)", -46)]
public void Binary_Calculations_UpdatesNumberConstraint(string expression, int result)
{
var code = """
var code = $"""
var i = 42;
var j = 5;
var x = i - j;
Tag("X", x);
var value = {expression};
Tag("Value", value);
""";
var validator = SETestContext.CreateCS(code).Validator;
validator.ValidateTag("X", x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(37)));
validator.ValidateTag("Value", x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(result)));
}
}

0 comments on commit 2b3af3b

Please sign in to comment.