/* File: file_mp3.c Copyright (C) 1998-2008 Christophe GRENIER This software is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program 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 General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. */ #if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_mp3) #ifdef HAVE_CONFIG_H #include #endif #ifdef HAVE_STRING_H #include #endif #include #include "types.h" #include "common.h" #include "filegen.h" #include "log.h" #if defined(__FRAMAC__) #include "__fc_builtin.h" #endif #if !defined(SINGLE_FORMAT) extern const file_hint_t file_hint_mkv; extern const file_hint_t file_hint_tiff; #endif /*@ requires valid_register_header_check(file_stat); */ static void register_header_check_mp3(file_stat_t *file_stat); const file_hint_t file_hint_mp3= { .extension="mp3", .description="MP3 audio (MPEG ADTS, layer III, v1)", .max_filesize=PHOTOREC_MAX_FILE_SIZE, .recover=1, .enable_by_default=1, .register_header_check=®ister_header_check_mp3 }; #define MPEG_V25 0 #define MPEG_V2 0x2 #define MPEG_V1 0x3 #define MPEG_L3 0x01 #define MPEG_L2 0x02 #define MPEG_L1 0x03 static const unsigned int sample_rate_table[4][4]={ {11025, 12000, 8000, 0}, /* MPEG_V25 */ { 0, 0, 0, 0}, {22050, 24000, 16000, 0}, /* MPEG_V2 */ {44100, 48000, 32000, 0} /* MPEG_V1 */ }; static const unsigned int bit_rate_table[4][4][16]= { /* MPEG_V25 */ /* MPEG_V_INVALID */ { /* MPEG_L_INVALID */ { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, /* MPEG_L3 */ { 0, 8, 16, 24, 32, 40, 48, 56, 64, 80, 96, 112, 128, 144, 160, 0}, /* MPEG_L2 */ { 0, 8, 16, 24, 32, 40, 48, 56, 64, 80, 96, 112, 128, 144, 160, 0}, /* MPEG_L1 */ { 0, 32, 48, 56, 64, 80, 96, 112, 128, 144, 160, 176, 192, 224, 256, 0} }, { /* MPEG_L_INVALID */ { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, /* MPEG_L3 */ { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, /* MPEG_L2 */ { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, /* MPEG_L1 */ { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, }, /* MPEG_V2 */ { /* MPEG_L_INVALID */ { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, /* MPEG_L3 */ { 0, 8, 16, 24, 32, 40, 48, 56, 64, 80, 96, 112, 128, 144, 160, 0}, /* MPEG_L2 */ { 0, 8, 16, 24, 32, 40, 48, 56, 64, 80, 96, 112, 128, 144, 160, 0}, /* MPEG_L1 */ { 0, 32, 48, 56, 64, 80, 96, 112, 128, 144, 160, 176, 192, 224, 256, 0} }, /* MPEG_V1 */ { /* MPEG_L_INVALID */ { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, /* MPEG_L3 */ { 0, 32, 40, 48, 56, 64, 80, 96, 112, 128, 160, 192, 224, 256, 320, 0}, /* MPEG_L2 */ { 0, 32, 48, 56, 64, 80, 96, 112, 128, 160, 192, 224, 256, 320, 384, 0}, /* MPEG_L1 */ { 0, 32, 64, 96, 128, 160, 192, 224, 256, 288, 320, 352, 294, 416, 448, 0} }, }; /*@ @ requires needle_size > 0; @ requires haystack_size > 0; @ requires \valid_read(needle+(0..needle_size-1)); @ requires \valid_read(haystack+(0..haystack_size-1)); @ ensures \result == 0 || needle_size <= \result <= haystack_size; @ assigns \nothing; @*/ static unsigned int pos_in_mem(const unsigned char *haystack, const unsigned int haystack_size, const unsigned char *needle, const unsigned int needle_size) { unsigned int i; if(haystack_size < needle_size) return 0; /*@ assert haystack_size >= needle_size; */ /*@ @ loop assigns i; @ loop invariant 0 <= i <= haystack_size - needle_size + 1; @ loop variant haystack_size - needle_size - i; @*/ for(i=0; i <= haystack_size - needle_size; i++) if(memcmp(&haystack[i],needle,needle_size)==0) return (i+needle_size); return 0; } /*@ @ requires 0 < buffer_size <= 10*1024*1024; @ requires i <= buffer_size; @ requires \valid_read(buffer+(0..buffer_size-1)); @ ensures \result <= buffer_size + 0x80; @ assigns \nothing; @*/ static unsigned int search_MMT(const unsigned char *buffer, const unsigned int i, const unsigned int buffer_size) { /* Check for MusicMatch Tag http://freenet-homepage.de/StefanRypalla/stuff/musicmatch.txt min size = 8192bytes header is optional structure : header 256 bytes optional image extension 4 bytes image binary >= 4 bytes unused 4 bytes version info 256 bytes audio meta-data >= 7868 bytes In all versions of the MusicMatch format up to and including 3.00, this section (audio meta-data) is always 7868 bytes in length. All subsequent versions allowed three possible lengths for this section: 7936, 8004, and 8132 bytes. data offsets 20 bytes Footer 48 bytes (optional?!) */ const unsigned char mm_header[10]= {'1','8','2','7','3','6','4','5',0x00, 0x00}; const unsigned char mm_pad_version_info[14] = {0x00,0x00,0x00,0x00,'1','8','2','7','3','6','4','5',0x00,0x00}; const char mm_footer[]="Brava Software Inc."; const char mm_footer_tag[]="TAG"; unsigned int size=0; if(i+sizeof(mm_header)>buffer_size) return 0; /*@ assert i + sizeof(mm_header) <= buffer_size; */ if(memcmp(&buffer[i],mm_header,sizeof(mm_header))==0) // Optional Header { size=256; /* Don't check image extension */ /* log_info("search_MMT: mm_header present\n"); */ } else { /* Check image extension */ if( memcmp(&buffer[i]," ",4)!=0 && memcmp(&buffer[i],"bmp ",4)!=0 && memcmp(&buffer[i],"jpg ",4)!=0) return 0; /* log_info("search_MMT: image extension present\n"); */ } { const unsigned int tmp=i+size; const uint32_t *image_size_ptr; uint32_t image_size; if(tmp+8>buffer_size) return 0; /*@ assert tmp + 8 <= buffer_size; */ image_size_ptr = (const uint32_t *)&buffer[tmp+4]; image_size = le32(*image_size_ptr); /* Check if the image size */ if(image_size > buffer_size) return 0; /*@ assert image_size <= buffer_size; */ /* Image binary */ size+=8+image_size; } { const unsigned int tmp=i+size; /* check null padding + version_info */ if(tmp+sizeof(mm_pad_version_info)>buffer_size) { /* FIXME: Is it better to have a partial MusicMatch Tag or none ? */ /* log_trace("search_MMT: partial MusicMatch Tag 1\n"); */ return 0; } /*@ assert tmp + sizeof(mm_pad_version_info) <= buffer_size; */ if(memcmp(&buffer[tmp], mm_pad_version_info, sizeof(mm_pad_version_info))!=0) { /* log_trace("search_MMT: mm_pad_version_info not present\n"); */ return 0; } } size+=4+256; /* padding + version_info */ size+=20; /* data offset */ { const unsigned int tmp=i+size; /* check footer for various audio meta-data size: 7868, 7936, 8004, 8132 */ if(tmp+8132+sizeof(mm_footer) > buffer_size) { /* FIXME: Is it better to have a partial MusicMatch Tag or none ? */ /* log_trace("search_MMT: partial MusicMatch 2\n"); */ return 0; } /*@ assert tmp + 8132 + sizeof(mm_footer) <= buffer_size; */ if( memcmp(&buffer[tmp+7868], mm_footer, sizeof(mm_footer)-1)==0 || memcmp(&buffer[tmp+7868], mm_footer_tag, sizeof(mm_footer_tag) - 1)==0) size+=7868; else if(memcmp(&buffer[tmp+7936], mm_footer, sizeof(mm_footer)-1)==0 || memcmp(&buffer[tmp+7936], mm_footer_tag, sizeof(mm_footer_tag) - 1)==0) size+=7936; else if(memcmp(&buffer[tmp+8004], mm_footer, sizeof(mm_footer)-1)==0 || memcmp(&buffer[tmp+8004], mm_footer_tag, sizeof(mm_footer_tag) - 1)==0) size+=8004; else if(memcmp(&buffer[tmp+8132], mm_footer, sizeof(mm_footer)-1)==0 || memcmp(&buffer[tmp+8132], mm_footer_tag, sizeof(mm_footer_tag)-1)==0) size+=8132; else { /* log_trace("search_MMT: no mm_footer present\n"); */ return 0; } } { const unsigned int tmp=i+size; if(tmp + sizeof(mm_footer) > buffer_size) return 0; /*@ assert tmp + sizeof(mm_footer) <= buffer_size; */ if(memcmp(&buffer[tmp],mm_footer, sizeof(mm_footer)-1)==0) size+=48; /* footer */ else size+=0x80; /* TAG footer */ } /* log_trace("search_MMT: MMT found size=%u (0x%x)\n", size, size); */ return size; } /*@ @ requires buffer_size >= 32; @ requires file_recovery->data_check==&data_check_mp3; @ requires valid_data_check_param(buffer, buffer_size, file_recovery); @ ensures valid_data_check_result(\result, file_recovery); @ ensures \result == DC_CONTINUE || \result == DC_STOP; @ assigns file_recovery->calculated_file_size; @*/ static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) { #ifdef DEBUG_MP3 log_info("data_check_mp3 file_size=%llu, calculated_file_size=%llu\n", (long long unsigned)file_recovery->file_size, (long long unsigned)file_recovery->calculated_file_size); #endif /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */ /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */ /*@ @ loop assigns file_recovery->calculated_file_size; @ loop variant file_recovery->file_size + buffer_size/2 - (file_recovery->calculated_file_size + 16); @*/ while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && file_recovery->calculated_file_size + 16 < file_recovery->file_size + buffer_size/2) { const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size; /*@ assert 0 <= i < buffer_size - 16 ; */ #ifdef DEBUG_MP3 log_info("data_check_mp3 start i=0x%x buffer_size=0x%x calculated_file_size=%lu file_size=%lu\n", i, buffer_size, (long unsigned)file_recovery->calculated_file_size, (long unsigned)file_recovery->file_size); #endif if(buffer[i+0]==0xFF && ((buffer[i+1]&0xE0)==0xE0)) { const unsigned int mpeg_version =(buffer[i+1]>>3)&0x03; const unsigned int mpeg_layer =(buffer[i+1]>>1)&0x03; const unsigned int bit_rate_key =(buffer[i+2]>>4)&0x0F; const unsigned int sampling_rate_key=(buffer[i+2]>>2)&0x03; const unsigned int padding =(buffer[i+2]>>1)&0x01; /*@ split mpeg_version; */ const unsigned int sample_rate =sample_rate_table[mpeg_version][sampling_rate_key]; /*@ assert sample_rate == 0 || 8000 <= sample_rate <= 48000; */ const unsigned int bit_rate =bit_rate_table[mpeg_version][mpeg_layer][bit_rate_key]; unsigned int frameLengthInBytes=0; if(sample_rate==0 || bit_rate==0 || mpeg_layer==MPEG_L1) return DC_STOP; /*@ assert 8000 <= sample_rate <= 48000; */ /*@ assert 0 < bit_rate <= 448; */ if(mpeg_layer==MPEG_L3) { if(mpeg_version==MPEG_V1) frameLengthInBytes = 144000 * bit_rate / sample_rate + padding; else frameLengthInBytes = 72000 * bit_rate / sample_rate + padding; } else if(mpeg_layer==MPEG_L2) frameLengthInBytes = 144000 * bit_rate / sample_rate + padding; else frameLengthInBytes = (12000 * bit_rate / sample_rate + padding)*4; if(frameLengthInBytes<3) return DC_STOP; /*@ assert 3 <= frameLengthInBytes <= 8065; */ file_recovery->calculated_file_size+=frameLengthInBytes; /*@ assert file_recovery->calculated_file_size > 0; */ } else if(buffer[i]=='L' && buffer[i+1]=='Y' && buffer[i+2]=='R' && buffer[i+3]=='I' && buffer[i+4]=='C' && buffer[i+5]=='S' && buffer[i+6]=='B' && buffer[i+7]=='E' && buffer[i+8]=='G' && buffer[i+9]=='I' && buffer[i+10]=='N') { /* Lyrics3 tag http://www.id3.org/Lyrics3 Lyrics3 v2.00 tag http://www.id3.org/Lyrics3v2 Lyrics Header : 'LYRICSBEGIN' (both version) Lyrics Footer : 'LYRICSEND' Lyrics3 tags 'LYRICS200' Lyrics3v2 Tags The maximum length of the lyrics is 5100 bytes for Lyrics3 and 4096 bytes for Lyrics3 v2. */ unsigned int pos_lyrics=0; if(i + 5100 > buffer_size) return DC_STOP; /*@ assert i + 5100 <= buffer_size; */ if((pos_lyrics=pos_in_mem(&buffer[i], 4096, (const unsigned char*)"LYRICS200", 9)) != 0) { /*@ assert 0 < pos_lyrics <= 4096; */ file_recovery->calculated_file_size+=pos_lyrics; /*@ assert file_recovery->calculated_file_size > 0; */ } else if((pos_lyrics=pos_in_mem(&buffer[i], 5100, (const unsigned char*)"LYRICSEND", 9)) != 0) { /*@ assert 0 < pos_lyrics <= 5100; */ file_recovery->calculated_file_size+=pos_lyrics; /*@ assert file_recovery->calculated_file_size > 0; */ } else { /* log_warning("End of Lyrics not found \n"); */ return DC_STOP; } } else if(buffer[i]=='A' && buffer[i+1]=='P' && buffer[i+2]=='E' && buffer[i+3]=='T' && buffer[i+4]=='A' && buffer[i+5]=='G' && buffer[i+6]=='E' && buffer[i+7]=='X') { /* APE Tagv2 (APE Tagv1 has no header) http://wiki.hydrogenaudio.org/index.php?title=APE_Tags_Header */ const uint64_t ape_tag_size = (buffer[i+12] | (buffer[i+13]<<8) | (buffer[i+14]<<16) | ((uint64_t)buffer[i+15]<<24))+(uint64_t)32; /*@ assert ape_tag_size > 0; */ file_recovery->calculated_file_size+=ape_tag_size; /*@ assert file_recovery->calculated_file_size > 0; */ } else if(buffer[i]=='T' && buffer[i+1]=='A' && buffer[i+2]=='G') { /* http://www.id3.org/ID3v1 TAGv1 size = 128 bytes with header "TAG" */ file_recovery->calculated_file_size+=128; /*@ assert file_recovery->calculated_file_size > 0; */ } else if(buffer[i]=='I' && buffer[i+1]=='D' && buffer[i+2]=='3' && (buffer[i+3]==2 || buffer[i+3]==3 || buffer[i+3]==4) && buffer[i+4]==0) { unsigned int potential_frame_offset=0; if(buffer[i+3]==4 && (buffer[i+5]&0x10)==0x10) potential_frame_offset = 10; potential_frame_offset+=((buffer[i+6]&0x7f)<<21) + ((buffer[i+7]&0x7f)<<14) + ((buffer[i+8]&0x7f)<<7) + (buffer[i+9]&0x7f)+ 10; /*@ assert potential_frame_offset > 0; */ file_recovery->calculated_file_size+=potential_frame_offset; /*@ assert file_recovery->calculated_file_size > 0; */ } else { const unsigned int MMT_size=search_MMT(buffer,i,buffer_size); if(MMT_size==0) return DC_STOP; /*@ assert 0 < MMT_size <= buffer_size + 0x80; */ /* log_info("MusicMatch Tag found at offset 0x%x with size 0x%x \n", file_recovery->calculated_file_size, MMT_size); */ file_recovery->calculated_file_size+=MMT_size; /*@ assert file_recovery->calculated_file_size > 0; */ } } return DC_CONTINUE; } /*@ @ requires buffer_size >= 32; @ requires file_recovery->data_check==&data_check_id3; @ requires valid_data_check_param(buffer, buffer_size, file_recovery); @ ensures valid_data_check_result(\result, file_recovery); @ ensures \result == DC_CONTINUE || \result == DC_STOP; @ ensures file_recovery->data_check==&data_check_id3 || file_recovery->data_check==&data_check_mp3; @ assigns file_recovery->data_check, file_recovery->calculated_file_size; @*/ static data_check_t data_check_id3(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) { /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */ /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */ /*@ @ loop assigns file_recovery->data_check, file_recovery->calculated_file_size; @ loop variant file_recovery->file_size + buffer_size/2 - (file_recovery->calculated_file_size + 1); @*/ while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && file_recovery->calculated_file_size + 1 < file_recovery->file_size + buffer_size/2) { const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size; /*@ assert 0 <= i < buffer_size - 1 ; */ if(buffer[i]==0) { /* Padding is present */ file_recovery->calculated_file_size++; } else { /* no more padding or no padding */ file_recovery->data_check=&data_check_mp3; /*@ assert file_recovery->data_check==&data_check_mp3; */ if(data_check_mp3(buffer, buffer_size, file_recovery)!=DC_CONTINUE) return DC_STOP; return DC_CONTINUE; } } /*@ assert file_recovery->data_check==&data_check_id3; */ return DC_CONTINUE; } /*@ @ requires buffer_size >= 10; @ requires separation: \separated(&file_hint_mp3, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); @ terminates \true; @ ensures valid_header_check_result(\result, file_recovery_new); @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_mp3.extension); @ ensures (\result == 1) ==> (file_recovery_new->time == 0); @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size > 0); @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0); @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 287); @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_id3); @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size); @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null); @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension)); @ assigns *file_recovery_new; @*/ static int header_check_id3(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new) { if(buffer[0]=='I' && buffer[1]=='D' && buffer[2]=='3' && (buffer[3]==2 || buffer[3]==3 || buffer[3]==4) && buffer[4]==0) { unsigned int potential_frame_offset=0; /* * TODO Handle ID3 tag * http://www.id3.org/id3v2-00 * http://www.id3.org/id3v2.3.0 */ if(buffer[3]==4 && (buffer[5]&0x10)==0x10) /* a footer is present http://www.id3.org/id3v2.4.0-structure chap. 3.1 */ potential_frame_offset = 10; potential_frame_offset+=((buffer[6]&0x7f)<<21) + ((buffer[7]&0x7f)<<14) + ((buffer[8]&0x7f)<<7) + (buffer[9]&0x7f)+ 10; /* log_info("ID3v2.%u found \n potential_frame_offset at 0x%x\n",buffer[3], potential_frame_offset); */ reset_file_recovery(file_recovery_new); file_recovery_new->calculated_file_size=potential_frame_offset; /*@ assert file_recovery_new->calculated_file_size > 0; */ file_recovery_new->min_filesize=287; file_recovery_new->data_check=&data_check_id3; file_recovery_new->extension=file_hint_mp3.extension; file_recovery_new->file_check=&file_check_size; return 1; } return 0; } /*@ @ requires buffer_size >= 6; @ requires separation: \separated(&file_hint_mp3, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); @ ensures valid_header_check_result(\result, file_recovery_new); @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_mp3.extension); @ ensures (\result == 1) ==> (file_recovery_new->time == 0); @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size > 0); @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0); @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 287); @ ensures (\result == 1 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->data_check == &data_check_mp3); @ ensures (\result == 1 && file_recovery_new->blocksize >= 16) ==> (file_recovery_new->file_check == &file_check_size); @ ensures (\result == 1 && file_recovery_new->blocksize < 16) ==> (file_recovery_new->data_check == \null); @ ensures (\result == 1 && file_recovery_new->blocksize < 16) ==> (file_recovery_new->file_check == \null); @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null); @*/ static int header_check_mp3(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new) { unsigned int potential_frame_offset=0; unsigned int nbr=0; /* A Frame sync 11 (length in bits) B MPEG audio version (MPEG-1, 2, etc.) 2 C MPEG layer (Layer I, II, III, etc.) 2 D Protection (if on, then checksum follows header) 1 AAAA AAAA AAAB BCCD 1111 1111 1111 1010 = FA = MPEG-1 layer 3 1111 1111 1111 0010 = F2 = MPEG-2 layer 3 1111 1111 1110 0010 = E2 = MPEG-2.5 layer 3 http://www.dv.co.yu/mpgscript/mpeghdr.htm */ if(!(buffer[0]==0xFF && ((buffer[1]&0xFE)==0xFA || (buffer[1]&0xFE)==0xF2 || (buffer[1]&0xFE)==0xE2))) return 0; /*@ assert nbr == 0; */ /*@ @ loop invariant 0 <= nbr <= potential_frame_offset <= 8192 + 8065; @ loop assigns potential_frame_offset,nbr; @ loop variant 8192 - potential_frame_offset; @*/ while(potential_frame_offset+1 < buffer_size && potential_frame_offset+1 < 8192) { if(buffer[potential_frame_offset+0]!=0xFF) return 0; { const unsigned int mpeg_version =(buffer[potential_frame_offset+1]>>3)&0x03; const unsigned int mpeg_layer =(buffer[potential_frame_offset+1]>>1)&0x03; const unsigned int bit_rate_key =(buffer[potential_frame_offset+2]>>4)&0x0F; const unsigned int sampling_rate_key=(buffer[potential_frame_offset+2]>>2)&0x03; const unsigned int padding =(buffer[potential_frame_offset+2]>>1)&0x01; /*@ split mpeg_version; */ const unsigned int bit_rate =bit_rate_table[mpeg_version][mpeg_layer][bit_rate_key]; const unsigned int sample_rate =sample_rate_table[mpeg_version][sampling_rate_key]; unsigned int frameLengthInBytes=0; if(sample_rate==0 || bit_rate==0 || mpeg_layer==MPEG_L1) return 0; /*@ assert 8000 <= sample_rate <= 48000; */ /*@ assert 0 < bit_rate <= 448; */ if(mpeg_layer==MPEG_L3) { if(mpeg_version==MPEG_V1) frameLengthInBytes = 144000 * bit_rate / sample_rate + padding; else frameLengthInBytes = 72000 * bit_rate / sample_rate + padding; } else if(mpeg_layer==MPEG_L2) frameLengthInBytes = 144000 * bit_rate / sample_rate + padding; else frameLengthInBytes = (12000 * bit_rate / sample_rate + padding)*4; #ifdef DEBUG_MP3 log_info("framesize: %u, layer: %u, bitrate: %u, padding: %u\n", frameLengthInBytes, 4-mpeg_layer, bit_rate, padding); #endif if(frameLengthInBytes<3) return 0; /*@ assert 3 <= frameLengthInBytes <= 8065; */ potential_frame_offset+=frameLengthInBytes; /*@ assert potential_frame_offset > 0; */ nbr++; } } if(nbr<=1) return 0; if(file_recovery->file_stat!=NULL && file_recovery->file_check!=NULL) { if(file_recovery->file_stat->file_hint==&file_hint_mp3 #if !defined(SINGLE_FORMAT) || file_recovery->file_stat->file_hint==&file_hint_mkv #endif ) { header_ignored(file_recovery_new); return 0; } #if !defined(SINGLE_FORMAT) /* RGV values from TIFF may be similar to the beginning of an mp3 */ if(file_recovery->file_stat->file_hint==&file_hint_tiff && buffer[0]==buffer[3] && buffer[1]==buffer[4] && buffer[2]==buffer[5]) { if(header_ignored_adv(file_recovery, file_recovery_new)==0) return 0; } #endif } /*@ assert nbr > 1; */ /*@ assert potential_frame_offset > 0; */ #ifdef DEBUG_MP3 log_info("header_check_mp3 mp3 found\n"); #endif reset_file_recovery(file_recovery_new); /*@ assert file_recovery_new->file_check == \null; */ /*@ assert file_recovery_new->data_check == \null; */ file_recovery_new->calculated_file_size=potential_frame_offset; /*@ assert file_recovery_new->calculated_file_size > 0; */ file_recovery_new->min_filesize=287; file_recovery_new->extension=file_hint_mp3.extension; if(file_recovery_new->blocksize >= 16) { file_recovery_new->data_check=&data_check_mp3; file_recovery_new->file_check=&file_check_size; } return 1; } /*@ @ requires valid_register_header_check(file_stat); @*/ static void register_header_check_mp3(file_stat_t *file_stat) { static const unsigned char mpeg1_L3_header1[2]= {0xFF, 0xFA}; static const unsigned char mpeg1_L3_header2[2]= {0xFF, 0xFB}; static const unsigned char mpeg2_L3_header1[2]= {0xFF, 0xF2}; static const unsigned char mpeg2_L3_header2[2]= {0xFF, 0xF3}; static const unsigned char mpeg25_L3_header1[2]={0xFF, 0xE2}; static const unsigned char mpeg25_L3_header2[2]={0xFF, 0xE3}; register_header_check(0, "ID3", 3, &header_check_id3, file_stat); register_header_check(0, mpeg1_L3_header1, sizeof(mpeg1_L3_header1), &header_check_mp3, file_stat); register_header_check(0, mpeg1_L3_header2, sizeof(mpeg1_L3_header2), &header_check_mp3, file_stat); register_header_check(0, mpeg2_L3_header1, sizeof(mpeg2_L3_header1), &header_check_mp3, file_stat); register_header_check(0, mpeg2_L3_header2, sizeof(mpeg2_L3_header2), &header_check_mp3, file_stat); register_header_check(0, mpeg25_L3_header1, sizeof(mpeg25_L3_header1), &header_check_mp3, file_stat); register_header_check(0, mpeg25_L3_header2, sizeof(mpeg25_L3_header2), &header_check_mp3, file_stat); } #endif #if defined(MAIN_mp3) #define BLOCKSIZE 65536u static int main_id3() { const char fn[] = "recup_dir.1/f0000000.mp3"; unsigned char buffer[BLOCKSIZE]; file_recovery_t file_recovery_new; file_recovery_t file_recovery; file_stat_t file_stats; /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */ #if defined(__FRAMAC__) Frama_C_make_unknown((char *)buffer, BLOCKSIZE); #endif reset_file_recovery(&file_recovery); file_recovery.blocksize=BLOCKSIZE; file_recovery_new.blocksize=BLOCKSIZE; file_recovery_new.data_check=NULL; file_recovery_new.file_stat=NULL; file_recovery_new.file_check=NULL; file_recovery_new.file_rename=NULL; file_recovery_new.calculated_file_size=0; file_recovery_new.file_size=0; file_recovery_new.location.start=0; file_stats.file_hint=&file_hint_mp3; file_stats.not_recovered=0; file_stats.recovered=0; register_header_check_mp3(&file_stats); if(header_check_id3(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new) != 1) return 0; /*@ assert valid_read_string((char *)&fn); */ memcpy(file_recovery_new.filename, fn, sizeof(fn)); file_recovery_new.file_stat=&file_stats; /*@ assert valid_read_string((char *)file_recovery_new.filename); */ /*@ assert file_recovery_new.extension == file_hint_mp3.extension; */ /*@ assert file_recovery_new.calculated_file_size > 0; */ /*@ assert file_recovery_new.file_size == 0; */ /*@ assert file_recovery_new.min_filesize == 287; */ /*@ assert file_recovery_new.data_check == &data_check_id3; */ /*@ assert file_recovery_new.file_rename == \null; */ { unsigned char big_buffer[2*BLOCKSIZE]; data_check_t res_data_check=DC_CONTINUE; memset(big_buffer, 0, BLOCKSIZE); memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE); /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */; res_data_check=data_check_id3(big_buffer, 2*BLOCKSIZE, &file_recovery_new); /*@ assert file_recovery_new.data_check == &data_check_id3 || file_recovery_new.data_check == &data_check_mp3; */ /*@ assert res_data_check == DC_CONTINUE && file_recovery_new.data_check == &data_check_mp3 ==> (file_recovery_new.calculated_file_size >= file_recovery_new.file_size + BLOCKSIZE - 16); */ /*@ assert res_data_check == DC_CONTINUE && file_recovery_new.data_check == &data_check_id3 ==> (file_recovery_new.calculated_file_size >= file_recovery_new.file_size + BLOCKSIZE - 1); */ /*@ assert res_data_check == DC_CONTINUE ==> (file_recovery_new.calculated_file_size >= file_recovery_new.file_size + BLOCKSIZE - 16); */ file_recovery_new.file_size+=BLOCKSIZE; if(res_data_check == DC_CONTINUE) { /*@ assert file_recovery_new.calculated_file_size >= file_recovery_new.file_size - 16; */ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE); #if defined(__FRAMAC__) Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE); #endif file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new); } } if(file_recovery_new.file_stat!=NULL) { file_recovery_t file_recovery_new2; /* Test when another file of the same is detected in the next block */ file_recovery_new2.blocksize=BLOCKSIZE; file_recovery_new2.file_stat=NULL; file_recovery_new2.file_check=NULL; file_recovery_new2.location.start=BLOCKSIZE; file_recovery_new.handle=NULL; /* In theory should be not null */ header_check_id3(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2); } if(file_recovery_new.file_check!=NULL) { file_recovery_new.handle=fopen(fn, "rb"); if(file_recovery_new.handle!=NULL) { (file_recovery_new.file_check)(&file_recovery_new); fclose(file_recovery_new.handle); } } return 0; } static int main_mp3() { const char fn[] = "recup_dir.1/f0000000.mp3"; unsigned char buffer[BLOCKSIZE]; file_recovery_t file_recovery_new; file_recovery_t file_recovery; file_stat_t file_stats; /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */ #if defined(__FRAMAC__) Frama_C_make_unknown((char *)buffer, BLOCKSIZE); #endif reset_file_recovery(&file_recovery); file_recovery.blocksize=BLOCKSIZE; file_recovery_new.blocksize=BLOCKSIZE; file_recovery_new.data_check=NULL; file_recovery_new.file_stat=NULL; file_recovery_new.file_check=NULL; file_recovery_new.file_rename=NULL; file_recovery_new.calculated_file_size=0; file_recovery_new.file_size=0; file_recovery_new.location.start=0; file_stats.file_hint=&file_hint_mp3; file_stats.not_recovered=0; file_stats.recovered=0; register_header_check_mp3(&file_stats); if(header_check_mp3(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1) return 0; /*@ assert valid_read_string((char *)&fn); */ memcpy(file_recovery_new.filename, fn, sizeof(fn)); /*@ assert file_recovery_new.file_size == 0; */ /*@ assert file_recovery_new.min_filesize == 287; */ /*@ assert file_recovery_new.extension == file_hint_mp3.extension; */ /*@ assert file_recovery_new.calculated_file_size > 0; */ /*@ assert file_recovery_new.file_rename == \null; */ file_recovery_new.file_stat=&file_stats; if(file_recovery_new.file_stat!=NULL && file_recovery_new.file_stat->file_hint!=NULL && file_recovery_new.data_check!=NULL) { unsigned char big_buffer[2*BLOCKSIZE]; data_check_t res_data_check=DC_CONTINUE; memset(big_buffer, 0, BLOCKSIZE); memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE); /*@ assert file_recovery_new.data_check == &data_check_mp3; */ /*@ assert file_recovery_new.file_size == 0; */; /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */; res_data_check=data_check_mp3(big_buffer, 2*BLOCKSIZE, &file_recovery_new); /*@ assert res_data_check == DC_CONTINUE ==> (file_recovery_new.calculated_file_size >= file_recovery_new.file_size + BLOCKSIZE - 16); */ file_recovery_new.file_size+=BLOCKSIZE; if(res_data_check == DC_CONTINUE) { /*@ assert file_recovery_new.calculated_file_size >= file_recovery_new.file_size - 16; */ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE); #if defined(__FRAMAC__) Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE); #endif file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new); } } if(file_recovery_new.file_stat!=NULL) { file_recovery_t file_recovery_new2; /* Test when another file of the same is detected in the next block */ file_recovery_new2.blocksize=BLOCKSIZE; file_recovery_new2.file_stat=NULL; file_recovery_new2.file_check=NULL; file_recovery_new2.location.start=BLOCKSIZE; file_recovery_new.handle=NULL; /* In theory should be not null */ header_check_mp3(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2); } if(file_recovery_new.file_check!=NULL) { /*@ assert valid_read_string((char *)file_recovery_new.filename); */ file_recovery_new.handle=fopen(fn, "rb"); if(file_recovery_new.handle!=NULL) { (file_recovery_new.file_check)(&file_recovery_new); fclose(file_recovery_new.handle); } } return 0; } int main() { main_mp3(); main_id3(); return 0; } #endif