diff --git a/lang/el-compiler/src/codegen.el b/lang/el-compiler/src/codegen.el index c8e4853..be628f5 100644 --- a/lang/el-compiler/src/codegen.el +++ b/lang/el-compiler/src/codegen.el @@ -1526,6 +1526,37 @@ fn cg_stmt(stmt: Map, 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, diff --git a/lang/tests/integration/annotation_query.sh b/lang/tests/integration/annotation_query.sh new file mode 100755 index 0000000..5e6cf70 --- /dev/null +++ b/lang/tests/integration/annotation_query.sh @@ -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 }" +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 diff --git a/lang/tools/check/annotations.sh b/lang/tools/check/annotations.sh new file mode 100755 index 0000000..34e7ce5 --- /dev/null +++ b/lang/tools/check/annotations.sh @@ -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 }" +[ -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"