feat: Add resolver plugin that automatically creates test wrappers for contracts

[atomb]

The Dafny reference manual, in the documentation for the expect statement, suggests that it can be used as a way to dynamically check the contract of a method.

However, doing this manually in Dafny as-is introduces the possibility that the expect statement and the ensures clause could get out of sync. Instead, we could have a plugin that would automatically generate a wrapper to check the ensures clauses (and possibly even requires clauses) of a method using expect, guaranteeing that the dynamic checks would always match the stated contracts.

Further comments on this issue will elaborate a proposed design.

[atomb]

Here's a proposal for the next step we might take.

Expected Use

• Write contracts on functions and methods as usual
• Specify /testContracts:<modes> to enable testing contracts, where <modes> is a comma-separated list containing any of the following possible values:
  • tests - check contracts on functions and methods when calling them directly from {:test} methods
  • externs - check contracts on code marked with {:extern}, whether being used to import or export, regardless of where it’s being called from
• Run the compiler and get target-language code generated for wrappers that check contracts of specific functions or methods
  • Contract checks will be in wrapper definitions that call the original definitions, allowing tools that work with the target language to use either
  • Contract checks will have the behavior of a manually-written expect

Wrapper Details

It’s possible that the contract on a method could be difficult to prove due to SMT solver limitations, such as the following.

method HardCastMethod(i: nat) returns (res: nat)
  requires i < 64
  ensures res == (64 - i as bv64) as int
{
  return (64 - i as bv8) as int;
}

Or, alternatively, it could be difficult to prove because it’s written in a different language, such as the following.

method {:extern} GenerateBytes(i: int32) returns (res: seq<uint8>)
    requires i >= 0
    ensures |res| == i as int

In either case, we will use the same approach to test the contract contract before and after calling the underlying method, such as the following.

method HardCastMethod_checked(i: nat) returns (res: nat)
  requires i < 64
  ensures res == (64 - i as bv64) as int
{
  expect i < 64;
  res := HardCastMethod(i);
  expect res == (64 - i as bv64) as int;
}

method {:extern} GenerateBytes_checked(i: int32) returns (res: seq<uint8>)
    requires i >= 0
    ensures |res| == i as int
{
  expect i >= 0;
  res := GenerateBytes(i);
  expect |res| == i as int;
}

Functions would behave similarly, but with one additional factor. Consider this functional equivalent of the above method.

function HardCastFunction(i: nat): (res: nat)
  requires i < 64
  ensures res == (64 - i as bv64) as int
{
  (64 - i as bv8) as int
}

It could have a similar checked wrapper using by method.

function HardCastFunction_checked(i: nat): (res: nat)
  requires i < 64
  ensures res == (64 - i as bv64) as int
{
   HardCastFunction(i)
} by method {
  expect i < 64;
  res := HardCastFunction(i);
  expect res == (64 - i as bv64) as int;
}

Otherwise, functions would behave identically to methods. Supporting this approach suggests continuing to allow expect in function by method definitions (see #1376).

First Iteration Plan

Limitations

• Support ghost code only to the extent that it would currently compile if copied into an expect statement. Future improvements may include extending the range of specifications that can be compiled.
• Wrappers will initially check both preconditions and postconditions. Greater flexibility may be valuable in the future.

Implementation Plan

• Write as resolver plugin that uses the rewriting interface to generate new Dafny code to describe the wrappers
  • Generate only the wrappers that will be called, according to the options described above
  • The wrappers won’t be realized as concrete source code, but will be fed directly into the target language compilers
• Treat expect as the current {:test} code does

Side Benefits

Because contract-checking wrappers will exist as separate but directly-callable code in the target language, anyone who wants to use them from property-based tests, fuzzing harnesses, or bounded-model-checking harnesses can do so, and that allows us to experiment with the utility of those connections before automating them.

Later Stages

After this first iteration, there are a number of improvements that may be valuable. These could include:

• Support for compiling more ghost code
• Support for wrappers that check only preconditions or only postconditions
• A mechanism for specific call sites to request runtime contract checking
• Automated integration with target-language property-based testing libraries
• Automated integration with target-language fuzzers
• Automated integration with target-language verifiers that focus on proving the absence of assertion failures (such as CBMC, Crux, Gillian, JBMC, Kani, and others)

[robin-aws]

Loving this direction. My only ask is that you're very explicit in the documentation that /testContracts:<modes> is experimental and very likely to change. I'm very confident that checking specifications at runtime is valuable, but I'm much less confident the two modes you suggest specifically will be the most useful and/or scale to real code.

My only other ask is that you rename HardCastMeth to HardCastMethod, because the former keeps making me think of Breaking Bad. :D

[atomb]

Yep, that sounds great. I'm not fully confident that these are the right modes, either, but they at least give us something to start experimenting with.

And I edited it to fully spell out Method and Function everywhere. 🤣

[keyboardDrummer]

Could you say something about what error messages are generated if you use non-compilable expression in your ensures clauses combined with /testContracts ?

What's the use-case of /testContracts:tests? Would you always use this in combination with /noVerify, so you don't have to prove the ensures clauses of the ensures that you want to check at runtime?

[atomb]

I think a message something along the lines of /testContracts can only be used with compilable contracts, and the ensures clause of method m at foo.dfy(1,3) called from the test at bar.dfy(5,3) is not compilable is what I have in mind.

I have two use cases in mind for /testContracts:tests:

• For code imported with {:extern} that will never be verified but can be tested.
• For code that's hard to prove, in which case you'd probably mark an individual function or method (or several) with {:verify false}, though you could use /noVerify more broadly. It might also be valuable to allow {:verify false} on individual contract clauses, though I'd be inclined to hold off on that until we've identified specific cases where we know we need it.