Merge branch 'master' into supportAllOptionTypesInProjectFile

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -46,10 +46,11 @@ module {:extern "DAST"} DAST {
  DeclareVar(name: string, typ: Type, maybeValue: Optional<Expression>) |
  Assign(lhs: AssignLhs, value: Expression) |
  If(cond: Expression, thn: seq<Statement>, els: seq<Statement>) |
- While(cond: Expression, body: seq<Statement>) |
+ While(lbl: Optional<string>, cond: Expression, body: seq<Statement>) |
  Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Optional<seq<Ident>>) |
  Return(expr: Expression) |
  EarlyReturn() |
+ Break(toLabel: Optional<string>) |
  TailRecursive(body: seq<Statement>) |
  JumpTailCallStart() |
  Halt() |

Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs

@@ -377,7 +377,7 @@ interface StatementContainer {
  }
 
  public WhileBuilder While() {
- var ret = new WhileBuilder();
+ var ret = new WhileBuilder(null);
  AddBuildable(ret);
  return ret;
  }
@@ -399,6 +399,10 @@ interface StatementContainer {
  AddBuildable(ret);
  return ret;
  }
+
+ public LabeledBuilder Labeled(string label) {
+ return new LabeledBuilder(label, this);
+ }
  }
 
  interface BuildableStatement {
@@ -597,10 +601,13 @@ class ElseBuilder : StatementContainer {
  }
 
  class WhileBuilder : ExprContainer, StatementContainer, BuildableStatement {
+ readonly string label;
  object condition = null;
  readonly List<object> body = new();
 
- public WhileBuilder() { }
+ public WhileBuilder(string label) {
+ this.label = label;
+ }
 
  public void AddExpr(DAST.Expression value) {
  if (condition != null) {
@@ -640,6 +647,7 @@ class WhileBuilder : ExprContainer, StatementContainer, BuildableStatement {
  StatementContainer.RecursivelyBuild(body, builtStatements);
 
  return (DAST.Statement)DAST.Statement.create_While(
+ label == null ? Optional<ISequence<Rune>>.create_None() : Optional<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString(label)),
  builtCondition[0],
  Sequence<DAST.Statement>.FromArray(builtStatements.ToArray())
  );
@@ -770,6 +778,38 @@ class ReturnBuilder : ExprContainer, BuildableStatement {
  }
  }
 
+ class LabeledBuilder : StatementContainer {
+ readonly string label;
+ readonly StatementContainer parent;
+
+ public LabeledBuilder(string label, StatementContainer parent) {
+ this.label = label;
+ this.parent = parent;
+ }
+
+ public void AddStatement(DAST.Statement item) {
+ parent.AddStatement(item);
+ }
+
+ public void AddBuildable(BuildableStatement item) {
+ parent.AddBuildable(item);
+ }
+
+ public StatementContainer Fork() {
+ return null;
+ }
+
+ public List<object> ForkList() {
+ throw new InvalidOperationException();
+ }
+
+ public WhileBuilder While() {
+ var ret = new WhileBuilder(label);
+ parent.AddBuildable(ret);
+ return ret;
+ }
+ }
+
  class StatementBuffer : StatementContainer {
  readonly List<object> statements = new();
 

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -877,11 +877,26 @@ private class ExprLvalue : ILvalue {
  }
 
  protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) {
- throw new NotImplementedException();
+ if (createContinueLabel) {
+ return wr;
+ }
+
+ if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
+ var labelBuilder = stmtContainer.Builder.Labeled(label);
+ return new BuilderSyntaxTree<StatementContainer>(labelBuilder);
+ } else {
+ throw new InvalidOperationException();
+ }
  }
 
  protected override void EmitBreak(string label, ConcreteSyntaxTree wr) {
- throw new NotImplementedException();
+ if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
+ stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_Break(
+ label == null ? Optional<ISequence<Rune>>.create_None() : Optional<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString(label))
+ ));
+ } else {
+ throw new InvalidOperationException();
+ }
  }
 
  protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {

Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy

@@ -809,7 +809,7 @@ module {:extern "DCOMP"} DCOMP {
  readIdents := readIdents + elsIdents;
  generated := "if " + condString + " {\n" + thnString + "\n} else {\n" + elsString + "\n}";
  }
- case While(cond, body) => {
+ case While(lbl, cond, body) => {
  var condString, _, condErased, recIdents := GenExpr(cond, selfIdent, params, true);
  if !condErased {
  condString := "::dafny_runtime::DafnyErasable::erase(" + condString + ")";
@@ -818,7 +818,27 @@ module {:extern "DCOMP"} DCOMP {
  readIdents := recIdents;
  var bodyString, bodyIdents := GenStmts(body, selfIdent, params, false, earlyReturn);
  readIdents := readIdents + bodyIdents;
- generated := "while " + condString + " {\n" + bodyString + "\n}";
+
+ var lblString := "";
+ match lbl {
+ case Some(id) => {
+ lblString := "'label_" + id + ": ";
+ }
+ case None => {}
+ }
+
+ generated := lblString + "while " + condString + " {\n" + bodyString + "\n}";
+ }
+ case Break(toLabel) => {
+ match toLabel {
+ case Some(lbl) => {
+ generated := "break 'label_" + lbl + ";";
+ }
+ case None => {
+ generated := "break;";
+ }
+ }
+ readIdents := {};
  }
  case TailRecursive(body) => {
  // clone the parameters to make them mutable

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -3301,7 +3301,9 @@ public class CheckHasNoAssumes_Visitor : BottomUpVisitor {
  // emit a loop structure. The structure "while (false) { }" comes to mind, but that results in
  // an "unreachable code" error from Java, so we instead use "while (true) { break; }".
  var wBody = CreateWhileLoop(out var guardWriter, wr);
- guardWriter.Write(True);
+ EmitExpr(new LiteralExpr(null, true) {
+ Type = Type.Bool
+ }, false, guardWriter, wStmts);
  EmitBreak(null, wBody);
  Coverage.UnusedInstrumentationPoint(s.Body.Tok, "while body");
  } else {
@@ -3315,7 +3317,9 @@ public class CheckHasNoAssumes_Visitor : BottomUpVisitor {
  }
  if (loopStmt.Alternatives.Count != 0) {
  var w = CreateWhileLoop(out var whileGuardWriter, wr);
- whileGuardWriter.Write(True);
+ EmitExpr(new LiteralExpr(null, true) {
+ Type = Type.Bool
+ }, false, whileGuardWriter, wStmts);
  w = EmitContinueLabel(loopStmt.Labels, w);
  foreach (var alternative in loopStmt.Alternatives) {
  var thn = EmitIf(out var guardWriter, true, w);