From e01efbec3a7b5f32f3467f0085fd95d4d5de04a9 Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Mon, 15 Mar 2021 16:42:56 +0100 Subject: [PATCH 1/9] Bump stainless version. --- .stainless-version | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.stainless-version b/.stainless-version index 8b771430..27f718d3 100644 --- a/.stainless-version +++ b/.stainless-version @@ -1 +1 @@ -noxt-0.7.6-67-g533f5d5 +noxt-0.8.0-41-g20d258d \ No newline at end of file From 370eca1a243cf3266cb5b5ff63e573cd13379311 Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Mon, 15 Mar 2021 18:38:42 +0100 Subject: [PATCH 2/9] Update generated stainless AST. --- stainless_data/src/ast/generated.rs | 187 ++++++++++++++++++++++++++-- 1 file changed, 176 insertions(+), 11 deletions(-) diff --git a/stainless_data/src/ast/generated.rs b/stainless_data/src/ast/generated.rs index 2125144e..da99387d 100644 --- a/stainless_data/src/ast/generated.rs +++ b/stainless_data/src/ast/generated.rs @@ -419,7 +419,7 @@ pub struct LocalTypeDef<'a> { impl<'a> Serializable for LocalTypeDef<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(246))?; + s.write_marker(MarkerId(247))?; self.id.serialize(s)?; self.tparams.serialize(s)?; self.rhs.serialize(s)?; @@ -439,7 +439,7 @@ pub struct TypeDef<'a> { impl<'a> Serializable for TypeDef<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(244))?; + s.write_marker(MarkerId(255))?; self.id.serialize(s)?; self.tparams.serialize(s)?; self.rhs.serialize(s)?; @@ -514,6 +514,7 @@ pub enum Flag<'a> { Derived(&'a Derived<'a>), Erasable(&'a Erasable), Extern(&'a Extern), + FieldDefPosition(&'a FieldDefPosition), Final(&'a Final), Ghost(&'a Ghost), HasADTEquality(&'a HasADTEquality<'a>), @@ -532,14 +533,19 @@ pub enum Flag<'a> { IsMutable(&'a IsMutable), IsPure(&'a IsPure), IsSealed(&'a IsSealed), + IsTypeMemberOf(&'a IsTypeMemberOf<'a>), IsUnapply(&'a IsUnapply<'a>), IsVar(&'a IsVar), Law(&'a Law), + Lazy(&'a Lazy), Library(&'a Library), Opaque(&'a Opaque), PartialEval(&'a PartialEval), Private(&'a Private), + StrictBV(&'a StrictBV), Synthetic(&'a Synthetic), + Template(&'a Template), + TraceInduct(&'a TraceInduct), Unchecked(&'a Unchecked), ValueClass(&'a ValueClass), Variance(&'a Variance), @@ -567,6 +573,10 @@ impl Factory { self.bump.alloc(Extern {}) } + pub fn FieldDefPosition<'a>(&'a self, i: Int) -> &'a mut FieldDefPosition { + self.bump.alloc(FieldDefPosition { i }) + } + pub fn Final<'a>(&'a self) -> &'a mut Final { self.bump.alloc(Final {}) } @@ -642,6 +652,10 @@ impl Factory { self.bump.alloc(IsSealed {}) } + pub fn IsTypeMemberOf<'a>(&'a self, id: &'a SymbolIdentifier<'a>) -> &'a mut IsTypeMemberOf<'a> { + self.bump.alloc(IsTypeMemberOf { id }) + } + pub fn IsUnapply<'a>( &'a self, isEmpty: &'a SymbolIdentifier<'a>, @@ -658,6 +672,10 @@ impl Factory { self.bump.alloc(Law {}) } + pub fn Lazy<'a>(&'a self) -> &'a mut Lazy { + self.bump.alloc(Lazy {}) + } + pub fn Library<'a>(&'a self) -> &'a mut Library { self.bump.alloc(Library {}) } @@ -674,10 +692,22 @@ impl Factory { self.bump.alloc(Private {}) } + pub fn StrictBV<'a>(&'a self) -> &'a mut StrictBV { + self.bump.alloc(StrictBV {}) + } + pub fn Synthetic<'a>(&'a self) -> &'a mut Synthetic { self.bump.alloc(Synthetic {}) } + pub fn Template<'a>(&'a self) -> &'a mut Template { + self.bump.alloc(Template {}) + } + + pub fn TraceInduct<'a>(&'a self) -> &'a mut TraceInduct { + self.bump.alloc(TraceInduct {}) + } + pub fn Unchecked<'a>(&'a self) -> &'a mut Unchecked { self.bump.alloc(Unchecked {}) } @@ -703,6 +733,7 @@ impl<'a> Serializable for Flag<'a> { Flag::Derived(v) => v.serialize(s)?, Flag::Erasable(v) => v.serialize(s)?, Flag::Extern(v) => v.serialize(s)?, + Flag::FieldDefPosition(v) => v.serialize(s)?, Flag::Final(v) => v.serialize(s)?, Flag::Ghost(v) => v.serialize(s)?, Flag::HasADTEquality(v) => v.serialize(s)?, @@ -721,14 +752,19 @@ impl<'a> Serializable for Flag<'a> { Flag::IsMutable(v) => v.serialize(s)?, Flag::IsPure(v) => v.serialize(s)?, Flag::IsSealed(v) => v.serialize(s)?, + Flag::IsTypeMemberOf(v) => v.serialize(s)?, Flag::IsUnapply(v) => v.serialize(s)?, Flag::IsVar(v) => v.serialize(s)?, Flag::Law(v) => v.serialize(s)?, + Flag::Lazy(v) => v.serialize(s)?, Flag::Library(v) => v.serialize(s)?, Flag::Opaque(v) => v.serialize(s)?, Flag::PartialEval(v) => v.serialize(s)?, Flag::Private(v) => v.serialize(s)?, + Flag::StrictBV(v) => v.serialize(s)?, Flag::Synthetic(v) => v.serialize(s)?, + Flag::Template(v) => v.serialize(s)?, + Flag::TraceInduct(v) => v.serialize(s)?, Flag::Unchecked(v) => v.serialize(s)?, Flag::ValueClass(v) => v.serialize(s)?, Flag::Variance(v) => v.serialize(s)?, @@ -743,6 +779,7 @@ derive_conversions_for_ast!(Flag<'a>, Bounds<'a>); derive_conversions_for_ast!(Flag<'a>, Derived<'a>); derive_conversions_for_ast!(Flag<'a>, Erasable); derive_conversions_for_ast!(Flag<'a>, Extern); +derive_conversions_for_ast!(Flag<'a>, FieldDefPosition); derive_conversions_for_ast!(Flag<'a>, Final); derive_conversions_for_ast!(Flag<'a>, Ghost); derive_conversions_for_ast!(Flag<'a>, HasADTEquality<'a>); @@ -761,14 +798,19 @@ derive_conversions_for_ast!(Flag<'a>, IsMethodOf<'a>); derive_conversions_for_ast!(Flag<'a>, IsMutable); derive_conversions_for_ast!(Flag<'a>, IsPure); derive_conversions_for_ast!(Flag<'a>, IsSealed); +derive_conversions_for_ast!(Flag<'a>, IsTypeMemberOf<'a>); derive_conversions_for_ast!(Flag<'a>, IsUnapply<'a>); derive_conversions_for_ast!(Flag<'a>, IsVar); derive_conversions_for_ast!(Flag<'a>, Law); +derive_conversions_for_ast!(Flag<'a>, Lazy); derive_conversions_for_ast!(Flag<'a>, Library); derive_conversions_for_ast!(Flag<'a>, Opaque); derive_conversions_for_ast!(Flag<'a>, PartialEval); derive_conversions_for_ast!(Flag<'a>, Private); +derive_conversions_for_ast!(Flag<'a>, StrictBV); derive_conversions_for_ast!(Flag<'a>, Synthetic); +derive_conversions_for_ast!(Flag<'a>, Template); +derive_conversions_for_ast!(Flag<'a>, TraceInduct); derive_conversions_for_ast!(Flag<'a>, Unchecked); derive_conversions_for_ast!(Flag<'a>, ValueClass); derive_conversions_for_ast!(Flag<'a>, Variance); @@ -842,6 +884,20 @@ impl Serializable for Extern { } } +/// stainless.extraction.methods.Trees.FieldDefPosition +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct FieldDefPosition { + pub i: Int, +} + +impl Serializable for FieldDefPosition { + fn serialize(&self, s: &mut S) -> SerializationResult { + s.write_marker(MarkerId(245))?; + self.i.serialize(s)?; + Ok(()) + } +} + /// stainless.ast.Definitions.Final #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct Final {} @@ -1058,6 +1114,20 @@ impl Serializable for IsSealed { } } +/// stainless.extraction.oo.Definitions.IsTypeMemberOf +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct IsTypeMemberOf<'a> { + pub id: &'a SymbolIdentifier<'a>, +} + +impl<'a> Serializable for IsTypeMemberOf<'a> { + fn serialize(&self, s: &mut S) -> SerializationResult { + s.write_marker(MarkerId(246))?; + self.id.serialize(s)?; + Ok(()) + } +} + /// stainless.ast.Definitions.IsUnapply #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct IsUnapply<'a> { @@ -1096,13 +1166,24 @@ impl Serializable for Law { } } +/// stainless.ast.Definitions.Lazy +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct Lazy {} + +impl Serializable for Lazy { + fn serialize(&self, s: &mut S) -> SerializationResult { + s.write_marker(MarkerId(167))?; + Ok(()) + } +} + /// stainless.ast.Definitions.Library #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct Library {} impl Serializable for Library { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(158))?; + s.write_marker(MarkerId(168))?; Ok(()) } } @@ -1140,6 +1221,17 @@ impl Serializable for Private { } } +/// stainless.extraction.xlang.Trees.StrictBV +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct StrictBV {} + +impl Serializable for StrictBV { + fn serialize(&self, s: &mut S) -> SerializationResult { + s.write_marker(MarkerId(256))?; + Ok(()) + } +} + /// stainless.ast.Definitions.Synthetic #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct Synthetic {} @@ -1151,6 +1243,28 @@ impl Serializable for Synthetic { } } +/// stainless.ast.Definitions.Template +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct Template {} + +impl Serializable for Template { + fn serialize(&self, s: &mut S) -> SerializationResult { + s.write_marker(MarkerId(169))?; + Ok(()) + } +} + +/// stainless.extraction.trace.Trees.TraceInduct +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct TraceInduct {} + +impl Serializable for TraceInduct { + fn serialize(&self, s: &mut S) -> SerializationResult { + s.write_marker(MarkerId(244))?; + Ok(()) + } +} + /// stainless.ast.Definitions.Unchecked #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct Unchecked {} @@ -1275,6 +1389,7 @@ pub enum Expr<'a> { LocalMethodInvocation(&'a LocalMethodInvocation<'a>), LocalThis(&'a LocalThis<'a>), MapApply(&'a MapApply<'a>), + MapMerge(&'a MapMerge<'a>), MapUpdated(&'a MapUpdated<'a>), MatchExpr(&'a MatchExpr<'a>), Max(&'a Max<'a>), @@ -1295,6 +1410,7 @@ pub enum Expr<'a> { Plus(&'a Plus<'a>), Remainder(&'a Remainder<'a>), Require(&'a Require<'a>), + Return(&'a Return<'a>), SetAdd(&'a SetAdd<'a>), SetDifference(&'a SetDifference<'a>), SetIntersection(&'a SetIntersection<'a>), @@ -1781,6 +1897,15 @@ impl Factory { self.bump.alloc(MapApply { map, key }) } + pub fn MapMerge<'a>( + &'a self, + mask: Expr<'a>, + map1: Expr<'a>, + map2: Expr<'a>, + ) -> &'a mut MapMerge<'a> { + self.bump.alloc(MapMerge { mask, map1, map2 }) + } + pub fn MapUpdated<'a>( &'a self, map: Expr<'a>, @@ -1909,6 +2034,10 @@ impl Factory { self.bump.alloc(Require { pred, body }) } + pub fn Return<'a>(&'a self, expr: Expr<'a>) -> &'a mut Return<'a> { + self.bump.alloc(Return { expr }) + } + pub fn SetAdd<'a>(&'a self, set: Expr<'a>, elem: Expr<'a>) -> &'a mut SetAdd<'a> { self.bump.alloc(SetAdd { set, elem }) } @@ -2116,6 +2245,7 @@ impl<'a> Serializable for Expr<'a> { Expr::LocalMethodInvocation(v) => v.serialize(s)?, Expr::LocalThis(v) => v.serialize(s)?, Expr::MapApply(v) => v.serialize(s)?, + Expr::MapMerge(v) => v.serialize(s)?, Expr::MapUpdated(v) => v.serialize(s)?, Expr::MatchExpr(v) => v.serialize(s)?, Expr::Max(v) => v.serialize(s)?, @@ -2136,6 +2266,7 @@ impl<'a> Serializable for Expr<'a> { Expr::Plus(v) => v.serialize(s)?, Expr::Remainder(v) => v.serialize(s)?, Expr::Require(v) => v.serialize(s)?, + Expr::Return(v) => v.serialize(s)?, Expr::SetAdd(v) => v.serialize(s)?, Expr::SetDifference(v) => v.serialize(s)?, Expr::SetIntersection(v) => v.serialize(s)?, @@ -2236,6 +2367,7 @@ derive_conversions_for_ast!(Expr<'a>, LocalClassSelector<'a>); derive_conversions_for_ast!(Expr<'a>, LocalMethodInvocation<'a>); derive_conversions_for_ast!(Expr<'a>, LocalThis<'a>); derive_conversions_for_ast!(Expr<'a>, MapApply<'a>); +derive_conversions_for_ast!(Expr<'a>, MapMerge<'a>); derive_conversions_for_ast!(Expr<'a>, MapUpdated<'a>); derive_conversions_for_ast!(Expr<'a>, MatchExpr<'a>); derive_conversions_for_ast!(Expr<'a>, Max<'a>); @@ -2256,6 +2388,7 @@ derive_conversions_for_ast!(Expr<'a>, Passes<'a>); derive_conversions_for_ast!(Expr<'a>, Plus<'a>); derive_conversions_for_ast!(Expr<'a>, Remainder<'a>); derive_conversions_for_ast!(Expr<'a>, Require<'a>); +derive_conversions_for_ast!(Expr<'a>, Return<'a>); derive_conversions_for_ast!(Expr<'a>, SetAdd<'a>); derive_conversions_for_ast!(Expr<'a>, SetDifference<'a>); derive_conversions_for_ast!(Expr<'a>, SetIntersection<'a>); @@ -3450,6 +3583,24 @@ impl<'a> Serializable for MapApply<'a> { } } +/// inox.ast.Expressions.MapMerge +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct MapMerge<'a> { + pub mask: Expr<'a>, + pub map1: Expr<'a>, + pub map2: Expr<'a>, +} + +impl<'a> Serializable for MapMerge<'a> { + fn serialize(&self, s: &mut S) -> SerializationResult { + s.write_marker(MarkerId(103))?; + self.mask.serialize(s)?; + self.map1.serialize(s)?; + self.map2.serialize(s)?; + Ok(()) + } +} + /// inox.ast.Expressions.MapUpdated #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct MapUpdated<'a> { @@ -3575,7 +3726,7 @@ pub struct MutableMapApply<'a> { impl<'a> Serializable for MutableMapApply<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(234))?; + s.write_marker(MarkerId(250))?; self.map.serialize(s)?; self.key.serialize(s)?; Ok(()) @@ -3590,7 +3741,7 @@ pub struct MutableMapDuplicate<'a> { impl<'a> Serializable for MutableMapDuplicate<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(237))?; + s.write_marker(MarkerId(253))?; self.map.serialize(s)?; Ok(()) } @@ -3606,7 +3757,7 @@ pub struct MutableMapUpdate<'a> { impl<'a> Serializable for MutableMapUpdate<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(235))?; + s.write_marker(MarkerId(251))?; self.map.serialize(s)?; self.key.serialize(s)?; self.value.serialize(s)?; @@ -3624,7 +3775,7 @@ pub struct MutableMapUpdated<'a> { impl<'a> Serializable for MutableMapUpdated<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(236))?; + s.write_marker(MarkerId(252))?; self.map.serialize(s)?; self.key.serialize(s)?; self.value.serialize(s)?; @@ -3642,7 +3793,7 @@ pub struct MutableMapWithDefault<'a> { impl<'a> Serializable for MutableMapWithDefault<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(233))?; + s.write_marker(MarkerId(249))?; self.from.serialize(s)?; self.to.serialize(s)?; self.default.serialize(s)?; @@ -3772,6 +3923,20 @@ impl<'a> Serializable for Require<'a> { } } +/// stainless.extraction.imperative.Trees.Return +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct Return<'a> { + pub expr: Expr<'a>, +} + +impl<'a> Serializable for Return<'a> { + fn serialize(&self, s: &mut S) -> SerializationResult { + s.write_marker(MarkerId(257))?; + self.expr.serialize(s)?; + Ok(()) + } +} + /// inox.ast.Expressions.SetAdd #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct SetAdd<'a> { @@ -4616,7 +4781,7 @@ pub struct MutableMapType<'a> { impl<'a> Serializable for MutableMapType<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(232))?; + s.write_marker(MarkerId(248))?; self.from.serialize(s)?; self.to.serialize(s)?; Ok(()) @@ -4759,7 +4924,7 @@ pub struct TypeApply<'a> { impl<'a> Serializable for TypeApply<'a> { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(238))?; + s.write_marker(MarkerId(254))?; self.selector.serialize(s)?; self.tps.serialize(s)?; Ok(()) @@ -4857,7 +5022,7 @@ pub struct UnknownType { impl Serializable for UnknownType { fn serialize(&self, s: &mut S) -> SerializationResult { - s.write_marker(MarkerId(245))?; + s.write_marker(MarkerId(238))?; self.isPure.serialize(s)?; Ok(()) } From f121b2557955a8eb64251ee0653b0c1a1354c7ee Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Mon, 15 Mar 2021 18:58:31 +0100 Subject: [PATCH 3/9] Update README. --- README.md | 37 +++++++++++++++++++++++++++++++++---- 1 file changed, 33 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index b104de21..fb57684c 100644 --- a/README.md +++ b/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 `epfl-lara/rust-interop`. +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)) From 04a31cafc1fc682941235d803807cd1062a9e5b0 Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Tue, 16 Mar 2021 13:39:00 +0100 Subject: [PATCH 4/9] Fix test failing due to a Stainless bug. --- stainless_frontend/tests/pass/type_class_multi_lookup.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/stainless_frontend/tests/pass/type_class_multi_lookup.rs b/stainless_frontend/tests/pass/type_class_multi_lookup.rs index 982a2873..0e63fd61 100644 --- a/stainless_frontend/tests/pass/type_class_multi_lookup.rs +++ b/stainless_frontend/tests/pass/type_class_multi_lookup.rs @@ -1,4 +1,5 @@ extern crate stainless; +use stainless::*; trait Clone { fn clone(&self) -> Self; @@ -9,6 +10,7 @@ pub enum Option { None, } impl Clone for Option { + #[measure(self)] fn clone(&self) -> Self { match self { Option::Some(v) => Option::Some(v.clone()), From 5c9c78a7d945e5c091ac45b16394092096af5d6c Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Tue, 16 Mar 2021 16:57:40 +0100 Subject: [PATCH 5/9] Use renamed archive to see if test suite is hanging because of caching issue --- .github/workflows/rust.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index ba54e3cc..dd09cee5 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -52,12 +52,12 @@ jobs: with: repository: epfl-lara/stainless tag: ${{ env.stainless_version }} - file: stainless-${{ env.stainless_version }}-linux.zip + file: stainless-${{ env.stainless_version }}-2-linux.zip - name: Unzip Stainless uses: montudor/action-zip@v0.1.1 with: - args: unzip ./stainless-${{ env.stainless_version }}-linux.zip -d ./stainless-noxt + args: unzip ./stainless-${{ env.stainless_version }}-2-linux.zip -d ./stainless-noxt - name: Run cargo build uses: actions-rs/cargo@v1 From 6f65a6d591c721dc8b4169990dc5799ce5a806a9 Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Tue, 16 Mar 2021 17:21:42 +0100 Subject: [PATCH 6/9] Update README.md Co-authored-by: Romain Ruetschi --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index fb57684c..aa0cac8e 100644 --- a/README.md +++ b/README.md @@ -64,7 +64,7 @@ If Stainless gets new features or a fix, it is sometimes necessary to regenerate 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 `epfl-lara/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`. From e1e4e837f976658188cc58cba4f495579cf0b021 Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Wed, 17 Mar 2021 12:58:45 +0100 Subject: [PATCH 7/9] Set parallelism to 0. --- stainless_backend/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/stainless_backend/src/lib.rs b/stainless_backend/src/lib.rs index d25d7c45..1636003f 100644 --- a/stainless_backend/src/lib.rs +++ b/stainless_backend/src/lib.rs @@ -57,6 +57,7 @@ impl Backend { .arg("--batched") .arg("--vc-cache=false") .arg("--type-checker=false") + .arg("-Dparallel=0") .arg(format!("--timeout={}", config.timeout)) .arg(format!("--print-ids={}", config.print_ids)) .arg(format!("--print-types={}", config.print_types)) From b1c21623541ff55f8de7bee79fb544e75b229fce Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Wed, 17 Mar 2021 14:52:26 +0100 Subject: [PATCH 8/9] Disable measure inference for v0.8 --- stainless_backend/src/lib.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/stainless_backend/src/lib.rs b/stainless_backend/src/lib.rs index 1636003f..d9131310 100644 --- a/stainless_backend/src/lib.rs +++ b/stainless_backend/src/lib.rs @@ -57,7 +57,8 @@ impl Backend { .arg("--batched") .arg("--vc-cache=false") .arg("--type-checker=false") - .arg("-Dparallel=0") + .arg("--check-measures=no") + .arg("--infer-measures=false") .arg(format!("--timeout={}", config.timeout)) .arg(format!("--print-ids={}", config.print_ids)) .arg(format!("--print-types={}", config.print_types)) From db3f319654b1ecad8894d5445378ad5378ef4414 Mon Sep 17 00:00:00 2001 From: Yann Bolliger Date: Wed, 17 Mar 2021 15:09:55 +0100 Subject: [PATCH 9/9] Respond to comments. --- .github/workflows/rust.yml | 4 ++-- .stainless-version | 2 +- stainless_backend/src/lib.rs | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index dd09cee5..ba54e3cc 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -52,12 +52,12 @@ jobs: with: repository: epfl-lara/stainless tag: ${{ env.stainless_version }} - file: stainless-${{ env.stainless_version }}-2-linux.zip + file: stainless-${{ env.stainless_version }}-linux.zip - name: Unzip Stainless uses: montudor/action-zip@v0.1.1 with: - args: unzip ./stainless-${{ env.stainless_version }}-2-linux.zip -d ./stainless-noxt + args: unzip ./stainless-${{ env.stainless_version }}-linux.zip -d ./stainless-noxt - name: Run cargo build uses: actions-rs/cargo@v1 diff --git a/.stainless-version b/.stainless-version index 27f718d3..a45c0ef2 100644 --- a/.stainless-version +++ b/.stainless-version @@ -1 +1 @@ -noxt-0.8.0-41-g20d258d \ No newline at end of file +noxt-0.8.0-41-g20d258d diff --git a/stainless_backend/src/lib.rs b/stainless_backend/src/lib.rs index d9131310..61012b8d 100644 --- a/stainless_backend/src/lib.rs +++ b/stainless_backend/src/lib.rs @@ -57,7 +57,7 @@ impl Backend { .arg("--batched") .arg("--vc-cache=false") .arg("--type-checker=false") - .arg("--check-measures=no") + .arg("--check-measures=false") .arg("--infer-measures=false") .arg(format!("--timeout={}", config.timeout)) .arg(format!("--print-ids={}", config.print_ids))