luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

src/file_jpg.c: make most code frama-c friendly, file_tiff* modified to help

Browse source
This commit is contained in:
Christophe Grenier 2019-11-23 18:30:36 +01:00
parent 7e8f99aa92
commit b310abea46
5 changed files with 363 additions and 219 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

340
src/file_jpg.c
View file

@ -288,7 +288,6 @@ static uint64_t check_mpo_le(const unsigned char *mpo, const uint64_t mpo_offset
@*/
static uint64_t check_mpo(const unsigned char *mpo, const uint64_t offset, const unsigned int size)
{
#ifndef MAIN_jpg
if(mpo[0]=='I' && mpo[1]=='I' && mpo[2]=='*' && mpo[3]==0)
{
return check_mpo_le(mpo, offset, size);
@ -297,13 +296,13 @@ static uint64_t check_mpo(const unsigned char *mpo, const uint64_t offset, const
{
return check_mpo_be(mpo, offset, size);
}
#endif
return 0;
}
/*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
@ requires valid_read_string((char *)&fr->filename);
@ requires \initialized(&fr->time);
@*/
static void file_check_mpo(file_recovery_t *fr)
@ -401,9 +400,37 @@ static int is_marker_valid(const unsigned int marker)
}
}
/*@
@ requires \valid_read(buffer + (0 .. buffer_size-1));
@*/
static time_t jpg_get_date(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int i, const unsigned int size)
{ /* APP1 Exif information */
const unsigned int tiff_offset=i+2+8;
if(tiff_offset < buffer_size && size > 8)
{
/*@ assert tiff_offset < buffer_size; */
/*@ assert size > 8; */
unsigned int tiff_size=size-0x08;
if(buffer_size - tiff_offset < tiff_size)
{
tiff_size=buffer_size - tiff_offset;
/*@ assert tiff_offset + tiff_size == buffer_size; */
}
else
{
/*@ assert tiff_offset + tiff_size <= buffer_size; */
}
/*@ assert tiff_offset + tiff_size <= buffer_size; */
return get_date_from_tiff_header(&buffer[tiff_offset], tiff_size);
}
return 0;
}
/*@
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid_read(file_recovery);
@ requires file_recovery->file_stat==\null || valid_read_string((char*)&file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ ensures \result == 0 || \result == 1;
@ -530,22 +557,14 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
}
while(i+4<buffer_size && buffer[i]==0xff && is_marker_valid(buffer[i+1]))
{
const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
if(buffer[i+1]==0xff)
i++;
else
{
if(buffer[i+1]==0xe1)
{ /* APP1 Exif information */
const unsigned int tmp=2+(buffer[i+2]<<8)+buffer[i+3];
if(i+0x0A < buffer_size && tmp > 0x0A)
{
unsigned int tiff_size=tmp-0x0A;
if(buffer_size - (i+0x0A) < tiff_size)
tiff_size=buffer_size - (i+0x0A);
#ifndef MAIN_jpg
jpg_time=get_date_from_tiff_header(&buffer[i+0x0A], tiff_size);
#endif
}
jpg_time=jpg_get_date(buffer, buffer_size, i, size);
}
else if(buffer[i+1]==0xc4)
{
@ -553,7 +572,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
if(jpg_check_dht(buffer, buffer_size, i, 2+(buffer[i+2]<<8)+buffer[i+3])!=0)
return 0;
}
i+=2+(buffer[i+2]<<8)+buffer[i+3];
i+=2+size;
}
}
if(i+1 < file_recovery_new->blocksize && buffer[i+1]!=0xda)
@ -572,8 +591,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
return 1;
}
#ifndef MAIN_jpg
#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && !defined(__FRAMAC__)
struct my_error_mgr {
struct jpeg_error_mgr pub; /* "public" fields, must be the first field */
@ -1378,7 +1396,6 @@ static void jpg_check_picture(file_recovery_t *file_recovery)
}
}
#endif
#endif
/*@
@ requires i < buffer_size;
@ -1461,6 +1478,7 @@ static int jpg_check_sof0(const unsigned char *buffer, const unsigned int buffer
@ requires \valid(file_recovery->handle);
@ requires file_recovery->blocksize <= 1048576;
@ requires file_recovery->offset_error <= (1<<63) - 1;
@ ensures \valid(file_recovery->handle);
@*/
static void jpg_search_marker(file_recovery_t *file_recovery)
{
@ -1498,6 +1516,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
@ loop invariant offset + i >= offset_test;
@ loop invariant offset_test >= file_recovery->offset_error;
@ loop invariant 0 <= i < nbytes + file_recovery->blocksize;
@ loop assigns i,file_recovery->extra;
@*/
while(i+1<nbytes)
{
@ -1514,12 +1533,14 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
)
{
file_recovery->extra=tmp - file_recovery->offset_error;
#ifndef __FRAMAC__
if(file_recovery->extra % file_recovery->blocksize != 0)
{
log_info("jpg_search_marker %s extra=%llu\n",
file_recovery->filename,
(long long unsigned)file_recovery->extra);
}
#endif
return ;
}
i+=file_recovery->blocksize;
@ -1533,6 +1554,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
@ requires \valid(file_recovery);
@ requires \valid(file_recovery->handle);
@ requires \valid(thumb_offset);
@ requires valid_read_string((char *)&file_recovery->filename);
@ requires file_recovery->blocksize > 0;
@ requires \valid_read(buffer + (0 .. nbytes-1));
@ requires \initialized(&file_recovery->time);
@ -1541,158 +1563,158 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
static int jpg_check_app1(file_recovery_t *file_recovery, const unsigned int extract_thumb, const unsigned char *buffer, const unsigned int i, const unsigned int offset, const unsigned int size, const size_t nbytes, uint64_t *thumb_offset)
{ /* APP1 Exif information */
const unsigned int tiff_offset=i+2+8;
if(tiff_offset < nbytes && size > 8)
const unsigned char *potential_error=NULL;
const unsigned char *thumb_data=NULL;
const unsigned char *tiff;
unsigned int thumb_size=0;
unsigned int tiff_size;
if(tiff_offset >= nbytes || size <= 8)
return 1;
/*@ assert tiff_offset < nbytes; */
/*@ assert size > 8; */
tiff_size=size-0x08;
if(nbytes - tiff_offset < tiff_size)
{
tiff_size=nbytes - tiff_offset;
/*@ assert tiff_offset + tiff_size == nbytes; */
}
else
{
/*@ assert tiff_offset < nbytes; */
/*@ assert size > 8; */
const unsigned char *potential_error=NULL;
unsigned int tiff_size=size-0x08;
const unsigned char *thumb_data=NULL;
unsigned int thumb_size=0;
if(nbytes - tiff_offset < tiff_size)
{
tiff_size=nbytes - tiff_offset;
/*@ assert tiff_offset + tiff_size == nbytes; */
}
else
{
/*@ assert tiff_offset + tiff_size <= nbytes; */
}
/*@ assert tiff_offset + tiff_size <= nbytes; */
if(tiff_size<sizeof(TIFFHeader))
return 1;
/*@ assert tiff_size >= sizeof(TIFFHeader); */
{
/*@ assert \valid_read(buffer + (0 .. tiff_offset+tiff_size-1)); */
/*@ assert \valid_read((buffer + tiff_offset) + (0 .. tiff_size-1)); */
const unsigned char *tiff=&buffer[tiff_offset];
/*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
if(file_recovery->time==0)
{
/*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
file_recovery->time=get_date_from_tiff_header(tiff, tiff_size);
}
#ifndef __FRAMAC__
*thumb_offset=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error);
if(*thumb_offset!=0)
{
*thumb_offset+=tiff_offset;
thumb_data=buffer+ (*thumb_offset);
thumb_size=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFBYTECOUNT, &potential_error);
}
}
/*@ assert tiff_offset + tiff_size <= nbytes; */
if(tiff_size<sizeof(TIFFHeader))
return 1;
/*@ assert tiff_size >= sizeof(TIFFHeader); */
/*@ assert \valid_read(buffer + (0 .. tiff_offset+tiff_size-1)); */
/*@ assert \valid_read((buffer + tiff_offset) + (0 .. tiff_size-1)); */
tiff=&buffer[tiff_offset];
/*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
if(file_recovery->time==0)
{
/*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
file_recovery->time=get_date_from_tiff_header(tiff, tiff_size);
}
*thumb_offset=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error);
if(*thumb_offset!=0)
{
*thumb_offset+=tiff_offset;
thumb_data=buffer+ (*thumb_offset);
thumb_size=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFBYTECOUNT, &potential_error);
}
if(potential_error!=NULL)
{
file_recovery->offset_error=potential_error-buffer;
return 0;
}
if(file_recovery->offset_ok<i)
file_recovery->offset_ok=i;
if(thumb_data!=0 && thumb_size!=0 && *thumb_offset < nbytes - 1)
{
unsigned int j=*thumb_offset+2;
unsigned int thumb_sos_found=0;
#ifdef DEBUG_JPEG
unsigned int j_old=j;
#endif
if(potential_error!=NULL)
if(buffer[*thumb_offset]!=0xff)
{
file_recovery->offset_error=*thumb_offset;
jpg_search_marker(file_recovery);
return 0;
}
if(buffer[*thumb_offset+1]!=0xd8)
{
file_recovery->offset_error=*thumb_offset+1;
return 0;
}
while(j+4<nbytes && thumb_sos_found==0)
{
if(buffer[j]!=0xff)
{
file_recovery->offset_error=potential_error-buffer;
file_recovery->offset_error=j;
#ifdef DEBUG_JPEG
log_info("%s thumb no marker at 0x%x\n", file_recovery->filename, j);
log_error("%s Error between %u and %u\n", file_recovery->filename, j_old, j);
#endif
jpg_search_marker(file_recovery);
return 0;
}
if(file_recovery->offset_ok<i)
file_recovery->offset_ok=i;
#ifndef MAIN_jpg
if(thumb_data!=0 && thumb_size!=0)
if(buffer[j+1]==0xff)
{
if(*thumb_offset < nbytes - 1)
/* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/
j++;
continue;
}
#ifdef DEBUG_JPEG
log_info("%s thumb marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
#endif
if(buffer[j+1]==0xda) /* Thumb SOS: Start Of Scan */
thumb_sos_found=1;
else if(buffer[j+1]==0xc4) /* DHT */
{
if(jpg_check_dht(buffer, nbytes, j, 2+(buffer[j+2]<<8)+buffer[j+3])!=0)
{
unsigned int j=*thumb_offset+2;
unsigned int thumb_sos_found=0;
file_recovery->offset_error=j+2;
return 0;
}
}
else if(buffer[j+1]==0xdb || /* DQT */
buffer[j+1]==0xc0 || /* SOF0 */
buffer[j+1]==0xdd) /* DRI */
{
}
else if((buffer[j+1]>=0xc0 && buffer[j+1]<=0xcf) || /* SOF0 - SOF15 */
(buffer[j+1]>=0xe0 && buffer[j+1]<=0xef) || /* APP0 - APP15 */
buffer[j+1]==0xfe) /* COM */
{
/* Unusual marker, bug ? */
}
else
{
log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
file_recovery->offset_error=j;
return 0;
}
if(file_recovery->offset_ok<j)
file_recovery->offset_ok=j;
#ifdef DEBUG_JPEG
unsigned int j_old=j;
j_old=j;
#endif
if(buffer[*thumb_offset]!=0xff)
j+=2U+(buffer[j+2]<<8)+buffer[j+3];
}
if(thumb_sos_found>0 && extract_thumb>0
&& offset < nbytes && buffer[offset]==0xff)
{
char *thumbname;
/*@ assert valid_read_string((char *)&file_recovery->filename); */
#ifndef __FRAMAC__
thumbname=strdup(file_recovery->filename);
if(thumbname!=NULL)
{
char *sep;
/*@ assert thumbname!=\null; */
/*@ assert valid_read_string(thumbname); */
sep=strrchr(thumbname,'/');
if(sep!=NULL && *(sep+1)=='f' && *thumb_offset+thumb_size < nbytes)
{
FILE *out;
*(sep+1)='t';
if((out=fopen(thumbname,"wb"))!=NULL)
{
file_recovery->offset_error=*thumb_offset;
jpg_search_marker(file_recovery);
return 0;
if(fwrite(&buffer[*thumb_offset], thumb_size, 1, out) < 1)
{
log_error("Can't write to %s: %s\n", thumbname, strerror(errno));
}
fclose(out);
if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1)
set_date(thumbname, file_recovery->time, file_recovery->time);
}
if(buffer[*thumb_offset+1]!=0xd8)
else
{
file_recovery->offset_error=*thumb_offset+1;
return 0;
}
while(j+4<nbytes && thumb_sos_found==0)
{
if(buffer[j]!=0xff)
{
file_recovery->offset_error=j;
#ifdef DEBUG_JPEG
log_info("%s thumb no marker at 0x%x\n", file_recovery->filename, j);
log_error("%s Error between %u and %u\n", file_recovery->filename, j_old, j);
#endif
jpg_search_marker(file_recovery);
return 0;
}
if(buffer[j+1]==0xff)
{
/* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/
j++;
continue;
}
#ifdef DEBUG_JPEG
log_info("%s thumb marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
#endif
if(buffer[j+1]==0xda) /* Thumb SOS: Start Of Scan */
thumb_sos_found=1;
else if(buffer[j+1]==0xc4) /* DHT */
{
if(jpg_check_dht(buffer, nbytes, j, 2+(buffer[j+2]<<8)+buffer[j+3])!=0)
{
file_recovery->offset_error=j+2;
return 0;
}
}
else if(buffer[j+1]==0xdb || /* DQT */
buffer[j+1]==0xc0 || /* SOF0 */
buffer[j+1]==0xdd) /* DRI */
{
}
else if((buffer[j+1]>=0xc0 && buffer[j+1]<=0xcf) || /* SOF0 - SOF15 */
(buffer[j+1]>=0xe0 && buffer[j+1]<=0xef) || /* APP0 - APP15 */
buffer[j+1]==0xfe) /* COM */
{
/* Unusual marker, bug ? */
}
else
{
log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
file_recovery->offset_error=j;
return 0;
}
if(file_recovery->offset_ok<j)
file_recovery->offset_ok=j;
#ifdef DEBUG_JPEG
j_old=j;
#endif
j+=2U+(buffer[j+2]<<8)+buffer[j+3];
}
if(thumb_sos_found>0 && extract_thumb>0
&& offset < nbytes && buffer[offset]==0xff)
{
char *thumbname;
char *sep;
thumbname=strdup(file_recovery->filename);
sep=strrchr(thumbname,'/');
if(sep!=NULL && *(sep+1)=='f' && *thumb_offset+thumb_size < nbytes)
{
FILE *out;
*(sep+1)='t';
if((out=fopen(thumbname,"wb"))!=NULL)
{
if(fwrite(&buffer[*thumb_offset], thumb_size, 1, out) < 1)
{
log_error("Can't write to %s: %s\n", thumbname, strerror(errno));
}
fclose(out);
if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1)
set_date(thumbname, file_recovery->time, file_recovery->time);
}
else
{
log_error("fopen %s failed\n", thumbname);
}
}
free(thumbname);
log_error("fopen %s failed\n", thumbname);
}
}
free(thumbname);
}
#endif
}
@ -1705,6 +1727,7 @@ static int jpg_check_app1(file_recovery_t *file_recovery, const unsigned int ext
@ requires \valid(file_recovery->handle);
@ requires file_recovery->blocksize > 0;
@ requires \initialized(&file_recovery->time);
@ requires valid_read_string((char *)&file_recovery->filename);
*/
static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsigned int extract_thumb)
{
@ -1740,7 +1763,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
if(buffer[i]!=0xff)
{
#ifdef DEBUG_JPEG
#if defined(DEBUG_JPEG) && !defined(__FRAMAC__)
log_info("%s no marker at 0x%x\n", file_recovery->filename, i);
#endif
file_recovery->offset_error=i;
@ -1753,7 +1776,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
offset++;
continue;
}
#ifdef DEBUG_JPEG
#if defined(DEBUG_JPEG) && !defined(__FRAMAC__)
log_info("%s marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i);
#endif
offset+=(uint64_t)2+size;
@ -1788,7 +1811,9 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
}
else
{
#ifndef __FRAMAC__
log_info("%s unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i+1);
#endif
file_recovery->offset_error=i+1;
return thumb_offset;
}
@ -1804,6 +1829,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
/*@
@ requires \valid(file_recovery);
@ requires \valid(file_recovery->handle);
@ requires valid_read_string((char *)&file_recovery->filename);
@ requires \initialized(&file_recovery->time);
@*/
static void file_check_jpg(file_recovery_t *file_recovery)
@ -1828,7 +1854,7 @@ static void file_check_jpg(file_recovery_t *file_recovery)
#ifdef DEBUG_JPEG
log_info("jpg_check_structure error at %llu\n", (long long unsigned)file_recovery->offset_error);
#endif
#ifndef MAIN_jpg
#ifndef __FRAMAC__
#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
if(thumb_offset!=0 &&
(file_recovery->checkpoint_status==0 || thumb_error!=0) &&
@ -1857,7 +1883,7 @@ static void file_check_jpg(file_recovery_t *file_recovery)
#endif
if(file_recovery->offset_error!=0)
return ;
#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && ! defined(MAIN_jpg)
#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && ! defined(__FRAMAC__)
jpg_check_picture(file_recovery);
#else
file_recovery->file_size=file_recovery->calculated_file_size;

9
src/file_tiff.c
View file

@ -140,8 +140,11 @@ const char *tag_name(unsigned int tag)
unsigned int find_tag_from_tiff_header(const unsigned char*buffer, const unsigned int buffer_size, const unsigned int tag, const unsigned char **potential_error)
{
const TIFFHeader *tiff=(const TIFFHeader *)buffer;
if(buffer_size < sizeof(TIFFHeader))
/*@ assert sizeof(TIFFHeader) <= sizeof(struct ifd_header); */
if(buffer_size < sizeof(struct ifd_header))
return 0;
/*@ assert buffer_size >= sizeof(TIFFHeader); */
/*@ assert buffer_size >= sizeof(struct ifd_header); */
#ifndef MAIN_tiff_le
if(tiff->tiff_magic==TIFF_BIGENDIAN)
return find_tag_from_tiff_header_be(buffer, buffer_size, tag, potential_error);
@ -159,9 +162,11 @@ time_t get_date_from_tiff_header(const unsigned char *buffer, const unsigned int
unsigned int date_asc=0;
time_t tmp;
/*@ assert \valid_read(buffer+(0..buffer_size-1)); */
if(buffer_size < sizeof(TIFFHeader) || buffer_size < 19)
/*@ assert sizeof(TIFFHeader) <= sizeof(struct ifd_header); */
if(buffer_size < sizeof(struct ifd_header) || buffer_size < 19)
return (time_t)0;
/*@ assert buffer_size >= sizeof(TIFFHeader); */
/*@ assert buffer_size >= sizeof(struct ifd_header); */
/* DateTimeOriginal */
date_asc=find_tag_from_tiff_header(buffer, buffer_size, 0x9003, &potential_error);
/* DateTimeDigitalized*/

1
src/file_tiff.h
View file

@ -69,7 +69,6 @@ struct ifd_header {
} __attribute__ ((gcc_struct, __packed__));
/*@
@ requires buffer_size >= sizeof(TIFFHeader);
@ requires \valid_read(buffer+(0..buffer_size-1));
@ ensures \valid_read(buffer+(0..buffer_size-1));
@*/

117
src/file_tiff_be.c
View file

@ -126,7 +126,7 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char *buffer, const uns
return 0;
/*@ assert \valid_read(buffer+(0..tiff_size-1)); */
/*@ assert offset_ifd0 + sizeof(struct ifd_header) <= tiff_size; */
/*@ assert \valid_read(buffer+(0..offset_ifd0 + sizeof(struct ifd_header)-1)); */
/*X assert \valid_read(buffer+(0..offset_ifd0 + sizeof(struct ifd_header)-1)); */
{
const unsigned int tmp=find_tag_from_tiff_header_be_aux(buffer, tiff_size, tag, potential_error, offset_ifd0);
/*@ assert \valid_read(buffer+(0..tiff_size-1)); */
@ -259,6 +259,7 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
data_read=fread(buffer, 1, sizeof(buffer), in);
if(data_read<2)
return TIFF_ERROR;
/*@ assert data_read >= 2; */
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, sizeof(buffer));
#endif
@ -336,16 +337,55 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
#endif
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
/*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
@ requires \separated(&errno, fr);
@ requires \valid_read(buffer + (0 .. buffer_size - 1));
@ ensures \valid(fr);
@ ensures \valid(fr->handle);
@ ensures valid_read_string(fr->extension);
@
*/
@*/
static uint64_t file_check_tiff_be_aux_next(file_recovery_t *fr, const unsigned int depth, const unsigned int count, const unsigned char *buffer, const unsigned int buffer_size, const unsigned int offset_ptr_offset)
{
if(buffer_size < 4)
return 0;
/*@ assert buffer_size >= 4; */
if(offset_ptr_offset > buffer_size-4)
return 0;
{
/*@ assert offset_ptr_offset <= buffer_size - 4; */
/*@ assert offset_ptr_offset + 4 <= buffer_size; */
/*@ assert \valid_read(buffer + (0 .. offset_ptr_offset + 4 - 1)); */
const unsigned char *ptr_offset=&buffer[offset_ptr_offset];
/*@ assert \valid_read(ptr_offset + (0 .. 4 - 1)); */
const uint32_t *ptr32_offset=(const uint32_t *)ptr_offset;
/*@ assert \valid_read(ptr32_offset); */
const unsigned int next_diroff=be32(*ptr32_offset);
if(next_diroff == 0)
return 0;
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
return file_check_tiff_be_aux(fr, next_diroff, depth+1, count+1);
}
}
/*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
@ requires \separated(&errno, fr);
@ ensures \valid(fr);
@ ensures \valid(fr->handle);
@ ensures valid_read_string(fr->extension);
@*/
static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
{
unsigned char buffer[8192];
@ -369,6 +409,9 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
const TIFFDirEntry *entry_strip_bytecounts=NULL;
const TIFFDirEntry *entry_tile_offsets=NULL;
const TIFFDirEntry *entry_tile_bytecounts=NULL;
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
#ifdef DEBUG_TIFF
log_info("file_check_tiff_be_aux(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
#endif
@ -395,6 +438,7 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
#endif
if(n==0)
return TIFF_ERROR;
/*@ assert 0 < n <= 65535; */
/*@ assert sizeof(TIFFDirEntry)==12; */
/*X
X loop invariant 0 <= i <=n && i <= (data_read-2)/12;
@ -402,6 +446,10 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
X*/
for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++)
{
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
const TIFFDirEntry *entry=&entries[i];
/*@ assert 0 <= i < n; */
/*@ assert \valid_read(entry); */
@ -454,28 +502,38 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
case TIFFTAG_TILEOFFSETS: tile_offsets=tmp; break;
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
#ifndef __FRAMAC__
{
const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
#endif
break;
case TIFFTAG_SUBIFD:
#ifndef __FRAMAC__
{
const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
#endif
break;
#ifdef ENABLE_TIFF_MAKERNOTE
case EXIFTAG_MAKERNOTE:
@ -515,15 +573,21 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp));
#endif
#ifndef __FRAMAC__
/*@
@ loop invariant 0 <= j <= nbr <=32;
@ loop variant nbr-j;
@*/
/*X
X loop invariant 0 <= j <= nbr <=32;
X loop variant nbr-j;
X*/
for(j=0; j<nbr; j++)
{
const uint64_t new_offset=file_check_tiff_be_aux(fr, be32(subifd_offsetp[j]), depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
const uint64_t new_offset=file_check_tiff_be_aux(fr, be32(subifd_offsetp[j]), depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
{
return TIFF_ERROR;
@ -531,7 +595,6 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < new_offset)
max_offset = new_offset;
}
#endif
}
break;
case TIFFTAG_STRIPOFFSETS:
@ -578,22 +641,16 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < tmp)
max_offset=tmp;
}
if(data_read < 6)
return max_offset;
/*@ assert data_read >= 6; */
#ifndef __FRAMAC__
if ( 2 + n*12 + 4 <= (unsigned int)data_read)
{
/*@ assert n <= (data_read - 6) /12; */
const uint32_t *tiff_next_diroff=(const uint32_t *)&entries[n];
if(be32(*tiff_next_diroff) > 0)
{
const uint64_t new_offset=file_check_tiff_be_aux(fr, be32(*tiff_next_diroff), depth+1, count+1);
if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
const unsigned int offset_ptr_offset=2+12*n;
const uint64_t new_offset=file_check_tiff_be_aux_next(fr, depth, count, buffer, data_read, offset_ptr_offset);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
#endif
return max_offset;
}

115
src/file_tiff_le.c
View file

@ -262,6 +262,7 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
data_read=fread(buffer, 1, sizeof(buffer), in);
if(data_read<2)
return TIFF_ERROR;
/*@ assert data_read >= 2; */
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, sizeof(buffer));
#endif
@ -339,16 +340,55 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
#endif
#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg)
static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
/*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
@ requires \separated(&errno, fr);
@ requires \valid_read(buffer + (0 .. buffer_size - 1));
@ ensures \valid(fr);
@ ensures \valid(fr->handle);
@ ensures valid_read_string(fr->extension);
@
*/
@*/
static uint64_t file_check_tiff_le_aux_next(file_recovery_t *fr, const unsigned int depth, const unsigned int count, const unsigned char *buffer, const unsigned int buffer_size, const unsigned int offset_ptr_offset)
{
if(buffer_size < 4)
return 0;
/*@ assert buffer_size >= 4; */
if(offset_ptr_offset > buffer_size-4)
return 0;
{
/*@ assert offset_ptr_offset <= buffer_size - 4; */
/*@ assert offset_ptr_offset + 4 <= buffer_size; */
/*@ assert \valid_read(buffer + (0 .. offset_ptr_offset + 4 - 1)); */
const unsigned char *ptr_offset=&buffer[offset_ptr_offset];
/*@ assert \valid_read(ptr_offset + (0 .. 4 - 1)); */
const uint32_t *ptr32_offset=(const uint32_t *)ptr_offset;
/*@ assert \valid_read(ptr32_offset); */
const unsigned int next_diroff=le32(*ptr32_offset);
if(next_diroff == 0)
return 0;
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
return file_check_tiff_le_aux(fr, next_diroff, depth+1, count+1);
}
}
/*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
@ requires \separated(&errno, fr);
@ ensures \valid(fr);
@ ensures \valid(fr->handle);
@ ensures valid_read_string(fr->extension);
@*/
static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
{
unsigned char buffer[8192];
@ -372,6 +412,9 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
const TIFFDirEntry *entry_strip_bytecounts=NULL;
const TIFFDirEntry *entry_tile_offsets=NULL;
const TIFFDirEntry *entry_tile_bytecounts=NULL;
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
#ifdef DEBUG_TIFF
log_info("file_check_tiff_le_aux(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
#endif
@ -398,6 +441,7 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
#endif
if(n==0)
return TIFF_ERROR;
/*@ assert 0 < n <= 65535; */
/*@ assert sizeof(TIFFDirEntry)==12; */
/*X
X loop invariant 0 <= i <=n && i <= (data_read-2)/12;
@ -405,6 +449,10 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
X*/
for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++)
{
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
const TIFFDirEntry *entry=&entries[i];
/*@ assert 0 <= i < n; */
/*@ assert \valid_read(entry); */
@ -458,16 +506,21 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
case TIFFTAG_TILEOFFSETS: tile_offsets=tmp; break;
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
#ifndef __FRAMAC__
{
const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
#endif
break;
case TIFFTAG_SUBIFD:
if(fr->extension == extension_arw)
@ -476,17 +529,22 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < tmp)
max_offset=tmp;
}
#ifndef __FRAMAC__
else
{
const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
#endif
break;
#ifdef ENABLE_TIFF_MAKERNOTE
case EXIFTAG_MAKERNOTE:
@ -526,15 +584,21 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp));
#endif
#ifndef __FRAMAC__
/*@
@ loop invariant 0 <= j <= nbr <=32;
@ loop variant nbr-j;
@*/
/*X
X loop invariant 0 <= j <= nbr <=32;
X loop variant nbr-j;
X*/
for(j=0; j<nbr; j++)
{
const uint64_t new_offset=file_check_tiff_le_aux(fr, le32(subifd_offsetp[j]), depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
const uint64_t new_offset=file_check_tiff_le_aux(fr, le32(subifd_offsetp[j]), depth+1, 0);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
{
return TIFF_ERROR;
@ -542,7 +606,6 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < new_offset)
max_offset = new_offset;
}
#endif
}
break;
case TIFFTAG_STRIPOFFSETS:
@ -589,22 +652,16 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < tmp)
max_offset=tmp;
}
if(data_read < 6)
return max_offset;
/*@ assert data_read >= 6; */
#ifndef __FRAMAC__
if ( 2 + n*12 + 4 <= (unsigned int)data_read)
{
/*@ assert n <= (data_read - 6) /12; */
const uint32_t *tiff_next_diroff=(const uint32_t *)&entries[n];
if(le32(*tiff_next_diroff) > 0)
{
const uint64_t new_offset=file_check_tiff_le_aux(fr, le32(*tiff_next_diroff), depth+1, count+1);
if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
const unsigned int offset_ptr_offset=2+12*n;
const uint64_t new_offset=file_check_tiff_le_aux_next(fr, depth, count, buffer, data_read, offset_ptr_offset);
/*@ assert \valid(fr); */
/*@ assert \valid(fr->handle); */
/*@ assert \valid_read(&fr->extension); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
#endif
return max_offset;
}