feat: success checker on by default in direct-link builds, free (jolt audit)
Checking inherently needs an inference pass (~2.6x compile as a standalone pass). But direct-link builds ALREADY run one inference pass for specialization (run-passes' infer-top), so checking can ride along: set a check-mode flag, turn checking? on during that existing pass, and collect the diagnostics after — ~2% overhead measured on the ray tracer, vs 2.6x for the separate pass. So the checker now defaults to `warn` in direct-link builds (where it's nearly free) and stays OFF in plain REPL/dev builds (no inference to ride, no forced cost — opt in with JOLT_TYPE_CHECK there). JOLT_TYPE_CHECK still overrides in both directions (off to disable, error to escalate). It checks the POST-optimization IR, which matches what the optimized program actually evaluates — scalar-replace only drops provably-pure code, an accepted opt-mode divergence, so no real error is hidden. The loaders enable position tracking whenever checking will run (env-selected or direct-link). type-check! (the standalone pass) stays for plain builds; both paths share report-diags!. cli-test pins: plain build silent, direct-link warns by default, JOLT_TYPE_CHECK=off disables. Gate green, suite 4718, runtime bench even.
This commit is contained in:
parent
69af83da89
commit
088232b778
6 changed files with 111 additions and 35 deletions
|
|
@ -1311,6 +1311,21 @@
|
||||||
(get fnode :arities))))
|
(get fnode :arities))))
|
||||||
def-node)))
|
def-node)))
|
||||||
|
|
||||||
|
;; Piggyback checking (jolt audit). In direct-link mode infer-top already runs
|
||||||
|
;; one inference pass for specialization; turning checking? on during it makes
|
||||||
|
;; the success checker nearly free there (no extra traversal — just the
|
||||||
|
;; per-call error-domain predicates). The back end sets the mode before
|
||||||
|
;; run-passes and reads take-diags! after. It checks the POST-optimization IR,
|
||||||
|
;; which matches what the optimized program actually evaluates (scalar-replace
|
||||||
|
;; only drops provably-pure code, an accepted opt-mode divergence).
|
||||||
|
(def ^:private check-mode-box (atom {:on false :strict false}))
|
||||||
|
(defn set-check-mode!
|
||||||
|
"Enable/disable checking during the next run-passes inference (direct-link)."
|
||||||
|
[on strict?] (reset! check-mode-box {:on (if on true false) :strict (if strict? true false)}))
|
||||||
|
(defn take-diags!
|
||||||
|
"Diagnostics accumulated by the last checking run-passes; clears the buffer."
|
||||||
|
[] (let [d (vec @diag-box)] (reset! diag-box []) d))
|
||||||
|
|
||||||
(defn run-passes
|
(defn run-passes
|
||||||
"All passes, in order. The back end applies this to every analyzed form. When
|
"All passes, in order. The back end applies this to every analyzed form. When
|
||||||
inlining is enabled for the unit (user code under direct-linking, jolt-87f),
|
inlining is enabled for the unit (user code under direct-linking, jolt-87f),
|
||||||
|
|
@ -1327,5 +1342,15 @@
|
||||||
(if (and @dirty (< i 8))
|
(if (and @dirty (< i 8))
|
||||||
(recur (inc i) n2)
|
(recur (inc i) n2)
|
||||||
n2)))]
|
n2)))]
|
||||||
(infer-top opt))
|
;; specialization inference, optionally also emitting success diagnostics
|
||||||
|
(if (get @check-mode-box :on)
|
||||||
|
(do (reset! diag-box [])
|
||||||
|
(reset! checking-box #{})
|
||||||
|
(reset! strict-box (get @check-mode-box :strict))
|
||||||
|
(reset! checking? true)
|
||||||
|
(let [r (infer-top opt)]
|
||||||
|
(reset! checking? false)
|
||||||
|
(reset! strict-box false)
|
||||||
|
r))
|
||||||
|
(infer-top opt)))
|
||||||
(const-fold node)))
|
(const-fold node)))
|
||||||
|
|
|
||||||
|
|
@ -369,8 +369,10 @@
|
||||||
Returns the result of the last form evaluated."
|
Returns the result of the last form evaluated."
|
||||||
[ctx s &opt file]
|
[ctx s &opt file]
|
||||||
(default file "<eval>")
|
(default file "<eval>")
|
||||||
# record form positions so the checker can report file:line:col (jolt-fqy)
|
# record form positions so the checker can report file:line:col (jolt-fqy).
|
||||||
(when (checker-enabled?)
|
# The checker is on when JOLT_TYPE_CHECK selects it, OR by default in
|
||||||
|
# direct-link builds (where it piggybacks on inference for free).
|
||||||
|
(when (or (checker-enabled?) (get (ctx :env) :inline?))
|
||||||
(track-positions! true)
|
(track-positions! true)
|
||||||
(put (ctx :env) :tc-source s)
|
(put (ctx :env) :tc-source s)
|
||||||
(put (ctx :env) :tc-file file))
|
(put (ctx :env) :tc-file file))
|
||||||
|
|
|
||||||
|
|
@ -613,13 +613,32 @@
|
||||||
[ctx]
|
[ctx]
|
||||||
(build-compiler! ctx))
|
(build-compiler! ctx))
|
||||||
|
|
||||||
(defn type-check!
|
(defn- report-diags!
|
||||||
"Success-type check the analyzed IR (RFC 0006). Looks up jolt.passes/check-form
|
"Render and emit success-type diagnostics (RFC 0006) at the given strictness:
|
||||||
(absent during pre-passes bootstrap -> no-op), runs it protected so a checker
|
|
||||||
bug never breaks compilation, then reports each diagnostic per strictness:
|
|
||||||
`warn` prints to stderr, `error` throws (failing this form's compilation).
|
`warn` prints to stderr, `error` throws (failing this form's compilation).
|
||||||
Because the checker only fires on PROVABLY-wrong code, a correct program has
|
file:line:col when the diagnostic carries an offset and the source is on the
|
||||||
nothing to report under either level.
|
env (jolt-fqy); else the ns."
|
||||||
|
[ctx diags strictness ns]
|
||||||
|
(def src (get (ctx :env) :tc-source))
|
||||||
|
(def file (or (get (ctx :env) :tc-file) (and ns (string ns))))
|
||||||
|
(each d diags
|
||||||
|
(def off (get d :pos))
|
||||||
|
(def loc
|
||||||
|
(if (and off src)
|
||||||
|
(let [lc (r/line-col src off)]
|
||||||
|
(string (or file "?") ":" (in lc 0) ":" (in lc 1)))
|
||||||
|
(string "in " (if ns (string ns) "?"))))
|
||||||
|
(def msg (string "type error " loc ": " (get d :msg)))
|
||||||
|
(if (= strictness "error")
|
||||||
|
(error msg)
|
||||||
|
(eprint " " msg))))
|
||||||
|
|
||||||
|
(defn type-check!
|
||||||
|
"Decoupled success-type check (RFC 0006): run jolt.passes/check-form as its OWN
|
||||||
|
inference pass over `ir` and report. Used in NON-direct-link builds, where the
|
||||||
|
optimization inference doesn't run — so checking costs a separate pass. (In
|
||||||
|
direct-link builds checking piggybacks on run-passes' inference instead, near
|
||||||
|
free; see analyze-form.) Protected so a checker bug never breaks compilation.
|
||||||
|
|
||||||
JOLT_TYPE_CHECK_USER (an orthogonal opt-in knob, jolt-zo1) additionally
|
JOLT_TYPE_CHECK_USER (an orthogonal opt-in knob, jolt-zo1) additionally
|
||||||
reports calls to user functions whose concrete argument types provably make
|
reports calls to user functions whose concrete argument types provably make
|
||||||
|
|
@ -633,23 +652,7 @@
|
||||||
(when (r 0)
|
(when (r 0)
|
||||||
(def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1)))
|
(def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1)))
|
||||||
(when (and diags (> (length diags) 0))
|
(when (and diags (> (length diags) 0))
|
||||||
# source + file for offset -> line:col (jolt-fqy). The loader stashes the
|
(report-diags! ctx diags strictness ns)))))
|
||||||
# current file's source + path on the env when checking is on.
|
|
||||||
(def src (get (ctx :env) :tc-source))
|
|
||||||
(def file (or (get (ctx :env) :tc-file) (and ns (string ns))))
|
|
||||||
(each d diags
|
|
||||||
(def off (get d :pos))
|
|
||||||
# precise: file:line:col of the offending form when its offset and the
|
|
||||||
# source are both available; else the ns (no worse than before)
|
|
||||||
(def loc
|
|
||||||
(if (and off src)
|
|
||||||
(let [lc (r/line-col src off)]
|
|
||||||
(string (or file "?") ":" (in lc 0) ":" (in lc 1)))
|
|
||||||
(string "in " (if ns (string ns) "?"))))
|
|
||||||
(def msg (string "type error " loc ": " (get d :msg)))
|
|
||||||
(if (= strictness "error")
|
|
||||||
(error msg)
|
|
||||||
(eprint " " msg)))))))
|
|
||||||
|
|
||||||
(defn analyze-form
|
(defn analyze-form
|
||||||
"Run the portable Clojure analyzer (jolt.analyzer/analyze) on a reader form,
|
"Run the portable Clojure analyzer (jolt.analyzer/analyze) on a reader form,
|
||||||
|
|
@ -683,6 +686,21 @@
|
||||||
# Resolved lazily; absent during the pre-passes bootstrap window.
|
# Resolved lazily; absent during the pre-passes bootstrap window.
|
||||||
(def pv (unless (= "1" (os/getenv "JOLT_NO_IR_PASSES"))
|
(def pv (unless (= "1" (os/getenv "JOLT_NO_IR_PASSES"))
|
||||||
(ns-find (ctx-find-ns ctx "jolt.passes") "run-passes")))
|
(ns-find (ctx-find-ns ctx "jolt.passes") "run-passes")))
|
||||||
|
# Success-type checking level (RFC 0006). JOLT_TYPE_CHECK wins when set;
|
||||||
|
# otherwise it defaults to `warn` in direct-link builds — where the
|
||||||
|
# optimization inference already runs, so checking piggybacks on it for nearly
|
||||||
|
# free — and stays OFF for plain REPL/dev builds (no inference -> no free ride;
|
||||||
|
# opt in with JOLT_TYPE_CHECK there). (jolt audit)
|
||||||
|
(def tc (os/getenv "JOLT_TYPE_CHECK"))
|
||||||
|
(def tc-off (or (= tc "off") (= tc "0")))
|
||||||
|
(def direct-link? (if (get (ctx :env) :inline?) true false))
|
||||||
|
(def level (cond tc-off nil tc tc direct-link? "warn" true nil))
|
||||||
|
(def uenv (os/getenv "JOLT_TYPE_CHECK_USER"))
|
||||||
|
(def strict? (and uenv (not= uenv "0") (not= uenv "off") true))
|
||||||
|
# piggyback: check DURING run-passes' inference (direct-link, the cheap path)
|
||||||
|
(def piggyback? (and level direct-link? pv true))
|
||||||
|
(def scm (and piggyback? (ns-find (ctx-find-ns ctx "jolt.passes") "set-check-mode!")))
|
||||||
|
(when scm ((var-get scm) true strict?))
|
||||||
(def result
|
(def result
|
||||||
(if pv
|
(if pv
|
||||||
(let [pr (protect ((var-get pv) (r 1) ctx))]
|
(let [pr (protect ((var-get pv) (r 1) ctx))]
|
||||||
|
|
@ -692,13 +710,19 @@
|
||||||
(ctx-set-current-ns ctx saved-ns)
|
(ctx-set-current-ns ctx saved-ns)
|
||||||
(if (pr 0) (pr 1) (r 1)))
|
(if (pr 0) (pr 1) (r 1)))
|
||||||
(r 1)))
|
(r 1)))
|
||||||
# Success-type check (RFC 0006), decoupled from specialization: runs whenever
|
(when scm ((var-get scm) false false))
|
||||||
# JOLT_TYPE_CHECK is warn/error, regardless of :inline?. Read at runtime so it
|
(cond
|
||||||
# needs no rebuild. The analyzed IR (r 1) carries no specialization; the
|
# direct-link: collect the diagnostics infer-top emitted and report them
|
||||||
# checker does its own inference.
|
piggyback?
|
||||||
(def tc (os/getenv "JOLT_TYPE_CHECK"))
|
(let [td (ns-find (ctx-find-ns ctx "jolt.passes") "take-diags!")]
|
||||||
(when (and tc (not= tc "off") (not= tc "0"))
|
(when td
|
||||||
(type-check! ctx (r 1) tc saved-ns))
|
(def raw ((var-get td)))
|
||||||
|
(def diags (if (pv/pvec? raw) (pv/pv->array raw) raw))
|
||||||
|
(when (and diags (> (length diags) 0))
|
||||||
|
(report-diags! ctx diags level saved-ns))))
|
||||||
|
# plain build with checking explicitly requested: a separate inference pass
|
||||||
|
(and level (not direct-link?))
|
||||||
|
(type-check! ctx (r 1) level saved-ns))
|
||||||
result)
|
result)
|
||||||
|
|
||||||
# The analyzer's deliberate punt signal — (uncompilable why) throws the string
|
# The analyzer's deliberate punt signal — (uncompilable why) throws the string
|
||||||
|
|
|
||||||
|
|
@ -377,7 +377,7 @@
|
||||||
(def toplevel (get (ctx :env) :toplevel-eval))
|
(def toplevel (get (ctx :env) :toplevel-eval))
|
||||||
# a require runs nested inside an outer file's eval; save/restore the outer
|
# a require runs nested inside an outer file's eval; save/restore the outer
|
||||||
# checker source so its later forms still convert offsets correctly (jolt-fqy)
|
# checker source so its later forms still convert offsets correctly (jolt-fqy)
|
||||||
(def checking (checker-enabled?))
|
(def checking (or (checker-enabled?) (get (ctx :env) :inline?)))
|
||||||
(def saved-src (and checking (get (ctx :env) :tc-source)))
|
(def saved-src (and checking (get (ctx :env) :tc-source)))
|
||||||
(def saved-file (and checking (get (ctx :env) :tc-file)))
|
(def saved-file (and checking (get (ctx :env) :tc-file)))
|
||||||
(when checking
|
(when checking
|
||||||
|
|
|
||||||
|
|
@ -112,7 +112,7 @@
|
||||||
(load-ns ctx filepath) → namespace symbol string"
|
(load-ns ctx filepath) → namespace symbol string"
|
||||||
[ctx filepath]
|
[ctx filepath]
|
||||||
(def source (slurp filepath))
|
(def source (slurp filepath))
|
||||||
(when (checker-enabled?)
|
(when (or (checker-enabled?) (get (ctx :env) :inline?))
|
||||||
(track-positions! true)
|
(track-positions! true)
|
||||||
(put (ctx :env) :tc-source source)
|
(put (ctx :env) :tc-source source)
|
||||||
(put (ctx :env) :tc-file filepath))
|
(put (ctx :env) :tc-file filepath))
|
||||||
|
|
|
||||||
|
|
@ -118,6 +118,31 @@
|
||||||
r)
|
r)
|
||||||
(has "could not find method"))
|
(has "could not find method"))
|
||||||
|
|
||||||
|
# --- success checker default-on in direct-link, off in plain builds ----------
|
||||||
|
# A provably-wrong defn (never called, so no runtime error): the checker is the
|
||||||
|
# only thing that can flag it. Plain build = silent (no dev regression);
|
||||||
|
# direct-link build = warns by default (free piggyback on inference).
|
||||||
|
(def tcw (string (or (os/getenv "TMPDIR") "/tmp") "/jolt-tcwarn-" (os/time) ".clj"))
|
||||||
|
(spit tcw "(ns tcw)\n\n(defn unused [s]\n (inc \"definitely-not-a-number\"))\n")
|
||||||
|
(check "plain build does not run the checker (no regression)"
|
||||||
|
(run-err tcw)
|
||||||
|
(fn [s] (nil? (string/find "type error" s))))
|
||||||
|
(check "direct-link build warns by default (free checking)"
|
||||||
|
(do (os/setenv "JOLT_DIRECT_LINK" "1")
|
||||||
|
(def r (run-err tcw))
|
||||||
|
(os/setenv "JOLT_DIRECT_LINK" nil)
|
||||||
|
r)
|
||||||
|
(fn [s] (and (string/find "type error" s)
|
||||||
|
(string/find "requires a number" s))))
|
||||||
|
(check "JOLT_TYPE_CHECK=off disables it even in direct-link"
|
||||||
|
(do (os/setenv "JOLT_DIRECT_LINK" "1")
|
||||||
|
(os/setenv "JOLT_TYPE_CHECK" "off")
|
||||||
|
(def r (run-err tcw))
|
||||||
|
(os/setenv "JOLT_DIRECT_LINK" nil)
|
||||||
|
(os/setenv "JOLT_TYPE_CHECK" nil)
|
||||||
|
r)
|
||||||
|
(fn [s] (nil? (string/find "type error" s))))
|
||||||
|
|
||||||
(if (> fails 0)
|
(if (> fails 0)
|
||||||
(error (string "cli-test: " fails " failing check(s)"))
|
(error (string "cli-test: " fails " failing check(s)"))
|
||||||
(print "\nAll CLI tests passed!"))
|
(print "\nAll CLI tests passed!"))
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue