Skip to content

Commit 5812e43

Browse files
hargoniXkim-em
authored andcommitted
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 a3a9f2a commit 5812e43

File tree

2 files changed

+6
-4
lines changed

2 files changed

+6
-4
lines changed

src/Init/Data/String/Basic.lean

Lines changed: 2 additions & 2 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 :=
@@ -1596,7 +1596,7 @@ def Slice.pos! (s : Slice) (off : String.Pos.Raw) : s.Pos :=
15961596
/-- Advances a valid position on a string to the next valid position, given a proof that the
15971597
position is not the past-the-end position, which guarantees that such a position exists. -/
15981598
@[expose, extern "lean_string_utf8_next_fast"]
1599-
def ValidPos.next {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos :=
1599+
def ValidPos.next {s : @& String} (pos : @& s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos :=
16001600
((inline (Slice.Pos.next pos.toSlice (ne_of_apply_ne Slice.Pos.ofSlice (by simpa)))).ofSlice)
16011601

16021602
/-- 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
@@ -1947,8 +1947,10 @@ extern "C" LEAN_EXPORT obj_res lean_decode_lossy_utf8(b_obj_arg a) {
19471947
return lean_mk_string_from_bytes(reinterpret_cast<char *>(lean_sarray_cptr(a)), lean_sarray_size(a));
19481948
}
19491949

1950-
extern "C" LEAN_EXPORT obj_res lean_string_from_utf8_unchecked(b_obj_arg a) {
1951-
return lean_mk_string_from_bytes_unchecked(reinterpret_cast<char *>(lean_sarray_cptr(a)), lean_sarray_size(a));
1950+
extern "C" LEAN_EXPORT obj_res lean_string_from_utf8_unchecked(obj_arg a) {
1951+
obj_res ret = lean_mk_string_from_bytes_unchecked(reinterpret_cast<char *>(lean_sarray_cptr(a)), lean_sarray_size(a));
1952+
lean_dec(a);
1953+
return ret;
19521954
}
19531955

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

0 commit comments

Comments
 (0)