Class SymbolicEngine

java.lang.Object
org.ek9lang.compiler.symbolic.SymbolicEngine
public final class SymbolicEngine extends Object
The Layer-2 symbolic engine of the Symbolic/Contract Scanner (M3/M4) — it turns "this construct carries undischarged obligations" (the M1 census verdict) into "here is the exact input that panics", or proves no such input exists within the bounded model (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §3/§11.2/§12).

It ties together the spike-proven cores without re-deriving either:

  • SymbolicPathConditionWalker (slice A) — reports a branch dead when its require/if relational facts are contradictory (Example 6).
  • WitnessEnumerator (slice B) — drives an undischarged obligation through a type's representative value-classes and returns the first violating input (Example 1: count=0).

Inter-procedural (M4, §3.4). A FunctionSummary captures a callee's require preconditions. The engine uses them two ways: (1) a division by a parameter dominated by a require that excludes zero is discharged (so reciprocal with require x <> 0 verifies rather than crying wolf); (2) a call whose argument is an affine transform of a caller parameter (reciprocal(n - 10)) is refuted by inverting the transform onto the callee's require boundary (Example 2: callee require x <> 0 → witness n = 10). This is the arithmetic no value-class enumeration finds — n = 10 is neither a boundary nor an edge.

Why the engine re-walks the AST. The M1 census records only a count; its Obligation records are package-private and carry no divisor symbol, type, or AST location. So the engine re-reads each obligation site from source — the same relational/arithmetic extraction the census uses inline, reused here off the resolved ParsedModule. Only a free parameter divisor / affine argument is refuted; literals and opaque-call operands are conservatively left alone.

  • Constructor Details

    • SymbolicEngine

      public SymbolicEngine(ParsedModule parsedModule)
      Same-module engine: a callee whose declaration is not in parsedModule is not summarised.
      Parameters:
      parsedModule - the resolved module the analysed constructs belong to (post PRE_IR_CHECKS)

    • SymbolicEngine

      public SymbolicEngine(ParsedModule parsedModule, Function<String, List<ParsedModule>> moduleResolver)
      Whole-program engine: moduleResolver maps a module name to its parsed modules so a cross-module callee's require summary can be read (Example 2 across a module boundary). The call site is always in parsedModule; only the callee's precondition is read from its own module.
      Parameters:
      parsedModule - the module the analysed construct belongs to
      moduleResolver - module name → its parsed modules, or null for same-module only

  • Method Details

    • verify

      public ConstructVerdict verify(FunctionSymbol function)
      Verify one function/program body: report the branches it proves dead and the counterexamples it finds for its undischarged obligations (divide-by-zero and callee-require violations).
      Parameters:
      function - the resolved function symbol to analyse
      Returns:
      the construct verdict (verified when no counterexample was found within the bounded model)