[BLOCKED] Builtin trait encoder#154
Conversation
| const TUPLE_TRAIT_ARGS: <(vir::ManyTyVal, vir::ManyCSnap) as vir::Arity>::Tys<'static> = | ||
| (&[vir::TYPE_TYVAL], &[]); | ||
|
|
||
| impl TaskEncoder for TupleTraitEnc { |
There was a problem hiding this comment.
In general there is way too much duplication between this and the Sized encoder. If we want to have something like this for all special traits, then this really needs to be reduced a lot to avoid copy-paste errors. At a glance it seems we'll need the encoder to do the same things but the code which checks whether a particular input implements the type is a bit different?
How about a single BuiltinTraitEnc<T: BuiltinTrait> and then trait BuiltinTrait which has the bit of code that actually changes between the encoders?
There was a problem hiding this comment.
Played around with it. Due to the caching with static, we cannot have impl<T: BuiltinTrait> TaskEncoder for BuiltinTraitEnc<T> { ... }. I'll try to reuse the functionality in other ways.
There was a problem hiding this comment.
I have extracted the shared logic. Not 100% loving it the solution but please let me know what you think about it.
|
And a separate question regarding special traits: right now you are invoking all the special trait encoders unconditionally from |
The issue is that we cannot know ahead of time whether we will be using a certain We somehow need to "record" all types that get fed to |
That's not exactly the issue, right: we must be requesting the
Is there sufficient information in ( |
Aurel300
changed the title
I'm not sure about moving to Also we only actually care about |
3 participants
This PR introduces a framework for encoding Rust's builtin traits. Specifically, it adds support for the
SizedandTupletraits as examples.In Rust, traits like
SizedandTupleare not defined through standard source-code declarations but are instead handled by the compiler's logic. To accurately verify Rust code, Prusti needs to know which types implement these traits.Key Changes
1. Builtin Trait Encoder
This PR implements a generic
BuiltinTraitEnc<T: BuiltinTrait>that depends onBuiltinTraitto provide trait specific logic.To avoid emitting outputs when not necessary, the builtin trait encoder must be "activated" by the
TraitEncwhen the latter encounters the corresponding builtin.2. Specialized Logic for
SizedandTupleThis PR provides concrete implementations for the
SizedandTupletraits.SizedTrait: Decides whether a type is (conditionally) sized, by matching whatrustcdoes internally.TupleTrait: Decides whether a given type is a tuple.3.
RustTymodificationThe PR modifies
RustTyto also preserve information about the original rust type, but in its "erased" form - meaning the type is stripped of its usage context.The erased type information is useful as it simplifies the encoding of the checks in the builtin trait encoder.
Rough points
We always compute the checks for all types for builtin traits, even though we might not always emit them.
Blocked by #137