-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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
- Loading branch information
1 parent
851f56c
commit 35d8710
Showing
1 changed file
with
41 additions
and
0 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |