Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into onlyClaimVerificati…
Browse files Browse the repository at this point in the history 
…onMemoryPerModule
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed Oct 21, 2024
2 parents b823a08 + a01b106 commit 6ae6071
Show file tree
Hide file tree
Showing 103 changed files with 2,156 additions and 1,084 deletions.
3 changes: 2 additions & 1 deletion Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,8 @@ exe:
(cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser

format-dfy:
(cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .)
(cd "${DIR}"/Source/DafnyCore ; make format)
(cd "${DIR}"/Source/DafnyStandardLibraries ; make format)

dfy-to-cs:
(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
Expand Down
343 changes: 341 additions & 2 deletions Source/DafnyCore/AST/Attributes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,37 @@ public static bool IsExplicitAxiom(this IAttributeBearingDeclaration me) =>
Attributes.Contains(me.Attributes, "axiom");
}

public class Attributes : TokenNode {
// Syntax of a formal of a built-in @-attribute
// To create one, prefer using the chaining BuiltInAtAttributeSyntax.WithArg()
public record BuiltInAtAttributeArgSyntax(
String ArgName,
Type ArgType, // If null, it means it's not resolved (@Induction and @Trigger)
Expression DefaultValue) {
public Formal ToFormal() {
Contract.Assert(ArgType != null);
return new Formal(Token.NoToken, ArgName, ArgType, true, false,
DefaultValue);
}
}

// Syntax for a built-in @-attribute.
// To create such an attribute, use the Attributes.B() helper
public record BuiltInAtAttributeSyntax(
string Name,
List<BuiltInAtAttributeArgSyntax> Args,
Func<IAttributeBearingDeclaration, bool> CanBeApplied) {
public BuiltInAtAttributeSyntax WithArg(String argName, Type argType, Expression defaultValue = null) {
var c = new List<BuiltInAtAttributeArgSyntax>(Args) {
new(argName, argType, defaultValue) };
return this with { Args = c };
}

public BuiltInAtAttributeSyntax Filter(Func<IAttributeBearingDeclaration, bool> canBeApplied) {
return this with { CanBeApplied = canBeApplied };
}
}

public class Attributes : TokenNode, ICanFormat {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Name != null);
Expand All @@ -37,6 +67,7 @@ void ObjectInvariant() {
public Attributes(string name, [Captured] List<Expression> args, Attributes prev) {
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(args));
Contract.Requires(name != UserSuppliedAtAttribute.AtName || this is UserSuppliedAtAttribute);
Name = name;
Args = args;
Prev = prev;
Expand Down Expand Up @@ -207,6 +238,241 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object
: new List<Node> { Prev });

public override IEnumerable<INode> PreResolveChildren => Children;
public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
foreach (var token in OwnedTokens) {
switch (token.val) {
case "}": {
formatter.SetClosingIndentedRegion(token, indentBefore);
break;
}
case "@": {
formatter.SetIndentations(token, indentBefore, indentBefore, indentBefore);
break;
}
case ",": {
formatter.SetDelimiterInsideIndentedRegions(token, indentBefore);
break;
}
case "{" or "{:": {
formatter.SetOpeningIndentedRegion(token, indentBefore);
break;
}
}
}
foreach (var arg in Args) {
formatter.SetExpressionIndentation(arg);
}
formatter.SetClosingIndentedRegion(EndToken, indentBefore);
return false; // Don't do inner attributes, they should be performed independently
}

// Typically, {:} are indented when @-attributes are not
public static void SetIndents(Attributes attrs, int indentBefore, TokenNewIndentCollector formatter) {
foreach (var attribute in attrs.AsEnumerable()) {
if (attribute.StartToken.val == UserSuppliedAtAttribute.AtName) {
attribute.SetIndent(indentBefore, formatter);
} else {
attribute.SetIndent(indentBefore + formatter.SpaceTab, formatter);
}
}
}
private static string TupleItem0Name => "0";
// Helper to create a built-in @-attribute
static BuiltInAtAttributeSyntax BuiltIn(string name) {
return new BuiltInAtAttributeSyntax(
name, new List<BuiltInAtAttributeArgSyntax>(), _ => true);
}

// Helper to create an old-style attribute
private static Attributes A(string name, params Expression[] args) {
return new Attributes(name, args.ToList(), null);
}

// Helper to create an old-style attribute with only one argument
private static Attributes A1(string name, ActualBindings bindings) {
if (Get(bindings, 0, out var expr) && expr != null) {
return A(name, expr);
}

return A(name);
}

// Given a user-supplied @-attribute, expand it if recognized as builtin to an old-style attribute
// or mark it as not built-in for later resolution
public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttribute atAttribute, IAttributeBearingDeclaration attributeHost) {
var toMatch = atAttribute.Arg;
var name = atAttribute.UserSuppliedName;
var bindings = atAttribute.UserSuppliedPreResolveBindings;

if (name == null) {
program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, "Attribute not recognized: " + atAttribute.ToString());
return null;
}

