What the compiler proves about your heap

This series has been making claims about memory one article at a time. This one collects them, because the collection is itself the point: not “Mica catches many bugs”, but a closed list — every classic heap bug, and for each one, exactly what happens.

Every row in that table was produced for this series by making the bug and reading the answer. The example for this article is built so you can do the same.

examples/HeapProofs is a workbench: a sound program — compiles clean, runs to exit 0 — where every section is one bug class held at bay, and every section’s comment names the one-line change that produces the bug and the report it earns. Make the change, rebuild, read the refusal, undo.

make -C mica-container/examples/HeapProofs run

The obligation rows

The first three rows are the heap article’s machinery. Delete one dispose from the workbench:

obligation error 13102: heap cell is not released on every path: last use at
line 68, the path leaving at line 138 releases nothing — dispose it, defer
the dispose, return it, or bind it to an owner with 'until'

Read the two line numbers: the last use is where you stopped needing the cell, and the leaking path is the program’s last line — the analysis followed the cell all the way to the exit before concluding no path releases it.

Move a read below the release:

obligation error 13105: heap cell is dereferenced after it was already
released on every path reaching here — the cell allocated at line 77 is
used after its dispose; move the use before the release

Release twice:

obligation error 13104: heap cell is disposed again after it was already
released on every path reaching here — remove the repeated dispose of the
cell allocated at line 77

Each report names the allocation it indicts and the move that repairs it. These are not warnings — the build stops.

Two rows join them where the cell is not in a variable but inside something else. Store a cell in a record’s field and release it by hand as well, and the container’s own release would free it a second time:

obligation error 13109: heap cell is released by hand although the container
holding it releases it: the cell allocated at line 11 stands in an owning
slot of a container on every path reaching here, and that container's own
release walks the slot - so this dispose is the first of two releases and
the second comes from code nobody wrote. Remove this dispose and let the
container's release make it, clear the slot first if the cell must leave the
container, or mark the slot 'borrowed pointer' so the container only views
the cell

Give one cell to two containers, and each would release it:

obligation error 13106: heap cell is handed to a second owner: the cell
allocated at line 11 already belongs to a container that releases it, and an
owning field or element releases everything it holds — so this store gives
one cell two owners and its release would happen twice, from code nobody
wrote. Store a fresh cell here, mark the destination 'borrowed pointer' to
borrow rather than own, or move the cell by clearing the slot that held it

Store a second cell into a field that still holds the first, and the first is lost, since the record’s release now reaches the second one only:

obligation error 13110: heap cell is lost here: this store overwrites the
owning slot that held the cell allocated at line 11, which nothing had
released, and nothing releases it after - dispose the slot's cell before
storing into the slot, or read it out into a name that disposes it or hands
it on

The three are the same machinery read from three sides. A cell stored into an owning slot is released — by the dispose of the record that holds it, or by the drain of the owner that record is bound to — and the compiler follows it in and out again: through a pointer field, through an element of a fixed or a dynamic array, and through a pointer parked inside a value record one level down. That is why releasing it yourself is refused, why reading it after its container is gone is 13105, and why writing the release the container already makes is not something you have to remember.

The leak that no analysis can prove

A leak the compiler can prove is 13102 and the build stops. But a cell can come to rest where no analysis follows it — an element written under a computed index, a structure handed across a boundary — and then nothing is refused. That case has an answer too, and it is the second half of the guarantee: a checked run names the cells that were never released, and fails. Each cell is named by its type and the file, line and column of the new that made it, at every checked tier:

Mica leak report: 4 heap cells were never released, holding 64 bytes
  Cell, made at leak.mica:32:17, 16 bytes
  Cell, made at leak.mica:32:17, 16 bytes
  Cell, made at leak.mica:32:17, 16 bytes
  Cell, made at leak.mica:32:17, 16 bytes
A checked run fails when a cell is never released: dispose the cell, bind it
to an owner with 'until', or hand it on.
The compiler refuses every leak it can prove; a checked run answers for the
rest.
Mica runtime failure: reason=leaked_cells (25), token_stream_index=unavailable (-1)

The two halves are the whole promise, and they are worth stating as one sentence: a Mica program cannot leak memory quietly — either the compiler refuses it, or a checked run reports it and fails. There is no third outcome in which a leak is a hint you may ignore.

The rows no analysis can reach

Hide a release behind runtime data — a flag, a configuration, a message — and the proof honestly gives up. Those runs belong to the checked tier (--optimize checked), where every release poisons the cell’s header and every dereference tests for poison. The heap article’s H4.mica reads a cell its flag released:

Mica runtime failure: reason=use_after_dispose (11), token_stream_index=47
Mica runtime context: file=H4.mica, line=17, column=27
Mica runtime source:     WriteLn("%lld", value p);

