neuron-technologies/el
3
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects Releases 5 Wiki Activity

verify the annotation against what it annotates

Browse Source 
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.
This commit is contained in:
bigmerge
2026-08-17 10:53:01 -05:00
parent cb7289f065
commit f1a7e224a7
3 changed files with 94 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
lang/el-compiler/src/codegen.el
+31
View File
@@ -1526,6 +1526,37 @@ fn cg_stmt(stmt: Map<String, Any>, indent: String, declared: [String]) -> [Strin
if str_eq(ltype, "Int") {
add_int_name(name)
}
// ANNOTATION CHECKING. El has type annotations and, until now, no type
// checking: the annotation fed dispatch and was never itself verified.
// That is the root cause of every silent miscompilation found on
// 2026-08-17, and the failure 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 ; print -> dereferenced address 42
//
// The second is an arbitrary-read primitive if the integer is ever
// attacker-influenced. Literals are checked here because they are
// unambiguous; the emitter only RECORDS the mismatch, the query decides.
let vkind: String = val["expr"]
if str_eq(ltype, "Int") {
if str_eq(vkind, "Str") {
record_call(state_get("__cg_current_fn"), "typemismatch:Int:String:" + name)
}
}
if str_eq(ltype, "String") {
if str_eq(vkind, "Int") {
record_call(state_get("__cg_current_fn"), "typemismatch:String:Int:" + name)
}
if str_eq(vkind, "Float") {
record_call(state_get("__cg_current_fn"), "typemismatch:String:Float:" + name)
}
}
if str_eq(ltype, "Float") {
if str_eq(vkind, "Str") {
record_call(state_get("__cg_current_fn"), "typemismatch:Float:String:" + name)
}
}
// UNANNOTATED let: take the type from what the initialiser RETURNS.
// Without this, `let a = str_len(s)` loses the Int and a later `a + b`
// lowers to el_str_concat on two integers -- silently, with no error,
lang/tests/integration/annotation_query.sh
Executable
+34
View File
@@ -0,0 +1,34 @@
#!/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
lang/tools/check/annotations.sh
Executable
+29
View File
@@ -0,0 +1,29 @@
#!/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"