Transform sv-benchmark ldv-multiproperty tasks to yml format

verdict_to_yml.py

#!/usr/bin/env python3

import argparse
import os
import shutil
import sys

PROP_DIR = 'properties'
PREFIX = 'reach_error_linux_'

def parse_args(argv):
    parser = argparse.ArgumentParser()
    parser.add_argument("file", nargs="+", help=".verdict file")
    parser.add_argument("--force", "-f", action="store_true", default=False, help="force overwrite of existing files. Otherwise tool crashes on existing files")
    return parser.parse_args(argv)


def get_prop(error_method):
    assert error_method.startswith(PREFIX)
    return "unreach-call-" + error_method.replace(PREFIX, '')


def get_method(prop):
    return PREFIX + prop.replace("unreach-call-", '')


def get_verdicts(args_file):
    with open(args_file) as inp:
        content = inp.readlines()
    verdicts = dict()
    for line in content:
        s = line.split(":")
        assert len(s) == 2
        prop, verdict = get_prop(s[0]), s[1].strip()
        verdicts[prop] = verdict
    return verdicts


def remove_verdict(task_name):
    return task_name.replace('_true-unreach-call', '').replace('_false-unreach-call', '')


def get_task_name(args_file):
    return '.'.join(args_file.split('.')[:-1])


def get_new_task_name(original_name):
    return remove_verdict(original_name)


def rename_program(original_name, new_name, force=False) -> str:
    program_name = original_name + ".c"
    target = new_name + ".c"
    assert force or not os.path.exists(target), f"File exists: {target}"
    shutil.move(program_name, target)
    print(f"Moved {program_name} to {target}")
    return target


def get_prop_file(prop):
    prop_file = os.path.join(PROP_DIR, prop + ".prp")
    if not os.path.exists(prop_file):
        error_method = get_method(prop)
        with open(prop_file, 'w') as outp:
            outp.write(f"CHECK( init(main()), LTL(G ! call({error_method}())) )\n")
        print(f"Wrote {prop_file}")
    return prop_file


def get_properties_yml(verdicts) -> list:
    properties = list()
    if any(v == 'false' for v in verdicts.values()):
        verdict_all = 'false'
    else:
        verdict_all = 'true'
    properties.append(f"  - property_file: ALL-multi.prp\n    expected_verdict: {verdict_all}")
    for prop, verd in verdicts.items():
        prop_file = get_prop_file(prop)
        prop_str = f"  - property_file: {prop_file}\n    expected_verdict: {verd}"
        properties.append(prop_str)
    return properties


def write_yaml(task_name, program_name, verdicts, force=False):
    target = task_name + ".yml"
    properties = get_properties_yml(verdicts)
    content = f"""format_version: '1.0'

input_files: '{program_name}'

properties:
""" + '\n'.join(properties)
    assert force or not os.path.exists(target), f"File exists: {target}"
    with open(target, "w") as outp:
        outp.write(content)
    print(f"Wrote {target}")



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

    for f in args.file:
        verdicts = get_verdicts(f)
        original_name = get_task_name(f)
        new_name = get_new_task_name(original_name)

        program_name = rename_program(original_name, new_name, force=args.force)
        write_yaml(new_name, program_name, verdicts, force=args.force)


if __name__ == '__main__':
    sys.exit(main())