From 7f24f81901375f974ec8c44eb0f8cf29a484ef34 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 16 Oct 2024 14:34:36 -0500 Subject: [PATCH] Resolution of attributes ensures arguments are literals --- Source/DafnyCore/AST/Attributes.cs | 7 ++++++- Source/DafnyCore/Dafny.atg | 1 - .../LitTest/at-attributes/at-attributes-typos.dfy | 1 + .../at-attributes/at-attributes-typos.dfy.expect | 11 ++++++----- 4 files changed, 13 insertions(+), 7 deletions(-) diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index db9a683340..a0fe3968a2 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -400,7 +400,6 @@ private static bool Get(ActualBindings bindings, int i, out Expression expr) { private static void ResolveLikeDatatypeConstructor( Program program, Formal[] formals, string attrName, UserSuppliedAtAttribute attrs, ActualBindings bindings) { - var datatypeName = new Name(RangeToken.NoToken, attrName); var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ; var typeMap = new Dictionary(); var resolver = new ModuleResolver(new ProgramResolver(program), program.Options); @@ -410,6 +409,12 @@ private static void ResolveLikeDatatypeConstructor( 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 diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index a7fbdde119..9289a4f838 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1694,7 +1694,6 @@ FunctionDecl List ens = new List(); List reads = new List(); List decreases; - Attributes attrs = null; Attributes decAttrs = null; Attributes readsAttrs = null; Expression body = null; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy index e401748ab3..309e33e82e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy @@ -11,6 +11,7 @@ function f(x:int) : bool @compile("true") // Should be Compile @Compile("true") // Should be boolean @Compile(true, false) // Should have one argument +@Compile(true && false) @fuel(low := 1, 2) // Should be Fuel @Fuel(2, low := 1) // Wrong position of arguments function g(y:int, b:bool) : bool diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect index 71df34ea36..88deab2c75 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect @@ -1,8 +1,9 @@ -at-attributes-typos.dfy(15,9): Error: the parameter named 'low' is already given positionally +at-attributes-typos.dfy(16,9): Error: the parameter named 'low' is already given positionally +at-attributes-typos.dfy(14,9): Error: Argument to attribute Compile must be a literal at-attributes-typos.dfy(13,20): Error: wrong number of arguments (got 2, but attribute 'Compile' expects at most 1: (0: bool)) at-attributes-typos.dfy(12,15): Error: incorrect argument type for attribute parameter '0' (expected bool, found string) -at-attributes-typos.dfy(22,31): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0) -at-attributes-typos.dfy(14,1): Error: unresolved identifier: fuel +at-attributes-typos.dfy(23,31): Error: wrong number of arguments (got 1, but attribute 'IsolateAssertions' expects 0) +at-attributes-typos.dfy(15,1): Error: unresolved identifier: fuel at-attributes-typos.dfy(11,1): Error: unresolved identifier: compile -at-attributes-typos.dfy(21,1): Error: unresolved identifier: isolate_assertions -7 resolution/type errors detected in at-attributes-typos.dfy +at-attributes-typos.dfy(22,1): Error: unresolved identifier: isolate_assertions +8 resolution/type errors detected in at-attributes-typos.dfy