1
0
mirror of https://github.com/FFmpeg/FFmpeg.git synced 2024-11-26 19:01:44 +02:00
FFmpeg/libavformat/movenc.h
Hu Weiwen 4cdab8d022 movenc: Get rid of frag_start
"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 bff7d662d7)

"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 <sehuww@mail.scut.edu.cn>
Signed-off-by: Martin Storsjö <martin@martin.st>
2021-08-18 13:07:46 +03:00

276 lines
7.9 KiB
C

/*
* MOV, 3GP, MP4 muxer
* Copyright (c) 2003 Thomas Raivio
* Copyright (c) 2004 Gildas Bazin <gbazin at videolan dot org>
* Copyright (c) 2009 Baptiste Coudurier <baptiste dot coudurier at gmail dot com>
*
* This file is part of FFmpeg.
*
* FFmpeg is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public
* License as published by the Free Software Foundation; either
* version 2.1 of the License, or (at your option) any later version.
*
* FFmpeg is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with FFmpeg; if not, write to the Free Software
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
*/
#ifndef AVFORMAT_MOVENC_H
#define AVFORMAT_MOVENC_H
#include "avformat.h"
#include "movenccenc.h"
#define MOV_FRAG_INFO_ALLOC_INCREMENT 64
#define MOV_INDEX_CLUSTER_SIZE 1024
#define MOV_TIMESCALE 1000
#define RTP_MAX_PACKET_SIZE 1450
#define MODE_MP4 0x01
#define MODE_MOV 0x02
#define MODE_3GP 0x04
#define MODE_PSP 0x08 // example working PSP command line:
// ffmpeg -i testinput.avi -f psp -r 14.985 -s 320x240 -b 768 -ar 24000 -ab 32 M4V00001.MP4
#define MODE_3G2 0x10
#define MODE_IPOD 0x20
#define MODE_ISM 0x40
#define MODE_F4V 0x80
typedef struct MOVIentry {
uint64_t pos;
int64_t dts;
int64_t pts;
unsigned int size;
unsigned int samples_in_chunk;
unsigned int chunkNum; ///< Chunk number if the current entry is a chunk start otherwise 0
unsigned int entries;
int cts;
#define MOV_SYNC_SAMPLE 0x0001
#define MOV_PARTIAL_SYNC_SAMPLE 0x0002
#define MOV_DISPOSABLE_SAMPLE 0x0004
uint32_t flags;
AVProducerReferenceTime prft;
} MOVIentry;
typedef struct HintSample {
uint8_t *data;
int size;
int sample_number;
int offset;
int own_data;
} HintSample;
typedef struct HintSampleQueue {
int size;
int len;
HintSample *samples;
} HintSampleQueue;
typedef struct MOVFragmentInfo {
int64_t offset;
int64_t time;
int64_t duration;
int64_t tfrf_offset;
int size;
} MOVFragmentInfo;
typedef struct MOVTrack {
int mode;
int entry;
unsigned timescale;
uint64_t time;
int64_t track_duration;
int last_sample_is_subtitle_end;
long sample_count;
long sample_size;
long chunkCount;
int has_keyframes;
int has_disposable;
#define MOV_TRACK_CTTS 0x0001
#define MOV_TRACK_STPS 0x0002
#define MOV_TRACK_ENABLED 0x0004
uint32_t flags;
#define MOV_TIMECODE_FLAG_DROPFRAME 0x0001
#define MOV_TIMECODE_FLAG_24HOURSMAX 0x0002
#define MOV_TIMECODE_FLAG_ALLOWNEGATIVE 0x0004
uint32_t timecode_flags;
int language;
int track_id;
int tag; ///< stsd fourcc
AVStream *st;
AVCodecParameters *par;
int multichannel_as_mono;
int vos_len;
uint8_t *vos_data;
MOVIentry *cluster;
unsigned cluster_capacity;
int audio_vbr;
int height; ///< active picture (w/o VBI) height for D-10/IMX
uint32_t tref_tag;
int tref_id; ///< trackID of the referenced track
int64_t start_dts;
int64_t start_cts;
int64_t end_pts;
int end_reliable;
int64_t dts_shift;
int hint_track; ///< the track that hints this track, -1 if no hint track is set
int src_track; ///< the track that this hint (or tmcd) track describes
AVFormatContext *rtp_ctx; ///< the format context for the hinting rtp muxer
uint32_t prev_rtp_ts;
int64_t cur_rtp_ts_unwrapped;
uint32_t max_packet_size;
int64_t default_duration;
uint32_t default_sample_flags;
uint32_t default_size;
HintSampleQueue sample_queue;
AVPacket *cover_image;
AVIOContext *mdat_buf;
int64_t data_offset;
int frag_discont;
int entries_flushed;
int nb_frag_info;
MOVFragmentInfo *frag_info;
unsigned frag_info_capacity;
struct {
int first_packet_seq;
int first_packet_entry;
int first_packet_seen;
int first_frag_written;
int packet_seq;
int packet_entry;
int slices;
} vc1_info;
void *eac3_priv;
MOVMuxCencContext cenc;
uint32_t palette[AVPALETTE_COUNT];
int pal_done;
int is_unaligned_qt_rgb;
} MOVTrack;
typedef enum {
MOV_ENC_NONE = 0,
MOV_ENC_CENC_AES_CTR,
} MOVEncryptionScheme;
typedef enum {
MOV_PRFT_NONE = 0,
MOV_PRFT_SRC_WALLCLOCK,
MOV_PRFT_SRC_PTS,
MOV_PRFT_NB
} MOVPrftBox;
typedef struct MOVMuxContext {
const AVClass *av_class;
int mode;
int64_t time;
int nb_streams;
int nb_meta_tmcd; ///< number of new created tmcd track based on metadata (aka not data copy)
int chapter_track; ///< qt chapter track number
int64_t mdat_pos;
uint64_t mdat_size;
MOVTrack *tracks;
int flags;
int rtp_flags;
int iods_skip;
int iods_video_profile;
int iods_audio_profile;
int moov_written;
int fragments;
int max_fragment_duration;
int min_fragment_duration;
int max_fragment_size;
int ism_lookahead;
AVIOContext *mdat_buf;
int first_trun;
int video_track_timescale;
int reserved_moov_size; ///< 0 for disabled, -1 for automatic, size otherwise
int64_t reserved_header_pos;
char *major_brand;
int per_stream_grouping;
AVFormatContext *fc;
AVPacket *pkt;
int use_editlist;
float gamma;
int frag_interleave;
int missing_duration_warned;
char *encryption_scheme_str;
MOVEncryptionScheme encryption_scheme;
uint8_t *encryption_key;
int encryption_key_len;
uint8_t *encryption_kid;
int encryption_kid_len;
int need_rewrite_extradata;
int use_stream_ids_as_track_ids;
int track_ids_ok;
int write_tmcd;
MOVPrftBox write_prft;
int empty_hdlr_name;
int movie_timescale;
} MOVMuxContext;
#define FF_MOV_FLAG_RTP_HINT (1 << 0)
#define FF_MOV_FLAG_FRAGMENT (1 << 1)
#define FF_MOV_FLAG_EMPTY_MOOV (1 << 2)
#define FF_MOV_FLAG_FRAG_KEYFRAME (1 << 3)
#define FF_MOV_FLAG_SEPARATE_MOOF (1 << 4)
#define FF_MOV_FLAG_FRAG_CUSTOM (1 << 5)
#define FF_MOV_FLAG_ISML (1 << 6)
#define FF_MOV_FLAG_FASTSTART (1 << 7)
#define FF_MOV_FLAG_OMIT_TFHD_OFFSET (1 << 8)
#define FF_MOV_FLAG_DISABLE_CHPL (1 << 9)
#define FF_MOV_FLAG_DEFAULT_BASE_MOOF (1 << 10)
#define FF_MOV_FLAG_DASH (1 << 11)
#define FF_MOV_FLAG_FRAG_DISCONT (1 << 12)
#define FF_MOV_FLAG_DELAY_MOOV (1 << 13)
#define FF_MOV_FLAG_GLOBAL_SIDX (1 << 14)
#define FF_MOV_FLAG_WRITE_COLR (1 << 15)
#define FF_MOV_FLAG_WRITE_GAMA (1 << 16)
#define FF_MOV_FLAG_USE_MDTA (1 << 17)
#define FF_MOV_FLAG_SKIP_TRAILER (1 << 18)
#define FF_MOV_FLAG_NEGATIVE_CTS_OFFSETS (1 << 19)
#define FF_MOV_FLAG_FRAG_EVERY_FRAME (1 << 20)
#define FF_MOV_FLAG_SKIP_SIDX (1 << 21)
#define FF_MOV_FLAG_CMAF (1 << 22)
#define FF_MOV_FLAG_PREFER_ICC (1 << 23)
int ff_mov_write_packet(AVFormatContext *s, AVPacket *pkt);
int ff_mov_init_hinting(AVFormatContext *s, int index, int src_index);
int ff_mov_add_hinted_packet(AVFormatContext *s, AVPacket *pkt,
int track_index, int sample,
uint8_t *sample_data, int sample_size);
void ff_mov_close_hinting(MOVTrack *track);
#endif /* AVFORMAT_MOVENC_H */