git clone --recursive git@github.com:cssl-unist/patch-validator.git
cd patch-validatorThen build and run the Docker container.
docker build -t patch-validator .
docker run -it patch-validatorResults can be found in demo/*/result/result.csv.
In result.csv, the OC_subset_PC column denotes OCFP′ ⇒ PCRP′.
undecidable is conservatively treated as functionality NOT being equivalent.
libxml2-5134 only works correctly when LowFat's reverse memory layout is
disabled. In src/sanitizer/LowFat/config/lowfat-config.c, find the part marked
with the // Edit this line for libxml2-5134 comment and comment out the
#define LOWFAT_REVERSE_MEM_LAYOUT 1 line. Once the macro is undefined, the
#if falls through to the #else branch, disabling the reverse layout.
Afterwards, apply the environment variables from the repo root and rebuild
LowFat with ./build.sh from the src/sanitizer/LowFat directory.
source setup.sh
cd src/sanitizer/LowFat
./build.shThere was a bug where the KLEE code instrumentation was being inserted at the wrong location, which has now been fixed.
The coreutils-19784 patch is functionally valid. In the master's thesis,
SPIDER and SPIDER' fail to evaluate it correctly and record it as invalid, and
ExtractCompare also recorded it as invalid — but only because of this
instrumentation bug. Now that the bug is fixed, ExtractCompare — unlike SPIDER
and SPIDER' — correctly evaluates the coreutils-19784 patch as valid,
assessing the functional validity of patches more accurately.