M3
M3 is the memory-mmodel-mmapper, and maps (not-so-)TinyPseuCo to Z3 formulas to answer different queries about a programs' semantic with regard to a given memory model.
Installation
M3 is a Python based application, and requires Python >= 3.5 or PyPy3 >= 6.0.0 It also depends on the following third-party packages:
- z3: The python bindings for the z3 solver
- autobahn, a library to handle the websocket communication
- pyparsing, a parser combinator library which is used to parse TinyPseuCo
It is highly recommended to install all dependencies using pipenv A Pipfile is provided, which installs everything but z3. As z3 is outdated on PyPi.org, it is recommended to install an up-to-date version from your Linux distribution.
To install the packages with pipenv run
- pipenv --site-packages # (so you still get the system installed z3)
- pipenv intall
Deployment
To run M3 locally, enter the pipenv environment via pipenv shell
Then you can start the server by running python server.py
It will then run on 127.0.0.1, listening on port 5678
To change hostname and port, run python server.py --port=<PORT> --hostname=<NAME>