From 4cdab8d022844dddcac3c4c5c849fd207bc73dea Mon Sep 17 00:00:00 2001 From: Hu Weiwen Date: Thu, 12 Aug 2021 12:42:12 +0800 Subject: [PATCH] movenc: Get rid of frag_start MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit "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 Signed-off-by: Martin Storsjö --- libavformat/movenc.c | 24 ++++-------------------- libavformat/movenc.h | 1 - 2 files changed, 4 insertions(+), 21 deletions(-) diff --git a/libavformat/movenc.c b/libavformat/movenc.c index a460cd9ada..18410c70fa 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 af1ea0bce6..daeaad1cc6 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;