Skip to content

Commit

Permalink
SE: Add BitXorOperation
Browse files Browse the repository at this point in the history
  • Loading branch information
@antonioaversa
antonioaversa committed May 24, 2023
1 parent 8aa1194 commit 8407081
Show file tree
Hide file tree
Showing 4 changed files with 159 additions and 1 deletion.
16 changes: 16 additions & 0 deletions analyzers/src/SonarAnalyzer.Common/SymbolicExecution/Constraints/NumberConstraint.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,22 @@ public static NumberConstraint From(BigInteger? min, BigInteger? max)
public bool CanContain(BigInteger value) =>
!(value < Min || Max < value);

public bool CanOverlap(NumberConstraint other)
{
if (Min is null)
{
return other.Min is null || Max < other.Min;
}
else if (Max < other.Min || Min > other.Max)
{
return false;
}
else
{
return true;
}
}

public override bool Equals(object obj) =>
obj is NumberConstraint other && other.Min == Min && other.Max == Max;

Expand Down
44 changes: 44 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 @@ -34,6 +34,8 @@ internal sealed partial class Binary : BranchingProcessor<IBinaryOperationWrappe
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
};

Expand Down Expand Up @@ -141,6 +143,48 @@ private static NumberConstraint CalculateMultiply(NumberConstraint left, NumberC
}
}

private static BigInteger? CalculateXorMin(NumberConstraint left, NumberConstraint right)
{
if (left.IsPositive && right.IsPositive)
{
return left.CanOverlap(right) ? 0 : Min(left.Min - right.Max, right.Min - left.Max);
}
else if (left.IsNegative && right.IsNegative)
{
return left.CanOverlap(right) ? 0 : Min(left.Max - right.Min, right.Max - left.Min);
}
return null;

static BigInteger? Min(BigInteger? first, BigInteger? second)
{
if (first is null)
{
return second;
}
else if (second is null)
{
return first;
}
else
{
return BigInteger.Min(first.Value, second.Value);
}
}
}

private static BigInteger? CalculateXorMax(NumberConstraint left, NumberConstraint right)
{
if ((left.IsPositive && right.IsPositive) || (left.IsPositive && right.CanBePositive) || (right.IsPositive && left.CanBeNegative))
{
return left.Max.HasValue && right.Max.HasValue ? PositiveMagnitude(left.Max.Value | right.Max.Value) : null;
}
else if ((left.IsPositive && right.IsNegative) || (left.IsNegative && right.IsPositive))
{
return -1;
}
return null;
}

