Skip to content

About

Static semantic analysis for Elixir and the BEAM, combining source code, compiler evidence, and program dependence graphs to model calls, data flow, OTP actors, messaging, state transitions, supervision, and effects.

Topics

Resources

Contributing

Stars

5 stars

Watchers

1 watching

Forks

Repository files navigation

ElixirScope

GitHub repository Hex package HexDocs documentation License: MIT

elixir_scope — Static Semantics for the BEAM

Status: Phase 1a source-authored implementation; no Elixir compilation or runtime tests were possible in the authoring environment. Not release-qualified.

This package analyzes source and compiled BEAM artifacts, uses Reach for program dependence and Sourceror for source locations, and produces portable, provenance-qualified static facts (Contract A). Its findings describe possible behavior, not runtime observations.

Toolchain

  • Elixir 1.20.5 minimum (>= 1.20.5 and < 2.0.0).
  • Supported OTP candidates: 27, 28, 29; OTP 29.1 is the authoring reference, not a verified matrix.
  • Tested runtime versions: none during Phase 1a. Phase 1b must compile and run the full suite before committing.

First build and QA (Phase 1b)

elixir --version
mix local.hex --force
mix local.rebar --force
mix deps.get
mix deps.compile
mix format
mix compile --warnings-as-errors
mix test
mix test --include integration --include live_provider
mix credo --strict
mix dialyzer
mix docs
mix scope.doctor
mix scope.analyze test/fixtures/hold_ledger --providers source --out /tmp/es-contract-a
mix scope.inspect /tmp/es-contract-a
python3 scripts/contract_a_verify.py /tmp/es-contract-a

Caution: The code has not been executed. The handoff document describes likely failure points and completion gates. Do not mark the implementation tested or production-ready based on this ZIP.

Library usage

{:ok, snapshot} = ElixirScope.analyze_source("../target_project",
  repository_key: "target_project",
  providers: [:source, :erlang, :compiler, :xref, :reach]
)

actors = ElixirScope.Query.actors(snapshot)
triggers = ElixirScope.Query.triggers(snapshot)
effects = ElixirScope.Query.effects(snapshot)
{:ok, path} = ElixirScope.export_static(snapshot, "./static-facts-target")
{:ok, loaded} = ElixirScope.Export.ContractA.read(path)

The source-only provider is non-executing. The compiler provider reads existing .beam artifacts without loading target modules. decode_abstract: true is explicitly opt-in because BEAM debug information may invoke backend-specific decoding; it must be used only in an appropriately isolated extraction worker for untrusted inputs.

Fact model

An entity has id, kind, attrs, evidence. A relation additionally has from and to entity IDs. Evidence describes basis, resolution, provider, rule, witnesses, and alternatives. All public facts use strings, numbers, booleans, maps and lists. Reach's local IR IDs and Erlang terms do not cross the wire.

IDs use human-inspectable bc:* keys. Source/build/artifact SHA-256 digests are separate; insertion in an unrelated file does not change a definition's logical ID. A source occurrence that moves may need cross-revision lineage matching; it is not silently assigned the prior identity.

Contract A bundle

static-facts-*/
  manifest.json
  entities.ndjson
  relations.ndjson
  coverage.ndjson
  diagnostics.ndjson

manifest.json contains source/build/toolchain identity and per-stream SHA-256 and record counts. The Elixir serializer enforces reference integrity; an independent Python validator is bundled. JSON schemas are drafts in priv/contracts/v1 and will be reconciled with the broader BeamCompass contract before a stable release.

Implementation contents (Phase 1a)

  • Non-executing acquisition; source hashes and BEAM fingerprinting.
  • Sourceror AST navigation, modules/definitions/clauses, source ranges, call-site indexing, effect descriptor literals, declared registrations/strategies.
  • Erlang :epp source module/function indexing.
  • BEAM imports/exports/behaviours, optional abstract functions; :xref external-call candidates.
  • Reach project graph adapter, source-range normalization, graph edges, OTP edge attempt and classified effect candidates.
  • Conservative source/compiled MFA alignment, known-source direct call candidates.
  • OTP actor roles, explicit named-message target candidates, callback return-tag transition candidates, declared supervision candidates, framework trigger candidates and API effect sites.
  • Bounded static graph queries, fact explanations, canonical JSON/NDJSON export and integrity-checked import.
  • Mix CLI tasks; ExUnit, StreamData, Credo, Dialyxir, docs and CI scaffolding.

Important limitations

  • Not yet compiled/tested; some APIs or AST patterns may require Phase 1b correction.
  • Actor/message and state analysis are conservative initial passes, not exhaustive selective-receive, guard, dynamic-registry or value-flow analysis.
  • Supervision does not yet resolve child lists/restart closures.
  • Source-to-compiled alignment is possible pending stronger build provenance.
  • Effect catalog rules in Elixir code and JSON catalog need consolidation; framework coverage is limited.
  • Source-only queries operate on the authored/inferred graph. Reach synthetic vertices without canonical IR identities are omitted with explicit partial coverage. Containment and unclassified graph edges are excluded from default semantic slices.
  • Query.paths_report/4 exposes path-search work and truncation; Query.paths/4 returns just the bounded paths. Acquisition enforces file, byte and elapsed-time budgets and rejects unreadable files and symlink inputs.
  • xref requires supported debug information. Stripped BEAM files retain compiler export/import facts, while xref reports the rejected module; arbitrary debug backends are not invoked.
  • Incremental caching, robust sandbox orchestration, more precise identity lineage, precompile event ingestion and production memory budgets are future work.

See architecture, invariants, and the separate Phase 1b handoff.

About

Static semantic analysis for Elixir and the BEAM, combining source code, compiler evidence, and program dependence graphs to model calls, data flow, OTP actors, messaging, state transitions, supervision, and effects.

Topics

Resources

Contributing

Stars

5 stars

Watchers

1 watching

Forks

Releases

Packages

Contributors

Languages