Skip to content
This repository was archived by the owner on Sep 8, 2026. It is now read-only.

nikos-tui.md

Latest commit

 

History

History
192 lines (150 loc) · 8.22 KB

nikos-tui.md

File metadata and controls

192 lines (150 loc) · 8.22 KB
Raw

NIKOS TUI Usage Guide

NTU-037: Interactive terminal analysis dashboard

Overview

npkc --tui launches an interactive terminal dashboard backed by ftxui. It runs NIKOS abstract interpretation analysis via npkc --analyze in the background and displays results in a live, keyboard-navigable interface.

npkc --tui myfile.npk
npkc --analyze --interactive myfile.npk    # same as --tui

Layout

┌─────────────────────────────────────────────────────────────────────────────┐
│ ◈ NIKOS Abstract Interpretation Dashboard                                   │  ← TitleBar
├─────────────────────────────────────────────────────────────────────────────┤
│ [TOTAL 42] [ERRORS 3] [WARNINGS 8] [OK 31] [UNRCH 0]      ⏱ 1.234s        │  ← SummaryBar
├─────────────────────────────────────────────────────────────────────────────┤
│ Filter: [__________]  ✗ Error  ⚠ Warning  ✓ OK  ∅ Unreachable   sort:status▲│  ← FilterBar
├─────────────────────────────────────────────────────────────────────────────┤
│ Status  │ Function                │ File:Line    │ Check       │ Description │
│─────────┼─────────────────────────┼──────────────┼─────────────┼────────────│
│ ✗ ERR   │ compute_divisor         │ algo.npk:42  │ check_dbz   │ Division…  │  ← CheckTable
│ ⚠ WARN  │ read_buffer             │ io.npk:88    │ check_boa   │ Buffer…    │
│ ✓ OK    │ init_values             │ main.npk:12  │ check_uva   │ All vars…  │
│ ⟳ Analyzing… (abstract interpretation running)                              │  ← Spinner
├─────────────────────────────────────────────────────────────────────────────┤
│   [error] check_dbz  compute_divisor          algo.npk:42                  │
│                                                                             │  ← DetailPanel
│   Division by zero is possible when n == 0                                 │
│   Call chain:                                                               │
│     ├ main @ main.npk:5                                                    │
│     └ compute_divisor @ algo.npk:42                                        │
├─────────────────────────────────────────────────────────────────────────────┤
│ npkc --tui │ myfile.npk              q=quit ?=help e=export t=timing s=sort │  ← StatusBar
└─────────────────────────────────────────────────────────────────────────────┘

Keybindings

Key Action
q Quit
j / ↓ Next row
k / ↑ Previous row
PgDn Page down (20 rows)
PgUp Page up (20 rows)
Enter Open detail panel for selected row
f Focus filter text input
s Cycle sort column (status→function→file→check)
S Toggle sort direction (ascending ▲ / descending ▼)
t Toggle IKOS phase timing bar chart
x Toggle cross-validation overlay
p Toggle warning promotion overlay
e Open export dialog (then h=HTML, j=JSON)
T Toggle dark/light color theme
? Toggle keybinding help overlay
Esc Close any overlay

Overlays

Timing (t)

Horizontal bar chart showing IKOS phase durations:

  • load_bc — bitcode loading
  • liveness — liveness analysis
  • widening_hint — widening hint computation
  • value_analysis — abstract value analysis
  • check — checker phase

Cross-Validation (x)

Table of Z3 vs IKOS verdict agreement for each check:

  • CONFIRMED — both Z3 and IKOS agree (error)
  • DISMISSED — both agree (safe)
  • IKOS-ONLY — IKOS found error, Z3 inconclusive
  • Z3-ONLY — Z3 found error, IKOS safe
  • INCONCLUSIVE — disagree or unknown

Warning Promotion (p)

List of warnings promoted to errors or dismissed by heuristic.

Export (e)

  • h — Write HTML report to <input>-nikos.html
  • j — Write JSON report to <input>-nikos.json

Filter Bar

Text filter: Type to search function names, check names, and descriptions.
Press f to focus the input; Esc to blur.

Status checkboxes:

  • ✗ Error — show/hide proven-unsafe checks (default: on)
  • ⚠ Warning — show/hide potentially-unsafe (default: on)
  • ✓ OK — show/hide proven-safe (default: off)
  • ∅ Unreachable — show/hide unreachable code (default: off)

Row count badge: Showing N / M in the top right of the filter bar.

Environment Variables

Variable Purpose
NPKC_PATH Path to npkc binary (auto-detected from executable sibling dir)
NIKOS_ANALYZER_PATH Path to ikos-analyzer binary

Minimum Terminal Size

  • Width: 80 columns (layout degrades gracefully at narrower sizes)
  • Height: 24 rows (recommended: 40+)

Build Prerequisites

The TUI requires NITPICK_HAS_TUI=ON (default) at cmake configure time. ftxui is fetched automatically via CMake FetchContent:

cmake -B build -DNITPICK_HAS_TUI=ON
cmake --build build --target npkc -j$(nproc)
./build/npkc --tui myfile.npk

To build without TUI (e.g. for CI):

cmake -B build -DNITPICK_HAS_TUI=OFF

Config File Integration (NCF-012/013)

When launched with --tui, npkc loads the NIKOS per-project config file before the TUI starts — the domain and checker settings are resolved at startup so the SummaryBar can display them immediately, before any analysis results arrive.

See nikos-config.md for the full config file reference.

SummaryBar Config Badge

The SummaryBar now includes a right-aligned cyan badge showing the active domain and checker count, positioned to the left of the timing display:

│ [TOTAL 42] [ERRORS 3] [WARNINGS 8] [OK 31] [UNRCH 0]   domain:octagon  checkers:14  ⏱ 1.234s │
  • domain:X reflects the domain field from the [nikos] config section (e.g. interval, octagon, var-pack-dbm).
  • checkers:N shows the count of active checkers. If the checkers field is omitted from the config (meaning all checkers run), N is the total number of built-in checkers (17 as of NIKOS 0.11).
  • The badge is rendered using the ftxui color::Cyan foreground attribute.
  • If no config file is found (built-in defaults apply), the badge still appears showing the defaults: domain:interval checkers:17.

Config Loading Sequence in TUI Mode

npkc --tui myfile.npk
│
├─ 1. Walk-up discovery: find nitpick.toml (or aria.toml)
│       aria.toml found → print deprecation warning to stderr, then continue
│
├─ 2. Parse [nikos] section; validate all fields
│       invalid field → print warning to stderr and use default for that field
│
├─ 3. Initialise ftxui TUI; render initial SummaryBar with domain/checker badge
│
└─ 4. Spawn npkc --analyze subprocess with resolved flags
        results streamed into CheckTable as they arrive

The TUI does not re-read the config file while running. To pick up config changes, quit (q) and relaunch.