private static BigInteger? NegativeMagnitude(BigInteger value)
{
// For increasing powers of 2 with negative sign, we're looking for the longest chain of 1 from the MSB side
Expand Down
31 changes: 31 additions & 0 deletions analyzers/tests/SonarAnalyzer.UnitTest/SymbolicExecution/Constraints/NumberConstraintTest.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,5 +191,36 @@ public void CanContain_True(int? min, int? max, int value) =>
[DataRow(42, null, 41)]
public void CanContain_False(int? min, int? max, int value) =>
NumberConstraint.From(min, max).CanContain(value).Should().BeFalse();

[DataTestMethod]
[DataRow(null, +2, null, +3, true)]
[DataRow(null, +3, null, +2, true)]
[DataRow(null, -3, null, +2, true)]
[DataRow(+2, null, +3, null, true)]
[DataRow(+3, null, +2, null, true)]
[DataRow(-3, null, +2, null, true)]
[DataRow(-3, -1, -2, 0, true)]
[DataRow(-3, -1, 0, 0, false)]
[DataRow(1, 3, 0, null, true)]
[DataRow(1, 3, 1, null, true)]
[DataRow(1, 3, 3, null, true)]
[DataRow(1, 3, 4, null, false)]
[DataRow(1, 1, 0, null, true)]
[DataRow(1, 1, 1, null, true)]
[DataRow(1, 1, 2, null, false)]
[DataRow(0, null, 1, 3, true)]
[DataRow(1, null, 1, 3, true)]
[DataRow(3, null, 1, 3, true)]
[DataRow(4, null, 1, 3, false)]
[DataRow(0, null, 1, 1, true)]
[DataRow(1, null, 1, 1, true)]
[DataRow(2, null, 1, 1, false)]
[DataRow(1, 3, 0, 4, true)]
[DataRow(0, 1, 1, 3, true)]
[DataRow(0, 2, 1, 3, true)]
[DataRow(0, 3, 1, 3, true)]
[DataRow(0, 4, 1, 3, true)]
public void CanOverlap(int? firstMin, int? firstMax, int? secondMin, int? secondMax, bool result) =>
NumberConstraint.From(firstMin, firstMax).CanOverlap(NumberConstraint.From(secondMin, secondMax)).Should().Be(result);
}
}
69 changes: 68 additions & 1 deletion ...sts/SonarAnalyzer.UnitTest/SymbolicExecution/Roslyn/RoslynSymbolicExecutionTest.Binary.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -839,7 +839,7 @@ public void Binary_BitAnd_SingleValue(int left, int right, int expected)
var value = left & right;
Tag("Value", value);
""";
SETestContext.CreateCS(code).Validator.ValidateTag("Value", x => x.Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(expected)));
SETestContext.CreateCS(code).Validator.TagValue("Value").Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(expected));
}

[DataTestMethod]
Expand Down Expand Up @@ -946,4 +946,71 @@ public void Binary_BitOr_Range(string expression, int? expectedMin, int? expecte
SETestContext.CreateCS(code, "int i, int j").Validator.TagValue("Value").Should().HaveOnlyConstraints(ObjectConstraint.NotNull);
}
}

[DataTestMethod]
[DataRow(0b0000, 0b0000, 0b0000)]
[DataRow(0b0101, 0b0101, 0b0000)]
[DataRow(0b0101, 0b0001, 0b0100)]
[DataRow(0b1010, 0b0110, 0b1100)]
[DataRow(0b1010, 0b0000, 0b1010)]
[DataRow(0b1111, 0b1111, 0b0000)]
[DataRow(5, -5, -2)]
[DataRow(5, -4, -7)]
[DataRow(-5, -5, 0)]
[DataRow(-5, -4, 7)]
public void Binary_BitXor_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 >= 4 && j >= 6", 0, null)]
[DataRow("i >= 4 && j >= -6", null, null)]
[DataRow("i >= 4 && j <= 6", null, null)]
[DataRow("i >= 4 && j <= -6", null, -1)]
[DataRow("i >= -4 && j >= 6", null, null)]
[DataRow("i >= -4 && j >= -6", null, null)]
[DataRow("i >= -4 && j <= 6", null, null)]
[DataRow("i >= -4 && j <= -6", null, null)] // exact range: null, -1
[DataRow("i == 4 && j >= 6", 2, null)]
[DataRow("i == 4 && j >= -6", null, null)] // exact range: -8, null
[DataRow("i == 4 && j <= 6", null, 7)]
[DataRow("i == 4 && j <= -6", null, -1)] // exact range: null, -2
[DataRow("i == -4 && j >= 6", null, null)] // exact range: null, -5
[DataRow("i == -4 && j >= -6", null, null)] // exact range: null, 7
[DataRow("i == -4 && j <= 6", null, null)] // exact range: -8, null
[DataRow("i == -4 && j <= -6", -2, null)] // exact range: 4, null
[DataRow("i <= 4 && j >= 6", null, null)]
[DataRow("i <= 4 && j >= -6", null, null)]
[DataRow("i <= 4 && j <= 6", null, null)]
[DataRow("i <= 4 && j <= -6", null, null)]
[DataRow("i <= -4 && j >= 6", null, null)] // exact range: null, -1
[DataRow("i <= -4 && j >= -6", null, null)]
[DataRow("i <= -4 && j <= 6", null, null)]
[DataRow("i <= -4 && j <= -6", 0, null)]
public void Binary_BitXor_Range(string expression, int? expectedMin, int? expectedMax)
{
var code = $$"""
if ({{expression}})
{
var value = i ^ j;
Tag("Value", value);
}
""";

if (expectedMin is not null || expectedMax is not null)
{
SETestContext.CreateCS(code, "int i, int j").Validator.TagValue("Value").Should().HaveOnlyConstraints(ObjectConstraint.NotNull, NumberConstraint.From(expectedMin, expectedMax));
}
else
{
SETestContext.CreateCS(code, "int i, int j").Validator.TagValue("Value").Should().HaveOnlyConstraints(ObjectConstraint.NotNull);
}
}
}

0 comments on commit 8407081

Please sign in to comment.