Repeated-character append panics when resize reborrows its receiver
perfloop-oss/cpp2rust · UNCATALOGUED CORRECTNESS
https://perfloop.ai/t/oss/case_rmkdg2esen
Verdict
VERIFIED · settled 2026-11-02 · merged as Cpp2Rust/cpp2rust#580
What happened: The assertion is violated on the comparison and satisfied with this change.
Hypothesis
Repeated-character append can panic on an ordinary addressable string even when no characters are requested and its result is ignored. Its generated resize holds a mutable borrow while trying to read the receiver's length through another borrow. This prevents a valid C++ operation from completing; consumer frequency remains unknown.
f21 spells the mutation as a0.resize(a0.len() + count, character). For the refcount representation used by the retained byte fixture, this becomes borrow_mut().resize(...) with borrow().len() in the first argument. RefCell, the runtime's checked mutable storage, rejects that shared read while the mutable receiver borrow is active. The previous pop has already run. No concurrency, external source alias, invalid range, large count or allocation failure is needed.
checkProperty(prop_35eet8cwt4), running python3 tests/property/string_repeat_append/check.py bytes at revision 337827dde8a229193acd95e7c1a55a3b650051ce, completed all 2,400 native cases. Emitted Rust stopped in its first case: an empty string, count zero, character zero and no shrink_to_fit. It exited 101 with 'RefCell already mutably borrowed' at the generated length read. The checker confirmed that case alone and retained bytes.replay.json. The emitted grid did not complete, so the native grid size is not a count of observed failing Rust calls.
The fixture inspects s.data() after append, which makes this receiver addressable in the translator. That is a supported string use, not an overlapping append source or a side-effecting operand. The observation is limited to this checked-storage expansion; it does not assert a panic for every unboxed Vec expansion or every f21 invocation.
This repair independently restores ignored-result calls. It does not require removing the result clone or proving single evaluation of a side-effecting receiver. Those mechanisms have separate questions, including admitted hyp_yq3tv1cvf1 for operand effects. A result-type change alone is not the assurance proof for this nested length borrow.
The first Case check is the retained empty-string replay and its exact emitted borrow scope. Then compare normal completion, receiver bytes, size and trailing zero with native C++ across the stored bounded byte grid, including zero counts, embedded NULs and growth. An expansion that completes the length read before the mutable resize borrow, or uses the same underlying Vec access for both, would reject the conflicting-borrow prediction. Keep the runtime's borrow checks rather than bypassing them. This is an architecture-independent correctness repair, not a claimed speedup or an optional concurrency hardening layer.
Prior hyp_ezmpqn07bd concerns counted-byte f4 reading an overlapping source under its destination borrow. This f21 witness has no source argument and conflicts on its own length read instead. The inspected merged implementations at https://github.com/Cpp2Rust/cpp2rust/pull/577 and https://github.com/Cpp2Rust/cpp2rust/pull/576 change substring and vector behavior, not this resize. The refreshed open implementation at https://github.com/Cpp2Rust/cpp2rust/pull/561 does not change it either. The local repair preserves the documented default refcount model and requires no new public API or representation migration.
Change to test: Arrange f21's length calculation and resize so they do not acquire overlapping RefCell borrows, using one underlying Vec borrow or a length read completed before resize borrows mutably. Preserve checked pointer access and normal append bytes, size and termination even when the returned result is ignored.
Where it lives
Evidence
The assertion is violated on the comparison and satisfied with this change: `Under successful bounded allocation, ignored-result std::string::append(count, character) on an addressable receiver completes without conflicting RefCell borrows and preserves native C++ receiver bytes, size, and trailing zero for the empty-string zero-count replay and every input in the 2,400-case string_repeat_append grid.`
Checks: 4 of 4 passed. Verification: no defect found.