virtualenv/FFmpeg
1
0
Fork 0
mirror of https://github.com/FFmpeg/FFmpeg.git synced 2024-12-28 20:53:54 +02:00
Code Issues Releases Activity
Mirror of https://git.ffmpeg.org/ffmpeg.git
103,285 Commits 37 Branches 400 Tags 467 MiB
C 90.3%
Assembly 7.8%
Makefile 1.3%
C++ 0.2%
Objective-C 0.2%
Other 0.1%
4cdab8d022
Go to file
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
compat compat/cuda: add __expf() implementation 2021-08-14 15:06:47 +02:00
doc avcodec: add SMC encoder 2021-08-18 08:55:56 +02:00
ffbuild avfilter: compress CUDA PTX code if possible 2021-06-22 14:05:44 +02:00
fftools ffmpeg_hw: Don't ignore key parameters when initializing a hw device 2021-08-17 10:10:07 -03:00
libavcodec avcodec/libx265: improve full range flag setting logic 2021-08-18 12:09:37 +03:00
libavdevice avdevice/decklink: support for more duplex mode for Decklink 8K Pro 2021-08-16 10:00:39 +08:00
libavfilter avfilter/avfilter: Remove unused feature to add pads in the middle 2021-08-17 21:20:59 +02:00
libavformat movenc: Get rid of frag_start 2021-08-18 13:07:46 +03:00
libavutil avutil/opt: Document actual behaviour of av_opt_copy a bit more 2021-08-17 19:11:57 +02:00
libpostproc postproc/postprocess: Remove legacy cruft 2021-07-29 22:02:06 +02:00
libswresample (postproc|swresample)/version: Don't include libavutil/avutil.h 2021-07-29 22:02:05 +02:00
libswscale avutil/internal, swresample/audioconvert: Remove cpu.h inclusions 2021-07-22 14:33:45 +02:00
presets
tests avcodec/options_table: Treat (request_)channel_layout as channel layout 2021-08-15 23:19:35 +02:00
tools FATE: add a test for sliced scaling 2021-08-08 19:26:05 +02:00
.gitattributes
.gitignore avfilter: compress CUDA PTX code if possible 2021-06-22 14:05:44 +02:00
.mailmap
.travis.yml
Changelog avcodec: add SMC encoder 2021-08-18 08:55:56 +02:00
configure avfilter/vf_convolve: switch to TX FFT from avutil 2021-08-17 09:15:06 +02:00
CONTRIBUTING.md
COPYING.GPLv2
COPYING.GPLv3
COPYING.LGPLv2.1
COPYING.LGPLv3
CREDITS
INSTALL.md
LICENSE.md
MAINTAINERS avformat: add Argonaut Games CVG demuxer 2021-05-12 20:25:50 +10:00
Makefile FATE: add a test for sliced scaling 2021-08-08 19:26:05 +02:00
README.md
RELEASE Bump Versions before release/4.4 branch 2021-03-20 01:01:12 +01:00

README.md

FFmpeg README

FFmpeg is a collection of libraries and tools to process multimedia content such as audio, video, subtitles and related metadata.

Libraries

  • libavcodec provides implementation of a wider range of codecs.
  • libavformat implements streaming protocols, container formats and basic I/O access.
  • libavutil includes hashers, decompressors and miscellaneous utility functions.
  • libavfilter provides a mean to alter decoded Audio and Video through chain of filters.
  • libavdevice provides an abstraction to access capture and playback devices.
  • libswresample implements audio mixing and resampling routines.
  • libswscale implements color conversion and scaling routines.

Tools

  • ffmpeg is a command line toolbox to manipulate, convert and stream multimedia content.
  • ffplay is a minimalistic multimedia player.
  • ffprobe is a simple analysis tool to inspect multimedia content.
  • Additional small tools such as aviocat, ismindex and qt-faststart.

Documentation

The offline documentation is available in the doc/ directory.

The online documentation is available in the main website and in the wiki.

Examples

Coding examples are available in the doc/examples directory.

License

FFmpeg codebase is mainly LGPL-licensed with optional components licensed under GPL. Please refer to the LICENSE file for detailed information.

Contributing

Patches should be submitted to the ffmpeg-devel mailing list using git format-patch or git send-email. Github pull requests should be avoided because they are not part of our review process and will be ignored.