Utility to automatically reduce programs generated by the SpecAST utility.
- Python >= 3.6
- any C++ compiler (tested with
g++andclang++) - CMake >= 3.13
We provide a CMakeLists file to ease the building process.
> mkdir build && cd build
> cmake -DCMAKE_BUILD_TYPE=Release ..
> cd -
This will provide the mfReduce binary in the build directory.
The input to the reducer is a SpecAST generated test file. The execution is
rather tightly integrated with the
SpecASTSpecs repository. For a test to
be reduced, we expect to use a CMake compilation script, and a corresponding
compile_commands.json to correctly set paths, both of which are included for
each SUT specification in the aforementioned repository. However, an SUT
installed in the system paths might just work out of the box - the only
dependency is having access to the SUT definition.
Another component is an interestingness test, which should tell the reducer
whether the reduction process was successful. Currently, we distinguish a
successful reduction process if the return code has been maintained, as in the
provided interestingness.py.
NOTE currently this integration is quite tight, and the CMake compilation
*script is wrapped via the compile.sh script available in the SpecAST repo.
*This can be decoupled upon infrastructure revisit.
There are a few flags which affect the way the reduction is performed.
monotonic- if unset, will retry all previously attempted reduction passes upon a successful reductionno-reduce-checks- sometimes, the metamorphic checks are not required in order for a reduction to be considered successful; this option prevent these checks from being removed, in order to ensure an oracle remains, to be potentially polished further manuallyno-reduce-last-var- sometimes, a single metamorphic variant is sufficient for a successful reduction; similar to the above option, it might be useful to keep at least one other variant, in order for checks to be available