• Stars
    star
    142
  • Rank 249,707 (Top 6 %)
  • Language
    Ada
  • License
    Other
  • Created over 8 years ago
  • Updated 28 days ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Ada semantic analysis library.

Libadalang

Libadalang is a library for parsing and semantic analysis of Ada code. It is meant as a building block for integration into other tools. (IDE, static analyzers, etc.)

Libadalang provides mainly the following services to users:

  • Complete syntactic analysis with error recovery, producing a precise syntax tree when the source is correct, and a best effort tree when the source is incorrect.

  • Semantic queries on top of the syntactic tree, such as, but not limited to:

    • Resolution of references (what a reference corresponds to)
    • Resolution of types (what is the type of an expression)
    • General cross references queries (find all references to this entity)

Libadalang does not (at the moment) provide full legality checks for the Ada language. If you want such a functionality, you’ll need to use a full Ada compiler, such as GNAT.

While it can be used in Ada (2012+) and Python (3.9 or Python 3.10) Libadalang also provides a low-level C API (meant to write bindings to other languages) and an experimental OCaml API.

If you have problems building or using Libadalang, or want to suggest enhancements, please open a GitHub issue. We also gladly accept pull requests!

Status of the project

Libadalang is still in development and we allow ourselves some headroom in terms of breaking backwards compatibility. If you want to use a stable version of Libadalang, you'll need to build from one of the stable branches, such as 19.1.

Libadalang currently:

  • Is able to parse 100% of Ada 2012 syntax, and presents a well formed tree for it. Support for Ada 2022 constructs is a work in progress.

  • Is able to recover most common syntax errors. The error messages are behind those of GNAT, but the recovery will potentially work better in many situations.

  • Provides name resolution/navigation.

  • Is able to handle some very simple incremental processing. Reparsing a source A and querying xref on a source B that depends on A is handled efficiently.

How to use Libadalang

There are several ways to get Libadalang:

  • Build it using the Libadalang Alire crate. This will only let you build the current and the previous releases (i.e. not the development version), but is by far the easiest way, as Alire automatically deals with dependencies.

  • Build it from Git repository sources: install all dependencies, generate its code and to build it. Please refer to the User Manual for detailed instructions.

  • Important: if you are an AdaCore customer with a GNAT Pro subscription, please get Libadalang through GNATtracker, as this is the only version of Libadalang that is covered by your support contract.

To learn how to use the API from Libadalang's the development branch, you can read the AdaCore Live Docs (updated daily).

Quick overview

Libadalang has a Python API, for easy prototyping and explorative programming. It ships with an executable named playground, that allows you to analyze Ada files and play with them in an interactive Python console.

Given the following main.adb Ada file:

with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
begin
    Put_Line ("Hello World");
end Main;

You can start the playground on it:

% playground main.adb

--
-- libadalang playground
--

The file(s) passed as argument have been put into the `u` variable, or units if
there are multiple.

Enjoy!

In [1]: print(u.root.text)
with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
begin
    Put_Line ("Hello World");
end Main;

In [2]: print(u.root.findall(mdl.CallExpr))
[<CallExpr 5:5-5:29>]

In [3]: print(u.root.findall(mdl.CallExpr)[0].text)
Put_Line ("Hello World")

The playground embeds the IPython interactive Python console, so you have a modern interactive programming environment. You can use tab completion to explore the Libadalang API.

Libadalang and ASIS

ASIS is widely used for static analysis of Ada code, and is an ISO standard. It is still the go-to tool if you want to create a tool that analyses Ada code. Also, as explained above, Libadalang is not mature yet, and cannot replace ASIS in tools that require semantic analysis.

