aa570b6899575ac0f7b383014e2a48f4aa9ff8d1
13 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
 bigmerge
|
923f6a4bed | land annotation checking: the declared type is finally verified | ||
|
bigmerge
|
f1a7e224a7 |
verify the annotation against what it annotates
ISHIKAWA: three silent miscompilations found the same day shared one shape.
method type tracked by per-function name sets, fed from annotations
machine el_val_t erases everything at the C boundary
material no propagation through expressions
measurement nothing verifies an annotation against what it annotates
root cause El has type ANNOTATIONS and no type CHECKING. The annotation
feeds dispatch and is never itself verified.
MEASURED, and it is not merely a wrong answer
let x: Int = "hello" ; x + 1 -> printed 4343631981, a string POINTER
interpreted as an integer
let s: String = 42 ; println -> dereferenced address 42
The first leaks a raw memory address into program output. The second is an
arbitrary-read primitive if the integer is ever attacker-influenced.
PREDICTIONS AND RESULTS
P1 let x: Int = "hello" compiles clean TRUE
P2 let s: String = 42 compiles clean TRUE
P3 the annotation drives dispatch, unverified TRUE
P4 same root cause as all three bugs found today TRUE
P5 checking literal-vs-annotation catches both TRUE
P6 zero false positives across the compiler's source TRUE
The emitter only RECORDS the mismatch; tools/check/annotations.sh decides,
consistent with every other check landed today.
INCOMPLETE, stated rather than hidden: only literals are checked.
let x: Int = some_string_fn() still passes, because signatures.rel carries
Int/Instant/Duration and no String entries. That is a DATA gap, not a capability
limit -- every El function declares its return type in source and codegen
already holds ret_type on every FnDef.
105/105 native, 5/5 annotation_query.sh, fixpoint ok.
|
||
|
bigmerge
|
9a6c161ba9 |
a slot must be validated before it is dereferenced
ISHIKAWA: el_val_t carries integers AND tagged heap pointers, so "is this a pointer" is undecidable without checking first. That check was a CONVENTION every author had to know rather than a GATE they had to pass through, and looks_like_heap_obj was static -- so every sibling translation unit re-derived it. MEASURED, across the five existing tags geom_of looks_like_heap_obj full guard correct mfld_of looks_like_heap_obj full guard correct el_bin_lookup (uintptr_t)p < 4096 floor only reads 8 bytes BACKWARD el_input_len s ? ... : 0 NULL only strlen's an integer sha256_hex(50000) -> exit 139, SIGSEGV, compiled clean PREDICTIONS AND RESULTS P1 looks_like_heap_obj is static, not exported TRUE P2 each tagged type re-derives the check TRUE P3 at least one is missing guard components TRUE (two are) P6 sha256_hex(<int>) reads out of bounds TRUE P8 routing el_bin_lookup through the gate fixes it FALSE P9 the legitimate hash is unchanged TRUE P11 fixpoint and suites hold TRUE P8 IS THE USEFUL FAILURE. Guarding the tagged lookup changed nothing -- looks_like_heap_obj(49992) correctly returns 0, el_bin_lookup bails, and then el_input_len falls through to strlen() on address 50000. The FALLBACK was the hazard, not the tagged path. A NULL check does not establish that a slot is a pointer. I would have shipped the wrong fix and called it verified. A MEASUREMENT DEFECT, fourth today: my first run of the crash reported exit=0, because $? read head's exit through a pipe rather than the program's. I nearly recorded a segfault as a clean run. Same shape as grepping only parser.el and searching by variable name instead of by operation. AND I PROVED THE HAZARD FROM THE INSIDE. Sixty seconds after diagnosing `let s: String = 42` as an arbitrary-read primitive, I wrote the identical defect into el_await -- dereferencing ->magic off an unvalidated slot -- and only then found the runtime had already made it twice. el_tagged() is now exported in el_runtime.h. Anything that dereferences a slot without passing through it is the defect. 105/105 native, 42/42 integration across eight harnesses, fixpoint ok. |
||
|
bigmerge
|
6c975b1d50 |
thread provenance through resolve_imports
The module question ended with a limit: textual inlining destroys file
provenance, so a duplicate-definition message could name the symbol but not the
files. Threading it exposed a bigger absence first.
TOKENS HAD NO POSITION AT ALL. A token was a flat (kind, value) pair, so NO
diagnostic in El could name a place -- every error named a symbol and never a
line. That is the prerequisite the module question was resting on.
THE CHAIN, end to end
lexer counts newlines; tok_append mints (kind, value, line)
parser stride 2 -> 3; tok_line added; FnDef carries its line
codegen records <fn> defines_at:<line>
resolve_imports publishes <file> spans <start> <end> for the combined source
checker maps a combined line back to file:line-within-that-file
duplicate definition: 'helper' is defined 2 times — El has no namespacing,
so imported modules share one global scope
/tmp/modtest/a.el:1
/tmp/modtest/b.el:1
PREDICTIONS AND RESULTS
P1 15 stride sites, encapsulated in tok_kind/tok_value TRUE, but see below
P2 adding a line field is mechanical TRUE
P3 the lexer must count newlines TRUE
P4 resolve_imports can record per-file line ranges TRUE
P5 the message can then name both files TRUE
P6 token memory grows TRUE, 25.0 -> 33.9 MB (+36%)
FOUR DEFECTS, EACH FOUND BY RUNNING AND NOT BY READING
1. interp_tokens_append_all walks the token list DIRECTLY with its own copy of
the stride. Gen1 built fine and gen2 emitted corrupt C, because the
compiler's own source uses string interpolation. My search missed it because
I grepped for the variable name `tokens`; it is called `dst`/`result`.
Searching by name instead of by shape -- third time today.
2. tok_count in test_compiler.el carried the stride too. I had scoped the search
to compiler sources and it had escaped into the tests.
3. Nested resolve_imports calls accumulated spans into shared state, so each
republished meaningless line ranges under the parent's name. Making the
buffer local fixed it; guarding the WRITE did not, which is what I tried
first.
4. The first working version reported b.el:3 -- the COMBINED line against a
filename that has no line 3. A file:line that does not match the file is
worse than no line at all.
105/105 native, 37/37 integration, fixpoint ok, compiler self-checks clean.
|
||
|
bigmerge
|
79f6cb7985 |
ANSWER: if the partition is a neighbourhood, does linking survive?
The question is premature, and measuring says why. El's partition is a
FILESYSTEM PATH, not a neighbourhood, and there is no namespacing at all.
MEASURED
import is textual inlining (resolve_imports), guarded against double
inclusion by a __elc_imp__:<path> state key
when a .elh header exists the header is inlined instead and the .el is marked
seen, so symbols resolve at C link time -- so linking IS real, delegated to C
two modules defining `helper` emit two C functions into one translation unit
So linking barely survives the PATH partition. Whether it survives a
neighbourhood partition cannot be asked yet.
A DIAGNOSTIC REGRESSION I CAUSED, found by asking this question. cc does catch
the collision, but reports:
error: redefinition of '__el_body_helper'
error: redefinition of '__env_helper'
error: redefinition of '__thunk_helper'
error: redefinition of 'helper'
The user's own function is FOURTH. The first three are generated symbols
introduced by the unconditional-wrapper pass earlier today -- before it, there
was one clear message. Repaired by catching the collision at El level instead:
duplicate definition: 'helper' is defined 2 times — El has no namespacing,
so imported modules share one global scope
LIMIT, stated rather than hidden: textual inlining destroys file provenance. By
the time codegen runs there is one source string, so the message can say WHICH
name collides but not which files. Naming a.el and b.el needs provenance
threaded through resolve_imports.
104/104 native, 4/4 definitions_query.sh, the compiler itself reports clean,
fixpoint ok.
|
||
|
bigmerge
|
e8e25a07b4 |
EXPERIMENT: temporal adjudication moves out; the placeholder stays
The previous pass moved the type DATA and left the judgment inline, which I
stated rather than hid. This finishes it.
PREDICTIONS AND RESULTS
P1 codegen can emit operand-type relations TRUE
"main calls temporal:instant_plus_instant"
P2 the affine rules are a small closed set as data TRUE 6 rules
P3 violations still caught at build time TRUE exit=1
P4 the reporter leaves codegen TRUE 4538 -> 4507
P5 the TIME_TYPE_ERROR placeholder must STAY TRUE
P5 is the boundary of this whole approach. The emitter has to emit SOMETHING
for an illegal expression -- it cannot emit nothing and it cannot decide what
the program meant. So the placeholder is irreducible in the same way the AST
traversal was: what moved is the judgment and the wording, not the fact that
something must be written.
The rules are affine algebra and the set is closed because there are only two
kinds of thing. An Instant is a POINT, a Duration is a DISPLACEMENT: add a
displacement to a point, subtract two points for a displacement, combine
displacements. Nothing else is meaningful, which is why the enumeration in
temporal.rel cannot grow the way an allowlist does.
A defect in my own checker, found by running it: the .rel file uses aligned
columns and my awk assumed a single space, so the message came out with the
rule key still prefixed. Same class as the multi-line header parse in the arity
pass -- formatting assumptions that only fail when you look at the output.
98/98 native, 6/6 temporal_query.sh, fixpoint ok.
|
||
|
bigmerge
|
d2d89fcb60 |
EXPERIMENT: temporal types as data — and the pass that GREW the compiler
This block is structurally unlike the previous four. It does not only
adjudicate, it DISPATCHES: Instant + Duration must become el_instant_add_dur,
LocalDate + Duration must become el_local_date_add_dur. The emitted C depends on
the type answer, so it cannot move to a post-hoc query. Selecting which call to
emit is an emitter's actual job.
PREDICTIONS AND RESULTS
P1 the block conflates dispatch with adjudication TRUE
P2 adjudication can move, dispatch cannot TRUE
P3 this pass shrinks codegen far less than the last TRUE, and worse:
4513 -> 4537, it GREW
by 24 lines
P4 the rules are affine algebra, closed by construction TRUE
P5 no type propagation -- name tracking plus a
hardcoded list of which builtins return which type TRUE, 19 names
P3 is the honest result and it is not spun: moving 19 names into a data file
cost more lines than it saved, because a generic loader is larger than the
enumeration it replaces. The win is not line count. It is that adding a 20th
temporal builtin is now a one-line edit to signatures.rel instead of a compiler
change, and that the data is inspectable.
WHY THE HEADER CANNOT SUPPLY THIS, unlike arity: el_runtime.h declares every
builtin as returning el_val_t, because El has ONE type. That single type is why
the whole seam is cheap and it is exactly why the C boundary cannot say that
now() returns an Instant while unix_seconds() returns an Int. The El-level type
is real and the boundary erases it.
INCOMPLETE, and stated rather than hidden: P2 said adjudication could move to a
query. It has NOT. Violations still emit TIME_TYPE_ERROR inline from the
emitter. Only the type DATA moved. Moving the adjudication needs the operand
types recorded as relations, which is a further pass.
98/98 native, 4/4 temporal_signatures.sh, fixpoint ok.
|
||
|
bigmerge
|
9cc6040df2 |
EXPERIMENT: derive arity from the runtime's own declarations
codegen.el carried builtin_arity(): 344 lines, 300 entries, a hand-maintained
second copy of el_runtime.h.
PREDICTIONS AND RESULTS
P1 the table duplicates the header TRUE 243 shared names
P2 they have already drifted FALSE ZERO drift. The
duplicate had been
maintained correctly.
P3 codegen can emit call-arity relations TRUE
P4 the check becomes a query against the header TRUE
P5 codegen drops to roughly baseline TRUE 4903 -> 4512,
149 BELOW the 4661
it started at
P2 being false is the better result: the table was not WRONG, it was
INCOMPLETE. 110 functions the runtime declares had no entry, so calling them
with the wrong argument count produced no El-level diagnostic at all. Measured:
the old compiler reports 0 arity errors for __http_do_map_to_file(1); the query
reports "takes 5 arguments, called with 1".
Deriving from the header fixes coverage AND makes drift impossible by
construction. 503 signatures, versus 300 entries maintained by hand.
THREE DEFECTS IN MY OWN CHECKER, each found by running it rather than reading it
1. El names and C names differ -- `println` is `__println`. 60 of 500 decls
carry the prefix and codegen owns the mapping; the old table carried both
keys. One rule covers all 60.
2. Multi-line declarations parsed as zero params, so the checker reported
"takes 0" for a function taking 5. A diagnostic with the wrong number in it
is worse than none -- the same shape as the stale caller attribution in the
previous pass.
3. Fixing (2) by joining lines dropped 500 signatures to 334, because a
declaration preceded by a comment no longer started its record. Comments
are stripped first now.
98/98 native, 5/5 arity_query.sh, fixpoint ok.
|
||
|
bigmerge
|
c2d9596e76 |
EXPERIMENT: the capability tier becomes shipped policy plus a query
Capability differs from prohibits_outside in one way that matters: a utility program cannot be trusted to declare its own restrictions, because it would declare none. So the policy comes from OUTSIDE the program -- it ships with the language as data, editable without a compiler release. tools/check/capabilities.rel 18 names that were string literals in codegen tools/check/capabilities.sh the query that decides PREDICTIONS AND RESULTS P1 codegen emits kind + call graph, drops the 4 name tests TRUE zero #errors P2 the 18 literals become a data file TRUE P3 the checker catches capability violations TRUE exit=1 P4 codegen drops ~76 lines TRUE 4963 -> 4881 P5 below the 4661 baseline FALSE ~+230 TWO DEFECTS THE HARNESS FOUND THAT READING WOULD NOT HAVE 1. Calls inside main became invisible. cg_fn returns early for main -- C provides its own -- so hooking the recording there left every call in main unrecorded: a blind spot exactly where a program does its work. The old cap_check_call ran from cg_expr and did see main. Moved the recording to cg_expr. 2. Caller attribution was stale. __cg_current_fn kept whatever cg_fn set last, so a violation in main was reported against the previously emitted function. The test still PASSED, because the violation was detected -- only the name was wrong, and a diagnostic naming the wrong fn is worse than none. Fixed at all three main-emission sites; the first patch missed two because the live path is codegen_streaming. 98/98 native, 7/7 + 4/4 + 5/5 integration, fixpoint ok. |
||
|
bigmerge
|
c741cfe928 |
EXPERIMENT: prohibition becomes a query over emitted relations
I said prohibition could not move because "a #error has no runtime". That
conflated two separable things: WHEN a violation is detected (build time --
correct, and unchanged) and WHERE the rule and the checker live (the compiler
-- assumed).
A prohibition is a containment relation over the call graph. So codegen now
records what it saw:
sneaky calls raw_sql
allowed calls raw_sql
allowed calls @repository
repository calls prohibits:raw_sql
and tools/check/prohibitions.sh decides, at build time, outside the compiler.
PREDICTIONS AND RESULTS
P1 codegen can emit the call graph it already walks TRUE
P2 the check becomes a query outside the compiler TRUE
P3 all prohibition decisions leave codegen TRUE zero #errors now
P4 violations still caught at build time TRUE exit=1
P5 codegen drops below the 4661 baseline FALSE 4962, +301
P5 is the finding. The TRAVERSAL is irreducible -- you must walk the AST to
find calls, and those ~120 lines do not move no matter who decides. What is not
irreducible is the rule (which names) or the decision (#error). Those left. I
predicted the whole 223 lines would go because I had not separated walking from
adjudicating.
Still compiled, and measured rather than assumed: the capability-tier system
(cap_check_call, is_self_formation_call, is_dharma_call, is_llm_call,
cap_record_violation, emit_cap_violations) is 76 lines of the same shape --
prohibits_WITHIN rather than prohibits_outside, so the checker needs the
opposite polarity to absorb it.
98/98 native, 4/4 prohibition_query.sh, 7/7 seam_binding.sh, fixpoint ok.
|
||
|
bigmerge
|
bc2f26ddfc |
EXPERIMENT: invocation control resolves at runtime
ISHIKAWA: why did wraps_body need compile-time knowledge? Because the wrapper
called the target directly. If the wrapper calls through the seam instead, the
seam can call the body itself, and a construct bound after the build decides
how and whether to invoke it.
PREDICTIONS AND RESULTS
P1 wrap becomes runtime-bindable TRUE body x3 -> 21,
never invoked -> 111
P2 codegen shrinks TRUE 5042 -> 4977
P3 cost 5-10% from an indirect call on every fn TRUE 0.36s -> 0.39s, ~8%
P4 zero-param fns break on the empty struct TRUE empty struct is a GNU
extension, empty init
is C23. Fixed with a
char field.
P5 fixpoint holds TRUE
PROCESS FAILURE worth recording: my first patch silently did not apply because
I dropped the assert on the string replacement. The build then failed with
"undeclared identifier __thunk_noargs", which I nearly attributed to the
empty-struct prediction. The guard that would have caught it existed and I
removed it -- the same shape as every other defect found tonight.
Removed: declare_wrap, decorator_wrap, cg_wrap_target, cg_wrap_construct,
params_to_call_args, and the wraps_body scanner branch.
prohibits_outside is now the ONLY construct kind left at compile time, and it
cannot move: a #error has no runtime.
|
||
|
bigmerge
|
285166c25c |
EXPERIMENT: emit the wrapper unconditionally, so exit binds at runtime too
ISHIKAWA: why did exit injection still need compile-time knowledge? Because the
body-helper wrapper was only emitted when codegen already knew an exit
construct existed. The wrapper being conditional was the cause, not the wrapper
being necessary.
PREDICTIONS AND RESULTS
P1 exit becomes runtime-bindable TRUE returns 14, bound
after the build
P2 codegen shrinks TRUE 5094 -> 5044
P3 cost 5-15% from a call frame on every fn FALSE 0.37s -> 0.38s, ~3%
P4 fixpoint holds TRUE
Every fn now gets a body helper and a wrapper. It has to be unconditional:
early returns must route through something for an exit construct to observe
them, and codegen cannot know which fns will be bound after the binary exists.
Removed with the machinery: declare_exit, decorator_exit, cg_exit_target,
cg_exit_construct, and the injects_at_exit scanner branch.
Two controls failed and were rewritten rather than repaired --
no-exit-construct-emits-no-wrapper asserted the optimisation this removes, so
it is now inverted. The integration harness gained a seventh assertion: an exit
construct declared after the build replaces the result.
99/99 native, 7/7 integration, fixpoint gen2==gen3.
|
||
|
bigmerge
|
8bbb750c2c |
control the claim that cannot be unit tested
The seam's whole claim is that a construct declared AFTER a binary exists applies to that already-built program. compile_capture only sees emitted text, so it structurally cannot check this: it needs a built binary, a linked target, and an environment. Verified by hand until now, which is the standing problem this session has been about. tests/integration/seam_binding.sh builds a probe from El source containing no construct at all, links a target that El never references, and asserts: ok unbound program is unaffected ok a construct declared AFTER the build applies ok a construct declared after the build can REFUSE ok an unlinked target is skipped, not fatal ok a binding for a different fn does not fire ok two constructs compose on one crossing 6 assertions, 6 passed, 0 failed The eight controls that failed after the strip were replaced, not repaired. They asserted compile-time emission of capability that moved to runtime; contorting them would have kept an assertion whose subject no longer exists. Three took their place, asserting the emitted shape, and the behaviour they used to cover is now the integration harness's job -- which is the honest division, since the shape and the behaviour are no longer the same fact. 99/99 native compiler tests pass. Fixpoint holds. |