if (!TryGetBuiltinAtAttribute(name, out var builtinSyntax) || builtinSyntax == null) {
atAttribute.Builtin = false; // Will be resolved after
return null;
}

if (!builtinSyntax.CanBeApplied(attributeHost)) {
program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind);
}

var formals = builtinSyntax.Args.Select(arg => arg.ToFormal()).ToArray();
ResolveLikeDatatypeConstructor(program, formals, name, atAttribute, bindings);

atAttribute.Builtin = true;
atAttribute.Arg.Type = Type.Int; // Dummy type to avoid crashes

switch (name) {
case "Compile": {
return A1("compile", bindings);
}
case "Fuel": {
if (Get(bindings, 0, out var lowFuel) && lowFuel != null) {
if (Get(bindings, 1, out var highFuel) && highFuel != null) {
if (Get(bindings, 2, out var functionName) && IsStringNotEmpty(functionName)) {
return A("fuel", functionName, lowFuel, highFuel);
}

return A("fuel", lowFuel, highFuel);
}

return A("fuel", lowFuel);
}

return A("fuel");
}
case "IsolateAssertions": {
return A("isolate_assertions");
}
case "Options": {
return A1("options", bindings);
}
default: {
throw new Exception("@-Attribute added to Attributes.BuiltinAtAttributes needs to be handled here");
}
}
}

// 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() {
BuiltIn("Compile")
.WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
.Filter(attributeHost =>
attributeHost is TopLevelDecl and not TypeParameter or MemberDecl or ModuleDefinition),
BuiltIn("Fuel")
.WithArg("low", Type.Int, DefaultInt(1))
.WithArg("high", Type.Int, DefaultInt(2))
.WithArg("functionName", Type.ResolvedString(), DefaultString(""))
.Filter(attributeHost => attributeHost is Function or AssertStmt),
BuiltIn("IsolateAssertions")
.Filter(attributeHost => attributeHost is ICanVerify),
BuiltIn("Options")
.WithArg(TupleItem0Name, Type.ResolvedString())
.Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition),
};

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

public static LiteralExpr DefaultString(string value) {
return Expression.CreateStringLiteral(Token.NoToken, value);
}

public static LiteralExpr DefaultBool(bool value) {
return Expression.CreateBoolLiteral(Token.NoToken, value);
}

public static LiteralExpr DefaultInt(int value) {
return Expression.CreateIntLiteralNonnegative(Token.NoToken, value);
}

private static bool IsStringNotEmpty(Expression value) {
return value is StringLiteralExpr { Value: string and not "" };
}

// Given resolved bindings, gets the i-th argument according to the
// declaration formals order
private static bool Get(ActualBindings bindings, int i, out Expression expr) {
if (bindings.Arguments.Count < i + 1) {
expr = null;
return false;
}

expr = bindings.Arguments[i];
return true;
}

// Resolves bindings given a list of datatype constructor-like formals,
// obtained from built-in @-attribute definitions
private static void ResolveLikeDatatypeConstructor(
Program program, Formal[] formals, string attrName,
UserSuppliedAtAttribute attrs, ActualBindings bindings) {
var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ;
var typeMap = new Dictionary<TypeParameter, Type>();
var resolver = new ModuleResolver(new ProgramResolver(program), program.Options);
resolver.reporter = program.Reporter;
resolver.moduleInfo = resolver.ProgramResolver.SystemModuleManager.systemNameInfo;
resolver.ResolveActualParameters(bindings, formals.ToList(), attrs.tok,
attrs, resolutionContext, typeMap, null);
resolver.FillInDefaultValueExpressions();
resolver.SolveAllTypeConstraints();
// Verify that arguments are given literally
foreach (var binding in bindings.ArgumentBindings) {
if (binding.Actual is not LiteralExpr) {
program.Reporter.Error(MessageSource.Resolver, binding.Actual.RangeToken, $"Argument to attribute {attrName} must be a literal");
}
}
}

// Recovers a built-in @-Attribute if it exists
public static bool TryGetBuiltinAtAttribute(string name, out BuiltInAtAttributeSyntax builtinAtAttribute) {
return BuiltInAtAttributeDictionary.TryGetValue(name, out builtinAtAttribute);
}

// Builtin @-attributes dictionary based on the sequence of definitions of @-attributes
public static Dictionary<string, BuiltInAtAttributeSyntax> BuiltInAtAttributeDictionary =
BuiltinAtAttributes.ToDictionary(b => {
if (b.Name.Contains("_") || b.Name.Contains("-") || Char.IsLower(b.Name[0])) {
throw new Exception("Builtin @-attributes are PascalCase for consistency");
}
return b.Name;
}, b => b);

