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

* [FFmpeg-devel] [RFC] Value analysis with Frama-C's Eva plugin (and an UB fix)
@ 2024-05-15 19:39 Tomas Härdin
  2024-05-15 21:29 ` Michael Niedermayer
  2024-05-16 12:12 ` Andrew Sayers
  0 siblings, 2 replies; 6+ messages in thread
From: Tomas Härdin @ 2024-05-15 19:39 UTC (permalink / raw)
  To: FFmpeg development discussions and patches

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

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.

/Tomas

[1] https://frama-c.com/
[2] https://frama-c.com/fc-plugins/eva.html

[-- Attachment #2: 0001-lavu-Very-basic-Eva-setup.patch --]
[-- Type: text/x-patch, Size: 2694 bytes --]

From 919279c36ee2bf93e02a756148eb8316e1a535a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git@haerdin.se>
Date: Wed, 15 May 2024 20:01:48 +0200
Subject: [PATCH 1/7] lavu: Very basic Eva setup

Only av_log2() for now.
---
 libavutil/Makefile | 8 ++++++++
 libavutil/common.h | 7 +++++--
 libavutil/eva.c    | 8 ++++++++
 3 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 libavutil/eva.c

diff --git a/libavutil/Makefile b/libavutil/Makefile
index 6e6fa8d800..d9c59f02c7 100644
--- a/libavutil/Makefile
+++ b/libavutil/Makefile
@@ -290,3 +290,11 @@ tools/crypto_bench$(EXESUF): ELIBS += $(if $(VERSUS),$(subst +, -l,+$(VERSUS)),)
 tools/crypto_bench.o: CFLAGS += -DUSE_EXT_LIBS=0$(if $(VERSUS),$(subst +,+USE_,+$(VERSUS)),)
 
 $(SUBDIR)tests/lzo$(EXESUF): ELIBS = -llzo2
+
+verify:
+	frama-c -cpp-extra-args="-DEVA -I.." -eva eva.c
+
+verify-gui:
+	frama-c-gui -cpp-extra-args="-DEVA -I.." -eva eva.c
+
+.PHONY: verify
diff --git a/libavutil/common.h b/libavutil/common.h
index 3e4c339893..b532ef8a46 100644
--- a/libavutil/common.h
+++ b/libavutil/common.h
@@ -160,6 +160,9 @@
 #endif
 
 #ifndef av_log2
+/*@ ensures 0 <= \result <= 31;
+    assigns \result \from v;
+ */
 av_const int av_log2(unsigned v);
 #endif
 
@@ -349,7 +352,7 @@ static av_always_inline int av_sat_dsub32_c(int a, int b)
  * @return sum with signed saturation
  */
 static av_always_inline int64_t av_sat_add64_c(int64_t a, int64_t b) {
-#if (!defined(__INTEL_COMPILER) && AV_GCC_VERSION_AT_LEAST(5,1)) || AV_HAS_BUILTIN(__builtin_add_overflow)
+#if (!defined(__INTEL_COMPILER) && AV_GCC_VERSION_AT_LEAST(5,1) && !defined(EVA)) || AV_HAS_BUILTIN(__builtin_add_overflow)
     int64_t tmp;
     return !__builtin_add_overflow(a, b, &tmp) ? tmp : (tmp < 0 ? INT64_MAX : INT64_MIN);
 #else
@@ -368,7 +371,7 @@ static av_always_inline int64_t av_sat_add64_c(int64_t a, int64_t b) {
  * @return difference with signed saturation
  */
 static av_always_inline int64_t av_sat_sub64_c(int64_t a, int64_t b) {
-#if (!defined(__INTEL_COMPILER) && AV_GCC_VERSION_AT_LEAST(5,1)) || AV_HAS_BUILTIN(__builtin_sub_overflow)
+#if (!defined(__INTEL_COMPILER) && AV_GCC_VERSION_AT_LEAST(5,1) && !defined(EVA)) || AV_HAS_BUILTIN(__builtin_sub_overflow)
     int64_t tmp;
     return !__builtin_sub_overflow(a, b, &tmp) ? tmp : (tmp < 0 ? INT64_MAX : INT64_MIN);
 #else
diff --git a/libavutil/eva.c b/libavutil/eva.c
new file mode 100644
index 0000000000..c7f0c9a09c
--- /dev/null
+++ b/libavutil/eva.c
@@ -0,0 +1,8 @@
+#include "common.h"
+#include "__fc_builtin.h"
+
+int main(void) {
+    unsigned uint = Frama_C_unsigned_int_interval(0, UINT_MAX);
+    av_log2(uint);
+    return 0;
+}
-- 
2.39.2


[-- Attachment #3: 0002-eva-Add-av_log2_16bit.patch --]
[-- Type: text/x-patch, Size: 1033 bytes --]

From 1280368e2cbe329092ad6bccef089d72dce1bcbe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git@haerdin.se>
Date: Wed, 15 May 2024 20:06:36 +0200
Subject: [PATCH 2/7] eva: Add av_log2_16bit()

---
 libavutil/common.h | 3 +++
 libavutil/eva.c    | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/libavutil/common.h b/libavutil/common.h
index b532ef8a46..d81131f8ad 100644
--- a/libavutil/common.h
+++ b/libavutil/common.h
@@ -167,6 +167,9 @@ av_const int av_log2(unsigned v);
 #endif
 
 #ifndef av_log2_16bit
+/*@ ensures 0 <= \result <= 15;
+    assigns \result \from v;
+ */
 av_const int av_log2_16bit(unsigned v);
 #endif
 
diff --git a/libavutil/eva.c b/libavutil/eva.c
index c7f0c9a09c..1f7f457015 100644
--- a/libavutil/eva.c
+++ b/libavutil/eva.c
@@ -3,6 +3,8 @@
 
 int main(void) {
     unsigned uint = Frama_C_unsigned_int_interval(0, UINT_MAX);
+    unsigned short ushort = Frama_C_unsigned_short_interval(0, UINT16_MAX);
     av_log2(uint);
+    av_log2_16bit(ushort);
     return 0;
 }
-- 
2.39.2


[-- Attachment #4: 0003-eva-av_clip.patch --]
[-- Type: text/x-patch, Size: 918 bytes --]

From d74bf77c642005e694905d091c97f1b2276f814c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git@haerdin.se>
Date: Wed, 15 May 2024 20:43:54 +0200
Subject: [PATCH 3/7] eva: av_clip()

---
 libavutil/eva.c | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/libavutil/eva.c b/libavutil/eva.c
index 1f7f457015..0bdfd4ff1a 100644
--- a/libavutil/eva.c
+++ b/libavutil/eva.c
@@ -2,9 +2,15 @@
 #include "__fc_builtin.h"
 
 int main(void) {
+    int a = Frama_C_int_interval(INT_MIN, INT_MAX);
+    int amin = Frama_C_int_interval(INT_MIN, INT_MAX);
+    int amax = Frama_C_int_interval(INT_MIN, INT_MAX);
     unsigned uint = Frama_C_unsigned_int_interval(0, UINT_MAX);
     unsigned short ushort = Frama_C_unsigned_short_interval(0, UINT16_MAX);
     av_log2(uint);
     av_log2_16bit(ushort);
+    if (amin <= amax) {
+        int res = av_clip(a, amin, amax);
+    }
     return 0;
 }
-- 
2.39.2


[-- Attachment #5: 0004-eva-av_clip64.patch --]
[-- Type: text/x-patch, Size: 1073 bytes --]

From ca877359781199baace8b23f300d20e091e01f00 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git@haerdin.se>
Date: Wed, 15 May 2024 20:47:32 +0200
Subject: [PATCH 4/7] eva: av_clip64

---
 libavutil/eva.c | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/libavutil/eva.c b/libavutil/eva.c
index 0bdfd4ff1a..565460d024 100644
--- a/libavutil/eva.c
+++ b/libavutil/eva.c
@@ -7,10 +7,17 @@ int main(void) {
     int amax = Frama_C_int_interval(INT_MIN, INT_MAX);
     unsigned uint = Frama_C_unsigned_int_interval(0, UINT_MAX);
     unsigned short ushort = Frama_C_unsigned_short_interval(0, UINT16_MAX);
+    int64_t a64 = Frama_C_long_long_interval(INT64_MIN, INT64_MAX);
+    int64_t a64min = Frama_C_long_long_interval(INT64_MIN, INT64_MAX);
+    int64_t a64max = Frama_C_long_long_interval(INT64_MIN, INT64_MAX);
+
     av_log2(uint);
     av_log2_16bit(ushort);
     if (amin <= amax) {
         int res = av_clip(a, amin, amax);
     }
+    if (a64min <= a64max) {
+        av_clip64(a64, a64min, a64max);
+    }
     return 0;
 }
-- 
2.39.2


[-- Attachment #6: 0005-eva-av_clip_.patch --]
[-- Type: text/x-patch, Size: 635 bytes --]

From f593ea6cc3b5899f853d8474169dccef4c0ba5c1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git@haerdin.se>
Date: Wed, 15 May 2024 20:54:42 +0200
Subject: [PATCH 5/7] eva: av_clip_*()

---
 libavutil/eva.c | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/libavutil/eva.c b/libavutil/eva.c
index 565460d024..3f60e1a9ce 100644
--- a/libavutil/eva.c
+++ b/libavutil/eva.c
@@ -19,5 +19,11 @@ int main(void) {
     if (a64min <= a64max) {
         av_clip64(a64, a64min, a64max);
     }
+
+    av_clip_uint8(a);
+    av_clip_int8(a);
+    av_clip_uint16(a);
+    av_clip_int16(a);
+
     return 0;
 }
-- 
2.39.2


[-- Attachment #7: 0006-lavu-common.h-Fix-UB-in-av_clipl_int32_c.patch --]
[-- Type: text/x-patch, Size: 972 bytes --]

From 8a535878b9f1f87ca20d5e626f2c4c098b1c948e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <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()

---
 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;
 }
 
 /**
-- 
2.39.2


[-- Attachment #8: 0007-eva-av_clipl_int32.patch --]
[-- Type: text/x-patch, Size: 557 bytes --]

From 035c01de096eb94bd6bb2fcbbbdd5e0a70a703a2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git@haerdin.se>
Date: Wed, 15 May 2024 21:03:56 +0200
Subject: [PATCH 7/7] eva: av_clipl_int32()

---
 libavutil/eva.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/libavutil/eva.c b/libavutil/eva.c
index 3f60e1a9ce..e5334ecb38 100644
--- a/libavutil/eva.c
+++ b/libavutil/eva.c
@@ -24,6 +24,7 @@ int main(void) {
     av_clip_int8(a);
     av_clip_uint16(a);
     av_clip_int16(a);
+    av_clipl_int32(a64);
 
     return 0;
 }
-- 
2.39.2


[-- Attachment #9: 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".

^ permalink raw reply	[flat|nested] 6+ messages in thread