New attempt at fixing CI

Source/DafnyCore/Backends/Dafny/AST.dfy

@@ -205,5 +205,12 @@ module {:extern "DAST"} DAST {
 
  datatype UnaryOp = Not | BitwiseNot | Cardinality
 
- datatype Literal = BoolLiteral(bool) | IntLiteral(string, Type) | DecLiteral(string, string, Type) | StringLiteral(string) | CharLiteral(char) | Null(Type)
+ datatype Literal =
+ | BoolLiteral(bool)
+ | IntLiteral(string, Type)
+ | DecLiteral(string, string, Type)
+ | StringLiteral(string, verbatim: bool)
+ | CharLiteral(char)
+ | CharLiteralUTF16(nat)
+ | Null(Type)
 }

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -1312,14 +1312,29 @@ private class ExprLvalue : ILvalue {
  switch (e) {
  case CharLiteralExpr c:
  var codePoint = Util.UnescapedCharacters(Options, (string)c.Value, false).Single();
- baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_CharLiteral(
- new Rune(codePoint)
- ));
+ if (Rune.IsRune(new BigInteger(codePoint))) { // More readable version in the generated code.
+ baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_CharLiteral(
+ new Rune(codePoint)
+ ));
+ } else {
+ baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_CharLiteralUTF16(
+ codePoint
+ ));
+ }
+
  break;
  case StringLiteralExpr str:
- baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_StringLiteral(
- Sequence<Rune>.UnicodeFromString(str.AsStringLiteral())
- ));
+ if (!UnicodeCharEnabled && Util.TokensWithEscapes(str.AsStringLiteral(), false) is var tokens && tokens.Any((string token) => Util.Utf16Escape.IsMatch(token))) {
+ var s = Util.UnescapedCharacters(UnicodeCharEnabled, str.AsStringLiteral(), true);
+ var chars = tokens.Select((string singleChar) =>
+ ConvertExpressionNoStatement(new CharLiteralExpr(Token.NoToken, singleChar) {Type = Type.Char})).ToArray();
+ baseExpr = (DAST.Expression)DAST.Expression.create_SeqValue(Sequence<DAST.Expression>.FromArray(chars), GenType(new CharType()));
+ // We need to emit a sequence of chars literal. We first 
+ } else {
+ baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_StringLiteral(
+ Sequence<Rune>.UnicodeFromString(str.AsStringLiteral()), str.IsVerbatim
+ ));
+ }
  break;
  case StaticReceiverExpr:
  if (e.Type.NormalizeExpandKeepConstraints() is UserDefinedType udt && udt.ResolvedClass is DatatypeDecl dt &&

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-coverage.dfy

@@ -53,7 +53,8 @@ module DafnyToRustCompilerCoverage {
  TestNoOptimize(StmtExpr(BinaryOp("&&", x, x, BinaryOpFormat.NoFormat), x));
  TestNoOptimize(StmtExpr(TypeAscription(x, I128), x));
  TestNoOptimize(StmtExpr(LiteralInt("1"), x));
- TestNoOptimize(StmtExpr(LiteralString("1", true), x));
+ TestNoOptimize(StmtExpr(LiteralString("2", true, false), x));
+ TestNoOptimize(StmtExpr(LiteralString("3", false, true), x));
  AssertCoverage(StmtExpr(DeclareVar(MUT, "z", Some(I128), None), StmtExpr(AssignVar("z", y), RawExpr("return"))).Optimize()
  == StmtExpr(DeclareVar(MUT, "z", Some(I128), Some(y)), RawExpr("return")));
 
@@ -70,8 +71,8 @@ module DafnyToRustCompilerCoverage {
  BinaryOp("+", Identifier("x"), Identifier("y"), BinaryOpFormat.NoFormat),
  TypeAscription(Identifier("x"), I128),
  LiteralInt("322"),
- LiteralString("abc", true),
- LiteralString("abc", false),
+ LiteralString("abc", true, false),
+ LiteralString("abc", false, true),
  DeclareVar(MUT, "abc", Some(I128), None),
  DeclareVar(CONST, "abc", None, Some(Identifier("x"))),
  AssignVar("abc", Identifier("x")),
@@ -117,7 +118,7 @@ module DafnyToRustCompilerCoverage {
  AssertCoverage(RawExpr("x").printingInfo.UnknownPrecedence?);
  AssertCoverage(x.printingInfo == Precedence(1));
  AssertCoverage(LiteralInt("3").printingInfo == Precedence(1));
- AssertCoverage(LiteralString("abc", true).printingInfo == Precedence(1));
+ AssertCoverage(LiteralString("abc", true, false).printingInfo == Precedence(1));
  AssertCoverage(UnaryOp("?", x, UnaryOpFormat.NoFormat).printingInfo == SuffixPrecedence(5));
  AssertCoverage(UnaryOp("-", x, UnaryOpFormat.NoFormat).printingInfo == Precedence(6));
  AssertCoverage(UnaryOp("*", x, UnaryOpFormat.NoFormat).printingInfo == Precedence(6));

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

@@ -539,7 +539,7 @@ module RAST
  | TypeAscription(left: Expr, tpe: Type) // underlying as tpe
  | LiteralInt(value: string)
  | LiteralBool(bvalue: bool)
- | LiteralString(value: string, binary: bool)
+ | LiteralString(value: string, binary: bool, verbatim: bool)
  | DeclareVar(declareType: DeclareType, name: string, optType: Option<Type>, optRhs: Option<Expr>) // let mut name: optType = optRhs;
  | Assign(names: Option<AssignLhs>, rhs: Expr) // name1, name2 = rhs;
  | IfExpr(cond: Expr, thn: Expr, els: Expr) // if cond { thn } else { els }
@@ -567,7 +567,7 @@ module RAST
  case Identifier(_) => Precedence(1)
  case LiteralInt(_) => Precedence(1)
  case LiteralBool(_) => Precedence(1)
- case LiteralString(_, _) => Precedence(1)
+ case LiteralString(_, _, _) => Precedence(1)
  // Paths => Precedence(1)
  // Method call => Precedence(2)
  // Field expression => PrecedenceAssociativity(3, LeftToRight)
@@ -610,7 +610,7 @@ module RAST
  case ExprFromType(_) => 1
  case LiteralInt(_) => 1
  case LiteralBool(_) => 1
- case LiteralString(_, _) => 1
+ case LiteralString(_, _, _) => 1
  case Match(matchee, cases) =>
  1 + max(matchee.Height(),
  SeqToHeight(cases, (oneCase: MatchCase)
@@ -732,7 +732,7 @@ module RAST
  if |args| == 1 && (base == dafny_runtime || base == global) then
  match args[0] {
  case LiteralInt(number) => LiteralInt(number)
- case LiteralString(number, _) => LiteralInt(number)
+ case LiteralString(number, _, _) => LiteralInt(number)
  case _ => this
  }
  else this
@@ -790,6 +790,18 @@ module RAST
  }
  }
 
+ static function MaxHashes(s: string, currentHashes: string, mostHashes: string): string {
+ if |s| == 0 then if |currentHashes| < |mostHashes| then mostHashes else currentHashes else
+ if s[0..1] == "#" then MaxHashes(s[1..], currentHashes + "#", mostHashes)
+ else MaxHashes(s[1..], "", if |currentHashes| < |mostHashes| then mostHashes else currentHashes)
+ }
+
+ static function RemoveDoubleQuotes(s: string): string {
+ if |s| <= 1 then s else
+ if s[0..2] == @"""""" then @"""" + RemoveDoubleQuotes(s[2..]) else
+ s[0..1] + RemoveDoubleQuotes(s[1..])
+ }
+
  function ToString(ind: string): string
  decreases Height()
  {
@@ -798,9 +810,10 @@ module RAST
  case ExprFromType(t) => t.ToString(ind)
  case LiteralInt(number) => number
  case LiteralBool(b) => if b then "true" else "false"
- case LiteralString(characters, binary) =>
- (if binary then "b" else "") +
- "\"" + characters + "\""
+ case LiteralString(characters, binary, verbatim) =>
+ var hashes := if verbatim then MaxHashes(characters, "", "") + "#" else "";
+ (if binary then "b" else "") + (if verbatim then "r" + hashes else "") +
+ "\"" + (if verbatim then RemoveDoubleQuotes(characters) else characters) + "\"" + hashes
  case Match(matchee, cases) =>
  "match " + matchee.ToString(ind + IND) + " {" +
  SeqToString(cases,
@@ -2483,13 +2496,13 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
  newEnv := env;
  }
  case Halt() => {
- generated := R.Identifier("panic!").Apply1(R.LiteralString("Halt", false));
+ generated := R.Identifier("panic!").Apply1(R.LiteralString("Halt", false, false));
  readIdents := {};
  newEnv := env;
  }
  case Print(e) => {
  var printedExpr, recOwnership, recIdents := GenExpr(e, selfIdent, env, OwnershipBorrowed);
- generated := R.Identifier("print!").Apply([R.LiteralString("{}", false),
+ generated := R.Identifier("print!").Apply([R.LiteralString("{}", false, false),
  R.dafny_runtime.MSel("DafnyPrintWrapper").Apply1(printedExpr)]);
  readIdents := recIdents;
  newEnv := env;
@@ -2609,6 +2622,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
  expectedOwnership: Ownership
  ) returns (r: R.Expr, resultingOwnership: Ownership, readIdents: set<string>)
  requires e.Literal?
+ modifies this
  ensures OwnershipGuarantee(expectedOwnership, resultingOwnership)
  decreases e, 0
  {
@@ -2626,7 +2640,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
  r := R.dafny_runtime.MSel("int!").Apply1(R.LiteralInt(i));
  } else {
  r := R.dafny_runtime.MSel("int!").Apply1(
- R.LiteralString(i, binary := true));
+ R.LiteralString(i, binary := true, verbatim := false));
  }
  }
  case o => {
@@ -2653,8 +2667,19 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
  readIdents := {};
  return;
  }
- case Literal(StringLiteral(l)) => {
- r := R.dafny_runtime.MSel(string_of).Apply1(R.LiteralString(l, false));
+ case Literal(StringLiteral(l, verbatim)) => {
+ if verbatim {
+ error := Some("Verbatim strings prefixed by @ not supported yet.");
+ }
+ r := R.dafny_runtime.MSel(string_of).Apply1(R.LiteralString(l, binary := false, verbatim := verbatim));
+ r, resultingOwnership := FromOwned(r, expectedOwnership);
+ readIdents := {};
+ return;
+ }
+ case Literal(CharLiteralUTF16(c)) => {
+ r := R.LiteralInt(Strings.OfNat(c));
+ r := R.TypeAscription(r, R.U16);
+ r := R.dafny_runtime.MSel(DafnyChar).Apply1(r);
  r, resultingOwnership := FromOwned(r, expectedOwnership);
  readIdents := {};
  return;

Source/DafnyCore/GeneratedFromDafny/DAST.cs

@@ -7153,6 +7153,7 @@ public interface _ILiteral {
  bool is_DecLiteral { get; }
  bool is_StringLiteral { get; }
  bool is_CharLiteral { get; }
+ bool is_CharLiteralUTF16 { get; }
  bool is_Null { get; }
  bool dtor_BoolLiteral_a0 { get; }
  Dafny.ISequence<Dafny.Rune> dtor_IntLiteral_a0 { get; }
@@ -7161,7 +7162,9 @@ public interface _ILiteral {
  Dafny.ISequence<Dafny.Rune> dtor_DecLiteral_a1 { get; }
  DAST._IType dtor_DecLiteral_a2 { get; }
  Dafny.ISequence<Dafny.Rune> dtor_StringLiteral_a0 { get; }
+ bool dtor_verbatim { get; }
  Dafny.Rune dtor_CharLiteral_a0 { get; }
+ BigInteger dtor_CharLiteralUTF16_a0 { get; }
  DAST._IType dtor_Null_a0 { get; }
  _ILiteral DowncastClone();
  }
@@ -7185,12 +7188,15 @@ public abstract class Literal : _ILiteral {
  public static _ILiteral create_DecLiteral(Dafny.ISequence<Dafny.Rune> _a0, Dafny.ISequence<Dafny.Rune> _a1, DAST._IType _a2) {
  return new Literal_DecLiteral(_a0, _a1, _a2);
  }
- public static _ILiteral create_StringLiteral(Dafny.ISequence<Dafny.Rune> _a0) {
- return new Literal_StringLiteral(_a0);
+ public static _ILiteral create_StringLiteral(Dafny.ISequence<Dafny.Rune> _a0, bool verbatim) {
+ return new Literal_StringLiteral(_a0, verbatim);
  }
  public static _ILiteral create_CharLiteral(Dafny.Rune _a0) {
  return new Literal_CharLiteral(_a0);
  }
+ public static _ILiteral create_CharLiteralUTF16(BigInteger _a0) {
+ return new Literal_CharLiteralUTF16(_a0);
+ }
  public static _ILiteral create_Null(DAST._IType _a0) {
  return new Literal_Null(_a0);
  }
@@ -7199,6 +7205,7 @@ public abstract class Literal : _ILiteral {
  public bool is_DecLiteral { get { return this is Literal_DecLiteral; } }
  public bool is_StringLiteral { get { return this is Literal_StringLiteral; } }
  public bool is_CharLiteral { get { return this is Literal_CharLiteral; } }
+ public bool is_CharLiteralUTF16 { get { return this is Literal_CharLiteralUTF16; } }
  public bool is_Null { get { return this is Literal_Null; } }
  public bool dtor_BoolLiteral_a0 {
  get {
@@ -7242,12 +7249,24 @@ public abstract class Literal : _ILiteral {
  return ((Literal_StringLiteral)d)._a0;
  }
  }
+ public bool dtor_verbatim {
+ get {
+ var d = this;
+ return ((Literal_StringLiteral)d)._verbatim;
+ }
+ }
  public Dafny.Rune dtor_CharLiteral_a0 {
  get {
  var d = this;
  return ((Literal_CharLiteral)d)._a0;
  }
  }
+ public BigInteger dtor_CharLiteralUTF16_a0 {
+ get {
+ var d = this;
+ return ((Literal_CharLiteralUTF16)d)._a0;
+ }
+ }
  public DAST._IType dtor_Null_a0 {
  get {
  var d = this;
@@ -7354,27 +7373,32 @@ public class Literal_DecLiteral : Literal {
  }
  public class Literal_StringLiteral : Literal {
  public readonly Dafny.ISequence<Dafny.Rune> _a0;
- public Literal_StringLiteral(Dafny.ISequence<Dafny.Rune> _a0) : base() {
+ public readonly bool _verbatim;
+ public Literal_StringLiteral(Dafny.ISequence<Dafny.Rune> _a0, bool verbatim) : base() {
  this._a0 = _a0;
+ this._verbatim = verbatim;
  }
  public override _ILiteral DowncastClone() {
  if (this is _ILiteral dt) { return dt; }
- return new Literal_StringLiteral(_a0);
+ return new Literal_StringLiteral(_a0, _verbatim);
  }
  public override bool Equals(object other) {
  var oth = other as DAST.Literal_StringLiteral;
- return oth != null && object.Equals(this._a0, oth._a0);
+ return oth != null && object.Equals(this._a0, oth._a0) && this._verbatim == oth._verbatim;
  }
  public override int GetHashCode() {
  ulong hash = 5381;
  hash = ((hash << 5) + hash) + 3;
  hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._a0));
+ hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._verbatim));
  return (int) hash;
  }
  public override string ToString() {
  string s = "DAST.Literal.StringLiteral";
  s += "(";
  s += this._a0.ToVerbatimString(true);
+ s += ", ";
+ s += Dafny.Helpers.ToString(this._verbatim);
  s += ")";
  return s;
  }
@@ -7406,6 +7430,33 @@ public class Literal_CharLiteral : Literal {
  return s;
  }
  }
+ public class Literal_CharLiteralUTF16 : Literal {
+ public readonly BigInteger _a0;
+ public Literal_CharLiteralUTF16(BigInteger _a0) : base() {
+ this._a0 = _a0;
+ }
+ public override _ILiteral DowncastClone() {
+ if (this is _ILiteral dt) { return dt; }
+ return new Literal_CharLiteralUTF16(_a0);
+ }
+ public override bool Equals(object other) {
+ var oth = other as DAST.Literal_CharLiteralUTF16;
+ return oth != null && this._a0 == oth._a0;
+ }
+ public override int GetHashCode() {
+ ulong hash = 5381;
+ hash = ((hash << 5) + hash) + 5;
+ hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._a0));
+ return (int) hash;
+ }
+ public override string ToString() {
+ string s = "DAST.Literal.CharLiteralUTF16";
+ s += "(";
+ s += Dafny.Helpers.ToString(this._a0);
+ s += ")";
+ return s;
+ }
+ }
  public class Literal_Null : Literal {
  public readonly DAST._IType _a0;
  public Literal_Null(DAST._IType _a0) : base() {
@@ -7421,7 +7472,7 @@ public class Literal_Null : Literal {
  }
  public override int GetHashCode() {
  ulong hash = 5381;
- hash = ((hash << 5) + hash) + 5;
+ hash = ((hash << 5) + hash) + 6;
  hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._a0));
  return (int) hash;
  }