// Overridable method to clone the attribute as if the new attribute was placed after "prev" in the source code
public virtual Attributes CloneAfter(Attributes prev) {
return new Attributes(Name, Args, prev);
}

//////// Helpers for parsing attributes //////////////////

// Returns the memory location's attributes content and set the memory location to null (no attributes)
public static Attributes Consume(ref Attributes tmpStack) {
var result = tmpStack;
tmpStack = null;
return result;
}

// Empties the first attribute memory location while prepending its attributes to the second attribute memory location, in the same order
public static void MergeInto(ref Attributes tmpStack, ref Attributes attributesStack) {
MergeIntoReadonly(tmpStack, ref attributesStack);
tmpStack = null;
}

// Prepends the attributes tmpStack before the attributes contained in the memory location attributesStack
private static void MergeIntoReadonly(Attributes tmpStack, ref Attributes attributesStack) {
if (tmpStack == null) {
return;
}
if (attributesStack == null) {
attributesStack = tmpStack;
return;
}
MergeIntoReadonly(tmpStack.Prev, ref attributesStack);
attributesStack = tmpStack.CloneAfter(attributesStack);
}
}

public static class AttributesExtensions {
Expand All @@ -221,6 +487,7 @@ public static IEnumerable<Attributes> AsEnumerable(this Attributes attr) {
}
}

// {:..} Attributes parsed are built using this class
public class UserSuppliedAttributes : Attributes {
public readonly IToken OpenBrace;
public readonly IToken CloseBrace;
Expand All @@ -237,11 +504,83 @@ public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, L
}
}

// @-Attributes parsed are built using this class
public class UserSuppliedAtAttribute : Attributes {
public static readonly string AtName = "@";
public readonly IToken AtSign;
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(IToken tok, Expression arg, Attributes prev)
: base(AtName, new List<Expression>() { arg }, prev) {
Contract.Requires(tok != null);
this.tok = tok;
this.AtSign = tok;
}

public Expression Arg => Args[0];

public override Attributes CloneAfter(Attributes prev) {
return new UserSuppliedAtAttribute(AtSign, Args[0], prev);
}

// Name of this @-Attribute, which is the part right after the @
public string UserSuppliedName =>
GetName(this);

// Pre-resolved bindings of this @-Attribute
public ActualBindings UserSuppliedPreResolveBindings =>
GetPreResolveBindings(this);

// Pre-resolved arguments of this @-Attributes. The order is the one provided by the user,
// not by any binding. Used for
public IEnumerable<Expression> UserSuppliedPreResolveArguments =>
GetPreResolveArguments(this);

// Gets the name of an @-attribute. Attributes might be applied.
public static string GetName(Attributes a) {
if (a is UserSuppliedAtAttribute { Arg: ApplySuffix { Lhs: NameSegment { Name: var name } } }) {
return name;
}
if (a is UserSuppliedAtAttribute { Arg: NameSegment { Name: var singleName } }) {
return singleName;
}

return null;
}

// Gets the pre-resolved bindings of an @-Attribute.
// Returns an empty bindings if it's anything else
public static ActualBindings GetPreResolveBindings(Attributes a) {
if (a is UserSuppliedAtAttribute { Arg: ApplySuffix { Bindings: var bindings } }) {
return bindings;
}
return new ActualBindings(new List<ActualBinding>());
}

// Gets the list of pre-resolved arguments of an @-Attribute, and an empty list otherwise
public static IEnumerable<Expression> GetPreResolveArguments(Attributes a) {
if (a is UserSuppliedAtAttribute { UserSuppliedPreResolveBindings: var bindings }) {
return bindings.ArgumentBindings.Select(arg => arg.Actual);
}

return new List<Expression>();
}

// Gets the list of pre-resolved arguments of an @-Attribute, and the list of arguments
// for any other kind of attributes. Used for example to extract module options for parsing.
public static IEnumerable<Expression> GetUserSuppliedArguments(Attributes a) {
return a is UserSuppliedAtAttribute { UserSuppliedPreResolveArguments: var arguments } ? arguments : a.Args;
}

public override string ToString() => Prev + (Prev == null ? "" : " ") + "@" + Arg;
}

/// <summary>
/// A class implementing this interface is one that can carry attributes.
/// </summary>
public interface IAttributeBearingDeclaration {
Attributes Attributes { get; }
Attributes Attributes { get; internal set; }
string WhatKind { get; }
}

public static class AttributeBearingDeclarationExtensions {
Expand Down
Loading

0 comments on commit 6ae6071

Please sign in to comment.