bigmerge
c2d9596e76
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.
37 lines
1.6 KiB
Bash
Executable File
37 lines
1.6 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# Control for capability-as-policy: the compiler records the program's kind and
|
|
# its call graph; the shipped policy file and the checker decide.
|
|
set -uo pipefail
|
|
ELC="${1:?usage: capability_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)); }; }
|
|
|
|
cat > "$W/u.el" <<'EOF'
|
|
fn leaky() -> Int {
|
|
dharma_emit("x", "y")
|
|
return 1
|
|
}
|
|
fn main() { println("ok") }
|
|
EOF
|
|
EL_RELATIONS_OUT="$W/r.txt" "$ELC" "$W/u.el" >/dev/null 2>&1
|
|
chk "the emitter does not adjudicate" "0" "$("$ELC" "$W/u.el" 2>/dev/null | grep -c 'capability violation')"
|
|
"$LANG_DIR/tools/check/capabilities.sh" "$W/r.txt" > "$W/o.txt" 2>&1; rc=$?
|
|
chk "a utility calling a DHARMA primitive is caught" "1" "$rc"
|
|
chk "the offending fn is named" "1" "$(grep -c 'called from leaky' "$W/o.txt")"
|
|
|
|
cat > "$W/c.el" <<'EOF'
|
|
fn quiet() -> Int { return 1 }
|
|
fn main() { println("ok") }
|
|
EOF
|
|
EL_RELATIONS_OUT="$W/r2.txt" "$ELC" "$W/c.el" >/dev/null 2>&1
|
|
"$LANG_DIR/tools/check/capabilities.sh" "$W/r2.txt" >/dev/null 2>&1
|
|
chk "a clean program exits 0" "0" "$?"
|
|
|
|
# the policy is DATA: editing it changes enforcement, with no compiler rebuild
|
|
printf 'utility prohibits_within println\n' > "$W/policy.rel"
|
|
"$LANG_DIR/tools/check/capabilities.sh" "$W/r2.txt" "$W/policy.rel" >/dev/null 2>&1
|
|
chk "editing the policy file changes enforcement, no rebuild" "1" "$?"
|
|
|
|
echo; echo " 5 assertions, $((5-F)) passed, $F failed"; exit $F
|