From 5f5968f93141558caceba08159f8ff17e4c987cd Mon Sep 17 00:00:00 2001 From: FedericoAureliano Date: Sat, 10 Feb 2024 14:08:40 -0800 Subject: [PATCH] initial commit with Adwait's code. About to start merging with procedural API --- .coveragerc | 28 + .github/workflows/ci.yml | 125 +++ .gitignore | 192 ++--- .isort.cfg | 3 + .pre-commit-config.yaml | 67 ++ .readthedocs.yml | 27 + AUTHORS.rst | 6 + CHANGELOG.rst | 10 + CONTRIBUTING.rst | 327 ++++++++ README.md | 2 - README.rst | 25 + docs/Makefile | 29 + docs/_static/.gitignore | 1 + docs/authors.rst | 2 + docs/changelog.rst | 2 + docs/conf.py | 286 +++++++ docs/contributing.rst | 1 + docs/index.rst | 61 ++ docs/license.rst | 7 + docs/readme.rst | 2 + docs/requirements.txt | 5 + pyproject.toml | 9 + setup.cfg | 117 +++ setup.py | 22 + src/uclid/__init__.py | 16 + src/uclid/ast.py | 1559 ++++++++++++++++++++++++++++++++++++++ tests/conftest.py | 10 + tests/test_ast.py | 9 + tox.ini | 93 +++ 29 files changed, 2892 insertions(+), 151 deletions(-) create mode 100644 .coveragerc create mode 100644 .github/workflows/ci.yml create mode 100644 .isort.cfg create mode 100644 .pre-commit-config.yaml create mode 100644 .readthedocs.yml create mode 100644 AUTHORS.rst create mode 100644 CHANGELOG.rst create mode 100644 CONTRIBUTING.rst delete mode 100644 README.md create mode 100644 README.rst create mode 100644 docs/Makefile create mode 100644 docs/_static/.gitignore create mode 100644 docs/authors.rst create mode 100644 docs/changelog.rst create mode 100644 docs/conf.py create mode 100644 docs/contributing.rst create mode 100644 docs/index.rst create mode 100644 docs/license.rst create mode 100644 docs/readme.rst create mode 100644 docs/requirements.txt create mode 100644 pyproject.toml create mode 100644 setup.cfg create mode 100644 setup.py create mode 100644 src/uclid/__init__.py create mode 100644 src/uclid/ast.py create mode 100644 tests/conftest.py create mode 100644 tests/test_ast.py create mode 100644 tox.ini diff --git a/.coveragerc b/.coveragerc new file mode 100644 index 0000000..5cc8753 --- /dev/null +++ b/.coveragerc @@ -0,0 +1,28 @@ +# .coveragerc to control coverage.py +[run] +branch = True +source = uclid +# omit = bad_file.py + +[paths] +source = + src/ + */site-packages/ + +[report] +# Regexes for lines to exclude from consideration +exclude_lines = + # Have to re-enable the standard pragma + pragma: no cover + + # Don't complain about missing debug-only code: + def __repr__ + if self\.debug + + # Don't complain if tests don't hit defensive assertion code: + raise AssertionError + raise NotImplementedError + + # Don't complain if non-runnable code isn't run: + if 0: + if __name__ == .__main__.: diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..d5c6825 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,125 @@ +# GitHub Actions configuration **EXAMPLE**, +# MODIFY IT ACCORDING TO YOUR NEEDS! +# Reference: https://docs.github.com/en/actions + +name: tests + +on: + push: + # Avoid using all the resources/limits available by checking only + # relevant branches and tags. Other branches can be checked via PRs. + branches: [main] + tags: ['v[0-9]*', '[0-9]+.[0-9]+*'] # Match tags that resemble a version + pull_request: # Run in every PR + workflow_dispatch: # Allow manually triggering the workflow + schedule: + # Run roughly every 15 days at 00:00 UTC + # (useful to check if updates on dependencies break the package) + - cron: '0 0 1,16 * *' + +permissions: + contents: read + +concurrency: + group: >- + ${{ github.workflow }}-${{ github.ref_type }}- + ${{ github.event.pull_request.number || github.sha }} + cancel-in-progress: true + +jobs: + prepare: + runs-on: ubuntu-latest + outputs: + wheel-distribution: ${{ steps.wheel-distribution.outputs.path }} + steps: + - uses: actions/checkout@v3 + with: {fetch-depth: 0} # deep clone for setuptools-scm + - uses: actions/setup-python@v4 + id: setup-python + with: {python-version: "3.11"} + - name: Run static analysis and format checkers + run: pipx run pre-commit run --all-files --show-diff-on-failure + - name: Build package distribution files + run: >- + pipx run --python '${{ steps.setup-python.outputs.python-path }}' + tox -e clean,build + - name: Record the path of wheel distribution + id: wheel-distribution + run: echo "path=$(ls dist/*.whl)" >> $GITHUB_OUTPUT + - name: Store the distribution files for use in other stages + # `tests` and `publish` will use the same pre-built distributions, + # so we make sure to release the exact same package that was tested + uses: actions/upload-artifact@v3 + with: + name: python-distribution-files + path: dist/ + retention-days: 1 + + test: + needs: prepare + strategy: + matrix: + python: + - "3.7" # oldest Python supported by PSF + - "3.11" # newest Python that is stable + platform: + - ubuntu-latest + - macos-latest + - windows-latest + runs-on: ${{ matrix.platform }} + steps: + - uses: actions/checkout@v3 + - uses: actions/setup-python@v4 + id: setup-python + with: + python-version: ${{ matrix.python }} + - name: Retrieve pre-built distribution files + uses: actions/download-artifact@v3 + with: {name: python-distribution-files, path: dist/} + - name: Run tests + run: >- + pipx run --python '${{ steps.setup-python.outputs.python-path }}' + tox --installpkg '${{ needs.prepare.outputs.wheel-distribution }}' + -- -rFEx --durations 10 --color yes # pytest args + - name: Generate coverage report + run: pipx run coverage lcov -o coverage.lcov + - name: Upload partial coverage report + uses: coverallsapp/github-action@master + with: + path-to-lcov: coverage.lcov + github-token: ${{ secrets.GITHUB_TOKEN }} + flag-name: ${{ matrix.platform }} - py${{ matrix.python }} + parallel: true + + finalize: + needs: test + runs-on: ubuntu-latest + steps: + - name: Finalize coverage report + uses: coverallsapp/github-action@master + with: + github-token: ${{ secrets.GITHUB_TOKEN }} + parallel-finished: true + + publish: + needs: finalize + if: ${{ github.event_name == 'push' && contains(github.ref, 'refs/tags/') }} + runs-on: ubuntu-latest + permissions: + contents: write + steps: + - uses: actions/checkout@v3 + - uses: actions/setup-python@v4 + with: {python-version: "3.11"} + - name: Retrieve pre-built distribution files + uses: actions/download-artifact@v3 + with: {name: python-distribution-files, path: dist/} + - name: Publish Package + env: + # TODO: Set your PYPI_TOKEN as a secret using GitHub UI + # - https://pypi.org/help/#apitoken + # - https://docs.github.com/en/actions/security-guides/encrypted-secrets + TWINE_REPOSITORY: pypi + TWINE_USERNAME: __token__ + TWINE_PASSWORD: ${{ secrets.PYPI_TOKEN }} + run: pipx run tox -e publish diff --git a/.gitignore b/.gitignore index 68bc17f..e9e1e9b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,160 +1,54 @@ -# Byte-compiled / optimized / DLL files -__pycache__/ +# Temporary and binary files +*~ *.py[cod] -*$py.class - -# C extensions *.so +*.cfg +!.isort.cfg +!setup.cfg +*.orig +*.log +*.pot +__pycache__/* +.cache/* +.*.swp +*/.ipynb_checkpoints/* +.DS_Store -# Distribution / packaging -.Python -build/ -develop-eggs/ -dist/ -downloads/ -eggs/ -.eggs/ -lib/ -lib64/ -parts/ -sdist/ -var/ -wheels/ -share/python-wheels/ -*.egg-info/ -.installed.cfg +# Project files +.ropeproject +.project +.pydevproject +.settings +.idea +.vscode +tags + +# Package files *.egg -MANIFEST - -# PyInstaller -# Usually these files are written by a python script from a template -# before PyInstaller builds the exe, so as to inject date/other infos into it. -*.manifest -*.spec - -# Installer logs -pip-log.txt -pip-delete-this-directory.txt +*.eggs/ +.installed.cfg +*.egg-info -# Unit test / coverage reports -htmlcov/ -.tox/ -.nox/ +# Unittest and coverage +htmlcov/* .coverage .coverage.* -.cache -nosetests.xml +.tox +junit*.xml coverage.xml -*.cover -*.py,cover -.hypothesis/ .pytest_cache/ -cover/ - -# Translations -*.mo -*.pot - -# Django stuff: -*.log -local_settings.py -db.sqlite3 -db.sqlite3-journal - -# Flask stuff: -instance/ -.webassets-cache - -# Scrapy stuff: -.scrapy - -# Sphinx documentation -docs/_build/ - -# PyBuilder -.pybuilder/ -target/ - -# Jupyter Notebook -.ipynb_checkpoints -# IPython -profile_default/ -ipython_config.py - -# pyenv -# For a library or package, you might want to ignore these files since the code is -# intended to run in multiple environments; otherwise, check them in: -# .python-version - -# pipenv -# According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control. -# However, in case of collaboration, if having platform-specific dependencies or dependencies -# having no cross-platform support, pipenv may install dependencies that don't work, or not -# install all needed dependencies. -#Pipfile.lock - -# poetry -# Similar to Pipfile.lock, it is generally recommended to include poetry.lock in version control. -# This is especially recommended for binary packages to ensure reproducibility, and is more -# commonly ignored for libraries. -# https://python-poetry.org/docs/basic-usage/#commit-your-poetrylock-file-to-version-control -#poetry.lock - -# pdm -# Similar to Pipfile.lock, it is generally recommended to include pdm.lock in version control. -#pdm.lock -# pdm stores project-wide configurations in .pdm.toml, but it is recommended to not include it -# in version control. -# https://pdm.fming.dev/#use-with-ide -.pdm.toml - -# PEP 582; used by e.g. github.com/David-OConnor/pyflow and github.com/pdm-project/pdm -__pypackages__/ - -# Celery stuff -celerybeat-schedule -celerybeat.pid - -# SageMath parsed files -*.sage.py - -# Environments -.env -.venv -env/ -venv/ -ENV/ -env.bak/ -venv.bak/ - -# Spyder project settings -.spyderproject -.spyproject - -# Rope project settings -.ropeproject - -# mkdocs documentation -/site - -# mypy -.mypy_cache/ -.dmypy.json -dmypy.json - -# Pyre type checker -.pyre/ - -# pytype static type analyzer -.pytype/ - -# Cython debug symbols -cython_debug/ +# Build and docs folder/files +build/* +dist/* +sdist/* +docs/api/* +docs/_rst/* +docs/_build/* +cover/* +MANIFEST -# PyCharm -# JetBrains specific template is maintained in a separate JetBrains.gitignore that can -# be found at https://github.com/github/gitignore/blob/main/Global/JetBrains.gitignore -# and can be added to the global gitignore or merged into this file. For a more nuclear -# option (not recommended) you can uncomment the following to ignore the entire idea folder. -#.idea/ +# Per-project virtualenvs +.venv*/ +.conda*/ +.python-version diff --git a/.isort.cfg b/.isort.cfg new file mode 100644 index 0000000..6ebff36 --- /dev/null +++ b/.isort.cfg @@ -0,0 +1,3 @@ +[settings] +profile = black +known_first_party = uclid diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml new file mode 100644 index 0000000..0305f4a --- /dev/null +++ b/.pre-commit-config.yaml @@ -0,0 +1,67 @@ +exclude: '^docs/conf.py' + +repos: +- repo: https://github.com/pre-commit/pre-commit-hooks + rev: v4.5.0 + hooks: + - id: trailing-whitespace + - id: check-added-large-files + - id: check-ast + - id: check-json + - id: check-merge-conflict + - id: check-xml + - id: check-yaml + - id: debug-statements + - id: end-of-file-fixer + - id: requirements-txt-fixer + - id: mixed-line-ending + args: ['--fix=auto'] # replace 'auto' with 'lf' to enforce Linux/Mac line endings or 'crlf' for Windows + +## If you want to automatically "modernize" your Python code: +# - repo: https://github.com/asottile/pyupgrade +# rev: v3.7.0 +# hooks: +# - id: pyupgrade +# args: ['--py37-plus'] + +## If you want to avoid flake8 errors due to unused vars or imports: +# - repo: https://github.com/PyCQA/autoflake +# rev: v2.1.1 +# hooks: +# - id: autoflake +# args: [ +# --in-place, +# --remove-all-unused-imports, +# --remove-unused-variables, +# ] + +- repo: https://github.com/PyCQA/isort + rev: 5.13.2 + hooks: + - id: isort + +- repo: https://github.com/psf/black + rev: 24.1.1 + hooks: + - id: black + language_version: python3 + +## If like to embrace black styles even in the docs: +# - repo: https://github.com/asottile/blacken-docs +# rev: v1.13.0 +# hooks: +# - id: blacken-docs +# additional_dependencies: [black] + +- repo: https://github.com/PyCQA/flake8 + rev: 7.0.0 + hooks: + - id: flake8 + ## You can add flake8 plugins via `additional_dependencies`: + # additional_dependencies: [flake8-bugbear] + +## Check for misspells in documentation files: +# - repo: https://github.com/codespell-project/codespell +# rev: v2.2.5 +# hooks: +# - id: codespell diff --git a/.readthedocs.yml b/.readthedocs.yml new file mode 100644 index 0000000..a2bcab3 --- /dev/null +++ b/.readthedocs.yml @@ -0,0 +1,27 @@ +# Read the Docs configuration file +# See https://docs.readthedocs.io/en/stable/config-file/v2.html for details + +# Required +version: 2 + +# Build documentation in the docs/ directory with Sphinx +sphinx: + configuration: docs/conf.py + +# Build documentation with MkDocs +#mkdocs: +# configuration: mkdocs.yml + +# Optionally build your docs in additional formats such as PDF +formats: + - pdf + +build: + os: ubuntu-22.04 + tools: + python: "3.11" + +python: + install: + - requirements: docs/requirements.txt + - {path: ., method: pip} diff --git a/AUTHORS.rst b/AUTHORS.rst new file mode 100644 index 0000000..391d689 --- /dev/null +++ b/AUTHORS.rst @@ -0,0 +1,6 @@ +============ +Contributors +============ + +* Federico Mora +* Adwait Godbole diff --git a/CHANGELOG.rst b/CHANGELOG.rst new file mode 100644 index 0000000..226e6f5 --- /dev/null +++ b/CHANGELOG.rst @@ -0,0 +1,10 @@ +========= +Changelog +========= + +Version 0.1 +=========== + +- Feature A added +- FIX: nasty bug #1729 fixed +- add your changes here! diff --git a/CONTRIBUTING.rst b/CONTRIBUTING.rst new file mode 100644 index 0000000..1878a46 --- /dev/null +++ b/CONTRIBUTING.rst @@ -0,0 +1,327 @@ +============ +Contributing +============ + +Welcome to ``uclid`` contributor's guide. + +This document focuses on getting any potential contributor familiarized +with the development processes, but `other kinds of contributions`_ are also +appreciated. + +If you are new to using git_ or have never collaborated in a project previously, +please have a look at `contribution-guide.org`_. Other resources are also +listed in the excellent `guide created by FreeCodeCamp`_ [#contrib1]_. + +Please notice, all users and contributors are expected to be **open, +considerate, reasonable, and respectful**. When in doubt, `Python Software +Foundation's Code of Conduct`_ is a good reference in terms of behavior +guidelines. + + +Issue Reports +============= + +If you experience bugs or general issues with ``uclid``, please have a look +on the `issue tracker`_. If you don't see anything useful there, please feel +free to fire an issue report. + +.. tip:: + Please don't forget to include the closed issues in your search. + Sometimes a solution was already reported, and the problem is considered + **solved**. + +New issue reports should include information about your programming environment +(e.g., operating system, Python version) and steps to reproduce the problem. +Please try also to simplify the reproduction steps to a very minimal example +that still illustrates the problem you are facing. By removing other factors, +you help us to identify the root cause of the issue. + + +Documentation Improvements +========================== + +You can help improve ``uclid`` docs by making them more readable and coherent, or +by adding missing information and correcting mistakes. + +``uclid`` documentation uses Sphinx_ as its main documentation compiler. +This means that the docs are kept in the same repository as the project code, and +that any documentation update is done in the same way was a code contribution. + +.. todo:: Don't forget to mention which markup language you are using. + + e.g., reStructuredText_ or CommonMark_ with MyST_ extensions. + +.. todo:: If your project is hosted on GitHub, you can also mention the following tip: + + .. tip:: + Please notice that the `GitHub web interface`_ provides a quick way of + propose changes in ``uclid``'s files. While this mechanism can + be tricky for normal code contributions, it works perfectly fine for + contributing to the docs, and can be quite handy. + + If you are interested in trying this method out, please navigate to + the ``docs`` folder in the source repository_, find which file you + would like to propose changes and click in the little pencil icon at the + top, to open `GitHub's code editor`_. Once you finish editing the file, + please write a message in the form at the bottom of the page describing + which changes have you made and what are the motivations behind them and + submit your proposal. + +When working on documentation changes in your local machine, you can +compile them using |tox|_:: + + tox -e docs + +and use Python's built-in web server for a preview in your web browser +(``http://localhost:8000``):: + + python3 -m http.server --directory 'docs/_build/html' + + +Code Contributions +================== + +.. todo:: Please include a reference or explanation about the internals of the project. + + An architecture description, design principles or at least a summary of the + main concepts will make it easy for potential contributors to get started + quickly. + +Submit an issue +--------------- + +Before you work on any non-trivial code contribution it's best to first create +a report in the `issue tracker`_ to start a discussion on the subject. +This often provides additional considerations and avoids unnecessary work. + +Create an environment +--------------------- + +Before you start coding, we recommend creating an isolated `virtual +environment`_ to avoid any problems with your installed Python packages. +This can easily be done via either |virtualenv|_:: + + virtualenv + source /bin/activate + +or Miniconda_:: + + conda create -n uclid python=3 six virtualenv pytest pytest-cov + conda activate uclid + +Clone the repository +-------------------- + +#. Create an user account on |the repository service| if you do not already have one. +#. Fork the project repository_: click on the *Fork* button near the top of the + page. This creates a copy of the code under your account on |the repository service|. +#. Clone this copy to your local disk:: + + git clone git@github.com:YourLogin/uclid.git + cd uclid + +#. You should run:: + + pip install -U pip setuptools -e . + + to be able to import the package under development in the Python REPL. + + .. todo:: if you are not using pre-commit, please remove the following item: + +#. Install |pre-commit|_:: + + pip install pre-commit + pre-commit install + + ``uclid`` comes with a lot of hooks configured to automatically help the + developer to check the code being written. + +Implement your changes +---------------------- + +#. Create a branch to hold your changes:: + + git checkout -b my-feature + + and start making changes. Never work on the main branch! + +#. Start your work on this branch. Don't forget to add docstrings_ to new + functions, modules and classes, especially if they are part of public APIs. + +#. Add yourself to the list of contributors in ``AUTHORS.rst``. + +#. When you're done editing, do:: + + git add + git commit + + to record your changes in git_. + + .. todo:: if you are not using pre-commit, please remove the following item: + + Please make sure to see the validation messages from |pre-commit|_ and fix + any eventual issues. + This should automatically use flake8_/black_ to check/fix the code style + in a way that is compatible with the project. + + .. important:: Don't forget to add unit tests and documentation in case your + contribution adds an additional feature and is not just a bugfix. + + Moreover, writing a `descriptive commit message`_ is highly recommended. + In case of doubt, you can check the commit history with:: + + git log --graph --decorate --pretty=oneline --abbrev-commit --all + + to look for recurring communication patterns. + +#. Please check that your changes don't break any unit tests with:: + + tox + + (after having installed |tox|_ with ``pip install tox`` or ``pipx``). + + You can also use |tox|_ to run several other pre-configured tasks in the + repository. Try ``tox -av`` to see a list of the available checks. + +Submit your contribution +------------------------ + +#. If everything works fine, push your local branch to |the repository service| with:: + + git push -u origin my-feature + +#. Go to the web page of your fork and click |contribute button| + to send your changes for review. + + .. todo:: if you are using GitHub, you can uncomment the following paragraph + + Find more detailed information in `creating a PR`_. You might also want to open + the PR as a draft first and mark it as ready for review after the feedbacks + from the continuous integration (CI) system or any required fixes. + + +Troubleshooting +--------------- + +The following tips can be used when facing problems to build or test the +package: + +#. Make sure to fetch all the tags from the upstream repository_. + The command ``git describe --abbrev=0 --tags`` should return the version you + are expecting. If you are trying to run CI scripts in a fork repository, + make sure to push all the tags. + You can also try to remove all the egg files or the complete egg folder, i.e., + ``.eggs``, as well as the ``*.egg-info`` folders in the ``src`` folder or + potentially in the root of your project. + +#. Sometimes |tox|_ misses out when new dependencies are added, especially to + ``setup.cfg`` and ``docs/requirements.txt``. If you find any problems with + missing dependencies when running a command with |tox|_, try to recreate the + ``tox`` environment using the ``-r`` flag. For example, instead of:: + + tox -e docs + + Try running:: + + tox -r -e docs + +#. Make sure to have a reliable |tox|_ installation that uses the correct + Python version (e.g., 3.7+). When in doubt you can run:: + + tox --version + # OR + which tox + + If you have trouble and are seeing weird errors upon running |tox|_, you can + also try to create a dedicated `virtual environment`_ with a |tox|_ binary + freshly installed. For example:: + + virtualenv .venv + source .venv/bin/activate + .venv/bin/pip install tox + .venv/bin/tox -e all + +#. `Pytest can drop you`_ in an interactive session in the case an error occurs. + In order to do that you need to pass a ``--pdb`` option (for example by + running ``tox -- -k --pdb``). + You can also setup breakpoints manually instead of using the ``--pdb`` option. + + +Maintainer tasks +================ + +Releases +-------- + +.. todo:: This section assumes you are using PyPI to publicly release your package. + + If instead you are using a different/private package index, please update + the instructions accordingly. + +If you are part of the group of maintainers and have correct user permissions +on PyPI_, the following steps can be used to release a new version for +``uclid``: + +#. Make sure all unit tests are successful. +#. Tag the current commit on the main branch with a release tag, e.g., ``v1.2.3``. +#. Push the new tag to the upstream repository_, e.g., ``git push upstream v1.2.3`` +#. Clean up the ``dist`` and ``build`` folders with ``tox -e clean`` + (or ``rm -rf dist build``) + to avoid confusion with old builds and Sphinx docs. +#. Run ``tox -e build`` and check that the files in ``dist`` have + the correct version (no ``.dirty`` or git_ hash) according to the git_ tag. + Also check the sizes of the distributions, if they are too big (e.g., > + 500KB), unwanted clutter may have been accidentally included. +#. Run ``tox -e publish -- --repository pypi`` and check that everything was + uploaded to PyPI_ correctly. + + + +.. [#contrib1] Even though, these resources focus on open source projects and + communities, the general ideas behind collaborating with other developers + to collectively create software are general and can be applied to all sorts + of environments, including private companies and proprietary code bases. + + +.. <-- start --> +.. todo:: Please review and change the following definitions: + +.. |the repository service| replace:: GitHub +.. |contribute button| replace:: "Create pull request" + +.. _repository: https://github.com//uclid +.. _issue tracker: https://github.com//uclid/issues +.. <-- end --> + + +.. |virtualenv| replace:: ``virtualenv`` +.. |pre-commit| replace:: ``pre-commit`` +.. |tox| replace:: ``tox`` + + +.. _black: https://pypi.org/project/black/ +.. _CommonMark: https://commonmark.org/ +.. _contribution-guide.org: https://www.contribution-guide.org/ +.. _creating a PR: https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/creating-a-pull-request +.. _descriptive commit message: https://chris.beams.io/posts/git-commit +.. _docstrings: https://www.sphinx-doc.org/en/master/usage/extensions/napoleon.html +.. _first-contributions tutorial: https://github.com/firstcontributions/first-contributions +.. _flake8: https://flake8.pycqa.org/en/stable/ +.. _git: https://git-scm.com +.. _GitHub's fork and pull request workflow: https://guides.github.com/activities/forking/ +.. _guide created by FreeCodeCamp: https://github.com/FreeCodeCamp/how-to-contribute-to-open-source +.. _Miniconda: https://docs.conda.io/en/latest/miniconda.html +.. _MyST: https://myst-parser.readthedocs.io/en/latest/syntax/syntax.html +.. _other kinds of contributions: https://opensource.guide/how-to-contribute +.. _pre-commit: https://pre-commit.com/ +.. _PyPI: https://pypi.org/ +.. _Pytest can drop you: https://docs.pytest.org/en/stable/how-to/failures.html#using-python-library-pdb-with-pytest +.. _Python Software Foundation's Code of Conduct: https://www.python.org/psf/conduct/ +.. _reStructuredText: https://www.sphinx-doc.org/en/master/usage/restructuredtext/ +.. _Sphinx: https://www.sphinx-doc.org/en/master/ +.. _tox: https://tox.wiki/en/stable/ +.. _virtual environment: https://realpython.com/python-virtual-environments-a-primer/ +.. _virtualenv: https://virtualenv.pypa.io/en/stable/ + +.. _GitHub web interface: https://docs.github.com/en/repositories/working-with-files/managing-files/editing-files +.. _GitHub's code editor: https://docs.github.com/en/repositories/working-with-files/managing-files/editing-files diff --git a/README.md b/README.md deleted file mode 100644 index f255377..0000000 --- a/README.md +++ /dev/null @@ -1,2 +0,0 @@ -# uclid-api -Python API for UCLID5 diff --git a/README.rst b/README.rst new file mode 100644 index 0000000..a2b51f8 --- /dev/null +++ b/README.rst @@ -0,0 +1,25 @@ +===== +UCLID5 Python API +===== + + + UCLID5 Python API + + +The official repository for the UCLID5 Python API. + + + +Making Changes & Contributing +============================= + +This project uses `pre-commit`_, please make sure to install it before making any +changes:: + + pip install pre-commit + cd uclid-api + pre-commit install + +It is a good idea to update the hooks to the latest version:: + + pre-commit autoupdate diff --git a/docs/Makefile b/docs/Makefile new file mode 100644 index 0000000..31655dd --- /dev/null +++ b/docs/Makefile @@ -0,0 +1,29 @@ +# Makefile for Sphinx documentation +# + +# You can set these variables from the command line, and also +# from the environment for the first two. +SPHINXOPTS ?= +SPHINXBUILD ?= sphinx-build +SOURCEDIR = . +BUILDDIR = _build +AUTODOCDIR = api + +# User-friendly check for sphinx-build +ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $?), 1) +$(error "The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from https://sphinx-doc.org/") +endif + +.PHONY: help clean Makefile + +# Put it first so that "make" without argument is like "make help". +help: + @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) + +clean: + rm -rf $(BUILDDIR)/* $(AUTODOCDIR) + +# Catch-all target: route all unknown targets to Sphinx using the new +# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). +%: Makefile + @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) diff --git a/docs/_static/.gitignore b/docs/_static/.gitignore new file mode 100644 index 0000000..3c96363 --- /dev/null +++ b/docs/_static/.gitignore @@ -0,0 +1 @@ +# Empty directory diff --git a/docs/authors.rst b/docs/authors.rst new file mode 100644 index 0000000..cd8e091 --- /dev/null +++ b/docs/authors.rst @@ -0,0 +1,2 @@ +.. _authors: +.. include:: ../AUTHORS.rst diff --git a/docs/changelog.rst b/docs/changelog.rst new file mode 100644 index 0000000..871950d --- /dev/null +++ b/docs/changelog.rst @@ -0,0 +1,2 @@ +.. _changes: +.. include:: ../CHANGELOG.rst diff --git a/docs/conf.py b/docs/conf.py new file mode 100644 index 0000000..ee73b3d --- /dev/null +++ b/docs/conf.py @@ -0,0 +1,286 @@ +# This file is execfile()d with the current directory set to its containing dir. +# +# This file only contains a selection of the most common options. For a full +# list see the documentation: +# https://www.sphinx-doc.org/en/master/usage/configuration.html +# +# All configuration values have a default; values that are commented out +# serve to show the default. + +import os +import sys +import shutil + +# -- Path setup -------------------------------------------------------------- + +__location__ = os.path.dirname(__file__) + +# If extensions (or modules to document with autodoc) are in another directory, +# add these directories to sys.path here. If the directory is relative to the +# documentation root, use os.path.abspath to make it absolute, like shown here. +sys.path.insert(0, os.path.join(__location__, "../src")) + +# -- Run sphinx-apidoc ------------------------------------------------------- +# This hack is necessary since RTD does not issue `sphinx-apidoc` before running +# `sphinx-build -b html . _build/html`. See Issue: +# https://github.com/readthedocs/readthedocs.org/issues/1139 +# DON'T FORGET: Check the box "Install your project inside a virtualenv using +# setup.py install" in the RTD Advanced Settings. +# Additionally it helps us to avoid running apidoc manually + +try: # for Sphinx >= 1.7 + from sphinx.ext import apidoc +except ImportError: + from sphinx import apidoc + +output_dir = os.path.join(__location__, "api") +module_dir = os.path.join(__location__, "../src/uclid") +try: + shutil.rmtree(output_dir) +except FileNotFoundError: + pass + +try: + import sphinx + + cmd_line = f"sphinx-apidoc --implicit-namespaces -f -o {output_dir} {module_dir}" + + args = cmd_line.split(" ") + if tuple(sphinx.__version__.split(".")) >= ("1", "7"): + # This is a rudimentary parse_version to avoid external dependencies + args = args[1:] + + apidoc.main(args) +except Exception as e: + print("Running `sphinx-apidoc` failed!\n{}".format(e)) + +# -- General configuration --------------------------------------------------- + +# If your documentation needs a minimal Sphinx version, state it here. +# needs_sphinx = '1.0' + +# Add any Sphinx extension module names here, as strings. They can be extensions +# coming with Sphinx (named 'sphinx.ext.*') or your custom ones. +extensions = [ + "sphinx.ext.autodoc", + "sphinx.ext.intersphinx", + "sphinx.ext.todo", + "sphinx.ext.autosummary", + "sphinx.ext.viewcode", + "sphinx.ext.coverage", + "sphinx.ext.doctest", + "sphinx.ext.ifconfig", + "sphinx.ext.mathjax", + "sphinx.ext.napoleon", +] + +# Add any paths that contain templates here, relative to this directory. +templates_path = ["_templates"] + +# The suffix of source filenames. +source_suffix = ".rst" + +# The encoding of source files. +# source_encoding = 'utf-8-sig' + +# The master toctree document. +master_doc = "index" + +# General information about the project. +project = "uclid" +copyright = "2024, Federico Mora" + +# The version info for the project you're documenting, acts as replacement for +# |version| and |release|, also used in various other places throughout the +# built documents. +# +# version: The short X.Y version. +# release: The full version, including alpha/beta/rc tags. +# If you don’t need the separation provided between version and release, +# just set them both to the same value. +try: + from uclid import __version__ as version +except ImportError: + version = "" + +if not version or version.lower() == "unknown": + version = os.getenv("READTHEDOCS_VERSION", "unknown") # automatically set by RTD + +release = version + +# The language for content autogenerated by Sphinx. Refer to documentation +# for a list of supported languages. +# language = None + +# There are two options for replacing |today|: either, you set today to some +# non-false value, then it is used: +# today = '' +# Else, today_fmt is used as the format for a strftime call. +# today_fmt = '%B %d, %Y' + +# List of patterns, relative to source directory, that match files and +# directories to ignore when looking for source files. +exclude_patterns = ["_build", "Thumbs.db", ".DS_Store", ".venv"] + +# The reST default role (used for this markup: `text`) to use for all documents. +# default_role = None + +# If true, '()' will be appended to :func: etc. cross-reference text. +# add_function_parentheses = True + +# If true, the current module name will be prepended to all description +# unit titles (such as .. function::). +# add_module_names = True + +# If true, sectionauthor and moduleauthor directives will be shown in the +# output. They are ignored by default. +# show_authors = False + +# The name of the Pygments (syntax highlighting) style to use. +pygments_style = "sphinx" + +# A list of ignored prefixes for module index sorting. +# modindex_common_prefix = [] + +# If true, keep warnings as "system message" paragraphs in the built documents. +# keep_warnings = False + +# If this is True, todo emits a warning for each TODO entries. The default is False. +todo_emit_warnings = True + + +# -- Options for HTML output ------------------------------------------------- + +# The theme to use for HTML and HTML Help pages. See the documentation for +# a list of builtin themes. +html_theme = "alabaster" + +# Theme options are theme-specific and customize the look and feel of a theme +# further. For a list of options available for each theme, see the +# documentation. +html_theme_options = { + "sidebar_width": "300px", + "page_width": "1200px" +} + +# Add any paths that contain custom themes here, relative to this directory. +# html_theme_path = [] + +# The name for this set of Sphinx documents. If None, it defaults to +# " v documentation". +# html_title = None + +# A shorter title for the navigation bar. Default is the same as html_title. +# html_short_title = None + +# The name of an image file (relative to this directory) to place at the top +# of the sidebar. +# html_logo = "" + +# The name of an image file (within the static path) to use as favicon of the +# docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32 +# pixels large. +# html_favicon = None + +# Add any paths that contain custom static files (such as style sheets) here, +# relative to this directory. They are copied after the builtin static files, +# so a file named "default.css" will overwrite the builtin "default.css". +html_static_path = ["_static"] + +# If not '', a 'Last updated on:' timestamp is inserted at every page bottom, +# using the given strftime format. +# html_last_updated_fmt = '%b %d, %Y' + +# If true, SmartyPants will be used to convert quotes and dashes to +# typographically correct entities. +# html_use_smartypants = True + +# Custom sidebar templates, maps document names to template names. +# html_sidebars = {} + +# Additional templates that should be rendered to pages, maps page names to +# template names. +# html_additional_pages = {} + +# If false, no module index is generated. +# html_domain_indices = True + +# If false, no index is generated. +# html_use_index = True + +# If true, the index is split into individual pages for each letter. +# html_split_index = False + +# If true, links to the reST sources are added to the pages. +# html_show_sourcelink = True + +# If true, "Created using Sphinx" is shown in the HTML footer. Default is True. +# html_show_sphinx = True + +# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True. +# html_show_copyright = True + +# If true, an OpenSearch description file will be output, and all pages will +# contain a tag referring to it. The value of this option must be the +# base URL from which the finished HTML is served. +# html_use_opensearch = '' + +# This is the file name suffix for HTML files (e.g. ".xhtml"). +# html_file_suffix = None + +# Output file base name for HTML help builder. +htmlhelp_basename = "uclid-doc" + + +# -- Options for LaTeX output ------------------------------------------------ + +latex_elements = { + # The paper size ("letterpaper" or "a4paper"). + # "papersize": "letterpaper", + # The font size ("10pt", "11pt" or "12pt"). + # "pointsize": "10pt", + # Additional stuff for the LaTeX preamble. + # "preamble": "", +} + +# Grouping the document tree into LaTeX files. List of tuples +# (source start file, target name, title, author, documentclass [howto/manual]). +latex_documents = [ + ("index", "user_guide.tex", "uclid Documentation", "Federico Mora", "manual") +] + +# The name of an image file (relative to this directory) to place at the top of +# the title page. +# latex_logo = "" + +# For "manual" documents, if this is true, then toplevel headings are parts, +# not chapters. +# latex_use_parts = False + +# If true, show page references after internal links. +# latex_show_pagerefs = False + +# If true, show URL addresses after external links. +# latex_show_urls = False + +# Documents to append as an appendix to all manuals. +# latex_appendices = [] + +# If false, no module index is generated. +# latex_domain_indices = True + +# -- External mapping -------------------------------------------------------- +python_version = ".".join(map(str, sys.version_info[0:2])) +intersphinx_mapping = { + "sphinx": ("https://www.sphinx-doc.org/en/master", None), + "python": ("https://docs.python.org/" + python_version, None), + "matplotlib": ("https://matplotlib.org", None), + "numpy": ("https://numpy.org/doc/stable", None), + "sklearn": ("https://scikit-learn.org/stable", None), + "pandas": ("https://pandas.pydata.org/pandas-docs/stable", None), + "scipy": ("https://docs.scipy.org/doc/scipy/reference", None), + "setuptools": ("https://setuptools.pypa.io/en/stable/", None), + "pyscaffold": ("https://pyscaffold.org/en/stable", None), +} + +print(f"loading configurations for {project} {version} ...", file=sys.stderr) diff --git a/docs/contributing.rst b/docs/contributing.rst new file mode 100644 index 0000000..e582053 --- /dev/null +++ b/docs/contributing.rst @@ -0,0 +1 @@ +.. include:: ../CONTRIBUTING.rst diff --git a/docs/index.rst b/docs/index.rst new file mode 100644 index 0000000..d13bd2e --- /dev/null +++ b/docs/index.rst @@ -0,0 +1,61 @@ +===== +uclid +===== + +This is the documentation of **uclid**. + +.. note:: + + This is the main page of your project's `Sphinx`_ documentation. + It is formatted in `reStructuredText`_. Add additional pages + by creating rst-files in ``docs`` and adding them to the `toctree`_ below. + Use then `references`_ in order to link them from this page, e.g. + :ref:`authors` and :ref:`changes`. + + It is also possible to refer to the documentation of other Python packages + with the `Python domain syntax`_. By default you can reference the + documentation of `Sphinx`_, `Python`_, `NumPy`_, `SciPy`_, `matplotlib`_, + `Pandas`_, `Scikit-Learn`_. You can add more by extending the + ``intersphinx_mapping`` in your Sphinx's ``conf.py``. + + The pretty useful extension `autodoc`_ is activated by default and lets + you include documentation from docstrings. Docstrings can be written in + `Google style`_ (recommended!), `NumPy style`_ and `classical style`_. + + +Contents +======== + +.. toctree:: + :maxdepth: 2 + + Overview + Contributions & Help + License + Authors + Changelog + Module Reference + + +Indices and tables +================== + +* :ref:`genindex` +* :ref:`modindex` +* :ref:`search` + +.. _toctree: https://www.sphinx-doc.org/en/master/usage/restructuredtext/directives.html +.. _reStructuredText: https://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html +.. _references: https://www.sphinx-doc.org/en/stable/markup/inline.html +.. _Python domain syntax: https://www.sphinx-doc.org/en/master/usage/restructuredtext/domains.html#the-python-domain +.. _Sphinx: https://www.sphinx-doc.org/ +.. _Python: https://docs.python.org/ +.. _Numpy: https://numpy.org/doc/stable +.. _SciPy: https://docs.scipy.org/doc/scipy/reference/ +.. _matplotlib: https://matplotlib.org/contents.html# +.. _Pandas: https://pandas.pydata.org/pandas-docs/stable +.. _Scikit-Learn: https://scikit-learn.org/stable +.. _autodoc: https://www.sphinx-doc.org/en/master/ext/autodoc.html +.. _Google style: https://google.github.io/styleguide/pyguide.html#38-comments-and-docstrings +.. _NumPy style: https://numpydoc.readthedocs.io/en/latest/format.html +.. _classical style: https://www.sphinx-doc.org/en/master/domains.html#info-field-lists diff --git a/docs/license.rst b/docs/license.rst new file mode 100644 index 0000000..3989c51 --- /dev/null +++ b/docs/license.rst @@ -0,0 +1,7 @@ +.. _license: + +======= +License +======= + +.. include:: ../LICENSE.txt diff --git a/docs/readme.rst b/docs/readme.rst new file mode 100644 index 0000000..81995ef --- /dev/null +++ b/docs/readme.rst @@ -0,0 +1,2 @@ +.. _readme: +.. include:: ../README.rst diff --git a/docs/requirements.txt b/docs/requirements.txt new file mode 100644 index 0000000..2ddf98a --- /dev/null +++ b/docs/requirements.txt @@ -0,0 +1,5 @@ +# Requirements file for ReadTheDocs, check .readthedocs.yml. +# To build the module reference correctly, make sure every external package +# under `install_requires` in `setup.cfg` is also listed here! +sphinx>=3.2.1 +# sphinx_rtd_theme diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..89a5bed --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,9 @@ +[build-system] +# AVOID CHANGING REQUIRES: IT WILL BE UPDATED BY PYSCAFFOLD! +requires = ["setuptools>=46.1.0", "setuptools_scm[toml]>=5"] +build-backend = "setuptools.build_meta" + +[tool.setuptools_scm] +# For smarter version schemes and other configuration options, +# check out https://github.com/pypa/setuptools_scm +version_scheme = "no-guess-dev" diff --git a/setup.cfg b/setup.cfg new file mode 100644 index 0000000..ab2b489 --- /dev/null +++ b/setup.cfg @@ -0,0 +1,117 @@ +# This file is used to configure your project. +# Read more about the various options under: +# https://setuptools.pypa.io/en/latest/userguide/declarative_config.html +# https://setuptools.pypa.io/en/latest/references/keywords.html + +[metadata] +name = uclid +description = UCLID5 Python API +author = Federico Mora +author_email = fmora@berkeley.edu +license = MIT +license_files = LICENSE.txt +long_description = file: README.rst +long_description_content_type = text/x-rst; charset=UTF-8 +url = https://github.com/uclid-org/uclid-api +# Add here related links, for example: +project_urls = + Source = https://github.com/uclid-org/uclid-api + +# Change if running only on Windows, Mac or Linux (comma-separated) +platforms = any + +# Add here all kinds of additional classifiers as defined under +# https://pypi.org/classifiers/ +classifiers = + Development Status :: 4 - Beta + Programming Language :: Python + + +[options] +zip_safe = False +packages = find_namespace: +include_package_data = True +package_dir = + =src + +# Require a min/specific Python version (comma-separated conditions) +# python_requires = >=3.8 + +# Add here dependencies of your project (line-separated), e.g. requests>=2.2,<3.0. +# Version specifiers like >=2.2,<3.0 avoid problems due to API changes in +# new major versions. This works if the required packages follow Semantic Versioning. +# For more information, check out https://semver.org/. +install_requires = + importlib-metadata; python_version<"3.8" + + +[options.packages.find] +where = src +exclude = + tests + +[options.extras_require] +# Add here additional requirements for extra features, to install with: +# `pip install uclid[PDF]` like: +# PDF = ReportLab; RXP + +# Add here test requirements (semicolon/line-separated) +testing = + setuptools + pytest + pytest-cov + +[options.entry_points] +# Add here console scripts like: +# console_scripts = +# script_name = uclid.module:function +# For example: +# console_scripts = +# fibonacci = uclid.skeleton:run + +[tool:pytest] +# Specify command line options as you would do when invoking pytest directly. +# e.g. --cov-report html (or xml) for html/xml output or --junitxml junit.xml +# in order to write a coverage file that can be read by Jenkins. +# CAUTION: --cov flags may prohibit setting breakpoints while debugging. +# Comment those flags to avoid this pytest issue. +addopts = + --cov uclid --cov-report term-missing + --verbose +norecursedirs = + dist + build + .tox +testpaths = tests +# Use pytest markers to select/deselect specific tests +# markers = +# slow: mark tests as slow (deselect with '-m "not slow"') +# system: mark end-to-end system tests + +[devpi:upload] +# Options for the devpi: PyPI server and packaging tool +# VCS export must be deactivated since we are using setuptools-scm +no_vcs = 1 +formats = bdist_wheel + +[flake8] +# Some sane defaults for the code style checker flake8 +max_line_length = 90 +extend_ignore = E203, W503 +# ^ Black-compatible +# E203 and W503 have edge cases handled by black +exclude = + .tox + build + dist + .eggs + docs/conf.py + +[pyscaffold] +# PyScaffold's parameters when the project was created. +# This will be used when updating. Do not change! +version = 4.5 +package = uclid +extensions = + github_actions + pre_commit diff --git a/setup.py b/setup.py new file mode 100644 index 0000000..a0ab001 --- /dev/null +++ b/setup.py @@ -0,0 +1,22 @@ +""" + Setup file for uclid. + Use setup.cfg to configure your project. + + This file was generated with PyScaffold 4.5. + PyScaffold helps you to put up the scaffold of your new Python project. + Learn more under: https://pyscaffold.org/ +""" + +from setuptools import setup + +if __name__ == "__main__": + try: + setup(use_scm_version={"version_scheme": "no-guess-dev"}) + except: # noqa + print( + "\n\nAn error occurred while building the project, " + "please ensure you have the most updated version of setuptools, " + "setuptools_scm and wheel with:\n" + " pip install -U setuptools setuptools_scm wheel\n\n" + ) + raise diff --git a/src/uclid/__init__.py b/src/uclid/__init__.py new file mode 100644 index 0000000..e451f10 --- /dev/null +++ b/src/uclid/__init__.py @@ -0,0 +1,16 @@ +import sys + +if sys.version_info[:2] >= (3, 8): + # TODO: Import directly (no need for conditional) when `python_requires = >= 3.8` + from importlib.metadata import PackageNotFoundError, version # pragma: no cover +else: + from importlib_metadata import PackageNotFoundError, version # pragma: no cover + +try: + # Change here if project is renamed and does not equal the package name + dist_name = __name__ + __version__ = version(dist_name) +except PackageNotFoundError: # pragma: no cover + __version__ = "unknown" +finally: + del version, PackageNotFoundError diff --git a/src/uclid/ast.py b/src/uclid/ast.py new file mode 100644 index 0000000..405fb9f --- /dev/null +++ b/src/uclid/ast.py @@ -0,0 +1,1559 @@ +import logging +import textwrap +from enum import Enum + +__author__ = "Adwait Godbole" +__copyright__ = "Adwait Godbole" +__license__ = "MIT" + +_logger = logging.getLogger(__name__) + + +class UclidContext: + # dict: + # modulename : str -> declname : str -> UclidDecl + var_decls = {} + # dict: + # modulename : str -> declname : str -> UclidDecl + const_decls = {} + # dict: + # modulename : str -> declname : str -> UclidDecl + typ_decls = {} + # dict: + # modulename : str -> declname : str -> UclidDecl + instance_decls = {} + # dict: + # modulename : str -> [UclidDecl]list + ip_var_decls = {} + # dict: + # modulename : str -> [UclidDecl]list + op_var_decls = {} + # dict: + # modulename : str -> [UclidImport]list + import_decls = {} + # dict: + # modulename : str -> [UclidDefine]list + define_decls = {} + # dict: + # modulename : str -> [UclidProcedure]list + procedure_defns = {} + # dict: + # modulename : str -> [UclidAssume]list + module_assumes = {} + # dict: + # modulename : str -> UclidModule + modules = {} + # name of module in current context + module_name = "main" + + @staticmethod + def clearAll(): + """ + Deletes all context information (restart). + """ + UclidContext.var_decls = {} + UclidContext.const_decls = {} + UclidContext.typ_decls = {} + UclidContext.instance_decls = {} + UclidContext.ip_var_decls = {} + UclidContext.op_var_decls = {} + UclidContext.import_decls = {} + UclidContext.define_decls = {} + UclidContext.procedure_defns = {} + UclidContext.module_assumes = {} + UclidContext.modules = {} + UclidContext.module_name = "main" + + @staticmethod + def setContext(module_name): + UclidContext.module_name = module_name + if module_name not in UclidContext.modules: + UclidContext.var_decls[module_name] = dict() + UclidContext.const_decls[module_name] = dict() + UclidContext.typ_decls[module_name] = dict() + UclidContext.instance_decls[module_name] = dict() + UclidContext.ip_var_decls[module_name] = [] + UclidContext.op_var_decls[module_name] = [] + UclidContext.import_decls[module_name] = [] + UclidContext.define_decls[module_name] = [] + UclidContext.procedure_defns[module_name] = [] + UclidContext.module_assumes[module_name] = [] + UclidContext.modules[module_name] = None + + @staticmethod + def __add_typdecl__(name, decl): + if name in UclidContext.typ_decls[UclidContext.module_name]: + _logger.warn("Redeclaration of type named {}".format(name)) + else: + UclidContext.typ_decls[UclidContext.module_name][name] = decl + + @staticmethod + def __add_vardecl__(name, decl): + if name in UclidContext.var_decls[UclidContext.module_name]: + _logger.warn("Redeclaration of name {}".format(name)) + else: + if decl.porttype == PortType.input: + _ = UclidContext.ip_var_decls[UclidContext.module_name].append(decl) + elif decl.porttype == PortType.output: + _ = UclidContext.op_var_decls[UclidContext.module_name].append(decl) + UclidContext.var_decls[UclidContext.module_name][name] = decl + + @staticmethod + def __add_constdecl__(name, decl): + if name in UclidContext.const_decls[UclidContext.module_name]: + _logger.warn("Redeclaration of const {}".format(name)) + else: + UclidContext.const_decls[UclidContext.module_name][name] = decl + + @staticmethod + def __add_instancedecl__(name, decl): + if name in UclidContext.instance_decls[UclidContext.module_name]: + _logger.warn("Redeclaration of instance {}".format(name)) + else: + UclidContext.instance_decls[UclidContext.module_name][name] = decl + + @staticmethod + def __add_importdecl__(decl): + UclidContext.import_decls[UclidContext.module_name].append(decl) + + @staticmethod + def __add_definedecl__(decl): + UclidContext.define_decls[UclidContext.module_name].append(decl) + + @staticmethod + def __add_proceduredefn__(defn): + UclidContext.procedure_defns[UclidContext.module_name].append(defn) + + @staticmethod + def __add_moduleassumes__(assm): + UclidContext.module_assumes[UclidContext.module_name].append(assm) + + # @staticmethod + # def __add_moduleproperty__(prop): + # UclidContext.module_properties[UclidContext.module_name].append(prop) + + @staticmethod + def __typdecls__(module): + if module.name not in UclidContext.typ_decls: + return "" + return "\n".join( + [ + textwrap.indent(decl.__inject__(), "\t") + for k, decl in UclidContext.typ_decls[module.name].items() + ] + ) + + @staticmethod + def __vardecls__(module): + if module.name not in UclidContext.var_decls: + return "" + return "\n".join( + [ + textwrap.indent(decl.__inject__(), "\t") + for k, decl in UclidContext.var_decls[module.name].items() + ] + ) + + @staticmethod + def __constdecls__(module): + if ( + module.name not in UclidContext.const_decls + or not UclidContext.const_decls[module.name] + ): + return "" + return "\n".join( + [ + textwrap.indent(decl.__inject__(), "\t") + for k, decl in UclidContext.const_decls[module.name].items() + ] + ) + + @staticmethod + def __instancedecls__(module): + if module.name not in UclidContext.instance_decls: + return "" + return "\n".join( + [ + textwrap.indent(decl.__inject__(), "\t") + for k, decl in UclidContext.instance_decls[module.name].items() + ] + ) + + @staticmethod + def __importdecls__(module): + if module.name not in UclidContext.import_decls: + return "" + return "\n".join( + [ + textwrap.indent(decl.__inject__(), "\t") + for decl in UclidContext.import_decls[module.name] + ] + ) + + @staticmethod + def __definedecls__(module): + if module.name not in UclidContext.define_decls: + return "" + return "\n".join( + [decl.__inject__() for decl in UclidContext.define_decls[module.name]] + ) + + @staticmethod + def __proceduredefns__(module): + if module.name not in UclidContext.procedure_defns: + return "" + return "\n".join( + [ + textwrap.indent(defn.__inject__(), "\t") + for defn in UclidContext.procedure_defns[module.name] + ] + ) + + @staticmethod + def __moduleassumes__(module): + if module.name not in UclidContext.module_assumes: + return "" + return "\n".join( + [ + textwrap.indent(assm.__inject__(), "\t") + for assm in UclidContext.module_assumes[module.name] + ] + ) + + # @staticmethod + # def __moduleproperties__(module): + # if module.name not in UclidContext.module_properties: + # return "" + # return "\n".join([prop.__inject__() for + # prop in UclidContext.module_properties[module.name]]) + + @staticmethod + def __inject__(): + acc = "" + for modulename in UclidContext.modules: + acc += UclidContext.modules[modulename].__inject__() + return acc + + +setContext = UclidContext.setContext +clearAll = UclidContext.clearAll + + +class UclidElement: + def __init__(self) -> None: + pass + + def __inject__(self): + raise NotImplementedError + + +class UclidModule(UclidElement): + + def __init__(self, name, init=None, nextb=None, control=None, properties=[]): + super().__init__() + self.name = name + self.init = init + self.nextb = nextb + self.control = control + self.properties = properties + UclidContext.modules[self.name] = self + + def __inject__(self): + # dependencies: + # i.obj.module.name for i in UclidContext.instance_decls[self.name].values() + # acc: + # "\n\n".join([UclidContext.modules[dep].__inject__() for dep in dependencies]) + acc = "" + init_code = textwrap.indent( + self.init.__inject__() if self.init is not None else "", "\t" + ) + next_code = textwrap.indent( + self.nextb.__inject__() if self.nextb is not None else "", "\t" + ) + control_code = textwrap.indent( + self.control.__inject__() if self.control is not None else "", "\t" + ) + decls_code = textwrap.dedent( + """ + \t// Imports + {} + + \t// Types + {} + + \t// Variables + {} + + \t// Consts + {} + + \t// Instances + {} + + \t// Defines + {} + + \t// Procedures + {} + + \t// Assumes + {} + """ + ).format( + UclidContext.__importdecls__(self), + UclidContext.__typdecls__(self), + UclidContext.__vardecls__(self), + UclidContext.__constdecls__(self), + UclidContext.__instancedecls__(self), + UclidContext.__definedecls__(self), + UclidContext.__proceduredefns__(self), + UclidContext.__moduleassumes__(self), + ) + prop_code = "\n".join( + [textwrap.indent(prop.__inject__(), "\t") for prop in self.properties] + ) + acc += textwrap.dedent( + """ + module {} {{ + {} + + {} + + {} + + {} + + {} + }} + """ + ).format(self.name, decls_code, init_code, next_code, prop_code, control_code) + return acc + + +class UclidInit(UclidElement): + def __init__(self, block) -> None: + super().__init__() + if isinstance(block, UclidBlock): + self.block = block + elif isinstance(block, list): + self.block = UclidBlock(block, 1) + else: + _logger.error( + "Unsupported type {} of block in UclidInit".format(type(block)) + ) + + def __inject__(self): + return """ +init {{ +{} +}}""".format( + textwrap.indent(self.block.__inject__(), "\t") + ) + + +class UclidNext(UclidElement): + def __init__(self, block) -> None: + super().__init__() + if isinstance(block, UclidBlock): + self.block = block + elif isinstance(block, list): + self.block = UclidBlock(block, 1) + elif isinstance(block, UclidStmt): + self.block = UclidBlock([block], 1) + else: + _logger.error( + "Unsupported type {} of block in UclidNext".format(type(block)) + ) + + def __inject__(self): + return textwrap.dedent( + """ + next {{ + {} + }}""" + ).format(textwrap.indent(self.block.__inject__().strip(), "\t")) + + +class UclidProperty(UclidElement): + def __init__(self, name, body, is_ltl=False) -> None: + super().__init__() + self.name = name + self.body = body + self.is_ltl = is_ltl + + def __inject__(self): + if not self.is_ltl: + return "property {} : {};\n".format(self.name, self.body.__inject__()) + return "property[LTL] {} : {};\n".format(self.name, self.body.__inject__()) + + +class UclidModuleAssume(UclidElement): + def __init__(self, body) -> None: + super().__init__() + self.body = body + UclidContext.__add_moduleassumes__(self) + + def __inject__(self): + return " assume ({});".format(self.body.__inject__()) + + +class Operators: + """ + Comprehensive operator list + """ + + OpMapping = { + "add": ("+", 2), + "sub": ("-", 2), + "umin": ("-", 1), + "gt": (">", 2), + "gte": (">=", 2), + "lt": ("<", 2), + "lte": ("<=", 2), + "eq": ("==", 2), + "neq": ("!=", 2), + "not": ("!", 1), + "xor": ("^", 2), + "and": ("&&", -1), + "or": ("||", -1), + "implies": ("==>", 2), + "bvadd": ("+", 2), + "bvsub": ("-", 2), + "bvand": ("&", 2), + "bvor": ("|", 2), + "bvnot": ("~", 1), + "bvlt": ("<", 2), + "bvult": ("<_u", 2), + "bvgt": (">", 2), + "bvugt": (">_u", 2), + "next": ("X", 1), + "eventually": ("F", 1), + "always": ("G", 1), + "concat": ("++", -1), + } + + def __init__(self, op_) -> None: + self.op = op_ + + def __inject__(self): + return Operators.OpMapping[self.op][0] + + +# Base class for Uclid expressions +class UclidExpr(UclidElement): + def __inject__(self): + raise NotImplementedError + + def __eq__(self, other): + if isinstance(other, UclidExpr): + return UclidOpExpr("eq", [self, other]) + elif isinstance(other, int): + return UclidOpExpr("eq", [self, UclidLiteral(str(other))]) + elif isinstance(other, str): + return UclidOpExpr("eq", [self, UclidLiteral(other)]) + else: + _logger.error( + "Unsupported types for operation {}: {} and {}".format( + " == ", "UclidExpr", type(other) + ) + ) + + def __ne__(self, other): + if isinstance(other, UclidExpr): + return UclidOpExpr("neq", [self, other]) + elif isinstance(other, int): + return UclidOpExpr("neq", [self, UclidLiteral(str(other))]) + elif isinstance(other, str): + return UclidOpExpr("neq", [self, UclidLiteral(other)]) + else: + _logger.error( + "Unsupported types for operation {}: {} ({}) and {}".format( + "!=", "UclidExpr", self.__inject__(), type(other) + ) + ) + + def __add__(self, other): + if isinstance(other, UclidExpr): + return UclidOpExpr("add", [self, other]) + elif isinstance(other, int): + return UclidOpExpr("add", [self, UclidLiteral(str(other))]) + else: + _logger.error( + "Unsupported types for operation {}: {} and {}".format( + "+", "UclidExpr", type(other) + ) + ) + + def __invert__(self): + return UclidOpExpr("not", [self]) + + def __and__(self, other): + if isinstance(other, UclidExpr): + return UclidOpExpr("and", [self, other]) + else: + _logger.error( + "Unsupported types for operation {}: {} and {}".format( + "&", "UclidExpr", type(other) + ) + ) + + +# All kinds of operators Operators +class UclidOpExpr(UclidExpr): + def __init__(self, op, children) -> None: + super().__init__() + self.op = op + self.children = [ + UclidLiteral(str(child)) if isinstance(child, int) else child + for child in children + ] + + def __inject__(self): + children_code = ["({})".format(child.__inject__()) for child in self.children] + oprep = Operators.OpMapping[self.op] + if oprep[1] == 1: + assert len(children_code) == 1, "Unary operator must have one argument" + return "{} {}".format(oprep[0], children_code[0]) + if oprep[1] == 2: + assert len(children_code) == 2, "Unary operator must have two arguments" + return "{} {} {}".format(children_code[0], oprep[0], children_code[1]) + if oprep[1] == -1: + return (" " + oprep[0] + " ").join(children_code) + else: + _logger.error("Operator arity not yet supported") + + +def Uadd(args): + return UclidOpExpr("add", args) + + +def Usub(args): + return UclidOpExpr("sub", args) + + +def Uumin(args): + return UclidOpExpr("umin", args) + + +def Ugt(args): + return UclidOpExpr("gt", args) + + +def Ugte(args): + return UclidOpExpr("gte", args) + + +def Ult(args): + return UclidOpExpr("lt", args) + + +def Ulte(args): + return UclidOpExpr("lte", args) + + +def Ueq(args): + return UclidOpExpr("eq", args) + + +def Uneq(args): + return UclidOpExpr("neq", args) + + +def Unot(args): + return UclidOpExpr("not", args) + + +def Uxor(args): + return UclidOpExpr("xor", args) + + +def Uand(args): + return UclidOpExpr("and", args) + + +def Uor(args): + return UclidOpExpr("or", args) + + +def Uimplies(args): + return UclidOpExpr("implies", args) + + +def Ubvadd(args): + return UclidOpExpr("bvadd", args) + + +def Ubvsub(args): + return UclidOpExpr("bvsub", args) + + +def Ubvand(args): + return UclidOpExpr("bvand", args) + + +def Ubvor(args): + return UclidOpExpr("bvor", args) + + +def Ubvnot(args): + return UclidOpExpr("bvnot", args) + + +def Ubvlt(args): + return UclidOpExpr("bvlt", args) + + +def Ubvult(args): + return UclidOpExpr("bvult", args) + + +def Ubvgt(args): + return UclidOpExpr("bvgt", args) + + +def Ubvugt(args): + return UclidOpExpr("bvugt", args) + + +def Unext(args): + return UclidOpExpr("next", args) + + +def Ueventually(args): + return UclidOpExpr("eventually", args) + + +def Ualways(args): + return UclidOpExpr("always", args) + + +def Uconcat(args): + return UclidOpExpr("concat", args) + + +class UclidBVSignExtend(UclidExpr): + def __init__(self, var, ewidth): + super().__init__() + self.var = var + self.ewidth = ewidth + + def __inject__(self): + return "bv_sign_extend({}, {})".format(self.ewidth, self.var.__inject__()) + + +class UclidFunctionApply(UclidExpr): + def __init__(self, func, arglist): + super().__init__() + self.iname = func if isinstance(func, str) else func.name + self.arglist = arglist + + def __inject__(self): + return "{}({})".format( + self.iname, ", ".join([arg.__inject__() for arg in self.arglist]) + ) + + +class UclidArraySelect(UclidExpr): + def __init__(self, array, indexseq): + super().__init__() + self.iname = array if isinstance(array, str) else array.__inject__() + self.indexseq = [ + ind if isinstance(ind, UclidExpr) else UclidLiteral(str(ind)) + for ind in indexseq + ] + + def __inject__(self): + return "{}[{}]".format( + self.iname, "][".join([ind.__inject__() for ind in self.indexseq]) + ) + + +class UclidArrayUpdate(UclidExpr): + def __init__(self, array, index, value): + super().__init__() + self.iname = array if isinstance(array, str) else array.__inject__() + self.index = index if isinstance(index, UclidExpr) else UclidLiteral(str(index)) + self.value = value if isinstance(value, UclidExpr) else UclidLiteral(str(value)) + + def __inject__(self): + return "{}[{} -> {}]".format( + self.iname, self.index.__inject__(), self.value.__inject__() + ) + + +class UclidBVExtract(UclidExpr): + def __init__(self, bv: UclidExpr, high, low): + super().__init__() + self.bv = bv + self.high = high + self.low = low + + def __inject__(self): + return "({})[{}:{}]".format(self.bv.__inject__(), self.high, self.low) + + +class UclidRecordSelect(UclidExpr): + def __init__(self, recvar, elemname): + super().__init__() + self.recvar = recvar + self.elemname = elemname + + def __inject__(self): + return "{}.{}".format(self.recvar.__inject__(), self.elemname) + + +class UclidForall(UclidExpr): + def __init__(self, variable, typ, expr: UclidExpr): + super().__init__() + self.variable = variable + self.typ = typ + self.expr = expr + + def __inject__(self): + return "forall ({} : {}) :: ({})".format( + self.variable, self.typ.__inject__(), self.expr.__inject__() + ) + + +class DeclTypes(Enum): + VAR = 0 + FUNCTION = 1 + TYPE = 2 + INSTANCE = 3 + SYNTHFUN = 4 + DEFINE = 5 + CONST = 6 + + def __inject__(self): + if self.value == 0: + return "var" + elif self.value == 1: + return "function" + elif self.value == 2: + return "type" + elif self.value == 3: + return "instance" + elif self.value == 4: + return "synthesis function" + elif self.value == 5: + return "define" + elif self.value == 6: + return "const" + else: + _logger.error("Unsupported decl type {}".format(self.name)) + return "" + + +# Base class for (all sorts of) uclid declarations +class UclidDecl(UclidElement): + def __init__(self, obj, decltype) -> None: + super().__init__() + # name is just a string + self.name = obj.name + self.obj = obj + # body should support the __inject__() operator + self.declstring = obj.declstring + self.decltype = decltype + if self.decltype == DeclTypes.VAR: + self.porttype = obj.porttype + self.inject_str = "{} {} : {};".format( + self.porttype.name, self.name, self.declstring + ) + UclidContext.__add_vardecl__(self.name, self) + elif self.decltype == DeclTypes.TYPE: + self.inject_str = "type {} = {};".format(self.name, self.declstring) + UclidContext.__add_typdecl__(self.name, self) + elif self.decltype == DeclTypes.INSTANCE: + self.inject_str = "instance {} : {};".format(self.name, self.declstring) + UclidContext.__add_instancedecl__(self.name, self) + elif self.decltype == DeclTypes.CONST: + self.inject_str = "const {} : {};".format(self.name, self.declstring) + UclidContext.__add_constdecl__(self.name, self) + # TODO: add support for other types + # TODO: add full type system + else: + _logger.error("Currently only var declaration is permitted") + exit(1) + + def __inject__(self): + return self.inject_str + + +class UclidTypeDecl(UclidDecl): + def __init__(self, obj) -> None: + super().__init__(obj, DeclTypes.TYPE) + + +class UclidType: + def __init__(self, name): + self.name = name + + def __inject__(self): + return self.name + + +class UclidBooleanType(UclidType): + def __init__(self, name=""): + super().__init__(name) + self.declstring = "boolean" + if name != "": + self.name = name + self.decl = UclidTypeDecl(self) + else: + self.name = self.declstring + + +UBool = UclidBooleanType + + +class UclidIntegerType(UclidType): + def __init__(self, name=""): + super().__init__(name) + self.declstring = "integer" + if name != "": + self.name = name + self.decl = UclidTypeDecl(self) + else: + self.name = self.declstring + + +class UclidBVType(UclidType): + def __init__(self, width, name=""): + super().__init__(name) + self.width = width + self.declstring = "bv{}".format(self.width) + if name != "": + self.name = name + self.decl = UclidTypeDecl(self) + else: + self.name = self.declstring + + +Ubv = UclidBVType + + +class UclidArrayType(UclidType): + def __init__(self, itype, etype, name=""): + super().__init__(name) + self.indextype = itype + self.elemtype = etype + self.declstring = "[{}]{}".format( + self.indextype.__inject__(), self.elemtype.__inject__() + ) + if name != "": + self.name = name + self.decl = UclidTypeDecl(self) + else: + self.name = self.declstring + + +class UclidEnumType(UclidType): + def __init__(self, members, name=""): + super().__init__(name) + self.members = members + if name != "": + self.name = name + self.declstring = "enum {{ {} }}".format(", ".join(self.members)) + self.decl = UclidTypeDecl(self) + else: + _logger.error("Enum type must be a named type in UclidEnumType!") + + +class UclidLiteralType(UclidType): + def __init__(self, name): + super().__init__(name) + self.declstring = name + + +class UclidFunctionType(UclidType): + """ + Function signature type + """ + + def __init__(self, ip_args, out_type) -> None: + # Function type does not have a declaration + # so it also does not require a name/declstring + super().__init__("") + self.ip_args = ip_args + self.out_type = out_type + + def __inject__(self): + input_sig = ", ".join( + ["{} : {}".format(i[0], i[1].__inject__()) for i in self.ip_args] + ) + return "({}) : {}".format(input_sig, self.out_type.__inject__()) + + +class UclidProcedureType(UclidType): + # inputs_args are pairs of str, Uclidtype elements + def __init__(self, ip_args, modify_vars, return_vars): + # Procedure type does not have a declaration + # so it also does not require a name/declstring + super().__init__("") + self.ip_args = ip_args + self.modify_vars = modify_vars + self.return_vars = return_vars + + def __inject__(self): + input_sig = ", ".join( + [ + "{} : {}".format( + i[0] if isinstance(i[0], str) else i[0].lit, i[1].declstring + ) + for i in self.ip_args + ] + ) + modify_sig = ( + "\nmodifies {};".format( + ", ".join([sig.__inject__() for sig in self.modify_vars]) + ) + if len(self.modify_vars) != 0 + else "" + ) + return_sig = ( + "\nreturns ({})".format( + ", ".join( + ["{} : {}".format(i[0], i[1].declstring) for i in self.return_vars] + ) + ) + if len(self.return_vars) != 0 + else "" + ) + return "({}){}{}".format(input_sig, modify_sig, return_sig) + + +class PortType(Enum): + var = 0 + input = 1 + output = 2 + + def __inject__(self): + if self.value == PortType.var: + return "var" + elif self.value == PortType.input: + return "input" + elif self.value == PortType.output: + return "output" + else: + _logger.error("Unsupported port type") + + +class UclidInstance(UclidElement): + """ + Module instances in Uclid + """ + + def __init__(self, name, module, argmap) -> None: + super().__init__() + self.name = name + self.module = module + self.argmap = argmap + modname = module.name + # print(argmap) + # print([i.__inject__() for i in UclidContext.ip_var_decls[modname]]) + self.declstring = "{}({})".format( + modname, + ", ".join( + [ + "{} : ({})".format(port.name, argmap[port.name].__inject__()) + for port in UclidContext.ip_var_decls[modname] + + UclidContext.op_var_decls[modname] + ] + ), + ) + self.decl = UclidDecl(self, DeclTypes.INSTANCE) + + def __inject__(self): + return self.name + + +class UclidInstanceRaw(UclidElement): + """ + Raw (external) module instances in Uclid + """ + + def __init__(self, name, module, argmap) -> None: + super().__init__() + self.name = name + self.argmap = argmap + modname = module.name if isinstance(module, UclidModule) else module + # print(argmap) + # print([i.__inject__() for i in UclidContext.ip_var_decls[modname]]) + self.declstring = "{}({})".format( + modname, + ", ".join( + ["{} : ({})".format(portname, argmap[portname]) for portname in argmap] + ), + ) + self.decl = UclidDecl(self, DeclTypes.INSTANCE) + + def __inject__(self): + return self.name + + +class UclidInstanceVarAccess(UclidExpr): + def __init__(self, instance, var): + self.instance = ( + instance.__inject__() if isinstance(instance, UclidModule) else instance + ) + self.var = var + + def __inject__(self): + return "{}.{}".format(self.instance, self.var.__inject__()) + + +class UclidImport(UclidElement): + """ + Import declarations from other modules + """ + + def __init__(self, impobj, modulename, refname=None) -> None: + super().__init__() + self.impobj = impobj + self.modulename = modulename + self.refname = refname if refname is not None else impobj.name + UclidContext.__add_importdecl__(self) + + def __inject__(self): + return "{} {} = {}.{};".format( + self.impobj.decl.decltype.__inject__(), + self.impobj.name, + self.modulename, + self.refname, + ) + + +class UclidWildcardImport(UclidImport): + """ + Import declarations from other modules + """ + + def __init__(self, type_: DeclTypes, modulename) -> None: + self.type = type_ + self.modulename = modulename + UclidContext.__add_importdecl__(self) + + def __inject__(self): + return "{} * = {}.*;".format(self.type.__inject__(), self.modulename) + + +class UclidDefine(UclidElement): + """ + Define (function) declarations + """ + + def __init__( + self, name: str, function_sig: UclidFunctionType, body: UclidExpr + ) -> None: + super().__init__() + self.name = name + self.function_sig = function_sig + self.body = body + UclidContext.__add_definedecl__(self) + + def __inject__(self): + return "\tdefine {}{} = {};".format( + self.name, self.function_sig.__inject__(), self.body.__inject__() + ) + + +# A named literal (WYSIWYG) +class UclidLiteral(UclidExpr): + """ + Literals and variables in Uclid + """ + + def __init__(self, lit, isprime=False) -> None: + super().__init__() + self.lit = lit if isinstance(lit, str) else str(lit) + self.isprime = isprime + + def p(self): + if self.isprime: + _logger.warn("Double prime for literal {}".format(self.lit)) + return UclidLiteral(self.lit + "'", True) + + def __inject__(self): + return self.lit + + def __add__(self, other): + return super().__add__(other) + + +class UclidIntegerConst(UclidLiteral): + def __init__(self, val): + super().__init__(val) + + +class UclidBooleanConst(UclidLiteral): + def __init__(self, val: bool): + super().__init__(str(val).lower()) + + +class UclidBVConst(UclidLiteral): + def __init__(self, val, width: int): + super().__init__(val) + self.width = width + self.lit = f"{self.lit}bv{str(self.width)}" + + +# Uclid literal which must be declared as a variable +class UclidVar(UclidLiteral): + def __init__(self, name, typ: UclidType, porttype=PortType.var): + super().__init__(name) + self.name = name + self.typ = typ + self.porttype = porttype + self.declstring = typ.name + _ = UclidDecl(self, DeclTypes.VAR) + + def __inject__(self): + return self.name + + def __add__(self, other): + return super().__add__(other) + + +def mkVar(varname: list, typ, porttype): + return UclidVar(varname, typ, porttype) + + +def mkVars(varnames: list, typ, porttype): + return [UclidVar(varname, typ, porttype) for varname in varnames] + + +class UclidConst(UclidLiteral): + def __init__(self, name: str, typ: UclidType, value=None): + super().__init__(name) + self.name = name + self.typ = typ + if value is None: + self.declstring = typ.name + else: + self.declstring = "{} = {}".format( + typ.name, + value.__inject__() if isinstance(value, UclidExpr) else str(value), + ) + _ = UclidDecl(self, DeclTypes.CONST) + + def __inject__(self): + return self.name + + +# Uclid integer type declaration +class UclidIntegerVar(UclidVar): + def __init__(self, name, porttype=PortType.var) -> None: + super().__init__(name, UclidIntegerType(), porttype) + + def __add__(self, other): + return super().__add__(other) + + +def mkIntVar(varname: str, porttype=PortType.var): + return UclidIntegerVar(varname, porttype) + + +def mkIntVars(varnames: list, porttype=PortType.var): + return [UclidIntegerVar(varname, porttype) for varname in varnames] + + +# Uclid bitvector type declaration +class UclidBVVar(UclidVar): + def __init__(self, name, width, porttype=PortType.var) -> None: + super().__init__(name, UclidBVType(width), porttype) + self.width = width + + def __add__(self, other): + return super().__add__(other) + + +class UclidBooleanVar(UclidVar): + def __init__(self, name, porttype=PortType.var) -> None: + super().__init__(name, UclidBooleanType(), porttype) + + def __add__(self, _): + _logger.error("Addition not supported on Boolean type") + # return super().__add__(other) + + +class UclidComment(UclidElement): + def __init__(self, text: str) -> None: + super().__init__() + self.text = text + + def __inject__(self): + return "\t//{}\n".format(self.text) + + +class UclidStmt(UclidElement): + """ + Statements in Uclid. + """ + + def __init__(self): + pass + + def __inject__(self): + raise NotImplementedError + + +class UclidRaw(UclidStmt): + def __init__(self, stmt: str): + super().__init__() + self.stmt = stmt + + def __inject__(self): + return self.stmt + + +class UclidEmpty(UclidRaw): + def __init__(self): + super().__init__("") + + +class UclidLocalVarInst(UclidStmt): + def __init__(self, name, typ): + super().__init__() + self.name = name + self.typ = typ + + def __inject__(self): + return "var {} : {};".format(self.name, self.typ.__inject__()) + + +class UclidAssign(UclidStmt): + def __init__(self, lval, rval) -> None: + super().__init__() + self.lval = lval + if isinstance(rval, UclidExpr): + self.rval = rval + elif isinstance(rval, int): + self.rval = UclidLiteral(str(rval)) + elif isinstance(rval, str): + self.rval = UclidLiteral(rval) + else: + _logger.error("Unsupported rval type {} in UclidAssign".format(type(rval))) + + def __inject__(self): + return "{} = {};".format(self.lval.__inject__(), self.rval.__inject__()) + + +class UclidBlock(UclidStmt): + def __init__(self, stmts=[], indent=0) -> None: + super().__init__() + self.stmts = stmts + self.indent = indent + + def __inject__(self): + return ("\n" + self.indent * "\t").join( + [stmt.__inject__() for stmt in self.stmts] + ) + + +class UclidCase(UclidStmt): + def __init__(self, conditionlist, stmts): + if not isinstance(conditionlist, list) or not isinstance(stmts, list): + _logger.error( + "UclidCase requires a pair of lists denoting case-split conditions/stmts" + ) + print([cond.__inject__() for cond in conditionlist]) + self.conditionlist = conditionlist + self.stmts = stmts + + def __inject__(self): + cases = [ + "({})\t: {{ \n{} \n}}".format( + item[0].__inject__(), textwrap.indent(item[1].__inject__(), "\t") + ) + for item in zip(self.conditionlist, self.stmts) + ] + return textwrap.dedent( + """ + case + {} + esac + """ + ).format("\n".join(cases)) + + +class UclidITE(UclidStmt): + def __init__(self, condition, tstmt, estmt=None): + self.condition = condition + self.tstmt = tstmt + self.estmt = estmt + + def __inject__(self): + if self.estmt is None: + return """ + if ({}) {{ {} }} + """.format( + self.condition.__inject__(), self.tstmt.__inject__() + ) + else: + return """ + if ({}) {{ {} }} else {{ {} }} + """.format( + self.condition.__inject__(), + self.tstmt.__inject__(), + self.estmt.__inject__(), + ) + + +class UclidITENested(UclidStmt): + def __init__(self, conditionlist, stmtlist): + if len(conditionlist) == len(stmtlist): + self.format = "IT" + elif len(conditionlist) == len(stmtlist) - 1: + self.format = "ITE" + else: + _logger.error( + "Illegal lengths of conditionlist and stmt blocks in ITE operator" + ) + self.conditionlist = conditionlist + self.stmtlist = stmtlist + + def __inject__(self): + def ite_rec(clist, slist): + if len(clist) > 0 and len(slist) > 0: + nesting = ite_rec(clist[1:], slist[1:]) + return """ + if ({}) {{ {} }} + else {{ {} }}""".format( + clist[0].__inject__(), slist[0].__inject__(), nesting + ) + elif len(slist) > 0: + return "{}".format(slist[0].__inject__()) + elif len(clist) == 0: + return "" + else: + _logger.error("Mismatched clist/slist lengths in ite_rec") + + return ite_rec(self.conditionlist, self.stmtlist) + + +class UclidProcedure(UclidElement): + def __init__(self, name: str, typ: UclidProcedureType, body: UclidStmt): + super().__init__() + self.name = name + self.typ = typ + self.body = body + UclidContext.__add_proceduredefn__(self) + + def __inject__(self): + return """procedure {} {} +{{ +{} +}} + """.format( + self.name, + self.typ.__inject__(), + textwrap.indent(self.body.__inject__(), "\t"), + ) + + +class UclidProcedureCall(UclidStmt): + def __init__(self, proc, ip_args, ret_vals): + super().__init__() + self.iname = proc if isinstance(proc, str) else proc.name + self.ip_args = ip_args + self.ret_vals = ret_vals + + def __inject__(self): + return "call ({}) = {}({});".format( + ", ".join([ret.__inject__() for ret in self.ret_vals]), + self.iname, + ", ".join([arg.__inject__() for arg in self.ip_args]), + ) + + +class UclidInstanceProcedureCall(UclidStmt): + def __init__(self, instance, proc, ip_args, ret_vals): + super().__init__() + self.instance = instance if isinstance(instance, str) else instance.name + self.iname = "{}.{}".format( + self.instance, proc if isinstance(proc, str) else proc.name + ) + self.ip_args = ip_args + self.ret_vals = ret_vals + + def __inject__(self): + return "call ({}) = {}({});".format( + ", ".join([ret.__inject__() for ret in self.ret_vals]), + self.iname, + ", ".join([arg.__inject__() for arg in self.ip_args]), + ) + + +class UclidNextStmt(UclidStmt): + def __init__(self, instance): + super().__init__() + self.instance = instance + + def __inject__(self): + return "next ({});".format(self.instance.__inject__()) + + +class UclidAssume(UclidStmt): + def __init__(self, body): + super().__init__() + self.body = body + + def __inject__(self): + return "assume({});".format(self.body.__inject__()) + + +class UclidAssert(UclidStmt): + def __init__(self, body): + super().__init__() + self.body = body + + def __inject__(self): + return "assert({});".format(self.body.__inject__()) + + +class UclidHavoc(UclidStmt): + def __init__(self, variable): + super().__init__() + self.variable = variable + + def __inject__(self): + return "havoc {};".format(self.variable.__inject__()) + + +class UclidFor(UclidStmt): + def __init__(self, range_variable, range_typ, range_low, range_high, body): + super().__init__() + self.range_high = range_high + self.range_low = range_low + self.range_variable = range_variable + self.range_typ = range_typ + self.body = body + + def __inject__(self): + return """ +for ({} : {}) in range({}, {}) {{ + {} +}} +""".format( + self.range_variable.__inject__(), + self.range_typ.__inject__(), + self.range_low.__inject__(), + self.range_high.__inject__(), + self.body.__inject__(), + ) + + +class UclidControlCommand(UclidElement): + """ + Uclid control block commands. + """ + + def __init__(self): + pass + + def __inject__(self): + raise NotImplementedError + + +class UclidControlBlock(UclidControlCommand): + def __init__(self, stmts=[]): + super().__init__() + self.stmts = stmts + + def add(self, stmt): + self.stmts.append(stmt) + + def __inject__(self): + return """ +control {{ +{} +}}""".format( + textwrap.indent("\n".join([stmt.__inject__() for stmt in self.stmts]), "\t") + ) + + +class UclidUnrollCommand(UclidControlCommand): + def __init__(self, name, depth): + self.depth = depth + self.name = name + + def __inject__(self): + return "{} = unroll({});".format(self.name, self.depth) + + +class UclidBMCCommand(UclidControlCommand): + def __init__(self, name, depth): + self.depth = depth + self.name = name + + def __inject__(self): + return "{} = bmc({});".format(self.name, self.depth) + + +class UclidCheckCommand(UclidControlCommand): + def __init__(self): + super().__init__() + + def __inject__(self): + return "check;" + + +class UclidPrintCexCommand(UclidControlCommand): + def __init__(self, engine, trace_items=[]): + super().__init__() + self.engine = engine + self.trace_items = trace_items + + def __inject__(self): + return "{}.print_cex({});".format( + self.engine.name, + ", ".join( + [ + item.__inject__() if isinstance(item, UclidExpr) else str(item) + for item in self.trace_items + ] + ), + ) + + +class UclidPrintCexJSONCommand(UclidControlCommand): + def __init__(self, engine, trace_items=[]): + super().__init__() + self.engine = engine + self.trace_items = trace_items + + def __inject__(self): + return "{}.print_cex_json({});".format( + self.engine.name, + ", ".join( + [ + item.__inject__() if isinstance(item, UclidExpr) else str(item) + for item in self.trace_items + ] + ), + ) + + +class UclidPrintResultsCommand(UclidControlCommand): + def __init__(self): + super().__init__() + + def __inject__(self): + return "print_results;" + + +# LTL Operator Macros +def X(expr): + return UclidOpExpr("next", [expr]) + + +def F(expr): + return UclidOpExpr("eventually", [expr]) + + +def G(expr): + return UclidOpExpr("globally", [expr]) + + +CMD_check = UclidCheckCommand() +CMD_print = UclidPrintResultsCommand() diff --git a/tests/conftest.py b/tests/conftest.py new file mode 100644 index 0000000..d4132c2 --- /dev/null +++ b/tests/conftest.py @@ -0,0 +1,10 @@ +""" + Dummy conftest.py for uclid. + + If you don't know what this is for, just leave it empty. + Read more about conftest.py under: + - https://docs.pytest.org/en/stable/fixture.html + - https://docs.pytest.org/en/stable/writing_plugins.html +""" + +# import pytest diff --git a/tests/test_ast.py b/tests/test_ast.py new file mode 100644 index 0000000..61779ea --- /dev/null +++ b/tests/test_ast.py @@ -0,0 +1,9 @@ +from uclid.ast import Uadd + +__author__ = "Federico Mora" +__copyright__ = "Federico Mora" +__license__ = "MIT" + + +def test_uadd(): + assert Uadd([1, 2]).__inject__() == "(1) + (2)" diff --git a/tox.ini b/tox.ini new file mode 100644 index 0000000..69f8159 --- /dev/null +++ b/tox.ini @@ -0,0 +1,93 @@ +# Tox configuration file +# Read more under https://tox.wiki/ +# THIS SCRIPT IS SUPPOSED TO BE AN EXAMPLE. MODIFY IT ACCORDING TO YOUR NEEDS! + +[tox] +minversion = 3.24 +envlist = default +isolated_build = True + + +[testenv] +description = Invoke pytest to run automated tests +setenv = + TOXINIDIR = {toxinidir} +passenv = + HOME + SETUPTOOLS_* +extras = + testing +commands = + pytest {posargs} + + +# # To run `tox -e lint` you need to make sure you have a +# # `.pre-commit-config.yaml` file. See https://pre-commit.com +# [testenv:lint] +# description = Perform static analysis and style checks +# skip_install = True +# deps = pre-commit +# passenv = +# HOMEPATH +# PROGRAMDATA +# SETUPTOOLS_* +# commands = +# pre-commit run --all-files {posargs:--show-diff-on-failure} + + +[testenv:{build,clean}] +description = + build: Build the package in isolation according to PEP517, see https://github.com/pypa/build + clean: Remove old distribution files and temporary build artifacts (./build and ./dist) +# https://setuptools.pypa.io/en/stable/build_meta.html#how-to-use-it +skip_install = True +changedir = {toxinidir} +deps = + build: build[virtualenv] +passenv = + SETUPTOOLS_* +commands = + clean: python -c 'import shutil; [shutil.rmtree(p, True) for p in ("build", "dist", "docs/_build")]' + clean: python -c 'import pathlib, shutil; [shutil.rmtree(p, True) for p in pathlib.Path("src").glob("*.egg-info")]' + build: python -m build {posargs} +# By default, both `sdist` and `wheel` are built. If your sdist is too big or you don't want +# to make it available, consider running: `tox -e build -- --wheel` + + +[testenv:{docs,doctests,linkcheck}] +description = + docs: Invoke sphinx-build to build the docs + doctests: Invoke sphinx-build to run doctests + linkcheck: Check for broken links in the documentation +passenv = + SETUPTOOLS_* +setenv = + DOCSDIR = {toxinidir}/docs + BUILDDIR = {toxinidir}/docs/_build + docs: BUILD = html + doctests: BUILD = doctest + linkcheck: BUILD = linkcheck +deps = + -r {toxinidir}/docs/requirements.txt + # ^ requirements.txt shared with Read The Docs +commands = + sphinx-build --color -b {env:BUILD} -d "{env:BUILDDIR}/doctrees" "{env:DOCSDIR}" "{env:BUILDDIR}/{env:BUILD}" {posargs} + + +[testenv:publish] +description = + Publish the package you have been developing to a package index server. + By default, it uses testpypi. If you really want to publish your package + to be publicly accessible in PyPI, use the `-- --repository pypi` option. +skip_install = True +changedir = {toxinidir} +passenv = + # See: https://twine.readthedocs.io/en/latest/ + TWINE_USERNAME + TWINE_PASSWORD + TWINE_REPOSITORY + TWINE_REPOSITORY_URL +deps = twine +commands = + python -m twine check dist/* + python -m twine upload {posargs:--repository {env:TWINE_REPOSITORY:testpypi}} dist/*