Parse: C# source → syntax tree

NStatic parses your C# code into an immutable abstract syntax tree (AST). The parser is hand-written and lenient — it handles partial or incomplete code, which matters for real-time analysis inside an editor. Multiple languages (C++, Python, Objective-C) share the same parser infrastructure.

Translate: syntax tree → lambda-calculus expressions

Each C# construct is translated into a mathematical expression built from lambda calculus. This is the core idea — called denotational semantics. The expression for a piece of code describes what it means, not just what itdoes.

// C# source:
if (x > 0)
    result = x * 2;
else
    result = -x;

// Internal representation (simplified):
If(GreaterThan(x, 0),
    SetValue(state, result, Times(x, 2)),
    SetValue(state, result, Negate(x)))

A while loop becomes a fixed-point combinator — a mathematical object that represents "the function that calls itself until the guard is false." Anif/else becomes an If(condition, thenExpr, elseExpr)expression.

Solve loops: fixed points → closed forms

Loops are the hardest part of static analysis. A while loop translates to a Fix expression — the mathematical fixed point of the loop's body function. NStatic then attempts to convert this into a Repeat expression: a closed-form formula for what the loop produces after n iterations.

// Fibonacci loop in C#:
int a = 0, b = 1;
for (int i = 0; i < n; i++) { int t = a + b; a = b; b = t; }

// NStatic recognizes this as a 2nd-order homogeneous recurrence.
// Closed-form solution (golden ratio formula):
// a(n) = (φⁿ − ψⁿ) / √5   where φ = (1+√5)/2, ψ = (1−√5)/2

Recognized patterns include arithmetic and geometric progressions, idempotent functions (applying the function twice gives the same result as once), involutive functions (applying twice returns to the start), and second-order homogeneous recurrences like Fibonacci.

Simplify: algebraic reduction until convergence

The resulting expression is passed to the Simplifier — a constraint propagation engine that applies algebraic rules repeatedly until no more reductions are possible. It maintains an equation database: a set of known facts about the program state at each point.

The simplifier uses a priority heap to schedule reductions, processes the expression graph until it reaches a fixed point, and caches results to avoid redundant work. Each operator type has its own reduction rules — If, And,Lambda, Fix, and all arithmetic operators.

// After branch analysis, the simplifier knows x > 0.
// It can then simplify within the true branch:
Abs(x)      →  x          // because x > 0
Max(x, 0)   →  x          // because x > 0
If(x > 0, A, B) →  A      // branch is known-true

Analyze interprocedurally: follow call chains

NStatic categorizes every method as either simple (pure, no external effects, analyzed to depth 10) or complex (stateful or virtual, analyzed to depth 2). Simple functions are inlined into call sites during analysis; complex ones are summarized as pre/post-condition pairs.

For .NET Framework library methods (which have no C# source), NStatic interprets the IL (intermediate language bytecode) directly — so it knows thatstring.ToCharArray() returns a non-null array of length equal to the string's length, and that List<T>.Add increments Count by 1.

On a 37,000-method codebase (the Rotor shared-source .NET runtime), this analysis completes in under two minutes.

Surface findings: errors, paths, and symbolic state

After simplification, any expression containing an Exception sub-expression that hasn't been caught, or a branch condition that simplifies to False(dead code), or a condition that simplifies to True (redundant check) — becomes a finding.

The finding is reported with:

• The exact source location (file, line, expression)
• The call stack showing which methods contributed
• The Locals panel: symbolic values of variables at the error site
• The Assumptions panel: every constraint the analyzer recorded on the path to this error
• Execution path arrows overlaid on the source, showing the paths that reach the error