From 0b1e6843c94480df8e05790f43ae4182e52e3204 Mon Sep 17 00:00:00 2001
From: zafer-esen <zesen@amazon.com>
Date: Thu, 27 Jul 2023 17:09:33 -0400
Subject: [PATCH] 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                | 21 ++++++++++++++++++--
 Source/Core/AST/Program.cs             |  6 +++++-
 Test/functiondefine/fundef6.bpl.expect | 10 ++++++----
 Test/inline/fundef.bpl.expect          | 10 ++++++----
 Test/pruning/UsesClausesPrint.bpl      | 27 ++++++++++++++++++++++++++
 5 files changed, 63 insertions(+), 11 deletions(-)
 create mode 100644 Test/pruning/UsesClausesPrint.bpl

diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index 61ca5af2e..71e370470 100644
--- a/Source/Core/AST/Absy.cs
+++ b/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)
diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs
index 7ac5728ee..7e333b3f7 100644
--- a/Source/Core/AST/Program.cs
+++ b/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>
diff --git a/Test/functiondefine/fundef6.bpl.expect b/Test/functiondefine/fundef6.bpl.expect
index 1bf6a54b1..a0037242e 100644
--- a/Test/functiondefine/fundef6.bpl.expect
+++ b/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
diff --git a/Test/inline/fundef.bpl.expect b/Test/inline/fundef.bpl.expect
index 5adced6d8..daca38f2a 100644
--- a/Test/inline/fundef.bpl.expect
+++ b/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
diff --git a/Test/pruning/UsesClausesPrint.bpl b/Test/pruning/UsesClausesPrint.bpl
new file mode 100644
index 000000000..75bc90c5f
--- /dev/null
+++ b/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;
+{
+
+}
\ No newline at end of file