However, there are a few reasons you might eventually choose to use Libadalang instead of ASIS:

  1. The ASIS standard has not yet been updated to the 2012 version of Ada. More generally, the advantages derived from ASIS being a standard also means that it will evolve very slowly.

  2. Syntax only tools will derive a lot of advantages on being based on Libadalang:

    • Libadalang will be completely tolerant to semantic errors. For example, a pretty-printer based on Libadalang will work whether your code is semantically correct or not, as long as it is syntactically correct.

    • Provided you only need syntax, Libadalang will be much faster than ASIS' main implementation (AdaCore's ASIS), because ASIS always does complete analysis of the input Ada code.

  3. The design of Libadalang's semantic analysis is lazy. It will only process semantic information on-demand, for specific portions of the code. It means that you can get up-to-date information for a correct portion of the code even if the file contains semantic errors.

  4. Libadalang has bindings to C and Python, and its design makes it easy to bind to new languages.

  5. Libadalang is suitable to write tools that work on code that is evolving dynamically. It can process code and changes to code incrementally. Thus, it is suitable as an engine for an IDE, unlike AdaCore's ASIS implementation.

  6. Libadalang is not tied to a particular compiler version. This combined with its staged and error tolerant design means that you can use it to detect bugs in Ada compilers/tools.

Implementation

The Libadalang project is based on the Langkit framework, so its Ada/Python/C/OCaml source code is not checked in this repository: it is instead generated from the Langkit language specification that you can find in ada/. This language specification, while embedded in Python syntax, is mostly its own language, the Langkit DSL, that is used to specify the part of Ada syntax and semantics that are of interest to us.

See the Developer Manual for more information about Libadalang's development.

More Repositories

1

gnatstudio

GNAT Studio is a powerful and lightweight IDE for Ada and SPARK.
Ada
373
star
2

spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
Ada
235
star
3

Ada_Drivers_Library

Ada source code and complete sample GNAT projects for selected bare-board platforms supported by GNAT.
Ada
229
star
4

ada_language_server

Server implementing the Microsoft Language Protocol for Ada and SPARK
Ada
217
star
5

gnat-llvm

LLVM based GNAT compiler
Ada
173
star
6

aws

AWS is a complete framework to develop Web based applications in Ada.
Ada
123
star
7

RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Ada
100
star
8

gsh

A POSIX shell for Windows.
C
97
star
9

learn

Sources for learn.adacore.com
Ada
91
star
10

gtkada

Ada bindings for the GTK+ graphical library.
Ada
84
star
11

langkit

Language creation framework.
Python
75
star
12

gprbuild

GPRbuild is an advanced build system designed to help automate the construction of multi-language systems.
Ada
63
star
13

svd2ada

An Ada binding generator from SVD descriptions for bare board ARM devices.
Ada
61
star
14

bb-runtimes

Source repository for the GNAT Bare Metal BSPs
Ada
61
star
15

ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
58
star
16

VSS

High level string and text processing library
Ada
49
star
17

gnatcoll-core

GNAT Components Collection – Core packages
Ada
43
star
18

gnatcoverage

GNATcoverage: Coverage Analysis Tool
Ada
32
star
19

Certyflie

Ada
30
star
20

ada-traits-containers

Generic Ada Library for Algorithms and Containers
Ada
28
star
21

why3

SPARK 2014 repository for the Why3 verification platform.
OCaml
27
star
22

e3-core

Core framework for developing portable automated build systems
Python
26
star
23

startup-gen

A startup code generator for embedded projects
Ada
25
star
24

git-hooks

Git hooks Python-based scripts
Python
24
star
25

Ada-IntelliJ

Support for Ada and SPARK languages in IntelliJ IDEA
Java
21
star
26

xmlada

The XML/Ada toolkit.
Ada
21
star
27

PolyORB

PolyORB provides a uniform solution to build distributed applications relying either on middleware standards
Ada
21
star
28

OPAVES

Open Platform for Autonomous VEhicle Systems
C
21
star
29

training_material

Ada
20
star
30

Ada-SPARK-Crate-Of-The-Year

19
star
31

gnat_community_install_script

Script to automate the installation of the GNAT Community Installers
Shell
18
star
32

cuda

Ada
17
star
33

spawn

Ada
16
star
34

libadalang-tools

Libadalang-based tools
Ada
16
star
35

gnat-gdb-scripts

GDB scripts for Ada programs built with GNAT
Python
16
star
36

win32ada

Ada API to the Windows library
Ada
16
star
37

Robotics_with_Ada

Robotics with Ada, ARM, and Lego
Ada
15
star
38

embedded-runtimes

runtimes that add support for various boards to the GNAT GPL compiler for ARM
Ada
14
star
39

gnatcoll-bindings

GNAT Components Collection – Bindings to C libraries
Ada
13
star
40

gpr

The framework for analyzing the GNAT Project (GPR) files
Ada
13
star
41

adareducer

Python
13
star
42

qemu

C
12
star
43

gnatcoll-db

GNAT Components Collection – Database packages
C
10
star
44

sparkformal

The project SPARK Formal aims at developing a complete semantics of the SPARK language in Coq.
Coq
10
star
45

UnityAdaTetris

Ada
9
star
46

markdown

Markdown parser
Ada
8
star
47

labs-material

Support Libraries for AdaCore University Labs
Ada
7
star
48

aunit

Ada
7
star
49

ada-py-bind

Ada
6
star
50

e3-testsuite

e3 testsuite driver
Python
6
star
51

RC_Car_Demo

An embedded Ada/SPARK demo
Ada
6
star
52

SPARK_Railway_Simulation_Demo

Ada
5
star
53

templates-parser

AWS templates engine.
Ada
5
star
54

Compile_And_Prove_Demo

Demo project for new web site: Compile It! / Prove It!
Ada
5
star
55

program_proofs_in_spark

This repository contains some programs from Rustan Leino's book "Program Proofs" verified with SPARK.
Ada
5
star
56

spdm-recordflux

5
star
57

RESSAC_Use_Case

A Collaborative Development Assurance Lab
Ada
5
star
58

gnatdashboard

Analyse a project.
Python
4
star
59

florist

Ada
4
star
60

Http_Cyclone

C
4
star
61

gnat-docker

Python
4
star
62

e3-aws

High level interface for CloudFormation
Python
4
star
63

Platinum_Reusable_Stack

Ada
4
star
64

wposix

Ada Windows POSIX binding
Ada
4
star
65

code_examples_server

prototype server for creating interactive "try SPARK / try Ada" webpages
Python
3
star
66

lmod_manager

lmod based management tool for GNAT and SPARK installations
Python
3
star
67

SPARK_PDI_Demo

Use of SPARK to implement Parameter Data Items
Ada
3
star
68

langkit-query-language

query language for Libadalang and Langkit
Java
3
star
69

gprconfig_kb

GPR configuration knowledge base
3
star
70

language-examples

Examples of common software engineering constructs written in Ada and SPARK
Ada
3
star
71

tictactoe

A tictactoe game written and proven in SPARK
Ada
3
star
72

RecordFlux-parser

3
star
73

RecordFlux-devutils

Python
3
star
74

ada_coding_standards

Ada
2
star
75

style_checker

The AdaCore style checker
C
2
star
76

gpr-unit-provider

GPR2 based unit provider for Libadalang
Ada
2
star
77

gnatdoc

GNAT Documentation Generator
Ada
2
star
78

Lunar_Lander_Rotation_Demo

Demonstration program that interacts with the AdaFruit BNO055 breakout board in order to send orientation data to a host computer
Ada
2
star
79

AdaSAT

Ada
2
star
80

training_labs_radar

Ada
2
star
81

uwrap

Ada
1
star
82

cheri-examples

1
star
83

z3

SPARK 2014 repository for the Z3 SMT solver.
C++
1
star
84

lal-checkers

Libadalang-based code checking infrastructure
Python
1
star
85

spark_translator

SPARK 2005 to 2014 translator
Python
1
star
86

Lumos_Maxima

Lumos_Maxima repository for VerifyThis challenge
Ada
1
star
87

training_labs_standalone

Ada
1
star
88

training_labs_solar_system

Ada
1
star
89

alt-ergo

SPARK 2014 repository for the Alt-Ergo SMT solver.
OCaml
1
star
90

lsif-ada

Ada
1
star
91

prettier-ada

Ada
1
star
92

SPARK-to-C_Tetris_Demo

Ada
1
star