From 5b14d3e809810830f6a86a504b7e6df7ef4f831a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 19 Dec 2024 03:52:56 +0100
Subject: [PATCH] fix: `sharecommon` bug (#6415)

This PR fixes a bug in the `sharecommon` module, which was returning
incorrect results for objects that had already been processed by
`sharecommon`. See the new test for an example that triggered the bug.
---
 src/runtime/sharecommon.cpp     |  5 ++++-
 tests/lean/run/sharecommon.lean | 11 +++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/runtime/sharecommon.cpp b/src/runtime/sharecommon.cpp
index 67951044d0fb..e8132a146d1f 100644
--- a/src/runtime/sharecommon.cpp
+++ b/src/runtime/sharecommon.cpp
@@ -233,7 +233,10 @@ class sharecommon_fn {
 
     obj_res operator()(obj_arg a) {
         if (push_child(a)) {
-            return m_state.pack(a);
+            object * r = m_children.back();
+            lean_inc(r);
+            lean_dec(a);
+            return m_state.pack(r);
         }
         while (!m_todo.empty()) {
             b_obj_arg curr = m_todo.back();
diff --git a/tests/lean/run/sharecommon.lean b/tests/lean/run/sharecommon.lean
index 6948cf08d358..baf7fa9824ee 100644
--- a/tests/lean/run/sharecommon.lean
+++ b/tests/lean/run/sharecommon.lean
@@ -177,3 +177,14 @@ info: [[2, 3, 4]]
 -/
 #guard_msgs in
 #eval (tst6 2).run
+
+
+unsafe def tst7 (x : Nat) : ShareCommonT IO Unit := do
+let o0 := mkByteArray2 x
+let o1 ← shareCommonM o0
+let o2 ← shareCommonM o1
+let o3 ← shareCommonM o0
+check $ ptrAddrUnsafe o1 == ptrAddrUnsafe o2
+check $ ptrAddrUnsafe o1 == ptrAddrUnsafe o3
+
+#eval (tst7 3).run