Update Stainless to v0.8 (#107)

* Bump stainless version.

* Update generated stainless AST.

* Update README.

* Fix test failing due to a Stainless bug.

* Use renamed archive to see if test suite is hanging because of caching issue

* Update README.md

Co-authored-by: Romain Ruetschi <[email protected]>

* Set parallelism to 0.

* Disable measure inference for v0.8

* Respond to comments.

Co-authored-by: Romain Ruetschi <[email protected]>
Co-authored-by: Romain Ruetschi <[email protected]>

.stainless-version

@@ -1 +1 @@
-noxt-0.7.6-67-g533f5d5
+noxt-0.8.0-41-g20d258d

README.md

@@ -16,9 +16,19 @@ The following instructions assume that you have installed Rust using [rustup](ht
 - Clone this repo in `/basedir/rust-stainless`.
 - Make sure your `rustup` toolchain within that directory is set to the currently supported nightly version (via `rustup override set $(cat rust-toolchain)` in `/basedir/rust-stainless`).
 - Make sure you have the `rustc-dev` and `llvm-tools-preview` components installed (via `rustup component add rustc-dev llvm-tools-preview`).
-- Install `stainless_driver` (via `cargo install --path stainless_frontend/`). This will build the `rustc_to_stainless` driver, which is essentially a modified version of `rustc`, and `cargo-stainless`, which provides a convenient way of invoking `rustc_to_stainless` from within Cargo project folders. Installation ensures that both of these binaries end up on your `PATH`.
-- Get a copy of the standalone version of `stainless-noxt` for [Linux](lara.epfl.ch/~gschmid/stainless/stainless-noxt-SNAPSHOT-linux.zip) or [macOS](lara.epfl.ch/~gschmid/stainless/stainless-noxt-SNAPSHOT-mac.zip). (This is based on forks of [inox](https://github.com/epfl-lara/inox/tree/rust-interop) and [stainless](https://github.com/epfl-lara/stainless/tree/rust-interop).) Extract it to `/basedir/stainless`.
-- Make sure that your `STAINLESS_HOME` environmental variable points to `/basedir/stainless`.
+- Install `stainless_frontend` (via `cargo install --path stainless_frontend/`). This will build the `rustc_to_stainless` driver, which is essentially a modified version of `rustc`, and `cargo-stainless`, which provides a convenient way of invoking `rustc_to_stainless` from within Cargo project folders. Installation ensures that both of these binaries end up on your `PATH`.
+
+- Get a copy of the standalone version of `stainless-noxt` from the release of
+Stainless that has the tag stated in [`.stainless-version`](.stainless-version).
+For example, [this one](https://github.com/epfl-lara/stainless/releases/tag/noxt-0.8.0-41-g20d258d)
+with the archive for [Linux](https://github.com/epfl-lara/stainless/releases/download/noxt-0.8.0-41-g20d258d/stainless-noxt-0.8.0-41-g20d258d-linux.zip)
+or [macOS](https://github.com/epfl-lara/stainless/releases/download/noxt-0.8.0-41-g20d258d/stainless-noxt-0.8.0-41-g20d258d-mac.zip).
+(This is based on forks of
+[inox](https://github.com/epfl-lara/inox/tree/rust-interop) and
+[stainless](https://github.com/epfl-lara/stainless/tree/rust-interop).)
+
+- Extract it to `/basedir/stainless`.
+- Make sure that your `STAINLESS_HOME` environment variable points to `/basedir/stainless`.
 
 Now you should be good to go.
 
@@ -32,7 +42,9 @@ Similarly to other cargo commands, you can also use `cargo stainless --example f
 
 ## What to expect
 
-Note that the fragment of Rust currently supported is very limited. _TODO: Give some examples_
+Note that the fragment of Rust currently supported is very limited. The test
+cases give you a good impression of [what works](stainless_frontend/tests/pass)
+and [what doesn't yet](stainless_frontend/tests/fail).
 
 ## Development
 
@@ -41,6 +53,23 @@ First, export the serialized stainless program using `cargo stainless --export o
 To then run verification on that file, navigate to your checked-out Stainless repo, run `sbt` in the root folder of the repo, and consequently switch to the appropriate subproject using `project stainless-noxt`.
 The actual verification can be started using `run /the/path/to/output.inoxser`.
 
+### Generating the Stainless ADT
+
+The `rust-stainless` frontend transforms Rust programs to Stainless trees which
+are fed to the Stainless backend. The definition of these trees is in found in
+[`stainless_data`](stainless_data/src/ast/generated.rs) and is automatically generated from the 
+Stainless repository. 
+
+If Stainless gets new features or a fix, it is sometimes necessary to regenerate the AST in order to
+stay compatible with the latest version of the Stainless backend. This is done from the `rust-interop` branch 
+on [Stainless](https://github.com/epfl-lara/stainless/tree/rust-interop).
+
+1. Checkout the `rust-interop` branch.
+2. Rebase or change what is needed.
+3. Run `sbt` and then `runMain stainless.utils.RustInteropGeneratorTool generated.rs`.
+4. Move the newly `generated.rs` file to `stainless_data/src/ast/generated.rs`.
+5. Rebuild and test the frontend to see whether everything still works and hope for the best.
+
 ## Contributors
 
 - Georg Schmid ([@gsps](https://github.com/gsps))

stainless_backend/src/lib.rs

@@ -57,6 +57,8 @@ impl Backend {
       .arg("--batched")
       .arg("--vc-cache=false")
       .arg("--type-checker=false")
+      .arg("--check-measures=false")
+      .arg("--infer-measures=false")
       .arg(format!("--timeout={}", config.timeout))
       .arg(format!("--print-ids={}", config.print_ids))
       .arg(format!("--print-types={}", config.print_types))