From patchwork Thu Aug 12 04:42:12 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Hu Weiwen X-Patchwork-Id: 29473 Delivered-To: ffmpegpatchwork2@gmail.com Received: by 2002:a6b:8e8b:0:0:0:0:0 with SMTP id q133csp406721iod; Wed, 11 Aug 2021 21:43:15 -0700 (PDT) X-Google-Smtp-Source: ABdhPJxCLxRV8GG+ddFGSTVu7kUf2cSgxpsqFd3kbc6LQykQseVIpNLQZsQFiOryFUWH69qWk1sT X-Received: by 2002:a17:907:d09:: with SMTP id gn9mr1818029ejc.447.1628743395410; Wed, 11 Aug 2021 21:43:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1628743395; cv=none; d=google.com; s=arc-20160816; b=Rn0IjFhQGJMAAavRvkzdNM9nolM4JuN/Tz1OdNfDwwbGH01qHHlTLXI+9NwSEcib31 AUUgFSxWeuLbzdHM9OXeY6S3l9tfx5xWQ83nkfLNW1pDYDSXSNTK07ZUz0x8g6ZVwIyl Ibsstg37JuGQgtjjKtpne/R2uW7BGGu+DKrVDQ5R2ts3ZeY1yBN+H/ZDJsLKP1phsoyG V3g3O7mS6cID+K4trrJIMFnUQjTiB09w9SK6eKiRtasWnEZCUcNKJ+Ch7gGeiuaihNM2 lu3x2KYiiGDxTV/RHKkBTpLv5qIwtJX16eXy3PyuVB7BPbERmMeJSeFOm/lIF0sfIKsm HAAQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:content-transfer-encoding:cc:reply-to :list-subscribe:list-help:list-post:list-archive:list-unsubscribe :list-id:precedence:subject:mime-version:message-id:date:to:from :delivered-to; bh=dIf0nJ5GmDwmx47ePiHYy14ONiXJxhywmozcxDoGkWw=; b=pxBrcax5kEYgnzJ07s29CWrMq1UDNRQqLpTg937pueW/6lbxGJTMSlxpJf74Yqu+CW QA/l8etaj8U4N7apdAtabk9v/cqi1HjtrGt6VDXjoZLZKOKmBZZUDe8G/mvnxpGfJ6dI M2PUbr9se6xuftII3/eBKlkX3TaIdB8MLWVOJuMkmOTNk/R7rzNTEBdeXNds6GqlTIbG XUuiq2J60aGX/6n67l2RpJylAhmFpqQz8U0/BtGZQYffVY0RrJP7vwARhEc2FXiJ2goC cnhCI42vAbYE0vCel2rFpicLeuD80xm1leiFPMZO4Y1cklBhuIT/UpQxkrgJemUsMR6q BuJw== 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; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=scut.edu.cn Return-Path: Received: from ffbox0-bg.mplayerhq.hu (ffbox0-bg.ffmpeg.org. [79.124.17.100]) by mx.google.com with ESMTP id c2si1535033edr.563.2021.08.11.21.43.14; Wed, 11 Aug 2021 21:43:15 -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; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=scut.edu.cn Received: from [127.0.1.1] (localhost [127.0.0.1]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id D03B368A2C0; Thu, 12 Aug 2021 07:43:09 +0300 (EEST) X-Original-To: ffmpeg-devel@ffmpeg.org Delivered-To: ffmpeg-devel@ffmpeg.org Received: from mail.scut.edu.cn (unknown [202.38.213.12]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id C6086688128 for ; Thu, 12 Aug 2021 07:43:00 +0300 (EEST) Received: from dorm.huww98.cn (unknown [125.216.246.30]) by main (Coremail) with SMTP id AQAAfwB3KAW7phRhIJsDAA--.5360S4; Thu, 12 Aug 2021 12:42:35 +0800 (CST) From: Hu Weiwen To: ffmpeg-devel@ffmpeg.org Date: Thu, 12 Aug 2021 12:42:12 +0800 Message-Id: <20210812044212.484900-1-sehuww@mail.scut.edu.cn> X-Mailer: git-send-email 2.25.1 MIME-Version: 1.0 X-CM-TRANSID: AQAAfwB3KAW7phRhIJsDAA--.5360S4 X-Coremail-Antispam: 1UD129KBjvJXoW3WF45Wr15GF4rKryfJry5Jwb_yoWfKr17pa y7tF4F93Z8tFWqvr1kCF95WFy8WrZrtFs2q345ua4rAr9Ivrn5tFyUtFWxtry5G3srCr4f ZFsYka4j9r4IkrDanT9S1TB71UUUUUUqnTZGkaVYY2UrUUUUjbIjqfuFe4nvWSU5nxnvy2 9KBjDU0xBIdaVrnRJUUUkm14x267AKxVWUJVW8JwAFc2x0x2IEx4CE42xK8VAvwI8IcIk0 rVWrJVCq3wAFIxvE14AKwVWUJVWUGwA2ocxC64kIII0Yj41l84x0c7CEw4AK67xGY2AK02 1l84ACjcxK6xIIjxv20xvE14v26r1j6r1xM28EF7xvwVC0I7IYx2IY6xkF7I0E14v26r1j 6r4UM28EF7xvwVC2z280aVAFwI0_Cr0_Gr1UM28EF7xvwVC2z280aVCY1x0267AKxVW8Jr 0_Cr1UM2AIxVAIcxkEcVAq07x20xvEncxIr21l5I8CrVACY4xI64kE6c02F40Ex7xfMcIj 6xIIjxv20xvE14v26r1j6r18McIj6I8E87Iv67AKxVWUJVW8JwAm72CE4IkC6x0Yz7v_Jr 0_Gr1lF7xvr2IYc2Ij64vIr41lF7I21c0EjII2zVCS5cI20VAGYxC7MxkIecxEwVAFwVW8 XwCF04k20xvY0x0EwIxGrwCFx2IqxVCFs4IE7xkEbVWUJVW8JwC20s026c02F40E14v26r 1j6r18MI8I3I0E7480Y4vE14v26r106r1rMI8E67AF67kF1VAFwI0_Jrv_JF1lIxkGc2Ij 64vIr41lIxAIcVC0I7IYx2IY67AKxVWUJVWUCwCI42IY6xIIjxv20xvEc7CjxVAFwI0_Jr 0_Gr1lIxAIcVCF04k26cxKx2IYs7xG6rW3Jr0E3s1lIxAIcVC2z280aVAFwI0_Jr0_Gr1l IxAIcVC2z280aVCY1x0267AKxVWUJVW8JbIYCTnIWIevJa73UjIFyTuYvjfU8lksUUUUU X-CM-SenderInfo: qsqrljqqwxllyrt6zt1loo2ulxwovvfxof0/1tbiAQAKBlepTBkBpwAwsw Subject: [FFmpeg-devel] [PATCH] movenc: Get rid of frag_start 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 Cc: =?utf-8?q?Martin_Storsj=C3=B6?= , Hu Weiwen Errors-To: ffmpeg-devel-bounces@ffmpeg.org Sender: "ffmpeg-devel" X-TUID: /ENA97ksYwdo "frag_start" is redundant, and every occurance can be replaced with cluster[0].dts - start_dts The proof of no behaviour changes: (All line number below is based on commit bff7d662d728) "frag_start" is read at 4 place (with all possible call stacks): mov_write_packet ... mov_flush_fragment mov_write_moof_tag mov_write_moof_tag_internal mov_write_traf_tag mov_write_tfxd_tag (#1) mov_write_tfdt_tag (#2) mov_add_tfra_entries (#3) mov_write_sidx_tags mov_write_sidx_tag (#4) mov_write_trailer mov_auto_flush_fragment mov_flush_fragment ... (#1 #2 #3 #4) mov_write_sidx_tags mov_write_sidx_tag (#4) shift_data compute_sidx_size get_sidx_size mov_write_sidx_tags mov_write_sidx_tag (#4) All read happens in "mov_write_trailer" and "mov_write_moof_tag". So we need to prove no behaviour change in these two functions. Condition 1: for every track that have "trk->entry == 0", trk->frag_start == trk->track_duration. Condition 2: for every track that have "trk->entry > 0", trk->frag_start == trk->cluster[0].dts - trk->start_dts. Definition 1: "Before flush" means just before the invocation of "mov_flush_fragment", except for the auto-flush case in "mov_write_single_packet", which means before L5934. Lemma 1: If Condition 1 & 2 is true before flush, Condition 1 & 2 is still true after "mov_flush_fragment" returns. Proof: No update to the tracks that have "trk->entry == 0" before flushing, so we only consider tracks that have "trk->entry > 0": Case 1: !moov_written and moov will be written in this iteration trk->entry = 0 L5366 trk->frag_start == trk->cluster[0].dts - trk->start_dts Lemma condition trk->frag_start += trk->start_dts + trk->track_duration - trk->cluster[0].dts; L5363 So trk->entry == 0 && trk->frag_start == trk->track_duration Case 2: !moov_written and moov will NOT be written in this iteration nothing changed Case 3: moov_written trk->entry = 0 L5445 trk->frag_start == trk->cluster[0].dts - trk->start_dts Lemma condition trk->frag_start += trk->start_dts + trk->track_duration - trk->cluster[0].dts; L5444 So trk->entry == 0 && trk->frag_start == trk->track_duration Note that trk->track_duration may be updated for the tracks that have "trk->entry > 0" (mov_write_moov_tag will update track_duration of "tmcd" track, but it must have 1 entry). But in all case, trk->frag_start is also updated to consider the new value. Lemma 2: If Condition 1 & 2 is true before "ff_mov_write_packet" invocation, Condition 1 & 2 is still true after it returns. Proof: Only the track corresponding to the pkt is updated, and no update to relevant variables if trk->entry > 0 before invocation. So we only need to prove "trk->frag_start == trk->cluster[0].dts - trk->start_dts" after trk->entry increase from 0 to 1. Case 1: trk->start_dts == AV_NOPTS_VALUE Case 1.1: trk->frag_discont && use_editlist trk->cluster[0].dts = pkt->dts at L5741 trk->frag_start = pkt->pts at L5785 trk->start_dts = pkt->dts - pkt->pts at L5786 So trk->frag_start == trk->cluster[0].dts - trk->start_dts Case 1.2: trk->frag_discont && !use_editlist trk->cluster[0].dts = pkt->dts at L5741 trk->frag_start = pkt->dts at L5790 trk->start_dts = 0 at L5791 So trk->frag_start == trk->cluster[0].dts - trk->start_dts Case 1.3: !trk->frag_discont trk->cluster[0].dts = pkt->dts at L5741 trk->frag_start = 0 init trk->start_dts = pkt->dts at L5779 So trk->frag_start == trk->cluster[0].dts - trk->start_dts Case 2: trk->start_dts != AV_NOPTS_VALUE Case 2.1: trk->frag_discont trk->cluster[0].dts = pkt->dts at L5741 trk->frag_start = pkt->dts - trk->start_dts at L5763 So trk->frag_start == trk->cluster[0].dts - trk->start_dts Case 2.2: !trk->frag_discont trk->cluster[0].dts = trk->start_dts + trk->track_duration at L5749 trk->track_duration == trk->frag_start Lemma condition So trk->frag_start == trk->cluster[0].dts - trk->start_dts Lemma 3: Condition 1 & 2 is true in all case before and after "ff_mov_write_packet" invocation, before flush and after "mov_flush_fragment" returns. Proof: All updates to relevant variable happen either in "ff_mov_write_packet", or during flush. And Condition 1 & 2 is true initially. So with lemma 1 & 2, we can prove this use induction. Noticed that all read of "frag_start" only happen in "trk->entry > 0" branch. Now we need to prove Condition 2 is true before each read. Because no update to variables relevant to Condition 2 between "before flush" and "mov_write_moof_tag" invocation, we can conclude Condition 2 is true before every invocation of "mov_write_moof_tag". No behaviour change in "mov_write_moof_tag" is proved. In "mov_write_trailer", No update to relevant variables after the last flush and before the invocation of "mov_write_sidx_tag". So no behaviour change to "mov_write_trailer" is proved. Q.E.D. Signed-off-by: Hu Weiwen --- Hopefully this patch and/or the proof can make the code more clear to future readers. Thank you for reading this long proof. I'm doing something like this for the first time. Please kindly point it out if you find anything incorrect or confusing. libavformat/movenc.c | 24 ++++-------------------- libavformat/movenc.h | 1 - 2 files changed, 4 insertions(+), 21 deletions(-) -- 2.25.1 diff --git a/libavformat/movenc.c b/libavformat/movenc.c index a460cd9adae..18410c70fa0 100644 --- a/libavformat/movenc.c +++ b/libavformat/movenc.c @@ -4483,8 +4483,7 @@ static int mov_write_tfxd_tag(AVIOContext *pb, MOVTrack *track) avio_write(pb, uuid, sizeof(uuid)); avio_w8(pb, 1); avio_wb24(pb, 0); - avio_wb64(pb, track->start_dts + track->frag_start + - track->cluster[0].cts); + avio_wb64(pb, track->cluster[0].dts + track->cluster[0].cts); avio_wb64(pb, track->end_pts - (track->cluster[0].dts + track->cluster[0].cts)); @@ -4563,8 +4562,7 @@ static int mov_add_tfra_entries(AVIOContext *pb, MOVMuxContext *mov, int tracks, info->size = size; // Try to recreate the original pts for the first packet // from the fields we have stored - info->time = track->start_dts + track->frag_start + - track->cluster[0].cts; + info->time = track->cluster[0].dts + track->cluster[0].cts; info->duration = track->end_pts - (track->cluster[0].dts + track->cluster[0].cts); // If the pts is less than zero, we will have trimmed @@ -4602,7 +4600,7 @@ static int mov_write_tfdt_tag(AVIOContext *pb, MOVTrack *track) ffio_wfourcc(pb, "tfdt"); avio_w8(pb, 1); /* version */ avio_wb24(pb, 0); - avio_wb64(pb, track->frag_start); + avio_wb64(pb, track->cluster[0].dts - track->start_dts); return update_size(pb, pos); } @@ -4679,8 +4677,7 @@ static int mov_write_sidx_tag(AVIOContext *pb, if (track->entry) { entries = 1; - presentation_time = track->start_dts + track->frag_start + - track->cluster[0].cts; + presentation_time = track->cluster[0].dts + track->cluster[0].cts; duration = track->end_pts - (track->cluster[0].dts + track->cluster[0].cts); starts_with_SAP = track->cluster[0].flags & MOV_SYNC_SAMPLE; @@ -5359,10 +5356,6 @@ static int mov_flush_fragment(AVFormatContext *s, int force) mov->moov_written = 1; mov->mdat_size = 0; for (i = 0; i < mov->nb_streams; i++) { - if (mov->tracks[i].entry) - mov->tracks[i].frag_start += mov->tracks[i].start_dts + - mov->tracks[i].track_duration - - mov->tracks[i].cluster[0].dts; mov->tracks[i].entry = 0; mov->tracks[i].end_reliable = 0; } @@ -5416,11 +5409,7 @@ static int mov_flush_fragment(AVFormatContext *s, int force) MOVTrack *track = &mov->tracks[i]; int buf_size, write_moof = 1, moof_tracks = -1; uint8_t *buf; - int64_t duration = 0; - if (track->entry) - duration = track->start_dts + track->track_duration - - track->cluster[0].dts; if (mov->flags & FF_MOV_FLAG_SEPARATE_MOOF) { if (!track->entry) continue; @@ -5440,8 +5429,6 @@ static int mov_flush_fragment(AVFormatContext *s, int force) ffio_wfourcc(s->pb, "mdat"); } - if (track->entry) - track->frag_start += duration; track->entry = 0; track->entries_flushed = 0; track->end_reliable = 0; @@ -5760,7 +5747,6 @@ int ff_mov_write_packet(AVFormatContext *s, AVPacket *pkt) /* New fragment, but discontinuous from previous fragments. * Pretend the duration sum of the earlier fragments is * pkt->dts - trk->start_dts. */ - trk->frag_start = pkt->dts - trk->start_dts; trk->end_pts = AV_NOPTS_VALUE; trk->frag_discont = 0; } @@ -5782,12 +5768,10 @@ int ff_mov_write_packet(AVFormatContext *s, AVPacket *pkt) /* Pretend the whole stream started at pts=0, with earlier fragments * already written. If the stream started at pts=0, the duration sum * of earlier fragments would have been pkt->pts. */ - trk->frag_start = pkt->pts; trk->start_dts = pkt->dts - pkt->pts; } else { /* Pretend the whole stream started at dts=0, with earlier fragments * already written, with a duration summing up to pkt->dts. */ - trk->frag_start = pkt->dts; trk->start_dts = 0; } trk->frag_discont = 0; diff --git a/libavformat/movenc.h b/libavformat/movenc.h index af1ea0bce64..daeaad1cc68 100644 --- a/libavformat/movenc.h +++ b/libavformat/movenc.h @@ -138,7 +138,6 @@ typedef struct MOVTrack { AVIOContext *mdat_buf; int64_t data_offset; - int64_t frag_start; int frag_discont; int entries_flushed;