APEX

A deterministic systems programming language with compile-time performance contracts.

APEX is a compiled, statically-typed language targeting embedded and real-time systems. Its defining feature is a contract system — inline annotations on functions that the compiler proves hold before producing any binary. If the proof fails, the program does not compile.

@interrupt
@max_cycles(200)
@loop_bound(8)
@no_heap
fn USART1_IRQHandler() {
    let sr: i32 = uart_read_sr();
    if sr > 0 {
        let byte: i32 = uart_read_dr();
        let _echo: i32 = byte + 1;
    }
}

The compiler verifies this interrupt handler completes in ≤ 200 cycles, never allocates heap memory, and is safe to register in a bare-metal vector table — at compile time, not at runtime, not in a post-hoc tool.

---

Motivation

Embedded and real-time systems impose constraints that no mainstream language can express:

Requirement	C / Rust / Zig	APEX
Execution bounded by N cycles	Convention, comment	@max_cycles(N) — compiler-proven
No heap allocation in ISR	#[no_std] (file-level)	@no_heap — function-level, transitive
Timing determinism	Manual analysis	@deterministic_latency — compiler-checked
Interrupt handler correctness	Convention	@interrupt — enforces void return, no params, requires timing bound
Volatile MMIO stores	volatile cast	@volatile — all stores in function body emit volatile

STARK/Ada provides formal verification for similar properties. APEX trades completeness for ergonomics: contracts are inline, verification runs during cargo build, and requires no proof assistant expertise.

---

Language Overview

Types

// Scalars
let x: i8  = 0;    let y: i64 = 0;
let a: u32 = 0;    let b: f64 = 0.0;
let c: bool = true; let d: char = 'A';

// Sized arrays (stack-allocated)
let buf: [i32; 16] = [0];

// Raw pointers (for MMIO)
let gpio: *mut u32 = 0x40020014 as *mut u32;
let reg:  *u32     = 0x40020000 as *u32;

// Structs
struct RingBuffer {
    head: i32,
    count: i32,
    data: i32,
}

Functions and Contracts

// A pure mathematical function — no side effects, no heap
@pure
@no_heap
@max_cycles(15)
fn compute_ccr(duty: i64, arr: i64) -> i64 {
    return (duty * arr) / 1000;
}

// A sensor pipeline — contracts compose transitively
@pure
@no_heap
@max_cycles(60)   // includes callee max_cycles budgets
fn process_sensor(raw: i64, prev: i64) -> i64 {
    let clamped: i64 = clamp_adc(raw);          // @max_cycles(15)
    let filtered: i64 = low_pass(clamped, prev); // @max_cycles(25)
    return filtered;
}

Interrupt Handlers

@interrupt               // naked function, no_mangle, external linkage
@max_cycles(80)          // must complete within 80 cycles
@no_heap                 // zero allocation
@parallel_safe           // safe to execute alongside sensor reads
fn TIM1_UP_IRQHandler() {
    let new_duty: i64 = ramp_step(500, 750, 10);
    let ccr: i64 = compute_ccr(new_duty, 1000);
    let _write: i64 = ccr;  // real: volatile store to TIM1->CCR1
}

Extern Functions (C Interop)

extern "C" fn printf(fmt: string) -> i32;
extern "C" fn malloc(n: i64) -> *u8;

---

Contract System

All contracts are verified at compile time over the Typed Intermediate Representation (TIR) in Static Single Assignment form.

Contract	Description	Verification Method
@max_cycles(N)	Worst-case execution time ≤ N cycles	DFS over SSA CFG with target-aware cost table; includes callee @max_cycles budgets
@loop_bound(N)	Loop body executes ≤ N times	Required when @max_cycles is declared on a function containing a loop
@deterministic_latency	Best-case path cost == worst-case path cost	Computes (min_path, max_path) via independent DFS traversals; checks equality
@no_heap	No dynamic allocation in transitive call graph	Checks for malloc/free call sites recursively across all reachable callees
@max_alloc(N)	Heap allocation ≤ N bytes	Estimates allocation size via escape analysis; counts escaping non-copy locals
@interrupt	Void return, no parameters, must have @max_cycles	Structural check + cross-contract dependency enforcement
@volatile	All stores emit LLVM volatile store	Codegen flag set for all Store/PtrStore instructions in function body
@pure	No observable side effects	Checks for store instructions and calls to non-pure functions
@no_panic	No panic paths reachable	Checks for division-by-zero and array OOB at provably-constant operands
@no_overflow	Integer arithmetic does not overflow	Verifiable only for constant-constant operations in current implementation
@parallel_safe	Safe for concurrent execution	Checks for shared mutable state and non-atomic stores

Transitive Verification

Contracts propagate across call boundaries. When verifying @max_cycles(N) on function F:

• If F calls G and G has @max_cycles(M), the cost of Call(G) is M cycles.
• If G has no @max_cycles contract, verification of F fails with an error.
• If G is reachable from G (recursion), verification fails — WCET is undefined for recursive functions.

Target Cost Models

Instruction	Cortex-M3	x86-64	Generic
add / sub	1	1	1
mul	3	3	3
div / mod	12	20	20
load	4	4	5
store	4	4	5
branch	1	1	1
call	callee's @max_cycles	—	—

Select target with --target=cortex-m3 or --target=x86_64.

---

Architecture

Source (.apex)
    │
    ├──▶ Lexer → Parser → AST Optimizer
    │
    ├──▶ TypeChecker
    │       Type system: i8–u64, f32/f64, bool, char, string,
    │       void, [T;N], *T, *mut T, struct, enum, fn(...)→T
    │
    ├──▶ TIR Builder  (Braun et al. SSA construction)
    │       typed_ir: FieldLoad, FieldStore, PtrLoad,
    │       PtrStore, Index, Phi, BinOp, Compare, Call
    │
    ├──▶ Analysis Passes
    │       ├── EscapeAnalysis    → marks escaping locals for heap allocation
    │       ├── OwnershipInference → move detection (linear scan)
    │       └── CostAnalysis (cost.rs)
    │               ├── analyze_function_cost         → worst-case path
    │               ├── analyze_function_cost_range   → (min, max) for @deterministic_latency
    │               └── analyze_function_transitive_cost → inter-procedural WCET
    │
    ├──▶ ContractVerifier (contracts/verifier.rs)
    │       Verifies all 11 contract types. 921 lines, 40+ tests.
    │
    └──▶ LLVM Codegen (inkwell, LLVM 21)
            ├── SSA → LLVM IR
            ├── Escape wiring → malloc for escaping non-copy locals
            ├── @interrupt → naked + external linkage attributes
            ├── @volatile → volatile store flag on all Store instructions
            └── --no-std + --linker-script → bare-metal output

---

Building

Requirements:

• Rust (stable toolchain, 2021 edition)
• LLVM 21 (llvm-config on PATH, or override via LLVM_SYS_210_PREFIX)

# Clone and build
git clone https://github.com/[TBD]/apex
cd apex
cargo build --release

# Run all tests
cargo test

# Compile an APEX program
./target/release/apex compile program.apex

# Inspect TIR / LLVM IR
./target/release/apex ir program.apex

# Check contracts only (no codegen)
./target/release/apex check program.apex

# Analyze escape + ownership
./target/release/apex analyze program.apex

# Bare-metal embedded target
./target/release/apex compile \
    --target=cortex-m3 \
    --no-std \
    --linker-script=memory.ld \
    uart_isr.apex

macOS (Homebrew):

brew install llvm@21
export LLVM_SYS_210_PREFIX="$(brew --prefix llvm@21)"
cargo build --release

---

Examples

All examples are in tests/integration/.

Arithmetic and basics

// tests/integration/arithmetic.apex
fn add(a: i64, b: i64) -> i64 {
    return a + b;
}
fn main() {
    print_i64(add(3, 4));
}

Performance contracts

// tests/integration/contracts.apex
@pure
@no_heap
fn square(x: i64) -> i64 {
    return x * x;
}

Sensor filter (embedded)

// tests/integration/sensor_filter.apex
@pure @no_heap @max_cycles(60)
fn process_sensor(raw: i64, prev: i64) -> i64 {
    let clamped: i64 = clamp_adc(raw);
    let filtered: i64 = low_pass(clamped, prev);
    return filtered;
}

UART ISR (bare-metal)

