SE: Add BitXorOperation #7246

antonioaversa · 2023-05-22T12:13:45Z

Part of #7267

Based on the property (holding for positive numbers only) that $a - b \leq a \oplus b \leq a + b$

antonioaversa · 2023-05-25T13:59:56Z

public bool IsSingleValue => Min.HasValue && Min == Max; seems fully covered by the following cases:

            NumberConstraint.From(42).IsSingleValue.Should().BeTrue();
            NumberConstraint.From(1, 1).IsSingleValue.Should().BeTrue();
            NumberConstraint.From(null, 42).IsSingleValue.Should().BeFalse();
            NumberConstraint.From(42, null).IsSingleValue.Should().BeFalse();
            NumberConstraint.From(1, 100).IsSingleValue.Should().BeFalse();

So the sub-100% coverage seems a glitch of AltCover.

Tim-Pohlmann

I think there are some things wrong. Let me know what you think and then I'll do another review.

...s/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs

Tim-Pohlmann · 2023-05-25T14:37:07Z

...s/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs

+        {
+            return left.CanOverlap(right) ? 0 : Min(left.Max - right.Min, right.Max - left.Min);
+        }
+        return null;


This should also be true, I think:

Suggested change

return null;

if (left.Min.HasValue && right.Min.HasValue)

{

NegativeMagnitude(BigInteger.Min(left.Min.Value, right.Min.Value));

}

return null;

This one breaks multiple cases, and flipping sign either inside and outside NegativeMagnitude doesn't fix it.

Given how little impactful this case can in practice be, I would not invest more time in supporting it.

Try this, it actually fixes two of the existing UTs.

Suggested change

return null;

else if ((left.IsPositive || right.IsNegative) && left.Max.HasValue && right.Min.HasValue)

{

return NegativeMagnitude(-BigInteger.Max(left.Max.Value, BigInteger.Abs(right.Min.Value)));

}

else if ((left.IsNegative || right.IsPositive) && left.Min.HasValue && right.Max.HasValue)

{

return NegativeMagnitude(-BigInteger.Max(BigInteger.Abs(left.Min.Value), right.Max.Value));

}

else if (left.Min.HasValue && left.Max.HasValue && right.Min.HasValue && right.Max.HasValue)

{

return NegativeMagnitude(-BigInteger.Max(

BigInteger.Max(BigInteger.Abs(left.Min.Value), right.Max.Value),

BigInteger.Max(left.Max.Value, BigInteger.Abs(right.Min.Value))));

}

else

{

return null;

}

Tried and worked for existing use cases. However, after some analysis, I could find a case that breaks your code:

[DataRow("i >= -3 && i <= -1 && j >= -4 && j <=-2", 0, 3)] // Expected SETestContext.CreateCS(code, "int i, int j").Validator.TagValue("Value") // to have constraints {NotNull, Number from 0 to 3}, but {Number from 0 to 3} are missing // and additional {Number from 3 to 7} are present. Actual are {NotNull, Number from 3 to 7}.

Even if I got CalculateXorMax (see comments below), an issue surely also affects CalculateXorMin.
So, I am not applying these changes, and only keep basic cases where we have solid understanding of how to calculate lower bounds.

Again, given how little impactful these cases can in practice be, I would not invest more time in supporting them.

The test case is not affected by the code I suggested. When I add my code suggestion to the current implementation it does what I expect: It improves two test cases ("i == 4 && j >= -6" and "i == -4 && j <= 6").

Tim-Pohlmann · 2023-05-25T14:42:18Z

...s/src/SonarAnalyzer.Common/SymbolicExecution/Roslyn/OperationProcessors/Binary.Arithmetic.cs

+        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;


This logic confuses me. Shouldn't it be symmetric? From my understanding the following should be correct:

Suggested change

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;

if ((left.IsPositive && right.IsNegative) || (left.IsNegative && right.IsPositive))

{

return -1;

}

else if (left.Max.HasValue && right.Max.HasValue)

{

return PositiveMagnitude(left.Max.Value | right.Max.Value);

}

else

{

return null;

}

Try this, it's the opposite to my suggested min:

if ((left.IsPositive && right.IsNegative) || (left.IsNegative && right.IsPositive)) { return -1; } else if ((left.IsPositive || right.IsPositive) && left.Max.HasValue && right.Max.HasValue) { return PositiveMagnitude(BigInteger.Max(left.Max.Value, right.Max.Value)); } else if ((left.IsNegative || right.IsNegative) && left.Min.HasValue && right.Min.HasValue) { return PositiveMagnitude(BigInteger.Max(BigInteger.Abs(left.Min.Value), BigInteger.Abs(right.Min.Value))); } else if (left.Min.HasValue && left.Max.HasValue && right.Min.HasValue && right.Max.HasValue) { return PositiveMagnitude(BigInteger.Max( BigInteger.Max(left.Max.Value, right.Max.Value), BigInteger.Max(BigInteger.Abs(left.Min.Value), BigInteger.Abs(right.Min.Value)))); } else { return null; }

Tried that too, and it breaks for the following test case:

[DataRow("i == 4 && j >= -6", null, null)] // exact range: -8, null Expected SETestContext.CreateCS(code, "int i, int j").Validator.TagValue("Value") to have constraints {NotNull}, but additional {Number from * to 7} are present. Actual are {NotNull, Number from * to 7}.

Counterexample: i = 4 = 0b00000100 and j = 11 = 0b00001011 => i ^ j = 0b00001111 =15 > 7

There is something wrong in the branch that returns 7:

else if ((left.IsNegative || right.IsNegative) && left.Min.HasValue && right.Min.HasValue) { return PositiveMagnitude(BigInteger.Max(BigInteger.Abs(left.Min.Value), BigInteger.Abs(right.Min.Value))); }

So, for max too, I would revert the code to the one surely working, and not invest more time in trying to support these cases, unless there is proven usefulness in doing so.

Also, I am not sure that return left.Max.HasValue && right.Max.HasValue ? PositiveMagnitude(BigInteger.Max(left.Max.Value, right.Max.Value)) : null; works correctly for negative numbers, so I am keeping return left.Max.HasValue && right.Max.HasValue ? PositiveMagnitude(left.Max.Value | right.Max.Value) : null;, for which I have strong intuition than it does and that works on all UTs.

I cannot reproduce the failing test case. Replacing the current implementation with my suggestion improves 5 test cases.

Tim-Pohlmann

I cannot reproduce the failing test cases. Applying my code suggestions improves multiple existing test cases. Please try once more to integrate the changes.

antonioaversa · 2023-05-31T12:04:11Z

I cannot reproduce the failing test cases. Applying my code suggestions improves multiple existing test cases. Please try once more to integrate the changes.

I may have missed something when trying to validate your suggestion. Since the release is already happening, and this work won't be included in it, I am keeping this PR on hold until your suggestions in #7310 get merged into this PR.

I still think we have already hit a diminishing return with this development, and we shouldn't invest more effort to cover more cases.

sonarcloud · 2023-06-05T12:15:47Z

Kudos, SonarCloud Quality Gate passed!

0 Bugs
0 Vulnerabilities
0 Security Hotspots
0 Code Smells

No Coverage information
No Duplication information

sonarcloud · 2023-06-05T12:18:54Z

Kudos, SonarCloud Quality Gate passed!

0 Bugs
0 Vulnerabilities
0 Security Hotspots
0 Code Smells

100.0% Coverage
0.0% Duplication

antonioaversa · 2023-06-05T12:40:08Z

#7310 has been merged into this PR.
We now have 100% coverage, green tests and no wrong ranges derivations, as far as I can tell.

Tim-Pohlmann

LGTM!

antonioaversa added the Sprint: SE label May 22, 2023

github-actions bot assigned antonioaversa May 22, 2023

antonioaversa force-pushed the Antonio/se-bitwise-xor branch 5 times, most recently from 8407081 to 9df6079 Compare May 25, 2023 06:49

antonioaversa requested a review from Tim-Pohlmann May 25, 2023 12:01

github-actions bot assigned Tim-Pohlmann and unassigned antonioaversa May 25, 2023

antonioaversa marked this pull request as ready for review May 25, 2023 12:01

Tim-Pohlmann requested changes May 25, 2023

View reviewed changes

github-actions bot assigned antonioaversa and unassigned Tim-Pohlmann May 25, 2023

antonioaversa added 5 commits May 26, 2023 16:15

SE: Add BitXorOperation

d00c5cd

Increase coverage

ec1a603

Increase coverage 2

eaf4215

Increase coverage and fix CanOverlap

af7caca

Review 1

72f1b86

antonioaversa force-pushed the Antonio/se-bitwise-xor branch from 47b41c6 to 72f1b86 Compare May 26, 2023 14:16

antonioaversa added 3 commits May 26, 2023 16:20

Fix UTs

5b11d33

Revert changes adding mixed ranges

9e7e43b

Increase coverage

c0ae9ec

