Artifact for "Verifying the Option Type with Rely-Guarantee Reasoning"

This repository contains the dataset and scripts to reproduce Table 1 and Table 2 in the paper "Verifying the Option Type with Rely-Guarantee Reasoning".

Requirements

Please see REQUIREMENTS.md for the same information, but listed separately from this README file.

Our scripts are designed for a Unix environment (Linux, macOS, WSL, etc.). They will not work under a Windows command shell.

Our scripts require the following tools:

Python 3, version 3.9.6 or later.

GNU grep. For macOS, install it as ggrep via the command brew install grep.

If not already installed, brew can be installed via the instructionshere

Subject programs

File dataset.txt lists the subject programs.

The subject programs are stored under the following directories:

optional-paper-base-repos: all the subject programs with their build files modified to run the Optional Checker.

optional-paper-annotated-repos: all the subject programs, with@SuppressWarnings for each true positive and false positive issued by the Optional Checker (scripts count these). It also contains the Optional Checker type qualifiers that we wrote.

optional-paper-intellij-repos: all the subject programs with @SuppressWarnings for each IntelliJ warning (so they can be programmatically counted).

optional-paper-errorprone-repos: all the subject programs with @SuppressWarnings for each Error Prone warning.

optional-paper-spotbugs-repos: all the subject programs with @SuppressWarnings for each SpotBugs warning.

Scripts

Looking to reproduce all the data in our tables? See reproduce-data.

This repository contains the following scripts:

reproduce-data: this script reproduces all the data for our tables.

compute-precision-recall-annotations: this script generates Table 1: it computes the values for precision, recall, and the number of human-written, machine-checked annotations used by each tool.

count-style-violations: this script generates Table 2: it reports the number of style violations detected by each tool.

mygrep.py: this is a Python utility used by other scripts as a thin wrapper around grep. You need not use it directly.

All these scripts may be executed from the root of this directory. For example, to generate Table 1:

% ./compute-precision-recall-annotations

Resulting Data

Each script produces the rows of the dataset, excluding the column titles. Below is a brief description of each output .tex file:

eval-statistics.tex: generated by the compute-precision-recall-annotations script, maps to Table 1 in our paper. The columns of the data are, in order from left-to-right:

Tool name

Number of true positives detected by the tool

Number of false positives detected by the tool

Precision

Recall

Total number of machine-verified annotations written as a specification across all subject programs.

style-violations.tex: generated by the count-style-violationsscript, maps to Table 2 in our paper. The columns are the data are, in order from left-to-right:

Tool name

Number of violations of style rule 1

Number of violations of style rule 3

Number of violations of style rule 4

Number of violations of style rule 5

Number of violations of style rule 6.a

Number of violations of style rule 6.b

Number of violations of style rule 6.c

Number of violations of style rule 7

Implementation

The implementation of the Optional Checker appears in the implementation directory. This folder contains the following subdirectories:

optional: the source code for the Optional Checker's verification logic for the Optional type system.

optional/qualifiers: the definitions for each type qualifier from the Optional type system that may be used with the Optional Checker.

nonempty: the source code for the Optional Checker's verification logic for the Non-Empty type system.

nonempty/qualifiers: the definitions for each type qualifier from the Non-Empty type system that may be used with the Optional Checker.