From 026abe163ed064d837f7042341646df6bc99d9bb Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Mon, 15 Jul 2024 15:22:17 +0200
Subject: [PATCH] Add test and fix bug in RevealedAnalysis

---
 Source/Core/AST/ChangeScope.cs                |  2 ++
 Source/Directory.Build.props                  |  2 +-
 Source/VCGeneration/Prune/RevealedAnalysis.cs | 21 ++++++++++++-------
 Test/pruning/Reveal.bpl                       | 11 ++++++++++
 Test/pruning/Reveal.bpl.expect                |  2 +-
 5 files changed, 29 insertions(+), 9 deletions(-)

diff --git a/Source/Core/AST/ChangeScope.cs b/Source/Core/AST/ChangeScope.cs
index 1b1f7eae8..b04922bd4 100644
--- a/Source/Core/AST/ChangeScope.cs
+++ b/Source/Core/AST/ChangeScope.cs
@@ -24,6 +24,8 @@ public override void Typecheck(TypecheckingContext tc) {
   }
 
   public override void Emit(TokenTextWriter stream, int level) {
+    stream.Write(this, level, Mode == Modes.Push ? "push" : "pop");
+    stream.WriteLine(";");
   }
 
   public override void AddAssignedVariables(List<Variable> vars) {
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index 5adb9b553..f4b95f000 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.2.0</Version>
+    <Version>3.2.1</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>
diff --git a/Source/VCGeneration/Prune/RevealedAnalysis.cs b/Source/VCGeneration/Prune/RevealedAnalysis.cs
index 4a70d3d0e..c4863721d 100644
--- a/Source/VCGeneration/Prune/RevealedAnalysis.cs
+++ b/Source/VCGeneration/Prune/RevealedAnalysis.cs
@@ -2,6 +2,7 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.Immutable;
+using System.Diagnostics;
 using Microsoft.Boogie;
 
 namespace VCGeneration.Prune;
@@ -27,10 +28,14 @@ public RevealedAnalysis(IReadOnlyList<Cmd> roots,
     RevealedState.AllRevealed);
 
   protected override ImmutableStack<RevealedState> Merge(ImmutableStack<RevealedState> first, ImmutableStack<RevealedState> second) {
-    var firstTop = first.Peek();
-    var secondTop = second.Peek();
-    var mergedTop = MergeStates(firstTop, secondTop);
-    return ImmutableStack.Create(mergedTop);
+    if (first.IsEmpty && second.IsEmpty) {
+      return ImmutableStack<RevealedState>.Empty;
+    }
+    var firstElement = first.Peek();
+    var secondElement = second.Peek();
+    var mergedTop = MergeStates(firstElement, secondElement);
+    var mergedTail = Merge(first.Pop(), second.Pop());
+    return mergedTail.Push(mergedTop);
   }
 
   protected override bool StateEquals(ImmutableStack<RevealedState> first, ImmutableStack<RevealedState> second) {
@@ -77,10 +82,12 @@ static RevealedState GetUpdatedState(HideRevealCmd hideRevealCmd, RevealedState
   }
   
   protected override ImmutableStack<RevealedState> Update(Cmd node, ImmutableStack<RevealedState> state) {
+    if (state.IsEmpty) {
+      throw new Exception("Unbalanced use of push and pop commands");
+    }
+
     if (node is ChangeScope changeScope) {
-      return changeScope.Mode == ChangeScope.Modes.Push 
-        ? state.Push(state.Peek()) 
-        : state.Pop();
+      return changeScope.Mode == ChangeScope.Modes.Push ? state.Push(state.Peek()) : state.Pop();
     }
 
     if (node is HideRevealCmd hideRevealCmd) {
diff --git a/Test/pruning/Reveal.bpl b/Test/pruning/Reveal.bpl
index f4dc72478..7cc017729 100644
--- a/Test/pruning/Reveal.bpl
+++ b/Test/pruning/Reveal.bpl
@@ -40,4 +40,15 @@ procedure Scoping() {
   assert outer(2) == inner(2) + 1;
   pop;
   assert outer(3) == inner(3) + 1; // error
+}
+
+procedure Nesting() {
+  hide *;
+  push;
+  push;
+  if (*) {
+    reveal outer;
+  }
+  pop;
+  pop;
 }
\ No newline at end of file
diff --git a/Test/pruning/Reveal.bpl.expect b/Test/pruning/Reveal.bpl.expect
index c366c4141..76504f595 100644
--- a/Test/pruning/Reveal.bpl.expect
+++ b/Test/pruning/Reveal.bpl.expect
@@ -3,4 +3,4 @@ Reveal.bpl(29,7): Error: this assertion could not be proved
 Reveal.bpl(31,7): Error: this assertion could not be proved
 Reveal.bpl(42,3): Error: this assertion could not be proved
 
-Boogie program verifier finished with 0 verified, 4 errors
+Boogie program verifier finished with 1 verified, 4 errors