Small fixes

[JonasAlaif]

Kinda fixes #878 but would prefer if @vakaras looked at it/made it less hacky

[vakaras]

I am not sure about the removed asserts, but other changes look good to me.

[JonasAlaif]

@vakaras if I convert this line:

prusti-dev/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs

Line 137 in d53bdd7

let qvar_ty = encoder.encode_type(arg_ty).unwrap();

to:

let qvar_ty = encoder.encode_type(arg_ty).unwrap().convert_to_snapshot();

Quantification over generic types works... but I probably shouldn't use convert_to_snapshot here, but instead SnapshotEncoder::encode_type. The issue is that fn encode_quantifier() only gets a encoder: &Encoder and not SnapshotEncoder - is there any way to get the latter to this function?

[vakaras]

@vakaras if I convert this line:

prusti-dev/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs

Line 137 in d53bdd7

let qvar_ty = encoder.encode_type(arg_ty).unwrap();

to:

let qvar_ty = encoder.encode_type(arg_ty).unwrap().convert_to_snapshot();

Quantification over generic types works... but I probably shouldn't use convert_to_snapshot here, but instead SnapshotEncoder::encode_type. The issue is that fn encode_quantifier() only gets a encoder: &Encoder and not SnapshotEncoder - is there any way to get the latter to this function?

Isn't the snapshot encoder, a field of the encoder? Anyway, the code was written by @Aurel300, so he could probably tell more.

[Aurel300]

Yeah the snapshot encoder works with the usual interface trait + state mechanism now. So, if you import crate::encoder::snapshot::SnapshotEncoderInterface, you can call the encode_snapshot_type method on Encoder. It also takes a SubstMap (which should eventually be SubstRef maybe) so generics should get properly monomorphised at the callsite.

[JonasAlaif]

Requires #895 now

[JonasAlaif]

Will merge this today or tomorrow if there are no objections? Though it's a small change it should actually improve generics support quite a bit

[Aurel300]

@JonasAlaif Can I try to get #899 in first?

[JonasAlaif]

@Aurel300 sounds good, looks like that might also fix some of the issues I might be running into with the test I just added. Let's see

[Aurel300]

Status: I found some problems with generics and extern specs still. WIP but I think the test you added @JonasAlaif should be supported soon.

(Some notes:)

The wrappers (from extern spec desugaring) are not inherited the same way that is_pure is. This can result in an annoying de-sync where an implementation (e.g. of Ord) is known to be pure but cannot be encoded because it would attempt to encode a non-local DefId. Extern spec wrappers should really disappear completely, and the DefSpecificationMap should have keys of DefId instead of only LocalDefId.

The reason the wrappers exist in the first place is because PureFunctionEncoder (and by extension the backwards interpreter and MIR encoder) are mis-used to encode call infos (encode_pure_function_use) and Prusti expressions (encode_body). I extracted the latter to a separate method and made fewer things in the PureFunctionEncoder depend on an MIR body to fix the former.

[Aurel300]

bors r+

[bors]

Build succeeded:

• all-tests (macos-latest)
• all-tests (ubuntu-latest)
• all-tests (windows-latest)
• clippy-check
• fmt-check
• purification-tests
• test-crates