From 9231ec68345c5286cad3537ef9f1d2844ba169b9 Mon Sep 17 00:00:00 2001 From: Timon Meyer Date: Wed, 1 Nov 2023 09:15:17 +0100 Subject: [PATCH 1/3] introduce offset type alias --- spec/lang/syntax.md | 4 ++-- spec/lang/types.md | 4 ++-- spec/mem/basic.md | 2 +- spec/prelude/main.md | 2 ++ tooling/miniutil/src/build/ty.rs | 4 ++-- tooling/miniutil/src/fmt/ty.rs | 2 +- 6 files changed, 10 insertions(+), 8 deletions(-) diff --git a/spec/lang/syntax.md b/spec/lang/syntax.md index 298697b0..5fb79312 100644 --- a/spec/lang/syntax.md +++ b/spec/lang/syntax.md @@ -341,7 +341,7 @@ pub struct Global { /// Cross-references pointing to other global allocations, /// together with an offset, expressing where this allocation should put the pointer. /// Note that the pointers created due to relocations overwrite the data given by `bytes`. - pub relocations: List<(Size, Relocation)>, + pub relocations: List<(Offset, Relocation)>, /// The alignment with which this global shall be allocated. pub align: Align, } @@ -351,6 +351,6 @@ pub struct Relocation { /// The name of the global allocation we are pointing into. pub name: GlobalName, /// The offset within that allocation. - pub offset: Size, + pub offset: Offset, } ``` diff --git a/spec/lang/types.md b/spec/lang/types.md index c76a6e9d..53443f7b 100644 --- a/spec/lang/types.md +++ b/spec/lang/types.md @@ -47,7 +47,7 @@ pub enum Type { /// preserved, and data between chunks is lost (like padding in a struct). /// This is necessary to model the behavior of some `repr(C)` unions, see /// for details. - chunks: List<(Size, Size)>, // (offset, length) for each chunk. + chunks: List<(Offset, Size)>, /// The total size of the union, can indicate padding after the last chunk. size: Size, /// Total alignment of the union. Due to `repr(packed)` and `repr(align)`, @@ -79,7 +79,7 @@ pub struct IntType { pub size: Size, } -pub type Fields = List<(Size, Type)>; // (offset, type) pair for each field +pub type Fields = List<(Offset, Type)>; /// We leave the details of enum tags to the future. /// (We might want to extend the "variants" field of `Enum` to also have a diff --git a/spec/mem/basic.md b/spec/mem/basic.md index c61a29b6..808c2e8c 100644 --- a/spec/mem/basic.md +++ b/spec/mem/basic.md @@ -204,7 +204,7 @@ impl BasicMemory { throw_ub!("out-of-bounds memory access"); } // All is good! - ret(Some((id, Size::from_bytes(offset_in_alloc).unwrap()))) + ret(Some((id, Offset::from_bytes(offset_in_alloc).unwrap()))) } } diff --git a/spec/prelude/main.md b/spec/prelude/main.md index ad1bff09..ca827e87 100644 --- a/spec/prelude/main.md +++ b/spec/prelude/main.md @@ -9,6 +9,8 @@ pub use libspecr::prelude::*; /// Make the two main modules available. pub use crate::{lang, mem}; +pub type Offset = Size; + /// All operations are fallible, so they return `Result`. If they fail, that /// means the program caused UB or put the machine to a halt. pub type Result = std::result::Result; diff --git a/tooling/miniutil/src/build/ty.rs b/tooling/miniutil/src/build/ty.rs index ae6e9615..691181b6 100644 --- a/tooling/miniutil/src/build/ty.rs +++ b/tooling/miniutil/src/build/ty.rs @@ -38,7 +38,7 @@ pub fn raw_ptr_ty() -> Type { Type::Ptr(PtrType::Raw) } -pub fn tuple_ty(f: &[(Size, Type)], size: Size, align: Align) -> Type { +pub fn tuple_ty(f: &[(Offset, Type)], size: Size, align: Align) -> Type { Type::Tuple { fields: f.iter().copied().collect(), size, @@ -46,7 +46,7 @@ pub fn tuple_ty(f: &[(Size, Type)], size: Size, align: Align) -> Type { } } -pub fn union_ty(f: &[(Size, Type)], size: Size, align: Align) -> Type { +pub fn union_ty(f: &[(Offset, Type)], size: Size, align: Align) -> Type { let chunks = list![(Size::ZERO, size)]; Type::Union { fields: f.iter().copied().collect(), diff --git a/tooling/miniutil/src/fmt/ty.rs b/tooling/miniutil/src/fmt/ty.rs index edfee15f..4f513045 100644 --- a/tooling/miniutil/src/fmt/ty.rs +++ b/tooling/miniutil/src/fmt/ty.rs @@ -166,7 +166,7 @@ fn fmt_comptype_fields(fields: Fields, comptypes: &mut Vec) -> String s } -fn fmt_comptype_chunks(chunks: List<(Size, Size)>) -> String { +fn fmt_comptype_chunks(chunks: List<(Offset, Size)>) -> String { let mut s = String::new(); for (offset, size) in chunks { let offset = offset.bytes(); From 6d18b412a9790081defaf595f9205bda8178ef6e Mon Sep 17 00:00:00 2001 From: Timon Meyer Date: Wed, 1 Nov 2023 09:26:04 +0100 Subject: [PATCH 2/3] Rename Size to Offset in minimize where applicable --- tooling/minimize/src/chunks.rs | 4 ++-- tooling/minimize/src/constant.rs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tooling/minimize/src/chunks.rs b/tooling/minimize/src/chunks.rs index 855e26cc..603cbb29 100644 --- a/tooling/minimize/src/chunks.rs +++ b/tooling/minimize/src/chunks.rs @@ -3,7 +3,7 @@ use crate::*; /// Calculates the Chunks for a union type. /// This works roughly as described here: /// https://github.com/rust-lang/unsafe-code-guidelines/issues/354#issuecomment-1297545313 -pub fn calc_chunks(fields: Fields, size: Size) -> List<(Size, Size)> { +pub fn calc_chunks(fields: Fields, size: Size) -> List<(Offset, Size)> { let s = size.bytes().try_to_usize().unwrap(); let mut markers = vec![false; s]; for (offset, ty) in fields { @@ -24,7 +24,7 @@ pub fn calc_chunks(fields: Fields, size: Size) -> List<(Size, Size)> { current_chunk_start = Some(i); } (false, Some(s)) => { - let start = Size::from_bytes(*s).unwrap(); + let start = Offset::from_bytes(*s).unwrap(); let length = Size::from_bytes(i - *s).unwrap(); chunks.push((start, length)); current_chunk_start = None; diff --git a/tooling/minimize/src/constant.rs b/tooling/minimize/src/constant.rs index f17cf2aa..4c5c54b7 100644 --- a/tooling/minimize/src/constant.rs +++ b/tooling/minimize/src/constant.rs @@ -66,7 +66,7 @@ fn translate_const_uneval<'cx, 'tcx>( .eval_to_allocation_raw(rs::ParamEnv::empty().and(cid)) .unwrap(); let name = translate_alloc_id(alloc.alloc_id, fcx); - let offset = Size::ZERO; + let offset = Offset::ZERO; let rel = Relocation { name, offset }; relocation_to_value_expr(rel, ty, fcx) From c76404a218820a2dd90eeb296e0d879eba52ff40 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 1 Nov 2023 19:49:27 +0100 Subject: [PATCH 3/3] add doc comment --- spec/prelude/main.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/spec/prelude/main.md b/spec/prelude/main.md index ca827e87..c7ab576e 100644 --- a/spec/prelude/main.md +++ b/spec/prelude/main.md @@ -9,6 +9,9 @@ pub use libspecr::prelude::*; /// Make the two main modules available. pub use crate::{lang, mem}; +/// When a non-negative integer is used as an offset into an allocation or type +/// rather than to describe the size of an object or type, use this type instead +/// of `Size` for extra clarity. pub type Offset = Size; /// All operations are fallible, so they return `Result`. If they fail, that