mutual refinement

This is an illustrative implementation for the mutual refinement algorithm proposed in the paper Mutual Refinements of Context-Free Language Reachability (SAS 2023).

Platform and dependencies

Platform

The project is known to work on Linux. On MacBook or Windows the memory measure code

mutual-refinement/src/main.cpp

Line 244 in e62f3d8

std::string getPeakMemory() {

won't work, but other components should work well since they only use the standard library.

Dependencies

Python >= 3.9, C++ >= 17, and any recent version of GNU make.

These version requirements are strict. For example, Python 3.8 will not work.

Build and run

Use Python (>= 3.9) to execute run.py to build the project and run every benchmark item in the following 5 categories with 10-second time limit. Please check run.py for detailed arguments for each invocation.

• Straightforward combination (naive) for taint
• Mutual refinement (refine) for taint
• Straightforward combination (naive) for valueflow
• Mutual refinement (refine) for valueflow
• Mutual refinement (refine) for simplified-taint

Result interpretation

For each benchmark item (<name>.grammar, <name>.dot) inside exp/, the result will be stored in the file <name>.naive.result or <name>.refine.result in the corresponding directory.

Docker container

You can also pack the project in a docker image and save it in the .tar format.

docker build -t mutual-refinement .
docker save -o mutual-refinement.tar mutual-refinement:latest

Once you have the .tar file, you can share it with others. Anyone with the .tar file can load the docker image and launch a container from the image. Then one can repeat the above experiment inside the docker container. Please note: inside the container you should use the python3.9 command to run the script.

docker load --input mutual-refinement.tar
docker run --rm -ti mutual-refinement