[FFmpeg-devel] [RFC] Value analysis with Frama-C's Eva plugin (and an UB fix)

[Michael Niedermayer]

On Wed, May 15, 2024 at 09:39:43PM +0200, Tomas Härdin wrote:
> Hi
> 
> 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.
> 
> 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.
> 
> 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.
> 
> 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: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git at 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()
> 
> ---
>  libavutil/common.h | 4 ++--
>  1 file changed, 2 insertions(+), 2 deletions(-)
> 
> 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_int16_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

[...]

-- 
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 195 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20240515/469d42b2/attachment.sig>