From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from ffbox0-bg.mplayerhq.hu (ffbox0-bg.ffmpeg.org [79.124.17.100]) by master.gitmailbox.com (Postfix) with ESMTP id DDB1B4ABF9 for ; 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 ; Thu, 16 May 2024 00:29:07 +0300 (EEST) Received: by mail.gandi.net (Postfix) with ESMTPSA id 81F6520002 for ; 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 To: FFmpeg development discussions and patches 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 List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-To: FFmpeg development discussions and patches Content-Type: multipart/mixed; boundary="===============7256966701859108404==" Errors-To: ffmpeg-devel-bounces@ffmpeg.org Sender: "ffmpeg-devel" Archived-At: List-Archive: List-Post: --===============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 > 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==--