Skip to content

Commit

Permalink
Merge branch 'master' into triggers-for-such-that
Browse files Browse the repository at this point in the history 
# Conflicts:
#	Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
  • Loading branch information
@RustanLeino
RustanLeino committed Feb 3, 2025
2 parents ba6eef4 + 5cd765a commit d5e0040
Show file tree
Hide file tree
Showing 281 changed files with 2,147 additions and 1,531 deletions.
6 changes: 3 additions & 3 deletions Source/AutoExtern/AutoProgram.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,7 @@ private bool IsSkippedBaseType(BaseTypeSyntax bt) {
syntax.BaseList?.Types
.Where(bt => !IsSkippedBaseType(bt))
.Select(bt => new Type(bt.Type, model))
?? Enumerable.Empty<Type>();
?? [];

public override void Pp(TextWriter wr, string indent) {
var baseTypes = BaseTypes.ToList();
Expand Down Expand Up @@ -388,8 +388,8 @@ public override void Pp(TextWriter wr, string indent) {
internal class Name {
private const string EscapePrefix = "CSharp_";

private static readonly List<string> DisallowedNameWords = new List<string>
{"type", "ORDINAL", "Keys", "Values", "Items", "IsLimit", "IsSucc", "Offset", "IsNat"};
private static readonly List<string> DisallowedNameWords =
["type", "ORDINAL", "Keys", "Values", "Items", "IsLimit", "IsSucc", "Offset", "IsNat"];
private static readonly Regex DisallowedNameRe =
new Regex($"^(_|({String.Join("|", DisallowedNameWords)})$)");

Expand Down
10 changes: 5 additions & 5 deletions Source/DafnyCore.Test/ClonerTest.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,11 @@ public void ClonerKeepsBodyStartTok() {
IsTypeExplicit = false
};
var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
false, false, new List<TypeParameter>(), new List<Formal> { formal1, formal2 },
new List<Formal>(), new List<AttributedExpression>(),
new Specification<FrameExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null),
new List<AttributedExpression>(), new Specification<Expression>(new List<Expression>(), null),
new BlockStmt(rangeToken, new List<Statement>()), null, Token.NoToken, false);
false, false, [], [formal1, formal2],
[], [],
new Specification<FrameExpression>(), new Specification<FrameExpression>([], null),
[], new Specification<Expression>([], null),
new BlockStmt(rangeToken, []), null, Token.NoToken, false);

dummyDecl.BodyStartTok = tokenBodyStart;
var cloner = new Cloner();
Expand Down
131 changes: 131 additions & 0 deletions Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,14 +20,142 @@ public static void AssertCoverage(bool x)
if (!(x)) {
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(26,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
}
public static void AssertEq<__T>(__T x, __T y)
{
if (!(object.Equals(x, y))) {
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(30,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
}
public static void TestExpr()
{
RASTCoverage.__default.TestOptimizeToString();
RASTCoverage.__default.TestPrintingInfo();
RASTCoverage.__default.TestNoExtraSemicolonAfter();
RASTCoverage.__default.TestDocstring();
}
public static Dafny.ISequence<Dafny.Rune> CanonicalNewlines(Dafny.ISequence<Dafny.Rune> s) {
Dafny.ISequence<Dafny.Rune> _0___accumulator = Dafny.Sequence<Dafny.Rune>.FromElements();
TAIL_CALL_START: ;
if ((new BigInteger((s).Count)).Sign == 0) {
return Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
} else if (((s).Select(BigInteger.Zero)) == (new Dafny.Rune('\r'))) {
if (((new BigInteger((s).Count)) > (BigInteger.One)) && (((s).Select(BigInteger.One)) == (new Dafny.Rune('\n')))) {
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
Dafny.ISequence<Dafny.Rune> _in0 = (s).Drop(new BigInteger(2));
s = _in0;
goto TAIL_CALL_START;
} else {
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
Dafny.ISequence<Dafny.Rune> _in1 = (s).Drop(BigInteger.One);
s = _in1;
goto TAIL_CALL_START;
}
} else {
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, (s).Take(BigInteger.One));
Dafny.ISequence<Dafny.Rune> _in2 = (s).Drop(BigInteger.One);
s = _in2;
goto TAIL_CALL_START;
}
}
public static void TestOneDocstring(Dafny.ISequence<Dafny.Rune> dafnyDocstring, Dafny.ISequence<Dafny.Rune> rustDocstring, Dafny.ISequence<Dafny.Rune> indent)
{
RASTCoverage.__default.AssertEq<Dafny.ISequence<Dafny.Rune>>(RAST.__default.ConvertDocstring(RASTCoverage.__default.CanonicalNewlines(dafnyDocstring), indent, true, Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_None()), RASTCoverage.__default.CanonicalNewlines(rustDocstring));
}
public static void TestDocstring()
{
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Hello
World"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Hello
/// World"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
```rs
let mut x = 1;
```
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// ```
/// let mut x = 1;
/// ```
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
`````rs
let mut x = 1;
`````
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// `````
/// let mut x = 1;
/// `````
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
```
var x := 1;
```
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// ```dafny
/// var x := 1;
/// ```
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
`````
var x := 1;
`````
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// `````dafny
/// var x := 1;
/// `````
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
`````md
# title
```
code
```
Outside of code
`````
```
dafnycode
```
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// `````md
/// # title
/// ```
/// code
/// ```
/// Outside of code
/// `````
/// ```dafny
/// dafnycode
/// ```
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
Indented code
More indented code
Back to normal
Normal as well
Also normal
But this one indented"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// | Indented code
/// | More indented code
/// Back to normal
/// Normal as well
/// Also normal
/// | But this one indented"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
}
public static void TestNoOptimize(RAST._IExpr e)
{
if (!(object.Equals((RASTCoverage.__default.ExprSimp).ReplaceExpr(e), e))) {
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(157,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
}
public static RAST._IExpr ConversionNum(RAST._IType t, RAST._IExpr x)
{
Expand Down Expand Up @@ -161,5 +289,8 @@ public static void TestNoExtraSemicolonAfter()
RASTCoverage.__default.AssertCoverage((RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x"), Std.Wrappers.Option<RAST._IType>.create_None(), Std.Wrappers.Option<RAST._IExpr>.create_None())).NoExtraSemicolonAfter());
RASTCoverage.__default.AssertCoverage(!((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x"))).NoExtraSemicolonAfter()));
}
public static RAST._IRASTBottomUpReplacer ExprSimp { get {
return ExpressionOptimization.__default.ExprSimplifier();
} }
}
} // end of namespace RASTCoverage
2 changes: 1 addition & 1 deletion Source/DafnyCore.Test/NodeTests.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ public class NodeTests {
class ConcreteNode : Node {
public ConcreteNode(IOrigin origin, IEnumerable<INode>? children = null) {
Origin = origin;
Children = children ?? Enumerable.Empty<INode>();
Children = children ?? [];
}

public override IOrigin Origin { get; }
Expand Down
56 changes: 49 additions & 7 deletions Source/DafnyCore/AST/Attributes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ public static List<List<Expression>> FindAllExpressions(Attributes attrs, string
List<List<Expression>> ret = null;
for (; attrs != null; attrs = attrs.Prev) {
if (attrs.Name == nm) {
ret = ret ?? new List<List<Expression>>(); // Avoid allocating the list in the common case where we don't find nm
ret = ret ?? []; // Avoid allocating the list in the common case where we don't find nm
ret.Add(attrs.Args);
}
}
Expand Down Expand Up @@ -280,7 +280,7 @@ public static void SetIndents(Attributes attrs, int indentBefore, TokenNewIndent
// Helper to create a built-in @-attribute
static BuiltInAtAttributeSyntax BuiltIn(string name) {
return new BuiltInAtAttributeSyntax(
name, new List<BuiltInAtAttributeArgSyntax>(), _ => true);
name, [], _ => true);
}

// Helper to create an old-style attribute
Expand Down Expand Up @@ -330,7 +330,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
atAttribute.Arg.Type = Type.Int; // Dummy type to avoid crashes
var intDecl = resolver.SystemModuleManager.valuetypeDecls.First(valueTypeDecl => valueTypeDecl.Name == PreType.TypeNameInt);

atAttribute.Arg.PreType = new DPreType(intDecl, new List<PreType>(), null);
atAttribute.Arg.PreType = new DPreType(intDecl, [], null);

switch (name) {
case "AssumeCrossModuleTermination": {
Expand Down Expand Up @@ -480,101 +480,143 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
// List of built-in @-attributes with their definitions.
// This list could be obtained from parsing and resolving a .Dfy file
// but for now it's good enough.
public static readonly List<BuiltInAtAttributeSyntax> BuiltinAtAttributes = new() {
public static readonly List<BuiltInAtAttributeSyntax> BuiltinAtAttributes = [
BuiltIn("AssumeCrossModuleTermination")
.Filter(attributeHost => attributeHost is ClassDecl or TraitDecl),

BuiltIn("AutoContracts")
.Filter(attributeHost => attributeHost is ClassDecl),

BuiltIn("AutoRequires")
.Filter(attributeHost => attributeHost is Function),

BuiltIn("AutoRevealDependenciesAll").WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
.Filter(attributeHost => attributeHost is MethodOrFunction),

BuiltIn("AutoRevealDependencies").WithArg("level", Type.Int)
.Filter(attributeHost => attributeHost is MethodOrFunction),

BuiltIn("Axiom")
.Filter(attributeHost => attributeHost is MethodOrFunction),

BuiltIn("Compile")
.WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
.Filter(attributeHost =>
attributeHost is TopLevelDecl and not TypeParameter or MemberDecl or ModuleDefinition),

BuiltIn("Concurrent")
.Filter(attributeHost =>
attributeHost is MethodOrFunction),

BuiltIn("DisableNonlinearArithmetic")
.WithArg("disable", Type.Bool, DefaultBool(true))
.Filter(attributeHost =>
attributeHost is ModuleDefinition),

BuiltIn("Fuel")
.WithArg("low", Type.Int, DefaultInt(1))
.WithArg("high", Type.Int, DefaultInt(2))
.WithArg("functionName", Type.ResolvedString(), DefaultString(""))
.Filter(attributeHost => attributeHost is MethodOrFunction or AssertStmt),

BuiltIn("IsolateAssertions")
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("NativeUInt8")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeInt8")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeUInt16")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeInt16")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeUInt32")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeInt32")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeInt53")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeUInt64")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeInt64")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeUInt128")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeInt128")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeInt")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeNone")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("NativeIntOrReal")
.Filter(attributeHost => attributeHost is NewtypeDecl),

BuiltIn("Options")
.WithArg(TupleItem0Name, Type.ResolvedString())
.Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition),

BuiltIn("Print")
.Filter(attributeHost => attributeHost is Method),

BuiltIn("Priority").WithArg(TupleItem0Name, Type.Int)
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("ResourceLimit").WithArg(TupleItem0Name, Type.ResolvedString())
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("Synthesize")
.Filter(attributeHost => attributeHost is Method),

BuiltIn("TimeLimit").WithArg(TupleItem0Name, Type.Int)
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("TimeLimitMultiplier").WithArg(TupleItem0Name, Type.Int)
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("TailRecursion")
.Filter(attributeHost => attributeHost is MethodOrFunction),

BuiltIn("Test")
.Filter(attributeHost => attributeHost is MethodOrFunction),

BuiltIn("TestEntry")
.Filter(attributeHost => attributeHost is MethodOrFunction),

BuiltIn("TestInline").WithArg("level", Type.Int, DefaultInt(1))
.Filter(attributeHost => attributeHost is MethodOrFunction),

BuiltIn("Transparent")
.Filter(attributeHost => attributeHost is Function),

BuiltIn("VcsMaxCost").WithArg(TupleItem0Name, Type.Int)
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("VcsMaxKeepGoingSplits").WithArg(TupleItem0Name, Type.Int)
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("VcsMaxSplits").WithArg(TupleItem0Name, Type.Int)
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("Verify")
.Filter(attributeHost => attributeHost is ICanVerify),

BuiltIn("VerifyOnly")
.Filter(attributeHost => attributeHost is ICanVerify),
};
.Filter(attributeHost => attributeHost is ICanVerify)

];

////// Helpers to create default values for the @-attribute definitions above //////

Expand Down Expand Up @@ -708,7 +750,7 @@ public class UserSuppliedAtAttribute : Attributes {
public bool Builtin; // set to true to indicate it was recognized as a builtin attribute
// Otherwise it's a user-defined one and Arg needs to be fully resolved
public UserSuppliedAtAttribute(IOrigin origin, Expression arg, Attributes prev)
: base(AtName, new List<Expression>() { arg }, prev) {
: base(AtName, [arg], prev) {
Contract.Requires(origin != null);
SetOrigin(origin);
this.AtSign = origin;
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ public ApplyExpr(IOrigin origin, Expression fn, List<Expression> args, Token clo
Function = fn;
Args = args;
CloseParen = closeParen;
FormatTokens = closeParen != null ? new[] { closeParen } : null;
FormatTokens = closeParen != null ? [closeParen] : null;
}

public ApplyExpr Clone(Cloner cloner) {
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ public ApplySuffix(IOrigin origin, IOrigin/*?*/ atLabel, Expression lhs, List<Ac
CloseParen = closeParen;
Bindings = new ActualBindings(args);
if (closeParen != null) {
FormatTokens = new[] { closeParen };
FormatTokens = [closeParen];
}
}

Expand Down
Loading

0 comments on commit d5e0040

Please sign in to comment.