gitea-mirror/rosenpass
1
0
Fork 0
mirror of https://github.com/rosenpass/rosenpass.git synced 2026-02-28 14:33:37 -08:00
Code Issues Packages Projects Releases Wiki Activity

feat: add parser for multi-line comments, without nesting

Browse Source 
Co-authored-by: Anja Rabich <a.rabich@uni-luebeck.de>
This commit is contained in:
Benjamin Lipp
2025-10-14 17:31:31 +02:00
parent a389e3c222
commit 3ce0d262d9
2 changed files with 64 additions and 36 deletions
Download Patch File Download Diff File Expand all files Collapse all files

81
marzipan/src/__init__.py
View File

@@ -1,5 +1,7 @@
from .util import pkgs, setup_exports, export, rename from .util import pkgs, setup_exports, export, rename
#from rich.console import Console from .parser import *
# from rich.console import Console
import click import click
target_subdir = "target/proverif" target_subdir = "target/proverif"
@@ -52,7 +54,13 @@ def run_proverif(file, extra_args=[]):
params = ["proverif", "-test", *extra_args, file] params = ["proverif", "-test", *extra_args, file]
logger.debug(params) logger.debug(params)
process = exc_piped(params, stderr=pkgs.subprocess.PIPE, stdout=pkgs.subprocess.PIPE, text=True, bufsize=1) process = exc_piped(
params,
stderr=pkgs.subprocess.PIPE,
stdout=pkgs.subprocess.PIPE,
text=True,
bufsize=1,
)
try: try:
prev_line = None prev_line = None
for line in process.stdout: for line in process.stdout:
@@ -72,7 +80,9 @@ def run_proverif(file, extra_args=[]):
return_code = process.wait() return_code = process.wait()
if return_code != 0: if return_code != 0:
logger.error(f"Proverif exited with a non-zero error code {params}: {return_code}") logger.error(
f"Proverif exited with a non-zero error code {params}: {return_code}"
)
exit(return_code) exit(return_code)
@@ -88,8 +98,13 @@ def cpp(file, cpp_prep):
def awk(repo_path, cpp_prep, awk_prep): def awk(repo_path, cpp_prep, awk_prep):
params = ["awk", "-f", str(pkgs.os.path.join(repo_path, "marzipan/marzipan.awk")), cpp_prep] params = [
with open(awk_prep, 'w') as file: "awk",
"-f",
str(pkgs.os.path.join(repo_path, "marzipan/marzipan.awk")),
cpp_prep,
]
with open(awk_prep, "w") as file:
exc(params, stderr=pkgs.sys.stderr, stdout=file) exc(params, stderr=pkgs.sys.stderr, stdout=file)
file.write("\nprocess main") file.write("\nprocess main")
@@ -104,11 +119,11 @@ def pretty_output_init(file_path):
expected = [] expected = []
descs = [] descs = []
with open(file_path, 'r') as file: with open(file_path, "r") as file:
content = file.read() content = file.read()
# Process lemmas first # Process lemmas first
result = pkgs.re.findall(r'@(lemma)(?=\s+\"([^\"]*)\")', content) result = pkgs.re.findall(r"@(lemma)(?=\s+\"([^\"]*)\")", content)
if result: if result:
# The regex only returns lemmas. For lemmas, we always expect the result 'true' from ProVerif. # The regex only returns lemmas. For lemmas, we always expect the result 'true' from ProVerif.
expected.extend([True for _ in range(len(result))]) expected.extend([True for _ in range(len(result))])
@@ -118,8 +133,10 @@ def pretty_output_init(file_path):
result = pkgs.re.findall(r'@(query|reachable)(?=\s+"[^\"]*")', content) result = pkgs.re.findall(r'@(query|reachable)(?=\s+"[^\"]*")', content)
if result: if result:
# For queries, we expect 'true' from ProVerif, for reachable, we expect 'false'. # For queries, we expect 'true' from ProVerif, for reachable, we expect 'false'.
expected.extend([e == '@query' for e in result]) expected.extend([e == "@query" for e in result])
reachable_result = pkgs.re.findall(r'@(query|reachable)\s+"([^\"]*)"', content) reachable_result = pkgs.re.findall(
r'@(query|reachable)\s+"([^\"]*)"', content
)
descs.extend([e[1] for e in reachable_result]) descs.extend([e[1] for e in reachable_result])
ta = pkgs.time.time() ta = pkgs.time.time()
@@ -133,9 +150,9 @@ def pretty_output_step(file_path, line, expected, descs, res, ctr, ta):
# Output from ProVerif contains a trailing newline, which we do not have in the expected output. Remove it for meaningful matching. # Output from ProVerif contains a trailing newline, which we do not have in the expected output. Remove it for meaningful matching.
outp_clean_raw = line.rstrip() outp_clean_raw = line.rstrip()
if outp_clean_raw == 'true': if outp_clean_raw == "true":
outp_clean = True outp_clean = True
elif outp_clean_raw == 'false': elif outp_clean_raw == "false":
outp_clean = False outp_clean = False
else: else:
outp_clean = outp_clean_raw outp_clean = outp_clean_raw
@@ -155,7 +172,9 @@ def pretty_output_step(file_path, line, expected, descs, res, ctr, ta):
def pretty_output(file_path): def pretty_output(file_path):
(ta, res, ctr, expected, descs) = pretty_output_init(file_path) (ta, res, ctr, expected, descs) = pretty_output_init(file_path)
for line in pkgs.sys.stdin: for line in pkgs.sys.stdin:
(res, ctr, ta) = pretty_output_step(file_path, line, expected, descs, res, ctr, ta) (res, ctr, ta) = pretty_output_step(
file_path, line, expected, descs, res, ctr, ta
)
def get_target_dir(path, output): def get_target_dir(path, output):
@@ -166,18 +185,21 @@ def get_target_dir(path, output):
@main.command() @main.command()
@click.option('--output', 'output', required=False) @click.option("--output", "output", required=False)
@click.argument("repo_path") @click.argument("repo_path")
def analyze(repo_path, output): def analyze(repo_path, output):
target_dir = get_target_dir(repo_path, output) target_dir = get_target_dir(repo_path, output)
pkgs.os.makedirs(target_dir, exist_ok=True) pkgs.os.makedirs(target_dir, exist_ok=True)
entries = [] entries = []
analysis_dir = pkgs.os.path.join(repo_path, 'analysis') analysis_dir = pkgs.os.path.join(repo_path, "analysis")
entries.extend(sorted(pkgs.glob.glob(str(analysis_dir) + '/*.entry.mpv'))) entries.extend(sorted(pkgs.glob.glob(str(analysis_dir) + "/*.entry.mpv")))
with pkgs.concurrent.futures.ProcessPoolExecutor() as executor: with pkgs.concurrent.futures.ProcessPoolExecutor() as executor:
futures = {executor.submit(metaverif, repo_path, target_dir, entry): entry for entry in entries} futures = {
executor.submit(metaverif, repo_path, target_dir, entry): entry
for entry in entries
}
for future in pkgs.concurrent.futures.as_completed(futures): for future in pkgs.concurrent.futures.as_completed(futures):
cmd = futures[future] cmd = futures[future]
logger.info(f"Metaverif {cmd} finished.") logger.info(f"Metaverif {cmd} finished.")
@@ -186,7 +208,7 @@ def analyze(repo_path, output):
@main.command() @main.command()
@click.option('--output', 'output', required=False) @click.option("--output", "output", required=False)
@click.argument("repo_path") @click.argument("repo_path")
def clean(repo_path, output): def clean(repo_path, output):
cleans_failed = 0 cleans_failed = 0
@@ -194,7 +216,9 @@ def clean(repo_path, output):
if pkgs.os.path.isdir(target_dir): if pkgs.os.path.isdir(target_dir):
for filename in pkgs.os.listdir(target_dir): for filename in pkgs.os.listdir(target_dir):
file_path = pkgs.os.path.join(target_dir, filename) file_path = pkgs.os.path.join(target_dir, filename)
if pkgs.os.path.isfile(file_path) and pkgs.os.path.splitext(file_path)[1] in [".pv", ".log"]: if pkgs.os.path.isfile(file_path) and pkgs.os.path.splitext(file_path)[
1
] in [".pv", ".log"]:
try: try:
pkgs.os.remove(file_path) pkgs.os.remove(file_path)
except Exception as e: except Exception as e:
@@ -206,11 +230,10 @@ def clean(repo_path, output):
exit(1) exit(1)
def metaverif(repo_path, tmpdir, file): def metaverif(repo_path, tmpdir, file):
print(f"Start metaverif on {file}") print(f"Start metaverif on {file}")
# Extract the name using regex # Extract the name using regex
name_match = pkgs.re.search(r'([^/]*)(?=\.mpv)', file) name_match = pkgs.re.search(r"([^/]*)(?=\.mpv)", file)
if name_match: if name_match:
name = name_match.group(0) # Get the matched name name = name_match.group(0) # Get the matched name
@@ -229,20 +252,30 @@ def metaverif(repo_path, tmpdir, file):
log_file = pkgs.os.path.join(tmpdir, f"{name}.log") log_file = pkgs.os.path.join(tmpdir, f"{name}.log")
ta, res, ctr, expected, descs = pretty_output_init(cpp_prep) ta, res, ctr, expected, descs = pretty_output_init(cpp_prep)
with open(log_file, 'a') as log: with open(log_file, "a") as log:
generator = run_proverif(awk_prep) generator = run_proverif(awk_prep)
for line in generator: for line in generator:
log.write(line) log.write(line)
# parse-result-line: # parse-result-line:
match = pkgs.re.search(r'^RESULT .* \b(true|false)\b\.$', line) match = pkgs.re.search(r"^RESULT .* \b(true|false)\b\.$", line)
if match: if match:
result = match.group(1) result = match.group(1)
# pretty-output: # pretty-output:
res, ctr, ta = pretty_output_step(cpp_prep, result, expected, descs, res, ctr, ta) res, ctr, ta = pretty_output_step(
cpp_prep, result, expected, descs, res, ctr, ta
)
else: else:
logger.error(f"No match found for the filename {file}: extension should be .mpv") logger.error(
f"No match found for the filename {file}: extension should be .mpv"
)
exit(1) exit(1)
@main.command()
@click.argument("file_path")
def parse(file_path):
parse_main(file_path)
if __name__ == "__main__": if __name__ == "__main__":
main() main()

