Refactor our integration of LFSC (#6201)

This PR further decouples LFSC from the remaining build system, but makes it more convenient to use at the same time.
The contrib/get-lfsc-checker script is now completely standalone and installs LFSC and the necessary signatures to deps/, as well as wrapper scripts to conveniently run lfscc from there and directly check cvc4 proofs.
The goal would be to automatically use LFSC in our regressions as well.

diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake
index 00a7a7d1810509006e6fb9803c4f2199786494e5..03b96d18681e4616dd9b46732ebedfe98dcc5ecf 100644 (file)
--- a/cmake/FindLFSC.cmake
+++ b/cmake/FindLFSC.cmake
@@ -13,17 +13,25 @@
 # LFSC_INCLUDE_DIR - the LFSC include directory
 # LFSC_LIBRARIES - Libraries needed to use LFSC
 
-find_program(LFSC_BINARY NAMES lfscc)
-find_path(LFSC_INCLUDE_DIR NAMES lfscc.h)
-find_library(LFSC_LIBRARIES NAMES lfscc)
+find_program(LFSC_BINARY
+    NAMES lfscc
+    PATHS ${CMAKE_SOURCE_DIR}/deps/bin
+)
+find_path(LFSC_INCLUDE_DIR
+    NAMES lfscc.h
+    PATHS ${CMAKE_SOURCE_DIR}/deps/include
+)
+find_library(LFSC_LIBRARIES
+    NAMES lfscc
+    PATHS ${CMAKE_SOURCE_DIR}/deps/lib
+)
 
 include(FindPackageHandleStandardArgs)
 find_package_handle_standard_args(LFSC
-  DEFAULT_MSG
-  LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES)
+    QUIET
+    LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES)
 
 mark_as_advanced(LFSC_BINARY LFSC_INCLUDE_DIR LFSC_LIBRARIES)
 if(LFSC_FOUND)
-  message(STATUS "Found LFSC include dir: ${LFSC_INCLUDE_DIR}")
-  message(STATUS "Found LFSC libs: ${LFSC_LIBRARIES}")
+  message(STATUS "Found LFSC: ${LFSC_BINARY}")
 endif()

diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index 01a49127b6da814f5515ac819e43af3e0f361432..45ae432f6d096702ccc9ffc92c4dd8f80bfabf23 100755 (executable)
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -1,18 +1,115 @@
 #!/usr/bin/env bash
-#
-source "$(dirname "$0")/get-script-header.sh"
 
-LFSC_DIR="$DEPS_DIR/lfsc-checker"
-version="61ef1dc55d2bc909656f905699b28c99ddcfc518"
+# utility function to download a file
+function download {
+  if [ -x "$(command -v wget)" ]; then
+    wget -c -O "$2" "$1"
+  elif [ -x "$(command -v curl)" ]; then
+    curl -L "$1" >"$2"
+  else
+    echo "Can't figure out how to download from web.  Please install wget or curl." >&2
+    exit 1
+  fi
+}
 
-setup_dep "https://github.com/CVC4/LFSC/archive/$version.tar.gz" "$LFSC_DIR"
-cd "$LFSC_DIR"
+CVC_DIR=$(dirname $(dirname "$0"))
+mkdir -p $CVC_DIR/deps
+pushd $CVC_DIR/deps
 
-mkdir build
-cd build
-cmake -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" ..
-make install -j$(nproc)
+BASE_DIR=`pwd`
+mkdir -p $BASE_DIR/tmp/
 
