diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index c74f035..63e221b 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -838,6 +838,17 @@ ;; The orchestrator populates this from sealed (opt-mode) cell roots + def inits. (def ^:private vtype-box (atom {})) ;; "ns/name" -> value type +;; User-function error domains (jolt-zo1), opt-in. As the checker walks defs it +;; registers each non-redefinable single-fixed-arity user fn's {:params :body} +;; here, keyed "ns/name". At a later call site (strict mode only) the body is +;; re-checked with ONE parameter bound to its concrete argument type — if that +;; alone produces a diagnostic the all-:any body did not, that argument is +;; provably wrong and the CALL is reported. Module state, like rtenv-box: a def +;; must precede its call (the same closed-world ordering RFC 0005 assumes). +(def ^:private user-sig-box (atom {})) ;; "ns/name" -> {:params [..] :body ir} +(def ^:private checking-box (atom #{})) ;; keys mid-recheck — cycle guard +(def ^:private strict-box (atom false)) ;; report against user-fn domains? + ;; fns that RETURN an element of their (first) collection arg, so a lookup on the ;; result of (rand-nth coll-of-structs) etc. types as the element. (def ^:private elem-fns #{"rand-nth" "first" "peek" "last" "nth" "fnext" "second"}) @@ -1145,6 +1156,75 @@ ", but argument 1 is " (type-name t))}))) :else nil)) +(declare check-walk) + +;; --- user-function error domains (jolt-zo1), opt-in -------------------------- +(defn- all-any-env + "tenv binding every param name to :any (the all-ambiguous baseline)." + [params] + (reduce (fn [e p] (assoc e p :any)) {} params)) + +(defn- isolated-diag-count + "Count of diagnostics check-walk produces for body under tenv, with the shared + diag-box saved and restored so this probe never leaks into the real report." + [body tenv] + (let [saved @diag-box] + (reset! diag-box []) + (check-walk body tenv) + (let [n (count @diag-box)] + (reset! diag-box saved) + n))) + +(defn- register-user-fn! + "Record a (def name (fn [params] body)) — single fixed arity, not redefinable — + for later user-fn call checking. Redefinable/dynamic and multi/variadic fns are + skipped (their body is not a stable requirement)." + [node] + (let [init (get node :init) + m (get node :meta) + redefable (and m (or (get m :redef) (get m :dynamic)))] + (when (and (not redefable) (= :fn (get init :op))) + (let [arities (get init :arities)] + (when (= 1 (count arities)) + (let [ar (first arities)] + (when (not (get ar :rest)) + (swap! user-sig-box assoc + (str (get node :ns) "/" (get node :name)) + {:name (get node :name) + :params (get ar :params) :body (get ar :body)})))))))) + +(defn- check-user-call + "Strict mode: report a call whose concrete argument type provably makes the + callee body throw. For each concrete arg, re-check the body with ONLY that + parameter bound to its arg type (others :any); a diagnostic the all-:any body + did not already have means the argument alone is provably wrong. Monotonic — + binding a concrete type can only ADD error-domain hits — so no false positive. + Cycle-guarded so mutually recursive fns terminate." + [key sig arg-types] + (when (not (contains? @checking-box key)) + (let [prev @checking-box] + (reset! checking-box (conj prev key)) + (let [params (:params sig) + body (:body sig) + base (isolated-diag-count body (all-any-env params)) + npar (count params) + nargs (count arg-types) + np (if (< npar nargs) npar nargs)] + (reduce + (fn [_ i] + (let [at (nth arg-types i)] + (when (and (not= at :any) (not= at :truthy)) + (let [pe (assoc (all-any-env params) (nth params i) at)] + (when (> (isolated-diag-count body pe) base) + (swap! diag-box conj + {:op :user-call :argpos i :type (type-name at) + :msg (str "argument " (inc i) " to `" (:name sig) + "` is " (type-name at) + ", which its body provably rejects")}))))) + nil) + nil (range np))) + (reset! checking-box prev)))) + (defn- check-walk "Walk the IR, inferring argument types and recording diagnostics for provably-wrong core-fn calls. Threads tenv through binders exactly like infer." @@ -1155,9 +1235,14 @@ (let [fnode (get node :fn) args (get node :args) cn (when (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns))) - (get fnode :name))] - (when cn - (check-invoke cn args (mapv (fn [a] (nth (infer a tenv) 0)) args))) + (get fnode :name)) + ukey (when (= :var (get fnode :op)) + (str (get fnode :ns) "/" (get fnode :name))) + usig (when (and @strict-box ukey) (get @user-sig-box ukey))] + (when (or cn usig) + (let [ats (mapv (fn [a] (nth (infer a tenv) 0)) args)] + (when cn (check-invoke cn args ats)) + (when usig (check-user-call ukey usig ats)))) (check-walk fnode tenv) (reduce (fn [_ a] (check-walk a tenv) nil) nil args)) (= op :let) @@ -1185,7 +1270,7 @@ (check-walk (get node :body) tenv)) (= op :recur) (reduce (fn [_ a] (check-walk a tenv) nil) nil (get node :args)) - (= op :def) (check-walk (get node :init) tenv) + (= op :def) (do (register-user-fn! node) (check-walk (get node :init) tenv)) (= op :throw) (check-walk (get node :expr) tenv) (= op :vector) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items)) (= op :set) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items)) @@ -1219,13 +1304,22 @@ (defn check-form "Success-type check a single analyzed form (RFC 0006). Returns a vector of - diagnostics [{:op :argpos :type :msg} ...] for provably-wrong core-fn calls; - empty when nothing is provably wrong. Runs independently of specialization so - it is usable in normal builds (the decoupled checking path)." - [node] - (reset! diag-box []) - (check-walk node {}) - (vec @diag-box)) + diagnostics [{:op :argpos :type :msg} ...] for provably-wrong calls; empty + when nothing is provably wrong. Runs independently of specialization so it is + usable in normal builds (the decoupled checking path). + + With strict? true, also reports calls to registered user functions whose + concrete argument types provably make the body throw (jolt-zo1, opt-in, + closed-world). user-sig-box accumulates registered defs across forms, so a + def must precede its call — the same ordering RFC 0005 already assumes." + ([node] (check-form node false)) + ([node strict?] + (reset! strict-box (if strict? true false)) + (reset! checking-box #{}) + (reset! diag-box []) + (check-walk node {}) + (reset! strict-box false) + (vec @diag-box))) (defn infer-body "Type `body` under tenv (local-name -> type). Returns [ret-type node' calls], diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 7cdf9e3..678fe05 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -619,11 +619,17 @@ bug never breaks compilation, then reports each diagnostic per strictness: `warn` prints to stderr, `error` throws (failing this form's compilation). Because the checker only fires on PROVABLY-wrong code, a correct program has - nothing to report under either level." + nothing to report under either level. + + JOLT_TYPE_CHECK_USER (an orthogonal opt-in knob, jolt-zo1) additionally + reports calls to user functions whose concrete argument types provably make + the body throw — sound only under the closed-world assumption, hence opt-in." [ctx ir strictness ns] (def cf (ns-find (ctx-find-ns ctx "jolt.passes") "check-form")) (when cf - (def r (protect ((var-get cf) ir))) + (def uenv (os/getenv "JOLT_TYPE_CHECK_USER")) + (def strict? (and uenv (not= uenv "0") (not= uenv "off"))) + (def r (protect ((var-get cf) ir strict?))) (when (r 0) (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1))) (when (and diags (> (length diags) 0)) diff --git a/test/integration/type-check-test.janet b/test/integration/type-check-test.janet index b77f340..8c7e25f 100644 --- a/test/integration/type-check-test.janet +++ b/test/integration/type-check-test.janet @@ -18,6 +18,10 @@ (defn diags [src] (api/normalize-pvecs (check (backend/analyze-form ctx (reader/parse-string src))))) (defn nd [src] (length (diags src))) +# strict mode (jolt-zo1): also report provably-wrong calls to user fns +(defn nds [src] + (length (api/normalize-pvecs + (check (backend/analyze-form ctx (reader/parse-string src)) true)))) # --- provably wrong: REPORTED ------------------------------------------------ (assert (= 1 (nd "(inc \"x\")")) "inc on a string") @@ -60,6 +64,27 @@ (assert (= 0 (nd "(fn [c] (:r (if c {:r 1} {:g 2})))")) "keyword lookup over a struct union is accepted (no false positive)") +# --- user-function error domains (jolt-zo1), opt-in strict mode -------------- +# A call passing a provably-wrong type to a user fn whose body requires +# otherwise is reported ONLY in strict mode; the default level never fires on +# user fns (closed-world soundness boundary). +(assert (= 0 (nd "(do (defn ufa [x] (+ x 1)) (ufa \"s\"))")) + "user-fn wrong call NOT reported at the default level") +(assert (= 1 (nds "(do (defn ufa [x] (+ x 1)) (ufa \"s\"))")) + "strict: arithmetic fn called with a string is reported") +(assert (= 0 (nds "(do (defn ufb [x] (+ x 1)) (ufb 5))")) + "strict: same fn called with a number is accepted") +(assert (= 0 (nds "(do (defn ufc [x] (:k x)) (ufc \"s\"))")) + "strict: a body that uses the param leniently is not reported") +# cross-form: a def registered by an earlier check is visible to a later call +(nds "(defn ufd [x] (count x))") +(assert (= 1 (nds "(ufd 42)")) + "strict: cross-form call to a seq-only fn with a number is reported") +(assert (= 0 (nds "(do (defn ^:redef ufe [x] (+ x 1)) (ufe \"s\"))")) + "strict: a ^:redef fn is not a stable requirement, not reported") +(assert (= 1 (nds "(do (defn ufrec [x] (ufrec (+ x 1))) (ufrec \"s\"))")) + "strict: self-recursion terminates (cycle guard) and the (+ x 1) on a string is reported once") + # --- the diagnostic carries op + type + a message ---------------------------- (def one (in (diags "(inc \"x\")") 0)) (assert (= "inc" (get one :op)) "diagnostic names the op")