diff --git a/marzipan/TODO.md b/marzipan/TODO.md index 6623cf0..8a53e92 100644 --- a/marzipan/TODO.md +++ b/marzipan/TODO.md @@ -2,4 +2,13 @@ ## Next steps -* figure out why ProVerif is started on the non-processed mpv file +* ~~figure out why ProVerif is started on the non-processed mpv file~~ +* ~~rework rebound warnings (`clean_warnings` Bash function)~~ + ```bash + rosenpass$ rosenpass-marzipan run-proverif target/proverif/03_identity_hiding_responder.entry.o.pv target/proverif/03_identity_hiding_responder.entry.log + ``` + +* provide log parameter to `rosenpass-marzipan`-call +* cpp pre-processing stuff +* awk pre-processing stuff +* `pretty_output` Bash function diff --git a/marzipan/src/__init__.py b/marzipan/src/__init__.py index 6644bfa..ee0f700 100644 --- a/marzipan/src/__init__.py +++ b/marzipan/src/__init__.py @@ -5,9 +5,11 @@ import click (__all__, export) = setup_exports() export(setup_exports) + def eprint(*args, **kwargs): print(*args, **{"file": pkgs.sys.stderr, **kwargs}) + def exc(argv, **kwargs): eprint("$", *argv) command = pkgs.subprocess.run(argv, **kwargs) @@ -15,6 +17,7 @@ def exc(argv, **kwargs): return command.stdout.decode("utf-8") return "" + @click.command() @click.argument("file") @click.argument("log") @@ -28,10 +31,6 @@ def run_proverif(file, log, extra_args=[]): return exc(params, stderr=pkgs.sys.stderr) -def clean_warnings(): - pass - - @click.command() @click.argument("prefix") @click.argument("mark") @@ -42,6 +41,7 @@ def pretty_output_line(prefix, mark, color, text): colored_mark_text = f"[{color}]{mark} {text}[/{color}]" print(colored_prefix, colored_mark_text) + @click.command() @click.argument("path") def analyze(path): @@ -50,12 +50,30 @@ def analyze(path): path ]) + @click.command() def clean(): click.echo("foo") pass +@click.command() +def clean_warnings(): + null = "0455290a-50d5-4f28-8008-3d69605c2835" + p = null + for line in pkgs.sys.stdin: + line = line.rstrip() + if not pkgs.re.match(r"^Warning: identifier \w+ rebound.$", line): + if p != null: + print(p) + p = line + else: + p = null + # print last line after EOF + if p != null: + print(p) + + @export @rename("main") # Click seems to erase __name__ @click.group() @@ -63,7 +81,9 @@ def main(): #pkgs.IPython.embed() pass + main.add_command(analyze) main.add_command(clean) main.add_command(run_proverif) main.add_command(pretty_output_line) +main.add_command(clean_warnings) diff --git a/marzipan/src/analyze.sh b/marzipan/src/analyze.sh index cef01c7..5880b00 100755 --- a/marzipan/src/analyze.sh +++ b/marzipan/src/analyze.sh @@ -6,14 +6,16 @@ exc() { } run_proverif() { - #local file; file="$1"; shift - #local log; log="$1"; shift + local file; file="$1"; shift + local log; log="$1"; shift #exc proverif -test "${@}" "${file}" 2>&1 - exc rosenpass-marzipan run-proverif "${file}" "${@}" + exc rosenpass-marzipan run-proverif "${file}" "${log}" "${@}" } clean_warnings() { + exc rosenpass-marzipan clean-warnings +: <<'END_COMMENT' awk ' BEGIN { null = "0455290a-50d5-4f28-8008-3d69605c2835" @@ -36,6 +38,7 @@ clean_warnings() { { bod(); } END { $0=null; bod(); } ' +END_COMMENT } color_red='\033[0;31m' @@ -97,6 +100,9 @@ metaverif() { local name; name="$(echo "${file}" | grep -Po '[^/]*(?=\.mpv)')" local cpp_prep; cpp_prep="${tmpdir}/${name}.i.pv" + + echo "internal metaverif" + exc cpp -P -I"${PWD}/$(dirname "${file}")" "${file}" -o "${cpp_prep}" local awk_prep; awk_prep="${tmpdir}/${name}.o.pv" @@ -135,6 +141,7 @@ analyze() { local entry local procs; procs=() for entry in "${entries[@]}"; do + echo "call metaverif" exc metaverif "${entry}" "$@" >&2 & procs+=("$!") done @@ -158,6 +165,8 @@ main() { cd -- "${dir}" tmpdir="target/proverif" + echo "call main" + case "${cmd}" in analyze) analyze ;; clean_warnings) clean_warnings ;;