Resolution of attributes ensures arguments are literals

dafny-lang · Oct 16, 2024 · 7f24f81 · 7f24f81
1 parent 78d7cf6
commit 7f24f81
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 7 deletions.
diff --git 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<TypeParameter, Type>();
     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
@@ -1694,7 +1694,6 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
      List<AttributedExpression> ens = new List<AttributedExpression>();
      List<FrameExpression> reads = new List<FrameExpression>();
      List<Expression> 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
@@ -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/.../IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos.dfy.expect b/.../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