Use versioned LLVM toolchain binaries

This allows SMACK to not interfere with existing installed compilers.

Author: shaobo-he

bin/build.sh

@@ -278,11 +278,6 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
     sudo apt-get update
 
     sudo apt-get install -y ${DEPENDENCIES}
-    sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 30
-    sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_SHORT_VERSION} 30
-    sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-${LLVM_SHORT_VERSION} 30
-    sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-${LLVM_SHORT_VERSION} 30
-    sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-${LLVM_SHORT_VERSION} 30
     ;;
 
   *)
@@ -464,7 +459,6 @@ fi
 if [ ${INSTALL_DEV_DEPENDENCIES} -eq 1 ] ; then
   sudo apt-get install -y python3-pip clang-format-${LLVM_SHORT_VERSION}
   sudo pip3 install -U flake8
-  sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-${LLVM_SHORT_VERSION} 30
   if [ "${GITHUB_ACTIONS}" = "true" ] ; then
     exit 0
   fi
@@ -480,7 +474,7 @@ if [ ${BUILD_SMACK} -eq 1 ] ; then
 
   mkdir -p ${SMACK_DIR}/build
   cd ${SMACK_DIR}/build
-  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
+  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
   ninja
 
   if [ -n "${CMAKE_INSTALL_PREFIX}" ] ; then

format/run-clang-format.py

@@ -203,12 +203,19 @@ def print_trouble(prog, message, use_colors):
 
 
 def main():
+
+    with open(os.path.join(os.path.dirname(os.path.dirname(
+        os.path.abspath(__file__))), 'bin', 'versions'), 'r') as f:
+        for line in f.readlines():
+            if line.startswith('LLVM_SHORT_VERSION='):
+                llvm_version = line.strip()[len('LLVM_SHORT_VERSION='):].replace('"', '')
+
     parser = argparse.ArgumentParser(description=__doc__)
     parser.add_argument(
         '--clang-format-executable',
         metavar='EXECUTABLE',
-        help='path to the clang-format executable',
-        default='clang-format')
+        help='path to the clang-format executable (default: %(default)s)',
+        default='clang-format-' + llvm_version)
     parser.add_argument(
         '--extensions',
         help='comma separated list of file extensions (default: {})'.format(

share/smack/frontend.py

@@ -4,6 +4,7 @@
 import json
 from .utils import temporary_file, try_command, temporary_directory
 from .versions import RUST_VERSION
+from .versions import LLVM_SHORT_VERSION
 
 # Needed for cargo operations
 try:
@@ -85,8 +86,19 @@ def smack_lib():
     return os.path.join(smack_root(), 'share', 'smack', 'lib')
 
 
+def llvm_exact_bin(name):
+    return name + '-' + LLVM_SHORT_VERSION
+
+
 def default_clang_compile_command(args, lib=False):
-    cmd = ['clang', '-c', '-emit-llvm', '-O0', '-g', '-gcolumn-info']
+    cmd = [
+           llvm_exact_bin('clang'),
+           '-c',
+           '-emit-llvm',
+           '-O0',
+           '-g',
+           '-gcolumn-info'
+          ]
     # Starting from LLVM 5.0, we need the following two options
     # in order to enable optimization passes.
     # See: https://stackoverflow.com/a/46753969.
@@ -165,7 +177,7 @@ def fortran_compile_to_bc(input_file, compile_command, args):
          '-i',
          's/i32 1, !\"Debug Info Version\"/i32 2, !\"Debug Info Version\"/g',
          ll])
-    try_command(['llvm-as', ll])
+    try_command([llvm_exact_bin('llvm-as'), ll])
     try_command(['rm', ll])
     bc = '.'.join(ll.split('.')[:-1] + ['bc'])
     return bc
@@ -189,7 +201,7 @@ def clang_frontend(input_file, args):
 def clang_plusplus_frontend(input_file, args):
     """Generate LLVM IR from C++ language source(s)."""
     compile_command = default_clang_compile_command(args)
-    compile_command[0] = 'clang++'
+    compile_command[0] = llvm_exact_bin('clang++')
     return compile_to_bc(input_file, compile_command, args)
 
 
@@ -263,9 +275,17 @@ def json_compilation_database_frontend(input_file, args):
             if 'objects' in cc:
                 # TODO what to do when there are multiple linkings?
                 bit_codes = [re.sub('[.]o$', '.bc', f) for f in cc['objects']]
-                try_command(['llvm-link', '-o', args.bc_file] + bit_codes)
-                try_command(['llvm-link', '-o', args.linked_bc_file,
-                             args.bc_file] + default_build_libs(args))
+                try_command([
+                             llvm_exact_bin('llvm-link'),
+                             '-o',
+                             args.bc_file
+                            ] + bit_codes)
+                try_command([
+                             llvm_exact_bin('llvm-link'),
+                             '-o',
+                             args.linked_bc_file,
+                             args.bc_file
+                            ] + default_build_libs(args))
 
             else:
                 command = cc['command']
@@ -316,7 +336,7 @@ def cargo_frontend(input_file, args):
             os.path.basename(input_file))[0],
         '.bc',
         args)
-    try_command(['llvm-link'] + bcs + ['-o', bc_file])
+    try_command([llvm_exact_bin('llvm-link')] + bcs + ['-o', bc_file])
     return bc_file
 
 
@@ -410,7 +430,7 @@ def cplusplus_build_libs(args):
     libs = ['smack.cpp']
 
     compile_command = default_clang_compile_command(args, True)
-    compile_command[0] = 'clang++'
+    compile_command[0] = llvm_exact_bin('clang++')
 
     for c in [os.path.join(smack_lib(), c) for c in libs]:
         bc = compile_to_bc(c, compile_command, args)
@@ -443,8 +463,8 @@ def link_bc_files(bitcodes, libs, args):
     for build_lib in libs:
         smack_libs += build_lib(args)
 
-    try_command(['llvm-link', '-o', args.bc_file] + bitcodes)
-    try_command(['llvm-link', '-o', args.linked_bc_file,
+    try_command([llvm_exact_bin('llvm-link'), '-o', args.bc_file] + bitcodes)
+    try_command([llvm_exact_bin('llvm-link'), '-o', args.linked_bc_file,
                  args.bc_file] + smack_libs)
 
     # import here to avoid a circular import