Scala 3 extraction frontend

.gitignore

@@ -3,6 +3,8 @@
 .stainless-cache/
 .stainless.conf
 stainless.conf
+.stainless-external-tests/
+.stainless-package-standalone/
 
 # Vim
 *.swp

.jvmopts

@@ -2,6 +2,6 @@
 -Xss512M
 -Xms1024M
 -Xmx12G
--XX:MaxMetaspaceSize=512M
+-XX:MaxMetaspaceSize=2G
 -XX:+UseCodeCacheFlushing
--XX:ReservedCodeCacheSize=256M
+-XX:ReservedCodeCacheSize=768M

.larabot.conf

@@ -12,6 +12,7 @@ nightly {
     "sbt -batch scripted"
     "bash bin/build-slc-lib.sh"
     "bash -c \"frontends/scalac/target/universal/stage/bin/stainless-scalac --coq frontends/benchmarks/coq/*.scala\""
+    "bash -c \"frontends/dotty/target/universal/stage/bin/stainless-dotty --coq frontends/benchmarks/coq/*.scala\""
   ]
 }
 

bin/bolts-tests.sh

@@ -3,15 +3,19 @@
 set -e
 
 TEST_DIR=$1
+FRONTEND=$2
 echo "Moving to $TEST_DIR"
 mkdir -p "$TEST_DIR"
 cd "$TEST_DIR" || exit 1
 
-git clone https://github.com/epfl-lara/bolts
+if [[ -d "bolts" ]]; then
+  cd bolts
+  git pull || exit 1
+else
+  git clone https://github.com/epfl-lara/bolts
+  cd bolts || exit 1
+fi
 
-cd bolts || exit 1
-
-bash ./run-tests.sh
+bash ./run-tests.sh "$FRONTEND"
 
 cd ../.. || true
-

bin/external-tests.sh

@@ -78,6 +78,47 @@ _canonicalize_file_path() {
 
 ### end of realpath code
 
+usage() {
+ cat <<EOM
+Usage: external-tests.sh [options]
+
+  -h | -help         Print this message
+  --skip-build       Do not build Stainless (saves time if the build is already up-to-date).
+  --only-scalac      Run the tests for the Scalac frontend only.
+  --only-dotty       Run the tests for the Dotty frontend only.
+EOM
+}
+
+SKIP_BUILD=false
+ONLY_SCALAC=false
+ONLY_DOTTY=false
+while [[ $# -gt 0 ]]; do
+  key="$1"
+
+  case $key in
+    -h|--help)
+      usage
+      exit 0
+      ;;
+    --skip-build)
+      SKIP_BUILD=true
+      shift # past argument
+      ;;
+    --only-scalac)
+      ONLY_SCALAC=true
+      shift # past argument
+      ;;
+    --only-dotty)
+      ONLY_DOTTY=true
+      shift # past argument
+      ;;
+    *)    # unknown option
+      usage
+      exit 1
+      ;;
+  esac
+done
+
 BIN_DIR=$( dirname "$( realpath "${BASH_SOURCE[0]}" )" )
 BASE_DIR=$( dirname "$BIN_DIR" )
 
@@ -92,29 +133,36 @@ cd "$BASE_DIR" || exit 1
 
 # Compile Stainless
 
-echo "Compiling Stainless..."
+if [[ "$SKIP_BUILD" = false ]]; then
+  echo "Compiling Stainless..."
+  sbt universal:stage
 
-sbt universal:stage
+  # Publish Stainless local and save the version
 
-export PATH="$BASE_DIR/frontends/scalac/target/universal/stage/bin:$PATH"
-
-# Publish Stainless local and save the version
+  echo "Publishing Stainless..."
 
-echo "Publishing Stainless..."
+  STAINLESS_VERSION=$(sbt publishLocal | $SED -n -r 's#^.*stainless-scalac-plugin_2.12.13/([^/]+)/poms.*$#\1#p' | head -n1)
 
-STAINLESS_VERSION=$(sbt publishLocal | $SED -n -r 's#^.*stainless-scalac-plugin_2.12.13/([^/]+)/poms.*$#\1#p' | head -n1)
+  echo "Published Stainless version is: $STAINLESS_VERSION"
+else
+  echo "Skipping build"
+fi
 
-echo "Published Stainless version is: $STAINLESS_VERSION"
+export PATH="$BASE_DIR/frontends/scalac/target/universal/stage/bin:$PATH"
+export PATH="$BASE_DIR/frontends/dotty/target/universal/stage/bin:$PATH"
 
 # Create a directory for doing tests and move there
 
