Compiler Internals

Advanced topic. This page explains how CK turns source code into output and how its optimizer checks transformations. You do not need these details to write or run CK programs.

From source to artifact#

.ck source
  → lexer, parser, type checker, contracts
  → semantic MIR
  → mode- and consumer-specific KIR
  → verified O0–O3 optimization
  → Native LLVM / C source / WAT or WASM

The frontend produces stable diagnostics. Semantic MIR preserves evaluation order and possible checked failures. KIR adds explicit guards, effects, memory information, and proof-carrying facts for optimization.

Verified optimization#

At O0 the compiler constructs and verifies KIR without optional transforms. O1 adds control-flow simplification and scalar propagation. O2 adds effect-aware inlining and memory optimizations. O3 adds bounded specialization, loop work, unrolling, SLP, and supported fixed-width vectorization for Native and opt-in WebAssembly simd128 kernels.

Transforms that need a proof are checked against the current KIR state. A speculative candidate is accepted as a complete verified state or leaves the previous state intact. Unknown safety facts cause conservative output.

ckc emit-mir kernel.ck
ckc emit-kir kernel.ck -O3 --print-facts --explain-optimization

The emit-kir inspection view is deterministic. Native inspection can select a specific consumer and CPU policy. C and the WebAssembly baseline profile consume verified scalar KIR. With -O3 --wasm-features simd128, eligible WebAssembly loops can use verified Vector KIR and SIMD128 instructions; other loops keep scalar lowering. Native supports its own fixed-width Vector KIR subset.

Profiles guide cost, not correctness#

CK workload profiles may influence the expected benefit of an optimization. They cannot establish a range, no-alias, alignment, bounds, or other safety fact. Profile identity is validated before use. Learn more in PGO & CPU Variants.

For implementation details, read the compiler architecture and optimizer reference.