CoVeNN/runner.py at master · hocdot/CoVeNN · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
import argparse
import tqdm
import time
import os

##############################################################
ROOT_DIR = os.path.dirname(__file__)

parser = argparse.ArgumentParser()
parser.add_argument('--tool', type=str, required=True)
parser.add_argument('--backend', type=str, required=False)
parser.add_argument('--benchmark', type=str, required=True, choices=['vae', 'resnet'])
args = parser.parse_args()

TIMEOUT = 3600.0
BENCHMARK_TYPE = args.benchmark
RESULT_DIR = f'{ROOT_DIR}/results/{BENCHMARK_TYPE}'
CSV_NAME = 'instances_pth.csv'
BENCHMARK_DIR = f'{ROOT_DIR}/benchmarks/{BENCHMARK_TYPE}'
BENCHMARKS = os.listdir(BENCHMARK_DIR)


##############################################################
print(f'{RESULT_DIR = }')
print(f'{BENCHMARK_DIR = }')
print(f'{TIMEOUT = }')
print(f'{args.backend = }')
os.makedirs(RESULT_DIR, exist_ok=True)
##############################################################

if args.backend  == 'neuralsat':
    cmd =        './vnncomp_scripts/run_instance.sh v1 {category} {onnx_path} {vnnlib_path} {res_file} {timeout} > {log_file}'
    cmd_wo_log = './vnncomp_scripts/run_instance.sh v1 {category} {onnx_path} {vnnlib_path} {res_file} {timeout}'
elif args.backend  == 'abcrown':
    cmd =        './vnncomp_scripts/run_instance_abcrown.sh v1 {category} {onnx_path} {vnnlib_path} {res_file} {timeout} > {log_file}'
    cmd_wo_log = './vnncomp_scripts/run_instance_abcrown.sh v1 {category} {onnx_path} {vnnlib_path} {res_file} {timeout}'
else:
    cmd =        './vnncomp_scripts/run_instance.sh v1 {category} {onnx_path} {vnnlib_path} {res_file} {timeout} > {log_file}'
    cmd_wo_log = './vnncomp_scripts/run_instance.sh v1 {category} {onnx_path} {vnnlib_path} {res_file} {timeout}'

##############################################################

for benchmark_name in BENCHMARKS:

    benchmark_path = os.path.join(BENCHMARK_DIR, benchmark_name)
    OUTPUT_DIR = f'{RESULT_DIR}/{args.tool}/{benchmark_name}'
    os.makedirs(OUTPUT_DIR, exist_ok=True)

    instance_csv  = f'{benchmark_path}/{CSV_NAME}'
    if not os.path.exists(instance_csv):
        print(f'[!] Missing {instance_csv=}')
        continue

    instances = []
    for line in open(instance_csv).read().strip().split('\n'):
        onnx_path, vnnlib_path, _ = line.split(',')
        onnx_path = os.path.join(benchmark_path, onnx_path)
        vnnlib_path = os.path.join(benchmark_path, vnnlib_path)
        assert os.path.exists(onnx_path)
        assert os.path.exists(vnnlib_path), f'{vnnlib_path=}'
        instances.append((onnx_path, vnnlib_path))

    pbar = tqdm.tqdm(instances)
    pbar.set_description(f'Benchmark {benchmark_name} (timeout={TIMEOUT})')
    for idx, (onnx_path, vnnlib_path) in enumerate(pbar):
        onnx_name = os.path.splitext(os.path.basename(onnx_path))[0]
        vnnlib_name = os.path.splitext(os.path.basename(vnnlib_path))[0]
        output_name = f'{OUTPUT_DIR}/net_{onnx_name}_spec_{vnnlib_name}'

        config_dict = {
            'category': benchmark_name,
            'onnx_path': onnx_path,
            'vnnlib_path': vnnlib_path,
            'timeout': TIMEOUT,
            'res_file': f'{output_name}.res',
            'log_file': f'{output_name}.log',
            'error_file': f'{output_name}.error',
            'command_file': f'{output_name}.command',
        }

        print('\n-----------------------------------------------------')
        print(cmd_wo_log.format(**config_dict))
        print('-----------------------------------------------------\n')

        with open(config_dict['command_file'], 'w') as fp:
            fp.write(f'{cmd_wo_log.format(**config_dict)}\n')

        if os.path.exists(config_dict['res_file']):
            continue

        if os.path.exists(config_dict['error_file']):
            os.system(f"rm -f {config_dict['error_file']}")

        os.system(cmd.format(**config_dict))

        if not os.path.exists(config_dict['res_file']):
            # error
            with open(config_dict['error_file'], 'w') as fp:
                fp.write(f'error,0.0\n')

        time.sleep(5)