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.