Explore coverage analysis for Rust
AdaCore
Grenoble
Internship
AdaCore: Helping Developers Build Software that Matters
Everything we do at AdaCore is centered around helping developers build safe, secure and reliable software.
For over 25 years, we've worked with global leaders across the military and civil avionics, defense systems, air traffic management/control, space, railway, and financial services industries, building tools and providing services that ease the complex and difficult process of developing high-integrity software. As the need for truly secure and reliable applications expands into industries such as automotive, medical, energy, and IOT, we’re advancing our time-tested technologies to bring expertise and services to help a whole new generation of developers. Through our subscription-based business model and dedicated services arm, we have worked with hundreds of customers over the year on thousands of projects.
Our 150 experts worldwide in the US (New York), France (Paris, Toulouse, Grenoble and Vannes), Germany, the UK, and Estonia, all play a role in developing state-of-the-art technologies to meet the challenges of building the highest grade of software.
Joining AdaCore is about joining a culture of innovation, openness, collaboration and dependability, which defines how we work together, with our customers and partners.
Context:
In line with industry trends, AdaCore has recently been expanding its toolchain offering to cater to safety-critical markets beyond Ada. Rust has attracted attention within the safety- and security-critical market due to its focus on memory safety and vibrant user community.
AdaCore provides all the necessary tools for certification purposes, among them being a coverage tool (GNATcoverage) that can provide 3 coverage criteria for 3 (increasing) levels of safety:
-
Statement coverage, focusing on the coverage of statements
-
Decision coverage, focusing on the coverage of decision outcomes. In this context, decisions are expressions controlling the program data flow.
-
MC/DC coverage, focusing on the coverage of decision structures. This stands for Modified Condition/Decision Coverage, where “condition” refers to the atomic operands of Boolean expressions, and which necessitates demonstrating that altering a single condition can impact the decision outcome.
We have recently started investigating what it would mean from a technical perspective to support MC/DC for Rust. We have investigated developing a solution from scratch, drawing upon our expertise in implementing coverage solutions for Ada and C/C++. Alternatively, we have also started exploring the use of existing coverage tool analysis for Rust and enhance them to meet our coverage criteria, with the goal of integrating them into GNATcoverage.
The most promising lead so far has been the LLVM source-based coverage, which has been implemented for Rust. The Rust compiler is invoked with a special coverage switch, which will make it produce source coverage obligations and LLVM instrumentation code to monitor the execution of “regions of interest”. This provides line coverage, which is not precise enough for certification-related activities.
Recent strides have been taken to integrate support for MC/DC source coverage analysis into LLVM's source-based coverage: https://reviews.llvm.org/D136385, with a full-fledged integration into clang. This shows that the coverage format can be extended to a more complex criterion.
Goals:
The initial step of the internship would be to investigate how the LLVM source-based coverage was implemented in the Rust compiler, and assess the feasibility of extending the implementation to support MC/DC source coverage analysis as well, leveraging the work done for clang. A most salient question would be whether the Rust implementation can provide adequate information to an MC/DC-enriched coverage format, as MC/DC coverage analysis usually requires precise source code traceability, which may be lost in intermediate representations.
Another step (and orthogonal) would be to investigate if we could integrate LLVM source-based coverage into GNATcoverage, to leverage existing report formats and consolidation modes implemented in GNATcoverage.
This project is ambitious and primarily involves technical research. We are seeking someone interested in exploring large open-source projects like the Rust compiler and LLVM, conducting in-depth technical research and assessment. We want to emphasize that most of the work for the internship will be investigation and experimentation, and that we do not necessarily expect a prototype out of it.
Skills required or Nice to have:
-
Knowledge of Rust
-
Knowledge of C/C++
Timeframe & Location:
During 2024 – 6 months – Paris office / Grenoble office
Beyond the job
We are looking for individuals who want their work to have a direct impact on improving the reliability, safety and security of the software that modern society has grown increasingly dependent on in an international environment. Our sales and marketing team is staffed with multi-talented, tenacious and creative individuals; and our HR team is committed to ensuring your tenure with AdaCore is a positive one.
AdaCore is a global organization driven by a team that personifies many different backgrounds and experiences. We are also a technology company that celebrates the open exchange of ideas, which makes innovation possible! We encourage applicants of all backgrounds to consider joining us. We welcome people of all ethnicities, nationalities, gender identities or expressions, ages, religions, physical abilities, sexual orientations, veteran status, or marital status; we celebrate everything that makes you uniquely, undeniably you.
We encourage our employees to explore their curiosity by providing them ongoing and lifelong training from their first day in AdaCore with a strong onboarding plan. As we know that juggling work and life is challenging, we offer flexibility to accommodate personal needs and work commitments.
AdaCore offers competitive compensation, benefits and thoughtful perks (summer meetings, activity weekends, Holiday dinner etc). We go beyond industry standards to help keep our employees comfortable and satisfied both on and off the job, no matter where they are based.