Static Analysis and sec analyse

Purpose

Sec deliberately moves complexity into the compiler when the compiler can establish a useful fact reliably. Static analysis supports:

• language validity;
• memory and resource safety;
• target and platform validity;
• verified effect guarantees;
• execution and concurrency safety;
• resource-bound checks;
• mentor-style diagnostics;
• editor tooling;
• safe optimization and lowering.

Some of these analyses are mandatory because the language requires a proof. Others are advisory and exist to help the programmer find suspicious, unnecessarily broad or error-prone code before it becomes a runtime defect.

One Semantic Source of Truth

The compiler owns the semantic model. The command-line compiler, language server, sec analyse and later tooling all consume the same canonical facts.

For example, pitfall analysis does not implement its own ownership checker, and the LSP does not build a second call graph. They consume the facts produced by the analyses that own those domains.

source + project + target
          |
          v
   compiler analysis facts
      /      |       \
     /       |        \
 build   sec analyse   LSP

This rule matters because two tools must not disagree about whether a value escaped, a call can allocate, a reference remains valid or a target-specific operation is legal.

Compilation Snapshot and Target

Analysis is performed for a specific compiler snapshot. The snapshot may include the source modules, project configuration, dependencies, selected target and variant, compiler-known declarations, platform knowledge and the resolved CompilationPlan.

Analysis results are valid only for the snapshot and plan that produced them. A target change can invalidate facts involving pointer width, ABI, stack budgets, interrupt relationships, hardware resources, allocation policy or other target-dependent rules.

Valid, Invalid and Unproven

Safety and validity analyses distinguish three conceptual proof outcomes:

Unproven is not another spelling of Invalid. It becomes a compilation failure only when the applicable language or target profile requires a positive proof.

A strict embedded profile may, for example, require a finite stack bound. If analysis cannot establish one, the diagnostic should say that the required proof is missing. It must not pretend that a stack overflow was proven.

Required vs Advisory Analysis

Required analyses establish properties needed for a valid build. Ownership, borrowing, mandatory lifetime validity and a target-required resource proof are examples of facts that can directly decide whether compilation may continue.

Advisory analyses produce useful findings without redefining language validity. Parameter-usage recommendations and pitfall findings are primarily advisory.

Analysis Dependencies

Analyses form a dependency graph rather than one permanently fixed pass list. A later analysis may consume facts produced by several earlier domains.

ownership  -----> borrowing
    \               |
     \              v
      +--------> lifetime/reference

call graph -----> effects ------+
      |                         |
      +-----> stack             +-----> ISR
      |                         |
      +-----> races/deadlocks --+

Other examples include escape and closure facts feeding execution-boundary checks, and Place/storage identity feeding data-race analysis. Pitfall analysis deliberately sits near the end of this graph because it consumes canonical facts rather than recreating them.

Fixed Points and Recursion

Recursive functions, mutually recursive call graphs, loops, closure target flow and transitive effects can require iterative analysis. Sec allows fixed-point or equivalent convergent algorithms for these cases.

The important user-visible rule is conservative convergence: running out of refinement must not turn uncertainty into proof. Recursive analysis must be deterministic and must retain Unproven or another conservative state when a stronger fact cannot safely be established.

Analysis Budgets

Expensive analyses may use configurable budgets. A budget can limit path sensitivity, call expansion, closure target propagation, recursive refinement, deadlock graph search or other potentially expensive work.

Budget exhaustion changes precision, not language semantics. For a required property, insufficient analysis may leave the result Unproven. For an advisory analysis, it may simply reduce coverage or confidence.

Interactive, Standard and Deep

Sec tooling uses three analysis-depth configurations:

• Interactive favors fast editor feedback and bounded refinement.
• Standard is the normal compiler analysis depth.
• Deep allows more expensive refinement when additional precision is useful.

The current compiler defaults to Standard, while the LSP defaults to Interactive. A project may configure LSP depth through analysis.lsp_depth in .sec/sec.toml.

sec analyse

sec analyse is the command-line surface for requesting deeper compiler analysis reports without turning the language manual into a compiler-debugging guide.

sec analyse

The canonical analysis model treats the default command as an all-analysis request over the analyses available in the current compiler. The explicit all-analysis form is:

sec analyse --all

Individual analysis selection is also part of the intended tooling surface. Exact selection names are owned by the CLI implementation and may grow as analyses are integrated.

Build-producing commands still run every analysis required by the selected language and profile guarantees. sec analyse is not an escape hatch for turning mandatory checks off; it is a reporting and deeper-analysis surface.

Analysis Reports

Reports may expose compiler-owned information such as:

