Add several new-style command-line options #3568

atomb · 2023-02-17T22:19:49Z

--error-limit is available everywhere
--solver-log is available for verify and measure-complexity
--solver-plugin is available for verify and measure-complexity
--resource-limit is available for verify and measure-complexity
--isolate-assertions and --format are also available for verify with --format renamed --log-format

Addresses #3468

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

* `--error-limit` is available everywhere * `--solver-log` is available for `verify` and `measure-complexity` * `--solver-plugin` is available for `verify` and `measure-complexity` * `--resource-limit` is available for `verify` and `measure-complexity` * `--isolate-assertions` and `--format` are also available for `verify` with `--format` renamed `--log-format`

keyboardDrummer · 2023-02-20T12:02:12Z

Source/DafnyCore/Options/CommonOptionBag.cs


 namespace Microsoft.Dafny;

 public class CommonOptionBag {

+  public static readonly Option<int> ErrorLimit =
+    new("--error-limit", () => 5, "Set the maximum number of errors to report (0 for unlimited).");


Shouldn't this be called verification-error-limit, since it limits only verification errors?

Also, the use-case of the option is unclear to me. If it's only used for testing then it would be better if it's a hidden option. What's the reason that the default is not unlimited? Is that to improve performance? If yes, then it would be good to explain that in the description of this option.

Right now, if I read the description of this option then I'm confused as to why the reported errors are limited to begin with.

I also think the default should be unlimited, and that perhaps the option isn't needed at all. My goal for now, though, was to replicate existing functionality in the new CLI, rather than change it. Since the default is to limit the number of errors presented, having an option to raise or eliminate that limit seems important.

Calling it --verification-error-limit makes sense. I think I'm going to have another PR to add some more options and could change it then.

It can be quite important. If you encode a method as one big VC, then it reports one assertion failure. To get more assertion failures you adjust the VC to prevent the failure you have already seen and rerun. You can continue this until no more failures are found. That iteration takes time and a user might well want to stop after some small number. The problem is that the order in which results are found is non-deterministic. There are arguments for a default either way -- when I was working with production code, I would set it to a small number for a faster debug cycle. No limit only works for users if the results are presented as they are found. I vote to keep it. Like Aaron, I did not know it was only for verification errors.

If you encode a method as one big VC, then it reports one assertion failure. To get more assertion failures you adjust the VC to prevent the failure you have already seen and rerun.

To be clear, I think this is what Boogie does automatically.

That iteration takes time and a user might well want to stop after some small number.

So it's indeed a performance related option.

The problem is that the order in which results are found is non-deterministic.

Why is that a problem?

I vote to keep it. Like Aaron, I did not know it was only for verification errors.

If we keep it then we should explain why we have it.

The non-determinism causes this problem. Suppose you run with an error-limit of 1, find a problem and "fix" it. Then run again. You get a different problem. Did you fix the first one or did you randomly get a different problem?

Non-determinism is also a problem for tests.(And is why I write tests with just one problem, though that does not capture the full range of uses)

And yes, I would count it as a (user) performance optimization.

The user manual says this: limits the number of verification errors reported per procedure. Default is 5; 0 means as many as possible; a small positive number runs faster but a large positive number reports more errors per run

To me that concisely captures the value and tradeoff of the option

keyboardDrummer · 2023-02-20T12:02:15Z

Source/DafnyCore/Options/ICommandSpec.cs

    BoogieOptionBag.Cores,
    CommonOptionBag.Libraries,
    CommonOptionBag.Plugin,
    CommonOptionBag.Prelude,
    Function.FunctionSyntaxOption,
    CommonOptionBag.QuantifierSyntax,
    CommonOptionBag.UnicodeCharacters,
+    CommonOptionBag.ErrorLimit,


Shouldn't this be in VerificationOptions, since it limits only verification errors?

Yes, you're right. I was mistakenly thinking it affected other sorts of errors, too.

keyboardDrummer · 2023-02-20T12:02:39Z

Source/DafnyCore/Options/CommonOptionBag.cs

+  };
+
+  public static readonly Option<uint> SolverResourceLimit = new("--resource-limit", @"Specify the maximum resource limit (rlimit) value to pass to Z3. Multiplied by 1000 before sending to Z3.");
+  public static readonly Option<string> SolverPlugin = new("--solver-plugin", @"Specify a plugin to use to solve verification conditions (instead of an external Z3 process).");


I would use the name --boogie-plugin instead of --solver-plugin because as far as I understand, the reason we have this option is that is supports the exact same plugin format as Boogie does, so users can re-use their Boogie plugins with Dafny. If you don't care about re-using a Boogie plugin and you want to write a Dafny specific solver plugin, I would recommend using --plugin instead since it provides the full Dafny plugin interface.

The only kind of plugin Boogie supports is a solver plugin, and I'd prefer that Dafny users not need to know about the existence of Boogie. So I'd prefer to leave it with the current naming.

I'd prefer that Dafny users not need to know about the existence of Boogie.

I think --solver-plugin as you've implemented it requires passing a .dll with a Boogie specific layout, otherwise it doesn't work. It relies on this code which requires the dll to have a factory class with Microsoft.Boogie.<AssemblyName>.Factory as a fully qualified name. For example, Microsoft.Boogie.SMTLib.Factory is the class in SMTLib that satisfies the naming format.

If a user doesn't know about Boogie then they have to use --plugin to add C# solver code. Inside their plugin they can set DafnyOptions.O.TheProverFactory = .

So, I suggest we either not add --solver-plugin altogether, since users can use --plugin for the same purpose, or we call it --boogie-plugin to indicate they can reuse the same plugins as in Boogie.

