#!/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 }" 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