do_SRPM.sh: Rebase to newer upstream version

* Add support for LLVM 11 on F33+
* Link with LLVM dynamically

Author: lzaoral

do_SRPM.sh

@@ -3,14 +3,14 @@
 set -e
 
 # upstream revision to checkout
-SYMBIOTIC_REV="svcomp19-506-g630bd29"
+SYMBIOTIC_REV="svcomp19-528-g0db3c4a"
 
 rm -rf srpm
 mkdir srpm
 cd srpm
 
 # clone symbiotic git repo, including its submodules
-git clone --recurse-submodules https://github.com/staticafi/symbiotic.git
+git clone --depth 1 --recurse-submodules https://github.com/staticafi/symbiotic.git
 
 pushd symbiotic > /dev/null
 
@@ -58,29 +58,34 @@ tar -Jcf "symbiotic-$VER.tar.xz" "symbiotic-$VER"
 cat > symbiotic.spec << EOF
 Name:       $PKG
 Version:    $VER
-Release:    5%{?dist}
+Release:    1%{?dist}
 Summary:    Tool for analysis of sequential computer programs written in C
-License:    Free
+License:    MIT
 URL:        https://github.com/staticafi/%{name}
+
 Source0:    %{name}-%{version}.tar.xz
 Source1:    symbiotic2cs.py
 Source2:    csexec-symbiotic.sh
+
 Patch0:     build.patch
 Patch1:     hotfix.patch
+Patch2:     llvm-dynamic-link.patch
+%if 0%{?fedora} > 32
+Patch3:     llvm-11.patch
+%endif
 
-BuildRequires: gcc
-BuildRequires: cmake
-BuildRequires: jsoncpp-devel
-BuildRequires: llvm-devel
-BuildRequires: llvm-static
+BuildRequires: gcc-c++
 BuildRequires: clang
+BuildRequires: cmake
 BuildRequires: glibc-devel
 BuildRequires: glibc-devel(x86-32)
+BuildRequires: jsoncpp-devel
+BuildRequires: llvm-devel
 BuildRequires: ncurses-devel
 BuildRequires: python3
 BuildRequires: sqlite-devel
 BuildRequires: z3-devel
-BuildRequires: zlib-static
+BuildRequires: zlib-devel
 
 Requires: clang
 Requires: llvm
@@ -117,6 +122,6 @@ ln -sf /opt/symbiotic/bin/symbiotic %{buildroot}%{_bindir}/symbiotic
 %{_bindir}/csexec-symbiotic
 EOF
 
-cp ../{symbiotic2cs.py,csexec-symbiotic.sh,build.patch,hotfix.patch} .
+cp ../{symbiotic2cs.py,csexec-symbiotic.sh,{build,hotfix,llvm-{11,dynamic-link}}.patch} .
 
 rpmbuild -bs symbiotic.spec --define "_sourcedir $PWD" --define "_srcrpmdir $PWD"

hotfix.patch

@@ -11,198 +11,7 @@
  # copy the jsoncpp.cpp file into parent's src/ folder
  cp dist/jsoncpp.cpp ../src/
 
