Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 12 additions & 2 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -244,10 +244,11 @@ jobs:
# publishes the length afterwards, including on the unwind paths its tests
# drive. `PreSized` (encode_sink.rs) writes a message into a sink's
# uninitialised spare capacity and advances the sink by the bytes written.
# The table interpreters (table/) access message fields through raw pointers.
# Miri tracks per-byte init state, so this job mechanically verifies these
# invariants on every path those test modules exercise. Scoped to them to
# keep the (interpreted, slow) run fast — under a minute steady state, so it
# runs on every PR as a blocking gate rather than on a nightly schedule.
# keep the (interpreted, slow) run fast, so it runs on every PR as a blocking
# gate rather than on a nightly schedule.
#
# The nightly is PINNED (not floating): a required check must not be broken by
# an unrelated bad nightly. Bump MIRI_TOOLCHAIN occasionally; the sysroot
Expand Down Expand Up @@ -284,6 +285,15 @@ jobs:
cargo +${{ env.MIRI_TOOLCHAIN }} miri test -p buffa --
size_cache copy_into_spare encode_sink::tests contiguous_sink_

# The table interpreters (table/) read and write message fields through
# raw pointers at offsets from a `Table`. Miri checks the pointer
# provenance, alignment and initialisation on the kinds and field
# shapes the module's tests build, including message fields stored
# inline, boxed and in a `Vec`, whose child pointers point into the
# parent or the heap.
- name: Miri (table interpreter soundness)
run: cargo +${{ env.MIRI_TOOLCHAIN }} miri test -p buffa --lib -- 'table::'

# OwnedView: the view borrows from the Bytes it is stored beside, with
# forged 'static lifetimes hidden behind a MaybeDangling wrapper. Miri
# turns a wrong field order (a dangling borrow while the view's
Expand Down
30 changes: 30 additions & 0 deletions buffa/src/encode_sink.rs
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,30 @@ pub trait EncodeSink {
#[doc(hidden)]
const __PRE_SIZED: bool = false;

/// Run `f` on this sink if it is a [`PreSized`] cursor, and return
/// whether it did.
///
/// Lets the table interpreters switch, once per message, from an instance
/// generic over the sink to one compiled in this crate. `f` gets the
/// cursor itself, and a `PreSized` cannot be built or altered outside this
/// crate, so `f` cannot claim more bytes than were written:
///
/// ```compile_fail,E0616
/// use buffa::EncodeSink;
///
/// let mut vec: Vec<u8> = Vec::new();
/// vec.__with_pre_sized(&mut |cursor| cursor.pos = 4);
/// ```
///
/// Implementations outside this crate keep the default, which does not
/// call `f`.
#[doc(hidden)]
#[inline]
fn __with_pre_sized(&mut self, f: &mut dyn FnMut(&mut PreSized<'_>)) -> bool {
let _ = f;
false
}

/// Run `fill` over `len` bytes of contiguous space at the end of the
/// sink and append the bytes it wrote, or give `fill` back unrun if the
/// sink's current chunk is shorter than `len`.
Expand Down Expand Up @@ -271,6 +295,12 @@ impl<'a> PreSized<'a> {
}

impl EncodeSink for PreSized<'_> {
#[inline]
fn __with_pre_sized(&mut self, f: &mut dyn FnMut(&mut PreSized<'_>)) -> bool {
f(self);
true
}

#[inline]
fn put_u8(&mut self, value: u8) {
let Some(slot) = self.dst.get_mut(self.pos) else {
Expand Down
4 changes: 4 additions & 0 deletions buffa/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -236,6 +236,10 @@ pub mod message_field;
pub mod message_set;
pub mod oneof;
mod size_cache;
// Runtime for table-driven message codecs, called by generated code; see the
// module docs.
#[doc(hidden)]
pub mod table;
#[cfg(test)]
pub(crate) mod test_doubles;
#[cfg(feature = "text")]
Expand Down
Loading
Loading