Provide on-the-fly static analysis capabilities for Ada
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 120 experts worldwide in the US (New York, Lexington), France (Paris, Toulouse, Grenoble and Vannes), 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.
Provide on-the-fly static analysis capabilities for Ada
Context
Developed at AdaCore, CodePeer (https://www.adacore.com/codepeer) is an Ada source code analyzer that detects run-time and logic errors. It assesses potential bugs before program execution, serving as an automated peer reviewer, helping to find errors easily at any stage of the development life-cycle. The analysis is static, in the sense that only the source code is considered -- the program is never executed.
We have recently added into CodePeer results from the Infer static analyzer developed by Facebook (https://fbinfer.com). This integration offers us the possibility of having more lightweight analyses that complement well the initial capabilities of CodePeer. We want to pursue the exploration of the new results available through Infer.
Goals
Currently, users run CodePeer on a stabilized set of sources of files. Typically, we expect the project to be compilable. To expand the usage scenario of CodePeer, we would like to offer the possibility of having on-the-fly analysis results, directly in the IDE. To achieve this goal, the intern would:
-
Improve the existing mode (“compiler-mode”) so that it behaves similarly to regular analyses. One missing feature of this mode is that there is no comparison performed with previous results.
-
Deploy Infer’s “incremental analysis” mode. Infer is able to perform partial analyses, thanks to the summaries it stores on disk. However, we do not use this functionality in CodePeer (yet). The intern will be responsible for deploying this new feature, as well as benchmarking it.
-
Assess whether Infer’s notion of dependencies is sound. Infer already knows how to invalidate summaries that depend on a modified file. The intern will check that the current heuristics are compatible with the code generated by the Ada frontend, and adapt them if necessary.
-
Depending on the time available, and if the intern is interested in that topic, make some modifications to GNATStudio (AdaCore’s IDE), so that it actually performs on-the-fly analyses. This will mean writing a server that receives source file changes notifications from the IDE, and communicates back the analysis results.
Skills required/nice to have:
-
Experience/interest in static analysis and/or compilation
-
Some knowledge of OCaml would be a plus
-
Taste for good user experience
Timeframe: During 2022 - 6 months
