[FFmpeg-devel] [PATCH] lavu/mem: Add av_fast_recalloc(), formally verify *size

[FFmpeg-devel] [PATCH] lavu/mem: Add av_fast_recalloc(), formally verify *size

[Tomas Härdin]

[-- Attachment #1: Type: text/plain, Size: 651 bytes --]

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

[-- Attachment #2: 0001-lavu-mem-Add-av_fast_recalloc-formally-verify-size.patch --]
[-- Type: text/x-patch, Size: 6577 bytes --]

From 6f08d504a60814d1ac50e6f237e1765855ab242d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git@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


[-- Attachment #3: Type: text/plain, Size: 251 bytes --]

_______________________________________________
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
https://ffmpeg.org/mailman/listinfo/ffmpeg-devel

To unsubscribe, visit link above, or email
ffmpeg-devel-request@ffmpeg.org with subject "unsubscribe".