WIP: Iterator tracking issues by vl0w · Pull Request #980 · viperproject/prusti-dev

vl0w · 2022-04-27T15:23:50Z

Some (smaller / bigger) changes needed to enable iterator support
(WIP / tracking PR)

Moved normalization of constraint param env (for assoc types) for better logging
Fixed a bug in SpecGraph: Preconditions of the base spec were copied to the constrained spec
Ghost constraint resolving is a bit relaxed (predicate_may_hold instead of predicate_must_hold_considering_regions) to account for references in associated types. See test associated_types_6.rs
merge_generics now also merges lifetimes to accout for lifetimes appearing in #[refine_trait_spec]
Lifetimes in type models are not converted to the anonymous lifetime '_ anymore
Do not #[derive(Copy, Clone] on type models, because the derive macro "conditionally" implements it when generics are involved. That is, #[derive(Copy)] struct Foo<T> adds impl<T: Copy> Copy for Foo {}, but we do not want to implement Copy only if T is Copy.
Quantified variables now support associated types: forall(|x: Self::SomeAssocType| ...)

…sociated types

…ns infer types

…ts to account for references in associated types

Aurel300 · 2022-07-19T15:28:08Z

bors r+

980: WIP: Iterator tracking issues r=Aurel300 a=vl0w Some (smaller / bigger) changes needed to enable iterator support (WIP / tracking PR) - Moved normalization of constraint param env (for assoc types) for better logging - Fixed a bug in `SpecGraph`: Preconditions of the base spec were copied to the constrained spec - Ghost constraint resolving is a bit relaxed (`predicate_may_hold` instead of `predicate_must_hold_considering_regions`) to account for references in associated types. See test `associated_types_6.rs` - `merge_generics` now also merges lifetimes to accout for lifetimes appearing in `#[refine_trait_spec]` - Lifetimes in type models are not converted to the anonymous lifetime `'_` anymore - Do not `#[derive(Copy, Clone]` on type models, because the derive macro "conditionally" implements it when generics are involved. That is, `#[derive(Copy)] struct Foo<T>` adds `impl<T: Copy> Copy for Foo {}`, but we do not want to implement `Copy` only if `T` is `Copy`. - Quantified variables now support associated types: `forall(|x: Self::SomeAssocType| ...)` Co-authored-by: Jonas Hansen <ganymed92@gmail.com>

bors · 2022-07-19T18:11:46Z

Build failed:

all-tests (ubuntu-latest)

Aurel300 · 2022-07-20T08:44:37Z

bors r+

980: WIP: Iterator tracking issues r=Aurel300 a=vl0w Some (smaller / bigger) changes needed to enable iterator support (WIP / tracking PR) - Moved normalization of constraint param env (for assoc types) for better logging - Fixed a bug in `SpecGraph`: Preconditions of the base spec were copied to the constrained spec - Ghost constraint resolving is a bit relaxed (`predicate_may_hold` instead of `predicate_must_hold_considering_regions`) to account for references in associated types. See test `associated_types_6.rs` - `merge_generics` now also merges lifetimes to accout for lifetimes appearing in `#[refine_trait_spec]` - Lifetimes in type models are not converted to the anonymous lifetime `'_` anymore - Do not `#[derive(Copy, Clone]` on type models, because the derive macro "conditionally" implements it when generics are involved. That is, `#[derive(Copy)] struct Foo<T>` adds `impl<T: Copy> Copy for Foo {}`, but we do not want to implement `Copy` only if `T` is `Copy`. - Quantified variables now support associated types: `forall(|x: Self::SomeAssocType| ...)` Co-authored-by: Jonas Hansen <ganymed92@gmail.com>

bors · 2022-07-20T09:22:16Z

Build failed:

all-tests (ubuntu-latest)

Aurel300 · 2022-07-22T08:52:20Z

@vakaras Could you have a look at the two failures here? I think they are the last ones before I can merge this and they are happening only in the unsafe core proof version.

…-flag

Aurel300 · 2022-07-29T16:16:22Z

bors r+

980: WIP: Iterator tracking issues r=Aurel300 a=vl0w Some (smaller / bigger) changes needed to enable iterator support (WIP / tracking PR) - Moved normalization of constraint param env (for assoc types) for better logging - Fixed a bug in `SpecGraph`: Preconditions of the base spec were copied to the constrained spec - Ghost constraint resolving is a bit relaxed (`predicate_may_hold` instead of `predicate_must_hold_considering_regions`) to account for references in associated types. See test `associated_types_6.rs` - `merge_generics` now also merges lifetimes to accout for lifetimes appearing in `#[refine_trait_spec]` - Lifetimes in type models are not converted to the anonymous lifetime `'_` anymore - Do not `#[derive(Copy, Clone]` on type models, because the derive macro "conditionally" implements it when generics are involved. That is, `#[derive(Copy)] struct Foo<T>` adds `impl<T: Copy> Copy for Foo {}`, but we do not want to implement `Copy` only if `T` is `Copy`. - Quantified variables now support associated types: `forall(|x: Self::SomeAssocType| ...)` Co-authored-by: Jonas Hansen <ganymed92@gmail.com>

bors · 2022-07-29T19:46:51Z

Build failed:

test-crates

1123: Snapshot equality r=Aurel300 a=Aurel300 Pulling this out of #980. `@vakaras` Co-authored-by: Aurel Bílý <aurel.bily@gmail.com>

