How to use cccheck to prove no case is forgotten

  • Article

Today we use the CodeContracts static checker to prove that no case is missing in a switch statement. This post is inspired by some feedback we had from CodeContracts users in product groups.

The problem. Suppose that we want to write a program to cook pasta. Cooking pasta is a simple. First we let the water boil, we add the pasta, we stir, and eventually we strain. We define an enum CookPasta to remember in which state we are and a Next method to tell us what’s coming next. The code is straightforward:

enum CookPasta { BoilWater, AddPasta, Stir, Strain, Done } public CookPasta Next(CookPasta state){

  switch(state)  {    case CookPasta.BoilWater:      return CookPasta.AddPasta;     case CookPasta.AddPasta:      return CookPasta.Stir;    case CookPasta.Stir:      return CookPasta.Strain;

    case CookPasta.Strain:      return CookPasta.Done;

    case CookPasta.Done:      return CookPasta.Done;    default:      throw new Exception("Unknown pasta state!");   } }

We added a throw statement to make the C# compiler happy - it would refuse to compile our code otherwise. However, we soon realize that our algorithm to cook pasta is wrong. We forgot a fundamental step: We need to add salt to the boiling water! Therefore we add a case to the enum case:

enum CookPasta { BoilWater, AddPasta, AddSalt, Stir, Strain, Done } 

But now suppose that we forgot to update the Next method (in real code there can be tenths of places to be updated). What is going to happen? An exception ("Unknown pasta state") will be thrown at runtime. But we love compile time analysis, so is there a way to have the static checker warn us that we forgot one case?

The solution. It is straightforward: All we need is to add an Assert(false) in the default branch:

default:
  Contract.Assert(false); // The static checker should prove it unreachable
  throw new Exception("Unknown pasta state!");

We are essentially asking the static checker to prove false, which is of course impossible. In fact, we get:

 warning : CodeContracts: This assert, always leading to an error, may be reachable. Are you missing an enum case?

If we fix the code, adding the missing cases

case CookPasta.BoilWater:
  return CookPasta.AddSalt;

case CookPasta.AddSalt:
  return CookPasta.AddPasta;

then cccheck will not emit any warning. Why? Did it just proved the impossible (false)? Actually no, it proved that there is no execution reaching the Contract.Assert(false), as we covered all the cases for CookPasta.

The improved solution. Nevertheless, there is something a little bit ugly about the above solution, as some friend in Microsoft product groups noticed. We should write two lines of code, an assert for the static (and dynamic) checker, and a throw instruction for the C# compiler. Is there a better way of doing it? The trick is to defined an helper class CodeContractsHelpers with an helper function ThrowIfReached.

In the switch statement we write something like

default:
  throw CodeContractsHelpers.ThrowIfReached("Unknown pasta state!");

Now it is a matter of defining ThrowIfReached. This is pretty easy:

  public static class CodeContractsHelpers
  {
    [ContractVerification(false)]
    public static Exception ThrowIfReached(string s)
    {
      Contract.Requires(false);

      return new Exception(s);
    }
  }

The helper method returns a new exception object. It has a precondition "false", i.e., it requires to never be called. When analyzing the Next method the static checker will turn the Contract.Requires(false) into a Contract.Assert(false), so that we have the same behavior as above - The static checker will complain if we miss one (or more) case. Finally we use the [ContractVerification(false)] to turn the verification of this helper off.

Is it sound? Are we 100% guaranteed that our switch case is comprehensive, and as a consequence no execution will ever reach the default branch? In the usual case yes. If the programmer only uses the defined enums, then everything is fine. However, C# allows to forge new enum values like this

    public const CookPasta AddOil = (CookPasta)(-1);

and invoke Next like this (with no type-checking error from C#):

var next = Next(AddOil);

Luckily the static checker will realize there may be a problem, and it will warn about it:

warning : CodeContracts: The actual value is not one of those defined for this enum. Forgotten [Flag] in the enum definition?