Merge remote-tracking branch 'upstream/master' into auto-update-night…

…ly-2023-07-15
viperproject · Aug 11, 2023 · f0996cc · f0996cc
2 parents 7e79b1d + 3802482
commit f0996cc
Show file tree

Hide file tree

Showing 10 changed files with 76 additions and 35 deletions.
diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
@@ -14,12 +14,13 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
 
       - name: Set up the environment
         run: python x.py setup

diff --git a/.github/workflows/crates-io.yml b/.github/workflows/crates-io.yml
@@ -20,7 +20,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Publish crates.io
         uses: katyo/publish-crates@v2
         with:

diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
@@ -19,17 +19,18 @@ jobs:
     runs-on: ${{ matrix.os }}
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Set up Python 3
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.x'
 
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
 
       - name: Set up the environment
         run: python x.py setup
@@ -61,17 +62,18 @@ jobs:
     if: false
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Set up Python 3
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.x'
 
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
 
       - name: Set up the environment
         run: python x.py setup

diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml
@@ -17,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
         with:
           path: "repo"
 

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -24,7 +24,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Check formatting
         run: |
           rustup component add rustfmt
@@ -35,11 +35,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
       - name: Set up the environment
         run: python x.py setup
       - name: Cache cargo
@@ -56,11 +57,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
       - name: Set up the environment
         run: python x.py setup
       - name: Cache cargo
@@ -77,7 +79,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Check and report illegal extern crate.
         run: |
           python ./x.py check-smir
@@ -91,11 +93,12 @@ jobs:
       PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
       - name: Set up the environment
         run: python x.py setup
       - name: Cache cargo
@@ -117,11 +120,12 @@ jobs:
       PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
       - name: Set up the environment
         run: python x.py setup
       - name: Cache cargo
@@ -215,15 +219,16 @@ jobs:
       PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Set up Python 3
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.x'
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
       - name: Set up the environment
         run: python x.py setup
       - name: Cache cargo
@@ -258,6 +263,34 @@ jobs:
           cd prusti-contracts/prusti-contracts-test/
           cargo +stable build
 
+  release-build:
+    needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
+    strategy:
+      matrix:
+        os: [ubuntu-latest, windows-latest, macos-latest]
+      fail-fast: false
+    runs-on: ${{ matrix.os }}
+    steps:
+      - name: Check out the repo
+        uses: actions/checkout@v3
+
+      - name: Set up Python 3
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.x'
+
+      - name: Set up Java
+        uses: actions/setup-java@v3
+        with:
+          java-version: '15'
+          distribution: 'zulu'
+
+      - name: Set up the environment
+        run: python x.py setup
+
+      - name: Build with cargo --release
+        run: python x.py build --release
+
   # Run Prusti on itself.
   # Disabled because of a bug when compiling jni-gen
   test-on-prusti:
@@ -266,11 +299,12 @@ jobs:
     if: false
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
       - name: Set up the environment
         run: python x.py setup
       - name: Cache cargo
@@ -297,15 +331,16 @@ jobs:
         shard_index: [0, 1, 2, 3]
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
       - name: Setup Python 3
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.x'
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: '15'
+          distribution: 'zulu'
       - name: Set up the environment
         run: python x.py setup
       - name: Cache cargo
@@ -323,7 +358,7 @@ jobs:
   # Dummy job to specify the jobs that must pass before merging on master
   can-merge:
     runs-on: ubuntu-latest
-    needs: [all-tests, purification-tests, test-crates]
+    needs: [all-tests, purification-tests, release-build, test-crates]
     # Always run, even if the workflow was cancelled
     if: ${{ always() }}
     steps:

diff --git a/.github/workflows/update-deps.yml b/.github/workflows/update-deps.yml
@@ -12,7 +12,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Cache cargo
         uses: Swatinem/rust-cache@v2

diff --git a/Cargo.toml b/Cargo.toml
@@ -36,6 +36,6 @@ debug = 1
 [profile.release]
 # Enable after fixing https://github.com/viperproject/prusti-dev/issues/383
 # lto = true
-# codegen-units = 1
+codegen-units = 1
 # Enable when profiling
 # debug = true
diff --git a/README.md b/README.md
@@ -18,10 +18,10 @@ The tool checks them, reporting error messages when the code does not adhere to
 Useful links
 ------------
 
-* 💻 [VSCode extension](https://marketplace.visualstudio.com/items?itemName=viper-admin.prusti-assistant) to use Prusti from your IDE.
+* 💻 [VS Code extension](https://marketplace.visualstudio.com/items?itemName=viper-admin.prusti-assistant) to use Prusti from your IDE.
 * 📖 [User guide](https://viperproject.github.io/prusti-dev/user-guide/), containing installation instructions, a guided tutorial and a description of various verification features.
 * 🧰 [Developer guide](https://viperproject.github.io/prusti-dev/dev-guide/), meant for new contributors.
-* 📚 [List of publications](http://www.pm.inf.ethz.ch/research/prusti.html). To cite Prusti, please use [this BibTeX entry](http://pm.inf.ethz.ch/publications/getbib.php?action=bibtex&bibname=Own&id=AstrauskasMuellerPoliSummers19b).
+* 📚 [List of publications](http://www.pm.inf.ethz.ch/research/prusti.html). To cite the Prusti verifier, please use [this BibTeX entry](http://pm.inf.ethz.ch/publications/getbib.php?action=bibtex&bibname=Own&id=AstrauskasMuellerPoliSummers19b).
 * ⚖️ [License](https://github.com/viperproject/prusti-dev/blob/master/LICENSE) of the source code (Mozilla Public License Version 2.0, with exceptions).
 * 💬 Do you still have questions? Open an issue or contact us on the [Zulip chat](https://prusti.zulipchat.com/).
 

diff --git a/prusti-contracts/Cargo.toml b/prusti-contracts/Cargo.toml
@@ -10,3 +10,6 @@ resolver = "2"
 # This should not be built as part of Prusti (instead being build by `prusti-contracts-build`)
 # It would require setting the `build.rustc-wrapper` in a `../.cargo/config.toml` correctly
 # But it's unclear how to figure out if we're doing a debug or release build there
+
+[profile.release]
+codegen-units = 1
diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs
@@ -129,10 +129,10 @@ impl PrustiError {
     pub fn internal<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
         let mut error = PrustiError::new(
-            "[Prusti internal error] Prusti encountered an unexpected internal error".to_string(),
+            "[Prusti: internal error] Prusti encountered an unexpected internal error".to_string(),
             span
         ).add_note(
-            "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
+            "This is likely to be a bug in Prusti. We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
             None
         ).add_note(
             format!("Details: {}", message.to_string()),