Modern programs in languages like Haskell include a lot of information beyond what is required for compilation. This includes unit tests, property-based tests, and type annotations more specific than those necessary to resolve ambiguity. This additional specification is usually only used for post-compilation verification by running the tests to verify that the code-as-written matches the specification the types and properties provide.
In this thesis, we explore ways of going beyond verification, and how this additional information can aid the developer during development. This can be done in multiple ways, for example, by helping the programmer write an implementation that matches the specification, by helping them track down the source of a bug in the implementation, and automatically repairing an implementation that does not match the specification.
In the first part, I explore the integration of program synthesis into GHC compiler error messages using typed-hole suggestions to aid completion of partial programs during development. In the second part, we present PropR, an automatic repair tool. PropR is based on type-driven synthesis, guided by property-based testing and fault localization in conjunction with genetic algorithms. A rich specification is required for these approaches to be effective. This motivates the third part of this thesis, where we present Spectacular, a specification synthesis tool. Spectacular uses ECTA-based synthesis to automatically infer properties of programs, letting us bootstrap specifications from previous versions.
In the fourth and fifth part of this thesis, we present the lightweight trace-based and spectrum-based fault localization tools CSI: Haskell and TastySpectrum respectively, and explore how we can localize program faults and find likely sources of a bug.
+ Added introduction.
+ Updated functional spectrums paper with the currently under submission version.
+ Removed final paper. Still a planned journal extension to the PropR paper, but now presented in the future work section in the introduction instead of a separate paper.
The thesis is available in PDF format. This contains the introduction as well as the papers in a thesis format.
There is also a short errata for chapter 6.
Presented here are the papers as published/submitted. I recommend reading the standalone thesis draft as presented above, as this includes more up-to-date and less space constrained versions of the papers.
Chapter 1: Introduction
by Matthías Páll Gissurarson
The kappa of the thesis, including motivation, overview, background, related work and future work.
Chapter 2: Suggesting Valid Hole-Fits for Typed-Holes (Experience Report)
by Matthías Páll Gissurarson
Published at the Haskell Symposium 2018
Suggesting Valid Hole Fits documents the implementation and design of the synthesis of valid hole-fits as they initially appeared in GHC. Of particular interest is the sorting of hole-fits by “relevance”, using either the simplistic number of type constructors (the “size” of the type) heuristic, and the more advanced subsumption sorting, where more “specific” types are treated as more “relevant” than more general types.
Chapter 3: PropR: Property-Based Automatic Program Repair
by Matthías Páll Gissurarson, Leonhard Applis, Annibale Panichella, David Sands, and Arie van Deursen.
Published at International Conference on Software Engineering (ICSE) 2022 - Technical Track
In the PropR paper, we introduce PropR, a tool that automatically repairs Haskell programs using a combination of typed-hole synthesis to repair program expressions with well-typed replacements and using QuickCheck properties to verify the repair. We use GHC’s Haskell program coverage functionality to figure out which expressions are involved in a fault based on QuickCheck generated counterexamples to failing properties, a typed-hole valid hole-fit plugin to generate well-typed replacements as fixes for said expressions, and a genetic algorithm to select and combine fixes based on QuickCheck property results after applying a fix.
Note: Me and Leonhard were joint first authors on this paper, where I focused on the implementation of the synthesis and repair, as well as the technical part. Leonhard focused on the genetic repair and experimental part.
Chapter 4: Spectacular: Finding Laws from 25 Trillion Programs
by Matthías Páll Gissurarson, Diego Roque, and James Koppel.
Published at International Conference on Software Testing, Verification, and Validation (ICST) 2023 - Research Track
Spectacular is a new tool for automatically discovering candidate laws for use in property-based testing. Incorporating many of the ideas from QuickSpec, but using the recently developed technique of ECTAs, Spectacular can explore vastly larger fully polymorphic program spaces efficiently.
Chapter 5: CSI: Haskell - Tracing Lazy Evaluations in a Functional Language
by Matthías Páll Gissurarson, and Leonhard Applis.
Published at Symposium on Implementation and Application of Functional Languages (IFL) 2023
In CSI: Haskell, we extended the Haskell Program Coverage implementation in GHC to enable runtime tracing of Haskell Programs. In the paper, we focus on the suffix of such traces, and investigate how effective they are at pointing to faulty locations in the nofib-buggy dataset.
Chapter 6: Functional Spectrums - Exploring Spectrum-Based Fault Localization in Functional Programming
by Leonhard Applis, Matthías Páll Gissurarson, and Annibale Panichella.
Manuscript
In Functional Spectrums, we implemented an ingredient for the Tasty test framework coupled with a GHC plugin to create typed-augmented spectrums for fault localization for functional programs. In the paper, we investigate how effective this approach is for the HasBugs data set.
Note: Me and Leonhard were joint first authors on this paper, where I focused on the implementation of spectrums and their processing, while Leonhard focused on the rules-based system and experimental verification.