-# lzaoral/fix-custom-llvm
-diff --git a/system-build.sh b/system-build.sh
-index cb4ecff..b83932a 100755
---- a/system-build.sh
-+++ b/system-build.sh
-@@ -246,21 +246,22 @@ elif [ $LLVM_MAJOR_VERSION -ge 3 -a $LLVM_MINOR_VERSION -ge 9 ]; then
- 	LLVM_CMAKE_CONFIG_DIR=lib/cmake/llvm
- fi
- 
-+LLVM_BIN_DIR=$("$LLVM_CONFIG" --bindir)
-+
- mkdir -p $LLVM_PREFIX/bin
- for T in $LLVM_TOOLS; do
--	TOOL=$(which $T || true)
--
--	# always avoid making copy of a ccache executable (symlink's target)
--	if [[ "$TOOL" =~ "ccache" ]]; then
--		TOOL="/usr/bin/$T"
-+	TOOL="$LLVM_BIN_DIR/$T"
-+	if [ ! -x "${TOOL}" ]; then
-+		exitmsg "Cannot find working $T binary".
- 	fi
- 
--	if [ -z "${TOOL}" -o ! -x "${TOOL}" ]; then
--		exitmsg "Cannot find working $T binary"
-+	TOOL_VERSION=$("$TOOL" --version)
-+	if [[ ! "$TOOL_VERSION" =~ "$LLVM_VERSION" ]]; then
-+		exitmsg "$T has wrong version. Expected: $LLVM_VERSION Found: $TOOL_VERSION"
- 	fi
- 
- 	# copy the binaries only with full-archive option
--	if [ "$FULL_ARCHIVE" = "no" ] || readlink -- "${TOOL}" > /dev/null; then
-+	if [ "$FULL_ARCHIVE" = "no" ] ; then
- 		ln -fs "${TOOL}" "${LLVM_PREFIX}/bin"
- 	else
- 		cp -rf "${TOOL}" "${LLVM_PREFIX}/bin"
-
-diff --git a/system-build.sh b/system-build.sh
-index b83932a..dbe983f 100755
---- a/system-build.sh
-+++ b/system-build.sh
-@@ -269,7 +269,11 @@ for T in $LLVM_TOOLS; do
- done
- 
- mkdir -p $LLVM_PREFIX/lib
--ln -sf $(dirname $(which clang))/../lib/clang/ $LLVM_PREFIX/lib/
-+CLANG_LIBS=$("$LLVM_CONFIG" --libdir)/clang/
-+if [ ! -d "$CLANG_LIBS" ]; then
-+    exitmsg "Invalid path to clang libraries."
-+fi
-+ln -sf "$CLANG_LIBS" "$LLVM_PREFIX/lib/"
- 
- ######################################################################
- #   dg
-
-diff --git a/scripts/precompile_bitcode_files.sh b/scripts/precompile_bitcode_files.sh
-index c662433..6dd9824 100755
---- a/scripts/precompile_bitcode_files.sh
-+++ b/scripts/precompile_bitcode_files.sh
-@@ -14,7 +14,7 @@ ORIG_CPPFLAGS="$CPPFLAGS"
- for LLVM in $PREFIX/llvm-*; do
- 	CLANG=$LLVM/bin/clang
- 	LLVM_VERSION=${LLVM#*llvm-*}
--	INCLUDE_DIR="llvm-${LLVM_VERSION}/build/lib/clang/${LLVM_VERSION}/include/"
-+	INCLUDE_DIR="$LLVM/lib/clang/${LLVM_VERSION}/include/"
- 	CPPFLAGS="-I ${INCLUDE_DIR} $ORIG_CPPFLAGS"
- 	for F in `find $INSTR/instrumentations/ -name '*.c'`; do
- 		NAME=`basename $F`
-@@ -33,7 +33,7 @@ done
- for LLVM in $PREFIX/llvm-*; do
- 	CLANG=$LLVM/bin/clang
- 	LLVM_VERSION=${LLVM#*llvm-*}
--	INCLUDE_DIR="llvm-${LLVM_VERSION}/build/lib/clang/${LLVM_VERSION}/include/"
-+	INCLUDE_DIR="$LLVM/lib/clang/${LLVM_VERSION}/include/"
- 	CPPFLAGS="-I ${INCLUDE_DIR} -Iinclude/ $ORIG_CPPFLAGS"
- 	for F in `find $LIBS -name '*.c'`; do
- 		NAME=`basename $F`
-
-diff --git a/scripts/build-utils.sh b/scripts/build-utils.sh
-index 3a43d55..8b6feed 100644
---- a/scripts/build-utils.sh
-+++ b/scripts/build-utils.sh
-@@ -1,4 +1,4 @@
--#!/bin/sh
-+#!/bin/bash
- 
- set -x
- 
-@@ -57,6 +57,20 @@ build()
- 	return 0
- }
- 
-+check_llvm_tool()
-+{
-+	TOOL_PATH="$1"
-+	TOOL_NAME="$(dirname "$1")"
-+	if [ ! -x "$TOOL_PATH" ]; then
-+		exitmsg "Cannot find working $TOOL_NAME binary".
-+	fi
-+
-+	TOOL_VERSION=$("$TOOL_PATH" --version)
-+	if [[ ! "$TOOL_VERSION" =~ "$LLVM_VERSION" ]]; then
-+		exitmsg "$TOOL_NAME has wrong version. Expected: $LLVM_VERSION Found: $TOOL_VERSION"
-+	fi
-+}
-+
- git_clone_or_pull()
- {
- 
-diff --git a/system-build.sh b/system-build.sh
-index dbe983f..8748120 100755
---- a/system-build.sh
-+++ b/system-build.sh
-@@ -250,28 +250,21 @@ LLVM_BIN_DIR=$("$LLVM_CONFIG" --bindir)
- 
- mkdir -p $LLVM_PREFIX/bin
- for T in $LLVM_TOOLS; do
--	TOOL="$LLVM_BIN_DIR/$T"
--	if [ ! -x "${TOOL}" ]; then
--		exitmsg "Cannot find working $T binary".
--	fi
--
--	TOOL_VERSION=$("$TOOL" --version)
--	if [[ ! "$TOOL_VERSION" =~ "$LLVM_VERSION" ]]; then
--		exitmsg "$T has wrong version. Expected: $LLVM_VERSION Found: $TOOL_VERSION"
--	fi
-+	check_llvm_tool "$LLVM_BIN_DIR/$T"
- 
- 	# copy the binaries only with full-archive option
- 	if [ "$FULL_ARCHIVE" = "no" ] ; then
--		ln -fs "${TOOL}" "${LLVM_PREFIX}/bin"
--	else
--		cp -rf "${TOOL}" "${LLVM_PREFIX}/bin"
-+		ln -fs "$LLVM_BIN_DIR/$T" "$LLVM_PREFIX/bin"
-+		continue
- 	fi
-+
-+	cp -L "$LLVM_BIN_DIR/$T" "$LLVM_PREFIX/bin"
- done
- 
- mkdir -p $LLVM_PREFIX/lib
- CLANG_LIBS=$("$LLVM_CONFIG" --libdir)/clang/
- if [ ! -d "$CLANG_LIBS" ]; then
--    exitmsg "Invalid path to clang libraries."
-+	exitmsg "Invalid path to clang libraries."
- fi
- ln -sf "$CLANG_LIBS" "$LLVM_PREFIX/lib/"
- 
-diff --git a/scripts/build-utils.sh b/scripts/build-utils.sh
-index 8b6feed..1cfdbd4 100644
---- a/scripts/build-utils.sh
-+++ b/scripts/build-utils.sh
-@@ -60,7 +60,7 @@ build()
- check_llvm_tool()
- {
- 	TOOL_PATH="$1"
--	TOOL_NAME="$(dirname "$1")"
-+	TOOL_NAME="$(basename "$1")"
- 	if [ ! -x "$TOOL_PATH" ]; then
- 		exitmsg "Cannot find working $TOOL_NAME binary".
- 	fi
-diff --git a/system-build.sh b/system-build.sh
-index 8748120..9b5a515 100755
---- a/system-build.sh
-+++ b/system-build.sh
-@@ -239,13 +239,6 @@ export LLVM_PREFIX="$PREFIX/llvm-$LLVM_VERSION"
- LLVM_MAJOR_VERSION="${LLVM_VERSION%%\.*}"
- LLVM_MINOR_VERSION=${LLVM_VERSION#*\.}
- LLVM_MINOR_VERSION="${LLVM_MINOR_VERSION%\.*}"
--LLVM_CMAKE_CONFIG_DIR=share/llvm/cmake
--if [ $LLVM_MAJOR_VERSION -gt 3 ]; then
--	LLVM_CMAKE_CONFIG_DIR=lib/cmake/llvm
--elif [ $LLVM_MAJOR_VERSION -ge 3 -a $LLVM_MINOR_VERSION -ge 9 ]; then
--	LLVM_CMAKE_CONFIG_DIR=lib/cmake/llvm
--fi
--
- LLVM_BIN_DIR=$("$LLVM_CONFIG" --bindir)
- 
- mkdir -p $LLVM_PREFIX/bin
-@@ -350,7 +343,9 @@ if [ $FROM -le 6 -a "$BUILD_PREDATOR" = "yes" ]; then
- 	pushd predator-${LLVM_VERSION}
- 
- 	if [ ! -d CMakeFiles ]; then
--	        CXX=clang++ ./switch-host-llvm.sh /usr/${LLVM_CMAKE_CONFIG_DIR}
-+		check_llvm_tool "$LLVM_BIN_DIR/clang++"
-+		CXX="$LLVM_BIN_DIR/clang++" ./switch-host-llvm.sh \
-+			"$("$LLVM_CONFIG" --cmakedir)"
- 	fi
- 
-        	build || exit 1
-
-# build with default Fedora build flags
+# Build with default Fedora build flags
 diff --git a/scripts/build-utils.sh b/scripts/build-utils.sh
 index 3a43d55..60597d0 100644
 --- a/scripts/build-utils.sh
@@ -268,130 +77,3 @@ index c662433..e84e123 100755
  		FILES="$FILES ${LLVM#install/}/lib32/$OUT"
  	done
  done
-diff --git a/transforms/CMakeLists.txt b/transforms/CMakeLists.txt
-index 4f71902..2e267f7 100644
---- a/transforms/CMakeLists.txt
-+++ b/transforms/CMakeLists.txt
-@@ -9,13 +9,6 @@ message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}")
- list(APPEND CMAKE_MODULE_PATH "${LLVM_DIR}")
- list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
- 
--if (${LLVM_PACKAGE_VERSION} VERSION_LESS_EQUAL "3.7")
--  # needed for LLVM 3.7
--  set(LLVM_RUNTIME_OUTPUT_INTDIR ${CMAKE_BINARY_DIR}/${CMAKE_CFG_INTDIR})
--  set(LLVM_LIBRARY_OUTPUT_INTDIR ${CMAKE_BINARY_DIR}/${CMAKE_CFG_INTDIR})
--  include(HandleLLVMOptions)
--endif()
--
- include(AddLLVM)
- 
- # explicitly add -std=c++11 (c++14), some cmake versions
-@@ -57,11 +50,6 @@ include(GNUInstallDirs)
- message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"")
- message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"")
- 
--# We need all the symbols with dynamic libs. With static libs, we get errors.
--if (BUILD_SHARED_LIBS)
--  set(LLVM_LINK_COMPONENTS analysis core support)
--endif()
--
- add_library(LLVMsbt MODULE "BreakCritLoops.cpp"
-                            "BreakInfiniteLoops.cpp"
-                            "CheckModule.cpp"
-@@ -92,6 +80,7 @@ add_library(LLVMsbt MODULE "BreakCritLoops.cpp"
- 
- # remove lib prefix for compatibility with older releases
- set_target_properties(LLVMsbt PROPERTIES PREFIX "")
-+target_link_libraries(LLVMsbt LLVM)
- 
- install(TARGETS LLVMsbt
-         LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR})
-diff --git a/transforms/InternalizeGlobals.cpp b/transforms/InternalizeGlobals.cpp
-index 3c6a3db..3d7c5a7 100644
---- a/transforms/InternalizeGlobals.cpp
-+++ b/transforms/InternalizeGlobals.cpp
-@@ -64,9 +64,8 @@ bool InternalizeGlobals::initializeExternalGlobals(Module& M) {
-     // GV is a pointer to some memory, we want the size of the memory
-     Type *Ty = GV->getType()->getContainedType(0);
-     if (!Ty->isSized()) {
--      GV->dump();
--      llvm::errs() << "ERROR: failed making global variable symbolic "
--                      "(type is unsized)\n";
-+      llvm::errs() << GV << "\nERROR: failed making global variable symbolic "
-+                            "(type is unsized)\n";
-       continue;
-     }
- 
-@@ -86,9 +85,8 @@ bool InternalizeGlobals::initializeExternalGlobals(Module& M) {
-     // point to and set it to symbolic at the beggining of main
-     if (Ty->isPointerTy()) {
-         if (!Ty->getContainedType(0)->isSized()) {
--            GV->dump();
--            llvm::errs() << "ERROR: failed making global variable symbolic "
--                            "(referenced type is unsized)\n";
-+            llvm::errs() << GV << "\nERROR: failed making global variable "
-+                                  "symbolic (referenced type is unsized)\n";
-             continue;
-         }
- 
-# Add --argv option
-diff --git a/lib/symbioticpy/symbiotic/options.py b/lib/symbioticpy/symbiotic/options.py
-index 4289a55..1d62f39 100644
---- a/lib/symbioticpy/symbiotic/options.py
-+++ b/lib/symbioticpy/symbiotic/options.py
-@@ -52,6 +52,7 @@ class SymbioticOptions(object):
-         self.witness_output = '{0}/witness.graphml'.format(os.getcwd())
-         self.testsuite_output = '{0}/test-suite'.format(os.getcwd())
-         self.source_is_bc = False
-+        self.argv = []
-         self.optlevel = ["before-O3", "after-O3"]
-         self.slicer_pta = 'fi'
-         self.memsafety_config_file = None
-@@ -205,7 +206,7 @@ def parse_command_line():
-                                     'instrumentation-timeout=', 'version', 'help',
-                                     'no-verification', 'output=', 'witness=', 'bc',
-                                     'optimize=', 'malloc-never-fails',
--                                    'pta=', 'no-link=',
-+                                    'pta=', 'no-link=', 'argv=',
-                                     'cflags=', 'cppflags=', 'link=', 'executable-witness',
-                                     'verifier=','target=', 'require-slicer',
-                                     'no-link-undefined', 'repeat-slicing=',
-@@ -246,6 +247,8 @@ def parse_command_line():
-         elif opt == '--version-short':
-             print_shortest_vers()
-             sys.exit(0)
-+        elif opt == '--argv':
-+            options.argv = arg.split(',')
-         elif opt == '--version':
-             print_versions()
-             sys.exit(0)
-@@ -475,6 +478,7 @@ where OPTS can be following:
-     --cflags=flags
-     --cppflags=flags          Append extra CFLAGS and CPPFLAGS to use while compiling,
-                               the environment CFLAGS and CPPFLAGS are used too
-+    --argv=args               Arguments for the main function of the verified bitcode
-     --slicer-params=STR       Pass parameters directly to slicer
-     --slicer-cmd=STR          Command to run slicer, default: sbt-slicer
-     --verifier-params=STR     Pass parameters directly to the verifier
-diff --git a/lib/symbioticpy/symbiotic/targets/klee.py b/lib/symbioticpy/symbiotic/targets/klee.py
-index 3e52eed..51b6577 100644
---- a/lib/symbioticpy/symbiotic/targets/klee.py
-+++ b/lib/symbioticpy/symbiotic/targets/klee.py
-@@ -125,7 +125,7 @@ class KleeToolFullInstrumentation(KleeBase):
-         if self._options.exit_on_error:
-             cmd.append('-exit-on-error-type=Assert')
-
--        return cmd + options + tasks
-+        return cmd + options + tasks + self._options.argv
-
-     def _parse_klee_output_line(self, line):
-         for (key, pattern) in self._patterns:
-@@ -335,7 +335,7 @@ class SymbioticTool(KleeBase):
-         # but we may remove this switch during debugging)
-         cmd.append('-output-source=false')
-
--        return cmd + options + tasks
-+        return cmd + options + tasks + self._options.argv
-
-     def _parse_klee_output_line(self, line):
-         opts = self._options