-TEST_DIR=$(mktemp -d 2>/dev/null || mktemp -d -t "stainless-external-tests")
-
+TEST_DIR="$BASE_DIR/.stainless-external-tests"
 mkdir -p "$TEST_DIR"
 
 # Stainless Actors are currently disabled: https://github.com/epfl-lara/stainless/issues/970
 # "$BIN_DIR/stainless-actors-tests.sh" "$TEST_DIR" "$STAINLESS_VERSION"
-"$BIN_DIR/bolts-tests.sh" "$TEST_DIR"
-
-rm -rf "$TEST_DIR" || true
-
+if [[ "$ONLY_DOTTY" = false ]]; then
+  echo "Running bolts test for scalac"
+  "$BIN_DIR/bolts-tests.sh" "$TEST_DIR" "stainless-scalac"
+fi
+if [[ "$ONLY_SCALAC" = false ]]; then
+  echo "Running bolts test for dotty"
+  "$BIN_DIR/bolts-tests.sh" "$TEST_DIR" "stainless-dotty"
+fi

bin/package-standalone.sh

@@ -1,7 +1,8 @@
 #!/usr/bin/env bash
 # ====
-#  This script assembles the `stainless-scalac-standalone` subproject into
-#  a fat jar and packages it into an archive that contains additional Z3
+#  This script assembles the `stainless-scalac-standalone` and
+#  `stainless-dotty-standalone` subprojects into two separate fat jars
+#  and packages them into an archive that contains additional Z3
 #  dependencies and a launcher script that makes said dependencies available
 #  to the java process.
 #  Currently only Linux (i.e. Z3's `ubuntu` binaries) and macOS are implemented.
@@ -16,8 +17,10 @@ fi
 SCALA_VERSION="3.0.2"
 Z3_VERSION="4.8.12"
 
-SBT_PACKAGE="sbt stainless-scalac-standalone/assembly"
-STAINLESS_JAR_PATH="./frontends/stainless-scalac-standalone/target/scala-$SCALA_VERSION/stainless-scalac-standalone-$STAINLESS_VERSION.jar"
+SBT_PACKAGE_SCALAC="sbt stainless-scalac-standalone/assembly"
+SBT_PACKAGE_DOTTY="sbt stainless-dotty-standalone/assembly"
+STAINLESS_SCALAC_JAR_PATH="./frontends/stainless-scalac-standalone/target/scala-$SCALA_VERSION/stainless-scalac-standalone-$STAINLESS_VERSION.jar"
+STAINLESS_DOTTY_JAR_PATH="./frontends/stainless-dotty-standalone/target/scala-$SCALA_VERSION/stainless-dotty-standalone-$STAINLESS_VERSION.jar"
 # Note: though Stainless is compiled with 3.0.2, we use a 2.13 version of ScalaZ3 (which is binary compatible with Scala 3)
 SCALAZ3_JAR_LINUX_PATH="./unmanaged/scalaz3-unix-64-2.13.jar"
 SCALAZ3_JAR_MAC_PATH="./unmanaged/scalaz3-mac-64-2.13.jar"
