From 35d871089e9bd4fc7070499c1fd1c4c5f818dc22 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Costa?= Date: Tue, 7 Jan 2025 11:56:13 +0100 Subject: [PATCH] Introduce script to measure the duration of the formal verification This commit introduces a python file that measure the required time for the formal verification. It also introduces the possibility to manually run it on the github workflow --- misc/formal_verification_time.py | 41 ++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 misc/formal_verification_time.py diff --git a/misc/formal_verification_time.py b/misc/formal_verification_time.py new file mode 100644 index 00000000..a491672d --- /dev/null +++ b/misc/formal_verification_time.py @@ -0,0 +1,41 @@ +import re +import subprocess +import time + +def extract_kani_names(file_path): + pattern = re.compile( + r"#\[cfg_attr\(kani, kani::proof\)\]\s*" + r"#\[cfg_attr\(test, test\)\]\s*" + r"pub fn (\w+)\s*\(" + ) + + with open(file_path, 'r') as file: + content = file.read() + + return pattern.findall(content) + +def time_cargo_run(subcommand): + command = ["cargo", "run", "--", "verify", subcommand] + + start_time = time.time() + + try: + with open('/dev/null', 'w') as devnull: + subprocess.run(command, check=True, stdout=devnull, stderr=devnull) + except subprocess.CalledProcessError as e: + print(f"Command failed with return code {e.returncode}") + + duration = time.time() - start_time + + print(f"{subcommand} verification completed in {duration:.2f} seconds.") + + return duration + +if __name__ == "__main__": + print("Please run the script from the miralis folder, otherwise it won't work.") + + file_path = "model_checking/src/lib.rs" + functions = extract_kani_names(file_path) + + for func in functions: + time_cargo_run(func)