antonioaversa requested a review from Tim-Pohlmann May 30, 2023 08:56

github-actions bot assigned Tim-Pohlmann and unassigned antonioaversa May 30, 2023

Tim-Pohlmann requested changes May 31, 2023

View reviewed changes

github-actions bot assigned antonioaversa and unassigned Tim-Pohlmann May 31, 2023

Tim-Pohlmann mentioned this pull request May 31, 2023

SE: Improve XOROperation #7310

Merged

SE: Improve XOROperation (#7310)

6b5578c

antonioaversa requested a review from Tim-Pohlmann June 5, 2023 12:38

github-actions bot assigned Tim-Pohlmann and unassigned antonioaversa Jun 5, 2023

Tim-Pohlmann approved these changes Jun 5, 2023

View reviewed changes

github-actions bot assigned antonioaversa and unassigned Tim-Pohlmann Jun 5, 2023

antonioaversa merged commit 1614d7d into master Jun 8, 2023

antonioaversa deleted the Antonio/se-bitwise-xor branch June 8, 2023 07:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

SE: Add BitXorOperation #7246

SE: Add BitXorOperation #7246

antonioaversa commented May 22, 2023 •

edited

Loading

antonioaversa commented May 25, 2023

Tim-Pohlmann left a comment

Tim-Pohlmann May 25, 2023

antonioaversa May 25, 2023

Tim-Pohlmann May 26, 2023 •

edited

Loading

antonioaversa May 26, 2023 •

edited

Loading

Tim-Pohlmann May 31, 2023

Tim-Pohlmann May 25, 2023

Tim-Pohlmann May 26, 2023 •

edited

Loading

antonioaversa May 26, 2023

Tim-Pohlmann May 31, 2023

Tim-Pohlmann left a comment

antonioaversa commented May 31, 2023

sonarcloud bot commented Jun 5, 2023

sonarcloud bot commented Jun 5, 2023

antonioaversa commented Jun 5, 2023

Tim-Pohlmann left a comment

-        return null;
+        else if ((left.IsPositive || right.IsNegative) && left.Max.HasValue && right.Min.HasValue)
+        {
+            return NegativeMagnitude(-BigInteger.Max(left.Max.Value, BigInteger.Abs(right.Min.Value)));
+        }
+        else if ((left.IsNegative || right.IsPositive) && left.Min.HasValue && right.Max.HasValue)
+        {
+            return NegativeMagnitude(-BigInteger.Max(BigInteger.Abs(left.Min.Value), right.Max.Value));
+        }
+        else if (left.Min.HasValue && left.Max.HasValue && right.Min.HasValue && right.Max.HasValue)
+        {
+            return NegativeMagnitude(-BigInteger.Max(
+                BigInteger.Max(BigInteger.Abs(left.Min.Value), right.Max.Value),
+                BigInteger.Max(left.Max.Value, BigInteger.Abs(right.Min.Value))));
+        }
+        else
+        {
+            return null;
+        }

SE: Add BitXorOperation #7246

SE: Add BitXorOperation #7246

Conversation

antonioaversa commented May 22, 2023 • edited Loading

antonioaversa commented May 25, 2023

Tim-Pohlmann left a comment

Choose a reason for hiding this comment

Tim-Pohlmann May 25, 2023

Choose a reason for hiding this comment

antonioaversa May 25, 2023

Choose a reason for hiding this comment

Tim-Pohlmann May 26, 2023 • edited Loading

Choose a reason for hiding this comment

antonioaversa May 26, 2023 • edited Loading

Choose a reason for hiding this comment

Tim-Pohlmann May 31, 2023

Choose a reason for hiding this comment

Tim-Pohlmann May 25, 2023

Choose a reason for hiding this comment

Tim-Pohlmann May 26, 2023 • edited Loading

Choose a reason for hiding this comment

antonioaversa May 26, 2023

Choose a reason for hiding this comment

Tim-Pohlmann May 31, 2023

Choose a reason for hiding this comment

Tim-Pohlmann left a comment

Choose a reason for hiding this comment

antonioaversa commented May 31, 2023

sonarcloud bot commented Jun 5, 2023

sonarcloud bot commented Jun 5, 2023

antonioaversa commented Jun 5, 2023

Tim-Pohlmann left a comment

Choose a reason for hiding this comment

antonioaversa commented May 22, 2023 •

edited

Loading

Tim-Pohlmann May 26, 2023 •

edited

Loading

antonioaversa May 26, 2023 •

edited

Loading

Tim-Pohlmann May 26, 2023 •

edited

Loading