Add support for the :axiom attribute for ghost methods.

This suppresses compiler errors for ghost methods and functions without bodies.
Also changed the parser to complain about bodyless methods and functions
without bodies if /noCheating:1 is specified.

7 files changed, 63 insertions, 6 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index fbb51bb2..e93d1f5c 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -686,7 +686,7 @@ namespace Microsoft.Dafny {
 

         } else if (member is Function) {

           Function f = (Function)member;

-          if (f.Body == null) {

+          if (f.Body == null && !Attributes.Contains(f.Attributes, "axiom")) {

             Error("Function {0} has no body", f.FullName);

           } else if (f.IsGhost) {

             // nothing to compile

@@ -705,7 +705,7 @@ namespace Microsoft.Dafny {
 

         } else if (member is Method) {

           Method m = (Method)member;

-          if (m.IsGhost && m.Body == null) {

+          if (m.IsGhost && m.Body == null && !Attributes.Contains(m.Attributes, "axiom")) {

             Error("Method {0} has no body", m.FullName);

           } else if (!m.IsGhost) {

             Indent(indent);

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 9ded81af..2a7aec1e 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -615,6 +615,15 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
 		args.Add(anArg);

 		attrs = new Attributes("verify", args, attrs);

      }

+

+	 if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

+		SemErr(t, "only ghost methods can have the :axiom attribute");

+     }

+

+     if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

+		SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

+     }

+

      if (isConstructor) {

        m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,

                            req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);

@@ -864,6 +873,11 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
 		args.Add(anArg);

 		attrs = new Attributes("verify", args, attrs);

 	 } 

+

+     if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

+		SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

+     }

+

 	 if (isPredicate) {

         f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

                           reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 9850b68f..9f7e96bb 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -790,6 +790,11 @@ bool SemiFollowsCall(Expression e) {
 		args.Add(anArg);

 		attrs = new Attributes("verify", args, attrs);

 		} 

+		

+		if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

+		SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

+		}

+		

 		if (isPredicate) {

 		  f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

 		                    reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);

@@ -910,6 +915,15 @@ bool SemiFollowsCall(Expression e) {
 		args.Add(anArg);

 		attrs = new Attributes("verify", args, attrs);

 		}

+		

+		if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

+		SemErr(t, "only ghost methods can have the :axiom attribute");

+		}

+		

+		if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

+		SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

+		}

+		

 		if (isConstructor) {

 		 m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,

 		                     req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index f7ce3c67..3ed26d96 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -442,7 +442,7 @@ namespace Microsoft.Dafny
             //     ensures foo(x, y) < 10;

             //   { x + y }

             // We produce:

-            //   lemma reveal_foo()

+            //   lemma {:axiom} reveal_foo()

             //     ensures forall x:int, y:int {:trigger foo(x,y)} :: 0 <= x < 5 && 0 <= y < 5 ==> foo(x,y) == foo_FULL(x,y);

             Expression reqExpr = new LiteralExpr(f.tok, true);

             foreach (Expression req in f.Req) {

@@ -481,9 +481,13 @@ namespace Microsoft.Dafny
             var newEnsuresList = new List<MaybeFreeExpression>();

             newEnsuresList.Add(newEnsures);

 

+            // Add an axiom attribute so that the compiler won't complain about the lemma's lack of a body

+            List<Attributes.Argument/*!*/> argList = new List<Attributes.Argument/*!*/>();

+            Attributes lemma_attrs = new Attributes("axiom", argList, null);

+

             var reveal = new Method(f.tok, "reveal_" + f.Name, f.IsStatic, true, f.TypeArgs, new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),

                                     new Specification<FrameExpression>(new List<FrameExpression>(), null), newEnsuresList,

-                                    new Specification<Expression>(new List<Expression>(), null), null, null, false);

+                                    new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, false);

             newDecls.Add(reveal);

 

             // Update f's body to simply call the full version, so we preserve recursion checks, decreases clauses, etc.

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 57a012f3..02693c7e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -9063,7 +9063,10 @@ namespace Microsoft.Dafny {
       public Bpl.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) {

         Bpl.QKeyValue kv = null;

         for ( ; attrs != null; attrs = attrs.Prev) {

-          if (attrs.Name == skipThisAttribute) { continue; }

+          if (attrs.Name == skipThisAttribute 

+           || attrs.Name == "axiom") {  // Dafny's axiom attribute clashes with Boogie's axiom keyword

+            continue; 

+          }

           List<object> parms = new List<object>();

           foreach (Attributes.Argument arg in attrs.Args) {

             if (arg.E != null) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5ac570f3..424b83bb 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2442,7 +2442,7 @@ Execution trace:
 

 Dafny program verifier finished with 28 verified, 2 errors

 

-Dafny program verifier finished with 30 verified, 0 errors

+Dafny program verifier finished with 37 verified, 0 errors

 Compiled assembly into Compilation.exe

 

 Dafny program verifier finished with 9 verified, 0 errors

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 5120bf81..734cc3e6 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -148,3 +148,25 @@ class DigitsClass {
   }

 }

 

+// Should not get errors about methods or functions with empty bodies

+// if they're marked with an :axiom attribute

+ghost method {:axiom} m_nobody() returns (y:int)

+  ensures y > 5;

+

+lemma {:axiom} l_nobody() returns (y:int)

+  ensures y > 5;

+

+function {:axiom} f_nobody():int 

+  ensures f_nobody() > 5;

+

+// Make sure the lemma created for opaque functions doesn't produce compiler errors

+function {:opaque} hidden():int

+{

+  7

+}

+

+method hidden_test()

+{

+  reveal_hidden();

+  assert hidden() == 7;

+}