Merge remote-tracking branch 'upstream/master' into iterators-feature…

…-flag

.devcontainer/Dockerfile

@@ -0,0 +1,9 @@
+# See here for image contents: https://github.com/microsoft/vscode-dev-containers/tree/v0.233.0/containers/rust/.devcontainer/base.Dockerfile
+
+# [Choice] Debian OS version (use bullseye on local arm64/Apple Silicon): buster, bullseye
+ARG VARIANT="buster"
+FROM mcr.microsoft.com/vscode/devcontainers/rust:0-${VARIANT}
+
+# [Optional] Uncomment this section to install additional packages.
+# RUN apt-get update && export DEBIAN_FRONTEND=noninteractive \
+#     && apt-get -y install --no-install-recommends <your-package-list-here>

.devcontainer/devcontainer.json

@@ -0,0 +1,58 @@
+// For format details, see https://aka.ms/devcontainer.json. For config options, see the README at:
+// https://github.com/microsoft/vscode-dev-containers/tree/v0.233.0/containers/rust
+{
+  "name": "Rust",
+  "build": {
+    "dockerfile": "Dockerfile",
+    "args": {
+      // Use the VARIANT arg to pick a Debian OS version: buster, bullseye
+      // Use bullseye when on local on arm64/Apple Silicon.
+      "VARIANT": "buster"
+    }
+  },
+  "runArgs": [
+    "--cap-add=SYS_PTRACE",
+    "--security-opt",
+    "seccomp=unconfined"
+  ],
+
+  // Set *default* container specific settings.json values on container create.
+  "settings": {
+    "lldb.executable": "/usr/bin/lldb",
+    // VS Code don't watch files under ./target
+    "files.watcherExclude": {
+      "**/target/**": true
+    },
+    "rust-analyzer.server.extraEnv": {
+      "JAVA_HOME": "/usr/local/sdkman/candidates/java/current",
+      "RUST_TEST_THREADS": 1,
+      "LD_LIBRARY_PATH": "/usr/local/sdkman/candidates/java/current/lib/server",
+      "VIPER_HOME": "/workspaces/prusti-dev/viper_tools/backends",
+      "Z3_EXE": "/workspaces/prusti-dev/viper_tools/z3/bin/z3"
+    }
+  },
+
+  // Add the IDs of extensions you want installed when the container is created.
+  "extensions": [
+    "bungcip.better-toml",
+    "vadimcn.vscode-lldb",
+    "stkb.rewrap",
+    "rust-lang.rust-analyzer",
+    "viper-admin.viper"
+  ],
+
+  // Use 'forwardPorts' to make a list of ports inside the container available locally.
+  // "forwardPorts": [],
+
+  // Use 'postCreateCommand' to run commands after the container is created.
+  // "postCreateCommand": "rustc --version",
+
+  // Comment out to connect as root instead. More info: https://aka.ms/vscode-remote/containers/non-root.
+  "remoteUser": "vscode",
+  "features": {
+    "fish": "latest",
+    "java": "17"
+  },
+
+  "updateContentCommand": "python ./x.py"
+}

.github/workflows/backlog.yml

@@ -15,7 +15,7 @@ jobs:
 
       - name: Choose developer
         run: |
-          declare -a DEVELOPERS=(Aurel300 fpoli JonasAlaif vakaras)
+          declare -a DEVELOPERS=(Aurel300 JonasAlaif vakaras) # fpoli
           UPDATE_NUMBER=$(( 10#$(date +%m) * 2 + (10#$(date +%d) / 15) - 2 ))
           DEVELOPER="${DEVELOPERS[ $UPDATE_NUMBER % ${#DEVELOPERS[@]} ]}"
           DATE="$(date +%Y-%m-%d)"

.github/workflows/test.yml

@@ -99,6 +99,22 @@ jobs:
           rustup component add rustfmt
           python ./x.py fmt-check-all
 
+  # Check that we depend on the compiler only through SMIR.
+  smir-check:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out the repo
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0 # deep clone, to allow us to use git merge-base
+      - name: Set up Python 3
+        uses: actions/setup-python@v2
+        with:
+          python-version: '3.x'
+      - name: Check and report illegal extern crate.
+        run: |
+          python ./x.py check-smir
+
   # Run a subset of the tests with the purification optimization enabled
   # to ensure that we do not introduce regressions.
   purification-tests:
@@ -165,6 +181,11 @@ jobs:
         run: python x.py build --all --verbose
       - name: Run cargo tests
         run: python x.py test --all --verbose
+      - name: Run a subset of tests with Carbon
+        run: |
+            python x.py test pass/no-annotation --all --verbose
+        env:
+          PRUSTI_VIPER_BACKEND: carbon
       - name: Check prusti-contracts
         run: |
           cd prusti-contracts-test/
@@ -191,7 +212,7 @@ jobs:
       - name: Run cargo-prusti on Prusti
         run: python x.py prusti
         env:
-          LD_LIBRARY_PATH=target/release:${{ env.LD_LIBRARY_PATH }}
-          PRUSTI_SKIP_UNSUPPORTED_FEATURES=true
-          PRUSTI_FULL_COMPILATION=true
-          PRUSTI_CHECK_PANICS=false
+          LD_LIBRARY_PATH: target/release:${{ env.LD_LIBRARY_PATH }}
+          PRUSTI_SKIP_UNSUPPORTED_FEATURES: true
+          PRUSTI_FULL_COMPILATION: true
+          PRUSTI_CHECK_PANICS: false

.github/workflows/update-deps.yml

@@ -29,7 +29,7 @@ jobs:
           )"
           echo "The latest usable version of rustc is $NIGHTLY_VERSION"
           sed -i 's/^channel\s*=.*$/channel = "'"$NIGHTLY_VERSION"'"/' rust-toolchain
-          declare -a DEVELOPERS=(Aurel300 fpoli JonasAlaif vakaras)
+          declare -a DEVELOPERS=(Aurel300 JonasAlaif vakaras) # fpoli
           UPDATE_NUMBER=$(( 10#$(date +%m) * 2 + (10#$(date +%d) / 15) - 0 ))
           DEVELOPER="${DEVELOPERS[ $UPDATE_NUMBER % ${#DEVELOPERS[@]} ]}"
           echo "The assigned developer is $DEVELOPER"
@@ -55,6 +55,7 @@ jobs:
           body: |
             * [x] Update Viper version to `${{ env.VIPER_VERSION }}`.
             * [x] Update rustc version to `${{ env.NIGHTLY_VERSION }}`.
+            * [ ] Run `cargo audit` and fix the issues.
             * [ ] Manualy update outdated dependencies (see the list below).
             * [ ] Manualy run `cargo update`.
             

.vscode/settings.json

@@ -1,3 +1,3 @@
 {
     "rust-analyzer.rustc.source": "discover"
-}
+}