Skip to content

Commit

Permalink
Implement Binary.PreProcess and add simple tests
Browse files Browse the repository at this point in the history
  • Loading branch information
Tim-Pohlmann committed May 5, 2023
1 parent b529eb3 commit d048521
Show file tree
Hide file tree
Showing 2 changed files with 58 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
* Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
*/

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

namespace SonarAnalyzer.SymbolicExecution.Roslyn.OperationProcessors;
Expand All @@ -44,6 +45,37 @@ protected override ProgramState LearnBranchingConstraint(ProgramState state, IBi
return state;
}

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)
{
state = state.SetOperationConstraint(operation.WrappedOperation, Calculate(leftNumber, rightNumber, calculation));
}
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(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 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 @@ -657,4 +657,30 @@ public void Binary_StringConcatenation_Compund_CS(string expression)
validator.ValidateContainsOperation(OperationKind.Binary);
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()
{
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(37)));
}
}

0 comments on commit d048521

Please sign in to comment.