Skip to content

Commit 02d5859

Browse files
francois141CharlyCst
authored andcommitted
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
1 parent fd2d746 commit 02d5859

File tree

1 file changed

+41
-0
lines changed

1 file changed

+41
-0
lines changed

misc/formal_verification_time.py

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
import re
2+
import subprocess
3+
import time
4+
5+
def extract_kani_names(file_path):
6+
pattern = re.compile(
7+
r"#\[cfg_attr\(kani, kani::proof\)\]\s*"
8+
r"#\[cfg_attr\(test, test\)\]\s*"
9+
r"pub fn (\w+)\s*\("
10+
)
11+
12+
with open(file_path, 'r') as file:
13+
content = file.read()
14+
15+
return pattern.findall(content)
16+
17+
def time_cargo_run(subcommand):
18+
command = ["cargo", "run", "--", "verify", subcommand]
19+
20+
start_time = time.time()
21+
22+
try:
23+
with open('/dev/null', 'w') as devnull:
24+
subprocess.run(command, check=True, stdout=devnull, stderr=devnull)
25+
except subprocess.CalledProcessError as e:
26+
print(f"Command failed with return code {e.returncode}")
27+
28+
duration = time.time() - start_time
29+
30+
print(f"{subcommand} verification completed in {duration:.2f} seconds.")
31+
32+
return duration
33+
34+
if __name__ == "__main__":
35+
print("Please run the script from the miralis folder, otherwise it won't work.")
36+
37+
file_path = "model_checking/src/lib.rs"
38+
functions = extract_kani_names(file_path)
39+
40+
for func in functions:
41+
time_cargo_run(func)

0 commit comments

Comments
 (0)