Add plugin to create wrapper functions/methods to check contracts at runtime #2712

atomb · 2022-09-08T16:09:08Z

This PR adds a flag to allow certain function and method contracts to be tested at runtime. For the moment, it focuses on {:extern} code, but could be applied to other code in the future. Some details of the design are described in the comment thread of issue #2235.

It is usable with the following:

/testContracts:<AllExterns|ExternsInTests>
    Enable run-time testing of compiled function or method contracts in
    certain situations, currently focused on :extern code.

    AllExterns - Check contracts on every call to a function or
        method marked :extern, regardless of where it occurs.
    Externs - Check contracts on every call to a function or method
        marked :extern when it occurs in one marked :test.

I'm not entirely happy that it required removing a few readonly qualifiers from AST fields, but that seems unavoidable without major rewriter infrastructure refactoring.

Fixes #2235.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

This works on one example, but is know to fail for polymorphic code and probably many other types, as well.

* Generate fewer resolved AST nodes before resolution happens * Don't run the redirection code while it's not working

Still doesn't work, though

Now it runs during `PostResolveIntermediate` so that it has easier access to attributes.

atomb · 2022-09-09T15:55:15Z

The following Dafny and C# files, together, demonstrate the basic operation of this for checking calls to externs from tests.

The Dafny code (check-extern.dfy):

method {:extern} Foo(x: int) returns (y: int)
  requires 1 < x < 10;
  ensures y >= 10;

method FooCaller(x: int) returns (y: int)
  requires 1 < x < 10;
  ensures y >= 10;
{
  y := Foo(x);
}

method {:test} FooTest()
{
  var y := Foo(3);
  expect y == 30;
}

function method {:extern} Bar(x: int): (y: int)
  requires 1 < x < 10;
  ensures y >= 10;

function method BarCaller(x: int): (y: int)
  requires 1 < x < 10;
  ensures y >= 10;
{
  Bar(x)
}

method {:test} BarTest()
{
  var y := Bar(3);
  expect y == 30;
}

And the C# code (FooBar.cs):

using System.Numerics;

namespace _module {

  public partial class __default {
    public static BigInteger Foo(BigInteger x)
    {
      return BigInteger.Zero;
    }
    public static BigInteger Bar(BigInteger x)
    {
      return BigInteger.Zero;
    }
  }
}

These can be run together with the following command:

dafny /compile:3 /runAllTests:1 /testContracts:Tests /useBaseNameForFileName check-extern.dfy FooBar.cs

This yields the following:

Dafny program verifier finished with 5 verified, 0 errors
Wrote textual form of target program to check-extern.cs
Running...

FooTest: FAILED
	check-extern.dfy(3,12): Runtime failure of ensures clause from check-extern.dfy:3:13
BarTest: FAILED
	check-extern.dfy(20,12): Runtime failure of ensures clause from check-extern.dfy:20:13
Test failures occurred: see above.

atomb · 2022-09-22T19:02:56Z

I think this PR is largely complete. The one key open question in my mind is whether the current set of /testContracts parameters is the right one. It could be that ExternsInTests is too specific to be very useful. (Compiling only your test code with /AllExterns could be the more common use case.) And it could be than an All option, to always test all (compilable) contracts would be valuable. I'm pretty convinced that /AllExterns is a useful mode, however, and perhaps the only one we need to support in this PR.

MikaelMayer · 2022-09-23T18:31:47Z

I'm ready to review it ! Let me have a look.

MikaelMayer

Great job ! This will be very valuable. Would it be possible that /runAllTests automatically triggers ExternsInTest to be set by default? This would not completely be a breaking change, as you'd only issue warnings.

Also I suggested a few doc upgrades

MikaelMayer · 2022-09-23T18:32:31Z

Source/DafnyCore/Cloner.cs

@@ -673,6 +673,8 @@ public class Cloner {
        var body = s.Body == null ? null : CloneBlockStmt(s.Body);
        r = new ModifyStmt(Tok(s.Tok), Tok(s.EndTok), mod.Expressions, mod.Attributes, body);

+      } else if (stmt is CallStmt s) {
+        r = new CallStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhs, s.MethodSelect, s.Args);


Looks like a good catch ^^

MikaelMayer · 2022-09-23T18:34:09Z

Source/DafnyCore/DafnyOptions.cs

@@ -1425,6 +1444,16 @@ verification outcome.
    option is useful in a diamond dependency situation, to prevent code
    from the bottom dependency from being generated more than once.

