Skip to content

Commit

Permalink
fix: sharecommon bug (#6415)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
leodemoura authored Dec 19, 2024
1 parent 7b81fb7 commit 5b14d3e
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 1 deletion.
5 changes: 4 additions & 1 deletion src/runtime/sharecommon.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
11 changes: 11 additions & 0 deletions tests/lean/run/sharecommon.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 5b14d3e

Please sign in to comment.