-
Notifications
You must be signed in to change notification settings - Fork 331
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
103 changed files
with
1,016 additions
and
9,719 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,287 @@ | ||
| #!python3 | ||
|
|
||
| import argparse | ||
| import os | ||
| import re | ||
| from functools import reduce | ||
| from itertools import chain | ||
| from pathlib import Path | ||
| from sys import stderr | ||
| from typing import Any, Dict, Optional | ||
| from typing import Tuple | ||
|
|
||
| METHOD_NAME_RE = r'(?P<name>[a-zA-Z_][a-zA-Z_0-9.]*)' | ||
| sinvoke_re = re.compile(rf'(\bsinvoke\s+{METHOD_NAME_RE})\s*\(') | ||
| invoke_re = re.compile(rf'(\binvoke\s+{METHOD_NAME_RE})\s*\(') | ||
| # Some funny stuff here in order to properly parse 'if(...foo().selector)' | ||
| selector_re = re.compile(rf'[^:]\b{METHOD_NAME_RE}(?=(\s*\([^)]*\)\.selector))') | ||
| # Find the start of the methods block. Ignore methods block that may be all on one | ||
| # line - this confuses the rest of the script and is not worth it. | ||
| methods_block_re = re.compile(r'methods\s*{\s*(?://.*)?$', re.MULTILINE) | ||
| method_line_re = re.compile(rf'\s*(?:/\*.*\*/)?\s*(?P<func>function)?\s*(?P<name_w_paren>{METHOD_NAME_RE}\s*\()') | ||
| rule_prefix_re = re.compile(rf'^{METHOD_NAME_RE}+\s*(\([^)]*\))?\s*{{?\s*$') | ||
| double_sig = re.compile(rf'sig:{METHOD_NAME_RE}.sig:') | ||
|
|
||
| def fixup_sinvoke(line: str) -> Tuple[str, int]: | ||
| matches = sinvoke_re.findall(line) | ||
| # stat[] += len(matches) | ||
| return (reduce(lambda l, m: l.replace(m[0], f'{m[1]}'), | ||
| matches, | ||
| line), | ||
| len(matches)) | ||
|
|
||
|
|
||
| def fixup_invoke(line: str) -> Tuple[str, int]: | ||
| matches = invoke_re.findall(line) | ||
| return (reduce(lambda l, m: l.replace(m[0], f'{m[1]}@withrevert'), | ||
| matches, | ||
| line), | ||
| len(matches)) | ||
|
|
||
|
|
||
| def fixup_selector_sig(line: str) -> Tuple[str, int]: | ||
| matches = selector_re.findall(line) | ||
| matches = list(filter(lambda m: m[0] not in ('if', 'require', 'assert'), matches)) | ||
| l, n = (reduce(lambda l, m: l.replace(m[0] + m[1], f'sig:{m[0] + m[1]}'), | ||
| matches, | ||
| line), | ||
| len(matches)) | ||
| # fix double sig | ||
| double_sig_matches = double_sig.findall(l) | ||
| for match in double_sig_matches: | ||
| l = l.replace(f'sig:{match}.sig:', f'sig:{match}.') | ||
| return l, n | ||
|
|
||
|
|
||
| def fixup_rule_prefix(line: str) -> Tuple[str, int]: | ||
| matches = rule_prefix_re.match(line) | ||
| if matches and matches['name'] != "methods": | ||
| return 'rule ' + line, 1 | ||
| return line, 0 | ||
|
|
||
|
|
||
| def fixup_static_assert(line: str) -> Tuple[str, int]: | ||
| if line.lstrip().startswith('static_assert '): | ||
| return (line.replace('static_assert', 'assert', 1), 1) | ||
| return (line, 0) | ||
|
|
||
|
|
||
| def fixup_static_require(line: str) -> Tuple[str, int]: | ||
| if line.lstrip().startswith('static_require '): | ||
| return (line.replace('static_require', 'require', 1), 1) | ||
| return (line, 0) | ||
|
|
||
|
|
||
| def find_invoke_whole(line: str) -> bool: | ||
| return 'invoke_whole(' in line | ||
|
|
||
|
|
||
| def methods_block_add_semicolon(line: str, next_line: Optional[str]) -> Tuple[str, int]: | ||
| l, *comment = line.split('//', 1) | ||
| l = l.rstrip() | ||
| do_nothing = (line, 0) | ||
| if not l.lstrip(): | ||
| # an empty line | ||
| return do_nothing | ||
|
|
||
| if any(l.endswith(s) for s in (';', '=>', '(', '{', '/*', '/**', '*/', ',')): | ||
| # this line doesn't need a semicolon | ||
| return do_nothing | ||
|
|
||
| if any(w in l.split() for w in ('if', 'else')): | ||
| # this is a branching line, skip it | ||
| return do_nothing | ||
|
|
||
| if next_line is not None and (next_line.lstrip().startswith("=>") or next_line.lstrip().startswith(')')): | ||
| # the method's summary is defined in the next line, don't append a ; | ||
| # also if we have a ) in the next line it means we broke lines for the parameters | ||
| return do_nothing | ||
|
|
||
| return l + ';' + (f' //{comment[0]}' if comment else ''), 1 | ||
|
|
||
|
|
||
| def methods_block_prepend_function(line: str) -> Tuple[str, int]: | ||
| m = method_line_re.match(line) | ||
| if m is not None and m['func'] is None: | ||
| return line.replace(m['name_w_paren'], f'function {m["name_w_paren"]}', 1), 1 | ||
| return line, 0 | ||
|
|
||
|
|
||
| def methods_block_add_external_visibility_no_summary(line: str) -> Tuple[str, int]: | ||
| m = method_line_re.match(line) | ||
| if m is not None and ('=>' not in line or '=> DISPATCHER' in line): | ||
| replacables = [' returns ', ' returns(', ' envfree', ' =>', ';'] | ||
| for r in replacables: | ||
| if r in line: | ||
| if all(f' {vis}{r2}' not in line for vis in ('internal', 'external') for r2 in replacables): | ||
| line = line.replace(r, f' external{r}') | ||
| return line, 1 | ||
| return line, 0 | ||
| else: | ||
| print(f"Unable to add 'external' modifier to {line}") | ||
| return line, 0 | ||
|
|
||
|
|
||
| def methods_block_summary_should_have_wildcard(line: str) -> Tuple[str, int]: | ||
| m = method_line_re.match(line) | ||
| if m is not None and '=>' in line and '.' not in line and ' internal ' not in line: | ||
| line = line.replace("function ", "function _.") | ||
| return line, 1 | ||
|
|
||
| return line, 0 | ||
|
|
||
|
|
||
| def append_semicolons_to_directives(line: str) -> Tuple[str, int]: | ||
| if line.lstrip().startswith(('pragma', 'import', 'using', 'use ')) and not line.rstrip().endswith((';', '{')): | ||
| line = line.rstrip() + ';' + os.linesep | ||
| return line, 1 | ||
| return line, 0 | ||
|
|
||
|
|
||
| def main() -> int: | ||
| parser = argparse.ArgumentParser() | ||
| parser.add_argument('-f', '--files', metavar='FILE', nargs='+', help='list of files to change', type=Path, | ||
| default=list()) | ||
| parser.add_argument('-d', '--dirs', metavar='DIR', nargs='+', help='the dir to search', type=Path, default=list()) | ||
| parser.add_argument('-r', '--recursive', action='store_true', help='if set dirs will be searched recursively') | ||
| args = parser.parse_args() | ||
|
|
||
| if not args.dirs and not args.files: | ||
| print('No files/dirs specified', file=stderr) | ||
| return 1 | ||
| if non_existent := list(filter(lambda f: not (f.exists() and f.is_file()), args.files)): | ||
| print(f'Cannot find files {non_existent}', file=stderr) | ||
| return 1 | ||
| if non_existent := list(filter(lambda d: not (d.exists() and d.is_dir()), args.dirs)): | ||
| print(f'Cannot find dirs {non_existent}', file=stderr) | ||
| return 1 | ||
|
|
||
| spec_files: chain = chain() | ||
| for d in args.dirs: | ||
| dir_files_unfiltered = (f for f in d.glob(f'{"**/" if args.recursive else ""}*') | ||
| if f.suffix in ('.cvl', '.spec')) | ||
| dir_files = filter( | ||
| lambda fname: not any(p.startswith('.certora_config') for p in fname.parts), | ||
| dir_files_unfiltered) | ||
| spec_files = chain(spec_files, dir_files) | ||
| spec_files = chain(spec_files, args.files) | ||
|
|
||
| sinvoke_str = 'sinvoke foo(...) -> foo(...)' | ||
| invoke_str = 'invoke foo(...) -> foo@withrevert(...)' | ||
| static_assert_str = 'static_assert -> assert' | ||
| static_require_str = 'static_require -> require' | ||
| invoke_whole_str = "lines with 'invoke_whole'" | ||
| sig_selector_str = "selectors prepended with 'sig:'" | ||
| rule_prefix_str = "rule declarations prepended with 'rule'" | ||
| semicolon_in_directives_str = "'pragma', 'import', 'using' or 'use' directives appended with ';'" | ||
| semicolon_in_methods_str = "lines in 'methods' block appended with ';'" | ||
| prepend_function_for_methods_str = "lines in 'methods' block prepended with 'function'" | ||
| add_external_visibility_for_non_summary_str = "declarations in 'methods' block with 'external' visibility added" | ||
| summary_should_have_wildcard_str = "declarations in 'methods' block with wildcard added" | ||
|
|
||
| stats: Dict[Any, Any] = {} | ||
| for fname in spec_files: | ||
| print(f"processing {fname}") | ||
| stats[fname] = {} | ||
| stats[fname][sinvoke_str] = 0 | ||
| stats[fname][invoke_str] = 0 | ||
| stats[fname][static_assert_str] = 0 | ||
| stats[fname][static_require_str] = 0 | ||
| stats[fname][sig_selector_str] = 0 | ||
| stats[fname][rule_prefix_str] = 0 | ||
| stats[fname][invoke_whole_str] = [] | ||
| stats[fname][semicolon_in_directives_str] = 0 | ||
| stats[fname][semicolon_in_methods_str] = 0 | ||
| stats[fname][prepend_function_for_methods_str] = 0 | ||
| stats[fname][add_external_visibility_for_non_summary_str] = 0 | ||
| stats[fname][summary_should_have_wildcard_str] = 0 | ||
|
|
||
| flines = open(fname).readlines() | ||
| for i, l in enumerate(flines): | ||
| l, num = fixup_sinvoke(l) | ||
| stats[fname][sinvoke_str] += num | ||
|
|
||
| l, num = fixup_invoke(l) | ||
| stats[fname][invoke_str] += num | ||
|
|
||
| l, num = fixup_static_assert(l) | ||
| stats[fname][static_assert_str] += num | ||
|
|
||
| l, num = fixup_static_require(l) | ||
| stats[fname][static_require_str] += num | ||
|
|
||
| l, num = append_semicolons_to_directives(l) | ||
| stats[fname][semicolon_in_directives_str] += num | ||
|
|
||
| l, num = fixup_selector_sig(l) | ||
| stats[fname][sig_selector_str] += num | ||
| flines[i] = l | ||
|
|
||
| l, num = fixup_rule_prefix(l) | ||
| stats[fname][rule_prefix_str] += num | ||
| flines[i] = l | ||
|
|
||
| with open(fname, 'w') as f: | ||
| f.writelines(flines) | ||
|
|
||
| # methods block | ||
| contents = open(fname).read() | ||
| methods_block_declaration = methods_block_re.search(contents) | ||
| if not methods_block_declaration: | ||
| print(f"{fname} has no methods block, skipping...") | ||
| continue | ||
| try: | ||
| prev, methods_block = methods_block_re.split(contents) | ||
| except ValueError: | ||
| print(f"{fname}: Failed to find methods block - more than one 'methods' block found") | ||
| continue | ||
|
|
||
| try: | ||
| methods_block, rest = re.split(r'^}', methods_block, maxsplit=1, flags=re.MULTILINE) | ||
| except ValueError: | ||
| print(f"{fname}: Failed to find methods block - couldn't find block end") | ||
| continue | ||
|
|
||
| if methods_block.count("{") != methods_block.count("}"): | ||
| print(f"{fname}: Failed to find methods block - something went wrong with finding the end of the block") | ||
| continue | ||
|
|
||
| # add semicolons in the methods block where it's easy to do so | ||
| methods_block = methods_block.split("\n") | ||
| for i, l in enumerate(methods_block): | ||
| next_line = methods_block[i + 1] if i + 1 < len(methods_block) else None | ||
| l, n = methods_block_add_semicolon(l, next_line) | ||
| stats[fname][semicolon_in_methods_str] += n | ||
| l, n = methods_block_prepend_function(l) | ||
| stats[fname][prepend_function_for_methods_str] += n | ||
| l, n = methods_block_add_external_visibility_no_summary(l) | ||
| stats[fname][add_external_visibility_for_non_summary_str] += n | ||
| l, n = methods_block_summary_should_have_wildcard(l) | ||
| stats[fname][summary_should_have_wildcard_str] += n | ||
| methods_block[i] = l | ||
| methods_block = "\n".join(methods_block) | ||
|
|
||
| with open(fname, 'w') as f: | ||
| f.write(prev + methods_block_declaration.group(0) + methods_block + '}' + rest) | ||
|
|
||
| print('Change Statistics\n-----------------') | ||
| for fname, stat in stats.items(): | ||
| if all(not n for n in stat.values()): | ||
| continue | ||
| print(f'{fname}:') | ||
| for s, n in stat.items(): | ||
| if not n: | ||
| continue | ||
| print(f'\t{s}: {n}') | ||
|
|
||
| print("The following files have instances of 'invoke_whole' which need to be removed manually") | ||
| for fname in stats: | ||
| inv_whole_list = stats[fname][invoke_whole_str] | ||
| if not inv_whole_list: | ||
| continue | ||
| print(f"\t{fname} (line{'s' if len(inv_whole_list) > 1 else ''} {', '.join(str(n) for n in inv_whole_list)})") | ||
| return 0 | ||
|
|
||
|
|
||
| if __name__ == "__main__": | ||
| exit(main()) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.