simon/jolt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: report provably-wrong calls to user functions, opt-in (jolt-zo1)

Browse source 
The success checker fired only against core-fn error domains (stable, not
redefinable). This adds reporting of a call that passes a provably-wrong
type to a USER fn whose body requires otherwise — e.g. a fn that only does
arithmetic on a param, called with a string.

As check-walk sees defs it registers each non-redefinable single-fixed-arity
user fn's {:params :body} in module state (user-sig-box, accumulating across
forms like rtenv-box — a def must precede its call). At a call site (strict
mode only) the body is re-checked with ONE parameter bound to its concrete
argument type, others :any; if that produces a diagnostic the all-:any body
did not, the argument alone is provably wrong and the call is reported.
Monotonic — binding a concrete type can only add error-domain hits — so still
no false positives. A cycle guard (checking-box) terminates mutual recursion.

Gated behind JOLT_TYPE_CHECK_USER (orthogonal to the warn/error level)
because it rests on the closed-world assumption, weaker than the core-fn
case. check-form gains a strict? arity; the default path is unchanged and
user-fn code runs only when the checker is enabled. ^:redef/^:dynamic and
multi/variadic fns are not registered (their body is no stable requirement).

Gate green, suite 4718, conformance 335/335.
This commit is contained in:
Yogthos 2026-06-13 11:56:21 -04:00
parent 9f076937af
commit 824b30defd
3 changed files with 138 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

116
jolt-core/jolt/passes.clj
View file

@ -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],

10
src/jolt/backend.janet
View file

@ -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))

25
test/integration/type-check-test.janet
View file

@ -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")