Nitpick Compiler (npkc) Specification

The npkc compiler (v0.8.4) offers a comprehensive suite of flags for emitting different target binaries, enabling static verification, tuning memory management, and integrating with external analysis tools (like Z3 and NIKOS).

1. Core Compilation Options

Basic commands dictate the final compilation target and format.

• -o <file> : Specify the output filename.
• -c : Compile as a library module. The compiler will not look for or require a main or failsafe function.
• --shared : Compile to a shared dynamic library (.so).
• --static : Link as a fully static executable.
• -I, --search-path <dir> : Add a directory to the module search path for use imports.
• -l<library> : Link against an external library (e.g., -lm, -lpthread).
• -L<path> : Add a library search path.
• -Wl,<option> : Pass specific options directly to the linker.
• --incremental : Build performance feature. Caches per-module IR to skip unchanged files on rebuild.
• --cache-dir=<dir> : Sets the IR cache directory (default is .npk-cache).

2. Emitting Formats (Targets)

Nitpick supports compiling to CPU, GPU, and WebAssembly targets, as well as emitting intermediate files.

• --emit-llvm : Emit LLVM IR text (.ll).
• --emit-llvm-bc : Emit LLVM bitcode (.bc).
• --emit-asm : Emit raw assembly (.s).
• --emit-deps : Emit JSON dependency manifest (useful for build systems like npkbld / aria_make).
• --emit-ptx : Emit PTX assembly for GPU execution.
• --emit-wasm : Compile to WebAssembly (.wasm).

2.1 GPU/WASM Target Tuning

• --target=<arch> : Target architecture. Valid options: cpu, gpu, gpu+cpu, wasm32-wasi, wasm32-unknown-unknown.
• --gpu-arch=<sm> : Set the CUDA compute capability (e.g., sm_50, sm_86, sm_90).
• --gpu-opt=<lvl> : GPU optimization level (0-3).

3. Optimization & Debugging

• -O<level> : General optimization level, from 0 (none) to 3 (max).
• -g : Emit DWARF debug information. Necessary for debuggers like npk-dap.
• -v, --verbose : Enable verbose compiler output.
• -E : Run the preprocessor only, outputting the result to stdout.
• --ast-dump : Dump the Abstract Syntax Tree (AST) to stdout and exit.
• --tokens : Dump lexical tokens to stdout and exit.
• --expand-macros : Dump post-expansion macro trace.
• --borrow-debug : Emit internal borrow checker debug diagnostics to stderr.
• --borrow-dump : Dump borrow state visualization after analysis.

4. Formal Verification (Z3 SMT Solver)

Nitpick uses the Z3 SMT solver natively to enforce compile-time constraints, memory limits, and Design-by-Contract assertions (requires, ensures, invariant).

• --verify : Enable static verification of limit<Rules> constraints and base proofs.
• --verify-contracts : Verify function pre- and post-conditions (requires/ensures) and loop invariants.
• --verify-overflow : Verify that integer arithmetic cannot overflow under any possible execution path.
• --verify-concurrency : Verify freedom from data races and deadlocks.
• --verify-memory : Verify freedom from use-after-free and recursion bounds.
• --verify-level=N : Set the depth of verification (0 = none, 1 = fast, 2 = standard, 3 = thorough).
• --verify-report : Emit detailed proof results.
• --prove-report : Emit report of prove/assert_static outcomes.
• --smt-opt : Enable SMT-guided optimizations (the compiler strips runtime checks it can prove are 100% mathematically safe).
• --smt-timeout=N : Per-query Z3 timeout in milliseconds (default: 5000).

5. Abstract Interpretation (NIKOS/IKOS)

The compiler natively integrates NIKOS for abstract interpretation to verify properties the borrow checker cannot guarantee alone (like divide-by-zero, deep buffer overflow, and nullity).

• --verify-nikos : Run NIKOS after codegen (implied by --verify-level=3).
• --analyze / -A : Run NIKOS analysis only (skips linking/outputting binaries).
• --nikos-domain=<name> : Sets abstract domain constraints (e.g., interval, gauge, apron-octagon, apron-polyhedra).
• --nikos-checkers=<list> : Select which checkers to run (e.g., dbz, sio, nullity, boa).
• --tui / --analyze --interactive : Launch the interactive terminal analysis dashboard.

6. Runtime Auditing & Memory Diagnostics

Flags to enforce security parameters and analyze memory utilization at runtime.

• --seccomp : Install a seccomp-bpf sandbox into the binary, restricting system calls to a strict allowlist.
• --wild-stats : Print unmanaged (wild) memory statistics at program exit.
• --guard-pages : Enable memory guard pages around wild allocations to catch out-of-bounds access.
• --wildx-audit : Log executable memory (wildx) alloc/seal/exec/free lifecycle events to stderr.
• --wildx-guard-pages : Wrap executable memory regions in guard pages.
• --gc-stats : Print garbage collector statistics at program exit.
• --gc-nursery-size=N : Adjust GC nursery size (default: 4MB).
• --gc-threshold=N : Major GC trigger threshold (default: 64MB).
• --gc-max-heap=N : Maximum total heap size.

7. Warnings

• -picky / --picky / --extra-picky : Enables maximum pedantic strictness by automatically passing -Wall and -Werror under the hood. Supports parameterization to downgrade (warn-<rule>) or disable (no-<rule>) specific rules. For example, --extra-picky=warn-shadow,no-wild makes shadowing a warning and completely disables the wild memory check. Valid rules: literal-suffixes, explicit-widening, shadow, wild.
• -Wall : Enable all warnings.
• -Werror : Treat all warnings as compilation errors.
• -W<warning> : Enable a specific warning.
• -Wno-<warning> : Disable a specific warning.