CodeQL for Ada: a community extractor, library and query pack now available.

[peter-villadsen]

Hi all,

I've been building CodeQL support for Ada and it has reached a point where I'd like
people to try it: https://github.com/peter-villadsen/codeql-ada (MIT).

What it is

• An extractor built on Libadalang, AdaCore's
  Ada front end. It needs no build and no compiler (--build-mode=none): names and types
  are resolved from the GNAT project file.
• A QL library that reads like the Java one: Subprogram, Call, Parameter,
  Type, Variable, getEnclosingSubprogram(), getMetrics(), plus a class per
  Libadalang node kind.
• Control flow, data flow and taint tracking, built on the shared codeql/controlflow,
  codeql/ssa and codeql/dataflow libraries. Flow follows record components, arrays,
  Ada.Containers, package variables, dispatching calls, access-to-subprogram values and
  task entries. GNAT's finally parts are modelled with CFG splitting, after Ruby's
  ensure.
• 28 queries (/ada-queries on GHCR): reliability and maintainability
  checks, plus command-line, path and SQL injection. We expect many more queries to be provided over time.

Trying it

Please find the user manual in Docs/user-guide.md.

codeql database create mydb --language=ada --build-mode=none \
  --search-path=<dir containing the extractors ada> --source-root=<your project>

codeql database analyze mydb peter-villadsen/ada-queries \
  --format=sarif-latest --output=results.sarif