19
marzipan/parser.py → marzipan/src/parser.py
View File

@@ -351,7 +351,7 @@ proverif_grammar = Lark(
phase: "phase" NAT [";" process] phase: "phase" NAT [";" process]
TAG: IDENT TAG: IDENT
sync: "sync" NAT ["[" TAG "]"] [";" process] sync: "sync" NAT ["[" TAG "]"] [";" process]
COMMENT: "(*" /.*/ COMMENT: /\(\*(\*(?!\))|[^*])*\*\)/
%import common (WORD, DIGIT, NUMBER, WS) // imports from terminal library %import common (WORD, DIGIT, NUMBER, WS) // imports from terminal library
%ignore WS // Disregard spaces in text %ignore WS // Disregard spaces in text
%ignore COMMENT %ignore COMMENT
@@ -360,6 +360,10 @@ proverif_grammar = Lark(
# lexer_callbacks={"COMMENT": comments.append}, # lexer_callbacks={"COMMENT": comments.append},
) )
# COMMENT: /\(\*(\*(?!\))|[^*])*\*\)/
# COMMENT: "(*" /(\*(?!\))|[^*])*/ "*)"
# comment: /\(\*(?:(?!\(\*|\*\)).|(?R))*\*\)/
# TODO Open ProVerif compatibility questions # TODO Open ProVerif compatibility questions
# TODO * does it allow leading zeros for NAT? # TODO * does it allow leading zeros for NAT?
# TODO * tag is not defined? is it ident? # TODO * tag is not defined? is it ident?
@@ -373,17 +377,8 @@ def parsertest(input):
return parsetree return parsetree
def main(): def parse_main(file_path):
if len(sys.argv) != 2: with open(file_path, "r") as f:
print(f"Usage: {sys.argv[0]} <filename>")
sys.exit(1)
filename = sys.argv[1]
with open(filename, "r") as f:
content = f.read() content = f.read()
# print(content) # print(content)
parsertest(content) parsertest(content)
if __name__ == "__main__":
main()