CLI Tools

The saple binary exposes six subcommands. Each is described below with the most common flags.

`saple parse`

Parse an SPL file and print its AST.

saple parse examples/dining_philosophers.sbl
saple parse examples/dining_philosophers.sbl --format json

`saple analyze`

The main command. Verifies properties and matches patterns declared in the specification — derived from the SPL file itself, no hardcoded checks.

# Basic
saple analyze examples/dining_philosophers.sbl

# Full execution trace
saple analyze examples/dining_philosophers.sbl --trace

# Extract reusable rules and export
saple analyze examples/dining_philosophers.sbl \
  --extract-rules --export rules.json

Flags

Flag	Default	Description
`--input NAME=VALUE`		Bind a concrete value to a symbolic input (repeatable). Use when a property or pattern only fires for specific inputs.
`--trace`	off	Show full execution trace
`--verbose`, `-v`	off	Show constraint checks and summaries
`--extract-rules`	off	Extract vulnerability rules from findings
`--export <PATH>`		Export rule database as JSON
`--no-auto-load`	off	Don't auto-load previously generated rules
`--arch <ARCH>`	auto	Architecture (auto-detected from file extension)
`--threads <N>`	0 (auto)	Number of threads
`--memory-budget-mb <N>`	512	Memory budget for caches (MB)
`--max-memo-entries <N>`	10000	Max entries for path memoization
`--solver-pool-size <N>`	0 (auto)	Solver pool size

`saple model`

Run forward or backward symbolic state-space exploration.

saple model examples/network_protocol_stack.sbl --mode forward
saple model examples/network_protocol_stack.sbl --mode backward --max-steps 200

`saple match`

Match a specification against a reusable pattern file.

saple match examples/dining_philosophers.sbl --pattern patterns/deadlock.sbl

`saple test`

Generate test cases with a chosen coverage criterion.

saple test examples/dining_philosophers.sbl                       # transition coverage (default)
saple test examples/dining_philosophers.sbl --coverage state
saple test examples/dining_philosophers.sbl --coverage path

`saple translate`

Translate external formats into SPL. Supported input representations:

x86-64 assembly — --arch x86-64
ARM64 / AArch64 assembly — --arch arm64
Clang / LLVM IR (C, C++, Rust front-ends) — --arch clang
VHDL hardware description — --arch vhdl
Blockchain smart contract source — --arch blockchain

saple translate firmware.s   --arch x86-64    --output firmware.sbl
saple translate binary.s     --arch arm64     -o binary.sbl
saple translate module.ll    --arch clang     -o module.sbl
saple translate design.vhd   --arch vhdl      -o design.sbl
saple translate contract.vy  --arch blockchain -o contract.sbl

Global flags

Flag	Description
`--format <FORMAT>`	Output format: `table` (default), `json`, `dot`
`--verbose`, `-v`	Verbose output