Inter-procedural inference of conditions to error in cccheck

Today we pushed out a new release of CodeContracts. Among the many improvements, bug fixes, etc. we improved the inference of pre-conditions to errors. The static checker now also provides inter-procedural error traces.

But how it works?

Let me illustrate the inference of preconditions with this example

private int Max(int[] a)
{
  var max = a[0];
  for (var i = 1; i < a.Length; i++)
  {
    var tmp = a[i];
    if (tmp > max) max = tmp;
   }
  return max;
  }
}

private void CreateTheArrayAndDoSomething(int size)
{
  var array = new int[size]; 
  // ... fill the array ...

  var arrayMax = Max(array);

  // ... do something else ...
}

public void PublicAPI(int size)
{
  Contract.Requires(size != Int32.MinValue);

  if (size < 0) size = -size;

  CreateTheArrayAndDoSomething(size);
}

The static checker first analyzes the method Max. It determines that if the input array is null or it is empty, then an error will definitely happen. If we enable the suggestion of requires, it will report (remember to enable "Suggest Requires" to see those messages)

... : CodeContracts: Suggested requires: Contract.Requires(a != null);

... : CodeContracts: Suggested requires: Contract.Requires(0 < a.Length);

Those preconditions are necessary for Max to be correct: If they are violated Max will cause a runtime exception to occur. The static checker is also smart enough to determine that those preconditions are sufficient for Max to be correct: If satisfied, then the Max will never throw a runtime exception. As a consequence the static checker will not report any warning for Max, but it pushes the condition to the caller.

The caller passes a freshly allocated array of length size to Max. As a consequence, the first condition (a != null) is satisfied, but not the second one, which is further propagated to the caller:

... : CodeContracts: Suggested requires: Contract.Requires(0 < size);

The caller, PublicAPI, is careful enough to check whether the input values is negative in which case it negates it. Furthermore, it requires the input to be different from the MinValue which will cause an overflow on negation. Nevertheless, it forgot the case when size == 0, which will cause an error downstream. The static analyzer cannot push the condition further up in the call chain, as it reached the public surface. As a consequence it emits a warning as well as the inter-procedural trace that will cause the error

... : CodeContracts: Missing precondition in an externally visible method. Consider adding Contract.Requires(0 != size); for parameter validation. Otherwise the following sequence of method calls may cause an error. Sequence: PublicAPI -> CreateTheArrayAndDoSomething -> Max

The precondition inferred by cccheck is by design a condition to the error: if some caller fails to satisfy it, then a runtime error will occur. This makes the cccheck analyzer different from other tools, as all the inferred preconditions are sound.

Comments

• Anonymous
  November 09, 2014
  Nice work!