provenance.pl
Explanatory context, separate from executable IR and safety evidence.
A context(Function, Records) item accompanies a func/5. Bindings and origins have function-local identities. Origins are shallow typed nodes at the enclosing statement's location, not expression spans. Values retain their original identities and hints even when removed; alias/4 records substitution without renaming the surviving value.
site(inst(Label, Index), Origins) uses a zero-based index in THIS stage's instruction list. Passes produce explicit old-to-new site maps while rewriting. Phis and jumps have stable sites phi(Temp) and jump(Label). Context never participates in CFG or safety proofs.
Records
| Record | Meaning |
|---|---|
bindingId, Name, CType, Location | declaration identity and spelling; shadowed names have distinct IDs |
originId, Location, Description, Parents | a typed lowering node, enclosing statement, or generated operation, linked by origin IDs |
valueTemp, Hint, Origins | original definition, retained as history if eliminated |
siteSite, Origins | provenance of a live instruction, phi or terminator |
aliasTemp, Replacement, Hint, Origins | copy/phi substitution, including replacement by a constant |
historyId, Temp, Hint, Origins, Replacement | retired definition when an executable name is reused; Replacement is none or replaced(Value) |
Location is at(File, Line) or none. A typed description is typed(val|obj|fun, CType, ShallowForm), a statement is statement(Kind), and a synthesized operation is generated(Pass, Reason). Parents express containment or contributing origins, not executable uses. Hint is none or named(BindingId, value|address|piece). C types are explanations of source nodes, never substitutes for IR classes.
If a pass reuses a deleted temporary's spelling, its old definition moves to history/5. Incoming alias/history replacements then use historical(Id), referencing that history record, not the new value. This metadata-only reference can never be an executable operand.
Promotion conservatively cites the slot's declaration/initial value and stores, not an assertion that every store reaches every phi. Copies preserve the survivor's primary name. Raw accesses and their adjacent checks inherit the same access origin; checks and poll edges additionally have generated origins. Erasure cannot authorize an otherwise-invalid check/access pair.
Code is Items without their context/2 items: the executable part of a module's item list, in order.
Records are the context of function Name in Items, or [] if it has none. Items may be the contexts(Index) of context_index/2: a pass over every function of a large module (SQLite's 3,000) would otherwise scan its items for each.
Contexts indexes the contexts of Items by function name, the first of a name as memberchk/2 finds it, for context_records/3.
Sites is the assoc from each site of Records' site(Site, Origins) records to its Origins.
Origins are those Sites (site_index/2) gives Site, or [] if none.
Ids is the assoc of the identities of Records' origin/4 records, each to true, for fresh_origin/3,4.
Id is a new origin identity: Base when Ids0 does not have it, else the first derived(Base, N) it does not have. Ids is Ids0 with Id. Only metadata names consult metadata: executable fresh names stay exactly what the metadata-free transformation would choose.
Id is fresh_origin/4's for Base, but Ids is not extended: for a batch of bases that are distinct and so cannot choose the same Id (derived ids keep their base), inserting each one in a function's whole origin assoc only costs time.
Records are Records0 after a pass has given the temporaries Temps new definitions (pizlonate's chkN proofs, say) whose spellings Records0 already uses: each old value/3 or alias/4 record of such a name becomes a history/5 record with a fresh origin retired(T), and references to the old definition become historical(Id), so no record confuses the old value with the new one. Ids0 are Records0's origin identities (origin_ids/2); Ids is Ids0, since the retired(T) bases cannot meet any other base and so need not be added.
The temps Ts are distinct, so their bases retired(T) are, and no other base is retired/1: the new ids cannot meet each other or a later fresh_origin's, and Ids0 need not grow (inserting each one in a large function's origin assoc was most of retirement's time).
Incoming references identify the old definition, not a new proof that happens to reuse its spelling. Historical references are not IR values.
Records are Records0 with every instruction site moved by Map, a list of OldSite-NewSite pairs with one pair per emitted instruction: an instruction that expands has several destinations, one erased has none. Phi and jump sites are unchanged.
Map, ending in Rest, pairs the site inst(Label, Old) with each of the instructions Emitted for it, numbered from New in block Label; Next is the number after the last. A rewriting loop calls this with the instructions it just emitted, to build remap_sites/3's map. The cut leaves no choicepoint per instruction (10,000 in SQLite's sqlite3VdbeExec), which would pin the rest of the function's trail.
M is M0 with its loc(File, Line) markers turned into context records: each marker becomes an origin, and the instructions after it, up to the next, sites of that origin. Legacy loc markers remain valid input (hand-written IR); they become context at unchecked transformation boundaries, never before checked-IR validation, so a checked module is its own result. The frontend writes no loc markers: such a module is its own result too, shared rather than copied (a copy of SQLite's contexts is 60 MB, and the caller still holds the original).
The frontend writes no loc markers: such a module is its own result, shared rather than copied (a copy of SQLite's contexts is 60 MB, and the caller still holds the original).
Every context(Name, Records) of Items is for a function of Items, no two for the same one, and each record is well formed: its identity unique among records of its kind, every origin it cites defined, every hint's binding declared, and every site an instruction, phi or jump the function has. ir:valid_module/1 calls this last.
the K-true pairs of each kind of record's key, in order, in one pass over a context's records. Other records are left to valid_record/3, which rejects them.
The pairs are all K-true: the assoc is built from the sorted keys in linear time.