Skip to content

nikos-lsp-protocol.md

Latest commit

 

History

History
236 lines (181 loc) · 7.14 KB

nikos-lsp-protocol.md

File metadata and controls

236 lines (181 loc) · 7.14 KB
Raw

NIKOS LSP Protocol Specification

NLS-023/028: Wire format documentation for editor plugin authors

Overview

npk-ls (the Nitpick Language Server) emits NIKOS abstract interpretation diagnostics as standard LSP textDocument/publishDiagnostics notifications. This document describes the trigger, wire format, and filtering metadata.

Trigger

NIKOS analysis runs automatically on textDocument/didSave. It does not run on didChange (to avoid blocking on slow abstract interpretation during typing).

Typical latency: 1–5 seconds depending on program size and domain.

Wire Format

All messages use the standard LSP JSON-RPC 2.0 framing over stdio:

Content-Length: <N>\r\n
\r\n
<N bytes of UTF-8 JSON>

textDocument/publishDiagnostics Notification

One notification is sent per source file that has NIKOS findings.

{
  "jsonrpc": "2.0",
  "method": "textDocument/publishDiagnostics",
  "params": {
    "uri": "file:///absolute/path/to/file.npk",
    "diagnostics": [
      {
        "range": {
          "start": { "line": 4, "character": 8 },
          "end":   { "line": 4, "character": 9 }
        },
        "severity": 1,
        "source": "nikos-abstract",
        "code": "check_dbz",
        "message": "Division by zero  [in main]",
        "relatedInformation": [
          {
            "location": {
              "uri": "file:///absolute/path/to/file.npk",
              "range": {
                "start": { "line": 4, "character": 8 },
                "end":   { "line": 4, "character": 9 }
              }
            },
            "message": "call chain: main @ file.npk:5"
          }
        ]
      }
    ]
  }
}

Severity Mapping

NIKOS Status LSP Severity Integer Description
error Error 1 Proven unsafe by abstract interpretation
warning Warning 2 Potentially unsafe (inconclusive)
ok (not emitted) — Proven safe — suppressed to reduce noise
unreachable (not emitted) — Code is unreachable — suppressed

Only error and warning status results are sent to the editor.

Source and Code Fields

Every NIKOS diagnostic has:

Field Value Purpose
source "nikos-abstract" Identifies the origin; allows per-source filtering in VS Code
code "check_dbz", "check_sio", etc. Checker name; editors can link to docs

Checker Codes

Code Checker
check_dbz Division by Zero
check_boa Buffer Overflow
check_null_dereference Null Pointer Dereference
check_sio Signed Integer Overflow
check_uio Unsigned Integer Overflow
check_shc Shift Count
check_poa Pointer Overflow
check_upa Pointer Alignment
check_uva Uninitialized Variable
check_pcmp Pointer Comparison
check_dca Dead Code
check_dfa Double Free
check_fca Invalid Function Call
check_watch Memory Watch

Configuration

npk-ls respects the following environment variables:

Variable Purpose Default
NPKC_PATH Path to npkc binary Auto-detected (sibling dir or PATH)
NIKOS_ANALYZER_PATH Path to ikos-analyzer binary Auto-detected by npkc

Incremental Mode (NLS-026)

npk-ls maintains a per-file result cache (last check count). If the analysis produces the same number of diagnostics as the previous run, the notification is suppressed to reduce editor flicker. This is a lightweight heuristic — the cache is reset when the editor reconnects.

Example Session

→  Client sends: textDocument/didSave { textDocument: { uri: "file:///project/main.npk" } }
←  Server logs:  [nikos-lsp] Running NIKOS via: /usr/local/bin/npkc --analyze /project/main.npk
←  Server logs:  [nikos-lsp] Published 2 NIKOS diagnostic(s) for: file:///project/main.npk
←  Server sends: textDocument/publishDiagnostics { uri: "...", diagnostics: [...] }

Per-Project Config (nitpick.toml) (NCF-025)

npk-ls integrates with the NIKOS config file system described in nikos-config.md. The config file controls which flags are forwarded to the npkc --analyze subprocess on each textDocument/didSave.

On initialize

When the editor sends the initialize request, npk-ls performs a walk-up from the workspace root directory to locate a config file:

  1. Searches each ancestor directory for nitpick.toml (checked first, silently).
  2. If not found, checks for aria.toml and prints a deprecation warning to the language server log channel: 
    [npk-ls] warning: aria.toml is deprecated; rename to nitpick.toml
  3. If both files are present in the same directory, nitpick.toml wins and aria.toml is ignored without a warning.
  4. The resolved [nikos] values are cached in memory for the lifetime of the session (until the next reload event).

On workspace/didChangeConfiguration

When npk-ls receives a workspace/didChangeConfiguration notification (typically sent by the editor when the user saves the config file or changes workspace settings), it:

  1. Re-reads the config file from disk using the same walk-up logic.
  2. Validates all [nikos] fields.
  3. Updates the in-memory cache with the new values.
  4. The updated config takes effect on the next textDocument/didSave- triggered analysis — any in-flight analysis is not interrupted.

Deprecation Warning for aria.toml

If aria.toml is discovered (and no nitpick.toml overrides it), a warning diagnostic is also pushed to the aria.toml file itself at line 0, in addition to the log channel message:

{
  "uri": "file:///project/aria.toml",
  "diagnostics": [
    {
      "range": { "start": { "line": 0, "character": 0 }, "end": { "line": 0, "character": 0 } },
      "severity": 2,
      "source": "npk-ls",
      "message": "aria.toml is deprecated; rename this file to nitpick.toml to suppress this warning"
    }
  ]
}

Translating [nikos] Values to npkc Flags

When launching the npkc --analyze subprocess, npk-ls translates each active [nikos] field into the corresponding CLI flag:

[nikos] field npkc flag
domain = "octagon" --domain=octagon
checkers = ["dbz", "boa"] --check=dbz --check=boa
entry_points = ["main", "init"] --entry-point=main --entry-point=init
threads = 4 --jobs=4
widening_delay = 3 --widening-delay=3
report_file = "out.html" --report=out.html
report_format = "json" --report-format=json
always_verify = true --verify-nikos

Fields that are absent from the config file (or set to their default value) are not forwarded as flags — npkc uses its own built-in defaults for those.

Example Subprocess Invocation

For a project with:

[nikos]
domain   = "octagon"
checkers = ["dbz", "boa", "nullity"]
threads  = 2

npk-ls launches:

/usr/local/bin/npkc --analyze --domain=octagon --check=dbz --check=boa --check=nullity --jobs=2 /project/main.npk