diff --git a/analyze.sh b/analyze.sh index 8bc8022..69c6182 100755 --- a/analyze.sh +++ b/analyze.sh @@ -33,7 +33,7 @@ clean_warnings() { } { bod(); } END { $0=null; bod(); } - ' + ' } color_red='\033[0;31m' @@ -71,7 +71,7 @@ pretty_output() { readarray -t -O "${#descs[@]}" descs < <( < "$file" grep -Po '@(query|reachable)\s+"[^\"]*"' \ | sed 's/@\w\+\s\+//; s/"//g') - + local outp ctr res ta tz; ctr=0; res=0; ta="$(date +%s)" while read -r outp; do tz="$(date +%s)" @@ -99,7 +99,7 @@ metaverif() { local awk_prep; awk_prep="${tmpdir}/${name}.o.pv" { - exc awk -f marzipan/marzipan.awk "${cpp_prep}" + exc awk -f marzipan/marzipan.awk "${cpp_prep}" echo -e "\nprocess main" } > "${awk_prep}" @@ -125,14 +125,14 @@ metaverif() { main() { set -e -o pipefail - cd "$(dirname "$0")" + cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" tmpdir="target/proverif" mkdir -p "${tmpdir}" entries=() readarray -t -O "${#entries[@]}" entries < <( find analysis -iname '*.entry.mpv' | sort) - + local entry local procs; procs=() for entry in "${entries[@]}"; do @@ -144,4 +144,5 @@ main() { done } -main "$@" +# Do not execute main if sourced +(return 0 2>/dev/null) || main "$@" diff --git a/marzipan/poetry.lock b/marzipan/poetry.lock index 3b2cf2a..1a3ee7e 100644 --- a/marzipan/poetry.lock +++ b/marzipan/poetry.lock @@ -1,5 +1,20 @@ # This file is automatically @generated by Poetry 1.8.5 and should not be changed by hand. +[[package]] +name = "asttokens" +version = "3.0.0" +description = "Annotate AST trees with source code positions" +optional = false +python-versions = ">=3.8" +files = [ + {file = "asttokens-3.0.0-py3-none-any.whl", hash = "sha256:e3078351a059199dd5138cb1c706e6430c05eff2ff136af5eb4790f9d28932e2"}, + {file = "asttokens-3.0.0.tar.gz", hash = "sha256:0dcd8baa8d62b0c1d118b399b2ddba3c4aff271d0d7a9e0d4c1681c79035bbc7"}, +] + +[package.extras] +astroid = ["astroid (>=2,<4)"] +test = ["astroid (>=2,<4)", "pytest", "pytest-cov", "pytest-xdist"] + [[package]] name = "build" version = "1.2.2.post1" @@ -250,6 +265,20 @@ files = [ crashtest = ">=0.4.1,<0.5.0" rapidfuzz = ">=3.0.0,<4.0.0" +[[package]] +name = "click" +version = "8.1.8" +description = "Composable command line interface toolkit" +optional = false +python-versions = ">=3.7" +files = [ + {file = "click-8.1.8-py3-none-any.whl", hash = "sha256:63c132bbbed01578a06712a2d1f497bb62d9c1c0d329b7903a866228027263b2"}, + {file = "click-8.1.8.tar.gz", hash = "sha256:ed53c9d8990d83c2a27deae68e4ee337473f6330c040a31d4225c9574d16096a"}, +] + +[package.dependencies] +colorama = {version = "*", markers = "platform_system == \"Windows\""} + [[package]] name = "colorama" version = "0.4.6" @@ -321,6 +350,17 @@ ssh = ["bcrypt (>=3.1.5)"] test = ["certifi (>=2024)", "cryptography-vectors (==44.0.0)", "pretend (>=0.7)", "pytest (>=7.4.0)", "pytest-benchmark (>=4.0)", "pytest-cov (>=2.10.1)", "pytest-xdist (>=3.5.0)"] test-randomorder = ["pytest-randomly"] +[[package]] +name = "decorator" +version = "5.1.1" +description = "Decorators for Humans" +optional = false +python-versions = ">=3.5" +files = [ + {file = "decorator-5.1.1-py3-none-any.whl", hash = "sha256:b8c3f85900b9dc423225913c5aace94729fe1fa9763b38939a95226f02d37186"}, + {file = "decorator-5.1.1.tar.gz", hash = "sha256:637996211036b6385ef91435e4fae22989472f9d571faba8927ba8253acbc330"}, +] + [[package]] name = "distlib" version = "0.3.9" @@ -393,6 +433,20 @@ https = ["urllib3 (>=1.24.1)"] paramiko = ["paramiko"] pgp = ["gpg"] +[[package]] +name = "executing" +version = "2.2.0" +description = "Get the currently executing AST node of a frame, and other information" +optional = false +python-versions = ">=3.8" +files = [ + {file = "executing-2.2.0-py2.py3-none-any.whl", hash = "sha256:11387150cad388d62750327a53d3339fad4888b39a6fe233c3afbb54ecffd3aa"}, + {file = "executing-2.2.0.tar.gz", hash = "sha256:5d108c028108fe2551d1a7b2e8b713341e2cb4fc0aa7dcf966fa4327a5226755"}, +] + +[package.extras] +tests = ["asttokens (>=2.1.0)", "coverage", "coverage-enable-subprocess", "ipython", "littleutils", "pytest", "rich"] + [[package]] name = "fastjsonschema" version = "2.21.1" @@ -485,6 +539,42 @@ files = [ {file = "installer-0.7.0.tar.gz", hash = "sha256:a26d3e3116289bb08216e0d0f7d925fcef0b0194eedfa0c944bcaaa106c4b631"}, ] +[[package]] +name = "ipython" +version = "8.32.0" +description = "IPython: Productive Interactive Computing" +optional = false +python-versions = ">=3.10" +files = [ + {file = "ipython-8.32.0-py3-none-any.whl", hash = "sha256:cae85b0c61eff1fc48b0a8002de5958b6528fa9c8defb1894da63f42613708aa"}, + {file = "ipython-8.32.0.tar.gz", hash = "sha256:be2c91895b0b9ea7ba49d33b23e2040c352b33eb6a519cca7ce6e0c743444251"}, +] + +[package.dependencies] +colorama = {version = "*", markers = "sys_platform == \"win32\""} +decorator = "*" +jedi = ">=0.16" +matplotlib-inline = "*" +pexpect = {version = ">4.3", markers = "sys_platform != \"win32\" and sys_platform != \"emscripten\""} +prompt_toolkit = ">=3.0.41,<3.1.0" +pygments = ">=2.4.0" +stack_data = "*" +traitlets = ">=5.13.0" + +[package.extras] +all = ["ipython[black,doc,kernel,matplotlib,nbconvert,nbformat,notebook,parallel,qtconsole]", "ipython[test,test-extra]"] +black = ["black"] +doc = ["docrepr", "exceptiongroup", "intersphinx_registry", "ipykernel", "ipython[test]", "matplotlib", "setuptools (>=18.5)", "sphinx (>=1.3)", "sphinx-rtd-theme", "sphinxcontrib-jquery", "tomli", "typing_extensions"] +kernel = ["ipykernel"] +matplotlib = ["matplotlib"] +nbconvert = ["nbconvert"] +nbformat = ["nbformat"] +notebook = ["ipywidgets", "notebook"] +parallel = ["ipyparallel"] +qtconsole = ["qtconsole"] +test = ["packaging", "pickleshare", "pytest", "pytest-asyncio (<0.22)", "testpath"] +test-extra = ["curio", "ipython[test]", "matplotlib (!=3.2.0)", "nbformat", "numpy (>=1.23)", "pandas", "trio"] + [[package]] name = "jaraco-classes" version = "3.4.0" @@ -540,6 +630,25 @@ enabler = ["pytest-enabler (>=2.2)"] test = ["jaraco.classes", "pytest (>=6,!=8.1.*)"] type = ["pytest-mypy"] +[[package]] +name = "jedi" +version = "0.19.2" +description = "An autocompletion tool for Python that can be used for text editors." +optional = false +python-versions = ">=3.6" +files = [ + {file = "jedi-0.19.2-py2.py3-none-any.whl", hash = "sha256:a8ef22bde8490f57fe5c7681a3c83cb58874daf72b4784de3cce5b6ef6edb5b9"}, + {file = "jedi-0.19.2.tar.gz", hash = "sha256:4770dc3de41bde3966b02eb84fbcf557fb33cce26ad23da12c742fb50ecb11f0"}, +] + +[package.dependencies] +parso = ">=0.8.4,<0.9.0" + +[package.extras] +docs = ["Jinja2 (==2.11.3)", "MarkupSafe (==1.1.1)", "Pygments (==2.8.1)", "alabaster (==0.7.12)", "babel (==2.9.1)", "chardet (==4.0.0)", "commonmark (==0.8.1)", "docutils (==0.17.1)", "future (==0.18.2)", "idna (==2.10)", "imagesize (==1.2.0)", "mock (==1.0.1)", "packaging (==20.9)", "pyparsing (==2.4.7)", "pytz (==2021.1)", "readthedocs-sphinx-ext (==2.1.4)", "recommonmark (==0.5.0)", "requests (==2.25.1)", "six (==1.15.0)", "snowballstemmer (==2.1.0)", "sphinx (==1.8.5)", "sphinx-rtd-theme (==0.4.3)", "sphinxcontrib-serializinghtml (==1.1.4)", "sphinxcontrib-websupport (==1.2.4)", "urllib3 (==1.26.4)"] +qa = ["flake8 (==5.0.4)", "mypy (==0.971)", "types-setuptools (==67.2.0.1)"] +testing = ["Django", "attrs", "colorama", "docopt", "pytest (<9.0.0)"] + [[package]] name = "jeepney" version = "0.8.0" @@ -600,6 +709,55 @@ interegular = ["interegular (>=0.3.1,<0.4.0)"] nearley = ["js2py"] regex = ["regex"] +[[package]] +name = "markdown-it-py" +version = "3.0.0" +description = "Python port of markdown-it. Markdown parsing, done right!" +optional = false +python-versions = ">=3.8" +files = [ + {file = "markdown-it-py-3.0.0.tar.gz", hash = "sha256:e3f60a94fa066dc52ec76661e37c851cb232d92f9886b15cb560aaada2df8feb"}, + {file = "markdown_it_py-3.0.0-py3-none-any.whl", hash = "sha256:355216845c60bd96232cd8d8c40e8f9765cc86f46880e43a8fd22dc1a1a8cab1"}, +] + +[package.dependencies] +mdurl = ">=0.1,<1.0" + +[package.extras] +benchmarking = ["psutil", "pytest", "pytest-benchmark"] +code-style = ["pre-commit (>=3.0,<4.0)"] +compare = ["commonmark (>=0.9,<1.0)", "markdown (>=3.4,<4.0)", "mistletoe (>=1.0,<2.0)", "mistune (>=2.0,<3.0)", "panflute (>=2.3,<3.0)"] +linkify = ["linkify-it-py (>=1,<3)"] +plugins = ["mdit-py-plugins"] +profiling = ["gprof2dot"] +rtd = ["jupyter_sphinx", "mdit-py-plugins", "myst-parser", "pyyaml", "sphinx", "sphinx-copybutton", "sphinx-design", "sphinx_book_theme"] +testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"] + +[[package]] +name = "matplotlib-inline" +version = "0.1.7" +description = "Inline Matplotlib backend for Jupyter" +optional = false +python-versions = ">=3.8" +files = [ + {file = "matplotlib_inline-0.1.7-py3-none-any.whl", hash = "sha256:df192d39a4ff8f21b1895d72e6a13f5fcc5099f00fa84384e0ea28c2cc0653ca"}, + {file = "matplotlib_inline-0.1.7.tar.gz", hash = "sha256:8423b23ec666be3d16e16b60bdd8ac4e86e840ebd1dd11a30b9f117f2fa0ab90"}, +] + +[package.dependencies] +traitlets = "*" + +[[package]] +name = "mdurl" +version = "0.1.2" +description = "Markdown URL utilities" +optional = false +python-versions = ">=3.7" +files = [ + {file = "mdurl-0.1.2-py3-none-any.whl", hash = "sha256:84008a41e51615a49fc9966191ff91509e3c40b939176e643fd50a5c2196b8f8"}, + {file = "mdurl-0.1.2.tar.gz", hash = "sha256:bb413d29f5eea38f31dd4754dd7377d4465116fb207585f97bf925588687c1ba"}, +] + [[package]] name = "more-itertools" version = "10.5.0" @@ -695,6 +853,35 @@ files = [ {file = "packaging-24.2.tar.gz", hash = "sha256:c228a6dc5e932d346bc5739379109d49e8853dd8223571c7c5b55260edc0b97f"}, ] +[[package]] +name = "parso" +version = "0.8.4" +description = "A Python Parser" +optional = false +python-versions = ">=3.6" +files = [ + {file = "parso-0.8.4-py2.py3-none-any.whl", hash = "sha256:a418670a20291dacd2dddc80c377c5c3791378ee1e8d12bffc35420643d43f18"}, + {file = "parso-0.8.4.tar.gz", hash = "sha256:eb3a7b58240fb99099a345571deecc0f9540ea5f4dd2fe14c2a99d6b281ab92d"}, +] + +[package.extras] +qa = ["flake8 (==5.0.4)", "mypy (==0.971)", "types-setuptools (==67.2.0.1)"] +testing = ["docopt", "pytest"] + +[[package]] +name = "pexpect" +version = "4.9.0" +description = "Pexpect allows easy control of interactive console applications." +optional = false +python-versions = "*" +files = [ + {file = "pexpect-4.9.0-py2.py3-none-any.whl", hash = "sha256:7236d1e080e4936be2dc3e326cec0af72acf9212a7e1d060210e70a47e253523"}, + {file = "pexpect-4.9.0.tar.gz", hash = "sha256:ee7d41123f3c9911050ea2c2dac107568dc43b2d3b0c7557a33212c398ead30f"}, +] + +[package.dependencies] +ptyprocess = ">=0.5" + [[package]] name = "pkginfo" version = "1.12.0" @@ -768,6 +955,45 @@ files = [ {file = "poetry_core-2.0.0.tar.gz", hash = "sha256:3317a3cc3932011a61114236b2d49883f4fb1403d2f5e97771ac0d077cfa396f"}, ] +[[package]] +name = "prompt-toolkit" +version = "3.0.50" +description = "Library for building powerful interactive command lines in Python" +optional = false +python-versions = ">=3.8.0" +files = [ + {file = "prompt_toolkit-3.0.50-py3-none-any.whl", hash = "sha256:9b6427eb19e479d98acff65196a307c555eb567989e6d88ebbb1b509d9779198"}, + {file = "prompt_toolkit-3.0.50.tar.gz", hash = "sha256:544748f3860a2623ca5cd6d2795e7a14f3d0e1c3c9728359013f79877fc89bab"}, +] + +[package.dependencies] +wcwidth = "*" + +[[package]] +name = "ptyprocess" +version = "0.7.0" +description = "Run a subprocess in a pseudo terminal" +optional = false +python-versions = "*" +files = [ + {file = "ptyprocess-0.7.0-py2.py3-none-any.whl", hash = "sha256:4b41f3967fce3af57cc7e94b888626c18bf37a083e3651ca8feeb66d492fef35"}, + {file = "ptyprocess-0.7.0.tar.gz", hash = "sha256:5c5d0a3b48ceee0b48485e0c26037c0acd7d29765ca3fbb5cb3831d347423220"}, +] + +[[package]] +name = "pure-eval" +version = "0.2.3" +description = "Safely evaluate AST nodes without side effects" +optional = false +python-versions = "*" +files = [ + {file = "pure_eval-0.2.3-py3-none-any.whl", hash = "sha256:1db8e35b67b3d218d818ae653e27f06c3aa420901fa7b081ca98cbedc874e0d0"}, + {file = "pure_eval-0.2.3.tar.gz", hash = "sha256:5f4e983f40564c576c7c8635ae88db5956bb2229d7e9237d03b3c0b0190eaf42"}, +] + +[package.extras] +tests = ["pytest"] + [[package]] name = "pycparser" version = "2.22" @@ -779,6 +1005,20 @@ files = [ {file = "pycparser-2.22.tar.gz", hash = "sha256:491c8be9c040f5390f5bf44a5b07752bd07f56edf992381b05c701439eec10f6"}, ] +[[package]] +name = "pygments" +version = "2.19.1" +description = "Pygments is a syntax highlighting package written in Python." +optional = false +python-versions = ">=3.8" +files = [ + {file = "pygments-2.19.1-py3-none-any.whl", hash = "sha256:9ea1544ad55cecf4b8242fab6dd35a93bbce657034b0611ee383099054ab6d8c"}, + {file = "pygments-2.19.1.tar.gz", hash = "sha256:61c16d2a8576dc0649d9f39e089b5f02bcd27fba10d8fb4dcc28173f7a45151f"}, +] + +[package.extras] +windows-terminal = ["colorama (>=0.4.6)"] + [[package]] name = "pyproject-hooks" version = "1.2.0" @@ -936,6 +1176,24 @@ files = [ [package.dependencies] requests = ">=2.0.1,<3.0.0" +[[package]] +name = "rich" +version = "13.9.4" +description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal" +optional = false +python-versions = ">=3.8.0" +files = [ + {file = "rich-13.9.4-py3-none-any.whl", hash = "sha256:6049d5e6ec054bf2779ab3358186963bac2ea89175919d699e378b99738c2a90"}, + {file = "rich-13.9.4.tar.gz", hash = "sha256:439594978a49a09530cff7ebc4b5c7103ef57baf48d5ea3184f21d9a2befa098"}, +] + +[package.dependencies] +markdown-it-py = ">=2.2.0" +pygments = ">=2.13.0,<3.0.0" + +[package.extras] +jupyter = ["ipywidgets (>=7.5.1,<9)"] + [[package]] name = "secretstorage" version = "3.3.3" @@ -962,6 +1220,25 @@ files = [ {file = "shellingham-1.5.4.tar.gz", hash = "sha256:8dbca0739d487e5bd35ab3ca4b36e11c4078f3a234bfce294b0a0291363404de"}, ] +[[package]] +name = "stack-data" +version = "0.6.3" +description = "Extract data from python stack frames and tracebacks for informative displays" +optional = false +python-versions = "*" +files = [ + {file = "stack_data-0.6.3-py3-none-any.whl", hash = "sha256:d5558e0c25a4cb0853cddad3d77da9891a08cb85dd9f9f91b9f8cd66e511e695"}, + {file = "stack_data-0.6.3.tar.gz", hash = "sha256:836a778de4fec4dcd1dcd89ed8abff8a221f58308462e1c4aa2a3cf30148f0b9"}, +] + +[package.dependencies] +asttokens = ">=2.1.0" +executing = ">=1.2.0" +pure-eval = "*" + +[package.extras] +tests = ["cython", "littleutils", "pygments", "pytest", "typeguard"] + [[package]] name = "tomlkit" version = "0.13.2" @@ -973,6 +1250,21 @@ files = [ {file = "tomlkit-0.13.2.tar.gz", hash = "sha256:fff5fe59a87295b278abd31bec92c15d9bc4a06885ab12bcea52c71119392e79"}, ] +[[package]] +name = "traitlets" +version = "5.14.3" +description = "Traitlets Python configuration system" +optional = false +python-versions = ">=3.8" +files = [ + {file = "traitlets-5.14.3-py3-none-any.whl", hash = "sha256:b74e89e397b1ed28cc831db7aea759ba6640cb3de13090ca145426688ff1ac4f"}, + {file = "traitlets-5.14.3.tar.gz", hash = "sha256:9ed0579d3502c94b4b3732ac120375cda96f923114522847de4b3bb98b96b6b7"}, +] + +[package.extras] +docs = ["myst-parser", "pydata-sphinx-theme", "sphinx"] +test = ["argcomplete (>=3.0.3)", "mypy (>=1.7.0)", "pre-commit", "pytest (>=7.0,<8.2)", "pytest-mock", "pytest-mypy-testing"] + [[package]] name = "trove-classifiers" version = "2025.1.10.15" @@ -1021,6 +1313,17 @@ platformdirs = ">=3.9.1,<5" docs = ["furo (>=2023.7.26)", "proselint (>=0.13)", "sphinx (>=7.1.2,!=7.3)", "sphinx-argparse (>=0.4)", "sphinxcontrib-towncrier (>=0.2.1a0)", "towncrier (>=23.6)"] test = ["covdefaults (>=2.3)", "coverage (>=7.2.7)", "coverage-enable-subprocess (>=1)", "flaky (>=3.7)", "packaging (>=23.1)", "pytest (>=7.4)", "pytest-env (>=0.8.2)", "pytest-freezer (>=0.4.8)", "pytest-mock (>=3.11.1)", "pytest-randomly (>=3.12)", "pytest-timeout (>=2.1)", "setuptools (>=68)", "time-machine (>=2.10)"] +[[package]] +name = "wcwidth" +version = "0.2.13" +description = "Measures the displayed width of unicode strings in a terminal" +optional = false +python-versions = "*" +files = [ + {file = "wcwidth-0.2.13-py2.py3-none-any.whl", hash = "sha256:3da69048e4540d84af32131829ff948f1e022c1c6bdb8d6102117aac784f6859"}, + {file = "wcwidth-0.2.13.tar.gz", hash = "sha256:72ea0c06399eb286d978fdedb6923a9eb47e1c486ce63e9b4e64fc18303972b5"}, +] + [[package]] name = "xattr" version = "1.1.4" @@ -1109,4 +1412,4 @@ test = ["pytest"] [metadata] lock-version = "2.0" python-versions = ">=3.12,<3.13" -content-hash = "b7f8ea2821f5bb235a7f77cae3fa0e117a7a7f27183f5521f5f42dc034e2dd3a" +content-hash = "24150e63452e1200eeafe0bf650735c188d0964c7282fc5a57bed063fdfe99a6" diff --git a/marzipan/pyproject.toml b/marzipan/pyproject.toml index 2edd12d..686b82b 100644 --- a/marzipan/pyproject.toml +++ b/marzipan/pyproject.toml @@ -7,7 +7,8 @@ authors = ["Author Name "] # license = "BSD" packages = [ { include = "**/*.[hp]y", from = "src", to = "rosenpass_marzipan" }, - { include = "**/*.lark", from = "src", to = "rosenpass_marzipan" }, + { include = "**/*.sh", from = "src", to = "rosenpass_marzipan" }, + #{ include = "**/*.lark", from = "src", to = "rosenpass_marzipan" }, ] [tool.poetry.scripts] @@ -18,6 +19,9 @@ python = ">=3.12,<3.13" hy = "^1.0.0" lark = "^1.2.2" hyrule = "^0.8.0" +ipython = "^8.32.0" +click = "^8.1.8" +rich = "^13.9.4" [tool.poetry.group.dev.dependencies] poetry = "^2.0.0" diff --git a/marzipan/src/__init__.py b/marzipan/src/__init__.py index 5db74f3..20fe8c5 100644 --- a/marzipan/src/__init__.py +++ b/marzipan/src/__init__.py @@ -1,2 +1,64 @@ +from .util import pkgs, setup_exports, export, rename +from rich import print +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) + if command.stdout is not None: + return command.stdout.decode("utf-8") + return "" + +@click.command() +@click.argument("file") +@click.argument("log") +@click.argument("extra_args") +def run_proverif(file, log, extra_args): + return exc(["proverif", "-test", *extra_args, file], stderr=pkgs.sys.stderr) + + +def clean_warnings(): + pass + + +@click.command() +@click.argument("prefix") +@click.argument("mark") +@click.argument("color") +@click.argument("text") +def pretty_output_line(prefix, mark, color, text): + colored_prefix = f"[grey42]{prefix}[/grey42]" + colored_mark_text = f"[{color}]{mark} {text}[/{color}]" + print(colored_prefix, colored_mark_text) + +@click.command() +@click.argument("path") +def analyze(path): + exc([ + f"{pkgs.pathlib.Path(__file__).resolve().parent}/analyze.sh", + path + ]) + +@click.command() +def clean(): + click.echo("foo") + pass + + +@export +@rename("main") # Click seems to erase __name__ +@click.group() def main(): - print("Hello World") + #pkgs.IPython.embed() + pass + +main.add_command(analyze) +main.add_command(clean) +main.add_command(run_proverif) +main.add_command(pretty_output_line) diff --git a/marzipan/src/analyze.sh b/marzipan/src/analyze.sh new file mode 100755 index 0000000..3704b29 --- /dev/null +++ b/marzipan/src/analyze.sh @@ -0,0 +1,168 @@ +#!/usr/bin/env bash + +exc() { + echo >&2 "\$" "$@" + "$@" +} + +run_proverif() { + #local file; file="$1"; shift + #local log; log="$1"; shift + #exc proverif -test "${@}" "${file}" 2>&1 + + exc rosenpass-marzipan run_proverif "${file}" "${@}" +} + +clean_warnings() { + awk ' + BEGIN { + null = "0455290a-50d5-4f28-8008-3d69605c2835" + p = null; + } + + function pt(arg) { + if (arg != null) { + print(arg); + } + } + function bod() { + if ($0 !~ /^Warning: identifier \w+ rebound.$/) { + pt(p); + p=$0; + } else { + p=null; + } + } + { bod(); } + END { $0=null; bod(); } + ' +} + +color_red='\033[0;31m' +color_green='\033[0;32m' +color_gray='\033[0;30m' +color_clear='\033[0m' + +checkmark="✔" +cross="❌" + +pretty_output_line() { + local prefix; prefix="$1"; shift + local mark; mark="$1"; shift + local color; color="$1"; shift + local text; text="$1"; shift + echo -ne "\033[0\r${color_gray}${prefix}${color}${mark} ${text}${color_clear}" +} + +pretty_output() { + local file; file="$1"; shift + local expected=() descs=() + + # Lemmas are processed first + readarray -t -O "${#expected[@]}" expected < <( + < "$file" grep -Po '@(lemma)(?=\s+"[^\"]*")' \ + | sed 's/@lemma/true/') + readarray -t -O "${#descs[@]}" descs < <( + < "$file" grep -Po '@(lemma)\s+"[^\"]*"' \ + | sed 's/@\w\+\s\+//; s/"//g') + + # Then regular queries + readarray -t -O "${#expected[@]}" expected < <( + < "$file" grep -Po '@(query|reachable)(?=\s+"[^\"]*")' \ + | sed 's/@query/true/; s/@reachable/false/') + readarray -t -O "${#descs[@]}" descs < <( + < "$file" grep -Po '@(query|reachable)\s+"[^\"]*"' \ + | sed 's/@\w\+\s\+//; s/"//g') + + local outp ctr res ta tz; ctr=0; res=0; ta="$(date +%s)" + while read -r outp; do + tz="$(date +%s)" + if [[ "${outp}" = "${expected[$ctr]}" ]]; then + pretty_output_line "$((tz - ta))s " "${checkmark}" "${color_green}" "${descs[$ctr]}" + else + res=1 + pretty_output_line "$((tz - ta))s " "${cross}" "${color_red}" "${descs[$ctr]}" + fi + echo + + (( ctr += 1 )) + ta="${tz}" + done + + return "$res" +} + +metaverif() { + local file; file="$1"; shift + local name; name="$(echo "${file}" | grep -Po '[^/]*(?=\.mpv)')" + + local cpp_prep; cpp_prep="${tmpdir}/${name}.i.pv" + exc cpp -P -I"${PWD}/$(dirname "${file}")" "${file}" -o "${cpp_prep}" + + local awk_prep; awk_prep="${tmpdir}/${name}.o.pv" + { + exc awk -f marzipan/marzipan.awk "${cpp_prep}" + echo -e "\nprocess main" + } > "${awk_prep}" + + local log; log="${tmpdir}/${name}.log" + { + run_proverif "${awk_prep}" "$@" \ + | clean_warnings \ + | tee "${log}" \ + | awk ' + /^RESULT/ { + gsub(/\./, "", $NF); + print($NF); + fflush(stdout); + }' \ + | pretty_output "${cpp_prep}" + } || { + if ! grep -q "^Verification summary" "${log}"; then + echo -ne "\033[0\r" + cat "${log}" + fi + } +} + +analyze() { + mkdir -p "${tmpdir}" + + entries=() + readarray -t -O "${#entries[@]}" entries < <( + find analysis -iname '*.entry.mpv' | sort) + + local entry + local procs; procs=() + for entry in "${entries[@]}"; do + exc metaverif "${entry}" "$@" >&2 & procs+=("$!") + done + + for entry in "${procs[@]}"; do + exc wait -f "${entry}" + done +} + +err_usage() { + echo >&1 "USAGE: ${0} analyze PATH" + exit 1 +} + +main() { + set -e -o pipefail + + local cmd="$1"; shift || err_usage + local dir="$1"; shift || err_usage + + cd -- "${dir}" + tmpdir="target/proverif" + + case "${cmd}" in + analyze) analyze ;; + clean_warnings) clean_warnings ;; + *) err_usage + esac +} + +# Do not execute main if sourced +(return 0 2>/dev/null) || main "$@" diff --git a/marzipan/src/util.py b/marzipan/src/util.py index 010efb5..818f99e 100644 --- a/marzipan/src/util.py +++ b/marzipan/src/util.py @@ -32,6 +32,13 @@ def setup_exports() -> Tuple[List[str], Callable[[T], T]]: (__all__, export) = setup_exports() export(setup_exports) +@export +def rename(name: str) -> Callable[[T], T]: + def rename_impl(v: T) -> T: + v.__name__ = name + return v + return rename_impl + @export def attempt(fn): # TODO: Documentation tests