Hoare Advanced Homework Assistant Parser

Unofficial, handwritten parser aimed at transpilation of the HAHA language.

Overview

This is a from-scratch implementation of a parser for the language of the Hoare Advanced Homework Assistant (HAHA). Most language constructs are supported, but there are currently some limitations (see below). This implementation does not draw on any of the files originally shipped with HAHA, and is entirely handwritten (i.e. was not generated by a parser generator). I needed this working quickly and at the time grappling with the likes of ANTLR just wasn't worth it.

This parser is primarily aimed at the transpilation of simple HAHA program to other languages (such as Java, C, C++ etc.) and is therefore currently missing many features.

Installation

You can pull this package into your Maven project straight from here using JitPack. Add JitPack as a repository first:

<repositories>
    <repository>
        <id>jitpack.io</id>
        <url>https://jitpack.io</url>
    </repository>
</repositories>

Then add this project as a dependency:

<dependencies>
    <dependency>
        <groupId>com.github.lambdacasserole</groupId>
        <artifactId>haha-parser</artifactId>
        <version>v1.2</version>
    </dependency>
</dependencies>

Quickstart

See below for some code that'll get you started quite quickly parsing HAHA code.

import java.io.File;
import java.io.IOException;

import com.sauljohnson.haha.parser.*;
import com.sauljohnson.haha.parser.model.Program;

import org.apache.commons.io.FileUtils;

public class QuickHahaParserTest {

    /**
     * The application entry point.
     *
     * @param args the command-line arguments to the application
     */
    public static void main(String[] args) {
        try {
            // Read in source code.
            String source = FileUtils.readFileToString(new File("my_file.haha"));
            
            // Tokenize source.
            Tokenizer tokenizer = new HahaTokenizer();
            Token[] tokens = tokenizer.tokenize(source);
            
            // Filter out empty statements (i.e. consecutive punctuators).
            TokenStreamTransformer emptyStatementFilter = new ConsecutiveTokenFilter(TokenType.PUNCTUATOR);
            TokenStream tokenStream = emptyStatementFilter.transform(new TokenStream(tokens));
            
            // Parse program.
            Program result = Program.parse(streamTransformer.transform(tokenStream));
            
            // TODO: Interact with the resulting parse tree here.
        } catch (IOException e) {
            e.printStackTrace(); // File read error.
        } catch (TokenizationException e) {
            e.printStackTrace(); // Tokenizer error.
        } catch (ParseException e) {
            e.printStackTrace(); // Parser error.
        }
    }
}

Limitations

This parser is currently subject to some limitations:

• Parsing does not descend all the way to the expression level. Conditional/loop predicates and the right-hand side of assignments are all left unparsed.
• Predicates, axioms, invariants, preconditions, and postconditions are left unparsed.

Contributing

For most intents and purposes, this project is considered to fulfil its original use case. Bug fixes and suggestions are welcome, however, from any member of the community.

Acknowledgements

A big thank you to the team at the University of Warsaw behind HAHA. This really is an awesome tool for teaching software verification! By name, they're:

• Tadeusz Sznuk
• Jacek Chrząszcz
• Aleksy Schubert
• Jakub Zakrzewski