From 3d5ada268988542172953df67fdde58b49eb4f99 Mon Sep 17 00:00:00 2001 From: Philip Withnall Date: Thu, 19 Sep 2024 16:35:27 +0100 Subject: [PATCH] =?UTF-8?q?gvariant-parser:=20Add=20a=20proof=20for=20patt?= =?UTF-8?q?ern=5Fcoalesce()=E2=80=99s=20safety?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This proof backs up the already-present assertion that “the length of the output is loosely bounded by the sum of the input lengths”. Signed-off-by: Philip Withnall Helps: #3469 --- glib/gvariant-parser.c | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/glib/gvariant-parser.c b/glib/gvariant-parser.c index dc8cb3e5a..81d96ee29 100644 --- a/glib/gvariant-parser.c +++ b/glib/gvariant-parser.c @@ -401,6 +401,8 @@ token_stream_end_ref (TokenStream *stream, ref->end = stream->stream - stream->start; } +/* This is guaranteed to write exactly as many bytes to `out` as it consumes + * from `in`. i.e. The `out` buffer doesn’t need to be any longer than `in`. */ static void pattern_copy (gchar **out, const gchar **in) @@ -436,9 +438,12 @@ pattern_coalesce (const gchar *left, /* the length of the output is loosely bound by the sum of the input * lengths, not simply the greater of the two lengths. * - * (*(iii)) + ((iii)*) ((iii)(iii)) + * (*(iii)) + ((iii)*) = ((iii)(iii)) * - * 8 + 8 = 12 + * 8 + 8 = 12 + * + * This can be proven by the fact that `out` is never incremented by more + * bytes than are consumed from `left` or `right` in each iteration. */ buflen = strlen (left) + strlen (right); out = result = g_malloc (buflen);