From 0ce0f795166bb283f7d61bcd502936334047f91d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Apr 2025 11:00:49 +0000 Subject: [PATCH 01/11] Turn verbose Kani run into JSON Given a run of Kani on the standard library with `--verbose` (and, typically, `autoharness`) enabled this produces a machine-processable JSON result via ``` python3 log_parser.py \ --kani-list-file kani-list.json \ --analysis-results-dir std_lib_analysis/results/ \ verification.log -o results.json ``` where each entry in the resulting JSON array is of the form ``` { "thread_id": int, "result": { "harness": string, "is_autoharness": bool, "autoharness_result": string, "with_contract": bool, "crate": string, "function": string, "function_safeness": string, "file_name": string, "n_failed_properties": int, "n_total_properties": int, "result": string, "time": string, "output": array } } ``` With the help of `jq` one can then conveniently compute various metrics, e.g., ``` jq 'map(select(.result.result == "SUCCESSFUL" and .result.is_autoharness == true and .result.crate == "core" and .result.function_safeness == "unsafe" and .result.with_contract == true)) | length' results.json ``` to find the number of successfully-verified contracts of unsafe functions in crate `core` that were verified using automatically generated harnesses. --- scripts/kani-std-analysis/log_parser.py | 403 ++++++++++++++++++++++++ 1 file changed, 403 insertions(+) create mode 100755 scripts/kani-std-analysis/log_parser.py diff --git a/scripts/kani-std-analysis/log_parser.py b/scripts/kani-std-analysis/log_parser.py new file mode 100755 index 0000000000000..5b5de34f68775 --- /dev/null +++ b/scripts/kani-std-analysis/log_parser.py @@ -0,0 +1,403 @@ +#!/usr/bin/env python3 + +import argparse +import csv +import glob +import json +import re +import sys + + +def read_kani_list(kani_list_file, scanner_data): + with open(kani_list_file, 'r') as f: + harnesses = json.load(f) + + harness_pattern1 = re.compile(r'^(.+)::verify::(check|verify)_(.+)$') + harness_pattern2 = re.compile( + r'^(.+)::verify::(non_null|nonzero)_check_(.+)$') + harness_pattern3 = re.compile( + r'^time::duration_verify::duration_as_nanos(_panics)?$') + harness_pattern4 = re.compile( + r'^intrinsics::verify::transmute_unchecked_(.+)$') + harness_pattern5 = re.compile( + r'^num::verify::(carrying|widening)_mul_(.+)$') + harness_pattern6 = re.compile( + r'^option::verify::verify_as_slice$') + standard_harnesses = {} + for file_name, l in harnesses['standard-harnesses'].items(): + for h in l: + assert standard_harnesses.get(h) is None + if harness_match := re.match(harness_pattern1, h): + fn = harness_match.group(1) + harness_match.group(3) + elif harness_match := re.match(harness_pattern2, h): + fn = harness_match.group(1) + harness_match.group(3) + elif harness_match := re.match(harness_pattern3, h): + fn = 'time::duration::as_nanos' + elif harness_match := re.match(harness_pattern4, h): + fn = 'intrinsics::transmute_unchecked' + elif harness_match := re.match(harness_pattern5, h): + fn = 'num::' + harness_match.group(1) + elif h == 'option::verify::verify_as_slice': + fn = 'option::Option::::as_slice' + else: + lt_replaced = h.replace('<\'_>', '<\'a>') + if scanner_data.get(h) is None and ( + scanner_data.get(lt_replaced) is not None): + fn = lt_replaced + else: + fn = h + fn_info = scanner_data.get( + fn, {'crate': None, 'target_safeness': None}) + standard_harnesses[h] = { + 'file_name': file_name, + 'crate': fn_info['crate'], + 'function': fn, + 'target_safeness': fn_info['target_safeness'] + } + + contract_harnesses = {} + for file_name, l in harnesses['contract-harnesses'].items(): + for h in l: + assert contract_harnesses.get(h) is None + contract_harnesses[h] = { + 'file_name': file_name, + 'crate': None, + 'target_safeness': None + } + for o in harnesses['contracts']: + for h in o['harnesses']: + fn = o['function'] + fn_info = scanner_data.get( + fn, {'crate': None, 'target_safeness': None}) + if h == 'kani::internal::automatic_harness': + entry = contract_harnesses[fn] + else: + entry = contract_harnesses[h] + if o['file'] != entry['file_name']: + # replace harness file name by target function file name + entry['file_name'] = o['file'] + entry['function'] = fn + entry['crate'] = fn_info['crate'] + entry['target_safeness'] = fn_info['target_safeness'] + + return contract_harnesses, standard_harnesses + + +def read_scanner_results(scanner_results_dir): + crate_pattern = re.compile(r'^.*/(.+)_scan_functions.csv$') + fn_to_info = {} + for csv_file in glob.glob(f'{scanner_results_dir}/*_scan_functions.csv'): + crate_match = re.match(crate_pattern, csv_file) + crate = crate_match.group(1) + with open(csv_file) as f: + csv_reader = csv.DictReader(f, delimiter=';') + for row in csv_reader: + fn = row['name'] + if row['is_unsafe'] == 'false': + target_safeness = 'unsafe' + elif row['has_unsafe_ops'] == 'true': + target_safeness = 'safe abstraction' + else: + target_safeness = 'safe' + if ex_entry := fn_to_info.get(fn): + # print(f'Scanner entry for {fn} already exists', + # file=sys.stderr) + # the below don't even hold! + # assert ex_entry['crate'] == crate + # assert ex_entry['target_safeness'] == target_safeness + continue + fn_to_info[fn] = { + 'crate': crate, + 'target_safeness': target_safeness + } + + return fn_to_info + + +def find_harness_map_entry( + harness, autoharness_for_contract, contract_harnesses, + standard_harnesses): + if entry := contract_harnesses.get(harness): + return (entry, True) + elif entry := standard_harnesses.get(harness): + with_contract = autoharness_for_contract is True + return (entry, with_contract) + else: + return None, None + + +def init_entry( + match_group, is_autoharness, autoharness_for_contract, + contract_harnesses, standard_harnesses, active_threads, + autoharness_info): + thread_id = int(match_group(1)) + harness = match_group(2) + (harness_map_entry, with_contract) = find_harness_map_entry( + harness, autoharness_for_contract, contract_harnesses, + standard_harnesses) + if is_autoharness: + assert autoharness_info[harness] == 'ok' + del autoharness_info[harness] + autoharness_result = 'ok' + else: + fn = harness_map_entry['function'] + if autoharness_info_entry := autoharness_info.get(fn): + autoharness_result = autoharness_info_entry + del autoharness_info_entry + else: + autoharness_result = None + # Assert that the slot is empty when work starts + if thread_id in active_threads: + print(f'Error: Thread {thread_id} is already active ' + + 'when starting new work', file=sys.stderr) + assert False + active_threads[thread_id] = { + 'harness': harness, + 'is_autoharness': is_autoharness, + 'autoharness_result': autoharness_result, + 'with_contract': with_contract, + 'crate': harness_map_entry['crate'], + 'function': harness_map_entry['function'], + 'function_safeness': harness_map_entry['target_safeness'], + 'file_name': harness_map_entry['file_name'], + 'n_failed_properties': None, + 'n_total_properties': None, + 'result': None, + 'time': None, + 'output': [] + } + + +def create_autoharness_result( + fn, autoharness_result, contract_harnesses, standard_harnesses, + scanner_data): + (harness_map_entry, with_contract) = find_harness_map_entry( + fn, None, contract_harnesses, standard_harnesses) + if harness_map_entry is None: + fn_info = scanner_data.get( + fn, {'crate': None, 'target_safeness': None}) + return { + 'harness': fn, + 'is_autoharness': True, + 'autoharness_result': autoharness_result, + 'with_contract': None, + 'crate': fn_info['crate'], + 'function': fn, + 'function_safeness': fn_info['target_safeness'], + 'file_name': None, + 'n_failed_properties': None, + 'n_total_properties': None, + 'result': None, + 'time': None, + 'output': [] + } + else: + return { + 'harness': fn, + 'is_autoharness': True, + 'autoharness_result': autoharness_result, + 'with_contract': with_contract, + 'crate': harness_map_entry['crate'], + 'function': harness_map_entry['function'], + 'function_safeness': harness_map_entry['target_safeness'], + 'file_name': harness_map_entry['file_name'], + 'n_failed_properties': None, + 'n_total_properties': None, + 'result': None, + 'time': None, + 'output': [] + } + + +def parse_autoharness_info(lines, i): + fn_ok_pattern = re.compile(r'^\| (.+?)\s+\|$') + fn_fail_pattern = re.compile(r'^\| (.+?)\s+\| (.+?)\s+\|$') + parser_state = 0 + in_fails = False + autoharness_info = {} + while i < len(lines): + line = lines[i].rstrip() + if parser_state == 0 and ( + line.startswith('Kani generated automatic harnesses for') or + line.startswith('Kani did not generate automatic harnesses')): + parser_state = 1 + i += 1 + elif parser_state == 0 and not line: + i += 1 + elif parser_state == 1 and ( + line.startswith('+--') or + line.startswith('| Chosen Function') or + line.startswith('If you believe that the provided reason') or + line.startswith('| Skipped Function')): + i += 1 + elif parser_state == 1 and line.startswith('+=='): + parser_state = 2 + i += 1 + elif parser_state == 2 and line.startswith('|--'): + i += 1 + elif parser_state == 2 and line.startswith('+--'): + i += 1 + if in_fails: + break + else: + parser_state = 0 + in_fails = True + else: + assert parser_state == 2 + if in_fails: + fn_match = re.match(fn_fail_pattern, line) + fn = fn_match.group(1) + # there may be multiple entries here + # assert autoharness_info.get(fn) is None + autoharness_info[fn] = fn_match.group(2) + else: + fn_match = re.match(fn_ok_pattern, line) + fn = fn_match.group(1) + assert autoharness_info.get(fn) is None + autoharness_info[fn] = 'ok' + i += 1 + + return i, autoharness_info + + +def parse_log_lines( + lines, contract_harnesses, standard_harnesses, scanner_data): + # Regular expressions for matching patterns + start_work_autoharness_contract_pattern = re.compile( + r'Thread (\d+): Autoharness: Checking function (.*)\'s contract ' + + r'against all possible inputs\.\.\.$') + start_work_autoharness_pattern = re.compile( + r'Thread (\d+): Autoharness: Checking function (.*) against all ' + + r'possible inputs\.\.\.$') + start_work_manual_pattern = re.compile( + r'Thread (\d+): Checking harness (.*)\.\.\.$') + end_work_pattern = re.compile(r'Thread (\d+):$') + property_pattern = re.compile(r'^ \*\* (\d+) of (\d+) failed') + end_result_pattern = re.compile(r'^VERIFICATION:- (.*)') + end_result_with_time_pattern = re.compile(r'^Verification Time: (.*)') + + # Track active threads and results + active_threads = {} # thread_id -> list of result lines + all_results = [] + thread_id = None + + i = 0 + while i < len(lines): + if lines[i].startswith('Kani generated automatic harnesses for'): + (i, autoharness_info) = parse_autoharness_info(lines, i) + + line = lines[i].rstrip() + i += 1 + + # Check if a thread is starting work + if start_match := start_work_autoharness_contract_pattern.search(line): + init_entry( + start_match.group, True, True, contract_harnesses, + standard_harnesses, active_threads, autoharness_info) + continue + elif start_match := start_work_autoharness_pattern.search(line): + init_entry( + start_match.group, True, False, contract_harnesses, + standard_harnesses, active_threads, autoharness_info) + continue + elif start_match := start_work_manual_pattern.search(line): + init_entry( + start_match.group, False, None, contract_harnesses, + standard_harnesses, active_threads, autoharness_info) + continue + + # Check if a thread is ending work + if end_match := end_work_pattern.search(line): + thread_id = int(end_match.group(1)) + assert thread_id in active_threads + continue + + # Check if we're at the end of a result section + if end_result_match := end_result_pattern.match(line): + assert thread_id is not None + active_threads[thread_id]['result'] = end_result_match.group(1) + next_i = i + 1 + if next_i < len(lines): + next_line = lines[next_i].rstrip() + if next_line.startswith('CBMC timed out.'): + active_threads[thread_id]['time'] = 'TO' + active_threads[thread_id]['output'].append(next_line) + elif next_line.startswith('** WARNING:'): + active_threads[thread_id]['output'].append(next_line) + elif next_line.startswith('[Kani]'): + active_threads[thread_id]['output'].append(next_line) + active_threads[thread_id]['output'].append( + lines[next_i + 2].rstrip()) + next_i += 1 + elif t_match := end_result_with_time_pattern.match(next_line): + active_threads[thread_id]['time'] = t_match.group(1) + if next_i + 1 < len(lines): + next_line = lines[next_i + 1].rstrip() + if t_match := end_result_with_time_pattern.match( + next_line): + active_threads[thread_id]['time'] = t_match.group(1) + all_results.append({ + 'thread_id': thread_id, + 'result': active_threads[thread_id] + }) + del active_threads[thread_id] + thread_id = None + elif property_match := property_pattern.match(line): + assert thread_id is not None + active_threads[thread_id]['n_failed_properties'] = int( + property_match.group(1)) + active_threads[thread_id]['n_total_properties'] = int( + property_match.group(2)) + elif thread_id is not None: + if line not in ['VERIFICATION RESULT:', '']: + active_threads[thread_id]['output'].append(line) + + assert len(active_threads) == 0 + + for fn, value in autoharness_info.items(): + all_results.append({'result': create_autoharness_result( + fn, value, contract_harnesses, standard_harnesses, scanner_data)}) + + return all_results + + +def main(): + parser = argparse.ArgumentParser( + description='Parse log file of multi-threaded autoharness results') + parser.add_argument('log_file', help='Path to the log file to parse') + parser.add_argument( + '-o', '--output', help='Output file path (default: stdout)') + parser.add_argument( + '--kani-list-file', + type=str, + default='kani-list.json', + help='Path to the JSON file containing the Kani list data ' + + '(default: kani-list.json)') + parser.add_argument( + '--analysis-results-dir', + type=str, + default='/tmp/std_lib_analysis/results', + help='Path to the folder file containing the std-analysis.sh ' + + 'results (default: /tmp/std_lib_analysis/results)') + args = parser.parse_args() + + scanner_data = read_scanner_results(args.analysis_results_dir) + + (contract_harnesses, standard_harnesses) = read_kani_list( + args.kani_list_file, scanner_data) + + with open(args.log_file, 'r') as f: + log_lines = f.readlines() + + results = parse_log_lines( + log_lines, contract_harnesses, standard_harnesses, scanner_data) + + if args.output: + with open(args.output, 'w') as f: + json.dump(results, f, indent=2) + else: + print(json.dumps(results, indent=2)) + + +if __name__ == '__main__': + main() From 4bc3a53fe03c3efb0a8ea61f91947d8c32b6e7b7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 24 Apr 2025 12:16:25 +0000 Subject: [PATCH 02/11] Address comments, update to more recent Kani version --- scripts/kani-std-analysis/log_parser.py | 326 +++++++++++++++++------- 1 file changed, 237 insertions(+), 89 deletions(-) diff --git a/scripts/kani-std-analysis/log_parser.py b/scripts/kani-std-analysis/log_parser.py index 5b5de34f68775..dc8ba91ab9a96 100755 --- a/scripts/kani-std-analysis/log_parser.py +++ b/scripts/kani-std-analysis/log_parser.py @@ -1,5 +1,49 @@ #!/usr/bin/env python3 +""" +Parse log file of multi-threaded Kani run (terse output) into JSON. +Given a run of Kani on the standard library with `--jobs= +--output-format=terse` (and, typically, `autoharness`) enabled this produces +a machine-processable JSON result via +``` +python3 log_parser.py \ + --kani-list-file kani-list.json \ + --analysis-results-dir std_lib_analysis/results/ \ + verification.log -o results.json +``` +where each entry in the resulting JSON array is of the form +``` +{ + "thread_id": int, + "result": { + "harness": string, + "is_autoharness": bool, + "autoharness_result": string, + "with_contract": bool, + "crate": string, + "function": string, + "function_safeness": string, + "file_name": string, + "n_failed_properties": int, + "n_total_properties": int, + "result": string, + "time": string, + "output": array + } +} +``` +With the help of `jq` one can then conveniently compute various metrics: +``` +jq 'map(select(.result.result == "SUCCESSFUL" and + .result.is_autoharness == true and + .result.crate == "core" and + .result.function_safeness == "unsafe" and + .result.with_contract == true)) | length' results.json +``` +to find the number of successfully-verified contracts of unsafe functions in +crate `core` that were verified using automatically generated harnesses. +""" + import argparse import csv import glob @@ -8,10 +52,50 @@ import sys +def read_scanner_results(scanner_results_dir): + """Parse information produced by Kani's scanner tool.""" + crate_pattern = re.compile(r'^.*/(.+)_scan_functions.csv$') + fn_to_info = {} + for csv_file in glob.glob(f'{scanner_results_dir}/*_scan_functions.csv'): + crate_match = re.match(crate_pattern, csv_file) + crate = crate_match.group(1) + with open(csv_file) as f: + csv_reader = csv.DictReader(f, delimiter=';') + for row in csv_reader: + fn = row['name'] + if row['is_unsafe'] == 'true': + target_safeness = 'unsafe' + elif row['has_unsafe_ops'] == 'true': + target_safeness = 'safe abstraction' + else: + target_safeness = 'safe' + if fn_to_info.get(fn) is None: + fn_to_info[fn] = {} + else: + # assert fn_to_info[fn].get(crate) is None + if ex_entry := fn_to_info[fn].get(crate): + # print(f'Scanner entry for {fn} in {crate} already exists', + # file=sys.stderr) + # the below doesn't even hold! + # assert ex_entry['target_safeness'] == target_safeness + continue + fn_to_info[fn][crate] = { + 'target_safeness': target_safeness + } + + return fn_to_info + + def read_kani_list(kani_list_file, scanner_data): + """Read from kani_list_file (a JSON file produced using kani list) and + combine the information with the scanner's data.""" with open(kani_list_file, 'r') as f: harnesses = json.load(f) + # There is no reasonable way to reliably deduce which function a + # non-contract harness is targeting for verification, so we apply a bunch + # of patterns that we know are being used. We expect that, over time, + # manual harnesses will largely disappear. harness_pattern1 = re.compile(r'^(.+)::verify::(check|verify)_(.+)$') harness_pattern2 = re.compile( r'^(.+)::verify::(non_null|nonzero)_check_(.+)$') @@ -40,20 +124,33 @@ def read_kani_list(kani_list_file, scanner_data): elif h == 'option::verify::verify_as_slice': fn = 'option::Option::::as_slice' else: - lt_replaced = h.replace('<\'_>', '<\'a>') - if scanner_data.get(h) is None and ( - scanner_data.get(lt_replaced) is not None): - fn = lt_replaced - else: - fn = h - fn_info = scanner_data.get( - fn, {'crate': None, 'target_safeness': None}) - standard_harnesses[h] = { - 'file_name': file_name, - 'crate': fn_info['crate'], - 'function': fn, - 'target_safeness': fn_info['target_safeness'] - } + fn = h + fn_info = scanner_data.get(fn) + if fn_info is None: + standard_harnesses[h] = { + 'file_name': file_name, + 'crate': None, + 'function': fn, + 'target_safeness': None + } + elif len(fn_info.keys()) > 1: + crates = list(fn_info.keys()) + target_safenesses = [ts['target_safenesses'] + for _, ts in fn_info.items()] + standard_harnesses[h] = { + 'file_name': file_name, + 'crate': crates, + 'function': fn, + 'target_safeness': target_safenesses + } + else: + crate = list(fn_info.keys())[0] + standard_harnesses[h] = { + 'file_name': file_name, + 'crate': crate, + 'function': fn, + 'target_safeness': fn_info[crate]['target_safeness'] + } contract_harnesses = {} for file_name, l in harnesses['contract-harnesses'].items(): @@ -67,9 +164,9 @@ def read_kani_list(kani_list_file, scanner_data): for o in harnesses['contracts']: for h in o['harnesses']: fn = o['function'] - fn_info = scanner_data.get( - fn, {'crate': None, 'target_safeness': None}) - if h == 'kani::internal::automatic_harness': + if h == 'core::kani::internal::automatic_harness': + entry = contract_harnesses[fn] + elif h == 'kani::internal::automatic_harness': entry = contract_harnesses[fn] else: entry = contract_harnesses[h] @@ -77,71 +174,70 @@ def read_kani_list(kani_list_file, scanner_data): # replace harness file name by target function file name entry['file_name'] = o['file'] entry['function'] = fn - entry['crate'] = fn_info['crate'] - entry['target_safeness'] = fn_info['target_safeness'] - - return contract_harnesses, standard_harnesses - - -def read_scanner_results(scanner_results_dir): - crate_pattern = re.compile(r'^.*/(.+)_scan_functions.csv$') - fn_to_info = {} - for csv_file in glob.glob(f'{scanner_results_dir}/*_scan_functions.csv'): - crate_match = re.match(crate_pattern, csv_file) - crate = crate_match.group(1) - with open(csv_file) as f: - csv_reader = csv.DictReader(f, delimiter=';') - for row in csv_reader: - fn = row['name'] - if row['is_unsafe'] == 'false': - target_safeness = 'unsafe' - elif row['has_unsafe_ops'] == 'true': - target_safeness = 'safe abstraction' + fn_info = scanner_data.get(fn) + if fn_info is not None: + if len(fn_info.keys()) > 1: + crates = list(fn_info.keys()) + target_safenesses = [ts['target_safenesses'] + for _, ts in fn_info.items()] + entry['crate'] = crates + entry['target_safeness'] = target_safenesses else: - target_safeness = 'safe' - if ex_entry := fn_to_info.get(fn): - # print(f'Scanner entry for {fn} already exists', - # file=sys.stderr) - # the below don't even hold! - # assert ex_entry['crate'] == crate - # assert ex_entry['target_safeness'] == target_safeness - continue - fn_to_info[fn] = { - 'crate': crate, - 'target_safeness': target_safeness - } + crate = list(fn_info.keys())[0] + entry['crate'] = crate + entry['target_safeness'] = fn_info[crate][ + 'target_safeness'] - return fn_to_info + return contract_harnesses, standard_harnesses def find_harness_map_entry( harness, autoharness_for_contract, contract_harnesses, standard_harnesses): + """Find harness in either contract- or standard harness dict.""" if entry := contract_harnesses.get(harness): return (entry, True) elif entry := standard_harnesses.get(harness): with_contract = autoharness_for_contract is True return (entry, with_contract) else: - return None, None + return { + 'crate': None, + 'function': None, + 'target_safeness': None, + 'file_name': None + }, None def init_entry( match_group, is_autoharness, autoharness_for_contract, contract_harnesses, standard_harnesses, active_threads, autoharness_info): + """Initialize verification result entry.""" thread_id = int(match_group(1)) harness = match_group(2) (harness_map_entry, with_contract) = find_harness_map_entry( harness, autoharness_for_contract, contract_harnesses, standard_harnesses) + crate = harness_map_entry['crate'] if is_autoharness: - assert autoharness_info[harness] == 'ok' - del autoharness_info[harness] + if crate is None: + print(f'No autoharness info for {harness}', file=sys.stderr) + else: + if autoharness_info.get(crate) is None: + print(f'No autoharness info for {crate}', + file=sys.stderr) + else: + if autoharness_info[crate][harness] != 'ok': + print(f'Unexpected autoharness info for {harness} in {crate}', + file=sys.stderr) + del autoharness_info[crate][harness] autoharness_result = 'ok' else: fn = harness_map_entry['function'] - if autoharness_info_entry := autoharness_info.get(fn): + if autoharness_info.get(crate) is None: + autoharness_result = None + elif autoharness_info_entry := autoharness_info[crate].get(fn): autoharness_result = autoharness_info_entry del autoharness_info_entry else: @@ -156,7 +252,7 @@ def init_entry( 'is_autoharness': is_autoharness, 'autoharness_result': autoharness_result, 'with_contract': with_contract, - 'crate': harness_map_entry['crate'], + 'crate': crate, 'function': harness_map_entry['function'], 'function_safeness': harness_map_entry['target_safeness'], 'file_name': harness_map_entry['file_name'], @@ -169,28 +265,65 @@ def init_entry( def create_autoharness_result( - fn, autoharness_result, contract_harnesses, standard_harnesses, + crate, fn, autoharness_result, contract_harnesses, standard_harnesses, scanner_data): + """Initialize entries from autoharness summary tables.""" (harness_map_entry, with_contract) = find_harness_map_entry( fn, None, contract_harnesses, standard_harnesses) if harness_map_entry is None: - fn_info = scanner_data.get( - fn, {'crate': None, 'target_safeness': None}) - return { - 'harness': fn, - 'is_autoharness': True, - 'autoharness_result': autoharness_result, - 'with_contract': None, - 'crate': fn_info['crate'], - 'function': fn, - 'function_safeness': fn_info['target_safeness'], - 'file_name': None, - 'n_failed_properties': None, - 'n_total_properties': None, - 'result': None, - 'time': None, - 'output': [] - } + fn_info = scanner_data.get(fn) + if fn_info is None: + return { + 'harness': fn, + 'is_autoharness': True, + 'autoharness_result': autoharness_result, + 'with_contract': None, + 'crate': None, + 'function': fn, + 'function_safeness': None, + 'file_name': None, + 'n_failed_properties': None, + 'n_total_properties': None, + 'result': None, + 'time': None, + 'output': [] + } + elif len(fn_info.keys()) > 1: + crates = list(fn_info.keys()) + target_safenesses = [ts['target_safenesses'] + for _, ts in fn_info.items()] + return { + 'harness': fn, + 'is_autoharness': True, + 'autoharness_result': autoharness_result, + 'with_contract': None, + 'crate': crates, + 'function': fn, + 'function_safeness': target_safenesses, + 'file_name': None, + 'n_failed_properties': None, + 'n_total_properties': None, + 'result': None, + 'time': None, + 'output': [] + } + else: + crate = list(fn_info.keys())[0] + return { + 'harness': fn, + 'is_autoharness': True, + 'autoharness_result': autoharness_result, + 'with_contract': None, + 'crate': crate, + 'function': fn, + 'function_safeness': fn_info[crate]['target_safeness'], + 'file_name': None, + 'n_failed_properties': None, + 'n_total_properties': None, + 'result': None, + 'time': None, + 'output': [] + } else: return { 'harness': fn, @@ -210,8 +343,11 @@ def create_autoharness_result( def parse_autoharness_info(lines, i): - fn_ok_pattern = re.compile(r'^\| (.+?)\s+\|$') - fn_fail_pattern = re.compile(r'^\| (.+?)\s+\| (.+?)\s+\|$') + """Parse summary tables provided by autoharness.""" + ok_header_pattern = re.compile(r'^\| Crate\s+\| Selected Function') + fail_header_pattern = re.compile(r'\| Crate\s+\| Skipped Function') + fn_ok_pattern = re.compile(r'^\| (.+?)\s+\| (.+?)\s+\|$') + fn_fail_pattern = re.compile(r'^\| (.+?)\s+\| (.+?)\s+\| (.+?)\s+\|$') parser_state = 0 in_fails = False autoharness_info = {} @@ -226,9 +362,9 @@ def parse_autoharness_info(lines, i): i += 1 elif parser_state == 1 and ( line.startswith('+--') or - line.startswith('| Chosen Function') or line.startswith('If you believe that the provided reason') or - line.startswith('| Skipped Function')): + re.match(ok_header_pattern, line) is not None or + re.match(fail_header_pattern, line) is not None): i += 1 elif parser_state == 1 and line.startswith('+=='): parser_state = 2 @@ -246,15 +382,20 @@ def parse_autoharness_info(lines, i): assert parser_state == 2 if in_fails: fn_match = re.match(fn_fail_pattern, line) - fn = fn_match.group(1) - # there may be multiple entries here - # assert autoharness_info.get(fn) is None - autoharness_info[fn] = fn_match.group(2) + crate = fn_match.group(1) + if autoharness_info.get(crate) is None: + autoharness_info[crate] = {} + fn = fn_match.group(2) + assert autoharness_info[crate].get(fn) is None + autoharness_info[crate][fn] = fn_match.group(3) else: fn_match = re.match(fn_ok_pattern, line) - fn = fn_match.group(1) - assert autoharness_info.get(fn) is None - autoharness_info[fn] = 'ok' + crate = fn_match.group(1) + if autoharness_info.get(crate) is None: + autoharness_info[crate] = {} + fn = fn_match.group(2) + assert autoharness_info[crate].get(fn) is None + autoharness_info[crate][fn] = 'ok' i += 1 return i, autoharness_info @@ -262,6 +403,8 @@ def parse_autoharness_info(lines, i): def parse_log_lines( lines, contract_harnesses, standard_harnesses, scanner_data): + """Parse (terse) output from multi-threaded Kani run while considering list + and scanner data.""" # Regular expressions for matching patterns start_work_autoharness_contract_pattern = re.compile( r'Thread (\d+): Autoharness: Checking function (.*)\'s contract ' + @@ -316,7 +459,7 @@ def parse_log_lines( if end_result_match := end_result_pattern.match(line): assert thread_id is not None active_threads[thread_id]['result'] = end_result_match.group(1) - next_i = i + 1 + next_i = i if next_i < len(lines): next_line = lines[next_i].rstrip() if next_line.startswith('CBMC timed out.'): @@ -354,16 +497,21 @@ def parse_log_lines( assert len(active_threads) == 0 - for fn, value in autoharness_info.items(): - all_results.append({'result': create_autoharness_result( - fn, value, contract_harnesses, standard_harnesses, scanner_data)}) + for crate, crate_value in autoharness_info.items(): + for fn, value in crate_value.items(): + all_results.append({ + 'result': create_autoharness_result( + crate, fn, value, contract_harnesses, standard_harnesses, + scanner_data) + }) return all_results def main(): parser = argparse.ArgumentParser( - description='Parse log file of multi-threaded autoharness results') + description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) parser.add_argument('log_file', help='Path to the log file to parse') parser.add_argument( '-o', '--output', help='Output file path (default: stdout)') From 1a05e226688fa0fc68aa7408781c2c89fd9a6849 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Apr 2025 19:41:03 +0000 Subject: [PATCH 03/11] Add is_public, fixes --- scripts/kani-std-analysis/log_parser.py | 45 ++++++++++++++++++------- 1 file changed, 32 insertions(+), 13 deletions(-) diff --git a/scripts/kani-std-analysis/log_parser.py b/scripts/kani-std-analysis/log_parser.py index dc8ba91ab9a96..f9103fa892a0f 100755 --- a/scripts/kani-std-analysis/log_parser.py +++ b/scripts/kani-std-analysis/log_parser.py @@ -80,7 +80,8 @@ def read_scanner_results(scanner_results_dir): # assert ex_entry['target_safeness'] == target_safeness continue fn_to_info[fn][crate] = { - 'target_safeness': target_safeness + 'target_safeness': target_safeness, + 'public_target': row['is_public'] == 'true' } return fn_to_info @@ -96,9 +97,9 @@ def read_kani_list(kani_list_file, scanner_data): # non-contract harness is targeting for verification, so we apply a bunch # of patterns that we know are being used. We expect that, over time, # manual harnesses will largely disappear. - harness_pattern1 = re.compile(r'^(.+)::verify::(check|verify)_(.+)$') + harness_pattern1 = re.compile(r'^(.+::)verify::(check|verify)_(.+)$') harness_pattern2 = re.compile( - r'^(.+)::verify::(non_null|nonzero)_check_(.+)$') + r'^(.+::)verify::(non_null|nonzero)_check_(.+)$') harness_pattern3 = re.compile( r'^time::duration_verify::duration_as_nanos(_panics)?$') harness_pattern4 = re.compile( @@ -131,17 +132,21 @@ def read_kani_list(kani_list_file, scanner_data): 'file_name': file_name, 'crate': None, 'function': fn, - 'target_safeness': None + 'target_safeness': None, + 'public_target': None } elif len(fn_info.keys()) > 1: crates = list(fn_info.keys()) - target_safenesses = [ts['target_safenesses'] - for _, ts in fn_info.items()] + target_safenesses = [e['target_safenesses'] + for _, e in fn_info.items()] + public_targets = [e['public_target'] + for _, e in fn_info.items()] standard_harnesses[h] = { 'file_name': file_name, 'crate': crates, 'function': fn, - 'target_safeness': target_safenesses + 'target_safeness': target_safenesses, + 'public_target': public_targets } else: crate = list(fn_info.keys())[0] @@ -149,7 +154,8 @@ def read_kani_list(kani_list_file, scanner_data): 'file_name': file_name, 'crate': crate, 'function': fn, - 'target_safeness': fn_info[crate]['target_safeness'] + 'target_safeness': fn_info[crate]['target_safeness'], + 'public_target': fn_info[crate]['public_target'] } contract_harnesses = {} @@ -159,7 +165,8 @@ def read_kani_list(kani_list_file, scanner_data): contract_harnesses[h] = { 'file_name': file_name, 'crate': None, - 'target_safeness': None + 'target_safeness': None, + 'public_target': None } for o in harnesses['contracts']: for h in o['harnesses']: @@ -178,15 +185,19 @@ def read_kani_list(kani_list_file, scanner_data): if fn_info is not None: if len(fn_info.keys()) > 1: crates = list(fn_info.keys()) - target_safenesses = [ts['target_safenesses'] - for _, ts in fn_info.items()] + target_safenesses = [e['target_safenesses'] + for _, e in fn_info.items()] + public_targets = [e['public_target'] + for _, e in fn_info.items()] entry['crate'] = crates entry['target_safeness'] = target_safenesses + entry['public_target'] = public_targets else: crate = list(fn_info.keys())[0] entry['crate'] = crate entry['target_safeness'] = fn_info[crate][ 'target_safeness'] + entry['public_target'] = fn_info[crate]['public_target'] return contract_harnesses, standard_harnesses @@ -205,6 +216,7 @@ def find_harness_map_entry( 'crate': None, 'function': None, 'target_safeness': None, + 'public_target': None, 'file_name': None }, None @@ -255,6 +267,7 @@ def init_entry( 'crate': crate, 'function': harness_map_entry['function'], 'function_safeness': harness_map_entry['target_safeness'], + 'public_target': harness_map_entry['public_target'], 'file_name': harness_map_entry['file_name'], 'n_failed_properties': None, 'n_total_properties': None, @@ -281,6 +294,7 @@ def create_autoharness_result( 'crate': None, 'function': fn, 'function_safeness': None, + 'public_target': None, 'file_name': None, 'n_failed_properties': None, 'n_total_properties': None, @@ -290,8 +304,10 @@ def create_autoharness_result( } elif len(fn_info.keys()) > 1: crates = list(fn_info.keys()) - target_safenesses = [ts['target_safenesses'] - for _, ts in fn_info.items()] + target_safenesses = [e['target_safenesses'] + for _, e in fn_info.items()] + public_targets = [e['public_target'] + for _, e in fn_info.items()] return { 'harness': fn, 'is_autoharness': True, @@ -300,6 +316,7 @@ def create_autoharness_result( 'crate': crates, 'function': fn, 'function_safeness': target_safenesses, + 'public_target': public_targets, 'file_name': None, 'n_failed_properties': None, 'n_total_properties': None, @@ -317,6 +334,7 @@ def create_autoharness_result( 'crate': crate, 'function': fn, 'function_safeness': fn_info[crate]['target_safeness'], + 'public_target': fn_info[crate]['public_target'], 'file_name': None, 'n_failed_properties': None, 'n_total_properties': None, @@ -333,6 +351,7 @@ def create_autoharness_result( 'crate': harness_map_entry['crate'], 'function': harness_map_entry['function'], 'function_safeness': harness_map_entry['target_safeness'], + 'public_target': harness_map_entry['public_target'], 'file_name': harness_map_entry['file_name'], 'n_failed_properties': None, 'n_total_properties': None, From f14ef457ff589b7829577dda9cb56ef693e91658 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Apr 2025 20:37:29 +0000 Subject: [PATCH 04/11] Use log parser in workflow --- .github/workflows/kani.yml | 107 ++++++++++++++++++++++++++++++++++++- scripts/run-kani.sh | 1 - 2 files changed, 105 insertions(+), 3 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index fd949f8eef552..57b5cf801595b 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -53,7 +53,7 @@ jobs: - name: Run Kani Verification run: head/scripts/run-kani.sh --path ${{github.workspace}}/head - kani-autoharness: + kani_autoharness: name: Verify std library using autoharness runs-on: ${{ matrix.os }} strategy: @@ -124,7 +124,110 @@ jobs: --exclude-pattern ::precondition_check \ --harness-timeout 5m \ --default-unwind 1000 \ - --jobs=3 --output-format=terse + --jobs=3 --output-format=terse | tee autoharness-verification.log + gzip autoharness-verification.log + + - name: Upload Autoharness Verification Log + uses: actions/upload-artifact@v4 + with: + name: ${{ matrix.os }}-autoharness-verification.log.gz + path: autoharness-verification.log.gz + if-no-files-found: error + # Aggressively short retention: we don't really need these + retention-days: 3 + + run_kani_metrics: + name: Kani Metrics + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + include: + - os: ubuntu-latest + base: ubuntu + - os: macos-latest + base: macos + fail-fast: true + + steps: + # Step 1: Check out the repository + - name: Checkout Repository + uses: actions/checkout@v4 + with: + submodules: true + + # Step 2: Run list on the std library + - name: Run Kani Metrics + run: | + scripts/run-kani.sh --run metrics --with-autoharness + pushd /tmp/std_lib_analysis + tar czf results.tar.gz results + popd + + - name: Upload kani-list.json + uses: actions/upload-artifact@v4 + with: + name: ${{ matrix.os }}-kani-list.json + path: kani-list.json + if-no-files-found: error + # Aggressively short retention: we don't really need these + retention-days: 3 + + - name: Upload scanner results + uses: actions/upload-artifact@v4 + with: + name: ${{ matrix.os }}-results.tar.gz + path: /tmp/std_lib_analysis/results.tar.gz + if-no-files-found: error + # Aggressively short retention: we don't really need these + retention-days: 3 + + run-log-analysis: + name: TestLocalToolchain + needs: [run_kani_metrics, kani_autoharness] + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + include: + - os: ubuntu-latest + base: ubuntu + - os: macos-latest + base: macos + fail-fast: false + + steps: + - name: Download log + uses: actions/download-artifact@v4 + with: + name: ${{ matrix.os }}-autoharness-verification.log.gz + + - name: Download kani-list.json + uses: actions/download-artifact@v4 + with: + name: ${{ matrix.os }}-kani-list.json + + - name: Download scanner results + uses: actions/download-artifact@v4 + with: + name: ${{ matrix.os }}-results.tar.gz + + - name: Run log parser + run: | + gunzip ${{ matrix.os }}-autoharness-verification.log.gz + tar xzf ${{ matrix.os }}-results.tar.gz + python3 scripts/kani-std-analysis/log_parser.py \ + --kani-list-file kani-list.json \ + --analysis-results-dir results/ \ + ${{ matrix.os }}-autoharness-verification.log \ + -o results.json + + - name: Upload JSON + uses: actions/upload-artifact@v4 + with: + name: ${{ matrix.os }}-results.json + path: results.json + if-no-files-found: error run-kani-list: name: Kani List diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 1abe73df88b12..e79bda3d6c108 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -340,7 +340,6 @@ main() { --kani-list-file $current_dir/kani-list.json \ --metrics-file metrics-data-std.json popd - rm kani-list.json elif [[ "$run_command" == "autoharness-analyzer" ]]; then echo "Running Kani autoharness codegen command..." "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \ From ef062e8e1b497227db8678cee1561b6bcc7501ed Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 09:24:51 +0000 Subject: [PATCH 05/11] Ensure cleanup --- .github/workflows/kani-metrics.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml index 106ed3e160b4b..f2cf53b94c5da 100644 --- a/.github/workflows/kani-metrics.yml +++ b/.github/workflows/kani-metrics.yml @@ -26,7 +26,9 @@ jobs: python-version: '3.x' - name: Compute Kani Metrics - run: ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}} + run: | + ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}} + rm kani-list.json - name: Create Pull Request uses: peter-evans/create-pull-request@v7 From e1e273ffef2175c682069d74b988cb7bed6fe563 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 09:27:28 +0000 Subject: [PATCH 06/11] Fixup Python dep --- .github/workflows/kani.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 57b5cf801595b..a6d6e91bad633 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -156,6 +156,12 @@ jobs: with: submodules: true + # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed + - name: Set up Python + uses: actions/setup-python@v4 + with: + python-version: '3.x' + # Step 2: Run list on the std library - name: Run Kani Metrics run: | From 213026ed5ed0fbde4a3a27039cda2f48492b0b91 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 09:28:44 +0000 Subject: [PATCH 07/11] Name --- .github/workflows/kani.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index a6d6e91bad633..37fb31fa4565e 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -189,7 +189,7 @@ jobs: retention-days: 3 run-log-analysis: - name: TestLocalToolchain + name: Build JSON from logs needs: [run_kani_metrics, kani_autoharness] runs-on: ${{ matrix.os }} strategy: From 5ffbbdcc5ff4062db0991d67275595166c0f495f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 12:49:29 +0000 Subject: [PATCH 08/11] DEBUG --- .github/workflows/kani.yml | 43 ++------------------------------------ 1 file changed, 2 insertions(+), 41 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 37fb31fa4565e..8e0ed627aa47e 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -82,48 +82,7 @@ jobs: run: | scripts/run-kani.sh --run autoharness --kani-args \ --include-pattern alloc::layout::Layout::from_size_align \ - --include-pattern ascii::ascii_char::AsciiChar::from_u8 \ - --include-pattern char::convert::from_u32_unchecked \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::count_ones" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern "num::nonzero::NonZero::::rotate_" \ - --include-pattern ptr::align_offset::mod_inv \ - --include-pattern ptr::alignment::Alignment::as_nonzero \ - --include-pattern ptr::alignment::Alignment::as_usize \ - --include-pattern ptr::alignment::Alignment::log2 \ - --include-pattern ptr::alignment::Alignment::mask \ - --include-pattern ptr::alignment::Alignment::new \ - --include-pattern ptr::alignment::Alignment::new_unchecked \ - --include-pattern time::Duration::from_micros \ - --include-pattern time::Duration::from_millis \ - --include-pattern time::Duration::from_nanos \ - --include-pattern time::Duration::from_secs \ - --exclude-pattern time::Duration::from_secs_f \ - --include-pattern unicode::unicode_data::conversions::to_ \ --exclude-pattern ::precondition_check \ - --harness-timeout 5m \ - --default-unwind 1000 \ --jobs=3 --output-format=terse | tee autoharness-verification.log gzip autoharness-verification.log @@ -220,6 +179,8 @@ jobs: - name: Run log parser run: | + # DEBUG + ls -R gunzip ${{ matrix.os }}-autoharness-verification.log.gz tar xzf ${{ matrix.os }}-results.tar.gz python3 scripts/kani-std-analysis/log_parser.py \ From 2f6b18f60bef047b23c93f0fcc19fe73f554e782 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 17:16:59 +0000 Subject: [PATCH 09/11] Revert "DEBUG" This reverts commit 5ffbbdcc5ff4062db0991d67275595166c0f495f. --- .github/workflows/kani.yml | 43 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 41 insertions(+), 2 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 8e0ed627aa47e..37fb31fa4565e 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -82,7 +82,48 @@ jobs: run: | scripts/run-kani.sh --run autoharness --kani-args \ --include-pattern alloc::layout::Layout::from_size_align \ + --include-pattern ascii::ascii_char::AsciiChar::from_u8 \ + --include-pattern char::convert::from_u32_unchecked \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern ptr::align_offset::mod_inv \ + --include-pattern ptr::alignment::Alignment::as_nonzero \ + --include-pattern ptr::alignment::Alignment::as_usize \ + --include-pattern ptr::alignment::Alignment::log2 \ + --include-pattern ptr::alignment::Alignment::mask \ + --include-pattern ptr::alignment::Alignment::new \ + --include-pattern ptr::alignment::Alignment::new_unchecked \ + --include-pattern time::Duration::from_micros \ + --include-pattern time::Duration::from_millis \ + --include-pattern time::Duration::from_nanos \ + --include-pattern time::Duration::from_secs \ + --exclude-pattern time::Duration::from_secs_f \ + --include-pattern unicode::unicode_data::conversions::to_ \ --exclude-pattern ::precondition_check \ + --harness-timeout 5m \ + --default-unwind 1000 \ --jobs=3 --output-format=terse | tee autoharness-verification.log gzip autoharness-verification.log @@ -179,8 +220,6 @@ jobs: - name: Run log parser run: | - # DEBUG - ls -R gunzip ${{ matrix.os }}-autoharness-verification.log.gz tar xzf ${{ matrix.os }}-results.tar.gz python3 scripts/kani-std-analysis/log_parser.py \ From e5609b723d30db43b96d590bddd2714049e3c74b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 17:21:31 +0000 Subject: [PATCH 10/11] Fix file names --- .github/workflows/kani.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 37fb31fa4565e..b7552a89c80b6 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -220,12 +220,12 @@ jobs: - name: Run log parser run: | - gunzip ${{ matrix.os }}-autoharness-verification.log.gz - tar xzf ${{ matrix.os }}-results.tar.gz + gunzip autoharness-verification.log.gz + tar xzf results.tar.gz python3 scripts/kani-std-analysis/log_parser.py \ --kani-list-file kani-list.json \ --analysis-results-dir results/ \ - ${{ matrix.os }}-autoharness-verification.log \ + autoharness-verification.log \ -o results.json - name: Upload JSON From 217e220abee820dc40302583b9656b5b65f0bb8a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 21:19:31 +0000 Subject: [PATCH 11/11] Have repository --- .github/workflows/kani.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index b7552a89c80b6..935addbae9c07 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -203,6 +203,11 @@ jobs: fail-fast: false steps: + - name: Checkout Repository + uses: actions/checkout@v4 + with: + submodules: false + - name: Download log uses: actions/download-artifact@v4 with: