Add auditor support for the :concurrent attribute

Source/DafnyCore/AST/DafnyAst.cs

@@ -168,6 +168,8 @@ void ObjectInvariant() {
  }
 
  public static string AxiomAttributeName = "axiom";
+ public static string ConcurrentAttributeName = "concurrent";
+ public static string ExternAttributeName = "extern";
  public static string VerifyAttributeName = "verify";
  public static string AutoGeneratedAttributeName = "auto_generated";
 

Source/DafnyCore/AST/Function.cs

@@ -51,11 +51,15 @@ public override IEnumerable<AssumptionDescription> Assumptions() {
  yield return AssumptionDescription.NoBody(IsGhost);
  }
 
- if (Attributes.Contains(Attributes, "extern") && HasPostcondition) {
+ if (Body is not null && HasConcurrentAttribute) {
+ yield return AssumptionDescription.HasConcurrentAttribute;
+ }
+
+ if (HasExternAttribute && HasPostcondition) {
  yield return AssumptionDescription.ExternWithPostcondition;
  }
 
- if (Attributes.Contains(Attributes, "extern") && HasPrecondition) {
+ if (HasExternAttribute && HasPrecondition) {
  yield return AssumptionDescription.ExternWithPrecondition;
  }
 

Source/DafnyCore/AST/Method.cs

@@ -46,11 +46,15 @@ public override IEnumerable<AssumptionDescription> Assumptions() {
  yield return AssumptionDescription.NoBody(IsGhost);
  }
 
- if (Attributes.Contains(Attributes, "extern") && HasPostcondition) {
+ if (Body is not null && HasConcurrentAttribute) {
+ yield return AssumptionDescription.HasConcurrentAttribute;
+ }
+
+ if (HasExternAttribute && HasPostcondition) {
  yield return AssumptionDescription.ExternWithPostcondition;
  }
 
- if (Attributes.Contains(Attributes, "extern") && HasPrecondition) {
+ if (HasExternAttribute && HasPrecondition) {
  yield return AssumptionDescription.ExternWithPrecondition;
  }
 
@@ -63,7 +67,6 @@ public override IEnumerable<AssumptionDescription> Assumptions() {
  yield return a;
  }
  }
-
  }
 
  public override IEnumerable<Expression> SubExpressions {

Source/DafnyCore/AST/TopLevelDeclarations.cs

@@ -31,6 +31,12 @@ void ObjectInvariant() {
  public bool HasAxiomAttribute =>
  Attributes.Contains(Attributes, Attributes.AxiomAttributeName);
 
+ public bool HasConcurrentAttribute =>
+ Attributes.Contains(Attributes, Attributes.ConcurrentAttributeName);
+
+ public bool HasExternAttribute =>
+ Attributes.Contains(Attributes, Attributes.ExternAttributeName);
+
  public bool HasAutoGeneratedAttribute =>
  Attributes.Contains(Attributes, Attributes.AutoGeneratedAttributeName);
 

Source/DafnyCore/Auditor/Assumption.cs

@@ -43,6 +43,10 @@ public record AssumptionDescription(string issue, string mitigation, bool isExpl
  mitigation: "Provide a body.",
  isExplicit: false
  );
+ public static AssumptionDescription HasConcurrentAttribute = new(
+ issue: "Declaration has [{:concurrent}] attribute.",
+ mitigation: "Manually review and test in a concurrent setting.",
+ isExplicit: false);
 
  public static AssumptionDescription NoBody(bool isGhost) {
  return new(

Source/DafnyCore/Auditor/AuditReport.cs

@@ -42,7 +42,7 @@ public IEnumerable<Assumption> AllAssumptions() {
  }
 
  private string RenderRow(string beg, string sep, string end, IEnumerable<string> cells) {
- return beg + String.Join(sep, cells) + end;
+ return beg + String.Join(sep, cells) + end + "\n";
  }
 
  private string GetFullName(Declaration decl) {
@@ -70,7 +70,7 @@ private IEnumerable<string> IssueRow(Assumption a, string issue, string mitigati
  private string RenderAssumptionRows(Assumption a, string beg, string sep, string end, Func<string, string> targetFormatter) {
  var rows = a.assumptions
  .Select((desc, _) => RenderRow(beg, sep, end, IssueRow(a, desc.issue, desc.mitigation, targetFormatter)));
- return rows.Count() > 0 ? String.Join("\n", rows) : a.ToString();
+ return rows.Count() > 0 ? String.Concat(rows) : a.ToString();
  }
 
  public static string UpdateVerbatim(string text, string beg, string end) {
@@ -92,15 +92,15 @@ public string RenderHTMLTable() {
  "<tr><th>Name</th><th>Compiled</th><th>Explicit Assumption</th>" +
  "<th>Extern</th><th>Issue</th><th>Mitigation</th></tr>\n";
  var rows = AllAssumptions().Select(RenderAssumptionRowsHTML);
- return header + String.Join("\n", rows);
+ return header + String.Concat(rows);
  }
 
  public string RenderMarkdownTable() {
  var header =
  "|Name|Compiled|Explicit Assumption|Extern|Issue|Mitigation|\n" +
  "|----|--------|-------------------|------|-----|----------|\n";
  var rows = AllAssumptions().Select(RenderAssumptionRowsMarkdown);
- return header + String.Join("\n", rows);
+ return header + String.Concat(rows);
  }
 
  private void AppendMarkdownIETFDescription(AssumptionDescription desc, StringBuilder text) {

Source/DafnyCore/Auditor/Auditor.cs

@@ -106,7 +106,7 @@ private string GenerateHTMLReport(AuditReport report) {
  return table;
  }
  var templateText = new StreamReader(templateStream).ReadToEnd();
- return templateText.Replace("{{TABLE}}", table.ToString());
+ return templateText.Replace("{{TABLE}}\n", table.ToString());
  }
 
  internal override void PostResolve(Program program) {

Test/auditor/TestAuditor.dfy

@@ -104,3 +104,9 @@ abstract module M {
 opaque function f(): int {
  0
 }
+
+// A method that's safe for concurrent use because it doesn't touch the
+// heap.
+method {:concurrent} ConcurrentMethod(x: int) returns (r: int) {
+ return x;
+}

Test/auditor/TestAuditor.dfy-ietf.md.expect

@@ -53,3 +53,7 @@
 ### Member `LoopWithoutBody`
 
 * Definition contains loop with no body. MUST provide a body.
+
+### Member `ConcurrentMethod`
+
+* Declaration has `{:concurrent}` attribute. MUST manually review and test in a concurrent setting.

Test/auditor/TestAuditor.dfy.html.expect

@@ -47,6 +47,7 @@
 <tr><td>DoesNotTerminate</td><td>True</td><td>False</td><td>False</td><td>Method may not terminate (uses <code>decreases *</code>).</td><td>Provide a valid <code>decreases</code> clause.</td></tr>
 <tr><td>ForallWithoutBody</td><td>False</td><td>False</td><td>False</td><td>Definition contains <code>forall</code> statement with no body.</td><td>Provide a body.</td></tr>
 <tr><td>LoopWithoutBody</td><td>True</td><td>False</td><td>False</td><td>Definition contains loop with no body.</td><td>Provide a body.</td></tr>
+<tr><td>ConcurrentMethod</td><td>True</td><td>False</td><td>False</td><td>Declaration has <code>{:concurrent}</code> attribute.</td><td>Manually review and test in a concurrent setting.</td></tr>
 </table>
 <script>$( "table" ).last().addClass( "sortable" );</script>
 </body>

Test/auditor/TestAuditor.dfy.md.expect

@@ -13,4 +13,5 @@
 | GenerateBytesNoGuarantee | True | False | True | Declaration with `{:extern}` has a requires clause. | Test external caller (maybe with `/testContracts`). |
 | DoesNotTerminate | True | False | False | Method may not terminate (uses `decreases *`). | Provide a valid `decreases` clause. |
 | ForallWithoutBody | False | False | False | Definition contains `forall` statement with no body. | Provide a body. |
-| LoopWithoutBody | True | False | False | Definition contains loop with no body. | Provide a body. |
+| LoopWithoutBody | True | False | False | Definition contains loop with no body. | Provide a body. |
+| ConcurrentMethod | True | False | False | Declaration has `{:concurrent}` attribute. | Manually review and test in a concurrent setting. |

docs/DafnyRef/UserGuide.md

@@ -370,6 +370,49 @@ The command emits exit codes of
 
 It also takes the `--verbose` option, which then gives information about the files being formatted.
 
+The `dafny audit` command currently reports the following:
+
+* Any declaration marked with the `{:axiom}` attribute.
+This is typically used to mark that a lemma with no body (and is therefore assumed to always be true) is intended as an axiom.
+The key purpose of the `audit` command is to ensure that all assumptions are intentional and acknowledged.
+To improve assurance, however, try to provide a proof.
+
+* Any declaration marked with the `{:verify false}` attribute, which tells the verifier to skip verifying this declaration.
+Removing the attribute and providing a proof will improve assurance.
+
+* Any declaration marked with the `{:extern}` attribute that has at least one `requires` or `ensures` clause.
+If code implemented externally, and called from Dafny, has an `ensures` clause, Dafny assumes that it satisfies that clause.
+Since Dafny cannot prove properties about code written in other languages,
+adding tests to provide evidence that any `ensures` clauses do hold can improve assurance.
+The same considerations apply to `requires` clauses on Dafny code intended to be called from external code.
+
+* Any declaration marked with the `{:concurrent}` attribute.
+This is intended to indicate that the code is safe for use in a concurrent setting, but Dafny currently cannot prove that form of safety.
+The [addition of `reads` clauses to methods](https://github.com/dafny-lang/rfcs/pull/6) will be a step toward being able to prove safety in this case,
+but until it exists, careful inspection and testing are appropriate.
+
+* Any definition with an `assume` statement in its body.
+To improve assurance, attempt to convert it to an `assert` statement and prove that it holds.
+Such a definition will not be compilable unless the statement is also marked with `{:axiom}`.
+Alternatively, converting it to an `expect` statement will cause it to be checked at runtime.
+
+* Any method marked with `decreases *`.
+Such a method may not terminate.
+Although this cannot cause an unsound proof, in the logic of Dafny,
+it's generally important that any non-termination be intentional.
+
+* Any `forall` statement without a body.
+This is equivalent to an assumption of its conclusion.
+To improve assurance, provide a body that proves the conclusion.
+
+* Any loop without a body.
+This is equivalent to an assumption of any loop invariants in the code after the loop.
+To improve assurance, provide a body that establishes any stated invariants.
+
+* Any declaration with no body and at least one `ensures` clause.
+Any code that calls this declaration will assume that all `ensures` clauses are true after it returns.
+To improve assurance, provide a body that proves that any `ensures` clauses hold.
+
 #### 13.5.1.9. `dafny format` {#sec-dafny-format}
 
 Dafny supports a formatter, which for now only changes the indentation of lines in a Dafny file, so that it conforms

docs/dev/news/3660.feat

@@ -0,0 +1 @@
+The `dafny audit` command now reports instances of the `{:concurrent}` attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting.