I think it's best to send this as a separate patch. I also took some
time yesterday evening to formally verify the size computation because
it relying on overflow irked me. Doing the same with av_fast_realloc()
and av_fast_recalloc() themselves is rather more involved and probably
requires a newer version of frama-c because 20.0 does not support
verifying allocations.
For the uninitiated the lemmas are there to help the provers along. The
/*@ ... */ quote before compute_size() is its contract.
I also now guarantee that av_fast_recalloc() sets *size to a multiple
of elsize, and the size is also such a multiple except when nelem == 0.
/Tomas
From 6f08d504a60814d1ac50e6f237e1765855ab242d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <g...@haerdin.se>
Date: Tue, 14 Jun 2022 13:35:18 +0200
Subject: [PATCH] lavu/mem: Add av_fast_recalloc(), formally verify *size
Using frama-c version 20.0 (Calcium):
frama-c -cpp-extra-args="-Icompat/atomics/gcc" -wp -wp-rte -warn-unsigned-overflow -wp-prover alt-ergo,z3 -wp-fct compute_size libavutil/mem.c
Bump minor version and update Changelog as well
---
Changelog | 1 +
libavutil/mem.c | 56 +++++++++++++++++++++++++++++++++++++++++++--
libavutil/mem.h | 56 +++++++++++++++++++++++++++++++++++++++++++++
libavutil/version.h | 2 +-
4 files changed, 112 insertions(+), 3 deletions(-)
diff --git a/Changelog b/Changelog
index ef589705c4..ff2fc4e9fc 100644
--- a/Changelog
+++ b/Changelog
@@ -21,6 +21,7 @@ version 5.1:
- QOI image format support
- ffprobe -o option
- virtualbass audio filter
+- added av_fast_recalloc() to libavutil
version 5.0:
diff --git a/libavutil/mem.c b/libavutil/mem.c
index a0c9a42849..78e54fabd1 100644
--- a/libavutil/mem.c
+++ b/libavutil/mem.c
@@ -502,7 +502,30 @@ void av_memcpy_backptr(uint8_t *dst, int back, int cnt)
}
}
-void *av_fast_realloc(void *ptr, unsigned int *size, size_t min_size)
+//@ lemma floor_mod: \forall integer x, y; x >= 0 && y >= 1 ==> ((x / y) * y) % y == 0;
+//@ lemma floor_range: \forall integer x, y, z; x >= 0 && y >= 1 && z >= 0 && x <= z ==> (x / y) * y <= (z / y) * y;
+
+/*@
+ requires min_size <= max_size && elsize >= 1 && min_size % elsize == 0;
+ ensures mod: \result % elsize == 0;
+ ensures range: min_size <= \result <= max_size;
+ assigns \nothing;
+ */
+static size_t compute_size(size_t min_size, size_t max_size, size_t elsize)
+{
+ size_t extra = min_size / 16 + 32;
+
+ // avoid unsigned overflow
+ if (min_size > SIZE_MAX - extra)
+ min_size = SIZE_MAX;
+ else
+ min_size = min_size + extra;
+
+ min_size = FFMIN(max_size, min_size);
+ return (min_size / elsize) * elsize;
+}
+
+static void *realloc_inner(void *ptr, unsigned int *size, size_t min_size, size_t elsize)
{
size_t max_size;
@@ -516,7 +539,7 @@ void *av_fast_realloc(void *ptr, unsigned int *size, size_t min_size)
return NULL;
}
- min_size = FFMIN(max_size, FFMAX(min_size + min_size / 16 + 32, min_size));
+ min_size = compute_size(min_size, max_size, elsize);
ptr = av_realloc(ptr, min_size);
/* we could set this to the unmodified min_size but this is safer
@@ -530,6 +553,35 @@ void *av_fast_realloc(void *ptr, unsigned int *size, size_t min_size)
return ptr;
}
+void *av_fast_realloc(void *ptr, unsigned int *size, size_t min_size)
+{
+ return realloc_inner(ptr, size, min_size, 1);
+}
+
+int av_fast_recalloc(void *ptr, unsigned int *size, size_t nelem, size_t elsize)
+{
+ void *val;
+ void *new_ptr;
+ unsigned int new_size = *size;
+ size_t product;
+ int ret;
+ memcpy(&val, ptr, sizeof(val));
+
+ if ((ret = av_size_mult(nelem, elsize, &product)) < 0)
+ return ret;
+
+ if (!(new_ptr = realloc_inner(val, &new_size, product, elsize)))
+ return AVERROR(ENOMEM);
+
+ if (new_size > *size) {
+ memset((uint8_t*)new_ptr + *size, 0, new_size - *size);
+ *size = new_size;
+ memcpy(ptr, &new_ptr, sizeof(new_ptr));
+ }
+
+ return 0;
+}
+
static inline void fast_malloc(void *ptr, unsigned int *size, size_t min_size, int zero_realloc)
{
size_t max_size;
diff --git a/libavutil/mem.h b/libavutil/mem.h
index d91174196c..c2c7c7266a 100644
--- a/libavutil/mem.h
+++ b/libavutil/mem.h
@@ -380,6 +380,62 @@ int av_reallocp_array(void *ptr, size_t nmemb, size_t size);
*/
void *av_fast_realloc(void *ptr, unsigned int *size, size_t min_size);
+/**
+ * Reallocate the pointed-to buffer if it is not large enough, otherwise do
+ * nothing. Old data is memcpy()'d to the start of the new buffer. The newly
+ * allocated space at the end of the buffer is zero-initialized. In other
+ * words the buffer is expanded with zeroes when necessary. The size of the
+ * new buffer may be larger than what is requested, but never smaller.
+ *
+ * If the pointed-to buffer is `NULL`, then a new zero-initialized buffer is
+ * allocated.
+ *
+ * If the pointed-to buffer is not large enough, and reallocation fails,
+ * `AVERROR(ENOMEM)` is returned.
+ *
+ * If nelem*elsize is too large then `AVERROR(EINVAL)` is returned.
+ *
+ * Contrary to av_fast_malloc(), *ptr and *size are not touched in case of
+ * error, to allow for proper cleanup.
+ *
+ * On success *size is guaranteed to be a multiple of elsize.
+ *
+ * This function is intended for use with arrays of structures that contain
+ * pointers that are allowed to grow and typically don't shrink.
+ *
+ * A typical use pattern follows:
+ *
+ * @code{.c}
+ * int foo_work(SomeContext *s) {
+ * if (av_fast_recalloc(&s->foo, &s->foo_size, s->nfoo, sizeof(Foo)))
+ * return AVERROR(ENOMEM);
+ * for (x = 0; x < s->nfoo; x++)
+ * do stuff with s->foo[x]
+ * return 0;
+ * }
+ *
+ * void foo_close(SomeContext *s) {
+ * // note the use of s->foo_size, not s->nfoo
+ * for (x = 0; x < s->foo_size/sizeof(Foo); x++)
+ * av_freep(&s->foo[x].bar);
+ * av_freep(&s->foo);
+ * }
+ * @endcode
+ *
+ * @param[in,out] ptr Pointer to pointer to an already allocated buffer.
+ * `*ptr` will be overwritten with pointer to new
+ * buffer on success and will be left alone on failure
+ * @param[in,out] size Pointer to the size of buffer `*ptr`. `*size` is
+ * updated to the new allocated size and will be left
+ * along on failure.
+ * @param[in] nelem Number of desired elements in *ptr
+ * @param[in] elsize Size of each element in *ptr
+ * @return Zero on success, <0 on error.
+ * @see av_fast_realloc()
+ * @see av_fast_malloc()
+ */
+int av_fast_recalloc(void *ptr, unsigned int *size, size_t nelem, size_t elsize);
+
/**
* Allocate a buffer, reusing the given one if large enough.
*
diff --git a/libavutil/version.h b/libavutil/version.h
index 2e9e02dda8..87178e9e9a 100644
--- a/libavutil/version.h
+++ b/libavutil/version.h
@@ -79,7 +79,7 @@
*/
#define LIBAVUTIL_VERSION_MAJOR 57
-#define LIBAVUTIL_VERSION_MINOR 27
+#define LIBAVUTIL_VERSION_MINOR 28
#define LIBAVUTIL_VERSION_MICRO 100
#define LIBAVUTIL_VERSION_INT AV_VERSION_INT(LIBAVUTIL_VERSION_MAJOR, \
--
2.30.2
_______________________________________________
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
https://ffmpeg.org/mailman/listinfo/ffmpeg-devel
To unsubscribe, visit link above, or email
ffmpeg-devel-requ...@ffmpeg.org with subject "unsubscribe".