• call graphs and execution roots;
• effect summaries and verified guarantees;
• escape and closure facts;
• parameter demand;
• stack and Arena demand;
• data-race and deadlock findings;
• ISR proof results;
• pitfall findings;
• ownership and lifetime provenance;
• iterator resolution;
• target and profile applicability.

Reports distinguish compile errors, missing required proof, warnings and informational or advisory findings. A report must not downgrade a mandatory error into a suggestion.

Call Graph

The call graph records semantic callable relationships rather than only textual function-call syntax. It can include direct calls, methods, properties, closure calls, callbacks, cleanup helpers, task and thread entry edges, interrupt roots, foreign callbacks and compiler-generated helpers.

Execution edges are classified. A task spawn or ISR relationship is not automatically treated as an ordinary synchronous call. This distinction is essential for effects, stack usage, races and deadlocks.

Effects and Guarantees

Effect analysis derives facts such as MayPanic, MayAllocate, MayBlock, MaySuspend, MaySpawn, MayIO, MayAccessVolatile and external-state mutation.

It also verifies source-visible guarantees such as @noPanic, @noAlloc and @noBlock. These guarantees are transitive: a function cannot satisfy one merely because the prohibited operation appears in a helper several calls away.

See 48 Effects and Verified Guarantees for the source-level effect model.

Escape Analysis

Escape analysis answers where a value, reference, view, closure dependency or other semantic subject may outlive or be retained beyond its local context.

Escape does not mean “allocate this on the heap”. Sec does not repair an invalid lifetime with silent heap promotion. If a value legitimately escapes, its storage and lifetime mechanism must already support the destination. Invalid escapes are rejected.

Closure Analysis

Closure analysis tracks capture identity and mode, closure environment ownership, callable-value flow, possible invocation targets, environment escape and the lifetime/transfer implications of captured values.

It is also the bridge between function values and analyses that need to know what can actually be called indirectly. Unknown or open target sets remain conservative.

Parameter Usage

Parameter-usage analysis records how a parameter or receiver is demanded by the implementation. Dimensions may include read, write, consume, retain, escape, call, address-taking, task/thread transfer and effect contribution.

This analysis is primarily advisory. It may suggest that a signature can be narrower or that a parameter is more powerful than the implementation actually needs, but it must not silently rewrite the callable signature.

Stack Analysis

Stack analysis is designed to reason about semantic stack demand and, when target layout information is available, machine stack demand. It combines frame estimates, call paths, recursion, task/thread/ISR roots, interrupt nesting and target-specific budgets.

A result may be exact, bounded, unknown or proven unbounded. Strict targets can require a positive finite bound before code is accepted for a particular execution root.

Data-Race Analysis

Data-race analysis combines semantic memory-location identity, concurrent execution contexts, ownership and borrowing, transferability, synchronization, atomics, FFI, volatile/MMIO access and interrupt relationships.

Deadlock Analysis

Deadlock analysis reasons about resource acquisition, held locks, waits, task/thread completion dependencies, callbacks, foreign blocking behavior and ISR reentry.

It distinguishes a proven cycle from a possible or unproven risk. Unknown foreign locking or blocking behavior remains conservative rather than being guessed from a function name.

ISR Analysis

ISR analysis is a cross-analysis verifier. It consumes call-graph, effects, stack, race, deadlock, FFI, allocation, panic, blocking and target interrupt-profile facts to decide whether an ISR root satisfies the required interrupt-safety contract.

It does not duplicate those analyses. If stack safety is unproven, ISR analysis keeps that dependency visible rather than inventing a separate stack estimate.

Pitfall Analysis

Pitfall analysis looks for semantically suspicious patterns that are legal Sec but commonly indicate human mistakes. It consumes facts from the analyses that own types, bounds, control flow, Places, effects, FFI and other semantics.

Findings can carry evidence, confidence, suppression information and corrective guidance. A pitfall remains advisory unless another canonical rule defines the same situation as a language error.

This is where analyses such as likely off-by-one ranges, suspicious collection usage or dangerous FFI assumptions can be presented without weakening the distinction between “invalid program” and “valid but probably unintended”.

Other Core Analyses

The coordinated analysis system also includes core semantic checks that are so central that users may not think of them as optional analysis features. These include:

• type and interface/conformance analysis;
• ownership availability and move/copy transitions;
• borrow compatibility and non-lexical live ranges;
• lifetime and reference-origin validity;
• definite initialization;
• reachability and termination facts;
• contracts and compile-time bounds;
• transferability across tasks, threads, processes, ISRs and callbacks;
• target, ABI, layout and hardware validity.

sec analyse may expose some of these facts, but they remain part of the compiler's normal semantic responsibility even when no explicit analysis report is requested.

Evidence and Cause Paths

