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.
35 lines
1.8 KiB
Bash
Executable File
35 lines
1.8 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# annotation_query.sh — a declared type must match what it annotates.
|
|
#
|
|
# El had annotations and no checking: the annotation fed dispatch and was never
|
|
# verified against the value, so a mismatch did not fail, it REINTERPRETED
|
|
# MEMORY. let x: Int = "hello" printed 4343631981 (a string pointer used as an
|
|
# integer); let s: String = 42 dereferenced address 42.
|
|
set -uo pipefail
|
|
ELC="${1:?usage: annotation_query.sh <elc>}"
|
|
LANG_DIR="${2:-$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)}"
|
|
W=$(mktemp -d); trap 'rm -rf "$W"' EXIT; F=0
|
|
chk(){ [ "$2" = "$3" ] && printf ' ok %s\n' "$1" || { printf ' FAIL %s\n expected %s got %s\n' "$1" "$2" "$3"; F=$((F+1)); }; }
|
|
cd "$LANG_DIR"
|
|
|
|
printf 'fn main() { let x: Int = "hello" println("x") }\n' > "$W/a.el"
|
|
EL_RELATIONS_OUT="$W/r.txt" "$ELC" "$W/a.el" >/dev/null 2>&1
|
|
out=$(./tools/check/annotations.sh "$W/r.txt" 2>&1); rc=$?
|
|
chk "Int annotated on a String literal is caught" "1" "$rc"
|
|
chk "and names the variable" "1" "$(echo "$out" | grep -c "'x' is declared Int")"
|
|
|
|
printf 'fn main() { let s: String = 42 println(s) }\n' > "$W/b.el"
|
|
EL_RELATIONS_OUT="$W/r2.txt" "$ELC" "$W/b.el" >/dev/null 2>&1
|
|
./tools/check/annotations.sh "$W/r2.txt" >/dev/null 2>&1
|
|
chk "String annotated on an Int literal is caught" "1" "$?"
|
|
|
|
printf 'fn main() { let n: Int = 42 let s: String = "ok" println(s + int_to_str(n)) }\n' > "$W/c.el"
|
|
EL_RELATIONS_OUT="$W/r3.txt" "$ELC" "$W/c.el" >/dev/null 2>&1
|
|
./tools/check/annotations.sh "$W/r3.txt" >/dev/null 2>&1
|
|
chk "correct annotations are clean" "0" "$?"
|
|
|
|
EL_RELATIONS_OUT="$W/r4.txt" "$ELC" elc-cli.el >/dev/null 2>&1
|
|
./tools/check/annotations.sh "$W/r4.txt" >/dev/null 2>&1
|
|
chk "the compiler's own source is clean — no false positives" "0" "$?"
|
|
echo; echo " 5 assertions, $((5-F)) passed, $F failed"; exit $F
|