Initial C# port of auditor #3175

atomb · 2022-12-09T22:45:45Z

This PR integrates the functionality of the auditor plugin as built-in functionality exposed through the dafny audit command.

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

keyboardDrummer · 2022-12-12T09:27:13Z

Source/DafnyCore/Auditor/Assumption.cs

+/// combinations of these properties classify the entity as containing
+/// an assumption.
+/// </summary>
+public struct AssumptionProperties {


This struct doesn't sit well with me. It has a number of fields that contains information which is already available in the AST, and that may or may not apply to the AST Node that this AssumptionProperties is reflecting.

It would make more sense to me to directly extract Description() from the AST, without having AssumptionProperties as an in between. Note that implementing behavior on the AST nodes directly also has the advantage that if you add a new type of AST Node you're prompted to think about implementing the AssumptionDescription() method, while it's much harder to find the list of checks done in AssumptionExtractor. GetAssumptionTags

Also, I would like to know which of these descriptions should be warnings, and if they should be warnings, I would first makes them warnings and then extract them by filtering them from the actual warnings.

@keyboardDrummer have a point of ensuring that we want to ensure we can grow the auditor with new AST nodes.

However, if you don't want to add cluttering "AssumptionDecription()" on every legitimate node, then you'd have to add something in the base nodes that is going to be overriden by descendants, which in effect has the same effect as having a struct that contains assumptions.
It's about the same reason why we don't extract boogie assertions right from every node of the AST in the expression tree.
And I think it's appropriate to encode this information in a separate struct than trying to embed it deeply in AST nodes. It makes reasoning and reporting much more straightforward, and does not interfere with the existing AST.

An alternative to what's there right now but perhaps compatible with what @keyboardDrummer is suggesting would be to have a separate traversal (not a set of instance methods on the nodes) that goes directly from the tree to a set of (issue, mitigation) pairs. That is, GetAssumptionTags could be called GetAssumptionDescriptions and return a list of (string, string) pairs (or a record) directly.

I'd be quite happy to move in that direction. Early in the design I wanted to avoid doing many traversals over the whole tree, but the way things worked out that wouldn't happen even with the direct implementation.

And I think it's appropriate to encode this information in a separate struct than trying to embed it deeply in AST nodes.

Why? I don't see a downside to putting this information into the AST nodes. I would say that whatever is mandatory for Dafny, such as parsing, printing and resolution, should be in the AST nodes. I think this auditor is similar to warnings generated during resolution.

which in effect has the same effect as having a struct that contains assumptions.

It's not the same, because it's easy to see what methods you can override on a class, but it's not easy to see every place where all ASTs nodes are handled by a switch.

Why? I don't see a downside to putting this information into the AST nodes. I would say that whatever is mandatory for Dafny, such as parsing, printing and resolution, should be in the AST nodes. I think this auditor is similar to warnings generated during resolution.

So you want to make the auditor mandatory? It looks like that's the single point of debate. If it's not mandatory, then it makes sense to keep it separate. If it's mandatory, then yes of course we should just put all its information into the AST warnings and get rid of the auditor itself.
I believe it's not mandatory as it could reduce productivity, as explained in another post.

Having thought about this some more, I think I'm convinced that embedding the assumption descriptions in the AST does make sense, in part because it'll make sure that there's a clear place to put any description of assumptions that may be present in any language construct as the language evolves. That's just a question of where assumption descriptions exist, though, not a question of when or how they should be reported.

I firmly believe that there are multiple use cases, each of which warrants different "warnings", or at least different output. The key long-term goal of the auditor, in my mind, is to give a complete view of the possible caveats to the verification of a particular program. Some of those caveats may be completely unavoidable (i.e., "we assume that Z3 v4.8.5 is correct", which is not currently in the auditor report but will ultimately be included), so they don't make sense as warnings during development but do make sense as part of a complete assurance summary.

keyboardDrummer · 2022-12-12T09:27:29Z

Source/DafnyCore/Auditor/Assumption.cs

+ }
+ if (HasVerifyFalseAttribute) {
+ descs.Add(
+ ("Definition has `{:verify false}` attribute.",


This should be a warning right?

To warn or not to warn, the question is more about when it is appropriate to warn users and how much. It's not debatable to warn the user during an audit. However, I'm not sure I want to clutter my diagnostics with warnings when all I want is the result of verifying a portion of code. So I wouldn't mind these warnings if they were the only thing left (meaning I'm ready to move forward, I fixed all my errors on unrelated code), but while I'm having errors in my IDE, having such warnings for annotations I added manually myself to bypass the verifier would be extremely annoying.

By the way, on a side note, {:verify false} can be used in the following scenario. There are several methods, I edit them in VSCode, I want to focus on one (I use verification on save) and I've seen it take 10 seconds when I do a single edit for the language to cancel the verification of other methods and consider the new code. This is really frustrating sometimes. I don't know what is broken here.

Every assumption detected here is emitted as a warning by default (but can be written to a file in one of several formats, instead, as an option). So it seems to me the question is more one of which of the assumption types identified here should be warned about when not using the auditor. I could imagine that some of them might always be on, and some might be turned on by something like a --warn-assumptions flag. Do either of you have thoughts on that?

The fact that it may make sense to always emit some of these warnings argues even more strongly for including this functionality in the core implementation of Dafny rather than as an optional plugin.

To warn or not to warn, the question is more about when it is appropriate to warn users and how much. It's not debatable to warn the user during an audit. However, I'm not sure I want to clutter my diagnostics with warnings when all I want is the result of verifying a portion of code. So I wouldn't mind these warnings if they were the only thing left (meaning I'm ready to move forward, I fixed all my errors on unrelated code), but while I'm having errors in my IDE, having such warnings for annotations I added manually myself to bypass the verifier would be extremely annoying.

Could you explain what a warning means to you?

To me a warning means I need to resolve this before I create a commit, so I feel free to ignore them or hide them until I'm happy with my code and I'm ready to polish it for a commit.

It sounds like for you a warning is something that you already want to resolve while you're still getting verification to pass. Why is that?

Every assumption detected here is emitted as a warning by default

What do you mean? With a warning I mean that if you run dafny verify on a source file that includes {:verify false}, it returns a warning for that. Right now, that's not the case.

I could imagine that some of them might always be on

I think I said this before, but any warning that is not on by default is a UX flaw to me. We're telling users that probably they don't want to use this (because the default is OFF), but they should consider using it (that's why we added it). It's better not to overload the user with these small choices.

--warn-assumptions should be on by default.

Could you explain what a warning means to you?
To me a warning means I need to resolve this before I create a commit, so I feel free to ignore them or hide them until I'm happy with my code and I'm ready to polish it for a commit.
It sounds like for you a warning is something that you already want to resolve while you're still getting verification to pass. Why is that?

I don't place the bar of resolving warnings before creating a commit.
Moving forward one sub-proof is enough for me when writing Dafny to realize I should commit my result, even if there are other assume false. These kinds of warnings should be resolved when creating a PR to the main branch however, as they should be detected by the CI.

I'm not sure of your description of a warning, but it supposes that there is a single notion of warning. But in a verification-aware language like Dafny, I started recently to strongly believe there should be two kinds of warnings: verifier warnings and compiler/resolver warnings. To me, the only reason to trigger a verifier warning is when Dafny was able to prove that the code is correct, but it found unproven assumptions, or obviously false requirements, that the user should be aware of - so that they don't commit their code knowingly.
Users writing Dafny regularly understand why, as they are using proof scaffolding techniques where warnings would not be relevant until they actually prove something. Adding warnings on top of their regular proof authoring experience where they already struggle to prove a goal would be suboptimal.
Of course, these warnings should be reported by the auditor as well.

The second notion of warnings are regular warnings triggered by any mainstream language, such as a redundant case, or a variable that looks like a existing constructor in a pattern matching. These should be reported in any case.

We don't have mechanisms to hide warnings as of today, so I'm not counting on hiding warnings as part of a workflow - and I'm not sure it would be even desirable to force people hiding verification warnings. This looks to me like a UX flaw.

On the side, I do agree that every warning should be turned on by default. But only shown when some conditions are met, as explained above.

I don't place the bar of resolving warnings before creating a commit.

Sorry, I should have said before pushing to CI. Seems like we agree that before pushing to CI all warnings should be resolved, but while you still have (verification) errors, warnings can be ignored.

We don't have mechanisms to hide warnings as of today, so I'm not counting on hiding warnings as part of a workflow

You can tell the IDE to only show errors, and generally an IDE will sort warnings to be below errors, so they're easy to ignore.

I'm not sure of your description of a warning, but it supposes that there is a single notion of warning. But in a verification-aware language like Dafny, I started recently to strongly believe there should be two kinds of warnings: verifier warnings and compiler/resolver warnings.
On the side, I do agree that every warning should be turned on by default. But only shown when some conditions are met, as explained above.

My impression is that you want warnings to be ordered with verification warnings coming before non-verification warnings, and because it seems IDEs don't let you order warnings, you'd prefer not to publish lower priority warnings when there are still higher priority ones.

I think that's a UX detail we can think about, but I would prefer not discussing that in the scope of this PR, since it doesn't seem related.

keyboardDrummer · 2022-12-12T09:55:50Z

Source/DafnyCore/Auditor/Assumption.cs

+ if (IsTrait && MayNotTerminate) {
+ descs.Add(
+ ("Trait method calls may not terminate (uses `{:termination false}`).",
+ "Remove or justify."));


What does 'justify' mean? Does performing 'justify' cause this line in the report to disappear? I think that any report information whose action does not remove the report line reduces the effectiveness of the entire report.

Source/DafnyCore/Auditor/Assumption.cs

keyboardDrummer · 2022-12-12T09:56:22Z

Source/DafnyCore/Auditor/Assumption.cs

+ }
+ if (IsCallable && HasAssumeInBody) {
+ descs.Add(
+ ("Definition has `assume` statement in body.",


This should be a warning right?

It is currently not a warning.

keyboardDrummer · 2022-12-12T09:56:55Z

Source/DafnyCore/Auditor/Assumption.cs

+
+ if (IsCallable && MissingBody) {
+ descs.Add(
+ ((IsGhost ? "Ghost" : "Compiled") +


This should be a warning right?

I don't think it's a warning currently.

keyboardDrummer · 2022-12-12T09:59:00Z

Source/DafnyCore/Auditor/Assumption.cs

+ if (IsCallable && HasExternAttribute && RequiresClauses is not null) {
+ descs.Add(
+ ("Declaration with `{:extern}` has a requires clause.",
+ "Test external caller (maybe with `/testContracts`) or justify."));


What does 'justify' mean? Does performing 'justify' cause this line in the report to disappear? I think that any report information whose action does not remove the report line reduces the effectiveness of the entire report.

Agreed with the "justified".
On the side, why do we want to report requires on extern methods?
Adding a requires is always stronger to the verifier. It seems wrong that we are reporting on things that are strongly verified, extern or not.
Adding an ensures clause is always weaker. Weaknesses are what should be reported, especially if the method is extern.

I might remove the justify text, or enable it optionally. The reason for it is that output produced in the markdown-ietf format can be used by Duvet, which can then keep track of whether there are comments in the source code explaining why a particular assumption has been made. In this particular case, one of those comments would probably appear on the code that's responsible for testing the contract on the extern. However, it doesn't make much sense when not using that output format.

As for requires clauses, it depends on how the {:extern} is being used. It can be used to mark code as being called by an external client (and possibly to change the compiled name in that case). If it's being used that way, then any requires clause is an unchecked assumption. Ideally, we would distinguish between external "imports" and "exports", and warn about ensures clauses in the former case and requires clauses in the latter case. That'll have to wait for the FFI redesign that @robin-aws is working on though.

Can you explain what actions users can take to remove flagged code from the report? If there are situations where that is not possible, then I don't think the report will be effective.

As for requires clauses, it depends on how the {:extern} is being used. It can be used to mark code as being called by an external client (and possibly to change the compiled name in that case). If it's being used that way, then any requires clause is an unchecked assumption

Oh yeah indeed that makes sense. I hadn't thought of that. It's a way to fail more gracefully. How would could you provide the information that the external caller's interface is tested?

If you use Duvet, you can add a comment to the code doing the testing that declares that it tests that property. There isn't immediately a way to do that with the other report formats.

keyboardDrummer · 2022-12-12T09:59:07Z

Source/DafnyCore/Auditor/Assumption.cs

+ if (IsCallable && HasExternAttribute && EnsuresClauses is not null) {
+ descs.Add(
+ ("Declaration with `{:extern}` has a ensures clause.",
+ "Test external callee (maybe with `/testContracts`) or justify."));


What does 'justify' mean? Does performing 'justify' cause this line in the report to disappear? I think that any report information whose action does not remove the report line reduces the effectiveness of the entire report.

keyboardDrummer · 2022-12-12T10:02:15Z

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -176,5 +186,15 @@ public class CommonOptionBag {
 options.DefiniteAssignmentLevel = value ? 1 : 2;
 });

+ DafnyOptions.RegisterLegacyBinding(ReportFileOption, (options, value) => {
+ options.AuditorReportFile = value;


Instead of the field dafnyOptions.AuditorReportFile, use dafnyOptions.Get(ReportFileOption), and then you don't need to call RegisterLegacyBinding either.

keyboardDrummer · 2022-12-12T10:02:47Z

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -119,6 +119,16 @@ public class CommonOptionBag {
 public static readonly Option<bool> IncludeRuntime = new("--include-runtime",
 "Include the Dafny runtime as source in the target language.");

+ public static readonly Option<string> ReportFileOption = new("--report-file",


Could you move these options to AuditCommand.cs?

MikaelMayer

This looks great! A few questions and requests there and there.

MikaelMayer · 2022-12-12T15:31:37Z

Source/DafnyCore/Auditor/Assumption.cs

+ (MissingBody || HasExternAttribute)) ||
+ HasAssumeInBody)) ||
+ (MayNotTerminate && (IsCallable || IsTrait));
+ }


I wouldn't count the requires clause of an {:extern} or bodiless method as an assumption (i.e. would be a false positive), because that requires clause is always verified if it is called. I would be okay if we count requires clauses as assumptions if a method containing them had a body and was never called by some Dafny code.
But perhaps I'm short-sighted and I am missing something?

I put an explanation of this in one of my previous comment responses. :) It's an assumption for code that'll be called by external code.

MikaelMayer · 2022-12-12T15:35:52Z

Source/DafnyCore/Auditor/Assumption.cs

+/// combinations of these properties classify the entity as containing
+/// an assumption.
+/// </summary>
+public struct AssumptionProperties {


@keyboardDrummer have a point of ensuring that we want to ensure we can grow the auditor with new AST nodes.

However, if you don't want to add cluttering "AssumptionDecription()" on every legitimate node, then you'd have to add something in the base nodes that is going to be overriden by descendants, which in effect has the same effect as having a struct that contains assumptions.
It's about the same reason why we don't extract boogie assertions right from every node of the AST in the expression tree.
And I think it's appropriate to encode this information in a separate struct than trying to embed it deeply in AST nodes. It makes reasoning and reporting much more straightforward, and does not interfere with the existing AST.

MikaelMayer · 2022-12-12T15:38:42Z

Source/DafnyCore/Auditor/Assumption.cs

+
+ if (IsCallable && MissingBody) {
+ descs.Add(
+ ((IsGhost ? "Ghost" : "Compiled") +


I don't think it's a warning currently.

MikaelMayer · 2022-12-12T15:41:53Z

Source/DafnyCore/Auditor/Assumption.cs

+ if (IsCallable && HasExternAttribute && RequiresClauses is not null) {
+ descs.Add(
+ ("Declaration with `{:extern}` has a requires clause.",
+ "Test external caller (maybe with `/testContracts`) or justify."));


Agreed with the "justified".
On the side, why do we want to report requires on extern methods?
Adding a requires is always stronger to the verifier. It seems wrong that we are reporting on things that are strongly verified, extern or not.
Adding an ensures clause is always weaker. Weaknesses are what should be reported, especially if the method is extern.

MikaelMayer · 2022-12-12T15:42:24Z

Source/DafnyCore/Auditor/Assumption.cs

+ }
+ if (IsCallable && HasAssumeInBody) {
+ descs.Add(
+ ("Definition has `assume` statement in body.",


It is currently not a warning.

MikaelMayer · 2022-12-12T16:01:37Z

Source/DafnyCore/Auditor/AuditReport.cs

+ StringBuilder text = new StringBuilder();
+
+ foreach (var module in modulesWithEntries) {
+ text.AppendLine($"# Module `{module.Name}`");


Would it make sense to make the audit smaller by not reporting types and members if there is no audit warning in that module anyway? To achieve that, you could store the temporary strings and not emit sub-sections if they are empty. That way, the report would only contain the assumptions.

I'm not using the auditor myself so I don't know what is really useful for Dafny users. You probably know better.

If I understand what you're saying, that's already what it's doing. The modulesWithEntries collection includes only the modules that have audit warnings.

Does the filtering works as well on top-level declarations, and members? That's also something I had in mind

Yes, see lines 121 and 135.

MikaelMayer · 2022-12-12T16:50:00Z

Test/auditor/TestAuditor.dfy.html.expect

+ }
+ .display.math{display: block; text-align: center; margin: 0.5rem auto;}
+ table tr:nth-child(odd) td {
+ background-color: #BBBBBB;


Suggested change

background-color: #BBBBBB;

background-color: #EEE;

It looks better if it's lighter.

Sounds good!

MikaelMayer · 2022-12-12T16:51:16Z

Test/auditor/TestAuditor.dfy.html.expect

+<tr><td>GenerateBytes</td><td>True</td><td>False</td><td>True</td><td>Declaration with `{:extern}` has a ensures clause.</td><td>Test external callee (maybe with `/testContracts`) or justify.</td></tr>
+<tr><td>GenerateBytesWithModel</td><td>True</td><td>False</td><td>True</td><td>Declaration with `{:extern}` has a requires clause.</td><td>Test external caller (maybe with `/testContracts`) or justify.</td></tr>
+<tr><td>GenerateBytesWithModel</td><td>True</td><td>False</td><td>True</td><td>Declaration with `{:extern}` has a ensures clause.</td><td>Test external callee (maybe with `/testContracts`) or justify.</td></tr>
+<tr><td>GenerateBytesWrapper</td><td>True</td><td>False</td><td>False</td><td>Definition has `assume` statement in body.</td><td>Replace with `assert` and prove or add `{:axiom}`.</td></tr>


Suggested change

<tr><td>GenerateBytesWrapper</td><td>True</td><td>False</td><td>False</td><td>Definition has `assume` statement in body.</td><td>Replace with `assert` and prove or add `{:axiom}`.</td></tr>

<tr><td>GenerateBytesWrapper</td><td>True</td><td>False</td><td>False</td><td>Definition has `assume` statement in body.</td><td>Replace with <code>assert</code> and prove or add `{:axiom}`.</td></tr>

in HTML, could you please replace all backticks by code tags?

Also, I'm surprised that "Explicit Assumption" is false but the comment says that an assume statement was found and should be replaced by assert. Can you please comment on that?

I'll audit the "explicit assumption" logic, but the idea behind it is that it includes things that are clearly intended as assumptions, as opposed to those that could be accidental. So assume {:axiom} would be included but assume on its own would not. A different term might be warranted. Ideas welcome!

Oh I get it. Maybe "Axiomatized assumptions", "Forced assumptions"? Or perhaps keep "Explicit assumption" but just change the error message "Definition has assume statement with no {:axiom} in body. Either put {:axiom} or replace the assume by an assert"?

MikaelMayer · 2022-12-12T16:54:24Z

Test/auditor/TestAuditor.dfy.html.expect

+ vertical-align: middle;
+ }
+ .display.math{display: block; text-align: center; margin: 0.5rem auto;}
+ table tr:nth-child(odd) td {


Suggested change

table tr:nth-child(odd) td {

thead {

position: sticky;

top: 0px;

background: white;

}

table tr:nth-child(odd) td {

Looks much nicer for bigger tables if the header is sticky :-)

MikaelMayer · 2022-12-12T16:58:58Z

Test/auditor/TestAuditor.dfy.html.expect

+<tr><th>Name</th><th>Compiled</th><th>Explicit Assumption</th><th>Extern</th><th>Issue</th><th>Mitigation</th></tr>
+<tr><td>T</td><td>True</td><td>False</td><td>False</td><td>Trait method calls may not terminate (uses `{:termination false}`).</td><td>Remove or justify.</td></tr>
+<tr><td>MinusBv8NoBody</td><td>False</td><td>False</td><td>False</td><td>Ghost declaration has no body and has an ensures clause.</td><td>Provide a body or add `{:axiom}`.</td></tr>
+<tr><td>LeftShiftBV128</td><td>False</td><td>True</td><td>False</td><td>Declaration has explicit `{:axiom}` attribute.</td><td>Provide a proof, test, or other justification.</td></tr>


Suggested change

<tr><td>LeftShiftBV128</td><td>False</td><td>True</td><td>False</td><td>Declaration has explicit `{:axiom}` attribute.</td><td>Provide a proof, test, or other justification.</td></tr>

<tr><td>LeftShiftBV128</td><td>False</td><td class="true">True</td><td>False</td><td>Declaration has explicit `{:axiom}` attribute.</td><td>Provide a proof, test, or other justification.</td></tr>

I suggest that for the second and third column of booleans, you add a class if it's true, and a slightly different color (or bold) like this in CSS:

true { font-weight: bold; }

On further thought, the choice of which to highlight is somewhat context-dependent. Whether "true" or "false" should stand out depends on what you're doing. One of the intended purposes of the table sorting mechanism is to allow you to separate them so that you can focus on whichever category you most care about at the time.

Could you give me an example where a "True" might be desirable?
And what is this table sorting mechanism? is it accessible in HTML?

If you're using the HTML output, you can click on a header to sort by that column.

* Have {:axiom} override other warnings * Only warn on missing body when there are ensures clauses

keyboardDrummer · 2022-12-15T09:41:02Z

Source/DafnyDriver/Commands/AuditCommand.cs

@@ -21,5 +57,9 @@ class AuditCommand : ICommandSpec {
 public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
 dafnyOptions.Compile = false;
 dafnyOptions.Verify = false;
+ dafnyOptions.AuditProgram = true;
+ dafnyOptions.AuditorReportFile = dafnyOptions.Get(ReportFileOption);


I would prefer not having the field DafnyOptions.AuditorReportFile and instead using dafnyOptions.Get(ReportFileOption) everywhere. That way there is less boilerplate, but more importantly, DafnyOptions doesn't contain code related to many different things, and the option code can be located purely where the option is used.

I believe that would require moving the option definition back into DafnyCore instead of having it be a member of the AuditCommand class, since it would need to be checked from DafnyCore code (i.e., from the auditor code). Are you happy with having the option move back?

I see, ideally we would let AuditorCommand inject the Auditor.Auditor into Resolver, without Resolver.cs having to know about the Auditor.

Could you use the plugins mechanism for that?

Resolver already has

foreach (var plugin in DafnyOptions.O.Plugins) { rewriters.AddRange(plugin.GetRewriters(reporter)); }

I've moved the audit options into the Auditor class, so the rest of the codebase (except AuditCommand) doesn't need to know about them.

I'm not entirely sure I understand what goal you have in mind for the plugin mechanism here, though.

I'm not entirely sure I understand what goal you have in mind for the plugin mechanism here, though.

Then Auditor/Auditor.cs, Auditor/AuditReport.cs could move to DafnyDriver, and Resolver.cs wouldn't need changes.

keyboardDrummer · 2022-12-15T09:49:19Z

Source/DafnyCore/Auditor/Assumption.cs

+namespace Microsoft.Dafny.Auditor;
+
+public record AssumptionDescription(string issue, string mitigation, bool isExplicit) {
+ public static AssumptionDescription AxiomAttributeAssumption = new(


I would inline these statics. For the ones that are used multiple times, such as ExternWithRequires for function and method, you could move them to either one of those two, or a common location like ICallable.

I really like having them all in one place, so they can easily be reviewed for wording. Large string constants embedded in definitions seem like code smells to me.

atomb · 2023-01-04T23:54:40Z

I think I see three remaining open questions with this PR:

Should any of the issues reported by dafny audit also be warnings when using dafny verify or dafny resolve? I think several should be, but in a separate PR.
Should the auditor code be part of the DafnyDriver package? I don't particularly like this solution, though I do like the idea of making the code use the plugin interface and be capable of being separated out eventually. If we were to move the code in the Auditor directory into DafnyDriver, I'd argue that RunAllTestsMainMethod and ExpectContracts should go there, too, if not others.
Should we remove the --compare-report option? It's easy enough to do, but the current behavior also seems convenient to me. I'm on the fence.

Am I missing anything else?

davidcok · 2023-01-04T23:59:31Z

On (1) - I say yes, though I'd have to review a list of audit warnings to say which should be dafny warnings.
On (3) - I'd keep it for now. I can imagine a project that has some audit findings it is willing to live with but wanting CI to check that those findings have not changed.

keyboardDrummer · 2023-01-07T13:00:31Z

Hey, since we've been discussing this PR for quite a while, I wonder whether it wouldn't be better to just merge it so we get more data on the feature and the implementation. We can always change things again later. I will approve this PR as is but with comments. I'll leave it up to you whether you want to address the comments or merge.

Should the auditor code be part of the DafnyDriver package? I don't particularly like this solution, though I do like the idea of making the code use the plugin interface and be capable of being separated out eventually.

In a previous comment (#3175 (comment)) I asked whether we could put the code that determines the assumptions in the AST nodes that contain those assumptions. We've now switched to that but only partially, since the code in Method still refers to other AST node types like ForallStmt and OneBodyLoopStmt, as opposed to have an interface IHasAssumption : INode that is implemented by ForallStmt and OneBodyLoopStmt, and that new AST types could implement. There's also some duplication between Function and Method that I think could be avoided if we had a single AST traversal that looks for IHasAssumption in all nodes.

However, since I'm not sure what this feature will evolve towards, I've changed my mind on the above and would prefer to have all the code in DafnyDriver, so the code for the feature is all in the same project and isolated from the rest.

If we were to move the code in the Auditor directory into DafnyDriver, I'd argue that RunAllTestsMainMethod and ExpectContracts should go there, too, if not others.

Agreed.

Should any of the issues reported by dafny audit also be warnings when using dafny verify or dafny resolve? I think several should be, but in a separate PR.

If we keep the code from this feature isolated in DafnyDriver, then I think that question can be out of scope for this PR.

Should we remove the --compare-report option? It's easy enough to do, but the current behavior also seems convenient to me. I'm on the fence.

Let's leave it in.

keyboardDrummer · 2023-01-07T13:01:43Z

Source/DafnyCore/AST/DafnyAst.cs

@@ -41,6 +41,10 @@ public abstract class INode {
 /// </summary>
 public abstract IEnumerable<INode> Children { get; }

+ public IEnumerable<INode> DeepChildren() {


This is extremely subjective, but I'm used to calling a property like this Descendants

Yeah, I like that name better, too. :)

keyboardDrummer · 2023-01-07T13:03:20Z

Source/DafnyCore/AST/MemberDecls.cs

+ yield return AssumptionDescription.ForallWithoutBody;
+ }
+
+ if (DeepChildren().Any(n => n is OneBodyLoopStmt loopStmt && loopStmt.Body is null)) {


Traversing DeepChildren() three times, while in practice it probably doesn't matter much, doesn't look great. I think changing this into a single foreach would be better.

Even better would probably be to adopt your suggestion above to make this be an assumption on the loop itself, rather than on the method or function, and have member declarations yield all assumptions from their descendants. I'll make that change.

MikaelMayer

I'll approve it as this as we discussed about it. I'm fine leaving the code for the audit as part of DafnyCore because it feels like it belongs there. It will make it easier as well to ship Dafny as a library with audit integrated, and when we will add warnings for the things that are being audited, being able to detect duplicates feels more like the code should be at the same place.
For the command to do the diff, I'm good leaving it there so that one can do a diff without having to check the OS (diff does not exist on Windows)
Let's merge it and see how it evolves.

MikaelMayer · 2023-01-09T15:35:15Z

Source/DafnyCore/DafnyOptions.cs

@@ -195,7 +195,7 @@ public class DafnyOptions : Bpl.CommandLineOptions {
 }

 public DafnyOptions()
- : base("Dafny", "Dafny program verifier", new DafnyConsolePrinter()) {
+ : base("dafny", "Dafny program verifier", new DafnyConsolePrinter()) {


Why this change?

It makes the output of dafny audit --help (and other command --help invocations) more correct. Previously, the help text made it appear that the name of the executable was Dafny.

Also rename a few things for clarity and consistency.

…ted-auditor

This PR integrates the functionality of the auditor plugin (https://github.com/dafny-lang/compiler-bootstrap/tree/main/src/Tools/Auditor) as built-in functionality exposed through the `dafny audit` command. It also adds support for a new output format (Markdown formatted in sections rather than a table, using IETF RFC-style language) and an option to compare the report that would be generated with an existing file, rather than creating that file. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

atomb added 7 commits December 9, 2022 14:44

Initial C# port of auditor

2117393

Add release notes entry

fb98db0

Remove obsolete test output file

4c22634

Clean up option handling

cb21956

Remove unused method

fcb04ee

Add some documentation comments

4ada761

Merge remote-tracking branch 'upstream/master' into integrated-auditor

5b75fe3

atomb marked this pull request as ready for review December 10, 2022 00:44

atomb requested review from robin-aws, MikaelMayer and keyboardDrummer and removed request for robin-aws and MikaelMayer December 10, 2022 00:44

keyboardDrummer reviewed Dec 12, 2022

View reviewed changes

MikaelMayer requested changes Dec 12, 2022

View reviewed changes

atomb added 2 commits December 12, 2022 16:58

Introduce AssumptionDescription record

9092800

HTML formatting changes suggested by @MikaelMayer

ec9482c

keyboardDrummer assigned atomb Dec 13, 2022

atomb added 6 commits December 13, 2022 14:58

Refactor command-line parsing

0025b0d

Remove “justify” terminology

c36c7e9

Separate text of assumption descriptions

f583f9e

Embed assumptions in AST

e6357b2

Two improvements:

ef9882f

* Have {:axiom} override other warnings * Only warn on missing body when there are ensures clauses

Remove obsolete code

89501ce

atomb requested review from MikaelMayer and keyboardDrummer December 15, 2022 00:22

keyboardDrummer reviewed Dec 15, 2022

View reviewed changes

atomb added 4 commits January 3, 2023 16:25

Merge branch 'master' into integrated-auditor

cc60d12

Report on forall/loop statements without bodies

a3aacc9

Update expected help/version output

7e757d3

Merge remote-tracking branch 'upstream/master' into integrated-auditor

d55c89f

atomb requested a review from keyboardDrummer January 4, 2023 23:56

atomb added 2 commits January 6, 2023 09:49

Report only concrete definitions without bodies

99a8bab

Merge branch 'master' into integrated-auditor

034ae37

atomb enabled auto-merge (squash) January 6, 2023 22:21

keyboardDrummer previously approved these changes Jan 7, 2023

View reviewed changes

keyboardDrummer reviewed Jan 7, 2023

View reviewed changes

MikaelMayer previously approved these changes Jan 9, 2023

View reviewed changes

Merge branch 'master' into integrated-auditor

3cabce5

atomb disabled auto-merge January 9, 2023 16:45

atomb added 3 commits January 9, 2023 09:24

Move assumptions deeper into AST

20249c5

Also rename a few things for clarity and consistency.

Merge remote-tracking branch 'upstream/master' into integrated-auditor

c283bc3

Merge remote-tracking branch 'origin/integrated-auditor' into integra…

3dc1abb

…ted-auditor

atomb dismissed stale reviews from MikaelMayer and keyboardDrummer via 3dc1abb January 9, 2023 17:25

atomb enabled auto-merge (squash) January 9, 2023 17:28

MikaelMayer approved these changes Jan 9, 2023

View reviewed changes

Merge branch 'master' into integrated-auditor

c288dd6

atomb merged commit a4d5e89 into dafny-lang:master Jan 9, 2023

	<tr><td>GenerateBytesWrapper</td><td>True</td><td>False</td><td>False</td><td>Definition has `assume` statement in body.</td><td>Replace with `assert` and prove or add `{:axiom}`.</td></tr>
	<tr><td>GenerateBytesWrapper</td><td>True</td><td>False</td><td>False</td><td>Definition has `assume` statement in body.</td><td>Replace with <code>assert</code> and prove or add `{:axiom}`.</td></tr>

- table tr:nth-child(odd) td {
+ thead {
+ position: sticky;
+ top: 0px;
+ background: white;
+ }
+ table tr:nth-child(odd) td {

	<tr><td>LeftShiftBV128</td><td>False</td><td>True</td><td>False</td><td>Declaration has explicit `{:axiom}` attribute.</td><td>Provide a proof, test, or other justification.</td></tr>
	<tr><td>LeftShiftBV128</td><td>False</td><td class="true">True</td><td>False</td><td>Declaration has explicit `{:axiom}` attribute.</td><td>Provide a proof, test, or other justification.</td></tr>

Initial C# port of auditor #3175

Initial C# port of auditor #3175

Conversation

atomb commented Dec 9, 2022

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 Dec 13, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Dec 13, 2022 • 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

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 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

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 Dec 15, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Dec 16, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Dec 15, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented Jan 4, 2023

davidcok commented Jan 4, 2023

keyboardDrummer commented Jan 7, 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

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

keyboardDrummer Dec 13, 2022 •

edited

Loading

keyboardDrummer Dec 13, 2022 •

edited

Loading

keyboardDrummer Dec 15, 2022 •

edited

Loading

keyboardDrummer Dec 16, 2022 •

edited

Loading

keyboardDrummer Dec 15, 2022 •

edited

Loading

keyboardDrummer commented Jan 7, 2023 •

edited

Loading