From mboxrd@z Thu Jan 1 00:00:00 1970
Return-Path: <ffmpeg-devel-bounces@ffmpeg.org>
Received: from ffbox0-bg.mplayerhq.hu (ffbox0-bg.ffmpeg.org [79.124.17.100])
by master.gitmailbox.com (Postfix) with ESMTP id DDB1B4ABF9
for <ffmpegdev@gitmailbox.com>; Wed, 15 May 2024 21:29:17 +0000 (UTC)
Received: from [127.0.1.1] (localhost [127.0.0.1])
by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id C6B3868D5F4;
Thu, 16 May 2024 00:29:14 +0300 (EEST)
Received: from relay7-d.mail.gandi.net (relay7-d.mail.gandi.net
[217.70.183.200])
by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTPS id 657AE68D51F
for <ffmpeg-devel@ffmpeg.org>; Thu, 16 May 2024 00:29:07 +0300 (EEST)
Received: by mail.gandi.net (Postfix) with ESMTPSA id 81F6520002
for <ffmpeg-devel@ffmpeg.org>; Wed, 15 May 2024 21:29:06 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=niedermayer.cc;
s=gm1; t=1715808546;
h=from:from:reply-to:subject:subject:date:date:message-id:message-id:
to:to:cc:mime-version:mime-version:content-type:content-type:
in-reply-to:in-reply-to:references:references;
bh=zLYWHF4Nf/o5X1iPECtfnzVjpr1wVW9ExN6fcQC7bJQ=;
b=eSumbNiXEoNvXS8sU77ypuvO7yhnWO98mxDL/jXTHxAdgoBqi6W6CUCZB8jx9KIVj6ZALl
UOYOLxYxFetw7UF6YFTgHFcZAR4EjanzdTWH5zKvxkDvuBYoHgd4z6HVhe0uMWKEJHpJnL
uEwZK7LV/E00tJcK6VRiTNXDm87vgwghT6P9iULh3XPxEOAg98aIqz2zSHNnUAEvbhdAFa
4570Ru/a0LDEXGlT/WSpGR9voEVDPNhOe7V66HiPqK0sYVORgItWWj/fGkkQH/LDgBDlWF
e3oKt9KPrwrxxYv+ODlBsye6LySrRNu7aQmbJLkrhsU3pThKLumbOHY39r/cYA==
Date: Wed, 15 May 2024 23:29:05 +0200
From: Michael Niedermayer <michael@niedermayer.cc>
To: FFmpeg development discussions and patches <ffmpeg-devel@ffmpeg.org>
Message-ID: <20240515212905.GO6420@pb2>
References: <42af1d43261e04d99171c93ed26947712e263be8.camel@haerdin.se>
MIME-Version: 1.0
In-Reply-To: <42af1d43261e04d99171c93ed26947712e263be8.camel@haerdin.se>
X-GND-Sasl: michael@niedermayer.cc
Subject: Re: [FFmpeg-devel] [RFC] Value analysis with Frama-C's Eva plugin
(and an UB fix)
X-BeenThere: ffmpeg-devel@ffmpeg.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: FFmpeg development discussions and patches <ffmpeg-devel.ffmpeg.org>
List-Unsubscribe: <https://ffmpeg.org/mailman/options/ffmpeg-devel>,
<mailto:ffmpeg-devel-request@ffmpeg.org?subject=unsubscribe>
List-Archive: <https://ffmpeg.org/pipermail/ffmpeg-devel>
List-Post: <mailto:ffmpeg-devel@ffmpeg.org>
List-Help: <mailto:ffmpeg-devel-request@ffmpeg.org?subject=help>
List-Subscribe: <https://ffmpeg.org/mailman/listinfo/ffmpeg-devel>,
<mailto:ffmpeg-devel-request@ffmpeg.org?subject=subscribe>
Reply-To: FFmpeg development discussions and patches <ffmpeg-devel@ffmpeg.org>
Content-Type: multipart/mixed; boundary="===============7256966701859108404=="
Errors-To: ffmpeg-devel-bounces@ffmpeg.org
Sender: "ffmpeg-devel" <ffmpeg-devel-bounces@ffmpeg.org>
Archived-At: <https://master.gitmailbox.com/ffmpegdev/20240515212905.GO6420@pb2/>
List-Archive: <https://master.gitmailbox.com/ffmpegdev/>
List-Post: <mailto:ffmpegdev@gitmailbox.com>
--===============7256966701859108404==
Content-Type: multipart/signed; micalg=pgp-sha512;
protocol="application/pgp-signature"; boundary="QxnIWmKVhvdOmmJ8"
Content-Disposition: inline
--QxnIWmKVhvdOmmJ8
Content-Type: text/plain; charset=iso-8859-1
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable
On Wed, May 15, 2024 at 09:39:43PM +0200, Tomas H=E4rdin wrote:
> Hi
>=20
> So as I said in the coverity thread it would be good if we could get at
> least part of the codebase covered using formal tools. To this effect I
> sat down for an hour just now and gave libavutil/common.h a go with
> Frama-C's Eva plugin [1;2]. This plugin performs value analysis, which
> is a much simpler analysis compared to say the weakest predicate (WP)
> plugin.
>=20
> Going through the functions from top to bottom it only took until
> av_clipl_int32_c() to find my first UB, a patch for which is attached.
> Thus my harping on this has born at least some fruit.
>=20
> To run the analysis implemented in this set of patches (all of which
> I've attached here because I don't want to bother writing six follow-up
> email), first install frama-c using opam. I'm using 28.0~beta (Nickel).
> Then run "make verify" in libavutil/ and Eva should tell you that 33%
> of functions are covered and 100% of statements in those functions are
> covered, with zero alarms.
>=20
> If the project isn't interested in this then I'll probably continue
> fiddling with it on my own mostly as exercise. But I suspect it will
> bear even more fruit in time.
i think this is cool, especially considering
> common.h | 4 ++--
> 1 file changed, 2 insertions(+), 2 deletions(-)
> e451a7cd9a600ece22a6ee85ad7ed0c16349a411 0006-lavu-common.h-Fix-UB-in-av=
_clipl_int32_c.patch
> From 8a535878b9f1f87ca20d5e626f2c4c098b1c948e Mon Sep 17 00:00:00 2001
> From: =3D?UTF-8?q?Tomas=3D20H=3DC3=3DA4rdin?=3D <git@haerdin.se>
> Date: Wed, 15 May 2024 21:03:47 +0200
> Subject: [PATCH 6/7] lavu/common.h: Fix UB in av_clipl_int32_c()
>=20
> ---
> libavutil/common.h | 4 ++--
> 1 file changed, 2 insertions(+), 2 deletions(-)
>=20
> diff --git a/libavutil/common.h b/libavutil/common.h
> index d81131f8ad..0521ebbfc5 100644
> --- a/libavutil/common.h
> +++ b/libavutil/common.h
> @@ -258,8 +258,8 @@ static av_always_inline av_const int16_t av_clip_int1=
6_c(int a)
> */
> static av_always_inline av_const int32_t av_clipl_int32_c(int64_t a)
> {
> - if ((a+0x80000000u) & ~UINT64_C(0xFFFFFFFF)) return (int32_t)((a>>63=
) ^ 0x7FFFFFFF);
> - else return (int32_t)a;
> + if ((a+UINT64_C(0x80000000)) & ~UINT64_C(0xFFFFFFFF)) return (int32_=
t)((a>>63) ^ 0x7FFFFFFF);
> + else return (int32_=
t)a;
> }
it already found something
the av_clipl_int32_c patch LGTM
thx
[...]
--=20
Michael GnuPG fingerprint: 9FF2128B147EF6730BADF133611EC787040B0FAB
I know you won't believe me, but the highest form of Human Excellence is
to question oneself and others. -- Socrates
--QxnIWmKVhvdOmmJ8
Content-Type: application/pgp-signature; name="signature.asc"
-----BEGIN PGP SIGNATURE-----
iF0EABEKAB0WIQSf8hKLFH72cwut8TNhHseHBAsPqwUCZkUpHgAKCRBhHseHBAsP
q/s3AJ48UbSE9mbBr57o6h2nQnanYrGFZgCgguvhO9rHUJJb68m8Av8fFX8ARPo=
=0zJ8
-----END PGP SIGNATURE-----
--QxnIWmKVhvdOmmJ8--
--===============7256966701859108404==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
_______________________________________________
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".
--===============7256966701859108404==--