Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add --test-assumptions option #3185

Merged
merged 5 commits into from
Dec 16, 2022
Merged

Add --test-assumptions option #3185

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
1b1d2c4
Add --test-assumptions option
keyboardDrummer Dec 14, 2022
dfe563e
Fix description
keyboardDrummer Dec 14, 2022
6dddcc9
Update option arguments
keyboardDrummer Dec 16, 2022
0322ef9
Fix
keyboardDrummer Dec 16, 2022
db91085
Merge branch 'master' into test-assumptions
keyboardDrummer Dec 16, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions Source/DafnyCore/Options/CommonOptionBag.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
using System.Collections.Generic;
using System.CommandLine;
using System.Diagnostics.Tracing;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the code using this?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nope ^,^ would prefer not to have another review/build cycle again for this though. Maybe we can find a better way of catching this in the future, maybe through dotnet-format.

using System.Linq;

namespace Microsoft.Dafny;
Expand Down Expand Up @@ -124,13 +125,26 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
public static readonly Option<bool> IncludeRuntime = new("--include-runtime",
"Include the Dafny runtime as source in the target language.");

public enum TestAssumptionsMode {
None,
Externs
}

public static readonly Option<TestAssumptionsMode> TestAssumptions = new("--test-assumptions", () => TestAssumptionsMode.None, @"
(experimental) When turned on, inserts runtime tests at locations where (implicit) assumptions occur, such as when calling or being called by external code and when using assume statements.

Functionality is still being expanded. Currently only checks contracts on every call to a function or method marked with the {:extern} attribute.".TrimStart());

static CommonOptionBag() {
DafnyOptions.RegisterLegacyBinding(SolverPath, (options, value) => {
if (!string.IsNullOrEmpty(value)) {
options.ProverOptions.Add($"PROVER_PATH={value}");
}
});

DafnyOptions.RegisterLegacyBinding(TestAssumptions, (options, value) => {
options.TestContracts = value == TestAssumptionsMode.Externs ? DafnyOptions.ContractTestingMode.Externs : DafnyOptions.ContractTestingMode.None;
});
DafnyOptions.RegisterLegacyBinding(ManualLemmaInduction, (options, value) => {
if (value) {
options.Induction = 1;
Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/Options/ICommandSpec.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ static ICommandSpec() {
BoogieOptionBag.NoVerify,
CommonOptionBag.EnforceDeterminism,
CommonOptionBag.OptimizeErasableDatatypeWrapper,
CommonOptionBag.TestAssumptions
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm still slightly new the the modern options architecture we have here: will this option be available for dafny translate, too? I suspect it'll be used most often there, though also during dafny run and dafny test.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Execution options are available for run,build,translate and test

}.Concat(VerificationOptions).ToList();

public static IReadOnlyList<Option> ConsoleOutputOptions = new List<Option>(new Option[] {
Expand Down
2 changes: 1 addition & 1 deletion Test/contract-wrappers/AllExterns.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: ! %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:Externs %s %s.externs.cs > %t
// RUN: ! %baredafny test %args --no-verify --test-assumptions=externs %s %s.externs.cs > %t
// RUN: %diff "%s.expect" "%t"
// RUN: %OutputCheck --file-to-check "%S/AllExterns.cs" "%s"
// CHECK: .*Foo____dafny__checked\(x\).*
Expand Down