Enable RMC on Ubuntu 18.04 rust-lang#393 (rust-lang#404)

Add support to Ubuntu 18.04 (rust-lang#393)

Issue: Our python scripts use python 3.8+ while ubuntu 18.04 defaults
       to python 3.6.

Changes:
 * Change our scripts to use constructs available in older python versions.
 * Modify workflows file to add ubuntu-18.04.
 * Make ubuntu scripts generic.
 * Change copyright check script to ignore directories and symbolic links to directories.

Author: celinval

.github/workflows/rmc.yml

@@ -8,7 +8,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-10.15, ubuntu-20.04]
+        os: [macos-10.15, ubuntu-18.04, ubuntu-20.04]
     steps:
       - name: Checkout RMC
         uses: actions/checkout@v2
@@ -20,7 +20,7 @@ jobs:
 
       - name: Install CBMC
         run: ./scripts/setup/${{ matrix.os }}/install_cbmc.sh
-      
+
       - name: Install cbmc-viewer
         run: ./scripts/setup/install_viewer.sh 2.6
 

scripts/check-cbmc-version.py

@@ -6,6 +6,7 @@
 import re
 import sys
 import subprocess
+from subprocess import PIPE
 
 
 EXIT_CODE_SUCCESS = 0
@@ -16,8 +17,8 @@
 def cbmc_version():
     cmd = ["cbmc", "--version"]
     try:
-        version = subprocess.run(cmd,
-                                 capture_output=True, text=True, check=True)
+        version = subprocess.run(cmd, stdout=PIPE, stderr=PIPE, check=True,
+                universal_newlines=True)
     except (OSError, subprocess.SubprocessError) as error:
         print(error)
         print(f"Can't run command '{' '.join(cmd)}'")

scripts/check-cbmc-viewer-version.py

@@ -6,6 +6,7 @@
 import re
 import sys
 import subprocess
+from subprocess import PIPE
 
 
 EXIT_CODE_SUCCESS = 0
@@ -16,8 +17,8 @@
 def cbmc_viewer_version():
     cmd = ["cbmc-viewer", "--version"]
     try:
-        version = subprocess.run(cmd,
-                                 capture_output=True, text=True, check=True)
+        version = subprocess.run(cmd, stdout=PIPE, stderr=PIPE, check=True,
+                universal_newlines=True)
     except (OSError, subprocess.SubprocessError) as error:
         print(error)
         print(f"Can't run command '{' '.join(cmd)}'")

scripts/ci/copyright_check.py

@@ -3,8 +3,13 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 import re
 import sys
+import os.path as path
 
 def copyright_check(filename):
+    # Only check regular files (skip symbolic link to directories)
+    if not path.isfile(filename):
+        return True
+
     fo = open(filename)
     lines = fo.readlines()
 

scripts/rmc_flags.py

@@ -8,6 +8,12 @@
 # Taken from https://github.com/python/cpython/blob/3.9/Lib/argparse.py#L858
 # Cannot use `BooleanOptionalAction` with Python 3.8
 class BooleanOptionalAction(argparse.Action):
+    """ Implements argparse.BooleanOptionalAction introduced on Python 3.9
+
+        This allows us to define an action as well as its negation to control a
+        boolean option. For example, --default-checks and --no-default-checks
+        options to control the same boolean property.
+    """
     def __init__(self,
                  option_strings,
                  dest,
@@ -47,6 +53,33 @@ def __call__(self, parser, namespace, values, option_string=None):
     def format_usage(self):
         return ' | '.join(self.option_strings)
 
+class ExtendAction(argparse.Action):
+    """ Implements the "extend" option added on Python 3.8.
+
+        Extend combines in one list all the arguments provided using the
+        same option. For example, --c-lib <libA> --c-lib <libB> <libC> will
+        generate a list [<libA>, <libB>, <libC>].
+    """
+    def __init__(self,
+                 option_strings,
+                 dest,
+                 default=[],
+                 **kwargs):
+
+        if type(default) is not list:
+            raise ValueError('default value for ExtendAction must be a list')
+
+        super().__init__(
+            option_strings=option_strings,
+            dest=dest,
+            default=default,
+            **kwargs)
+
+    def __call__(self, parser, namespace, values, option_string=None):
+        items = getattr(namespace, self.dest, [])
+        items.extend(values)
+        setattr(namespace, self.dest, items)
+
 # Add flags related to debugging output.
 def add_loudness_flags(make_group, add_flag, config):
     group = make_group(
@@ -62,7 +95,8 @@ def add_loudness_flags(make_group, add_flag, config):
 def add_linking_flags(make_group, add_flag, config):
     group = make_group("Linking flags",
                        "Provide information about how to link the prover for RMC.")
-    add_flag(group, "--c-lib", type=pl.Path, nargs="*", default=[], action="extend",
+    add_flag(group, "--c-lib", type=pl.Path, nargs="*", default=[],
+             action=ExtendAction,
              help="Link external C files referenced by Rust code")
     add_flag(group, "--function", default="main",
              help="Entry point for verification")

scripts/setup/ubuntu-18.04

@@ -0,0 +1 @@
+ubuntu

scripts/setup/ubuntu-20.04

@@ -0,0 +1 @@
+ubuntu

scripts/setup/ubuntu-20.04/install_cbmc.sh renamed to scripts/setup/ubuntu/install_cbmc.sh

@@ -4,9 +4,8 @@
 
 set -eu
 
-# Install CBMC 5.30.1 for Ubuntu 20.04
-
-FILE="ubuntu-20.04-cbmc-5.30.1-Linux.deb"
+UBUNTU_VERSION=$(lsb_release -rs)
+FILE="ubuntu-${UBUNTU_VERSION}-cbmc-5.30.1-Linux.deb"
 URL="https://github.com/diffblue/cbmc/releases/download/cbmc-5.30.1/$FILE"
 
 set -x

scripts/setup/ubuntu-20.04/install_deps.sh renamed to scripts/setup/ubuntu/install_deps.sh

@@ -4,6 +4,7 @@
 
 set -eu
 
+# Dependencies.
 DEPS=(
   bison
   cmake
@@ -20,19 +21,31 @@ DEPS=(
   ninja-build
   patch
   pkg-config
-  python-is-python3
   python3-pip # Default in CI, but missing in AWS AMI
   software-properties-common
   wget
   zlib1g
   zlib1g-dev
 )
 
+# Version specific dependencies.
+declare -A VERSION_DEPS
+VERSION_DEPS["20.04"]="python-is-python3"
+VERSION_DEPS["18.04"]=""
+
 set -x
 
 sudo apt-get --yes update
 sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${DEPS[@]}"
 
+UBUNTU_VERSION=$(lsb_release -rs)
+OTHER_DEPS="${VERSION_DEPS[${UBUNTU_VERSION}]:-""}"
+if [[ ! -z ${OTHER_DEPS} ]]
+then
+    # This package was added on ubuntu 20.04.
+    sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${OTHER_DEPS[@]}"
+fi
+
 # Add Python package dependencies
 PYTHON_DEPS=(
   toml # Used for parsing `cargo-rmc` config toml