The extractor tarball is on the
releases page (https://github.com/peter-villadsen/codeql-ada/releases). Only supported on Linux x86-64
for now (use WSL on Windows), tested with CLI 2.25.6. The
user guide (https://github.com/peter-villadsen/codeql-ada/blob/master/docs/user-guide.md)
covers setup, writing your own queries (with worked examples), and running in GitHub
Actions and Azure DevOps. As with any third-party extractor, Ada can't go in
codeql-action/init's languages; the guide runs the CLI directly and uploads with
upload-sarif.

Status

Pre-1.0. It's tested on five open-source Ada projects (gpr2, AdaSAT,
libadalang-tools, Alire, libkeccak), and
known-limitations.md (https://github.com/peter-villadsen/codeql-ada/blob/master/docs/known-limitations.md)
lists what is still approximate. Bug reports, false positives and missed results are very
welcome as issues.

Feedback from people who know the shared libraries well would be especially useful. I'd
be glad to hear where the instantiation could be done better.

Also, I would be interested to know if Ada compiler vendors could adapt this to their project formats and offer the value provided here to their users.

[aschackmull]

I had a brief look through the QL library implementation, and it looks impressive! Well done! 🎉
Some comments:
We're moving away from splitting in the CFG. We've internally settled on the conclusion that splitting gives more problems than benefits. For that reason, we're planning to eventually delete the codeql.controlflow.Cfg library. Ruby, which you reference, has already migrated away. The replacement library codeql.controlflow.ControlFlowGraph should be much simpler to instantiate and use. See e.g. its instantiations for Ruby, Java, and C#. Getting the lost precision for something like finally-splitting back can then be achieved by using the codeql.controlflow.ControlFlowReachability library for any queries with a high dependency on accurate local path sensitivity - a good example for reference is the java/dereferenced-value-may-be-null query (NullMaybe.ql). Speaking of high precision local path sensitivity, if this is needed then the shared Guards library may also be of interest.

And if you need to reference SSA beyond its integration with data flow, then it's likely useful to instantiate the nested MakeSsa module. This provides a class-based SSA api where all the relevant predicates are correctly cached, and its api should match the expectations of the shared Guards and ControlFlowReachability libraries.

[peter-villadsen]

Hi, Thanks again for looking at the codeql-ada library and for the detailed advice. We acted on all of it the same day. Everything is on master at https://github.com/peter-villadsen/codeql-ada (commits 5ef030c..2674049) and will ship as 0.4.0. Here is what we did, step by step. 1. codeql.controlflow.Cfg → codeql.controlflow.ControlFlowGraph * The Ada CFG now instantiates Make0/Make1/Make2, modelled on the Java instantiation at the codeql-cli/v2.25.6 tag. The controlflow 2.0.35 pack we pin already ships the library, so no CLI or pack upgrade was needed. The old trees, completions and our finally splitting are deleted. * Ada constructs the library has no class for are ordinary nodes with their own steps, the way Java handles Kotlin's when: if … elsif (statement and expression), plain loop, exit when, and select. select chooses its alternative through tagged additional nodes with Boolean successors, so no node has two plain successors. * Every exit and goto is labelled with its resolved target (the loop, or the label statement), so only that construct catches the jump. An unlabelled exit inside a case alternative leaves the loop, not the case. * A case alternative's pattern is its whole choice list, matched at once. Ada choices are static, so one match edge per alternative is accurate, and it dominates the alternative's body, which Guards needs. * The public API follows Java's names (ControlFlowNode, ControlFlow::EntryNode, BasicBlock, …). The old names stay as deprecated aliases for one release. How we checked the switch: * We first built the new graph alongside the old one, and diffed their successor relations per AST node over our CFG tests and five open-source corpus projects (gpr2, libadalang-tools, alire, adasat, libkeccak). * The library's own consistency checks are empty everywhere. * The two graphs agreed to within 0.5% of edges, and every difference was explained before the switch. The largest group was infeasible paths through and then / or else, which the old graph joined at one node and the new one does not. * Across 28 queries and the five projects, one count changed: three unreachable-statement false positives on empty blocks disappeared. 2. The nested MakeSsa module It is instantiated and public as codeql.ada.dataflow.Ssa (SsaDefinition, SsaExplicitWrite, SsaParameterInit, SsaUncertainWrite, SsaPhiDefinition). SSA and data-flow results were unchanged, apart from a loop phi moving to the loop variable's node. 3. Shared Guards codeql.ada.controlflow.Guards instantiates Make and Logic over that SSA, with these Ada inputs: * equality: = / /=; * logical operators: and then / or else / not; * constants: null, Standard.True / False, and integer, character, string and enumeration literals; * non-null expressions: allocators and 'Access; * range guards: comparisons against decimal literals; * case alternatives; * wrapper functions: functions nothing overrides. The SSA data-flow integration now takes its guards from the library, which replaced our hand-written guard code. As a result, OK := Is_Safe (X); if OK then … is now a barrier. 4. ControlFlowReachability, and finally precision This is the one place we went a slightly different way, and I would value your view on it. * With finally parts merged, two of our path queries reported false positives: "file opened but not closed on every path" and "function may fall off its end". We confirmed both with test cases. * ControlFlowReachability did not fit either query. Neither has an SSA variable to follow. More importantly, the finally stack records only whether each finally part was entered abruptly. A part entered normally may still leave by an abrupt continuation edge, because from the graph alone that edge looks the same as a raise or return originating inside the part. One of our false positives (normal path → finally → return continuation, skipping a later Close) is exactly that case. * So for path questions without a variable, we added a small library, PathReachability. It records, for each enclosing finally part, how it was entered (normal, return, exception, exit, goto). The part's end may then only continue that way, while a raise or return inside the part may leave any way. Three queries use it. * We are keeping ControlFlowReachability for value questions, such as a future "may be null" query along the lines of NullMaybe.ql. Two questions 1. Is there a recommended way to ask variable-free path questions with the shared libraries? Or, would a per-kind finally stack (entry kind matched against the continuation edge's kind) be of interest upstream in ControlFlowReachability? 2. Is there a rough timeline for removing codeql.controlflow.Cfg? It no longer blocks us, but it would help us plan our CLI upgrades. The full step-by-step record, including every accepted difference between the old and new graphs, is in docs/cfg-migration-plan.md. The decisions are recorded as D-029 to D-035 in DECISIONS.md. Thanks again. The advice made the library simpler and more precise. Best regards, Peter From: Anders Schack-Mulligen ***@***.***> Sent: Monday, October 12, 2026 12:07 AM To: github/codeql ***@***.***> Cc: Peter Villadsen ***@***.***>; Author ***@***.***> Subject: Re: [github/codeql] CodeQL for Ada: a community extractor, library and query pack now available. (Discussion #22805) I had a brief look through the QL library implementation, and it looks impressive! Well done! 🎉 Some comments: We're moving away from splitting in the CFG. We've internally settled on the conclusion that splitting gives more problems than benefits. For that reason, we're planning to eventually delete the codeql.controlflow.Cfg library. Ruby, which you reference, has already migrated away. The replacement library codeql.controlflow.ControlFlowGraph should be much simpler to instantiate and use. See e.g. its instantiations for Ruby, Java, and C#. Getting the lost precision for something like finally-splitting back can then be achieved by using the codeql.controlflow.ControlFlowReachability library for any queries with a high dependency on accurate local path sensitivity - a good example for reference is the java/dereferenced-value-may-be-null query (NullMaybe.ql). Speaking of high precision local path sensitivity, if this is needed then the shared Guards library may also be of interest. And if you need to reference SSA beyond its integration with data flow, then it's likely useful to instantiate the nested MakeSsa module. This provides a class-based SSA api where all the relevant predicates are correctly cached, and its api should match the expectations of the shared Guards and ControlFlowReachability libraries. — Reply to this email directly, view it on GitHub<#22805?email_source=notifications&email_token=AS3TOVZJI37Q6AKIT3U4VFL5TR7JXA5CNFSNUABIM5UWIORPF5TWS5BNNB2WEL2ENFZWG5LTONUW63SDN5WW2ZLOOQXTCOBYG42TMNZUUZZGKYLTN5XKMYLVORUG64VFMV3GK3TUVRTG633UMVZF6Y3MNFRWW#discussioncomment-18875674>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AS3TOVY6CHJ37Z675YGOP5D5TR7JXAVCNFSNUABIKJSXA33TNF2G64TZHMYTIMZQGQYDIMRYHNCGS43DOVZXG2LPNY5TCMBZHE3TAOBZUF3AE>. You are receiving this because you authored the thread.Message ID: ***@***.******@***.***>>