+/testContracts:<AllExterns|ExternsInTests>
+    Enable run-time testing of compiled function or method contracts in
+    certain situations, currently focused on :extern code.


Suggested change

certain situations, currently focused on :extern code.

certain situations, currently focused on {:extern} code.

MikaelMayer · 2022-09-23T18:35:03Z

Source/DafnyCore/DafnyOptions.cs

+    certain situations, currently focused on :extern code.
+
+    AllExterns - Check contracts on every call to a function or
+        method marked :extern, regardless of where it occurs.


Suggested change

method marked :extern, regardless of where it occurs.

method with the {:extern} attribute, regardless of where it occurs.

MikaelMayer · 2022-09-23T19:10:50Z

Source/DafnyCore/DafnyOptions.cs

+        method marked :extern when it occurs in one marked :test, and
+        warn if no corresponding :test exists for a given :extern.


Suggested change

method marked :extern when it occurs in one marked :test, and

warn if no corresponding :test exists for a given :extern.

method with the {:extern} attribute when it occurs in a method with the {:test} attribute, and

warn if no corresponding method with a {:test} attribute exists for a given method with the {:extern} attribute.

MikaelMayer · 2022-09-23T19:15:46Z

Source/DafnyCore/DafnyOptions.cs

@@ -1425,6 +1444,16 @@ verification outcome.
    option is useful in a diamond dependency situation, to prevent code
    from the bottom dependency from being generated more than once.

+/testContracts:<AllExterns|ExternsInTests>


Now that I've read the doc, let me rephrase what these options do:

AllExterns will run the contract specifications on every extern method

ExternsInTests will run the contract specifications on every extern method, except those that are not part of any {:test} and thus will only issue a warning about the lack of test.

I see the two options to be useful, but 1 seems even more valuable, so let me suggest a different name

AllExterns => externs
ExternsInTests => testedExterns

What do you think of that?

Yeah, I like that naming. I'll switch to it.

MikaelMayer · 2022-09-23T19:16:27Z

Source/DafnyCore/Resolver.cs