// tests/integration/uart_isr.apex
@interrupt @max_cycles(200) @loop_bound(8) @no_heap
fn USART1_IRQHandler() { ... }

Timer PWM controller

// tests/integration/timer_pwm.apex
@interrupt @max_cycles(80) @no_heap @parallel_safe
fn TIM1_UP_IRQHandler() { ... }

---

Project Status

Component	Status
Lexer + Parser	✅ Complete
Type system (scalars, arrays, pointers, structs, enums)	✅ Complete
SSA IR (Braun et al.)	✅ Complete
LLVM codegen (x86-64, Cortex-M3)	✅ Complete
Escape analysis → heap allocation	✅ Wired
Ownership / move detection	✅ Complete
@max_cycles with transitive inter-procedural WCET	✅ Complete
@loop_bound enforcement	✅ Complete
@deterministic_latency	✅ Complete
@interrupt codegen (naked + no_mangle)	✅ Complete
@volatile LLVM volatile stores	✅ Complete
@no_heap, @max_alloc, @pure, @no_panic	✅ Complete
Struct field access in TIR + codegen (GEP)	✅ Complete
Pointer dereference + address-of	✅ Complete
--no-std + --linker-script	✅ Complete
Match expression lowering	🔶 Partial (reports error, returns void)
Generic functions (monomorphization)	✅ Complete — single type parameter, inferred at call site, zero overhead
Module system (use "path.apex")	✅ Complete — recursive file loading, canonical deduplication, cycle detection
Hardware-validated cost tables	⏳ Pending measurement

Test suite: 119 passing, 0 failing.

---

Research Direction

APEX is the subject of active research targeting publication at LCTES 2027 (Languages, Compilers, and Tools for Embedded Systems).

Research claim:

Compile-time WCET verification via contract-annotated SSA analysis can be integrated into a practical systems programming language without prohibitive annotation burden or proof assistant expertise.

Paper outline: see docs/paper/wcet_contracts.md (in progress).

Key open question: How accurately do the static cost tables predict actual cycle counts on real ARM Cortex-M3 hardware? Calibration against DWT cycle counter measurements on an STM32F103 Nucleo board is the primary pending evaluation step.

---

Repository Structure

apex/
├── src/
│   ├── main.rs                        CLI: compile / check / ir / analyze
│   └── compiler/
│       ├── lexer.rs                   Tokenizer
│       ├── parser.rs                  Recursive descent parser
│       ├── ast.rs                     AST node types
│       ├── typechecker.rs             Type inference + struct registry
│       ├── optimizer.rs               AST-level constant folding
│       ├── codegen.rs                 LLVM IR emission via inkwell
│       ├── diagnostics.rs             Error formatting
│       ├── ir/
│       │   ├── typed_ir.rs            TIR node types (SSA instructions, contracts)
│       │   └── tir_builder.rs         AST → SSA TIR (Braun et al.)
│       ├── analysis/
│       │   ├── escape.rs              Escape analysis (stack vs. heap decision)
│       │   ├── ownership.rs           Move detection
│       │   └── cost.rs                Cycle-cost analysis (WCET, range, transitive)
│       └── contracts/
│           └── verifier.rs            Contract verification engine (921 lines)
├── tests/
│   └── integration/                   .apex programs for end-to-end testing
│       ├── uart_isr.apex              UART receive ISR
│       ├── timer_pwm.apex             Timer PWM controller
│       ├── sensor_filter.apex         Moving average + low-pass filter
│       └── ...                        (20+ programs)
├── docs/
│   ├── decisions/                     Architecture Decision Records (ADR-001 to ADR-003)
│   ├── specs/grammar.ebnf             Formal language grammar
│   └── philosophy/                    Design principles
└── tools/
    └── llvm-config-wrapper.sh         LLVM version negotiation helper

---

Design Decisions

Full rationale for major architectural choices is documented in docs/decisions/:

• ADR-001 — LLVM via inkwell over Cranelift / custom backend
• ADR-002 — TIR as a typed SSA IR between AST and LLVM
• ADR-003 — Memory model and ownership strategy

---

License

To be determined.

---

APEX — Autonomous Program Evolution eXaminer Built with inkwell (LLVM 21 Rust bindings) Source: github.com/Saurav0989/apex