Chillersanim Chillersanim - 29 days ago 11
C# Question

Code contracts: Array access upper bound warning when mapping to 2d array

Good day.

I'm testing out C# code contracts.

I've been working on some matrix implementations, and wanted to use code contracts to do arithmetic checking (eg. when is a matrix multiplication valid).

In order to store the data, I use a one dimensional array and access the data like this:

values[r * TotalColumns + c]


r: row to access

c: column to access

My problem is:

Code contracts thinks that this access might be above the upper bounds of the array.

I think that I've given enough information, in order for the system to validate that this is not possible (see example bellow).

My question is:

Can you take a look at my example code and explain to me, what I did wrong and why Code Contracts still thinks that this array acces is unsafe?

The code in question is in the GetValue method and marked with a comment.

public class Test
{
[ContractPublicPropertyName("Values")]
private readonly double[] values;

[ContractPublicPropertyName("X")]
private readonly int x;

[ContractPublicPropertyName("Y")]
private readonly int y;

// Getter properties for required contract visibility.
public double[] Values => this.values;
public int X => this.x;
public int Y => this.y;

public Test(int x, int y)
{
Contract.Requires(x > 0);
Contract.Requires(y > 0);

Contract.Ensures(this.X == x);
Contract.Ensures(this.Y == y);
Contract.Ensures(this.Values.Length == this.X * this.Y);

this.x = x;
this.y = y;
this.values = new double[x * y];
}

[Pure]
public double GetValue(int xIndex, int yIndex)
{
Contract.Requires(xIndex >= 0);
Contract.Requires(yIndex >= 0);
Contract.Requires(xIndex < this.X);
Contract.Requires(yIndex < this.Y);

// Array access might be above the upper bound.
// Are you making some assumption on this.Y that the static checker is unaware of?
return this.values[xIndex * this.Y + yIndex];
}

[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(this.X > 0);
Contract.Invariant(this.Y > 0);
Contract.Invariant(this.values.Length == this.X * this.Y);
}
}


Thank you

Answer

After some trial and error, I found the solution.
It seems, that Code Contracts validation process is not able to verify, that the formula

xIndex * this.Y + yIndex < this.values.Length

is always true with the given preconditions and invariants.

Solution:
By adding a Contract.Assume, the validation process stops exclaiming.

public double GetValue(int xIndex, int yIndex)
{
    Contract.Requires(xIndex >= 0);
    Contract.Requires(yIndex >= 0);
    Contract.Requires(xIndex < this.X);
    Contract.Requires(yIndex < this.Y);

    // Help for Code Contract
    Contract.Assume(xIndex * this.Y + yIndex < this.values.Length);
    return this.values[xIndex * this.Y + yIndex];
}

Conclusion:
While Code Contracts is good for simple verifications (boundary, etc.), it needs help from the developer when verifying more complex formulas.