aarch32: sync with master

(merge branch 'master' into aarch32)

Author: sauclovian-g

.dockerignore

@@ -3,6 +3,7 @@
 .DS_Store
 .cabal-sandbox
 cabal.sandbox.config
+cabal.project.local
 .ghc.environment.x86_64-darwin-*
 s2nTests
 

.github/PropertiesTest.java

@@ -18,212 +18,164 @@ extract_exe() {
   $IS_WIN || chmod +x "$2/$name"
 }
 
-retry() {
-  echo "Attempting with retry:" "$@"
-  local n=1
-  while true; do
-    if "$@"; then
-      break
-    else
-      if [[ $n -lt 3 ]]; then
-        sleep $n # don't retry immediately
-        ((n++))
-        echo "Command failed. Attempt $n/3:"
-      else
-        echo "The command has failed after $n attempts."
-        return 1
-      fi
-    fi
-  done
-}
-
 setup_dist_bins() {
   if $IS_WIN; then
-    is_exe "dist/bin" "saw" && is_exe "dist/bin" "saw-remote-api" && return
+    is_exe "dist/bin" "saw" && return
   else
-    is_exe "dist/bin" "saw" && is_exe "dist/bin" "saw-remote-api" && is_exe "dist/bin" "jss" && return
-    extract_exe "jss" "dist/bin"
+    is_exe "dist/bin" "saw" && is_exe "dist/bin" "saw-remote-api" && return
+    extract_exe "saw-remote-api" "dist/bin"
   fi
   extract_exe "saw" "dist/bin"
-  extract_exe "saw-remote-api" "dist/bin"
+  extract_exe "cryptol" "dist/bin"
   export PATH=$PWD/dist/bin:$PATH
   echo "$PWD/dist/bin" >> "$GITHUB_PATH"
   strip dist/bin/saw* || echo "Strip failed: Ignoring harmless error"
-  strip dist/bin/jss* || echo "Strip failed: Ignoring harmless error"
-}
-
-install_z3() {
-  is_exe "$BIN" "z3" && return
-
-  case "$RUNNER_OS" in
-    Linux) file="ubuntu-16.04.zip" ;;
-    macOS) file="osx-10.14.6.zip" ;;
-    Windows) file="win.zip" ;;
-  esac
-  curl -o z3.zip -sL "https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION/z3-$Z3_VERSION-x64-$file"
-
-  if $IS_WIN; then 7z x -bd z3.zip; else unzip z3.zip; fi
-  cp z3-*/bin/z3$EXT $BIN/z3$EXT
-  $IS_WIN || chmod +x $BIN/z3
-  rm z3.zip
-}
-
-install_cvc4() {
-  is_exe "$BIN" "cvc4" && return
-  version="${CVC4_VERSION#4.}" # 4.y.z -> y.z
-
-  case "$RUNNER_OS" in
-    Linux) file="x86_64-linux-opt" ;;
-    Windows) file="win64-opt.exe" ;;
-    macOS) file="macos-opt" ;;
-  esac
-  # Temporary workaround
-  if [[ "$RUNNER_OS" == "Linux" ]]; then
-    curl -o cvc4$EXT -sL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-08-18-x86_64-linux-opt"
-  else
-    curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file"
-  fi
-  $IS_WIN || chmod +x cvc4$EXT
-  mv cvc4$EXT "$BIN/cvc4$EXT"
-}
-
-install_yices() {
-  is_exe "$BIN" "yices" && return
-  ext=".tar.gz"
-  case "$RUNNER_OS" in
-    Linux) file="pc-linux-gnu-static-gmp.tar.gz" ;;
-    macOS) file="apple-darwin18.7.0-static-gmp.tar.gz" ;;
-    Windows) file="pc-mingw32-static-gmp.zip" && ext=".zip" ;;
-  esac
-  curl -o "yices$ext" -sL "https://yices.csl.sri.com/releases/$YICES_VERSION/yices-$YICES_VERSION-x86_64-$file"
-
-  if $IS_WIN; then
-    7z x -bd "yices$ext"
-    mv "yices-$YICES_VERSION"/bin/*.exe "$BIN"
-  else
-    tar -xzf "yices$ext"
-    pushd "yices-$YICES_VERSION" || exit
-    sudo ./install-yices
-    popd || exit
-  fi
-  rm -rf "yices$ext" "yices-$YICES_VERSION"
-}
-
-install_yasm() {
-  is_exe "$BIN" "yasm" && return
-  case "$RUNNER_OS" in
-    Linux) sudo apt-get update -q && sudo apt-get install -y yasm ;;
-    macOS) brew install yasm ;;
-    Windows) choco install yasm ;;
-  esac
 }
 
 build() {
   ghc_ver="$(ghc --numeric-version)"
   cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
   cabal v2-update
-  echo "allow-newer: all" >> cabal.project.local
-  pkgs=(saw saw-remote-api)
+  # Configure with --disable-documentation and --haddock-internal so
+  # that the haddock run later, if enabled, doesn't recompile the
+  # world by using those flags. (See haddock() below for discussion of
+  # why those flags are used.) We could do this only for builds where
+  # we're intending to do the haddock run, but it should have no
+  # effect otherwise and unconditional is simpler.
+  cabal v2-configure -j --enable-tests --disable-documentation --haddock-internal
+  git status --porcelain
   if $IS_WIN; then
-    echo "flags: -builtin-abc" >> cabal.project.local
-    echo "constraints: jvm-verifier -builtin-abc, cryptol-saw-core -build-css" >> cabal.project.local
+    pkgs=(saw crux-mir-comp)
   else
-    pkgs+=(jss)
+    pkgs=(saw crux-mir-comp saw-remote-api)
   fi
-  echo "allow-newer: all" >> cabal.project.local
-  tee -a cabal.project > /dev/null < cabal.project.ci
-  if ! retry cabal v2-build "$@" "${pkgs[@]}"; then
-    if [[ "$RUNNER_OS" == "macOS" ]]; then
-      echo "Working around a dylib issue on macos by removing the cache and trying again"
-      cabal v2-clean
-      retry cabal v2-build "$@" "${pkgs[@]}"
-    else
-      return 1
-    fi
+  cat cabal.project.ci >> cabal.project.local
+  if [[ "$ENABLE_HPC" == "true" ]]; then
+    cat cabal.project.ci-hpc >> cabal.project.local
   fi
-}
-
-build_abc() {
-  arch=X86_64
-  case "$RUNNER_OS" in
-    Linux) os="Linux" ;;
-    macOS) os="OSX" ;;
-    Windows) return ;;
-  esac
-  pushd deps/abcBridge
-  $IS_WIN || scripts/build-abc.sh $arch $os
-  cp abc-build/abc $BIN/abc
-  popd
+  # In the distant past, we had to retry the `cabal build` command to work
+  # around issues with caching dylib files on macOS. These issues appear to
+  # be less likely with modern GitHub Actions caching, so we have removed the
+  # retry logic.
+  cabal v2-build "$@" "${pkgs[@]}"
+}
+
+haddock() {
+  # It seems that the secret sauce for getting cabal to _not_ go
+  # through building docs for every single sublibrary is to pass
+  # --disable-documentation, counterintuitive though that is.
+  #
+  # Note: there's a v2-haddock-project that runs haddock on all
+  # packages in the project, which would avoid needing to list them
+  # out. However, it doesn't support the --disable-documentation
+  # option, so it won't currently serve. (Also for some reason it
+  # currently demands --internal in place of --haddock-internal.)
+  #
+  # We use --haddock-internal because the point of generating the
+  # haddocks for SAW (which doesn't have an external-facing library
+  # interface) is to serve as an internals reference.
+  local PACKAGES='
+    rme
+    saw-core
+    cryptol-saw-core
+    saw-core-what4
+    saw-core-sbv
+    saw-core-aig
+    saw-core-coq
+    heapster-saw
+    saw-script
+    saw-remote-api
+    crucible-mir-comp
+    crux-mir-comp
+    verif-viewer
+  '
+  cabal v2-haddock --haddock-internal --disable-documentation $PACKAGES
+}
+
+# Gather and tar up all HPC coverage files and binaries
+collect_hpc_files() {
+  local MIX_FILES=$(find dist-newstyle -name "*.mix")
+  local GENERATED_HS_FILES=$(find dist-newstyle/build -name "*.hs")
+  local BINS="dist/bin"
+  tar cvf hpc.tar.gz ${MIX_FILES} ${GENERATED_HS_FILES} ${BINS}
+}
+
+# Download HTML coverage reports and generate an index file linking to them
+collect_all_html() {
+  local HTML_DIR=all-html
+  mkdir -p ${HTML_DIR}
+  (cd ${HTML_DIR} && gh run download -p "coverage-html-*" && python3 ../.github/generate_index.py)
 }
 
 install_system_deps() {
-  install_z3 &
-  install_cvc4 &
-  install_yices &
-  install_yasm &
-  wait
-  export PATH=$PWD/$BIN:$PATH
+  (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BUILD_TARGET_OS-$BUILD_TARGET_ARCH-bin.zip" && unzip -o bins.zip && rm bins.zip)
+  chmod +x $BIN/*
+  cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
+  export PATH="$BIN:$PATH"
   echo "$BIN" >> "$GITHUB_PATH"
-  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices && is_exe "$BIN" yasm
-}
-
-test_dist() {
-  find_java
-  pushd intTests
-  for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_examples test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done
-  env
-  LOUD=true ./runtests.sh
-  sh -c "! grep '<failure>' results.xml"
+  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices && is_exe "$BIN" bitwuzla && is_exe "$BIN" boolector
 }
 
 build_cryptol() {
-  is_exe "dist/bin" "cryptol" && return
-  pushd deps/cryptol
-  git submodule update --init
-  .github/ci.sh build
-  popd
+  cabal build exe:cryptol
 }
 
 bundle_files() {
-  mkdir -p dist dist/{bin,doc,examples,include,lib}
+  mkdir -p dist dist/{bin,deps,doc,examples,include,lib}
+  mkdir -p dist/doc/{llvm-java-verification-with-saw,rust-verification-with-saw,saw-user-manual}
 
-  cp deps/abcBridge/abc-build/copyright.txt dist/ABC_LICENSE
   cp LICENSE README.md dist/
   $IS_WIN || chmod +x dist/bin/*
 
-  cp doc/extcore.md dist/doc
-  cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf
-  cp doc/manual/manual.pdf dist/doc/manual.pdf
-  cp -r doc/tutorial/code dist/doc
-  cp deps/jvm-verifier/support/galois.jar dist/lib
+  (cd deps/cryptol-specs && git archive --prefix=cryptol-specs/ --format=tar HEAD) | (cd dist/deps && tar x)
+  cp doc/pdfs/llvm-java-verification-with-saw.pdf dist/doc/llvm-java-verification-with-saw
+  cp doc/pdfs/rust-verification-with-saw.pdf dist/doc/rust-verification-with-saw
+  cp doc/pdfs/saw-user-manual.pdf dist/doc/saw-user-manual
+  cp -r doc/llvm-java-verification-with-saw/code dist/doc/llvm-java-verification-with-saw
+  cp -r doc/rust-verification-with-saw/code dist/doc/rust-verification-with-saw
+  cp intTests/jars/galois.jar dist/lib
   cp -r deps/cryptol/lib/* dist/lib
   cp -r examples/* dist/examples
 }
 
-find_java() {
-  pushd .github
-  javac PropertiesTest.java
-  RT_JAR="$(java PropertiesTest | tr : '\n' | grep rt.jar | head -n 1)"
-  export RT_JAR
-  echo "RT_JAR=$RT_JAR" >> "$GITHUB_ENV"
-  rm PropertiesTest.class
-  popd
-}
-
 sign() {
+  # This is surrounded with `set +x; ...; set -x` to disable printing out
+  # statements that could leak GPG-related secrets.
+  set +x
   gpg --batch --import <(echo "$SIGNING_KEY")
-  fingerprint="$(gpg --list-keys | grep galois -a1 | head -n1 | awk '{$1=$1};1')"
+  fingerprint="$(gpg --list-keys | grep Galois -a1 | head -n1 | awk '{$1=$1};1')"
   echo "$fingerprint:6" | gpg --import-ownertrust
   gpg --yes --no-tty --batch --pinentry-mode loopback --default-key "$fingerprint" --detach-sign -o "$1".sig --passphrase-file <(echo "$SIGNING_PASSPHRASE") "$1"
+  set -x
 }
 
 zip_dist() {
-  : "${VERSION?VERSION is required as an environment variable}"
-  name="${name:-"saw-$VERSION-$RUNNER_OS-x86_64"}"
-  mv dist "$name"
+  name="$1"
+  cp -r dist "$name"
   tar -czf "$name".tar.gz "$name"
-  sign "$name".tar.gz
-  [[ -f "$name".tar.gz.sig ]] && [[ -f "$name".tar.gz ]]
+}
+
+zip_dist_with_solvers() {
+  sname="${1}"
+  # Because these binaries come from the what4-solvers repository, they
+  # should be at least as portable (in terms of dynamic library
+  # dependencies) as the SAW binaries.
+  cp "$BIN/abc"        dist/bin/
+  cp "$BIN/bitwuzla"   dist/bin/
+  cp "$BIN/boolector"  dist/bin/
+  cp "$BIN/cvc4"       dist/bin/
+  cp "$BIN/cvc5"       dist/bin/
+  cp "$BIN/yices"      dist/bin/
+  cp "$BIN/yices-smt2" dist/bin/
+  # Z3 4.8.14 has been known to nondeterministically time out with the AWSLC
+  # and BLST proofs, so we include both 4.8.8 and 4.8.14 so that we can fall
+  # back to 4.8.8 (a version known to work with the AWSLC and BLST proofs)
+  # where necessary. See #1772.
+  cp "$BIN/z3"         dist/bin/
+  cp "$BIN/z3-4.8.8"   dist/bin/
+  cp "$BIN/z3-4.8.14"  dist/bin/
+  cp -r dist "$sname"
+  tar -cvzf "$sname".tar.gz "$sname"
 }
 
 output() { echo "::set-output name=$1::$2"; }

.github/ci.sh

@@ -0,0 +1,30 @@
+#!/usr/bin/env python3
+
+# This script generates an HTML index file for all coverage reports
+
+import glob
+
+HEADER = """
+<!DOCTYPE html>
+<head>
+  <title>SAWScript Test Coverage Results</title>
+</head>
+<body>
+  <h1>SAWScript Test Coverage Results</h1>
+  <p>SAWScript coverage results by pull request number:</p>
+  <ul>
+"""
+
+FOOTER = """
+  </ul>
+</body>
+"""
+
+if __name__ == "__main__":
+  with open("index.html", "w") as f:
+    f.write(HEADER)
+    for dir in sorted(glob.glob("coverage-html-*")):
+      pr_num = dir[14:]
+      link_dest = f"{dir}/hpc_index.html"
+      f.write(f"    <li><a href={link_dest}>{pr_num}</a></li>")
+    f.write(FOOTER)