Class SymbolicPathConditionWalker

java.lang.Object

org.ek9lang.compiler.phase5.flow.SymbolicPathConditionWalker

public final class SymbolicPathConditionWalker
extends Object

The M3 symbolic dead-branch analyzer: seeds a function's parameters as SymbolicTermValue terms, reads the relational facts off its require/if nodes into a PathCondition, and reports a branch dead when its accumulated facts are unsatisfiable.

This discharges the "guarded by a contradiction" obligation class end-to-end from source — e.g. Example 6: require lo <= hi then if lo > hi yields {lo<=hi, lo>hi}, which is unsatisfiable, so the if body is unreachable for every input.

It reuses the compiler's own relational-extraction SSOTs rather than re-deriving grammar walking: operator+operands come off the relational EK9Parser.ExpressionContext the same way SelfComparisonOrError reads them, the if control expression is located the way IfStatementOrError does (ifControlBlock().get(0).preFlowAndControl().control), and the require expression is the relational expression directly (RequireStatementContext .expression()), as RequireStatementOrError treats it.

Proven and perturbation-verified by spike S3c (see EK9_SYMBOLIC_SCANNER_SPIKE_REFERENCE.md §4.4). Residual hardening tracked for later slices: key terms by symbol identity (not name) for shadowing/locals; resolve operands beyond bare identifiers; fold this into the phase-5 flow listener with a PathCondition snapshot stack pushed/popped on the analyzer's existing branch hooks (rather than a standalone AST walk); handle multiple require/if nodes.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static final record	SymbolicPathConditionWalker.AnalysisResult	The base (pre-branch) path condition and the verdict for the function's if branch.
static final record	SymbolicPathConditionWalker.BranchResult	Whether a branch is dead (unreachable for every input), and why.

Constructor Summary

Constructors

Constructor	Description
SymbolicPathConditionWalker(ParsedModule parsedModule)

Method Summary

Modifier and Type	Method	Description
SymbolicPathConditionWalker.AnalysisResult	analyse(FunctionSymbol function)	Analyse one function: seed params as terms, accumulate the require fact, then test the if branch's fact-set for unsatisfiability.

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

SymbolicPathConditionWalker

public SymbolicPathConditionWalker(ParsedModule parsedModule)

Method Details

analyse

public SymbolicPathConditionWalker.AnalysisResult analyse(FunctionSymbol function)

Analyse one function: seed params as terms, accumulate the require fact, then test the if branch's fact-set for unsatisfiability.

Parameters:

function - the resolved function symbol to analyse

Returns:

the base condition + the if-branch verdict (ifBranch is null if there is no if)