Skip to content

fix: potential Array.get!Internal leaks part 1#13147

Merged
hargoniX merged 3 commits intomasterfrom
hbv/fix_getbang_p1
Mar 27, 2026
Merged

fix: potential Array.get!Internal leaks part 1#13147
hargoniX merged 3 commits intomasterfrom
hbv/fix_getbang_p1

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

This PR fixes theoretical leaks in the handling of Array.get!Internal in the code generator.
Currently, the code generator assumes that the value returned by get!Internal is derived from the
Array argument. However, this does not generally hold up as we might also return the Inhabited
value in case of an out of bounds access (recall that we continue execution after panics by
default). This means that we sometimes convert an Array.get!Internal to
Array.get!InternalBorrowed when we are not allowed to do so because in the panic case the
Inhabited instance can be returned and if it is an owned value it is going to leak.

The fix consists of adapting several components to this change:

  1. PropagateBorrow will only mark the derived value as forcibly borrowed if both the Inhabited
    and Array argument are forcibly borrowed.
  2. InferBorrow will do the same for its data flow analysis
  3. The derived value analysis of ExplicitRC is extended from a derived value tree to a derived
    value graph where a value may have more than one parent. We only consider a value borrowed if all
    of its parents are still accessible. Then get!Internal is equipped with both its Inhabited
    and its Array parent.

These changes are sufficient for correctness on their own. However, they are going to break
get!Internal to get!InternalBorrowed conversion in most places. This happens because almost all
Inhabited instances are going to be constants. Currently reads from constants yield semantically
owned values and thus block the get!InternalBorrowed conversion. We would thus prefer for these
constants to be treated as borrows instead.

The owned return is implemented in two ways at the moment:

  1. In the C code emitter we do not need to do anything as constants are marked persistent to begin
    with
  2. In the interpreter whenever a constant is pulled from the constant cache it is inc-ed and then
    later dec-ed somewhere (potentially using a dec[persistent] which is a no-op in C)

This PR changes the semantics of constant reads to instead be borrows from the constant (they can be
cutely interpreted as "being borrowed from the world"). This enables many get!Internal to have
both their arguments be marked as borrowed and thus still converted to get!InternalBorrowed. Note
that this PR does not yet change the semantics of the interpreter to account for this
(it will be done in a part 2) and thus introduces (very minor) leaks temporarily.

Furthermore, we observed code with signatures such as the following:

@[specialize]
def foo {a : Type} [inst : Inhabited a] (xs : Array a) (f : a -> a -> Bool) ... :=
  ...
  let x := Array.get!Internal inst xs i
  ...

being instantiated with a := UInt32. This poses a challenge because Inhabited is currently
marked as nospecialize, meaning that we are sometimes going to end up with code such as:

def foo._spec (inst : UInt32) (xs : @&Array UInt32) ... :=
  ...
  let inst := box inst
  let x := Array.get!Internal inst xs i
  dec inst
  ...

Here xs itself was inferred as borrowed, however, the UInt32 Inhabited instance was not
specialized for (as Inhabited is marked nospecialize) and thus needs to be boxed. This causes
the inst parameter to get!Internal to be owned and thus get!InternalBorrowed conversion fails.
This PR marks Inhabited as weak_specialize which will make it get specialized for in this case,
yielding code such as:

def foo._spec (xs : @&Array UInt32) ... :=
  ...
  let inst := instInhabitedUInt32
  let inst := box inst
  let x := Array.get!Internal inst xs i
  dec inst
  ...

Fortunately the closed term extractor has support for precisely this feature and thus produces:

def inst.boxed_const :=
  let inst := instInhabitedUInt32
  let inst := box inst
  return inst

def foo._spec (xs : @&Array UInt32) ... :=
  ...
  let inst := inst.boxed_const
  let x := Array.get!Internal inst xs i
  ...

As described above reads from constants are now interpreted as borrows and thus the conversion to
get!InternalBorrowed becomes legal again.

@hargoniX hargoniX requested a review from leodemoura as a code owner March 26, 2026 23:49
@hargoniX hargoniX changed the title fix: Array.get!Internal leaks fix: Array.get!Internal leaks part 1 Mar 26, 2026
@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Mar 26, 2026
@hargoniX hargoniX changed the title fix: Array.get!Internal leaks part 1 fix: potential Array.get!Internal leaks part 1 Mar 26, 2026
@hargoniX hargoniX enabled auto-merge March 26, 2026 23:53
@hargoniX hargoniX added this pull request to the merge queue Mar 27, 2026
Merged via the queue into master with commit f9c8b5e Mar 27, 2026
23 of 27 checks passed
@hargoniX hargoniX deleted the hbv/fix_getbang_p1 branch March 27, 2026 01:05
github-merge-queue bot pushed a commit that referenced this pull request Mar 27, 2026
Part 2 for #13147, adding the necessary constant semantics to the
interpreter.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant