Scripts for modifying coverage-properties of sv-benchmarks

cross-check.sh

#!/bin/bash

## Usage: Run from directory `sv-benchmarks/c`.

echo "Tasks that have a coverage-error-call property, but that are not in selection (may be empty if everything is ok):"
find . -iname '*.yml' | xargs grep -l coverage-error-call.prp | cut -d"/" -f 2- | grep -xvf candidates_error-coverage.txt
echo "Tasks that have a coverage-branches property, but that are not in selection (may be empty if everything is ok):"
find . -iname '*.yml' | xargs grep -l coverage-branches.prp | cut -d"/" -f 2- | grep -xvf candidates_coverage.txt
echo "Tasks that are in selection, but do not have a coverage-error-call property (may be empty if everything is ok):"
find . -iname '*.yml' | xargs grep -L coverage-error-call.prp | grep -f candidates_error-coverage.txt
echo "Tasks that are in selection, but do not have a coverage-branches property (may be empty if everything is ok):"
find . -iname '*.yml' | xargs grep -L coverage-branches.prp | grep -f candidates_coverage.txt

get_testable_tasks.sh

#/bin/bash

## Usage: Adjust the benchmark folder and run the script from any directory.
## It will create two lists of testable tasks with one element 'sub-category/task' per line.
## The lists will be stored in the two files `candidates_coverage.txt` and `candidates_error-coverage.txt`
## in the current directory.
## Existing files will be overwritten!

BENCHMARK_FOLDER="../sv-benchmarks/c"
RESULTS_CSV="prtest.2020-11-12_15-09-31.results.CompileOnly.csv"

echo "Writing candidates_coverage.txt"
 for i in $(tail -n +4 "$RESULTS_CSV" | awk '$2 == "done" {print $1}'); do
    file="$BENCHMARK_FOLDER/$i"
    if yq -e 'all(.properties[]; .property_file != "../properties/termination.prp" or .expected_verdict == true)' "$file" > /dev/null; then
        dir_name=$(dirname "$file")
        if egrep -Eqx '[^e].*__VERIFIER_nondet_.*' "$dir_name/$(yq -r '.input_files' "$file")"; then
            echo $i
        fi
    fi
done > candidates_coverage.txt

echo "Writing candidates_error-coverage.txt"
for i in $(cat candidates_coverage.txt | grep xcsp); do
    if yq -e 'any(.properties[]; .property_file == "../properties/unreach-call.prp" and .expected_verdict == false)' $BENCHMARK_FOLDER/$i > /dev/null; then
        echo $i;
    fi;
done > candidates_error-coverage.txt

update_tasks.py

#!/usr/bin/env python3

## Usage:
## Run this script from `sv-benchmarks/c` (runtime varies, may be a few minutes).
## It will directly modify the task definition files.
## Changes can be inspected with `git diff`.

import argparse
import sys
import yaml
import logging
from pathlib import Path


def parse_args(argv):
    parser = argparse.ArgumentParser()
    parser.add_argument(
        "--candidates-error",
        required=True,
        help="List of task-definition candidates for coverage-error-call.prp",
    )
    parser.add_argument(
        "--candidates-branches",
        required=True,
        help="List of task-definition candidates for coverage-branches.prp",
    )

    args = parser.parse_args(argv)
    args.candidates_error = Path(args.candidates_error)
    args.candidates_branches = Path(args.candidates_branches)

    if not args.candidates_error.exists():
        raise ValueError(f"File doesn't exist: {str(args.candidates_error)}")
    if not args.candidates_branches.exists():
        raise ValueError(f"File doesn't exist: {str(args.candidates_branches)}")

    return args


def add_prop(candidate_list: Path, prop_to_add):
    with open(candidate_list) as inp:
        candidates = [Path(l.strip()) for l in inp.readlines()]
    for taskdef_file in candidates:
        assert taskdef_file.exists(), f"Doesn't exist: {str(taskdef_file)}"
        with open(taskdef_file) as inp:
            plain_content = inp.read()
        taskdef = yaml.safe_load(plain_content)
        if not any([p["property_file"] == prop_to_add for p in taskdef["properties"]]):
            logging.info(f"Adding {prop_to_add} to {taskdef_file}")
            with open(taskdef_file, "w") as outp:
                # we adjust the plain content, because we want to keep the diff minimal.
                # dumping the dict as a new yaml file may change the order of keys and add or remove synactic sugar
                outp.write(_add_prop(plain_content, prop_to_add))


def _add_prop(plain_content, prop_to_add) -> str:
    new_content = list()
    in_prop = False
    for line in plain_content.split("\n"):
        if in_prop and not line.startswith(" "):
            new_content.append(f"  - property_file: {prop_to_add}")
            in_prop = False
        new_content.append(line)
        if line.startswith("properties:"):
            in_prop = True
    return "\n".join(new_content)


def main(argv=None):
    if argv is None:
        argv = sys.argv[1:]
    args = parse_args(argv)

    add_prop(args.candidates_error, "../properties/coverage-error-call.prp")
    add_prop(args.candidates_branches, "../properties/coverage-branches.prp")


if __name__ == "__main__":
    logging.basicConfig(level=logging.INFO)
    sys.exit(main())