Skip to content

Commit 827a96a

Browse files
authored
fix: several memory leaks in the new String API (#11263)
This PR fixes several memory leaks in the new `String` API. These leaks are mostly situations where we forgot to put borrowing annotations. The single exception is the new `String` constructor `ofByteArray`. It cannot take the `ByteArray` as a borrowed argument anymore and must thus free it on its own.
1 parent e0f9620 commit 827a96a

File tree

2 files changed

+7
-5
lines changed

2 files changed

+7
-5
lines changed

src/Init/Data/String/Basic.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ where
8080
termination_by structural fuel
8181

8282
@[expose, extern "lean_string_validate_utf8"]
83-
def ByteArray.validateUTF8 (b : ByteArray) : Bool :=
83+
def ByteArray.validateUTF8 (b : @& ByteArray) : Bool :=
8484
go (b.size + 1) 0 (by simp) (by simp)
8585
where
8686
go (fuel : Nat) (i : Nat) (hi : i ≤ b.size) (hf : b.size - i < fuel) : Bool :=
@@ -1601,11 +1601,11 @@ def Slice.pos! (s : Slice) (off : String.Pos.Raw) : s.Pos :=
16011601
/-- Advances a valid position on a string to the next valid position, given a proof that the
16021602
position is not the past-the-end position, which guarantees that such a position exists. -/
16031603
@[expose, extern "lean_string_utf8_next_fast"]
1604-
def ValidPos.next {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos :=
1604+
def ValidPos.next {s : @& String} (pos : @& s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos :=
16051605
((inline (Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)))).ofSlice)
16061606

16071607
@[expose, extern "lean_string_utf8_next_fast"]
1608-
def Pos.next {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos :=
1608+
def Pos.next {s : @& String} (pos : @& s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos :=
16091609
((inline (Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)))).ofSlice)
16101610

16111611
/-- Advances a valid position on a string to the next valid position, or returns `none` if the

src/runtime/object.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1952,8 +1952,10 @@ extern "C" LEAN_EXPORT obj_res lean_decode_lossy_utf8(b_obj_arg a) {
19521952
return lean_mk_string_from_bytes(reinterpret_cast<char *>(lean_sarray_cptr(a)), lean_sarray_size(a));
19531953
}
19541954

1955-
extern "C" LEAN_EXPORT obj_res lean_string_from_utf8_unchecked(b_obj_arg a) {
1956-
return lean_mk_string_from_bytes_unchecked(reinterpret_cast<char *>(lean_sarray_cptr(a)), lean_sarray_size(a));
1955+
extern "C" LEAN_EXPORT obj_res lean_string_from_utf8_unchecked(obj_arg a) {
1956+
obj_res ret = lean_mk_string_from_bytes_unchecked(reinterpret_cast<char *>(lean_sarray_cptr(a)), lean_sarray_size(a));
1957+
lean_dec(a);
1958+
return ret;
19571959
}
19581960

19591961
extern "C" LEAN_EXPORT uint8 lean_string_validate_utf8(b_obj_arg a) {

0 commit comments

Comments
 (0)