Nontrivial facts retain provenance so the compiler can explain why a result exists. Provenance may include source locations, call edges, captures, ownership transfers, storage origins, target facts, FFI contracts and dependent analysis facts.

A useful diagnostic should point to the earliest meaningful cause rather than only the final symptom. For example, a @noAlloc failure should be able to show the call path that reaches the allocation-producing operation.

Trusted Facts

Some facts come from declarations outside ordinary Sec proof. Examples include FFI contracts, platform knowledge, ABI descriptions, inline assembly contracts and compiler intrinsics.

These facts may be trusted inputs, but trust provenance is retained. A trusted claim is not presented as if the compiler independently proved the behavior from Sec source. Changing the trusted dependency invalidates analyses that depend on it.

LSP Integration

The language server is a client of compiler analysis, not a competing analysis engine. Hover, call hierarchy, diagnostics, future code lenses and Sec-specific analysis views consume compiler-owned facts from the active workspace snapshot.

Interactive mode can publish fast direct findings first and refine them as additional analysis completes. However, an incomplete or stale result must never be presented as a positive required proof.

Incremental Analysis

Analysis facts are invalidated by semantic dependencies, not merely by changed text. A change to a function body, target, interface conformance, FFI contract, call target, hardware resource or effect summary can invalidate different subsets of the analysis graph.

Reuse is permitted only when the compiler can establish that the cached fact still belongs to a compatible snapshot and CompilationPlan. Parallel or cached analysis must remain deterministic.

Diagnostics

Rejecting analyses use mentor-style diagnostics. A good analysis diagnostic identifies:

• what is invalid or unproven;
• where the problem occurs;
• the rule or semantic reason;
• the operation or declaration that caused it;
• related locations and cause paths;
• why the compiler cannot establish safety;
• a practical safe correction when one is known.

The analysis that owns the violated fact normally owns the primary diagnostic. An advisory analysis should not repeat a stronger compiler error as a competing warning.

Current Implementation Status

The Sec analysis rulebooks are substantially design-complete, but implementation is intentionally uneven. The common compiler-analysis coordination layer is currently partial.

Implemented or partially integrated verticals already include:

• a compiler-owned call-graph slice used by Sema and LSP;
• initial effect propagation and allocation cause paths;
• escape facts and direct-call return-origin summaries;
• closure/capture infrastructure and analysis-depth configuration;
• parameter-demand analysis;
• structured high-confidence pitfall analysis;
• selected analysis facts exposed through LSP hover and call hierarchy.

The canonical stack, data-race, deadlock and ISR analyses are written but their implementation ledger entries are still planned. The common incremental coordination and complete sec analyse reporting surface also remain incomplete.

Best Practices

• Use ordinary compiler diagnostics first; use sec analyse when you want deeper explanation or advisory reports.
• Do not treat Unproven as a proven defect or as proven safety.
• Run deeper analysis before shipping code with strict resource or concurrency requirements.
• Use the same target and variant you intend to build when reviewing target-dependent analysis.
• Prefer canonical compiler reports over handwritten duplicate scripts for ownership, effects or call relationships.
• Read cause paths, not only the final diagnostic location.
• Keep FFI, inline-assembly and platform contracts precise; vague trusted inputs force conservative analysis.
• Use advisory parameter and pitfall findings as evidence, not as automatic source rewrites.
• Remember that unsafe code remains subject to ownership, race, ISR and other independent analysis rules.
• Do not weaken analysis depth to work around a real required-proof failure.

Summary

• Sec uses one coordinated compiler-owned analysis system.
• Each semantic fact has one canonical owner.
• Compiler, LSP and sec analyse consume the same semantic facts.
• Analysis results belong to a specific source snapshot and CompilationPlan.
• Safety proof states distinguish Valid, Invalid and Unproven.
• Required analysis may reject missing proof; advisory analysis may only reduce confidence or produce guidance.
• Recursive and interprocedural analysis may use deterministic fixed points.
• Analysis budgets reduce precision but never manufacture proof.
• Interactive, Standard and Deep change analysis depth, not language semantics.
• sec analyse exposes deeper compiler-owned reports and all-analysis behavior.
• The call graph models semantic call and execution relationships, not only textual calls.
• Effect analysis derives transitive effects and verifies guarantees.
• Escape analysis never silently promotes invalid values to heap storage.
• Closure analysis owns captures, callable flow and target sets.
• Parameter usage and pitfall analysis are primarily advisory.
• Stack, race, deadlock and ISR analyses compose other canonical facts rather than recreating them.
• Diagnostics preserve evidence and cause paths.
• Trusted FFI/platform/assembly facts retain trust provenance.
• Incremental and parallel analysis must preserve snapshot consistency and determinism.
• The rulebooks are normative; current implementation coverage remains partial.