and P3.mica releases it a second time behind the same flag:

program P3;
var
    p : pointer int64;
procedure Touch(release : bool);
begin
    if release then dispose p;
end;

begin
    p := new int64;
    Touch(True);
    dispose p;
end.

mica --compile --link --optimize checked --source P3.mica --build build
./build/P3

Mica runtime failure: reason=double_dispose (10), token_stream_index=37
Mica runtime context: file=P3.mica, line=12, column=5
Mica runtime source:     dispose p;

The division of labour is exact: the analysis refuses what your control flow proves; the checked tier traps what it cannot; and the class of silence — a stale read that returns plausible bytes and lets them propagate — has no tier anywhere in which it is the designed behaviour.

The rows that never reach the heap at all

Some classes die earlier. A pointer cannot leave the frame that owns its cell:

analyzer error 5150: cannot return pointer to local variable 'local': only
heap-origin pointers, pointer parameters, or lexical parent-scope variables
are allowed

A pointer cannot be read before its first assignment — the wild first read does not exist:

analyzer error 5167: identifier with pointer data type is used before its
initialization: p

A borrow cannot free, and cannot be laundered into an owner — the ownership article’s two refusals, 5200 and 5199, enforced inside the borrower’s own body.

The corruption floor

Two rows are traps at every optimization tier, because they are the floor under everything else — the two ways a program reads or writes memory that was never its own. The aggregates article’s B2.mica reads past its array’s last index:

Mica runtime failure: reason=index_out_of_range (12), token_stream_index=40
Mica runtime context: file=B2.mica, line=12, column=22
Mica runtime source:     WriteLn("%lld", r[i]);

and P2.mica reads through a field that holds no cell:

program P2;

imp
    WriteLn : std;
type
    Node = record
        v    : int64;
        next : pointer Node;
    end;
var
    n : pointer Node;
begin
    n := new Node;
    WriteLn("child %lld", n.next.v);
    dispose n;
end.

mica --compile --link --optimize release,full_optimizations --source P2.mica --build build
./build/P2

Mica runtime failure: reason=nil_dereference (9), token_stream_index=42
Mica runtime context: file=P2.mica, line=14, column=33
Mica runtime source:     WriteLn("child %lld", n.next.v);

Both were run at release,full_optimizations for this article, and both trapped identically. There is no build flag that trades these checks away — the aggregates article made that promise for indices, and it holds for nil. A wrong step is a named line, on x86-64 and ARM64 alike, never a lucky read of a neighbour.

That is the claim “no silent corruption” cashed out: every road from a type-correct Mica program to overwritten foreign memory ends in a refusal or a named-line trap. The workbench’s last section walks a linked list behind a # nil guard — drop the guard, and the trap above is what you get.

What this does not do

The checked-tier rows are the checked tier’s. A release build keeps lean dereferences, so a use-after-dispose that no analysis could prove is stale memory there. The floor rows — bounds and nil — hold at every tier; the poison rows hold at checked. Develop and soak under checked; choose the shipping tier by which rows your deployment can afford to lose.

Some cells still come to rest where the analysis cannot follow them. A cell stored into a container’s owning slot is followed — the container releases it and the compiler knows so. What is left are the places with no owner to follow: an element of a plain local array written under a computed index, a pointer handed to foreign code. The analysis says which cells those are rather than pretending, and the checked run’s exit report is what answers for them.

Cycles of owners are refused where they are visible, and trap where they are not. The ownership article’s borrowed back edge is the legal spelling. Write the cycle plainly — each cell into the other’s owning slot — and the first release of either is refused as 13109, because that is exactly what a cycle of owners is in the flow. Build one where no analysis can follow it and the checked drain reports cyclic_ownership instead; without checked the drain follows the cycle until the stack runs out, and the run ends in stack_overflow rather than naming the cycle.

None of this is a garbage collector. Nothing scans, nothing counts, nothing pauses. The proofs are static, the traps are one comparison, and the arena article runs the same programs with no OS allocator at all.

What the compiler proved

Eighteen rows, each one an answer produced by a real build or a real run — not a design intention. The workbench example is sound as written; every one-line mutation its comments name was made while writing this article, and every quoted report is what came back.

If you take one sentence from the whole memory section, take this one: in Mica, the interesting question about a heap bug is not “how do I find it?” but “which refusal or which trap is it?” — and the table at the top is the complete set of answers.

The table above covers the heap. The full trap vocabulary — every reason the runtime can name, arithmetic and casts and files included, with the tier each one runs on — is the reference chapter Traps and tiers.

Next

Defer, end to end — the one cleanup mechanism behind everything this section used: its exact ordering, its interplay with leave and loops, and why one mechanism serves scopes, generators, tasks and the heap alike.