EMME: ECMAScript Memory Model Evaluator
========================
    
This tools provides a SAT/SMT-based verification for JavaScript programs
with shared array memory access (i.e., SharedArrayBuffer).

`Learn more <https://github.com/FMJS/emme>`_.

Briefly, given a JavaScript-like SharedArrayBuffer bounded execution program (see .bex files in the examples folder), EMME computes all valid executions according with the ECMA specification (http://tc39.github.io/ecmascript_sharedmem/shmem.html). The valid executions are provided as: 1) a set of graphviz files represeting the memory model relations (i.e., mm*.dot), and 2) an assertion on the automatically generated JavaScript program (i.e., program.js).

========================
Installation
========================
Using Docker:

1) install Docker with your package manager e.g., ``sudo apt-get install docker``

2) build the Docker image: ``cd docker/fedora_64 && docker build -f fedora-emme .``

3) run the Docker image: ``docker run -i -t fedora-emme /bin/bash``

On Linux and MacOS:

1) install python package dependencies: ``pip install -r requirements.txt``

2) install CVC4 SMT solver (see http://cvc4.cs.stanford.edu/ for licensing and additional informations): ``cd ext_tools && bash get_CVC4.sh && cd ..``

3) install V8 JS engine (see https://developers.google.com/v8/ for licensing and additional informations): ``cd ext_tools && bash get_v8.sh && cd ..`` 

========================
Usage
========================

To start playing with the tool, you can run:

1) ``python emme.py examples/single_var/sv_simple01.bex`` (to generate the valid executions in the folder examples/single_var/sv_simple01/)
  
2) ``python litmus.py -c "bash ext_tools/run_v8.sh" -i examples/single_var/sv_simple01/program.js -n 1k -j 4`` (to check if the d8 engine obeys the expected results)

3) ``python emme.py examples/single_var/sv_simple01.bex --unmatched --jsengine="bash ext_tools/run_v8.sh" -n 1k -j 4`` (to perform the behavioral coverage constraint analysis)

4) ``python emme.py examples/single_var/sv_simple01.bex --synth`` (to generate all equivalent programs in the folder examples/single_var/sv_simple01/)

For more details on the license, have a look at LICENSE.txt

========================
Publications
========================

- "EMME: a formal tool for ECMAScript Memory Model Evaluation". *C. Mattarei, C. Barrett, S. Guo, B. Nelson, and B. Smith*. TACAS 2018, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Thessaloniki (Greece).

========================
Build Status
========================
.. image:: https://landscape.io/github/FMJS/EMME/master/landscape.svg?style=flat
   :target: https://landscape.io/github/FMJS/EMME/master
   :alt: Code Health

.. image:: https://travis-ci.org/FMJS/EMME.svg?branch=master
    :target: https://travis-ci.org/FMJS/EMME