From patchwork Wed May 15 19:39:43 2024 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: 48904 Delivered-To: ffmpegpatchwork2@gmail.com Received: by 2002:a05:6a21:3a48:b0:1af:fc2d:ff5a with SMTP id zu8csp1819111pzb; Wed, 15 May 2024 12:39:57 -0700 (PDT) X-Forwarded-Encrypted: i=2; AJvYcCVzNtUpA6/GUO1oM2eUQF6Nk53PJNCedGgoiOug9/Va6+rLJpDu4R9Gr38KOet/AhOTA/Ggjzi/RPJqhWuAiYKzesMoKhWjXnnaXQ== X-Google-Smtp-Source: AGHT+IGYPSPVAKEQCpRsMQ1/udy9F5SDSRQlm74oYSyesdHiu4sj4BTA/XXqs+/psPk37gRTd48d X-Received: by 2002:ac2:53b5:0:b0:518:b180:3f94 with SMTP id 2adb3069b0e04-5220fc7eb89mr8961296e87.2.1715801996808; Wed, 15 May 2024 12:39:56 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1715801996; cv=none; d=google.com; s=arc-20160816; b=Vd9+H9EegeKvLWGbOeUx+0Xx28pxrAXWf5uXw0QdawPcW0o3mm5+QE3JRL5KJMz5U1 9QJ3V9jBE96dS7d9Fl/H+39ctgbgwlSu5pQNjxmrW4Uzg9gozdVK6QHEBKY1HQxVnAIq cDjDIEUPF/TWJlVgQyIbvPJXl100cFnUXDqq10YdZycgVb12VdNwmOJVXxK7pSWQ9vh5 tdeAR8POrp4f5B/9GjBJurmGgIDI1LbKHHl0cyzIj9SkG2ULJQAhNrAaFHlXOoBVdFBI 4lOj1FJQmiYh0L4DQQER+gLKiYuOf3v2mIAXCThEg/WFLJ0d2iBPFm14YbkCd9sBzweJ /hBA== 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:delivered-to; bh=MC2VS1miEkupKZWI+2IagXDVykfvSOZMcnjPb0IY92U=; fh=e5zN9xSzcxLA6bGo3lF+CqTbY/oLwzApV03EO/RBfgQ=; b=vdfBev7xOx7On5eIjMr5Ts2lwqCgi8avnOFu7YMOJmSjL391vm2T9yOAZMR/OYmhwR E/NBYOCnFcoblIndZx+0j5GLifzK5/dX8SKwuEbfgjNTBryeJIGS3DqxdRdJAAHlHrbq 6ios6jKPduAK6KDc6brswdGvEb4TuCjC5GLmHixsOtQyOuVVeMjq33p+nsmZoXCQHIcO uTX+/ZzjGmGxE4wj9hPUlo41Wmv2aogzgZejli/KzAEtMUJJkpgVcxHbhyODJ2MU+FGf HpwfY692HlUEhGzL/PaWcCW7P0q6MGNV8HJctrHqif2fiXQRiLn454gyuRSnbPAegWZj 603w==; dara=google.com ARC-Authentication-Results: i=1; mx.google.com; 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 Return-Path: Received: from ffbox0-bg.mplayerhq.hu (ffbox0-bg.ffmpeg.org. [79.124.17.100]) by mx.google.com with ESMTP id 2adb3069b0e04-521f38da32esi4903669e87.392.2024.05.15.12.39.56; Wed, 15 May 2024 12:39:56 -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; 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 Received: from [127.0.1.1] (localhost [127.0.0.1]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id 673A768D5F2; Wed, 15 May 2024 22:39:51 +0300 (EEST) X-Original-To: ffmpeg-devel@ffmpeg.org Delivered-To: ffmpeg-devel@ffmpeg.org Received: from glom.nmugroup.com (glom.nmugroup.com [193.183.80.6]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTPS id 01A2168D36D for ; Wed, 15 May 2024 22:39:44 +0300 (EEST) Received: from localhost (localhost [127.0.0.1]) by glom.nmugroup.com (Postfix) with ESMTP id 857535429F01 for ; Wed, 15 May 2024 21:39:44 +0200 (CEST) Received: from [192.168.43.177] (host-217-213-155-126.mobileonline.telia.com [217.213.155.126]) (Authenticated sender: git01) by glom.nmugroup.com (Postfix) with ESMTPSA id 2FF955429EF5 for ; Wed, 15 May 2024 21:39:43 +0200 (CEST) Message-ID: <42af1d43261e04d99171c93ed26947712e263be8.camel@haerdin.se> From: Tomas =?iso-8859-1?q?H=E4rdin?= To: FFmpeg development discussions and patches Date: Wed, 15 May 2024 21:39:43 +0200 User-Agent: Evolution 3.46.4-2 MIME-Version: 1.0 Subject: [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 Errors-To: ffmpeg-devel-bounces@ffmpeg.org Sender: "ffmpeg-devel" X-TUID: 4lcKZSb75g3I 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 From 035c01de096eb94bd6bb2fcbbbdd5e0a70a703a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= 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