bigmerge
f1a7e224a7
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.
30 lines
1.2 KiB
Bash
Executable File
30 lines
1.2 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# annotations.sh — verify that a declared type matches what it annotates.
|
|
#
|
|
# El had annotations and no checking. The annotation fed dispatch (deciding
|
|
# whether `a + b` is arithmetic or concatenation) and was never verified against
|
|
# the value, so a mismatch did not fail -- it reinterpreted memory:
|
|
#
|
|
# let x: Int = "hello" a string pointer used as an integer
|
|
# let s: String = 42 address 42 dereferenced as a string
|
|
#
|
|
# The second is an arbitrary-read primitive if the integer is influenced.
|
|
set -uo pipefail
|
|
REL="${1:?usage: annotations.sh <relations-file>}"
|
|
[ -f "$REL" ] || exit 0
|
|
locate() {
|
|
awk -v L="$1" '$2=="spans" && $3<=L && $4>=L {printf "%s:%d", $1, L-$3+1; exit}' "$REL" 2>/dev/null
|
|
}
|
|
V=0
|
|
while read -r caller _ rest; do
|
|
[ "${rest#typemismatch:}" = "$rest" ] && continue
|
|
body="${rest#typemismatch:}"
|
|
declared="${body%%:*}"; body="${body#*:}"
|
|
actual="${body%%:*}"; var="${body#*:}"
|
|
printf "type error in %s: '%s' is declared %s but assigned a %s literal — the annotation drives dispatch, so the value will be reinterpreted rather than rejected\n" \
|
|
"$caller" "$var" "$declared" "$actual"
|
|
V=$((V+1))
|
|
done < <(sort -u "$REL")
|
|
[ "$V" -eq 0 ] && echo "annotations: clean"
|
|
exit "$V"
|