-echo
-echo ===================== Now configure CVC4 with =====================
-echo ./configure.sh --lfsc
+##### LFSC
+LFSC_DIR="$BASE_DIR/lfsc-checker"
+mkdir -p $LFSC_DIR
+
+# download and unpack LFSC
+version="15f53d6feb84e4ddb41deaf2b5630f5c1303b06d"
+download "https://github.com/CVC4/LFSC/archive/$version.tar.gz" $BASE_DIR/tmp/lfsc.tgz
+tar --strip 1 -xzf $BASE_DIR/tmp/lfsc.tgz -C $LFSC_DIR
+
+# build and install LFSC
+pushd $LFSC_DIR
+mkdir -p build && cd build
+cmake -DCMAKE_INSTALL_PREFIX="$BASE_DIR" ..
+make install
+popd
+
+##### signatures
+SIG_DIR="$BASE_DIR/lfsc-signatures"
+mkdir -p $SIG_DIR
+
+# download and unpack signatures
+sig_version="5d72dafd48aded21fd717ef77321e1c88f732d28"
+download "https://github.com/CVC4/signatures/archive/$sig_version.tar.gz" $BASE_DIR/tmp/signatures.tgz
+tar --strip 1 -xzf $BASE_DIR/tmp/signatures.tgz -C $SIG_DIR
+
+# install signatures and scripts
+mkdir -p $BASE_DIR/share/lfsc
+cp -r $SIG_DIR/lfsc/new/signatures $BASE_DIR/share/lfsc
+
+# based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen_and_check.sh
+cat << EOF > $BASE_DIR/bin/cvc4-lfsc-check.sh
+#!/bin/bash
+
+echo "=== Generate proof: \$@" 
+$BASE_DIR/bin/cvc4-proof.sh \$@ > proof.plf
+
+echo "=== Check proof with LFSC" 
+$BASE_DIR/bin/lfsc-check.sh proof.plf
+EOF
+chmod +x $BASE_DIR/bin/cvc4-lfsc-check.sh
+
+# based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen.sh
+cat << EOF > $BASE_DIR/bin/cvc4-proof.sh
+#!/bin/bash
+
+# call cvc4 and remove the first line of the output (should be "unsat")
+\$@ --dump-proofs --proof-format=lfsc | tail -n +2
+EOF
+chmod +x $BASE_DIR/bin/cvc4-proof.sh
+
+# based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/lfsc_check.sh
+cat << EOF > $BASE_DIR/bin/lfsc-check.sh
+#!/bin/bash
+
+cat \$@ | grep WARNING
+CHECK=\$(cat \$@ | grep check)
+[ -z "\$CHECK" ] && echo "; WARNING: Empty proof!!!"
+
+SIG_DIR=$BASE_DIR/share/lfsc/signatures
+SIGS="\$SIG_DIR/core_defs.plf \\
+    \$SIG_DIR/util_defs.plf \\
+    \$SIG_DIR/theory_def.plf \\
+    \$SIG_DIR/type_checking_programs.plf \\
+    \$SIG_DIR/nary_programs.plf \\
+    \$SIG_DIR/boolean_programs.plf \\
+    \$SIG_DIR/boolean_rules.plf \\
+    \$SIG_DIR/cnf_rules.plf \\
+    \$SIG_DIR/equality_rules.plf \\
+    \$SIG_DIR/arith_programs.plf \\
+    \$SIG_DIR/arith_rules.plf \\
+    \$SIG_DIR/strings_programs.plf \\
+    \$SIG_DIR/strings_rules.plf \\
+    \$SIG_DIR/quantifiers_rules.plf"
+$BASE_DIR/bin/lfscc \$SIGS \$@ >& lfsc.out
+
+# recover macros for applications of arity 1,2,3, and simplify builtin syntax for constants
+#sed -i.orig 's/(f_ite [^ \)]*)/f_ite/g' lfsc.out
+sed -i.orig 's/(\\ [^ ]* (\\ [^ ]* (\\ [^ ]* (apply (apply (apply f_\([^ ]*\) [^ ]*) [^ ]*) [^ ]*))))/\1/g; s/(\\ [^ ]* (\\ [^ ]* (apply (apply f_\([^ ]*\) [^ ]*) [^ ]*)))/\1/g; s/(\\ [^ ]* (apply f_\([^ ]*\) [^ ]*))/\1/g; s/(var \([^ ]*\) [^ \)]*)/var_\1/g; s/(int \([^ \)]*\))/\1/g; s/emptystr/""/g; s/int\.//g' lfsc.out
+
+cat lfsc.out
+rm lfsc.out
+EOF
+chmod +x $BASE_DIR/bin/lfsc-check.sh
+
+popd
+
+echo ""
+echo "========== How to use LFSC =========="
+echo "Generate a LFSC proof with CVC4:"
+echo "  $CVC_DIR/deps/bin/cvc4-proof.sh cvc4 <options> <input file>"
+echo "Check a generated proof:"
+echo "  $CVC_DIR/deps/bin/lfsc-check.sh <proof file>"
+echo "Run CVC4 and check the generated proof:"
+echo "  $CVC_DIR/deps/bin/cvc4-lfsc-check.sh cvc4 <options> <input file>"

diff --git a/contrib/lfsc_lsan.supp b/contrib/lfsc_lsan.supp
deleted file mode 100644 (file)
index 63022a8..0000000
--- a/contrib/lfsc_lsan.supp
+++ /dev/null
@@ -1,8 +0,0 @@
-# LSAN suppressions for memory leaks in LFSC.
-#
-# To use this file, add LSAN_OPTIONS to the commandline invocation.
-#   LSAN_OPTIONS=suppressions=contrib/lfsc_lsan.supp ./build/bin/cvc4 ...
-# For more information on the leak sanitizer in ASAN, see
-# https://github.com/google/sanitizers/wiki/AddressSanitizerLeakSanitizer
-leak:CVC4::CnfProof::pushCurrentDefinition
-