Layout guarantee information draft#1325
Conversation
…ut guarantees fully target-agnostic
| Serialize, | ||
| Deserialize, |
There was a problem hiding this comment.
Please remove these two whenever there's also De/SerializeState
There was a problem hiding this comment.
Funny thing, I believe at least ItemId requires both. It needs to be stateful to work in TranslatedCrate::item_names, but needs to be stateless for use in DeclarationGroup.
There was a problem hiding this comment.
Ah, this is hitting a limitation of serde_state I should fix :/ It's just that it doesn't support mixing stateless and using a custom serialization function.
| /// The basic building blocks of symbolic layout information. | ||
| #[derive(Debug, Clone, PartialEq, Eq, SerializeState, DeserializeState, Drive, DriveMut)] | ||
| #[serde_state(state_implements = HashConsSerializerState)] | ||
| pub enum LayoutGuaranteeAtom { |
There was a problem hiding this comment.
Does this always represent a symbolic number of bits?
There was a problem hiding this comment.
It represents a number of bytes, but yes, its always a symbolic of concrete number of bytes. For some types, knowing the target suffices to know the number of bytes, but since the type could also be a DST, it might still be an indeterminable number.
| /// Stores the exact alignments for most primitive types. | ||
| #[derive(Clone, Drive, DriveMut, Serialize, Deserialize)] | ||
| pub struct TargetAlignments { | ||
| pub i1_align: types::ByteCount, |
There was a problem hiding this comment.
That's a good question. Rustc has it, LLVM has it, and so I simply kept it. I currently use it for the alignment of booleans, bu I don't know whether that's correct.
There was a problem hiding this comment.
That isn't correct, booleans are aligned like u8. Looking through rustc, it's indeed used to align 1-bit integers, I just have no idea how one may come about
There was a problem hiding this comment.
Let's remove it until we have a use for it
| /// A structure that computes and stores originally symbolic layouts, which have been | ||
| /// concretized as much as possible. Will not be used during translation. | ||
| pub struct Concretizer { | ||
| computed_layouts: SeqHashMap<Ty, LayoutGuarantees>, | ||
| curr_requested: HashSet<Ty>, | ||
| } |
There was a problem hiding this comment.
What's "concretized"? Is this just "normalized"? The API I'd imagine for that would be:
pub struct LayoutComputer<'a> {
krate: &'a TranslatedCrate,
target: TargetTriple,
cache: HashMap<Ty, LayoutGuarantee>,
/// Stack to bail on cycles in the computation.
stack: Vec<Ty>,
}
impl LayoutComputer<'a> {
pub fn new(krate: &'a TranslatedCrate, target: Option<TargetTriple>) -> Self { ... }
/// Computes the most precise layout guarantees we can deduce for this type.
pub fn compute_layout(&self, ty: Ty) -> LayoutGuarantees { ... }
}There was a problem hiding this comment.
I'm open to bikeshedding the name. For me, it concretizes the layout guarantees, since it inserts concrete values where possible. Normalizing for me could also mean just rearranging the purely symbolic expressions.
Your API looks nice and I'll use it as the basis for further iterations.
There was a problem hiding this comment.
Normalizing for me could also mean just rearranging the purely symbolic expressions.
Well yeah, that's what it has to do in cases where fully concrete cannot be obtained, e.g. for any repr(Rust) layout
|
|
||
| /// Composite symbolic layout expressions. | ||
| /// | ||
| /// `non_exhaustive` since we might need many more composite layouts. |
There was a problem hiding this comment.
You didn't actually make it non_exaustive
| #[derive(Clone, Drive, DriveMut, Serialize, Deserialize)] | ||
| pub struct TargetAlignments { | ||
| pub i1_align: types::ConcreteByteCount, | ||
| pub i8_align: types::ConcreteByteCount, | ||
| pub i16_align: types::ConcreteByteCount, | ||
| pub i32_align: types::ConcreteByteCount, | ||
| pub i64_align: types::ConcreteByteCount, | ||
| pub i128_align: types::ConcreteByteCount, | ||
| pub f16_align: types::ConcreteByteCount, | ||
| pub f32_align: types::ConcreteByteCount, | ||
| pub f64_align: types::ConcreteByteCount, | ||
| pub f128_align: types::ConcreteByteCount, | ||
| pub ptr_align: types::ConcreteByteCount, | ||
| } |
There was a problem hiding this comment.
why not just make this a map from LiteralType to ConcreteByteCount? seems more exhaustive
There was a problem hiding this comment.
That would certainly be an option, if we can make it a cheap map. The current version is really just a direct translation of what rustc has.
There was a problem hiding this comment.
I agree it seems more usable as a map (just use a SeqHashMap, we're not optimizing for speed in our representation)
3 participants
This PR is a first draft of how Charon could support (partially) symbolic layout guarantee information. To make the draft more self-contained and easier to review, all relevant parts are in the new file
charon/src/ast/layout_guarantees.rs. Additional changes required for this PR can be found in other files, some of which should and probably will be extracted into their own PRs.About layout guarantees
Layout guarantees are (partially symbolic) expressions that describe what Rust guarantees about the layout of a type. I've tried to always refer to the reference in the code to keep everything in sync. In general, these guarantees can be computed for polymorphic types and are target-agnostic, but can be concretized/instantiated for specific type arguments and targets if needed (currently only implemented in Rust, not in OCaml).
The draft is insofar complete as it can compute layout guarantees for most types (an open question are DSTs). Further open points for future discussion are the following:
SizedTypeProperties, but symbolically.One ui test currently fails, but I was not able to figure out what exactly goes wrong and how to fix it.The problem now gets circumvented.