@@ -546,6 +550,11 @@ enum ValuetypeVariety {
            // Now we're ready to resolve the cloned module definition, using the compile signature

            ResolveModuleDefinition(nw, compileSig);
+
+            foreach (var rewriter in rewriters) {
+              rewriter.PostCompileCloneAndResolve(nw);


A new phase in the rewriter ! Fascinating.

It took an in-depth debugging session with @RustanLeino to understand that that was necessary! It's likely to be useful for other rewriter plugins that operate (even partly) post-resolution and need to make sure their effects persist in the compiled code.

MikaelMayer · 2022-09-23T19:17:57Z

Source/DafnyCore/Resolver/ExpectContracts.cs

+    return new BlockStmt(callStmt.Tok, callStmt.EndTok, bodyStatements.ToList());
+  }
+
+  private static Expression MakeApplySuffix(IToken tok, string name, List<Expression> args) {


Could you please move this generic expression builder to Expressions.cs or somewhere similar?

MikaelMayer · 2022-09-23T21:25:53Z

Source/DafnyCore/Resolver/ExpectContracts.cs

+    var expectEnsuresStmts = ensures.Select(ens =>
+      CreateContractExpectStatement(ens, "ensures"));
+    var callStmtList = new List<Statement>() { callStmt };
+    var bodyStatements = expectRequiresStmts.Concat(callStmtList).Concat(expectEnsuresStmts);


That's interesting. So your approach is to rewrite any extern method call to inline the requires call and the expects clause.
Do you need to check the requires? Isn't that going to be checked by Dafny statically?
For the ensures, it's great, because it means one can write a test fuzzer without any expect, and the method's postcondition will still be checked. Could you please add this idea in documentation of /testContracts?

For externs (of the form that this is focused on, where the implementation is written in the target language), that's true. Dafny will prove that the requires clause is satisfied. However, if you were to apply a fuzzer to the target language code, the existence of a branch on a requires clause is likely to make it easier to come up with inputs that satisfy that requires clause. Arguably, perhaps, it might make sense to check all of the requires clauses together in one expect statement, but check the ensures clauses separately, as the current code does.

I think any changes like that would be driven by how well it works in practice, though.

I'll add some reference manual documentation of /testContracts that goes into this.

However, if you were to apply a fuzzer to the target language code, the existence of a branch on a requires clause is likely to make it easier to come up with inputs that satisfy that requires clause.

If you were to apply a fuzzer to the target language code, should you not gracefully exit if the requires is not satisfied?

Ideally, yes, though I think that the current structure would at least give you enough to get started. If you run a fuzzer, and filter out the cases of failing requires clauses, you'll get a useful outcome.

In the long run, I'd like this code to integrate with target language fuzzing/verification APIs, using assume-like things for requires clauses and assert-like things for ensures clauses. I think that's a bit down the road, though.

MikaelMayer · 2022-09-23T21:27:08Z

Source/DafnyCore/Resolver/ExpectContracts.cs

+      if (origFunc.Result?.Name is null) {
+        body.AppendStmt(new ReturnStmt(tok, tok, new List<AssignmentRhs> { new ExprRhs(localExpr) }));
+      }
+      newFunc.ByMethodBody = body;


Clever ! You transform the ByMethod body of an extern function with these expect statements. Love it.

MikaelMayer · 2022-09-23T21:27:32Z

Source/DafnyCore/Resolver/ExpectContracts.cs

+    }
+  }
+
+  private class CallRedirector : TopDownVisitor<MemberDecl> {


Can you please add a comment about this class?

MikaelMayer · 2022-09-26T20:13:39Z

Source/DafnyCore/DafnyOptions.cs

@@ -99,7 +99,7 @@ public enum PrintModes {
    public enum ContractTestingMode {
      None,
      AllExterns,


Could you please rename this so that it matches the option?

MikaelMayer · 2022-09-26T20:19:14Z

Source/DafnyCore/DafnyOptions.cs

@@ -1444,15 +1444,16 @@ verification outcome.
    option is useful in a diamond dependency situation, to prevent code
    from the bottom dependency from being generated more than once.

-/testContracts:<AllExterns|ExternsInTests>
+/testContracts:<Externs|TestedExterns>
    Enable run-time testing of compiled function or method contracts in


I just realize one important thing. You are not testing "compiled functions", you are testing "compilable (function or method) contracts". Could you please rephrase it like the compilable contracts of methods or functions that have the {:extern} attribute, at the call site? I think it's important to mention the call site.

Ah, yeah, my original intent of the word "compiled" was just to say that this only applied to functions and methods that are being compiled. I think your use of the word is better, though! So I'll change the text accordingly.

MikaelMayer

Great job ! A good step forward to make it possible to rely more on contracts.
Down the road, how hard do you think it would be to integrate testing as part of the IDE extension?

atomb · 2022-09-27T15:19:05Z

Great job ! A good step forward to make it possible to rely more on contracts. Down the road, how hard do you think it would be to integrate testing as part of the IDE extension?

I suspect it'd be fairly easy, though I don't know the details of how testing works through LSP. I think that'd be a very nice thing to dig into soon.

davidcok · 2022-09-30T11:37:09Z

docs/DafnyRef/UserGuide.md

@@ -1668,3 +1668,27 @@ periods.
  compiled assembly rather than including `DafnyRuntime.cs` in the build
  process.

+
+* `-testContracts:<mode>` - test certain function and method contracts


"test certain ... contracts" -- which ones? all non-ghost ones? all non-ghost ones that are executable?

Ah, I updated the help text with what I think is better wording and forgot to update the RM! What do you think of the wording in DafnyOptions.cs?

atomb added 13 commits August 12, 2022 17:08

Basic contract-checking wrapper generator

5f4fd13

This works on one example, but is know to fail for polymorphic code and probably many other types, as well.

Start implementing redirection to wrappers

e9f9f39

Various cleanups

86b5e0a

More cleanup

5036db9

* Generate fewer resolved AST nodes before resolution happens * Don't run the redirection code while it's not working

Further redirection progress

5e6d886

Still doesn't work, though

Tiny tweak

2c0df47

Functional but messy call redirection

e151a6b

Clean up wrapper call redirection

c10d268

Add /testContracts command-line option

7ce5197

Merge branch 'master' into contract-wrappers

60929b7

Move wrapper generation to a later phase

1dbf4e9

Now it runs during `PostResolveIntermediate` so that it has easier access to attributes.

Update Options.txt

dc81692

Test on real-world example

2c9a9a2

atomb added 10 commits September 16, 2022 14:01

Merge remote-tracking branch 'upstream/master' into contract-wrappers

2e4b424

Improve warnings about testing ghost expressions

759c745

Update options and logic for which calls to wrap

aa0d31a

Minor code cleanups

a478ece

Update Options.txt

90660fc

Add tests for contract-checking wrappers

e141a12

Add previously-omitted C# files for contract-wrappers tests

4e2e6bd

Add successful runtime contract checking test

10f2274

Rearrange files to get tests to pass

d58329b

Merge remote-tracking branch 'upstream/master' into contract-wrappers

efdbfc6

atomb self-assigned this Sep 20, 2022

atomb added 2 commits September 21, 2022 09:17

Warn if :extern not tested with ExternsInTests

853a778

Merge remote-tracking branch 'upstream/master' into contract-wrappers

52d7f34

atomb added 2 commits September 22, 2022 12:03

Small cleanups

18ff188

Merge remote-tracking branch 'upstream/master' into contract-wrappers

17b8f3a

atomb added 3 commits September 22, 2022 14:18

Merge remote-tracking branch 'upstream/master' into contract-wrappers

39212b2

Update tests to match wrapper name change

3635bbc

Add a release notes entry

8247175

atomb requested review from MikaelMayer, robin-aws and cpitclaudel September 22, 2022 21:22

atomb marked this pull request as ready for review September 23, 2022 15:14

MikaelMayer requested changes Sep 23, 2022

View reviewed changes

atomb added 4 commits September 26, 2022 09:09

Change /testContracts arguments, update docs

f7d9a1d

Add class-level documentation comments

84947a1

Add RM entry for /testContracts

8f7496a

Move MakeApplySuffix to Expressions.cs

ca6eb3b

atomb requested a review from MikaelMayer September 26, 2022 17:18

MikaelMayer reviewed Sep 26, 2022

View reviewed changes

atomb added 2 commits September 26, 2022 15:11

Rename the internal constructor for the Externs mode

252dc6e

Finesse the help text for /testContracts

49f68ba

atomb requested a review from MikaelMayer September 26, 2022 22:14

atomb added 2 commits September 26, 2022 15:28

Update Options.txt

d69a1b3

Merge remote-tracking branch 'upstream/master' into contract-wrappers

eedefdd

MikaelMayer approved these changes Sep 27, 2022

View reviewed changes

atomb merged commit b2f3249 into dafny-lang:master Sep 27, 2022

davidcok reviewed Sep 30, 2022

View reviewed changes

atomb mentioned this pull request Dec 2, 2022

Extend /testContracts to be able to test contracts on any function/method #3151

Open

atomb deleted the contract-wrappers branch January 4, 2024 17:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add plugin to create wrapper functions/methods to check contracts at runtime #2712

Add plugin to create wrapper functions/methods to check contracts at runtime #2712

atomb commented Sep 8, 2022 •

edited

Loading

atomb commented Sep 9, 2022

atomb commented Sep 22, 2022 •

edited

Loading

MikaelMayer commented Sep 23, 2022

MikaelMayer left a comment

MikaelMayer Sep 23, 2022

MikaelMayer Sep 23, 2022

MikaelMayer Sep 23, 2022

MikaelMayer Sep 23, 2022

MikaelMayer Sep 23, 2022

atomb Sep 26, 2022

MikaelMayer Sep 23, 2022

atomb Sep 26, 2022

MikaelMayer Sep 23, 2022

MikaelMayer Sep 23, 2022

atomb Sep 26, 2022

MikaelMayer Sep 26, 2022

atomb Sep 26, 2022

MikaelMayer Sep 23, 2022

MikaelMayer Sep 23, 2022

MikaelMayer Sep 26, 2022

MikaelMayer Sep 26, 2022 •

edited

Loading

atomb Sep 26, 2022

MikaelMayer left a comment

atomb commented Sep 27, 2022

davidcok Sep 30, 2022

atomb Sep 30, 2022

	certain situations, currently focused on :extern code.
	certain situations, currently focused on {:extern} code.

	method marked :extern, regardless of where it occurs.
	method with the {:extern} attribute, regardless of where it occurs.

		method marked :extern when it occurs in one marked :test, and
		warn if no corresponding :test exists for a given :extern.

Add plugin to create wrapper functions/methods to check contracts at runtime #2712

Add plugin to create wrapper functions/methods to check contracts at runtime #2712

Conversation

atomb commented Sep 8, 2022 • edited Loading

atomb commented Sep 9, 2022

atomb commented Sep 22, 2022 • edited Loading

MikaelMayer commented Sep 23, 2022

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer Sep 26, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

atomb commented Sep 27, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented Sep 8, 2022 •

edited

Loading

atomb commented Sep 22, 2022 •

edited

Loading

MikaelMayer Sep 26, 2022 •

edited

Loading