Has anyone ever used a solver plugin? And are there any instructions on how to do it? Although there is a SMT-lib standard, solvers differ quite a bit in ways that end up mattering that this would be a very non-trivial exercise.

I'm inclined on this one to not expose it in the new CLI and see if anyone complains.

keyboardDrummer · 2023-02-20T12:05:39Z

Source/DafnyCore/Options/CommonOptionBag.cs

+
+  public static readonly Option<uint> SolverResourceLimit = new("--resource-limit", @"Specify the maximum resource limit (rlimit) value to pass to Z3. Multiplied by 1000 before sending to Z3.");
+  public static readonly Option<string> SolverPlugin = new("--solver-plugin", @"Specify a plugin to use to solve verification conditions (instead of an external Z3 process).");
+  public static readonly Option<string> SolverLog = new("--solver-log", @"Specify a file to use to log the SMT-Lib text sent to the solver.");


Based on this comment: #3537 (comment)

"The option that actually came up in our use case was /normalizeOptions:0, which makes the generated SMT files much easier to debug. Hopefully in the new CLI there remains a way to do this."

It seems like just exposing the raw SMT doesn't help users much. I suggest adding normalizeOptions as well and making both that and this hidden options, since they seem geared towards people who are developing Dafny or extensions to Dafny, not people who are only consuming Dafny.

Many Dafny users I've talked to want to be able to look at the generated SMT (or store it to send to a different solver). I wouldn't entirely be opposed to making it hidden, but I'd want to make sure that the standard help has some sort of message in the spirit of "there are other, more advanced options, too. Used --help-hidden to see them". It's used often enough that I'd be reluctant to make it hard to find.

I understand that some options are used only for development debugging of solver performance. But in general having hidden options smacks of being patriarchal "we know best what you need" to the users. Many tools have lots of options -- for myself (as a user) it is helpful to browse the list to see what is possible, but not dig into them unless I need them. I would bias towards not hiding options unless they real are deeply technical.

But in general having hidden options smacks of being patriarchal "we know best what you need" to the users.

I don't feel that way. There are many options that are only relevant to Dafny language developers, take printing out the resolved Dafny program for example. As a user, for each option in the help that I read that isn't useful to me, I will be less excited to keep reading the help, and there's a higher chance I will miss options that are relevant.

I'd want to make sure that the standard help has some sort of message in the spirit of "there are other, more advanced options, too. Used --help-hidden to see them". It's used often enough that I'd be reluctant to make it hard to find.

That sounds good, although I wouldn't say 'more advanced options' but 'options meant for debugging the Dafny language toolchain'

(or store it to send to a different solver)

Could this be part of a Dafny toolchain developer use-case?

keyboardDrummer · 2023-02-20T12:06:30Z

Source/DafnyCore/Options/CommonOptionBag.cs

+    ArgumentHelpName = "configuration"
+  };
+
+  public static readonly Option<uint> SolverResourceLimit = new("--resource-limit", @"Specify the maximum resource limit (rlimit) value to pass to Z3. Multiplied by 1000 before sending to Z3.");


How is a user supposed to use this option? There's no guidance for how to pick a value.

I'll add more thorough help text in a later PR.

atomb requested review from davidcok and robin-aws February 17, 2023 22:19

davidcok previously approved these changes Feb 17, 2023

View reviewed changes

davidcok and others added 3 commits February 17, 2023 18:52

Merge branch 'master' into more-new-cli-options

888d60d

Make --stdin available more broadly

1283f95

Fix --error-limit to match previous behavior

409c6f8

atomb dismissed davidcok’s stale review via 409c6f8 February 18, 2023 00:07

davidcok previously approved these changes Feb 18, 2023

View reviewed changes

Merge branch 'master' into more-new-cli-options

417f5ea

atomb enabled auto-merge (squash) February 18, 2023 00:27

Fix test output

05d3bf3

atomb dismissed davidcok’s stale review via 05d3bf3 February 18, 2023 00:53

davidcok approved these changes Feb 18, 2023

View reviewed changes

atomb merged commit ef4f346 into dafny-lang:master Feb 18, 2023

keyboardDrummer reviewed Feb 20, 2023

View reviewed changes

atomb deleted the more-new-cli-options branch January 4, 2024 17:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add several new-style command-line options #3568

Add several new-style command-line options #3568

atomb commented Feb 17, 2023

keyboardDrummer Feb 20, 2023 •

edited

Loading

atomb Feb 20, 2023

davidcok Feb 20, 2023

keyboardDrummer Feb 20, 2023

davidcok Feb 20, 2023

keyboardDrummer Feb 20, 2023

atomb Feb 20, 2023

keyboardDrummer Feb 20, 2023

atomb Feb 20, 2023

keyboardDrummer Feb 20, 2023 •

edited

Loading

davidcok Feb 20, 2023

davidcok Feb 20, 2023

keyboardDrummer Feb 20, 2023

atomb Feb 20, 2023

davidcok Feb 20, 2023

keyboardDrummer Feb 20, 2023 •

edited

Loading

keyboardDrummer Feb 20, 2023

atomb Feb 20, 2023

Add several new-style command-line options #3568

Add several new-style command-line options #3568

Conversation

atomb commented Feb 17, 2023

keyboardDrummer Feb 20, 2023 • edited Loading

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

keyboardDrummer Feb 20, 2023 • edited Loading

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

keyboardDrummer Feb 20, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Feb 20, 2023 •

edited

Loading

keyboardDrummer Feb 20, 2023 •

edited

Loading

keyboardDrummer Feb 20, 2023 •

edited

Loading