1135: Generics improvements r=Aurel300 a=Aurel300 - [x] Improved associated types resolution (thanks `@vl0w,` from #980). The hope is that this won't erase too many regions... - [x] Normalise associated types when monomorphising MIR bodies for pure functions. - [x] Cache encoded pure functions by `DefId` + (full) encoded signature, not just "type parameters". Co-authored-by: Aurel Bílý <aurel.bily@gmail.com> Co-authored-by: Jonas <ganymed92@gmail.com>

vl0w force-pushed the iterators-feature-flag branch 3 times, most recently from 546c701 to fb7d09e Compare April 28, 2022 09:53

vl0w added 6 commits April 28, 2022 15:35

Adjust copy check in environment to better handle regions

4caee3a

Maybe we need to handle TyKind::Ref differently?

ed7dffd

Support associated types in copy check

03b3640

Pass type with binder to type_is_copy to better account for regions

138d98e

Normalize function signature in PureFunctionEncoder to account for as…

a408861

…sociated types

Remove check for validity of pure function in process_encoding_queue

dbbed0d

vl0w force-pushed the iterators-feature-flag branch from fb7d09e to 3e7d676 Compare April 28, 2022 13:37

vl0w added 2 commits April 28, 2022 16:27

Erase all regions in copy check

161b956

Do not perform normalization when there are no projections

eda1445

vl0w force-pushed the iterators-feature-flag branch from 3e7d676 to 0cb7c15 Compare April 28, 2022 14:32

vl0w added 2 commits April 28, 2022 17:16

Partially undo removal of code in process_encoding_queue.

41aad37

Rename normalize_to, return original value if normalized value contai…

e2a5467

…ns infer types

vl0w force-pushed the iterators-feature-flag branch 2 times, most recently from 32ccf0e to ae6589d Compare April 28, 2022 17:46

Pass ParamEnv to resolve_assoc_types, make it fallible

43a5387

vl0w force-pushed the iterators-feature-flag branch 4 times, most recently from 12f63cf to ec42da1 Compare April 29, 2022 12:51

vl0w added 7 commits April 29, 2022 20:44

Small cleanups

b604cd4

Add custom iterator tests

5dc9705

Add flag to add experimental iterator support

f8f2859

Move predicate normalization in constraint solver for better debugging

0da3287

Do not copy preconditions of base spec to constrained spec

c1cbead

Use predicate_must_hold_modulo_regions when resolving ghost constrain…

59bc78c

…ts to account for references in associated types

Handle lifetimes in merge_generics

0af45d7

vl0w force-pushed the iterators-feature-flag branch from ec42da1 to 0af45d7 Compare April 29, 2022 18:49

Aurel300 force-pushed the iterators-feature-flag branch from 4197345 to c038711 Compare July 20, 2022 08:44

fix

186e97e

Aurel300 force-pushed the iterators-feature-flag branch from c038711 to 186e97e Compare July 20, 2022 10:21

Aurel300 added 2 commits July 22, 2022 12:29

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

8ed4eb2

…-flag

erase regions less eagerly for method calls

dbd4d2d

Aurel300 force-pushed the iterators-feature-flag branch from 1a06b91 to dbd4d2d Compare July 27, 2022 10:57

Aurel300 added 2 commits July 27, 2022 13:12

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

1eaa7d0

…-flag

fix

c74215b

Aurel300 force-pushed the iterators-feature-flag branch from 6e53b86 to c74215b Compare July 27, 2022 14:02

Aurel300 self-assigned this Jul 28, 2022

Aurel300 added 2 commits July 29, 2022 16:10

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

e9e5c78

…-flag

another unsafe core proof workaround for trait resolution

fa449f9

Aurel300 force-pushed the iterators-feature-flag branch from 280af36 to fa449f9 Compare July 29, 2022 14:44

Aurel300 mentioned this pull request Aug 8, 2022

Snapshot equality #1123

Merged

bors bot added a commit that referenced this pull request Aug 8, 2022

Merge #1123

43cb956

1123: Snapshot equality r=Aurel300 a=Aurel300 Pulling this out of #980. `@vakaras` Co-authored-by: Aurel Bílý <aurel.bily@gmail.com>

Aurel300 mentioned this pull request Aug 9, 2022

First class support for type parameters in VIR #187

Closed

Aurel300 pushed a commit to Aurel300/prusti-dev that referenced this pull request Aug 17, 2022

assoc type normaliser by Jonas (viperproject#980)

a33199b

Aurel300 mentioned this pull request Aug 17, 2022

Generics improvements #1135

Closed

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

WIP: Iterator tracking issues#980

WIP: Iterator tracking issues#980
vl0w wants to merge 45 commits intoviperproject:masterfrom
vl0w:iterators-feature-flag

vl0w commented Apr 27, 2022 •

edited

Loading

Uh oh!

Aurel300 commented Jul 19, 2022

Uh oh!

bors bot commented Jul 19, 2022

Uh oh!

Aurel300 commented Jul 20, 2022

Uh oh!

bors bot commented Jul 20, 2022

Uh oh!

Aurel300 commented Jul 22, 2022

Uh oh!

Aurel300 commented Jul 29, 2022

Uh oh!

bors bot commented Jul 29, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

vl0w commented Apr 27, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Aurel300 commented Jul 19, 2022

Uh oh!

bors bot commented Jul 19, 2022

Uh oh!

Aurel300 commented Jul 20, 2022

Uh oh!

bors bot commented Jul 20, 2022

Uh oh!

Aurel300 commented Jul 22, 2022

Uh oh!

Aurel300 commented Jul 29, 2022

Uh oh!

bors bot commented Jul 29, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

vl0w commented Apr 27, 2022 •

edited

Loading