From patchwork Fri Jun 17 09:39:43 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Tomas_H=C3=A4rdin?= X-Patchwork-Id: 36299 Delivered-To: ffmpegpatchwork2@gmail.com Received: by 2002:a05:6a20:1a22:b0:84:42e0:ad30 with SMTP id cj34csp26420pzb; Fri, 17 Jun 2022 02:40:12 -0700 (PDT) X-Google-Smtp-Source: AGRyM1uMxtbpb6U5wK8Y2HKQKb4lbz2nsg8soWHKb05DJcKzgLyYs5X7iH8flHFLbA+oaGcSFA+K X-Received: by 2002:a05:6402:61a:b0:433:406a:8d25 with SMTP id n26-20020a056402061a00b00433406a8d25mr11246865edv.276.1655458811979; Fri, 17 Jun 2022 02:40:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1655458811; cv=none; d=google.com; s=arc-20160816; b=bH0IC98cwrGmWpeiTdqOIDtLbSGuLfPbHsqZH/jNiqkTFeEexZXRpiTfGMtF6aEwk5 YEwN74/8YAqTaN3tShxU6GztnVzQWeiWR23F78Tx/5pbagfqIs+AhEFyW24tqQkEBlgX l3MTqzBHUUYkDh2k7+pu6R+tZeZopqxeWLRB7j7GCKNtidG0jh8YJAoVJGhBa18slt4N pR4+U2affM2IkQJBAKSMhR4sg1MycMiy78xvX2xoUdzjDD3JEmyMDOlvz8PWagETtOYh rURJ2EoUdbs5nHGavVCkzh7fRkulBsHDBys0C5VAOjoXW0xMNsw6zHJvcFIP9Q5Al6r2 uHNw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence:subject :mime-version:user-agent:date:to:from:message-id:dkim-signature :dkim-signature:delivered-to; bh=HR/KQIm9keY9XP+lSNi/LgweI8wJuWzanL2wHWWQtA8=; b=PY0am6EvFABhebWZKQL/cO1+qfTRbkyjaI2Mf5IBQm4Jx4UfOGuT5dZmWDtKsgigxS aTF5DPSlHevmB+uIR5p6RkxuvOSuWoYORPcOUj6TbTCxBUFv+FPW0fV2OKBVtluelOH+ G0RXajnhqpILgtudtv4STmD7NOscc2EoBvvpoP7CdX2KP//LioW3fQG88bda/F5Zws1H XXVQ0yjWDnrnAeOufQ997ST9gziPVsIIJAzbV1S1mke+N458ZAJ8XllFM+JzztW1gQA8 9WZpEmaVwKnhPNIP9oRUWC7t3gkAfJrp6f7Rlh4DzZes8lPRp/HJcmv4HrTMaqzVqO5f tAOw== ARC-Authentication-Results: i=1; mx.google.com; dkim=neutral (body hash did not verify) header.i=@acc.umu.se header.s=mail1 header.b=fAgSSYu7; dkim=neutral (body hash did not verify) header.i=@acc.umu.se header.s=mail1 header.b=fAgSSYu7; spf=pass (google.com: domain of ffmpeg-devel-bounces@ffmpeg.org designates 79.124.17.100 as permitted sender) smtp.mailfrom=ffmpeg-devel-bounces@ffmpeg.org; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=acc.umu.se Return-Path: Received: from ffbox0-bg.mplayerhq.hu (ffbox0-bg.ffmpeg.org. [79.124.17.100]) by mx.google.com with ESMTP id o10-20020a170906974a00b006fec90d6c9fsi800132ejy.305.2022.06.17.02.39.56; Fri, 17 Jun 2022 02:40:11 -0700 (PDT) Received-SPF: pass (google.com: domain of ffmpeg-devel-bounces@ffmpeg.org designates 79.124.17.100 as permitted sender) client-ip=79.124.17.100; Authentication-Results: mx.google.com; dkim=neutral (body hash did not verify) header.i=@acc.umu.se header.s=mail1 header.b=fAgSSYu7; dkim=neutral (body hash did not verify) header.i=@acc.umu.se header.s=mail1 header.b=fAgSSYu7; spf=pass (google.com: domain of ffmpeg-devel-bounces@ffmpeg.org designates 79.124.17.100 as permitted sender) smtp.mailfrom=ffmpeg-devel-bounces@ffmpeg.org; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=acc.umu.se Received: from [127.0.1.1] (localhost [127.0.0.1]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id 1C81868B89A; Fri, 17 Jun 2022 12:39:53 +0300 (EEST) X-Original-To: ffmpeg-devel@ffmpeg.org Delivered-To: ffmpeg-devel@ffmpeg.org Received: from mail.acc.umu.se (unknown [130.239.18.156]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTPS id 14B1568B887 for ; Fri, 17 Jun 2022 12:39:46 +0300 (EEST) Received: from localhost (localhost.localdomain [127.0.0.1]) by amavisd-new (Postfix) with ESMTP id D469144DEC for ; Fri, 17 Jun 2022 11:39:44 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=acc.umu.se; s=mail1; t=1655458784; bh=tLv6TPLopVRWd8BgVE8gBplLgIn/HcxJLlxpg02/EKI=; h=Subject:From:To:Date:From; b=fAgSSYu73gmCEpZMg9tWbUsQxXi1ZSn19ASV9EJhDh+ODhnCydV2sSJ/8gg7stk6s IczxahRSm2gZVS+D8W4yH+eZl9XBc1xxusrBcpA68s4VUgpNbFN1V0P8iVJuYSx+T4 Ip7qO7XqRohYF5PxncJktvtuMeNUR9JZQcHUM0rho39C5zAExG79v7qPav8K0LJGZs B5oXb7vTYx+RR6eiuAeh6gM+u1cUD6Wpyg2MrGXXQf5T/MaIGf/3yfDAK54GrE2GIg 4rMlgscNO3q05UKwpbBxCTNzR8IAfWvLx0/2obbb/z64pZkQQVDoR1zOxfeWoerU/f AuPFL1kxs9A/Q== Received: from debian.lan (unknown [IPv6:2a00:66c0:a::72c]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) (Authenticated sender: tjoppen) by mail.acc.umu.se (Postfix) with ESMTPSA id E63A444DDA for ; Fri, 17 Jun 2022 11:39:43 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=acc.umu.se; s=mail1; t=1655458784; bh=tLv6TPLopVRWd8BgVE8gBplLgIn/HcxJLlxpg02/EKI=; h=Subject:From:To:Date:From; b=fAgSSYu73gmCEpZMg9tWbUsQxXi1ZSn19ASV9EJhDh+ODhnCydV2sSJ/8gg7stk6s IczxahRSm2gZVS+D8W4yH+eZl9XBc1xxusrBcpA68s4VUgpNbFN1V0P8iVJuYSx+T4 Ip7qO7XqRohYF5PxncJktvtuMeNUR9JZQcHUM0rho39C5zAExG79v7qPav8K0LJGZs B5oXb7vTYx+RR6eiuAeh6gM+u1cUD6Wpyg2MrGXXQf5T/MaIGf/3yfDAK54GrE2GIg 4rMlgscNO3q05UKwpbBxCTNzR8IAfWvLx0/2obbb/z64pZkQQVDoR1zOxfeWoerU/f AuPFL1kxs9A/Q== Message-ID: <368f137a159a728214b6bd4e72b6bdcc8ff80684.camel@acc.umu.se> From: Tomas =?iso-8859-1?q?H=E4rdin?= To: FFmpeg development discussions and patches Date: Fri, 17 Jun 2022 11:39:43 +0200 User-Agent: Evolution 3.38.3-1 MIME-Version: 1.0 Subject: [FFmpeg-devel] [PATCH] lavu/mem: Add av_fast_recalloc(), formally verify *size X-BeenThere: ffmpeg-devel@ffmpeg.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: FFmpeg development discussions and patches List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-To: FFmpeg development discussions and patches Errors-To: ffmpeg-devel-bounces@ffmpeg.org Sender: "ffmpeg-devel" X-TUID: fyLu3Vw2qPlG 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?= 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