@@ -44,9 +47,13 @@ function fail {
 
 # -----
 
-TMP_DIR=$(mktemp -d 2>/dev/null || mktemp -d -t "stainless-package-standalone")
+# Directory of the script dir: https://stackoverflow.com/a/246128
+SCRIPT_DIR="$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )"
+TMP_DIR="$SCRIPT_DIR/../.stainless-package-standalone"
+mkdir -p "$TMP_DIR"
 
-STAINLESS_JAR_BASENAME=$(basename "$STAINLESS_JAR_PATH")
+STAINLESS_SCALAC_JAR_BASENAME=$(basename "$STAINLESS_SCALAC_JAR_PATH")
+STAINLESS_DOTTY_JAR_BASENAME=$(basename "$STAINLESS_DOTTY_JAR_PATH")
 
 function check_tools {
   for tool in \
@@ -75,10 +82,10 @@ function fetch_z3 {
   else
     wget -O "$ZIPF" "$Z3_GITHUB_URL/$NAME" 2>> $LOG || fail
   fi
-  (rm -r "$TMPD" 2>/dev/null || true) && mkdir "$TMPD" || fail
+  (rm -r "$TMPD" 2>/dev/null || true) && mkdir -p "$TMPD" || fail
   unzip -d "$TMPD" "$ZIPF" >> $LOG || fail
 
-  mkdir "$TMPD/z3" >> $LOG || fail
+  mkdir -p "$TMPD/z3" >> $LOG || fail
   for COPY_FILE in LICENSE.txt bin/z3; do
     cp "$TMPD/${NAME%.*}/$COPY_FILE" "$TMPD/z3" >> $LOG || fail
   done
@@ -88,7 +95,8 @@ function fetch_z3 {
 
 function generate_launcher {
   local TARGET="$1"
-  local SCALAZ3_JAR_BASENAME="$2"
+  local STAINLESS_JAR_BASENAME="$2"
+  local SCALAZ3_JAR_BASENAME="$3"
 
   cat "bin/launcher.tmpl.sh" | \
     sed "s#{STAINLESS_JAR_BASENAME}#$STAINLESS_JAR_BASENAME#g" | \
@@ -99,33 +107,39 @@ function generate_launcher {
 
 function package {
   local PLAT="$1"
-  local SCALAZ3_JAR_PATH="$2"
+  local STAINLESS_JAR_PATH="$2"
+  local SCALAZ3_JAR_PATH="$3"
+  local FRONTEND="$4"
+  local STAINLESS_JAR_BASENAME
   local SCALAZ3_JAR_BASENAME
+  STAINLESS_JAR_BASENAME=$(basename "$STAINLESS_JAR_PATH")
   SCALAZ3_JAR_BASENAME=$(basename "$SCALAZ3_JAR_PATH")
 
   local TMPD="$TMP_DIR/$PLAT"
-  info " - $PLAT"
+  info " - $PLAT (for $FRONTEND)"
 
   local ZIPF
   ZIPF="$(pwd)/${STAINLESS_JAR_BASENAME%.*}-$PLAT.zip"
 
   if [ -f "$ZIPF" ]; then
     rm "$ZIPF" || fail
-    info "    (Removed old archive.)"
+    info "    (Removed old $FRONTEND archive.)"
   fi
 
-  generate_launcher "$TMPD/stainless" "$SCALAZ3_JAR_BASENAME" || fail
+  generate_launcher "$TMPD/stainless" "$STAINLESS_JAR_BASENAME" "$SCALAZ3_JAR_BASENAME" || fail
 
   local TGTLIBD="$TMPD/lib"
-  mkdir "$TGTLIBD" >> $LOG || fail
+  mkdir -p "$TGTLIBD" >> $LOG || fail
   cp "$STAINLESS_JAR_PATH" "$TGTLIBD/$STAINLESS_JAR_BASENAME" >> $LOG || fail
   cp "$SCALAZ3_JAR_PATH" "$TGTLIBD/$SCALAZ3_JAR_BASENAME" >> $LOG || fail
   cp "stainless.conf.default" "$TMPD/stainless.conf" >> $LOG || fail
 
   cd "$TMPD" && \
     zip "$ZIPF" lib/** z3/** stainless stainless.conf >> $LOG && \
     cd - >/dev/null || fail
-  info "    Created archive $ZIPF"
+  info "    Created $FRONTEND archive $ZIPF"
+
+  rm "$TGTLIBD/$STAINLESS_JAR_BASENAME" >> $LOG || fail
 
   okay
 }
@@ -138,21 +152,25 @@ info "$(tput bold)[] Checking required tools..."
 check_tools
 
 info "$(tput bold)[] Assembling fat jar..."
-if [ -f "$STAINLESS_JAR_PATH" ]; then
+if [[ -f "$STAINLESS_SCALAC_JAR_PATH" && -f "$STAINLESS_DOTTY_JAR_PATH" ]]; then
   info "  (JAR already exists, skipping sbt assembly step.)" && okay
 else
-  $SBT_PACKAGE >> $LOG && okay || fail
+  $SBT_PACKAGE_SCALAC >> $LOG && okay || fail
+  $SBT_PACKAGE_DOTTY >> $LOG && okay || fail
 fi
 
 info "$(tput bold)[] Downloading Z3 binaries..."
 fetch_z3 "linux" $Z3_LINUX_NAME
 fetch_z3 "mac" $Z3_MAC_NAME
 
 info "$(tput bold)[] Packaging..."
-package "linux" $SCALAZ3_JAR_LINUX_PATH
-package "mac" $SCALAZ3_JAR_MAC_PATH
+package "linux" $STAINLESS_SCALAC_JAR_PATH $SCALAZ3_JAR_LINUX_PATH "scalac"
+package "linux" $STAINLESS_DOTTY_JAR_PATH $SCALAZ3_JAR_LINUX_PATH "dotty"
+package "mac" $STAINLESS_SCALAC_JAR_PATH $SCALAZ3_JAR_MAC_PATH "scalac"
+package "mac" $STAINLESS_DOTTY_JAR_PATH $SCALAZ3_JAR_MAC_PATH "dotty"
 
 info "$(tput bold)[] Cleaning up..."
-rm -r "$TMP_DIR" && okay
+# We only clean up the directories used for packaging; we leave the downloaded Z3 binaries.
+rm -r "$TMP_DIR/linux" "$TMP_DIR/mac" && okay
 
 info "$(tput bold)Packaging successful."