Print definition axioms for functions and constants. (#765)

When a function / constant has a definition axiom, in generated Boogie
files, these axioms were not printed inside `uses` clauses of that
function / constant. They were instead printed as top level
declarations. This caused issues when using that printed file with the
"/prune" option since some of these axioms could now be pruned.

This PR attempts to fix this issue such that axioms that define a
constant / function are now (only) printed inside `uses` clauses of the
function / constant they are defining.

Source/Core/AST/Absy.cs

@@ -1469,7 +1469,17 @@ public override void Emit(TokenTextWriter stream, int level)
 
       EmitVitals(stream, level, false);
 
-      stream.WriteLine(";");
+      if (this.DefinitionAxioms.Any())
+      {
+        stream.WriteLine();
+        stream.WriteLine(level,"uses {");
+        this.DefinitionAxioms.ForEach(axiom => axiom.Emit(stream, level));
+        stream.WriteLine("}");
+      }
+      else
+      {
+        stream.WriteLine(";");
+      }
     }
 
     public override void Register(ResolutionContext rc)
@@ -2167,10 +2177,17 @@ public override void Emit(TokenTextWriter stream, int level)
         stream.WriteLine();
         stream.WriteLine("}");
       }
-      else
+      else if (!this.DefinitionAxioms.Any())
       {
         stream.WriteLine(";");
       }
+      if (this.DefinitionAxioms.Any())
+      {
+        stream.WriteLine();
+        stream.WriteLine("uses {");
+        this.DefinitionAxioms.ForEach(axiom => axiom.Emit(stream, level));
+        stream.WriteLine("}");
+      }
     }
 
     public override void Register(ResolutionContext rc)

Source/Core/AST/Program.cs

@@ -27,7 +27,11 @@ public void Emit(TokenTextWriter stream)
   {
     Contract.Requires(stream != null);
     stream.SetToken(this);
-    this.topLevelDeclarations.Emit(stream);
+    var functionAxioms = 
+      this.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms);
+    var constantAxioms = 
+      this.Constants.Where(f => f.DefinitionAxioms.Any()).SelectMany(c => c.DefinitionAxioms);
+    this.topLevelDeclarations.Except(functionAxioms.Concat(constantAxioms)).ToList().Emit(stream);
   }
 
   /// <summary>

Test/functiondefine/fundef6.bpl.expect

@@ -9,12 +9,14 @@ function {:define true} foo1(x: int) : bool
   x > 0
 }
 
-function {:define false} foo2(x: int) : bool;
-
+function {:define false} foo2(x: int) : bool
+uses {
 axiom (forall x: int :: {:define false} { foo2(x): bool } foo2(x): bool == (x > 0));
+}
 
-function foo3(x: int) : bool;
-
+function foo3(x: int) : bool
+uses {
 axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));
+}
 
 Boogie program verifier finished with 0 verified, 0 errors

Test/inline/fundef.bpl.expect

@@ -4,12 +4,14 @@ function {:inline true} foo(x: int) : bool
   x > 0
 }
 
-function {:inline false} foo2(x: int) : bool;
-
+function {:inline false} foo2(x: int) : bool
+uses {
 axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));
+}
 
-function foo3(x: int) : bool;
-
+function foo3(x: int) : bool
+uses {
 axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));
+}
 
 Boogie program verifier finished with 0 verified, 0 errors

Test/pruning/UsesClausesPrint.bpl

@@ -0,0 +1,27 @@
+// RUN: %parallel-boogie /print:"%t" /errorTrace:0 "%s"
+// RUN: %OutputCheck "%s" --file-to-check="%t"
+// UNSUPPORTED: batch_mode
+
+const unique four: int;
+
+const unique ProducerConst: bool uses {
+    axiom four == 4;
+}
+// CHECK-L: uses {
+// CHECK-L: axiom four == 4
+// CHECK-L: }
+
+function ProducerFunc(x: int): bool uses {
+    axiom (forall x: int :: ConsumerFunc(x) == 3);
+}
+// CHECK-L: uses {
+// CHECK-L: axiom (forall x: int :: ConsumerFunc(x) == 3)
+// CHECK-L: }
+
+procedure hasAxioms()
+  requires ProducerFunc(2);
+  requires ProducerConst;
+  ensures four == 4;
+{
+
+}